Uses of Class
fmrisc.Syntax.ValueDeclIdentifier

Packages that use ValueDeclIdentifier

fmrisc.Proving
fmrisc.Proving.CVCL
fmrisc.Semantics
fmrisc.Syntax

Uses of ValueDeclIdentifier in fmrisc.Proving

Methods in fmrisc.Proving with parameters of type ValueDeclIdentifier

static Expression	ProofUtil.bind(ValueDeclIdentifier ident, Expression value, Expression body) Construct expression that binds ident to value in body.
static Expression	Substitute.substitute(Expression exp, ValueDeclIdentifier[] ident, Expression[] subst, boolean repeat) Return expression with simultaneous variable substitutions performed.

Uses of ValueDeclIdentifier in fmrisc.Proving.CVCL

Methods in fmrisc.Proving.CVCL with parameters of type ValueDeclIdentifier

static java.lang.String

CVCL.getExternalName(ValueDeclIdentifier ident) create CVCL identifier from given name

Uses of ValueDeclIdentifier in fmrisc.Semantics

Methods in fmrisc.Semantics that return ValueDeclIdentifier

ValueDeclIdentifier

ValueSymbol.getValueDeclIdentifier() Return identifier of symbol.

Methods in fmrisc.Semantics with parameters of type ValueDeclIdentifier

void	Environment.put(ValueDeclIdentifier ident) add the symbol associated to ident to current environment
ValueSymbol	ValueTable.put(ValueDeclIdentifier name, Type type, Expression value, int depth) put named value in value table
ValueSymbol	Environment.putValue(ValueDeclIdentifier name, Type type, Expression value) put named value in value table

Constructors in fmrisc.Semantics with parameters of type ValueDeclIdentifier

ValueSymbol(ValueDeclIdentifier ident)
Construct value symbol from ident (type and value are both null).

Uses of ValueDeclIdentifier in fmrisc.Syntax

Methods in fmrisc.Syntax that return ValueDeclIdentifier

ValueDeclIdentifier	TypedIdentifier.getIdentifier() returns identifier name
ValueDeclIdentifier	ValueDeclIdentifier.getSubstitution() returns substitution identifier for instantiation
ValueDeclIdentifier	ValueDeclaration.getValueDeclIdentifier() returns declaration name
ValueDeclIdentifier	ValueDeclIdentifier.instantiate() returns instantiated copy of identifier
static ValueDeclIdentifier	Construct.valueDeclIdentifier(java.lang.String name) construct value declaration identifier with denoted name.

Methods in fmrisc.Syntax with parameters of type ValueDeclIdentifier

static Reference	Construct.reference(ValueDeclIdentifier ident) construct reference from value declaration identifier.
void	ValueDeclIdentifier.setSubstitution(ValueDeclIdentifier substitution) set substitution expression for instantiation
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 ValueDeclIdentifier

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.