public abstract class TacletBuilder<T extends Taclet>
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
TacletBuilder.TacletBuilderException |
Modifier and Type | Field and Description |
---|---|
protected TacletAttributes |
attrs |
protected ImmutableSet<Choice> |
choices |
protected java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
goal2Choices |
protected ImmutableList<TacletGoalTemplate> |
goals |
protected Sequent |
ifseq |
protected Name |
name |
protected static Name |
NONAME |
protected java.lang.String |
origin |
protected ImmutableList<RuleSet> |
ruleSets |
protected Taclet |
taclet |
protected ImmutableSet<TacletAnnotation> |
tacletAnnotations |
protected ImmutableList<VariableCondition> |
variableConditions
List of additional generic conditions on the instantiations of
schema variables.
|
protected ImmutableList<NewVarcond> |
varsNew |
protected ImmutableList<NewDependingOn> |
varsNewDependingOn |
protected ImmutableList<NotFreeIn> |
varsNotFreeIn |
Constructor and Description |
---|
TacletBuilder() |
Modifier and Type | Method and Description |
---|---|
void |
addGoal2ChoicesMapping(TacletGoalTemplate gt,
ImmutableSet<Choice> soc)
adds a mapping from GoalTemplate
gt to SetOfsoc |
void |
addRuleSet(RuleSet rs)
adds a new rule set to the rule sets of the Taclet.
|
abstract void |
addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
void |
addVariableCondition(VariableCondition vc)
Add an additional generic condition on the instantiation of
schema variables.
|
void |
addVarsNew(ImmutableList<NewVarcond> list)
adds a list of new variables to the variable conditions of
the Taclet: v is new for all v's in the given list
|
void |
addVarsNew(NewVarcond nv)
adds a new new variable to the variable conditions of
the Taclet: v is new.
|
void |
addVarsNew(SchemaVariable v,
KeYJavaType type)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the given type
|
void |
addVarsNew(SchemaVariable v,
SchemaVariable peerSV)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the same type as peerSV
|
void |
addVarsNewDependingOn(SchemaVariable v0,
SchemaVariable v1)
Add a "v0 depending on v1"-statement.
|
void |
addVarsNotFreeIn(ImmutableList<NotFreeIn> 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.
|
void |
addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0,
java.lang.Iterable<? extends SchemaVariable> v1) |
void |
addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0,
SchemaVariable... v1) |
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.
|
ImmutableSet<Choice> |
getChoices() |
java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> |
getGoal2Choices() |
Name |
getName()
returns the name of the Taclet to be built
|
abstract T |
getTaclet()
builds and returns the Taclet that is specified by
former set...
|
T |
getTacletWithoutInactiveGoalTemplates(ImmutableSet<Choice> active) |
ImmutableList<TacletGoalTemplate> |
goalTemplates() |
Sequent |
ifSequent() |
void |
setAnnotations(ImmutableSet<TacletAnnotation> tacletAnnotations) |
void |
setChoices(ImmutableSet<Choice> choices) |
void |
setDisplayName(java.lang.String s)
sets an optional display name (presented to the user)
|
void |
setHelpText(java.lang.String s) |
void |
setIfSequent(Sequent seq)
sets the ifseq of the Taclet to be built
|
void |
setName(Name name)
sets the name of the Taclet to be built
|
void |
setOrigin(java.lang.String origin) |
void |
setRuleSets(ImmutableList<RuleSet> rs) |
void |
setTacletGoalTemplates(ImmutableList<TacletGoalTemplate> g) |
void |
setTrigger(Trigger trigger)
sets the trigger
|
java.util.Iterator<NotFreeIn> |
varsNotFreeIn() |
protected static final Name NONAME
protected Taclet taclet
protected Name name
protected Sequent ifseq
protected ImmutableList<NewVarcond> varsNew
protected ImmutableList<NotFreeIn> varsNotFreeIn
protected ImmutableList<NewDependingOn> varsNewDependingOn
protected ImmutableList<TacletGoalTemplate> goals
protected ImmutableList<RuleSet> ruleSets
protected TacletAttributes attrs
protected ImmutableList<VariableCondition> variableConditions
protected java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> goal2Choices
protected ImmutableSet<Choice> choices
protected ImmutableSet<TacletAnnotation> tacletAnnotations
protected java.lang.String origin
public void setAnnotations(ImmutableSet<TacletAnnotation> tacletAnnotations)
public void setTrigger(Trigger trigger)
public Name getName()
public void setName(Name name)
public void setDisplayName(java.lang.String s)
public void setHelpText(java.lang.String s)
public void setIfSequent(Sequent seq)
public void addGoal2ChoicesMapping(TacletGoalTemplate gt, ImmutableSet<Choice> soc)
gt
to SetOfsoc
public java.util.HashMap<TacletGoalTemplate,ImmutableSet<Choice>> getGoal2Choices()
public void setChoices(ImmutableSet<Choice> choices)
public ImmutableSet<Choice> getChoices()
public void addVarsNew(SchemaVariable v, SchemaVariable peerSV)
public void addVarsNew(SchemaVariable v, KeYJavaType type)
public void addVarsNew(NewVarcond nv)
public void addVarsNew(ImmutableList<NewVarcond> list)
public void addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1)
public void addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0, java.lang.Iterable<? extends SchemaVariable> v1)
public void addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0, SchemaVariable... v1)
public void addVarsNotFreeIn(ImmutableList<NotFreeIn> list)
public void addVarsNewDependingOn(SchemaVariable v0, SchemaVariable v1)
public void addVariableCondition(VariableCondition vc)
public abstract void addTacletGoalTemplate(TacletGoalTemplate goal)
public void addRuleSet(RuleSet rs)
public void setRuleSets(ImmutableList<RuleSet> rs)
public Sequent ifSequent()
public ImmutableList<TacletGoalTemplate> goalTemplates()
public java.util.Iterator<NotFreeIn> varsNotFreeIn()
public void setTacletGoalTemplates(ImmutableList<TacletGoalTemplate> g)
public abstract T getTaclet()
public T getTacletWithoutInactiveGoalTemplates(ImmutableSet<Choice> active)
public void setOrigin(java.lang.String origin)
Copyright © 2003-2019 The KeY-Project.