fmrisc.ProgramExplorer.Syntax.Spec

Class TheoryDeclaration

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTBase

fmrisc.ProgramExplorer.Syntax.ASTSourceBase

fmrisc.ProgramExplorer.Syntax.Program.DeclarationBase

fmrisc.ProgramExplorer.Syntax.Program.CompilationUnitBase

fmrisc.ProgramExplorer.Syntax.Spec.TheoryDeclaration

All Implemented Interfaces:

AST, ASTSource, Declaration, ASTProgram, ASTProgramAnnotated, CompilationUnit, ProgramDeclaration

public final class TheoryDeclaration
extends CompilationUnitBase

The declaration of a logical theory.

Field Summary

Fields inherited from class fmrisc.ProgramExplorer.Syntax.Program.CompilationUnitBase

imports, pname

Fields inherited from class fmrisc.ProgramExplorer.Syntax.Program.DeclarationBase

annotation, name

Method Summary

Modifier and Type	Method and Description
void	accept(ASTVisitor visitor) Accept visitor for a visit.
void	accept(ASTVisitorOld visitor) Accept visitor for a visit.
void	acceptChildren(ASTVisitor visitor) Accept visitor for a visit to the children of this node.
static TheoryDeclaration	construct(Name pname, Import[] imports, Identifier name, Name[] theories, Declaration[] decls) Construct a theory declaration
static TheoryDeclaration	construct(Name pname, java.util.Vector<Import> imports, Identifier name, java.util.Vector<Name> theories, java.util.Vector<Declaration> decls) Construct a theory.
Declaration[]	getDeclarations() Get declarations introduced in unit.
Name[]	getTheories() Get theories on which unit depends.

Methods inherited from class fmrisc.ProgramExplorer.Syntax.Program.CompilationUnitBase

getImports, getPackage

Methods inherited from class fmrisc.ProgramExplorer.Syntax.Program.DeclarationBase

getAnnotation, getName, setAnnotation

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTSourceBase

getPosition, setPosition

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTBase

accept, accept, print, printCore, toString, toStringCore

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface fmrisc.ProgramExplorer.Syntax.Declaration

getName

Methods inherited from interface fmrisc.ProgramExplorer.Syntax.ASTSource

getPosition, setPosition

Methods inherited from interface fmrisc.ProgramExplorer.Syntax.Program.ASTProgramAnnotated

getAnnotation, setAnnotation

Methods inherited from interface fmrisc.ProgramExplorer.Syntax.AST

print, printCore, toString, toStringCore

Method Detail

construct

public static TheoryDeclaration construct(Name pname,
                                          java.util.Vector<Import> imports,
                                          Identifier name,
                                          java.util.Vector<Name> theories,
                                          java.util.Vector<Declaration> decls)

Construct a theory.

Parameters:

pname - package name (may be null)

imports - import statements

name - theory identifier

theories - the names of the theories on which this theory depends (may be null)

decls - sequence of declarations

Returns:

the declaration.

construct

public static TheoryDeclaration construct(Name pname,
                                          Import[] imports,
                                          Identifier name,
                                          Name[] theories,
                                          Declaration[] decls)

Construct a theory declaration

Parameters:

pname - package name (may be null)

imports - import statements

name - theory identifier

theories - the names of the theories on which this theory depends

decls - sequence of declarations

Returns:

the declaration.

getDeclarations

public Declaration[] getDeclarations()

Get declarations introduced in unit.

Returns:

list of declarations used in unit.

getTheories

public Name[] getTheories()

Get theories on which unit depends.

Returns:

theories on which unit depends.

accept

public void accept(ASTVisitorOld visitor)

Accept visitor for a visit.

Specified by:

accept in interface AST

Overrides:

accept in class CompilationUnitBase

Parameters:

visitor - the visitor who is accepted by this node.

accept

public void accept(ASTVisitor visitor)

Accept visitor for a visit.

Specified by:

accept in interface AST

Overrides:

accept in class CompilationUnitBase

Parameters:

visitor - the visitor who is accepted by this node.

acceptChildren

public void acceptChildren(ASTVisitor visitor)

Accept visitor for a visit to the children of this node.

Specified by:

acceptChildren in interface AST

Overrides:

acceptChildren in class CompilationUnitBase

Parameters:

visitor - the visitor who is accepted by the children of this node.