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 |
Modifier and Type | Field and Description |
---|---|
private java.util.List<PosInOccurrence> |
failposInOccs
List of PosInOcc that haven't been successfully replaced
|
private java.util.List<PosInOccurrence> |
succposInOccs
List of PosInOcc that successfully replaced
|
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) |
private void |
executeRewriteTaclet(RewriteCommand.Parameters p,
PosTacletApp pta,
Goal goalold,
SequentFormula rewriteResult)
Execute taclet pta if after application p.find term is replaced by p.replace
throws IllegalArgumentException on not successfully applicable pta
|
private ImmutableList<TacletApp> |
findAllTacletApps(RewriteCommand.Parameters p,
EngineState state)
get all TacletApps that are applicable on the formula term
|
private java.util.List<PosInOccurrence> |
findAndExecReplacement(RewriteCommand.Parameters p,
ImmutableList<TacletApp> list,
EngineState state)
Filter tacletapps: term = find && result = replace
and execute taclet that matches the conditions
|
java.lang.String |
getName()
Returns the name of this proof command.
|
private Term |
getSubTerm(Term t,
IntIterator pit)
Gets subterm of t at the postion of pit
|
Term |
getTermAtPos(SequentFormula sf,
PosInOccurrence pio)
Calculates term at the PosInOccurrence pio
|
execute, getArguments, getDocumentation
private java.util.List<PosInOccurrence> failposInOccs
private java.util.List<PosInOccurrence> succposInOccs
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 happensprivate ImmutableList<TacletApp> findAllTacletApps(RewriteCommand.Parameters p, EngineState state) throws ScriptException
ScriptException
private java.util.List<PosInOccurrence> findAndExecReplacement(RewriteCommand.Parameters p, ImmutableList<TacletApp> list, EngineState state)
private void executeRewriteTaclet(RewriteCommand.Parameters p, PosTacletApp pta, Goal goalold, SequentFormula rewriteResult)
p
- pta
- goalold
- rewriteResult
- public Term getTermAtPos(SequentFormula sf, PosInOccurrence pio)
sf
- top-level formulapio
- PosInOccurrence of the to be returned termprivate Term getSubTerm(Term t, IntIterator pit)
t
- pit
-