de.uka.ilkd.key.rule.match.legacy

Class LegacyTacletMatcher

java.lang.Object

de.uka.ilkd.key.rule.match.legacy.LegacyTacletMatcher

All Implemented Interfaces:

TacletMatcher

public final class LegacyTacletMatcher
extends java.lang.Object
implements TacletMatcher

This class encapsulates the matching logic for taclet's. Instances of this class should not be created directly, use TacletMatcherKit.createTacletMatcher(Taclet) instead.

See Also:

TacletMatcherKit

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
LegacyTacletMatcher(Taclet taclet)

Method Summary

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) checks whether the given SchemaVariable sv matches the ProgramElement pe w.r.t.
MatchConditions	matchSV(SchemaVariable sv, Term term, MatchConditions matchCond, Services services) checks whether the given SchemaVariable sv matches the Term term w.r.t.
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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

varconditions

private final ImmutableList<VariableCondition> varconditions

assumesSequent

private final Sequent assumesSequent

boundVars

private final ImmutableSet<QuantifiableVariable> boundVars

varsNotFreeIn

private final ImmutableList<NotFreeIn> varsNotFreeIn

ignoreTopLevelUpdates

private final boolean ignoreTopLevelUpdates

findExp

private final Term findExp

Constructor Detail

LegacyTacletMatcher

public LegacyTacletMatcher(Taclet taclet)

Parameters:

taclet - the Taclet matched by this matcher

Method Detail

matchBoundVariables

private final 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

Parameters:

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 matched

matchCond - the MatchConditions that has to be paid respect when trying to match

Returns:

the new matchconditions if a match is possible, otherwise null

matchJavaBlock

protected final 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)

Parameters:

term - the Term whose JavaBlock is matched against the JavaBlock of the template

template - the Term whose JavaBlock is the template that has to be matched

matchCond - the MatchConditions that has to be paid respect when trying to match the JavaBlocks

services - the Services object encapsulating information about the program context

Returns:

the new matchconditions if a match is possible, otherwise null

match

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. (marked as final to help the compiler inlining methods)

Parameters:

term - the Term the Template should match

template - the Term tried to be instantiated so that it matches term

matchCond - the MatchConditions to be obeyed by a successful match

Returns:

the new MatchConditions needed to match template with term, if possible, null otherwise PRECONDITION: matchCond.getConstraint ().isSatisfiable ()

matchIf

public final IfMatchResult matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
                                   Term p_template,
                                   MatchConditions p_matchCond,
                                   Services p_services)

(non-Javadoc)

Specified by:

matchIf in interface TacletMatcher

Parameters:

p_toMatch - list of constraint formulas to match p_template to

p_template - template formula as in "match"

p_matchCond - already performed instantiations

p_services - the Services object encapsulating information about the java datastructures like (static)types etc.

Returns:

Two lists (in an IfMatchResult object), containing the the elements of p_toMatch that could successfully be matched against p_template, and the corresponding MatchConditions.

See Also:

TacletMatcher.matchIf(ImmutableList, de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)

matchIf

public final MatchConditions matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
                                     MatchConditions p_matchCond,
                                     Services p_services)

Description copied from interface: TacletMatcher

Match the whole if sequent using the given list of instantiations of all if sequent formulas, starting with the instantiations given by p_matchCond. PRECONDITION: p_toMatch.size () == ifSequent ().size ()

Specified by:

matchIf in interface TacletMatcher

Returns:

resulting MatchConditions or null if the given list p_toMatch does not match

See Also:

TacletMatcher.matchIf(java.lang.Iterable, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)

checkConditions

public final 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. If the given matchconditions are null then null is returned

Specified by:

checkConditions in interface TacletMatcher

Parameters:

cond - the matches to be checked

services - the Services

Returns:

the resulting match conditions or null if given matches do not satisfy the taclet's variable conditions

varDeclaredNotFree

private boolean varDeclaredNotFree(SchemaVariable var)

looks if a variable is declared as not free in

Parameters:

var - the SchemaVariable to look for

Returns:

true iff declared not free

varIsBound

private boolean varIsBound(SchemaVariable v)

returns true iff the given variable is bound either in the ifSequent or in any part of the TacletGoalTemplates

Parameters:

v - the bound variable to be searched

checkVariableConditions

public final MatchConditions checkVariableConditions(SchemaVariable var,
                                                     SVSubstitute instantiationCandidate,
                                                     MatchConditions matchCond,
                                                     Services services)

checks if the conditions for a correct instantiation are satisfied

Specified by:

checkVariableConditions in interface TacletMatcher

Parameters:

var - the SchemaVariable to be instantiated

instantiationCandidate - the SVSubstitute, which is a candidate for a possible instantiation of var

matchCond - the MatchConditions which have to be respected for the new match

services - the Services object encapsulating information about the Java type model

Returns:

the match conditions resulting from matching var with instantiationCandidate or null if a match was not possible

matchAndIgnoreUpdatePrefix

private Pair<Term,MatchConditions> matchAndIgnoreUpdatePrefix(Term term,
                                                              Term template,
                                                              MatchConditions matchCond,
                                                              TermServices services)

ignores a possible update prefix

Parameters:

term - the term to be matched

template - the pattern term

matchCond - the accumulated match conditions for a successful match

services - the Services

Returns:

a pair of updated match conditions and the unwrapped term without the ignored updates (Which have been added to the update context in the match conditions)

matchFind

public final 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

Specified by:

matchFind in interface TacletMatcher

Parameters:

term - the Term to be matched against the find expression of the taclet

matchCond - 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 true

services - the Services

Returns:

the found schema variable mapping or null if the matching failed

matchSV

public MatchConditions matchSV(SchemaVariable sv,
                               Term term,
                               MatchConditions matchCond,
                               Services services)

checks whether the given SchemaVariable sv matches the Term term w.r.t. the constraints (e.g., previous matches of sv) specified in the MatchConditions matchCond

Specified by:

matchSV in interface TacletMatcher

Parameters:

sv - the SchemaVariable

term - the Term as a candidate for instantition of sv

matchCond - the MatchConditions with additional constraints that need to be considered

services - the Services

Returns:

null if the match is not possible or the new MatchConditions with the instantiation sv <- term added

matchSV

public MatchConditions matchSV(SchemaVariable sv,
                               ProgramElement pe,
                               MatchConditions matchCond,
                               Services services)

checks whether the given SchemaVariable sv matches the ProgramElement pe w.r.t. the constraints (e.g., previous matches of sv) specified in the MatchConditions matchCond

Specified by:

matchSV in interface TacletMatcher

Parameters:

sv - the SchemaVariable

matchCond - the MatchConditions with additional constraints that need to be considered

services - the Services

Returns:

null if the match is not possible or the new MatchConditions with the instantiation sv <- term added