| java.lang.Object
 de.uka.ilkd.key.rule.Taclet
de.uka.ilkd.key.rule.FindTaclet
All known Subclasses: de.uka.ilkd.key.rule.AntecTaclet, de.uka.ilkd.key.rule.SuccTaclet, de.uka.ilkd.key.rule.RewriteTaclet,
| FindTaclet | | abstract public class FindTaclet extends Taclet (Code) | | An abstract class to represent Taclets with a find part. This means, they
have to be attached to a formula or term of the sequent. This class is
extended by several subclasses to distinct between taclets that have to
attached to a top level formula of the antecedent (
AntecTaclet ),
to the succedent (
SuccTaclet ) or to an arbitrary term that matches
the find part somewhere in the sequent (
RewriteTaclet ).
|
| Method Summary | |
| public ListOfGoal | apply(Goal goal, Services services, RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application. | | abstract protected void | applyAdd(Sequent add, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)
| | abstract protected void | applyReplacewith(TacletGoalTemplate gt, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)
| | protected boolean | createCopies(Goal goal, PosInOccurrence posOfFind, MatchConditions matchCond)
Determine whether a replacewith-part is really supposed to modify
concerned formulas when applying a taclet (otherwise copies of the
formulas are created). | | public Term | find()
| | protected SetOfQuantifiableVariable | getBoundVariablesHelper()
| | public SetOfSchemaVariable | getIfFindVariables()
| | abstract protected boolean | ignoreTopLevelUpdates()
this method is used to determine if top level updates are
allowed to be ignored. | | public MatchConditions | matchFind(Term term, MatchConditions matchCond, Services services, Constraint userConstraint)
matches the given term against the taclet's find term and
Parameters:
term - the Term to be matched against the find expression of the taclet
Parameters:
matchCond - the MatchConditions with side conditions to be satisfied, eg. | | public ListOfSchemaVariable | readSet()
| | protected Taclet | setName(String s, FindTacletBuilder b)
| | public String | toString()
| | StringBuffer | toStringFind(StringBuffer sb)
| | public ListOfSchemaVariable | writeSet()
|
| find | | protected Term find(Code) | | contains the find term
|
| FindTaclet | | public FindTaclet(Name name, TacletApplPart applPart, ListOfTacletGoalTemplate goalTemplates, ListOfRuleSet ruleSets, Constraint constraint, TacletAttributes attrs, Term find, MapFromSchemaVariableToTacletPrefix prefixMap, SetOfChoice choices)(Code) | | creates a FindTaclet
Parameters:
name - the Name of the taclet
Parameters:
applPart - the TacletApplPart that contains the if-sequent, thenot-free and new-vars conditions
Parameters:
goalTemplates - a ListOfTacletGoalTemplate that contains all goaltemplates ofthe taclet (these are the instructions used to create new goals whenapplying the Taclet)
Parameters:
ruleSets - a ListOfRuleSet that contains all rule sets the Tacletis attached to
Parameters:
constraint - the Constraint of the Taclet (has to be fulfilled inorder to achieve this Taclet)
Parameters:
attrs - the TacletAttributes encoding if the Taclet is non-interactive,recursive or something like that
Parameters:
find - the Term that is the pattern that has to be found in asequent and the places where it matches the Taclet can be applied
Parameters:
prefixMap - a MapFromSchemaVariableToTacletPrefix that contains theprefix for each SchemaVariable in the Taclet |
| apply | | public ListOfGoal apply(Goal goal, Services services, RuleApp ruleApp)(Code) | | the rule is applied on the given goal using the
information of rule application.
Parameters:
goal - the goal that the rule application should refer to.
Parameters:
services - the Services encapsulating all java information
Parameters:
ruleApp - the taclet application that is executed. |
| applyAdd | | abstract protected void applyAdd(Sequent add, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)(Code) | | adds the sequent of the add part of the Taclet to the goal sequent
Parameters:
add - the Sequent to be added
Parameters:
goal - the Goal to be updated
Parameters:
posOfFind - the PosInOccurrence describes the place where to addthe semisequent
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions with all required instantiations |
| applyReplacewith | | abstract protected void applyReplacewith(TacletGoalTemplate gt, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)(Code) | | CONSTRAINT NOT USED
applies the replacewith part of Taclets
Parameters:
gt - TacletGoalTemplate used to get the replaceexpression in the Taclet
Parameters:
goal - the Goal where the rule is applied
Parameters:
posOfFind - the PosInOccurrence belonging to the find expression
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions with all required instantiations |
| createCopies | | protected boolean createCopies(Goal goal, PosInOccurrence posOfFind, MatchConditions matchCond)(Code) | | Determine whether a replacewith-part is really supposed to modify
concerned formulas when applying a taclet (otherwise copies of the
formulas are created). Copies are created whenever the constraint of the
new formulas is stronger than the conjunction of the original
find-formula constraint and the user constraint. (Taking the user
constraint into account at this point ensures that the existence of the
user constraint is transparent to the user, and is a temporary solution
to cope with the absence of disunification constraints).
UPDATE: for the time being we are only considering the old constraint of
the formula (as the user constraint is more or less disable in
TacletApp. canUseMVAPosteriori right now)
Parameters:
goal - the goal to which the taclet is applied
Parameters:
posOfFind - position of the find-formula (which is the formula whoseconstraint is considered as the original formula constraint)
Parameters:
matchCond - results of matching the taclet, in particular the newconstraint that is attached to formulas added by replacewith true iff replacewith is supposed to create copies of concernedformulas |
| find | | public Term find()(Code) | | returns the find term of the taclet to be matched
|
| getBoundVariablesHelper | | protected SetOfQuantifiableVariable getBoundVariablesHelper()(Code) | | returns the variables that occur bound in the find part
the variables that occur bound in the find part |
| getIfFindVariables | | public SetOfSchemaVariable getIfFindVariables()(Code) | | Set of schemavariables of the if and the (optional)find part |
| ignoreTopLevelUpdates | | abstract protected boolean ignoreTopLevelUpdates()(Code) | | this method is used to determine if top level updates are
allowed to be ignored. This is the case if we have an Antec or
SuccTaclet but not for a RewriteTaclet
true if top level updates shall be ignored |
| matchFind | | public MatchConditions matchFind(Term term, MatchConditions matchCond, Services services, Constraint userConstraint)(Code) | | matches the given term against the taclet's find term and
Parameters:
term - the Term to be matched against the find expression of the taclet
Parameters:
matchCond - the MatchConditions with side conditions to be satisfied, eg. partial instantiations of schema variables; beforecalling this method the constraint contained in the match conditionsmust be ensured to be satisfiable, i.e. matchCond.getConstraint ().isSatisfiable () must return true
Parameters:
services - the Services
Parameters:
userConstraint - a Constraint derived from user defined instantiations of meta variables the found schema variable mapping or null if the matching failed |
| readSet | | public ListOfSchemaVariable readSet()(Code) | | returns the variables in a Taclet with a read access
|
| toString | | public String toString()(Code) | | returns a representation of the Taclet with find part as String
string representation |
| writeSet | | public ListOfSchemaVariable writeSet()(Code) | | returns the variable in a Taclet to which is written to
|
| Methods inherited from de.uka.ilkd.key.rule.Taclet | protected void addToAntec(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected void addToSucc(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code)(Java Doc)
public SetOfSchemaVariable addedRuleNameVars()(Code)(Java Doc)
public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code)(Java Doc)
protected boolean admissibleAutomatic(ListOfRuleSet ruleSets)(Code)(Java Doc)
protected boolean admissibleInteractive(ListOfRuleSet ruleSets)(Code)(Java Doc)
abstract public ListOfGoal apply(Goal goal, Services services, RuleApp tacletApp)(Code)(Java Doc)
protected void applyAddProgVars(SetOfSchemaVariable pvs, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected void applyAddrule(ListOfTaclet rules, Goal goal, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected void cacheMatchInfo()(Code)(Java Doc)
public MatchConditions checkConditions(MatchConditions cond, Services services)(Code)(Java Doc)
protected ListOfGoal checkIfGoals(Goal p_goal, ListOfIfFormulaInstantiation p_list, MatchConditions p_matchCond, int p_numberOfNewGoals)(Code)(Java Doc)
public MatchConditions checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)(Code)(Java Doc)
public boolean closeGoal()(Code)(Java Doc)
public Constraint constraint()(Code)(Java Doc)
public String displayName()(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
public SetOfQuantifiableVariable getBoundVariables()(Code)(Java Doc)
abstract protected SetOfQuantifiableVariable getBoundVariablesHelper()(Code)(Java Doc)
public SetOfChoice getChoices()(Code)(Java Doc)
abstract public SetOfSchemaVariable getIfFindVariables()(Code)(Java Doc)
protected SetOfSchemaVariable getIfVariables()(Code)(Java Doc)
public SchemaVariable getNameCorrespondent(SchemaVariable p)(Code)(Java Doc)
public TacletPrefix getPrefix(SchemaVariable sv)(Code)(Java Doc)
public ListOfRuleSet getRuleSets()(Code)(Java Doc)
public IteratorOfVariableCondition getVariableConditions()(Code)(Java Doc)
public ListOfTacletGoalTemplate goalTemplates()(Code)(Java Doc)
public boolean hasReplaceWith()(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public String helpText()(Code)(Java Doc)
public Sequent ifSequent()(Code)(Java Doc)
public boolean isContextInPrefix()(Code)(Java Doc)
protected MatchConditions match(Term term, Term template, boolean ignoreUpdates, MatchConditions matchCond, Services services, Constraint userConstraint)(Code)(Java Doc)
protected MatchConditions match(Term term, Term template, MatchConditions matchCond, Services services, Constraint userConstraint)(Code)(Java Doc)
public IfMatchResult matchIf(IteratorOfIfFormulaInstantiation p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
public MatchConditions matchIf(IteratorOfIfFormulaInstantiation p_toMatch, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
final protected MatchConditions matchJavaBlock(Term term, Term template, MatchConditions matchCond, Services services)(Code)(Java Doc)
public Name name()(Code)(Java Doc)
public boolean noninteractive()(Code)(Java Doc)
public ListOfName oldNames()(Code)(Java Doc)
public MapFromSchemaVariableToTacletPrefix prefixMap()(Code)(Java Doc)
public ListOfSchemaVariable readSet()(Code)(Java Doc)
protected void replaceAtPos(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code)(Java Doc)
public IteratorOfRuleSet ruleSets()(Code)(Java Doc)
abstract protected Taclet setName(String s)(Code)(Java Doc)
protected Taclet setName(String s, TacletBuilder b)(Code)(Java Doc)
protected void setRestrictedMetavariables(Goal p_goal, MatchConditions p_matchCond)(Code)(Java Doc)
protected Term syntacticalReplace(Term term, Services services, MatchConditions mc)(Code)(Java Doc)
public String toString()(Code)(Java Doc)
StringBuffer toStringAttribs(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringGoalTemplates(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringIf(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringRuleSets(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringVarCond(StringBuffer sb)(Code)(Java Doc)
public NewVarcond varDeclaredNew(SchemaVariable var)(Code)(Java Doc)
protected boolean varIsBound(SchemaVariable v)(Code)(Java Doc)
public ListOfNewVarcond varsNew()(Code)(Java Doc)
public IteratorOfNewDependingOn varsNewDependingOn()(Code)(Java Doc)
public IteratorOfNotFreeIn varsNotFreeIn()(Code)(Java Doc)
public ListOfSchemaVariable writeSet()(Code)(Java Doc)
|
|
|