public class RewriteTaclet extends FindTaclet
Taclet.TacletLabelHint
Modifier and Type | Field and Description |
---|---|
static int |
ANTECEDENT_POLARITY
If the surrounding formula has been decomposed completely, the find-term
will NOT appear on the SUCcedent.
|
private int |
applicationRestriction
encodes restrictions on the state where a rewrite taclet is applicable
If the value is equal to
NONE no state restrictions are posed
SAME_UPDATE_LEVEL then \assumes
must match on a formula within the same state as \find
rsp. |
static int |
IN_SEQUENT_STATE
all taclet constituents must be in the same state
as the sequent
|
static int |
NONE
does not pose state restrictions on valid matchings
|
static int |
SAME_UPDATE_LEVEL
all taclet constituents must appear in the same state
(and not below a modality (for efficiency reasons))
|
static int |
SUCCEDENT_POLARITY
If the surrounding formula has been decomposed completely, the find-term
will NOT appear on the ANTEcedent.
|
find
choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString
Constructor and Description |
---|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
checkPrefix(PosInOccurrence p_pos,
MatchConditions p_mc)
For taclets with
getSameUpdatePrefix () , collect
the updates above p_pos and add them to the update
context of the instantiations object p_mc . |
protected void |
createAndInitializeExecutor() |
int |
getApplicationRestriction()
returns the int encoding the kind of state restriction this rewrite
taclet must obey
|
RewriteTacletExecutor<? extends RewriteTaclet> |
getExecutor() |
SequentFormula |
getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
boolean |
ignoreTopLevelUpdates()
this method is used to determine if top level updates are
allowed to be ignored.
|
private int |
polarity(Operator op,
PIOPathIterator it,
int polarity)
Compute polarity
|
RewriteTaclet |
setName(java.lang.String s) |
protected java.lang.StringBuffer |
toStringFind(java.lang.StringBuffer sb) |
private boolean |
veto(Term t)
the top level operator has to be a simultaneous update.
|
equals, find, getBoundVariablesHelper, getIfFindVariables, hashCode, toString
admissible, admissibleAutomatic, admissibleInteractive, apply, closeGoal, collectSchemaVars, createAndInitializeMatcher, createTacletServices, displayName, getBoundVariables, getChoices, getIfVariables, getMatcher, getNameCorrespondent, getPrefix, getRuleJustification, getRuleSets, getSurviveSymbExec, getTrigger, getVariableConditions, goalTemplates, hasReplaceWith, hasTrigger, ifSequent, isContextInPrefix, name, prefixMap, ruleSets, toStringAttribs, toStringGoalTemplates, toStringIf, toStringRuleSets, toStringVarCond, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn
public static final int NONE
public static final int SAME_UPDATE_LEVEL
public static final int IN_SEQUENT_STATE
public static final int ANTECEDENT_POLARITY
public static final int SUCCEDENT_POLARITY
private int applicationRestriction
NONE
no state restrictions are posedSAME_UPDATE_LEVEL
then \assumes
must match on a formula within the same state as \find
rsp. \add
. For efficiency no modalities are allowed above
the \find
position IN_SEQUENT_STATE
the \find
part is
only allowed to match on formulas which are evaluated in the same state as
the sequentpublic RewriteTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, int p_applicationRestriction, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations)
name
- the Name of the TacletapplPart
- the TacletApplPart that contains the application part of an Taclet that is
the if-sequent, the variable conditionsgoalTemplates
- a list of goal descriptions.ruleSets
- a list of rule sets for the Tacletattrs
- the TacletAttributes; these are boolean values
indicating a noninteractive or recursive use of the Taclet.find
- the find term of the TacletprefixMap
- a ImmMapp_applicationRestriction
- an int defining state restrictions of the taclet
(required for location check)choices
- the SetOfpublic RewriteTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, int p_applicationRestriction, ImmutableSet<Choice> choices, boolean surviveSymbExec, ImmutableSet<TacletAnnotation> tacletAnnotations)
protected void createAndInitializeExecutor()
createAndInitializeExecutor
in class Taclet
public boolean ignoreTopLevelUpdates()
ignoreTopLevelUpdates
in class FindTaclet
public int getApplicationRestriction()
private boolean veto(Term t)
t
- the Term to checkpublic MatchConditions checkPrefix(PosInOccurrence p_pos, MatchConditions p_mc)
getSameUpdatePrefix ()
, collect
the updates above p_pos
and add them to the update
context of the instantiations object p_mc
.null
, if program modalities appear above
p_pos
private int polarity(Operator op, PIOPathIterator it, int polarity)
seems to reimplement this.
protected java.lang.StringBuffer toStringFind(java.lang.StringBuffer sb)
toStringFind
in class FindTaclet
public RewriteTacletExecutor<? extends RewriteTaclet> getExecutor()
getExecutor
in class Taclet
public SequentFormula getRewriteResult(Goal goal, TermLabelState termLabelState, Services services, TacletApp app)
public RewriteTaclet setName(java.lang.String s)