fmrisc.ProofNavigator.Syntax

Class EquivalentFormula

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.BinaryExpression

fmrisc.ProofNavigator.Syntax.EquivalentFormula

All Implemented Interfaces:

AST, Expression

public final class EquivalentFormula
extends BinaryExpression

Handling of equivalences.

Constructor Summary

Constructors

Constructor and Description
EquivalentFormula(Expression base1, Expression base2) construct equivalence with components base1 and base2

Method Summary

Modifier and Type	Method and Description
BinaryExpression	construct(Expression first, Expression second) Construct binary expression of the same kind as this expression.
int	getPriority() get binding level for printing (lower numbers mean greater binding power)
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).

Methods inherited from class fmrisc.ProofNavigator.Syntax.BinaryExpression

accept, getFirst, getSecond, instantiate

Methods inherited from class fmrisc.ProofNavigator.Syntax.ExpressionBase

printPriority

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTBase

print, 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

print, printParens, toString

Constructor Detail

EquivalentFormula

public EquivalentFormula(Expression base1,
                         Expression base2)

construct equivalence with components base1 and base2

Parameters:

base1 - the first component

base2 - the second component

Method Detail

getPriority

public int getPriority()

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

Specified by:

getPriority in interface Expression

Specified by:

getPriority in class ExpressionBase

Returns:

the priority level

construct

public BinaryExpression construct(Expression first,
                                  Expression second)

Construct binary expression of the same kind as this expression.

Specified by:

construct in class BinaryExpression

Parameters:

first - an expression.

second - an expression.

Returns:

a binary expression of the same kind as this expression with subexpressions first and second.

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 BinaryExpression

Parameters:

out - the stream on which the text is written