fmrisc.ProofNavigator.Syntax

Class FormulaDeclaration

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.DeclarationBase

fmrisc.ProofNavigator.Syntax.FormulaDeclaration

All Implemented Interfaces:

AST, Declaration

Direct Known Subclasses:

AxiomDeclaration

public class FormulaDeclaration
extends DeclarationBase

Handling of type declarations.

Constructor Summary

Constructors

Constructor and Description
FormulaDeclaration(FormulaDeclIdentifier name, Expression formula) construct formula declaration with denoted name and formula

Method Summary

Modifier and Type	Method and Description
AST	accept(ASTVisitor visitor) Accept visitor for a visit.
Expression	getFormula() returns declaration formula
FormulaDeclIdentifier	getFormulaDeclIdentifier() returns declaration name
Identifier	getIdentifier() returns declaration name
Symbol	getSymbol() returns symbol
void	printCore(java.io.PrintWriter out) Prints text representation of tree on out (without new line termination).

Methods inherited from class fmrisc.ProofNavigator.Syntax.DeclarationBase

print

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.AST

printParens, toString

Constructor Detail

FormulaDeclaration

public FormulaDeclaration(FormulaDeclIdentifier name,
                          Expression formula)

construct formula declaration with denoted name and formula

Parameters:

name - the declared name

formula - the formula associated to the name

Method Detail

getFormulaDeclIdentifier

public FormulaDeclIdentifier getFormulaDeclIdentifier()

returns declaration name

Returns:

the name

getIdentifier

public Identifier getIdentifier()

returns declaration name

Returns:

the name

getFormula

public Expression getFormula()

returns declaration formula

Returns:

the formula

printCore

public void printCore(java.io.PrintWriter out)

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

Specified by:

printCore in interface AST

Specified by:

printCore in class ASTBase

Parameters:

out - the stream on which the text is written

getSymbol

public Symbol getSymbol()

returns symbol

Returns:

the symbol (null, if not yet determined)

accept

public AST accept(ASTVisitor visitor)

Accept visitor for a visit.

Parameters:

visitor - the visitor who is accepted by this node.

Returns:

the result of the visit (may be null)