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 |
static java.lang.String |
Name
|
Method Summary |
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. |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Name
public static final java.lang.String Name
- See Also:
- Constant Field Values
DeclarationC
public DeclarationC(Declaration decl)
- Create a "declaration" command.
- Parameters:
decl
- the declaration to be processed
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
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