Uses of Interface
fmrisc.ProofNavigator.Syntax.Type

Packages that use Type

Package	Description
fmrisc.ProofNavigator
fmrisc.ProofNavigator.Communication
fmrisc.ProofNavigator.Proving.CVCL
fmrisc.ProofNavigator.Semantics
fmrisc.ProofNavigator.Syntax

Uses of Type in fmrisc.ProofNavigator

Methods in fmrisc.ProofNavigator that return Type

Modifier and Type	Method and Description
Type	PNParser.typeExp()
Type	PN2Parser.typeExp()
Type	PNParser.typeExpBase()
Type	PN2Parser.typeExpBase()

Uses of Type in fmrisc.ProofNavigator.Communication

Methods in fmrisc.ProofNavigator.Communication that return Type

Modifier and Type	Method and Description
static Type	Store.toType(org.w3c.dom.Node node) Convert DOM node to type.
static Type	OpenMath.toType(nl.tue.win.riaca.openmath.lang.OMObject om) Convert OpenMath type to AST.

Methods in fmrisc.ProofNavigator.Communication with parameters of type Type

Modifier and Type	Method and Description
void	MathML.appendType(org.w3c.dom.Node parent, Type object) Convert type to DOM representation of HTML/MathML markup.
void	PrettyPrinter.print(Type type) Pretty-print type.

Uses of Type in fmrisc.ProofNavigator.Proving.CVCL

Methods in fmrisc.ProofNavigator.Proving.CVCL that return Type

Modifier and Type	Method and Description
Type	CVCLParser.typeExp()
Type	CVCLParser.typeExpBase()

Uses of Type in fmrisc.ProofNavigator.Semantics

Methods in fmrisc.ProofNavigator.Semantics that return Type

Modifier and Type	Method and Description
static Type	Checking.canonical(Type type) Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
static Type	Checking.canonicalTcc(Type type) Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
Type	TypeExpression.getType() get type
Type	TypeSymbol.getType() Return type of symbol.
Type	ValueSymbol.getType() Return type of symbol.
Type	TypeTable.getType(Identifier key) returns canonical type associated to key type equality implies pointer equality of types.
Type	Environment.getType(Identifier name) returns canonical type associated to key type equality implies pointer equality of types.
static Type	Checking.processDefinitionTerm(Expression value) type check definition term with potential first-order type check
static Type	Checking.processFormula(Expression value) type check value without first-order type check
static Type	Checking.processTerm(Expression value) type check term with potential first-order type check
static Type	Checking.processTermOrFormula(Expression value) type check term with potential first-order type check
static Type	Checking.subType(Type type0, Type type1) return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.

Methods in fmrisc.ProofNavigator.Semantics with parameters of type Type

Modifier and Type	Method and Description
static Type	Checking.canonical(Type type) Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
static Type	Checking.canonicalTcc(Type type) Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
static TypeExpression	Checking.clearSubtypes(Type type, Expression exp) return version of type where subtypes and subranges (including NAT) are replaced by their base types; the corresponding constraints are returned as a formula which a corresponding expression exp has to fulfill
static java.util.Vector<ValueSymbol>	FreeVariables.compute(Type type, boolean constants) Compute free variables of type.
static boolean	Checking.hasType(Expression exp, Type etype, Type type, boolean tcc) returns true iff expr of type etype matches type.
static boolean	Checking.isBoolean(Type type) checks if type equals BOOLEAN
static boolean	Checking.isInt(Type type) checks if type equals INT
static boolean	Checking.isNat(Type type) checks if type equals NAT
static boolean	Checking.isReal(Type type) checks if type equals REAL
TypeSymbol	TypeTable.put(TypeDeclIdentifier key, Type type) put type in type table
ValueSymbol	ValueTable.put(ValueDeclIdentifier name, Type type, Expression value, int depth) put named value in value table
TypeSymbol	Environment.putType(TypeDeclIdentifier name, Type type) put type in type table
ValueSymbol	Environment.putValue(ValueDeclIdentifier name, Type type, Expression value) put named value in value table
void	TypeExpression.setType(Type type) set type
void	TypeSymbol.setType(Type type) Set type of symbol to type.
void	ValueSymbol.setType(Type type) Set type of symbol.
static Type	Checking.subType(Type type0, Type type1) return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.
static boolean	Checking.validDefinitionType(Type type) decide whether definition type is first order, i.e., - a function type is only allowed at the top level - the type BOOLEAN is only allowed at the top level or as the range of the function type
static boolean	Checking.validTermType(Type type) decide whether type does not contain a function type or BOOLEAN.

