public class InfFlowContractAppTaclet extends RewriteTaclet
Taclet.TacletLabelHint
Modifier and Type | Field and Description |
---|---|
private static ImmutableSet<Name> |
alreadyRegistered |
static java.lang.String |
USE_IF |
ANTECEDENT_POLARITY, IN_SEQUENT_STATE, NONE, SAME_UPDATE_LEVEL, SUCCEDENT_POLARITY
find
choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString
Constructor and Description |
---|
InfFlowContractAppTaclet(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) |
InfFlowContractAppTaclet(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) |
Modifier and Type | Method and Description |
---|---|
protected void |
createAndInitializeExecutor() |
static boolean |
hasType(Rule rule) |
static void |
register(Name name) |
static boolean |
registered(Name name) |
InfFlowContractAppTaclet |
setName(java.lang.String s) |
static boolean |
unregister(Name name) |
checkPrefix, getApplicationRestriction, getExecutor, getRewriteResult, ignoreTopLevelUpdates, toStringFind
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, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn
public static final java.lang.String USE_IF
private static ImmutableSet<Name> alreadyRegistered
public InfFlowContractAppTaclet(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)
public InfFlowContractAppTaclet(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)
public static boolean hasType(Rule rule)
public static boolean registered(Name name)
public static void register(Name name)
public static boolean unregister(Name name)
protected void createAndInitializeExecutor()
createAndInitializeExecutor
in class RewriteTaclet
public InfFlowContractAppTaclet setName(java.lang.String s)
setName
in class RewriteTaclet