fmrisc.ProgramExplorer.Semantics

Class TheorySymbol

java.lang.Object

fmrisc.ProgramExplorer.Semantics.SymbolBase

fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase

fmrisc.ProgramExplorer.Semantics.TheorySymbol

All Implemented Interfaces:

GlobalSymbol, Symbol

public final class TheorySymbol
extends GlobalSymbolBase

A symbol denoting a theory.

Constructor Summary

Constructors

Constructor and Description
TheorySymbol(ClassSymbol csymbol) Construct theory symbol for class theory for later processing (no declaration is provided yet).
TheorySymbol(ClassSymbol csymbol, Identifier name, TheoryDeclaration decl, ErrorStream error) Construct local theory symbol from declaration.
TheorySymbol(PackageSymbol psymbol, Identifier name, TheoryDeclaration decl, ErrorStream error) Construct theory symbol from declaration.
TheorySymbol(PackageSymbol psymbol, Identifier name, TheoryReader reader) Construct theory symbol from reader.

Method Summary

Modifier and Type	Method and Description
static void	add(java.util.Collection<TheorySymbol> symbols, java.util.Collection<TheorySymbol> symbols0) Add symbols to collection of symbols (if it is not there).
static void	add(java.util.Collection<TheorySymbol> symbols, TheorySymbol symbol) Add symbol to collection of symbols (if it is not there).
ClassSymbol	getClassSymbol() Returns class from which theory is derived (if any).
TheoryDeclaration	getDeclaration() Get the declaration of the theory.
SymbolTable<FormulaSymbol>	getFormulas() Get set of formulas of this class.
TaskFolder	getFormulaTasks() Get the formula tasks.
ClassSymbol	getHostClass() Get the class for which this theory is local.
LogicTypeTable	getLogicTypeTable() Get type table of class.
PackageSymbol	getPackage() Get package of theory.
java.util.Collection<Symbol>	getReferencedUnits() Get symbols of units referenced by this unit.
Source	getSource() Get source of theory (respectively of associated class).
TaskFolder	getTCCs() Get the type checking conditions.
SymbolTable<TypeSymbol>	getTypes() Get set of types of this theory.
TypeTable	getTypeTable() Get type table of theory.
SymbolTable<ValueSymbol>	getValues() Get set of values of this theory.
boolean	hasErrors() Show whether class has errors.
boolean	isFromClass() Returns true if theory is derived from class.
boolean	isRead() Returns true if theory has been read, i.e.
void	print(java.io.PrintWriter out) Print symbol on output stream.
boolean	read(ErrorStream error) Update declaration from reader or derive it from class symbol.
void	reset() Reset symbol.
void	setDeclaration(TheoryDeclaration decl, ErrorStream error) Set and process new theory declaration
void	setErrors(boolean status) Set error status.

Methods inherited from class fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase

getLongName

Methods inherited from class fmrisc.ProgramExplorer.Semantics.SymbolBase

getName

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProgramExplorer.Semantics.Symbol

getName

Constructor Detail

TheorySymbol

public TheorySymbol(PackageSymbol psymbol,
                    Identifier name,
                    TheoryReader reader)

Construct theory symbol from reader.

Parameters:

psymbol - the symbol of the package holding the theory.

name - the name of the theory.

reader - the reader for getting the declaration.

TheorySymbol

public TheorySymbol(ClassSymbol csymbol)

Construct theory symbol for class theory for later processing (no declaration is provided yet).

Parameters:

csymbol - the symbol of the class.

TheorySymbol

public TheorySymbol(PackageSymbol psymbol,
                    Identifier name,
                    TheoryDeclaration decl,
                    ErrorStream error)

Construct theory symbol from declaration.

Parameters:

psymbol - the symbol of the package holding the theory.

name - the name of the theory.

decl - the theory declaration.

error - the error stream to print messages to

TheorySymbol

public TheorySymbol(ClassSymbol csymbol,
                    Identifier name,
                    TheoryDeclaration decl,
                    ErrorStream error)

Construct local theory symbol from declaration.

Parameters:

csymbol - the symbol of the class holding the theory.

name - the name of the theory.

decl - the theory declaration.

error - the error stream to print messages to

Method Detail

getPackage

public PackageSymbol getPackage()

Get package of theory.

Returns:

the theory's package

getSource

public Source getSource()

Get source of theory (respectively of associated class).

Returns:

the theory's source.

getTypeTable

public TypeTable getTypeTable()

Get type table of theory.

Returns:

the theory's type table.

isRead

public boolean isRead()

Returns true if theory has been read, i.e. its values are defined.

Returns:

true if theory has been read.

isFromClass

public boolean isFromClass()

Returns true if theory is derived from class.

Returns:

true if theory is derived from class.

getClassSymbol

public ClassSymbol getClassSymbol()

Returns class from which theory is derived (if any).

Returns:

the class symbol (may be null).

read

public boolean read(ErrorStream error)

Update declaration from reader or derive it from class symbol.

Parameters:

error - the error stream on which to print any messages.

Returns:

true if everything went fine, false if an error occurred.

setDeclaration

public void setDeclaration(TheoryDeclaration decl,
                           ErrorStream error)

Set and process new theory declaration

Parameters:

decl - the new theory declaration (updating any previous one)

error - the error stream on which to print any messages.

hasErrors

public boolean hasErrors()

Show whether class has errors.

Returns:

true if class has errors

setErrors

public void setErrors(boolean status)

Set error status.

Parameters:

status - true iff errors, false otherwise.

reset

public void reset()

Reset symbol.

getDeclaration

public TheoryDeclaration getDeclaration()

Get the declaration of the theory.

Specified by:

getDeclaration in interface Symbol

Overrides:

getDeclaration in class SymbolBase

Returns:

the declaration (may be null)

getTypes

public SymbolTable<TypeSymbol> getTypes()

Get set of types of this theory.

Returns:

the set of types.

getValues

public SymbolTable<ValueSymbol> getValues()

Get set of values of this theory.

Returns:

the set of types.

getFormulas

public SymbolTable<FormulaSymbol> getFormulas()

Get set of formulas of this class.

Returns:

the set of types.

getLogicTypeTable

public LogicTypeTable getLogicTypeTable()

Get type table of class.

Returns:

the class's type table.

print

public void print(java.io.PrintWriter out)

Print symbol on output stream.

Parameters:

out - the output stream.

getTCCs

public TaskFolder getTCCs()

Get the type checking conditions.

Returns:

the folder holding the type checking conditions.

getFormulaTasks

public TaskFolder getFormulaTasks()

Get the formula tasks.

Returns:

the folder holding the formulas to be proved.

getReferencedUnits

public java.util.Collection<Symbol> getReferencedUnits()

Get symbols of units referenced by this unit.

Returns:

the collection of symbols.

add

public static void add(java.util.Collection<TheorySymbol> symbols,
                       TheorySymbol symbol)

Add symbol to collection of symbols (if it is not there).

Parameters:

symbols - the symbol collection to which to add.

symbol - the symbol to be added.

add

public static void add(java.util.Collection<TheorySymbol> symbols,
                       java.util.Collection<TheorySymbol> symbols0)

Add symbols to collection of symbols (if it is not there).

Parameters:

symbols - the symbol collection to which to add.

symbols0 - the symbols to be added.

getHostClass

public ClassSymbol getHostClass()

Get the class for which this theory is local.

Returns:

the class (null, if the theory is not local).