fmrisc.ProofNavigator.Syntax

Class SubType

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.TypeBase

fmrisc.ProofNavigator.Syntax.SubType

All Implemented Interfaces:

AST, Type

public final class SubType
extends TypeBase

Predicated subtypes.

Constructor Summary

Constructors

Constructor and Description
SubType(Expression predicate) construct subtype with denoted predicate.

Method Summary

Modifier and Type	Method and Description
AST	accept(ASTVisitor visitor) Accept visitor for a visit.
Type	getBase() returns base type
Expression	getPredicate() returns predicate
Type	instantiateType() 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 of type on out (without new line termination).
void	setBase(Type base) set base type

Methods inherited from class fmrisc.ProofNavigator.Syntax.TypeBase

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

SubType

public SubType(Expression predicate)

construct subtype with denoted predicate.

Parameters:

predicate - the predicate defining the subtype

Method Detail

getPredicate

public Expression getPredicate()

returns predicate

Returns:

the predicate associated to the subtype

getBase

public Type getBase()

returns base type

Returns:

the base type of the subtype

setBase

public void setBase(Type base)

set base type

Parameters:

base - the base type of the subtype

instantiateType

public Type instantiateType()

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 of type 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

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)