fmrisc.ProgramExplorer.Semantics

Class LogicEnvironment

java.lang.Object

fmrisc.ProgramExplorer.Semantics.LogicEnvironment

public final class LogicEnvironment
extends java.lang.Object

An environment giving meaning to identifiers in the logic context.

Field Summary

Fields

Modifier and Type	Field and Description
PackageSymbol	top

Constructor Summary

Constructors

Constructor and Description
LogicEnvironment(ErrorStream error) Create a new and empty environment.
LogicEnvironment(PackageSymbol top, ErrorStream error) Create a new environment at top-level.
LogicEnvironment(TheorySymbol tsymbol, ErrorStream error) Create a new environment from theory symbol.

Method Summary

Methods

Modifier and Type	Method and Description
void	enter() Enter a new scope.
void	exit() Exit a scope.
Declaration[][]	getDeclarations() Get sequence of ordered declarations sequences where declarations in a later sequence supersede the previous declarations.
FormulaSymbol	getFormulaSymbol(Identifier name) Returns formula symbol associated to name.
java.util.Collection<FormulaSymbol>	getFormulaSymbols() Get all formula symbols.
java.util.Vector<TheorySymbol>	getTheories() Get theories that may be referenced in environment in dependence order.
TypeSymbol	getTypeSymbol(Identifier name) Returns type symbol associated to name.
TypeSymbol	getTypeSymbol(Reference ref) Get type denoted by reference in current environment
java.util.Collection<TypeSymbol>	getTypeSymbols() Get all type symbols.
ValueSymbol	getValueSymbol(Identifier name) Returns value symbol associated to name.
ValueSymbol	getValueSymbol(Reference ref) Get value denoted by reference in current environment
java.util.Collection<ValueSymbol>	getValueSymbols() Get all value symbols.
FormulaSymbol	putFormula(Identifier name, Formula formula, FormulaDefinition decl, TheorySymbol theory) Attempts to put formula into value table
TypeSymbol	putType(Identifier name, Type type, TypeDeclaration decl) Attempts to put type into type table.
ValueSymbol	putValue(Identifier name, Type type, Declaration decl) Attempts to put value into value table
java.util.Vector<TheorySymbol>	setTheories(PackageSymbol psymbol, TheorySymbol baseTheory, TheorySymbol classTheory, Import[] imports, Name[] tnames) Set in this environment the theories that may be referenced (ensuring that they are indeed read from file).

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

top

public PackageSymbol top

Constructor Detail

LogicEnvironment

public LogicEnvironment(PackageSymbol top,
                ErrorStream error)

Create a new environment at top-level.

Parameters:

top - the top-level package for looking up global names

error - the stream for printing error messages.

LogicEnvironment

public LogicEnvironment(TheorySymbol tsymbol,
                ErrorStream error)

Create a new environment from theory symbol.

Parameters:

tsymbol - the symbol from which to create the environment

error - the stream for printing error messages.

LogicEnvironment

public LogicEnvironment(ErrorStream error)

Create a new and empty environment.

Parameters:

error - the error stream to write to.

Method Detail

setTheories

public java.util.Vector<TheorySymbol> setTheories(PackageSymbol psymbol,
                                         TheorySymbol baseTheory,
                                         TheorySymbol classTheory,
                                         Import[] imports,
                                         Name[] tnames)

Set in this environment the theories that may be referenced (ensuring that they are indeed read from file).

Parameters:

psymbol - the package in which this environment is processed.

baseTheory - the always referable base theory (may be null)

classTheory - the theory of the current class (may be null)

imports - the import statements to be processed.

tnames - the theory names that may be referenced.

Returns:

the vector of theory symbols corresponding to tnames in topological dependence order (null, if an error occurred).

getTheories

public java.util.Vector<TheorySymbol> getTheories()

Get theories that may be referenced in environment in dependence order.

Returns:

the collection of theories.

enter

public void enter()

Enter a new scope. All changes done to the environment after enter() will be undone after exit().

exit

public void exit()

Exit a scope. All changes done after the after the last enter() are undone

putType

public TypeSymbol putType(Identifier name,
                 Type type,
                 TypeDeclaration decl)

Attempts to put type into type table.

Parameters:

name - the name of the type

type - the type associated to the name

decl - the declaration of the type

Returns:

the constructed type symbol (null, if type table already contained a symbol with the denoted name)

getTypeSymbol

public TypeSymbol getTypeSymbol(Identifier name)

Returns type symbol associated to name.

Parameters:

name - the name of the type.

Returns:

the type symbol associated to the name (may be null).

getTypeSymbols

public java.util.Collection<TypeSymbol> getTypeSymbols()

Get all type symbols.

Returns:

collection of all type symbols declared in current scope.

putValue

public ValueSymbol putValue(Identifier name,
                   Type type,
                   Declaration decl)

Attempts to put value into value table

Parameters:

name - the name of the value

type - the type associated to the value

decl - the declaration of the value

Returns:

the constructed symbol (null, if value table already contained a symbol with the denoted name)

getValueSymbol

public ValueSymbol getValueSymbol(Identifier name)

Returns value symbol associated to name.

Parameters:

name - the name of the value.

Returns:

the value symbol associated to the name (may be null).

getValueSymbols

public java.util.Collection<ValueSymbol> getValueSymbols()

Get all value symbols.

Returns:

collection of all value symbols declared in current scope.

putFormula

public FormulaSymbol putFormula(Identifier name,
                       Formula formula,
                       FormulaDefinition decl,
                       TheorySymbol theory)

Attempts to put formula into value table

Parameters:

name - the name of the formula

formula - the formula itself

decl - the formula definition.

theory - the theory in which the formula occurs (may be null)

Returns:

the constructed symbol (null, if formula table already contained a symbol with the denoted name)

getFormulaSymbol

public FormulaSymbol getFormulaSymbol(Identifier name)

Returns formula symbol associated to name.

Parameters:

name - the name of the formula

Returns:

the formula symbol associated to the name (may be null).

getFormulaSymbols

public java.util.Collection<FormulaSymbol> getFormulaSymbols()

Get all formula symbols.

Returns:

collection of all formula symbols declared in current scope.

getDeclarations

public Declaration[][] getDeclarations()

Get sequence of ordered declarations sequences where declarations in a later sequence supersede the previous declarations.

Returns:

the sequence of declaration sequences.

getValueSymbol

public ValueSymbol getValueSymbol(Reference ref)

Get value denoted by reference in current environment

Parameters:

ref - the reference

Returns:

the value symbol respectively null, if an error occurred.

getTypeSymbol

public TypeSymbol getTypeSymbol(Reference ref)

Get type denoted by reference in current environment

Parameters:

ref - the reference

Returns:

the type symbol respectively null, if an error occurred.