de.uka.ilkd.key.macros.scripts

Class InstantiateCommand

java.lang.Object

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

de.uka.ilkd.key.macros.scripts.InstantiateCommand

All Implemented Interfaces:

ProofScriptCommand<InstantiateCommand.Parameters>

public class InstantiateCommand
extends AbstractCommand<InstantiateCommand.Parameters>

instantiate var=a occ=2 with="a_8" hide

instantiate formula="\forall int a; phi(a)" with="a_8"

Author:

mulbrich

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	InstantiateCommand.Parameters
private static class	InstantiateCommand.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
InstantiateCommand()

Method Summary

Modifier and Type	Method and Description
private void	computeFormula(InstantiateCommand.Parameters params, Goal goal)
InstantiateCommand.Parameters	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(AbstractUserInterfaceControl uiControl, InstantiateCommand.Parameters params, EngineState state)
private TacletApp	filterList(InstantiateCommand.Parameters p, ImmutableList<TacletApp> list)
private ImmutableList<TacletApp>	findAllTacletApps(InstantiateCommand.Parameters p, EngineState state)
private TacletApp	findTacletApp(InstantiateCommand.Parameters p, EngineState state)
java.lang.String	getName() Returns the name of this proof command.
private Term	stripUpdates(Term term)

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

InstantiateCommand

public InstantiateCommand()

Method Detail

evaluateArguments

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

Specified by:

evaluateArguments in interface ProofScriptCommand<InstantiateCommand.Parameters>

Overrides:

evaluateArguments in class AbstractCommand<InstantiateCommand.Parameters>

Returns:

Throws:

java.lang.Exception

execute

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

Specified by:

execute in interface ProofScriptCommand<InstantiateCommand.Parameters>

Overrides:

execute in class AbstractCommand<InstantiateCommand.Parameters>

Parameters:

uiControl - the current ui controller

params - the script arguments

state - the current state

Throws:

ScriptException - if something bad happens

java.lang.InterruptedException - if something bad happens

findTacletApp

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

Throws:

ScriptException

findAllTacletApps

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

Throws:

ScriptException

filterList

private TacletApp filterList(InstantiateCommand.Parameters p,
                             ImmutableList<TacletApp> list)

computeFormula

private void computeFormula(InstantiateCommand.Parameters params,
                            Goal goal)
                     throws ScriptException

Throws:

ScriptException

stripUpdates

private Term stripUpdates(Term term)

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