| java.lang.Object
 de.uka.ilkd.key.rule.TacletBuilder
All known Subclasses: de.uka.ilkd.key.rule.NoFindTacletBuilder, de.uka.ilkd.key.rule.FindTacletBuilder,
| TacletBuilder | | abstract public class TacletBuilder (Code) | | subclasss build Schematic Theory Specific Rules (Taclets)
|
| Method Summary | |
| public void | addGoal2ChoicesMapping(TacletGoalTemplate gt, SetOfChoice soc)
| | public void | addOldName(String s)
| | public void | addRuleSet(RuleSet rs)
adds a new rule set to the rule sets of the Taclet. | | abstract public void | addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet. | | public void | addVariableCondition(VariableCondition vc)
Add an additional generic condition on the instatiation of
schema variables. | | public void | addVarsNew(SchemaVariable v, SchemaVariable asSort, boolean elementsort)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the sort as asSort if elementsort=false and the
sort of the elements of asSort if elementsort=true and asSort is a program
array SV. | | public void | addVarsNew(SchemaVariable v, SchemaVariable asSort)
| | public void | addVarsNew(SchemaVariable v, Sort sort)
| | public void | addVarsNew(NewVarcond nv)
adds a new new variable to the variable conditions of
the Taclet: v is new. | | public void | addVarsNew(ListOfNewVarcond list)
| | public void | addVarsNewDependingOn(SchemaVariable v0, SchemaVariable v1)
Add a "v0 depending on v1"-statement. | | public void | addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1)
adds a new NotFreeIn variable pair to the variable conditions of
the Taclet: v0 is not free in v1. | | public void | addVarsNotFreeIn(ListOfNotFreeIn list)
adds a list of NotFreeIn variable pairs to the variable
conditions of
the Taclet: v0 is not free in v1 for all entries (v0,v1) in the given list. | | static void | checkContainsFreeVarSV(Sequent seq, Name tacletName, String str)
| | static void | checkContainsFreeVarSV(Term t, Name tacletName, String str)
| | public SetOfChoice | getChoices()
| | public HashMap | getGoal2Choices()
| | public Name | getName()
| | abstract public Taclet | getTaclet()
builds and returns the Taclet that is specified by
former set... | | public Taclet | getTacletWithoutInactiveGoalTemplates(SetOfChoice active)
| | public ListOfTacletGoalTemplate | goalTemplates()
| | public Sequent | ifSequent()
| | public void | setChoices(SetOfChoice choices)
| | public void | setConstraint(Constraint constraint)
| | public void | setDisplayName(String s)
| | public void | setHelpText(String s)
| | public void | setIfSequent(Sequent seq)
| | public void | setName(Name name)
| | public void | setNoninteractive(boolean ni)
sets the noninteractive flag to the given value. | | public void | setRuleSets(ListOfRuleSet rs)
| | public void | setTacletGoalTemplates(ListOfTacletGoalTemplate g)
| | public IteratorOfNotFreeIn | varsNotFreeIn()
|
| choices | | protected SetOfChoice choices(Code) | | |
| goals | | protected ListOfTacletGoalTemplate goals(Code) | | |
| ruleSets | | protected ListOfRuleSet ruleSets(Code) | | |
| variableConditions | | protected ListOfVariableCondition variableConditions(Code) | | List of additional generic conditions on the instantiations of
schema variables.
|
| varsNew | | protected ListOfNewVarcond varsNew(Code) | | |
| varsNewDependingOn | | protected ListOfNewDependingOn varsNewDependingOn(Code) | | |
| varsNotFreeIn | | protected ListOfNotFreeIn varsNotFreeIn(Code) | | |
| addGoal2ChoicesMapping | | public void addGoal2ChoicesMapping(TacletGoalTemplate gt, SetOfChoice soc)(Code) | | adds a mapping from GoalTemplate gt to SetOfChoice
soc
|
| addOldName | | public void addOldName(String s)(Code) | | adds an old name to the list of old names
|
| addRuleSet | | public void addRuleSet(RuleSet rs)(Code) | | adds a new rule set to the rule sets of the Taclet.
|
| addTacletGoalTemplate | | abstract public void addTacletGoalTemplate(TacletGoalTemplate goal)(Code) | | adds a new goal descriptions to the goal descriptions of the Taclet.
The TacletGoalTemplate must be of
the appropriate kind (Rewrite/Ante/Succ),
otherwise an IllegalArgumentException is thrown.
|
| addVariableCondition | | public void addVariableCondition(VariableCondition vc)(Code) | | Add an additional generic condition on the instatiation of
schema variables.
|
| addVarsNew | | public void addVarsNew(SchemaVariable v, SchemaVariable asSort, boolean elementsort)(Code) | | adds a new new variable to the variable conditions of
the Taclet: v is new and has the sort as asSort if elementsort=false and the
sort of the elements of asSort if elementsort=true and asSort is a program
array SV.
|
| addVarsNew | | public void addVarsNew(SchemaVariable v, SchemaVariable asSort)(Code) | | adds a new new variable to the variable conditions of
the Taclet: v is new and has the sort as asSort
|
| addVarsNew | | public void addVarsNew(SchemaVariable v, Sort sort)(Code) | | adds a new new variable to the variable conditions of
the Taclet: v is new and has type sort
|
| addVarsNew | | public void addVarsNew(NewVarcond nv)(Code) | | adds a new new variable to the variable conditions of
the Taclet: v is new.
|
| addVarsNew | | public void addVarsNew(ListOfNewVarcond list)(Code) | | adds a list of new variables to the variable conditions of
the Taclet: v is new for all v's in the given list
|
| addVarsNewDependingOn | | public void addVarsNewDependingOn(SchemaVariable v0, SchemaVariable v1)(Code) | | Add a "v0 depending on v1"-statement. "v0" may not occur within
the if sequent or the find formula/term, however, this is not
checked
|
| addVarsNotFreeIn | | public void addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1)(Code) | | adds a new NotFreeIn variable pair to the variable conditions of
the Taclet: v0 is not free in v1.
|
| addVarsNotFreeIn | | public void addVarsNotFreeIn(ListOfNotFreeIn list)(Code) | | adds a list of NotFreeIn variable pairs to the variable
conditions of
the Taclet: v0 is not free in v1 for all entries (v0,v1) in the given list.
|
| getChoices | | public SetOfChoice getChoices()(Code) | | |
| getName | | public Name getName()(Code) | | returns the name of the Taclet to be built
|
| getTaclet | | abstract public Taclet getTaclet()(Code) | | builds and returns the Taclet that is specified by
former set... / add... methods. If no name is specified then
an Taclet with an empty string name is build. No specifications
for variable conditions, goals or rule sets imply that the
corresponding parts of the Taclet are empty. No specification for
the if-sequence is represented as a sequent with two empty
semisequences. No specification for the interactive or
recursive flags imply that the flags are not set.
No specified find part for Taclets that require a find part
causes an IllegalStateException.
|
| getTacletWithoutInactiveGoalTemplates | | public Taclet getTacletWithoutInactiveGoalTemplates(SetOfChoice active)(Code) | | |
| goalTemplates | | public ListOfTacletGoalTemplate goalTemplates()(Code) | | |
| setChoices | | public void setChoices(SetOfChoice choices)(Code) | | |
| setConstraint | | public void setConstraint(Constraint constraint)(Code) | | sets the constraint that has to be satisfied if the Taclet
should be valid
|
| setDisplayName | | public void setDisplayName(String s)(Code) | | sets an optional display name (presented to the user)
|
| setIfSequent | | public void setIfSequent(Sequent seq)(Code) | | sets the ifseq of the Taclet to be built
|
| setName | | public void setName(Name name)(Code) | | sets the name of the Taclet to be built
|
| setNoninteractive | | public void setNoninteractive(boolean ni)(Code) | | sets the noninteractive flag to the given value.
|
| setRuleSets | | public void setRuleSets(ListOfRuleSet rs)(Code) | | |
| setTacletGoalTemplates | | public void setTacletGoalTemplates(ListOfTacletGoalTemplate g)(Code) | | |
| varsNotFreeIn | | public IteratorOfNotFreeIn varsNotFreeIn()(Code) | | |
|
|