de.uka.ilkd.key.macros.scripts

Class RewriteCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<RewriteCommand.Parameters>

de.uka.ilkd.key.macros.scripts.RewriteCommand

All Implemented Interfaces:

ProofScriptCommand<RewriteCommand.Parameters>

public class RewriteCommand
extends AbstractCommand<RewriteCommand.Parameters>

This class provides the command 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)
 

Author:

lulong, grebing, weigl

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	RewriteCommand.Parameters Parameters for the RewriteCommand

Field Summary

Fields

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

Fields inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
RewriteCommand() Constructs this rewrite command.

Method Summary

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

Methods inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

execute, getArguments, getDocumentation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

failposInOccs

private java.util.List<PosInOccurrence> failposInOccs

List of PosInOcc that haven't been successfully replaced

succposInOccs

private java.util.List<PosInOccurrence> succposInOccs

List of PosInOcc that successfully replaced

Constructor Detail

RewriteCommand

public RewriteCommand()

Constructs this rewrite command.

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofScriptCommand

Returns the name of this proof command. The name should be constant and not be clash with the name of other commands. The name is essential for finding this command within an hashmap.

Returns:

a non-null, non-empty string

See Also:

ProofScriptEngine

evaluateArguments

public RewriteCommand.Parameters evaluateArguments(EngineState state,
                                                   java.util.Map<java.lang.String,java.lang.String> arguments)
                                            throws java.lang.Exception

Specified by:

evaluateArguments in interface ProofScriptCommand<RewriteCommand.Parameters>

Overrides:

evaluateArguments in class AbstractCommand<RewriteCommand.Parameters>

Returns:

Throws:

java.lang.Exception

execute

public void execute(AbstractUserInterfaceControl uiControl,
                    RewriteCommand.Parameters args,
                    EngineState state)
             throws ScriptException,
                    java.lang.InterruptedException

Specified by:

execute in interface ProofScriptCommand<RewriteCommand.Parameters>

Overrides:

execute in class AbstractCommand<RewriteCommand.Parameters>

Parameters:

uiControl - the current ui controller

args - the script arguments

state - the current state

Throws:

ScriptException - if something bad happens

java.lang.InterruptedException - if something bad happens

findAllTacletApps

private ImmutableList<TacletApp> findAllTacletApps(RewriteCommand.Parameters p,
                                                   EngineState state)
                                            throws ScriptException

get all TacletApps that are applicable on the formula term

Throws:

ScriptException

findAndExecReplacement

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

executeRewriteTaclet

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

Parameters:

p -

pta -

goalold -

rewriteResult -

getTermAtPos

public Term getTermAtPos(SequentFormula sf,
                         PosInOccurrence pio)

Calculates term at the PosInOccurrence pio

Parameters:

sf - top-level formula

pio - PosInOccurrence of the to be returned term

Returns:

term at pio

getSubTerm

private Term getSubTerm(Term t,
                        IntIterator pit)

Gets subterm of t at the postion of pit

Parameters:

t -

pit -

Returns:

subterm