public abstract class FindTaclet extends Taclet
AntecTaclet
),
to the succedent (SuccTaclet
) or to an arbitrary term that matches
the find part somewhere in the sequent (RewriteTaclet
).Taclet.TacletLabelHint
Modifier and Type | Field and Description |
---|---|
protected Term |
find
contains the find term
|
private ImmutableSet<SchemaVariable> |
ifFindVariables
Set of schemavariables of the if and the (optional) find part
|
choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString
Modifier | Constructor and Description |
---|---|
protected |
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
protected |
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object o)
return true if
o is a taclet of the same name and
o and this contain no mutually exclusive
taclet options. |
Term |
find()
returns the find term of the taclet to be matched
|
protected ImmutableSet<QuantifiableVariable> |
getBoundVariablesHelper()
returns the variables that occur bound in the find part
|
ImmutableSet<SchemaVariable> |
getIfFindVariables() |
int |
hashCode() |
abstract boolean |
ignoreTopLevelUpdates()
this method is used to determine if top level updates are
allowed to be ignored.
|
java.lang.String |
toString()
returns a representation of the Taclet with find part as String
|
protected java.lang.StringBuffer |
toStringFind(java.lang.StringBuffer sb) |
admissible, admissibleAutomatic, admissibleInteractive, apply, closeGoal, collectSchemaVars, createAndInitializeExecutor, createAndInitializeMatcher, createTacletServices, displayName, getBoundVariables, getChoices, getExecutor, getIfVariables, getMatcher, getNameCorrespondent, getPrefix, getRuleJustification, getRuleSets, getSurviveSymbExec, getTrigger, getVariableConditions, goalTemplates, hasReplaceWith, hasTrigger, ifSequent, isContextInPrefix, name, prefixMap, ruleSets, setName, toStringAttribs, toStringGoalTemplates, toStringIf, toStringRuleSets, toStringVarCond, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn
protected Term find
private ImmutableSet<SchemaVariable> ifFindVariables
protected FindTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, boolean surviveSymbExec, ImmutableSet<TacletAnnotation> tacletAnnotations)
name
- the Name of the tacletapplPart
- the TacletApplPart that contains the if-sequent, the
not-free and new-vars conditionsgoalTemplates
- a IListruleSets
- a IListattrs
- the TacletAttributes encoding if the Taclet is non-interactive,
recursive or something like thatfind
- the Term that is the pattern that has to be found in a
sequent and the places where it matches the Taclet can be appliedprefixMap
- a ImmMapprotected FindTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations)
name
- the Name of the tacletapplPart
- the TacletApplPart that contains the if-sequent, the
not-free and new-vars conditionsgoalTemplates
- a IListruleSets
- a IListattrs
- the TacletAttributes encoding if the Taclet is non-interactive,
recursive or something like thatfind
- the Term that is the pattern that has to be found in a
sequent and the places where it matches the Taclet can be appliedprefixMap
- a ImmMappublic abstract boolean ignoreTopLevelUpdates()
public Term find()
protected java.lang.StringBuffer toStringFind(java.lang.StringBuffer sb)
public java.lang.String toString()
public ImmutableSet<SchemaVariable> getIfFindVariables()
getIfFindVariables
in class Taclet
public boolean equals(java.lang.Object o)
Taclet
o
is a taclet of the same name and
o
and this
contain no mutually exclusive
taclet options.protected ImmutableSet<QuantifiableVariable> getBoundVariablesHelper()
getBoundVariablesHelper
in class Taclet