public class InstantiateCommand extends AbstractCommand<InstantiateCommand.Parameters>
instantiate formula="\forall int a; phi(a)" with="a_8"
Modifier and Type | Class and Description |
---|---|
static class |
InstantiateCommand.Parameters |
private static class |
InstantiateCommand.TacletNameFilter |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
InstantiateCommand() |
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) |
execute, getArguments, getDocumentation
public InstantiateCommand.Parameters evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
evaluateArguments
in interface ProofScriptCommand<InstantiateCommand.Parameters>
evaluateArguments
in class AbstractCommand<InstantiateCommand.Parameters>
java.lang.Exception
public void execute(AbstractUserInterfaceControl uiControl, InstantiateCommand.Parameters params, EngineState state) throws ScriptException, java.lang.InterruptedException
execute
in interface ProofScriptCommand<InstantiateCommand.Parameters>
execute
in class AbstractCommand<InstantiateCommand.Parameters>
uiControl
- the current ui controllerparams
- the script argumentsstate
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happensprivate TacletApp findTacletApp(InstantiateCommand.Parameters p, EngineState state) throws ScriptException
ScriptException
private ImmutableList<TacletApp> findAllTacletApps(InstantiateCommand.Parameters p, EngineState state) throws ScriptException
ScriptException
private TacletApp filterList(InstantiateCommand.Parameters p, ImmutableList<TacletApp> list)
private void computeFormula(InstantiateCommand.Parameters params, Goal goal) throws ScriptException
ScriptException
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine