de.uka.ilkd.key.rule.match.vm

Class VMTacletMatcher

java.lang.Object

de.uka.ilkd.key.rule.match.vm.VMTacletMatcher

All Implemented Interfaces:

TacletMatcher

public class VMTacletMatcher
extends java.lang.Object
implements TacletMatcher

Matching algorithm using a virtual machine based approach inspired by Voronkonv et al. It matches exactly one taclet and does not produce code trees. 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 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 Summary

Constructors

Constructor and Description
VMTacletMatcher(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 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) 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 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

Methods inherited from class java.lang.Object

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

Field Detail

findMatchProgram

private final TacletMatchProgram findMatchProgram

the matcher for the find expression of the taclet

assumesMatchPrograms

private final java.util.HashMap<Term,TacletMatchProgram> assumesMatchPrograms

the matcher for the taclet's assumes formulas

varconditions

private final ImmutableList<VariableCondition> varconditions

the variable conditions of the taclet that need to be satisfied by found schema variable instantiations

varsNotFreeIn

private final ImmutableList<NotFreeIn> varsNotFreeIn

the built-in notFreeIn variable conditions

assumesSequent

private final Sequent assumesSequent

the assumes sequent of the taclet

boundVars

private final ImmutableSet<QuantifiableVariable> boundVars

the bound variables

ignoreTopLevelUpdates

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

findExp

private final Term findExp

the find expression of the taclet of null if it is a NoFindTaclet

Constructor Detail

VMTacletMatcher

public VMTacletMatcher(Taclet taclet)

Parameters:

taclet - the Taclet matched by this matcher

Method Detail

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)

matchUpdateContext

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.

Parameters:

context - the list of update label pairs describing the update context

formula - the formula whose own update context must be equal (modulo renaming) to the given one

Returns:

null if the update context does not match the one of the formula or the formula without the update context

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,
                                                              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

Parameters:

term - the term to be matched

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