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 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,
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 |
addVarsNew(SchemaVariable v,
Type type)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the given type
|
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.
|
(package private) static void |
checkContainsFreeVarSV(Sequent seq,
Name tacletName,
java.lang.String str) |
(package private) static void |
checkContainsFreeVarSV(Term t,
Name tacletName,
java.lang.String str) |
private static boolean |
containsFreeVarSV(Sequent sequent) |
private static boolean |
containsFreeVarSV(Term t) |
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... / add... methods.
|
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 |
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
public void setAnnotations(ImmutableSet<TacletAnnotation> tacletAnnotations)
private static boolean containsFreeVarSV(Term t)
private static boolean containsFreeVarSV(Sequent sequent)
static void checkContainsFreeVarSV(Sequent seq, Name tacletName, java.lang.String str)
static void checkContainsFreeVarSV(Term t, Name tacletName, java.lang.String str)
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, Type 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)