| java.lang.Object
 de.uka.ilkd.key.rule.Taclet
de.uka.ilkd.key.rule.FindTaclet
de.uka.ilkd.key.rule.SuccTaclet
| SuccTaclet | | public class SuccTaclet extends FindTaclet (Code) | | A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
| Constructor Summary | |
| public | SuccTaclet(Name name, TacletApplPart applPart, ListOfTacletGoalTemplate goalTemplates, ListOfRuleSet heuristics, Constraint constraint, TacletAttributes attrs, Term find, MapFromSchemaVariableToTacletPrefix prefixMap, SetOfChoice choices)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent. |
| SuccTaclet | | public SuccTaclet(Name name, TacletApplPart applPart, ListOfTacletGoalTemplate goalTemplates, ListOfRuleSet heuristics, Constraint constraint, TacletAttributes attrs, Term find, MapFromSchemaVariableToTacletPrefix prefixMap, SetOfChoice choices)(Code) | | creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
Parameters:
name - the name of the Taclet
Parameters:
applPart - contains the application part of an Taclet that isthe if-sequent, the variable conditions
Parameters:
goalTemplates - a list of goal descriptions.
Parameters:
heuristics - a list of heurisics for the Taclet
Parameters:
constraint - the Constraint under which the Taclet is valid
Parameters:
attrs - attributes for the Taclet; these are boolean valuesindicating a noninteractive or recursive use of the Taclet.
Parameters:
find - the find term of the Taclet
Parameters:
prefixMap - a MapFromSchemaVariableToTacletPrefix that contains theprefix for each SchemaVariable in the Taclet |
| applyAdd | | 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:
matchCond - the MatchConditions with all required instantiations |
| applyReplacewith | | 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 |
| ignoreTopLevelUpdates | | 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 |
| Methods inherited from de.uka.ilkd.key.rule.FindTaclet | public ListOfGoal apply(Goal goal, Services services, RuleApp ruleApp)(Code)(Java Doc)
abstract protected void applyAdd(Sequent add, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)(Code)(Java Doc)
abstract protected void applyReplacewith(TacletGoalTemplate gt, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected boolean createCopies(Goal goal, PosInOccurrence posOfFind, MatchConditions matchCond)(Code)(Java Doc)
public Term find()(Code)(Java Doc)
protected SetOfQuantifiableVariable getBoundVariablesHelper()(Code)(Java Doc)
public SetOfSchemaVariable getIfFindVariables()(Code)(Java Doc)
abstract protected boolean ignoreTopLevelUpdates()(Code)(Java Doc)
public MatchConditions matchFind(Term term, MatchConditions matchCond, Services services, Constraint userConstraint)(Code)(Java Doc)
public ListOfSchemaVariable readSet()(Code)(Java Doc)
protected Taclet setName(String s, FindTacletBuilder b)(Code)(Java Doc)
public String toString()(Code)(Java Doc)
StringBuffer toStringFind(StringBuffer sb)(Code)(Java Doc)
public ListOfSchemaVariable writeSet()(Code)(Java Doc)
|
| 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)
|
|
|