fmrisc.ProofNavigator.Syntax

Class Reference

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.Identifier

fmrisc.ProofNavigator.Syntax.Reference

All Implemented Interfaces:

AST, Expression, Type

public final class Reference
extends Identifier
implements Type, Expression

Handling of identifiers used in declarations

Constructor Summary

Constructors

Constructor and Description
Reference(java.lang.String name) construct reference from name (symbol is set to null)
Reference(java.lang.String name, Symbol symbol) construct reference from name and symbol

Method Summary

Methods

Modifier and Type	Method and Description
AST	accept(ASTVisitor visitor) Accept visitor for a visit.
int	getPriority() get binding level for printing (lower numbers mean greater binding power)
Symbol	getSymbol() returns symbol associated to reference
Expression	instantiate() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
Type	instantiateType() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
void	print(java.io.PrintWriter out) Prints text representation on out (without new line termination).
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).
void	setSymbol(Symbol symbol) sets symbol associated to reference

Methods inherited from class fmrisc.ProofNavigator.Syntax.Identifier

getName, printPriority, setName

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTBase

printParens, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProofNavigator.Syntax.Expression

printPriority

Methods inherited from interface fmrisc.ProofNavigator.Syntax.AST

printParens, toString

Constructor Detail

Reference

public Reference(java.lang.String name)

construct reference from name (symbol is set to null)

Parameters:

name - the text representation of the reference

Reference

public Reference(java.lang.String name,
         Symbol symbol)

construct reference from name and symbol

Parameters:

name - the text representation of the reference

symbol - the symbol associated to the reference

Method Detail

getSymbol

public Symbol getSymbol()

returns symbol associated to reference

Returns:

the symbol

setSymbol

public void setSymbol(Symbol symbol)

sets symbol associated to reference

Parameters:

symbol - the symbol

getPriority

public int getPriority()

get binding level for printing (lower numbers mean greater binding power)

Specified by:

getPriority in interface Expression

Returns:

the priority level

instantiate

public Expression instantiate()

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

Specified by:

instantiate in interface Expression

Returns:

the instantiated copy

instantiateType

public Type instantiateType()

return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

Specified by:

instantiateType in interface Type

Returns:

the instantiated copy

printCore

public void printCore(java.io.PrintWriter out)

Prints text representation on out (without new line termination).

Specified by:

printCore in interface AST

Overrides:

printCore in class Identifier

Parameters:

out - the stream on which the text is written

print

public void print(java.io.PrintWriter out)

Prints text representation on out (without new line termination). Overrides ASTBase.print such that parentheses are never printed around the number.

Specified by:

print in interface AST

Overrides:

print in class Identifier

Parameters:

out - the stream on which the text is written

accept

public AST accept(ASTVisitor visitor)

Accept visitor for a visit.

Specified by:

accept in interface AST

Parameters:

visitor - the visitor who is accepted by this node.

Returns:

the result of the visit (may be null).