Uses of Interface
fmrisc.Syntax.Type

Packages that use Type

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

Uses of Type in fmrisc.Communication

Methods in fmrisc.Communication that return Type

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.Communication with parameters of type Type

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

Methods in fmrisc.ProofNavigator that return Type

Type	PNParser.typeExp()
Type	PNParser.typeExpBase()

Uses of Type in fmrisc.Proving.CVCL

Methods in fmrisc.Proving.CVCL that return Type

Type	CVCLParser.typeExp()
Type	CVCLParser.typeExpBase()

Uses of Type in fmrisc.Semantics

Methods in fmrisc.Semantics that return Type

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 Type	Checking.getBooleanType() Get canonical type BOOLEAN
static Type	Checking.getIntType() Get canonical type INT
static Type	Checking.getNatType() Get canonical type NAT
Type	ValueSymbol.getType() Return type of symbol.
Type	TypeSymbol.getType() Return type of symbol.
Type	TypeExpression.getType() get type
Type	Environment.getType(Identifier name) returns canonical type associated to key type equality implies pointer equality of types.
Type	TypeTable.getType(Identifier key) returns canonical type associated to key type equality implies pointer equality of types.
static Type	Checking.process(Expression value) type check value
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.Semantics with parameters of type Type

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	FreeVariables.compute(Type type) 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
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	ValueSymbol.setType(Type type) Set type of symbol.
void	TypeSymbol.setType(Type type) Set type of symbol to type.
void	TypeExpression.setType(Type type) set type
static Type	Checking.subType(Type type0, Type type1) return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.

Constructors in fmrisc.Semantics with parameters of type Type

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

Uses of Type in fmrisc.Syntax

Classes in fmrisc.Syntax that implement Type

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.Syntax that return Type

Type	SubType.getBase() returns base type
Type[]	TupleType.getBase() returns base types
Type	ArrayType.getBase() returns base type
Type	LetType.getBase() get 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	TypedIdentifier.getType() returns identifier 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	RecordType.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
Type	Reference.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	ArrayType.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	LetType.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	FunctionType.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 v) converts vector v of Type objects to Type array

Methods in fmrisc.Syntax with parameters of type Type

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
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.

Constructors in fmrisc.Syntax with parameters of type Type

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.