public class ScriptApi
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ProofApi |
api |
private Matcher |
matcher |
private EngineState |
state |
Modifier and Type | Method and Description |
---|---|
<T> ScriptResults |
executeScriptCommand(ProofScriptCommandCall<T> call,
ProjectedNode onNode)
Execute ScriptCommand onto goal node
|
ProjectedNode |
getIntermediateTree(ScriptResults root,
ScriptResults end)
~> Beweisbaum -> Shallow Copy
hier implementieren
|
<T> ProofScriptCommandCall<T> |
instantiateCommand(ProofScriptCommand<T> command,
java.util.Map<java.lang.String,java.lang.String> arguments)
Evaluate the arguments passed to a command
|
java.util.List<VariableAssignments> |
matchPattern(java.lang.String pattern,
Sequent currentSeq,
VariableAssignments assignments)
Matches a sequent against a sequent pattern (a schematic sequent) returns a list of Nodes containing matching
results from where the information about instantiated schema variables can be extracted.
|
Term |
toTerm(java.lang.String term,
VariableAssignments assignments) |
private final ProofApi api
private final EngineState state
private Matcher matcher
public ScriptApi(ProofApi proofApi)
public java.util.List<VariableAssignments> matchPattern(java.lang.String pattern, Sequent currentSeq, VariableAssignments assignments)
pattern
- a string representation of the pattern sequent against which the current sequent should be matchedcurrentSeq
- current concrete sequentassignments
- variables appearing in the pattern as schemavariables with their corresponding type in KeYpublic <T> ScriptResults executeScriptCommand(ProofScriptCommandCall<T> call, ProjectedNode onNode) throws ScriptException, java.lang.InterruptedException
command
- to be applied with parameters setScriptException
java.lang.InterruptedException
public <T> ProofScriptCommandCall<T> instantiateCommand(ProofScriptCommand<T> command, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
T
- arguments
- java.lang.Exception
public Term toTerm(java.lang.String term, VariableAssignments assignments) throws java.lang.Exception
term
- assignments
- java.lang.Exception
- either for Syntax or Type errorpublic ProjectedNode getIntermediateTree(ScriptResults root, ScriptResults end)
root
- end
-