public class VMTacletMatcher extends java.lang.Object implements TacletMatcher
TacletMatcherKit.createTacletMatcher(Taclet)
instead.TacletMatcherKit
Modifier and Type | Field and Description |
---|---|
private java.util.HashMap<Term,TacletMatchProgram> |
assumesMatchPrograms
the matcher for the taclet's assumes formulas
|
private Sequent |
assumesSequent
the assumes sequent of the taclet
|
private ImmutableSet<QuantifiableVariable> |
boundVars
the bound variables
|
private Term |
findExp
the find expression of the taclet of
null if it is a NoFindTaclet |
private TacletMatchProgram |
findMatchProgram
the matcher for the find expression of the taclet
|
private boolean |
ignoreTopLevelUpdates
flag indicating if preceding updates of the term to be matched should be ignored
this requires the taclet to ignore updates and that the find term does not start with
an
UpdateApplication operator |
private ImmutableList<VariableCondition> |
varconditions
the variable conditions of the taclet that need to be satisfied by found
schema variable instantiations
|
private ImmutableList<NotFreeIn> |
varsNotFreeIn
the built-in notFreeIn variable conditions
|
Constructor and Description |
---|
VMTacletMatcher(Taclet taclet) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
private Pair<Term,MatchConditions> |
matchAndIgnoreUpdatePrefix(Term term,
MatchConditions matchCond,
TermServices services)
ignores a possible update prefix
This method assumes that the taclet allows to ignore updates and
the find expression does not start with an update application operator
|
MatchConditions |
matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
IfMatchResult |
matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
MatchConditions |
matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services)
Match the whole if sequent using the given list of
instantiations of all if sequent formulas, starting with the
instantiations given by p_matchCond.
|
MatchConditions |
matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
private Term |
matchUpdateContext(ImmutableList<SVInstantiations.UpdateLabelPair> context,
Term formula)
the formula ensures that the update context described the update of the given formula
It it does not
null is returned, otherwise the formula without the update context. |
private boolean |
varDeclaredNotFree(SchemaVariable var)
looks if a variable is declared as not free in
|
private boolean |
varIsBound(SchemaVariable v)
returns true iff the given variable is bound either in the
ifSequent or in
any part of the TacletGoalTemplates
|
private final TacletMatchProgram findMatchProgram
private final java.util.HashMap<Term,TacletMatchProgram> assumesMatchPrograms
private final ImmutableList<VariableCondition> varconditions
private final ImmutableList<NotFreeIn> varsNotFreeIn
private final Sequent assumesSequent
private final ImmutableSet<QuantifiableVariable> boundVars
private final boolean ignoreTopLevelUpdates
UpdateApplication
operatorprivate final Term findExp
null
if it is a NoFindTaclet
public VMTacletMatcher(Taclet taclet)
taclet
- the Taclet matched by this matcherpublic final IfMatchResult matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services)
matchIf
in interface TacletMatcher
p_toMatch
- list of constraint formulas to match p_template top_template
- template formula as in "match"p_matchCond
- already performed instantiationsp_services
- the Services object encapsulating information
about the java datastructures like (static)types etc.TacletMatcher.matchIf(ImmutableList, de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
private Term matchUpdateContext(ImmutableList<SVInstantiations.UpdateLabelPair> context, Term formula)
null
is returned, otherwise the formula without the update context.context
- the list of update label pairs describing the update contextformula
- the formula whose own update context must be equal (modulo renaming) to the given onenull
if the update context does not match the one of the formula or the formula without the update contextpublic final MatchConditions matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch, MatchConditions p_matchCond, Services p_services)
TacletMatcher
matchIf
in interface TacletMatcher
TacletMatcher.matchIf(java.lang.Iterable, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
public final MatchConditions checkConditions(MatchConditions cond, Services services)
null
if the found matches
do not satisfy the variable conditions. If the given matchconditions are null
then null
is returnedcheckConditions
in interface TacletMatcher
cond
- the matches to be checkedservices
- the Services
null
if
given matches do not satisfy the taclet's variable conditionsprivate boolean varDeclaredNotFree(SchemaVariable var)
var
- the SchemaVariable to look forprivate boolean varIsBound(SchemaVariable v)
v
- the bound variable to be searchedpublic final MatchConditions checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)
checkVariableConditions
in interface TacletMatcher
var
- the SchemaVariable to be instantiatedinstantiationCandidate
- the SVSubstitute, which is a
candidate for a possible instantiation of varmatchCond
- the MatchConditions which have to be respected
for the new matchservices
- the Services object encapsulating information
about the Java type modelvar
with instantiationCandidate
or
null
if a match was not possibleprivate Pair<Term,MatchConditions> matchAndIgnoreUpdatePrefix(Term term, MatchConditions matchCond, TermServices services)
term
- the term to be matchedmatchCond
- the accumulated match conditions for a successful matchservices
- the Servicespublic final MatchConditions matchFind(Term term, MatchConditions matchCond, Services services)
null
is returned
matchFind
in interface TacletMatcher
term
- the Term to be matched against the find expression
of the tacletmatchCond
- the MatchConditions with side conditions to be
satisfied, eg. partial instantiations of schema variables; before
calling this method the constraint contained in the match conditions
must be ensured to be satisfiable, i.e.
matchCond.getConstraint ().isSatisfiable ()
must return trueservices
- the Servicespublic MatchConditions matchSV(SchemaVariable sv, Term term, MatchConditions matchCond, Services services)
SchemaVariable
sv
matches the Term
term
w.r.t.
the constraints (e.g., previous matches of sv
) specified in the MatchConditions
matchCond
matchSV
in interface TacletMatcher
sv
- the SchemaVariable
term
- the Term
as a candidate for instantition of sv
matchCond
- the MatchConditions
with additional constraints that need to be consideredservices
- the Services
null
if the match is not possible or the new MatchConditions
with the instantiation sv <- term
addedpublic MatchConditions matchSV(SchemaVariable sv, ProgramElement pe, MatchConditions matchCond, Services services)
SchemaVariable
sv
matches the ProgramElement
pe
w.r.t.
the constraints (e.g., previous matches of sv
) specified in the MatchConditions
matchCond
matchSV
in interface TacletMatcher
sv
- the SchemaVariable
matchCond
- the MatchConditions
with additional constraints that need to be consideredservices
- the Services
null
if the match is not possible or the new MatchConditions
with the instantiation sv <- term
added