fmrisc.ProofNavigator.Commands

Class DeclarationC

java.lang.Object

fmrisc.ProofNavigator.Commands.CommandBase

fmrisc.ProofNavigator.Commands.DeclarationC

All Implemented Interfaces:

Command

public final class DeclarationC
extends CommandBase

Virtual command "declaration": process declaration in current environment

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	Name

Constructor Summary

Constructors

Constructor and Description
DeclarationC(Declaration decl) Create a "declaration" command.

Method Summary

Methods

Modifier and Type	Method and Description
static java.util.Vector<Symbol>	getReferenced(java.util.Collection<Symbol> symbols, Environment env) Get value symbols from collection that are contained in environment.
static Command	newCommand(org.w3c.dom.Node node) Convert DOM node to command.
void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).
void	process() Process declaration.
void	process(boolean display) Process declaration.

Methods inherited from class fmrisc.ProofNavigator.Commands.CommandBase

getName, toCommand, toNode, toString

Methods inherited from class java.lang.Object

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

Field Detail

Name

public static final java.lang.String Name

See Also:

Constant Field Values

Constructor Detail

DeclarationC

public DeclarationC(Declaration decl)

Create a "declaration" command.

Parameters:

decl - the declaration to be processed

Method Detail

process

public void process()

Process declaration. This means the following: - At the global level, type checking conditions are immediately checked and the declaration is added to the current environment. - Within a proof, a type checking condition lead to an additional child state; the declaration is added to a child state. E: A, ... |- B, ... => ( E: A, ... |- TCC_D ) E U {D}: A, ... |- B

process

public void process(boolean display)

Process declaration.

Parameters:

display - true iff declaration is to be displayed.

getReferenced

public static java.util.Vector<Symbol> getReferenced(java.util.Collection<Symbol> symbols,
                                     Environment env)

Get value symbols from collection that are contained in environment.

Parameters:

symbols - a collection of Symbol values.

env - the environment

Returns:

a vector of the value symbols from the symbols that are contained in the environment.

newCommand

public static Command newCommand(org.w3c.dom.Node node)

Convert DOM node to command.

Parameters:

node - the DOM representation of the command.

Returns:

the command (null, if an error occured).

printCore

public void printCore(java.io.PrintWriter out)

Prints text representation on out (without new line termination).

Specified by:

printCore in class CommandBase

Parameters:

out - the stream on which the text is written