fmrisc.ProofNavigator.Syntax

Class ApplicationExpression

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.ApplicationExpression

All Implemented Interfaces:

AST, Expression

public final class ApplicationExpression
extends ExpressionBase

Handling of function and predicate applications.

Constructor Summary

Constructors

Constructor and Description
ApplicationExpression(Expression fun, Expression[] args) construct application of fun to args

Method Summary

Modifier and Type	Method and Description
AST	accept(ASTVisitor visitor) Accept visitor for a visit.
Expression[]	getArguments() get arguments
Expression	getFunction() get function/predicate
int	getPriority() get binding level for printing (lower numbers mean greater binding power)
Expression	instantiate() 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).

Methods inherited from class fmrisc.ProofNavigator.Syntax.ExpressionBase

printPriority

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

ApplicationExpression

public ApplicationExpression(Expression fun,
                             Expression[] args)

construct application of fun to args

Parameters:

fun - the function/predicate

args - the sequence of arguments

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

getFunction

public Expression getFunction()

get function/predicate

Returns:

the function/predicate

getArguments

public Expression[] getArguments()

get arguments

Returns:

the argument sequence

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

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

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

Specified by:

print in interface AST

Overrides:

print in class ASTBase

Parameters:

out - the stream on which the text is written

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