Constructors in fmrisc.ProofNavigator.Semantics with parameters of type Type

Constructor and Description
TypeExpression(Type type, Expression exp) Construct pair of type and exp

Uses of Type in fmrisc.ProofNavigator.Syntax

Classes in fmrisc.ProofNavigator.Syntax that implement Type

Modifier and Type	Class and Description
class	ArrayType Handling of array types.
class	AtomicType Handling of atomic types.
class	FunctionType Handling of function type expressions
class	LetType Handling of terms with local bindings.
class	RecordType Handling of record types.
class	Reference Handling of identifiers used in declarations
class	SubrangeType Subranges of integers.
class	SubType Predicated subtypes.
class	TupleType Handling of tuple types.
class	TypeBase Base class of type expressions.

Methods in fmrisc.ProofNavigator.Syntax that return Type

Modifier and Type	Method and Description
Type	SubType.getBase() returns base type
Type	LetType.getBase() get base type
Type[]	TupleType.getBase() returns base types
Type	ArrayType.getBase() returns base type
Type[]	FunctionType.getDomain() returns domain of type
Type	ArrayType.getIndex() returns index type
Type	FunctionType.getRange() returns range of type
Type	ValueDeclaration.getType() returns declaration type
Type	TimesTerm.getType() get result type
Type	TypedIdentifier.getType() returns identifier type
Type	PowerTerm.getType() get result type
Type	TypeDeclaration.getType() returns declaration type
Type	SubType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	LetType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	AtomicType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	FunctionType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	TupleType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	RecordType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	Type.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	ArrayType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	Reference.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	SubrangeType.instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
static Type[]	ASTUtil.toTypeArray(java.util.Vector<Type> v) converts vector v of Type objects to Type array

Methods in fmrisc.ProofNavigator.Syntax with parameters of type Type

Modifier and Type	Method and Description
static ArrayType	Construct.arrayType(Type index, Type base) construct array type with denoted index type and base type.
static FunctionType	Construct.functionType(Type[] domain, Type range) construct function type from types domain and range.
static FunctionType	Construct.functionType(Type[] domain, Type range) construct function type from types domain and range.
static LetType	Construct.letType(TypeDeclaration[] declarations, Type base) construct let type of declarations and base type
void	SubType.setBase(Type base) set base type
void	TimesTerm.setType(Type t) set result type
void	PowerTerm.setType(Type t) set result type
static TupleType	Construct.tupleType(Type[] base) construct tuple type with denoted base types.
static TypeDeclaration	Construct.typeDeclaration(TypeDeclIdentifier name, Type type) construct type declaration with denoted name and type.
static TypedIdentifier	Construct.typedIdentifier(ValueDeclIdentifier identifier, Type type) construct typed identifier from identifier and type.
static ValueDeclaration	Construct.valueDeclaration(ValueDeclIdentifier name, Type type, Expression value) construct value declaration with denoted name, type and value.

Method parameters in fmrisc.ProofNavigator.Syntax with type arguments of type Type

Modifier and Type	Method and Description
static Type[]	ASTUtil.toTypeArray(java.util.Vector<Type> v) converts vector v of Type objects to Type array

Constructors in fmrisc.ProofNavigator.Syntax with parameters of type Type

Constructor and Description
ArrayType(Type index, Type base) construct array type with denoted index type and base type.
FunctionType(Type[] domain, Type range) construct function type from domain and range.
FunctionType(Type[] domain, Type range) construct function type from domain and range.
LetType(TypeDeclaration[] declarations, Type base) Construct let types of declarations and base types.
TupleType(Type[] base) construct record type with denoted base types.
TypeDeclaration(TypeDeclIdentifier name, Type type) construct type declaration with denoted name and type.
TypedIdentifier(ValueDeclIdentifier identifier, Type type) construct typed identifier from identifier and type.
ValueDeclaration(ValueDeclIdentifier name, Type type, Expression value) construct value declaration with denoted name, type and value.