public interface TacletMatcher
Modifier and Type | Method and Description |
---|---|
MatchConditions |
checkConditions(MatchConditions p_matchconditions,
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)
Match the given template (which is probably a formula of the if
sequence) against a list of constraint formulas (probably the
formulas of the antecedent or the succedent), starting with the
given instantiations and constraint p_matchCond.
|
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 term,
MatchConditions matchCond,
Services services)
|
MatchConditions |
matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
IfMatchResult matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services)
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.MatchConditions matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch, MatchConditions p_matchCond, Services p_services)
MatchConditions checkConditions(MatchConditions p_matchconditions, Services services)
null
if the found matches
do not satisfy the variable conditions. If the given matchconditions are null
then null
is returnedp_matchconditions
- the matches to be checkedservices
- the Services
null
if
given matches do not satisfy the taclet's variable conditionsMatchConditions checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)
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 possibleMatchConditions matchFind(Term term, MatchConditions matchCond, Services services)
null
is returned
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 ServicesMatchConditions 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
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
addedMatchConditions matchSV(SchemaVariable sv, ProgramElement term, 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
sv
- the SchemaVariable
pe
- the ProgramElement
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
added