public final class LegacyTacletMatcher extends java.lang.Object implements TacletMatcher
TacletMatcherKit.createTacletMatcher(Taclet)
instead.TacletMatcherKit
Modifier and Type | Field and Description |
---|---|
private Sequent |
assumesSequent |
private ImmutableSet<QuantifiableVariable> |
boundVars |
private Term |
findExp |
private boolean |
ignoreTopLevelUpdates |
private ImmutableList<VariableCondition> |
varconditions |
private ImmutableList<NotFreeIn> |
varsNotFreeIn |
Constructor and Description |
---|
LegacyTacletMatcher(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 MatchConditions |
match(Term term,
Term template,
MatchConditions matchCond,
Services services)
returns a SVInstantiations object with the needed SchemaVariable to Term
mappings to match the given Term template to the Term term or
null if no matching is possible.
|
private Pair<Term,MatchConditions> |
matchAndIgnoreUpdatePrefix(Term term,
Term template,
MatchConditions matchCond,
TermServices services)
ignores a possible update prefix
|
private MatchConditions |
matchBoundVariables(Term term,
Term template,
MatchConditions matchCond,
Services services)
tries to match the bound variables of the given term against the one
described by the template
|
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.
|
protected MatchConditions |
matchJavaBlock(Term term,
Term template,
MatchConditions matchCond,
Services services)
returns the matchconditions that are required if the java block of the
given term matches the schema given by the template term or null if no
match is possible
(marked as final to help the compiler inlining methods)
|
MatchConditions |
matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
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 ImmutableList<VariableCondition> varconditions
private final Sequent assumesSequent
private final ImmutableSet<QuantifiableVariable> boundVars
private final ImmutableList<NotFreeIn> varsNotFreeIn
private final boolean ignoreTopLevelUpdates
private final Term findExp
public LegacyTacletMatcher(Taclet taclet)
taclet
- the Taclet matched by this matcherprivate final MatchConditions matchBoundVariables(Term term, Term template, MatchConditions matchCond, Services services)
term
- the Term whose bound variables are matched against the
JavaBlock of the template
(marked as final to help the compiler inlining methods)template
- the Term whose bound variables are the template that have
to be matchedmatchCond
- the MatchConditions that has to be paid respect when
trying to matchprotected final MatchConditions matchJavaBlock(Term term, Term template, MatchConditions matchCond, Services services)
term
- the Term whose JavaBlock is matched against the JavaBlock of
the templatetemplate
- the Term whose JavaBlock is the template that has to
be matchedmatchCond
- the MatchConditions that has to be paid respect when
trying to match the JavaBlocksservices
- the Services object encapsulating information about the
program contextprivate MatchConditions match(Term term, Term template, MatchConditions matchCond, Services services)
term
- the Term the Template should matchtemplate
- the Term tried to be instantiated so that it matches termmatchCond
- the MatchConditions to be obeyed by a
successful matchpublic 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 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, Term template, MatchConditions matchCond, TermServices services)
term
- the term to be matchedtemplate
- the pattern termmatchCond
- 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