de.uka.ilkd.key.macros.scripts

Class RuleCommand

java.lang.Object

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

de.uka.ilkd.key.macros.scripts.RuleCommand

All Implemented Interfaces:

ProofScriptCommand<RuleCommand.Parameters>

public class RuleCommand
extends AbstractCommand<RuleCommand.Parameters>

Command that applies a calculus rule All parameters are passed as strings and converted by the command. The parameters are:

1. #2 = rule name
2. on= key.core.logic.Term on which the rule should be applied to as String (find part of the rule)
3. formula= toplevel formula in which term appears in
4. occ = occurrence number
5. inst_= instantiation

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	RuleCommand.Parameters
private static class	RuleCommand.TacletNameFilter

Field Summary

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

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
RuleCommand()

Method Summary

Modifier and Type	Method and Description
private IBuiltInRuleApp	builtInRuleApp(RuleCommand.Parameters p, EngineState state, BuiltInRule rule)
RuleCommand.Parameters	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(AbstractUserInterfaceControl uiControl, RuleCommand.Parameters args, EngineState state)
private java.util.List<TacletApp>	filterList(RuleCommand.Parameters p, ImmutableList<TacletApp> list)
private ImmutableList<TacletApp>	findAllTacletApps(RuleCommand.Parameters p, EngineState state)
private ImmutableList<IBuiltInRuleApp>	findBuiltInRuleApps(RuleCommand.Parameters p, EngineState state)
private TacletApp	findTacletApp(RuleCommand.Parameters p, EngineState state)
private static java.lang.String	formatTermString(java.lang.String str) Removes spaces and line breaks from the string representation of a term.
java.lang.String	getName() Returns the name of this proof command.
private TacletApp	instantiateTacletApp(RuleCommand.Parameters p, EngineState state, Proof proof, TacletApp theApp)
private boolean	isFormulaSearchedFor(RuleCommand.Parameters p, SequentFormula sf, Services services) Returns true iff the given SequentFormula either matches the RuleCommand.Parameters.formula parameter or its String representation matches the RuleCommand.Parameters.matches regex.
private TacletApp	makeNoFindTacletApp(Taclet taclet)
private RuleApp	makeRuleApp(RuleCommand.Parameters p, EngineState state)

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

Constructor Detail

RuleCommand

public RuleCommand()

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 RuleCommand.Parameters evaluateArguments(EngineState state,
                                                java.util.Map<java.lang.String,java.lang.String> arguments)
                                         throws java.lang.Exception

Specified by:

evaluateArguments in interface ProofScriptCommand<RuleCommand.Parameters>

Overrides:

evaluateArguments in class AbstractCommand<RuleCommand.Parameters>

Returns:

Throws:

java.lang.Exception

execute

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

Specified by:

execute in interface ProofScriptCommand<RuleCommand.Parameters>

Overrides:

execute in class AbstractCommand<RuleCommand.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

makeRuleApp

private RuleApp makeRuleApp(RuleCommand.Parameters p,
                            EngineState state)
                     throws ScriptException

Throws:

ScriptException

instantiateTacletApp

private TacletApp instantiateTacletApp(RuleCommand.Parameters p,
                                       EngineState state,
                                       Proof proof,
                                       TacletApp theApp)
                                throws ScriptException

Throws:

ScriptException

makeNoFindTacletApp

private TacletApp makeNoFindTacletApp(Taclet taclet)

builtInRuleApp

private IBuiltInRuleApp builtInRuleApp(RuleCommand.Parameters p,
                                       EngineState state,
                                       BuiltInRule rule)
                                throws ScriptException

Throws:

ScriptException

findTacletApp

private TacletApp findTacletApp(RuleCommand.Parameters p,
                                EngineState state)
                         throws ScriptException

Throws:

ScriptException

findBuiltInRuleApps

private ImmutableList<IBuiltInRuleApp> findBuiltInRuleApps(RuleCommand.Parameters p,
                                                           EngineState state)
                                                    throws ScriptException

Throws:

ScriptException

findAllTacletApps

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

Throws:

ScriptException

isFormulaSearchedFor

private boolean isFormulaSearchedFor(RuleCommand.Parameters p,
                                     SequentFormula sf,
                                     Services services)
                              throws ScriptException

Returns true iff the given SequentFormula either matches the RuleCommand.Parameters.formula parameter or its String representation matches the RuleCommand.Parameters.matches regex. If both parameters are not supplied, always returns true.

Parameters:

p - The RuleCommand.Parameters object.

sf - The SequentFormula to check.

Returns:

true if sf matches.

Throws:

ScriptException

formatTermString

private static java.lang.String formatTermString(java.lang.String str)

Removes spaces and line breaks from the string representation of a term.

Parameters:

str - The string to "clean up".

Returns:

The original without spaces and line breaks.

filterList

private java.util.List<TacletApp> filterList(RuleCommand.Parameters p,
                                             ImmutableList<TacletApp> list)