fmrisc.ProofNavigator.Syntax

Class QuantifiedExpression

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.QuantifiedExpression

All Implemented Interfaces:

AST, Expression

Direct Known Subclasses:

ArrayTerm, ExistsFormula, ForallFormula, LambdaTerm

public abstract class QuantifiedExpression
extends ExpressionBase

Abstract base class of quantified expressions.

Constructor Summary

Constructors

Constructor and Description
QuantifiedExpression(java.lang.String quantifier, TypedIdentifier[] variables, Expression base) constructs quantified expression from quantifier, variables, and base

Method Summary

Modifier and Type	Method and Description
AST	accept(ASTVisitor visitor) Accept visitor for a visit.
abstract QuantifiedExpression	construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
Expression	getBase() get base expression
int	getPriority() get binding level for printing (lower numbers mean greater binding power)
TypedIdentifier[]	getVariables() get quantified variables
Expression	instantiate() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).
fmrisc.ProofNavigator.Syntax.QuantifiedExpression.Substitution	substitution() return copy of AST with value references instantiated by the substitutions set in the corresponding declaration identifiers

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

QuantifiedExpression

public QuantifiedExpression(java.lang.String quantifier,
                            TypedIdentifier[] variables,
                            Expression base)

constructs quantified expression from quantifier, variables, and base

Parameters:

quantifier - the name of the quantifier used for printing

variables - the variable sequence

base - the base expression

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

getVariables

public TypedIdentifier[] getVariables()

get quantified variables

Returns:

the variable sequence

getBase

public Expression getBase()

get base expression

Returns:

the base expression

substitution

public fmrisc.ProofNavigator.Syntax.QuantifiedExpression.Substitution substitution()

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

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

Specified by:

printCore in class ASTBase

Parameters:

out - the stream on which the text is written

instantiate

public Expression instantiate()

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

Returns:

the instantiated copy

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

construct

public abstract QuantifiedExpression construct(TypedIdentifier[] variables,
                                               Expression base)

Construct quantified expression.

Parameters:

variables - typed variables.

base - an expression.

Returns:

a quantified expression of the same kind as this expression with the denoted variables and base expression.