public class RewriteCommand extends AbstractCommand<RewriteCommand.Parameters>
rewrite
.
This command takes two parameters. A term to find, and a term
as the substitutent. Parameter class is RewriteCommand.Parameters
.
Usage:
rewrite find="x+y" replace="y+x"; //(mulbrich script syntax) rewrite find=`y+x` replace=`y+x`; //(psdbg)
Modifier and Type | Class and Description |
---|---|
static class |
RewriteCommand.Parameters
Parameters for the
RewriteCommand |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
RewriteCommand()
Constructs this rewrite command.
|
Modifier and Type | Method and Description |
---|---|
RewriteCommand.Parameters |
evaluateArguments(EngineState state,
java.util.Map<java.lang.String,java.lang.String> arguments) |
void |
execute(AbstractUserInterfaceControl uiControl,
RewriteCommand.Parameters args,
EngineState state) |
java.lang.String |
getName()
Returns the name of this proof command.
|
Term |
getTermAtPos(SequentFormula sf,
PosInOccurrence pio)
Calculates term at the PosInOccurrence pio
|
execute, getArguments, getDocumentation
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine
public RewriteCommand.Parameters evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
evaluateArguments
in interface ProofScriptCommand<RewriteCommand.Parameters>
evaluateArguments
in class AbstractCommand<RewriteCommand.Parameters>
java.lang.Exception
public void execute(AbstractUserInterfaceControl uiControl, RewriteCommand.Parameters args, EngineState state) throws ScriptException, java.lang.InterruptedException
execute
in interface ProofScriptCommand<RewriteCommand.Parameters>
execute
in class AbstractCommand<RewriteCommand.Parameters>
uiControl
- the current ui controllerargs
- the script argumentsstate
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happenspublic Term getTermAtPos(SequentFormula sf, PosInOccurrence pio)
sf
- top-level formulapio
- PosInOccurrence of the to be returned termCopyright © 2003-2019 The KeY-Project.