public class VMTacletMatcher extends java.lang.Object implements TacletMatcher
TacletMatcherKit.createTacletMatcher(Taclet)
instead.TacletMatcherKit
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
|
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)
|
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)
public 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 conditionspublic 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 possiblepublic 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
addedCopyright © 2003-2019 The KeY-Project.