Package | Description |
---|---|
fmrisc.ProofNavigator.Proving | |
fmrisc.ProofNavigator.Proving.CVCL | |
fmrisc.ProofNavigator.Semantics | |
fmrisc.ProofNavigator.Syntax |
Modifier and Type | Method and Description |
---|---|
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.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
CVCL.getExternalName(ValueDeclIdentifier ident)
create CVCL identifier from given name
|
Modifier and Type | Method and Description |
---|---|
ValueDeclIdentifier |
ValueSymbol.getValueDeclIdentifier()
Return identifier of symbol.
|
Modifier and Type | Method and Description |
---|---|
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
|
Constructor and Description |
---|
ValueSymbol(ValueDeclIdentifier ident)
Construct value symbol from ident (type and value are both null).
|
Modifier and Type | Method and Description |
---|---|
ValueDeclIdentifier[] |
ArrayTerm.getFree()
Get free variables
|
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.
|
Modifier and Type | Method and Description |
---|---|
static Reference |
Construct.reference(ValueDeclIdentifier ident)
construct reference from value declaration identifier.
|
void |
ArrayTerm.setFree(ValueDeclIdentifier[] v)
Set free variables
|
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.
|
Constructor and Description |
---|
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.
|