public class Matcher
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
buildDecls(VariableAssignments assignments)
Builds a string that is used to create a new schemavariable declaration for the matchpattern
|
private void |
buildNameSpace(VariableAssignments assignments,
Services services)
Adds the variables of VariableAssignments to the namespace
|
private VariableAssignments |
extractAssignments(SearchNode sn,
VariableAssignments assignments)
Extract the matching results from each SearchNode and tranform these to Variable Assigments
|
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.
|
void |
parseDecls(java.lang.String s,
Services services)
Parse the declaration string for the current pattern and add the variables to the namespace
|
private Taclet |
parseTaclet(java.lang.String s,
Services services) |
private KeYParserF |
stringDeclParser(java.lang.String s,
Services services) |
private KeYParserF |
stringTacletParser(java.lang.String s,
Services services) |
private java.lang.String |
toDecl(java.lang.String id,
VariableAssignments.VarType type) |
private ProofApi api
public Matcher(ProofApi api)
api
- reference to proof api in order to get access to the key environmentpublic 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 KeYprivate VariableAssignments extractAssignments(SearchNode sn, VariableAssignments assignments)
sn
- SearchNodeprivate void buildNameSpace(VariableAssignments assignments, Services services)
assignments
- VariabelAssignments containing variable names and typesservices
- private java.lang.String buildDecls(VariableAssignments assignments)
assignments
- varaiables appearing as schema varaibels in the match pattern and their types (in KeY)private java.lang.String toDecl(java.lang.String id, VariableAssignments.VarType type)
private KeYParserF stringDeclParser(java.lang.String s, Services services)
public void parseDecls(java.lang.String s, Services services)
s
- declaration part of a tacletprivate KeYParserF stringTacletParser(java.lang.String s, Services services)