| java.lang.Object
 de.uka.ilkd.key.rule.TacletApp
All known Subclasses: de.uka.ilkd.key.rule.NoPosTacletApp, de.uka.ilkd.key.rule.PosTacletApp,
| TacletApp | | abstract public class TacletApp implements RuleApp(Code) | | A TacletApp object contains information required for a concrete application.
These information may consist of
- instantiations of the schemavariables
- position of the find term
Its methods complete or sufficientlyComplete are
used to determine if the information is complete or at least sufficient
(can be completed using meta variables) complete, so that is can be
applied.
|
| Method Summary | |
| public TacletApp | addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)
creates a new Tacletapp where the SchemaVariable sv is
instantiated with the the given Term term. | | public TacletApp | addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)
checks if the instantiation of sv with pe
is possible. | | abstract public TacletApp | addInstantiation(SchemaVariable sv, Term term, boolean interesting)
| | abstract public TacletApp | addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)
| | abstract public TacletApp | addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)
adds a new instantiation to this TacletApp. | | public TacletApp | addInstantiation(SchemaVariable sv, Name name)
| | abstract public TacletApp | addInstantiation(SVInstantiations svi)
| | public boolean | admissible(boolean interactive, ListOfRuleSet ruleSets)
| | protected static SetOfQuantifiableVariable | boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)
| | protected static SetOfQuantifiableVariable | boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)
| | protected SetOfSchemaVariable | calculateNeededNonInstantiatedSV()
Calculate needed SchemaVariables that have not been
instantiated yet and cannot be instantiated using
metavariables. | | protected SetOfSchemaVariable | calculateNonInstantiatedSV()
calculate needed SchemaVariables that have not been
instantiated yet. | | protected boolean | canUseMVAPosteriori(SchemaVariable p_var, Term p_term)
| | public boolean | canUseMVAPriori(SchemaVariable p_var)
| | public static boolean | checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)
checks if the variable conditions of type 'x not free in y' are
hold by the found instantiations. | | protected static SetOfQuantifiableVariable | collectBoundVarsAbove(PosInOccurrence pos)
| | abstract public boolean | complete()
returns true iff all necessary informations are collected, so
that the Taclet can be applied. | | public Constraint | constraint()
| | abstract protected SetOfQuantifiableVariable | contextVars(SchemaVariable sv)
| | public TacletApp | createSkolemConstant(String instantiation, SchemaVariable sv, boolean interesting, Services services)
Create a new constant named "instantiation" and instantiate
"sv" with. | | public TacletApp | createSkolemConstant(String instantiation, SchemaVariable sv, Sort sort, boolean interesting)
| | public TacletApp | createSkolemFunctions(Namespace p_func_ns, Services services)
| | public boolean | equals(Object o)
compares the given Object with this one and returns true iff both are
from type TacletApp with equal taclets, instantiations and positions. | | public ListOfGoal | execute(Goal goal, Services services)
| | public Namespace | extendVarNamespaceForSV(Namespace var_ns, SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations
of the schema variables in the context of the given schema
variable and (if the TacletApp's prefix has the context flag set)
by adding names of the logic variables of the context. | | public ListOfTacletApp | findIfFormulaInstantiations(Sequent p_seq, Services p_services, Constraint p_userConstraint)
Find all possible instantiations of the if sequent formulas
within the sequent "p_seq". | | public Sort | getRealSort(SchemaVariable p_sv, Services services)
| | public int | hashCode()
| | public ListOfIfFormulaInstantiation | ifFormulaInstantiations()
| | public boolean | ifInstsComplete()
| | protected static boolean | ifInstsCorrectSize(Taclet p_taclet, ListOfIfFormulaInstantiation p_list)
| | public TacletApp | instantiateWithMV(Goal p_goal)
Make the instantiation complete using metavariables and convert plain
instantiations to metavariables and user constraint entries if possible. | | public SVInstantiations | instantiations()
returns the instantiations for the application of the Taclet at the
specified position. | | public boolean | instsSufficientlyComplete()
| | public boolean | isDependingOnModifiesSV(SchemaVariable sv)
| | public MatchConditions | matchConditions()
| | public SetOfSchemaVariable | neededUninstantiatedVars()
| | public SetOfMetavariable | newMetavariables()
| | abstract public PosInOccurrence | posInOccurrence()
| | public TacletApp | prepareUserInstantiation()
checks if there are name conflicts (i.e. | | protected static SVInstantiations | replaceInstantiation(Taclet taclet, SVInstantiations insts, SchemaVariable varSV)
returns a new SVInstantiations that modifies the given
SVInstantiations insts at the bound SchemaVariable varSV to a new LogicVariable. | | protected static SVInstantiations | resolveCollisionVarSV(Taclet taclet, SVInstantiations insts)
| | public Rule | rule()
| | abstract protected TacletApp | setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)
| | public TacletApp | setIfFormulaInstantiations(ListOfIfFormulaInstantiation p_list, Services p_services, Constraint p_userConstraint)
Creates a new Taclet application by matching the given formulas
against the formulas of the if sequent, adding SV
instantiations, constraints and metavariables as needed. | | abstract protected TacletApp | setInstantiation(SVInstantiations svi)
| | abstract protected TacletApp | setMatchConditions(MatchConditions mc)
| | public PosTacletApp | setPosInOccurrence(PosInOccurrence pos)
| | abstract public boolean | sufficientlyComplete()
| | public Taclet | taclet()
| | public String | toString()
| | public TacletApp | tryToInstantiate(Goal goal, Services services)
| | public SetOfSchemaVariable | uninstantiatedVars()
returns the variables that have not yet been instantiated and
need to be instantiated to apply the Taclet. | | public SchemaVariable | varSVNameConflict()
returns the bound SchemaVariable that causes a name conflict (i.e. |
| fixedVars | | protected SetOfSchemaVariable fixedVars(Code) | | the instantiations of the following SVs must not be changed;
they must not be instantiated with metavariables either
|
| ifInstantiations | | ListOfIfFormulaInstantiation ifInstantiations(Code) | | choosen instantiations for the if sequent formulas
|
| instantiations | | protected SVInstantiations instantiations(Code) | | contains the instantiations of the schemavarioables of the
Taclet
|
| matchConstraint | | protected Constraint matchConstraint(Code) | | constraint under which the taclet application can be performed
|
| matchNewMetavariables | | protected SetOfMetavariable matchNewMetavariables(Code) | | metavariables that have been created during the matching
|
| updateContextFixed | | protected boolean updateContextFixed(Code) | | the update context given by the current instantiations must not
be changed
|
| TacletApp | | TacletApp(Taclet taclet)(Code) | | constructs a TacletApp for the given taclet, with an empty instantiation
map
|
| TacletApp | | TacletApp(Taclet taclet, SVInstantiations instantiations)(Code) | | constructs a TacletApp for the given taclet. With some information about
required instantiations.
|
| addCheckedInstantiation | | public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)(Code) | | creates a new Tacletapp where the SchemaVariable sv is
instantiated with the the given Term term. Sort equality is
checked. If the check fails an IllegalArgumentException is
thrown
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
term - the Term the SchemaVariable is instantiated with the new TacletApp |
| addCheckedInstantiation | | public TacletApp addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)(Code) | | checks if the instantiation of sv with pe
is possible. If the resulting instantiation is valid a new taclet application
with an extended instantiation mapping is created and returned. Otherwise an
exception is thrown.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pe - the ProgramElement the SV is instantiated with
Parameters:
services - the Services
Parameters:
interesting - a boolean marking if the instantiation of thissv needs to be saved for later proof loading (interesting==true)or if it can be derived deterministically (e.g. by matching) (interesting==false) a new taclet application equal to this one but including thenewly added instantiation entry (sv, pe), if theinstantiation results in a valid taclet application otherwise an exception is thrown
throws:
IllegalInstantiationException - exception thrown if sv cannot be instantiated with pe no matter if in generalor due to side conditions posed by this particular application |
| addInstantiation | | abstract public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting)(Code) | | adds a new instantiation to this TacletApp
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
term - the Term the SchemaVariable is instantiated with the new TacletApp |
| addInstantiation | | abstract public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code) | | adds a new instantiation to this TacletApp. This method does not
check (beside some very rudimentary tests) if the instantiation is possible.
If you cannot guarantee that adding the entry (sv, pe) will
result in a valid taclet instantiation, you have to use
TacletApp.addCheckedInstantiation(SchemaVariable,ProgramElement,Services,boolean) instead
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pe - the ProgramElement the SV is instantiated with
Parameters:
interesting - a boolean marking if the instantiation of thissv needs to be saved for later proof loading (interesting==true)or if it can be derived deterministically (e.g. by matching) (interesting==false) a new taclet application equal to this one but including thenewly added instantiation entry (sv, pe) |
| addInstantiation | | abstract public TacletApp addInstantiation(SVInstantiations svi)(Code) | | creates a new Taclet application containing all the
instantiations given
by the SVInstantiations
Parameters:
svi - the SVInstantiations whose entries are the neededinstantiations the new Taclet application |
| admissible | | public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code) | | true iff the Taclet may be applied for thegiven mode (interactive/non-interactive, activated rule sets) |
| boundAtOccurrenceSet | | protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)(Code) | | collects all bound variables above the occurrence of the schemavariable
whose prefix is given
Parameters:
prefix - the TacletPrefix of the schemavariable
Parameters:
instantiations - the SVInstantiations so that thefind(if)-expression matches set of the bound variables |
| boundAtOccurrenceSet | | protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)(Code) | | collects all bound variables above the occurrence of the schemavariable
whose prefix is given
Parameters:
prefix - the TacletPrefix of the schemavariable
Parameters:
instantiations - the SVInstantiations so that thefind(if)-expression matches
Parameters:
pos - the posInOccurrence describing the position of theschemavariable set of the bound variables |
| calculateNeededNonInstantiatedSV | | protected SetOfSchemaVariable calculateNeededNonInstantiatedSV()(Code) | | Calculate needed SchemaVariables that have not been
instantiated yet and cannot be instantiated using
metavariables. This is a subset of
calculateNonInstantiatedSV();
SetOfSchemaVariable that need to be instantiated butare not |
| calculateNonInstantiatedSV | | protected SetOfSchemaVariable calculateNonInstantiatedSV()(Code) | | calculate needed SchemaVariables that have not been
instantiated yet. This means to ignore SchemaVariables that
appear only in addrule-sections of Taclets
SetOfSchemaVariable that need to be instantiated butare not |
| canUseMVAPosteriori | | protected boolean canUseMVAPosteriori(SchemaVariable p_var, Term p_term)(Code) | | For a given SV of the taclet decide a posteriori whether an
instantiation via metavariable is possible
Parameters:
p_term - Term to instantiate the schemavariable with |
| canUseMVAPriori | | public boolean canUseMVAPriori(SchemaVariable p_var)(Code) | | For a given SV of the taclet decide a priori whether an
instantiation via metavariable is possible
true iff p_var is a termSV with empty prefix |
| checkVarCondNotFreeIn | | public static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)(Code) | | checks if the variable conditions of type 'x not free in y' are
hold by the found instantiations. The variable conditions is used
implicit in the prefix. (Used to calculate the prefix)
Parameters:
taclet - the Taclet that is tried to be instantiated. A match for thefind (or/and if) has been found.
Parameters:
instantiations - the SVInstantiations so that the find(if)expression matches
Parameters:
pos - the PosInOccurrence where the Taclet is applied true iff all variable conditions x not free in y are hold |
| collectBoundVarsAbove | | protected static SetOfQuantifiableVariable collectBoundVarsAbove(PosInOccurrence pos)(Code) | | collects all bound vars that are bound above the subterm described by
the given term position information
Parameters:
pos - the PosInOccurrence describing a subterm in Term a set of logic variables that are bound above the specifiedsubterm |
| complete | | abstract public boolean complete()(Code) | | returns true iff all necessary informations are collected, so
that the Taclet can be applied.
true iff all necessary informations are collected, sothat the Taclet can be applied. |
| createSkolemConstant | | public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, boolean interesting, Services services)(Code) | | Create a new constant named "instantiation" and instantiate
"sv" with. This constant will later (by
"createSkolemFunctions") be replaced by a function having
the occurring metavariables as arguments
Parameters:
services - the Services class allowing access to the type model |
| createSkolemFunctions | | public TacletApp createSkolemFunctions(Namespace p_func_ns, Services services)(Code) | | Create skolem functions (for variables declared via "\\new(c,
\\dependingOn(phi))" or via "\\new(upd, \\dependingOnMod(#modifiers))")
to replace previously created constants with
|
| equals | | public boolean equals(Object o)(Code) | | compares the given Object with this one and returns true iff both are
from type TacletApp with equal taclets, instantiations and positions.
|
| execute | | public ListOfGoal execute(Goal goal, Services services)(Code) | | applies the specified rule at the specified position
if all schema variables have been instantiated
Parameters:
goal - the Goal at which the Taclet is applied
Parameters:
services - the Services encapsulating all java information list of new created goals |
| extendVarNamespaceForSV | | public Namespace extendVarNamespaceForSV(Namespace var_ns, SchemaVariable sv)(Code) | | creates a new variable namespace by adding names of the instantiations
of the schema variables in the context of the given schema
variable and (if the TacletApp's prefix has the context flag set)
by adding names of the logic variables of the context.
Parameters:
sv - the schema variable to be considered
Parameters:
var_ns - the old variable namespace the new created variable namespace |
| findIfFormulaInstantiations | | public ListOfTacletApp findIfFormulaInstantiations(Sequent p_seq, Services p_services, Constraint p_userConstraint)(Code) | | Find all possible instantiations of the if sequent formulas
within the sequent "p_seq".
a list of tacletapps with the found if formulainstantiations |
| getRealSort | | public Sort getRealSort(SchemaVariable p_sv, Services services)(Code) | |
Parameters:
services - the Services class allowing access to the type model p_s iff p_s is not a generic sort, the concrete sortp_s is instantiated with currently otherwise
throws:
GenericSortException - iff p_s is a generic sort which isnot yet instantiated |
| hashCode | | public int hashCode()(Code) | | |
| ifFormulaInstantiations | | public ListOfIfFormulaInstantiation ifFormulaInstantiations()(Code) | | |
| ifInstsComplete | | public boolean ifInstsComplete()(Code) | | true iff the if instantiation list is not null or no ifsequent is needed |
| ifInstsCorrectSize | | protected static boolean ifInstsCorrectSize(Taclet p_taclet, ListOfIfFormulaInstantiation p_list)(Code) | | true iff the list of if instantiations has the correctsize or is null |
| instantiateWithMV | | public TacletApp instantiateWithMV(Goal p_goal)(Code) | | Make the instantiation complete using metavariables and convert plain
instantiations to metavariables and user constraint entries if possible.
Pre-condition: this.sufficientlyComplete()
|
| instantiations | | public SVInstantiations instantiations()(Code) | | returns the instantiations for the application of the Taclet at the
specified position.
the SVInstantiations needed to instantiate the Taclet |
| instsSufficientlyComplete | | public boolean instsSufficientlyComplete()(Code) | | true iff the SV instantiations can be made completeusing metavariables |
| isDependingOnModifiesSV | | public boolean isDependingOnModifiesSV(SchemaVariable sv)(Code) | |
Parameters:
sv - a schema variable true iff sv there is a variable condition of the form\newDepOnMod(modifies,sv) |
| neededUninstantiatedVars | | public SetOfSchemaVariable neededUninstantiatedVars()(Code) | | returns the variables that are currently uninstantiated and
cannot be instantiated automatically using metavariables
SetOfSchemaVariable with SchemaVariables that have notbeen instantiated yet |
| newMetavariables | | public SetOfMetavariable newMetavariables()(Code) | | |
| posInOccurrence | | abstract public PosInOccurrence posInOccurrence()(Code) | | returns the PositionInOccurrence (representing a ConstrainedFormula and
a position in the corresponding formula)
the PosInOccurrence |
| prepareUserInstantiation | | public TacletApp prepareUserInstantiation()(Code) | | checks if there are name conflicts (i.e. there are
two matched bound SchemaVariable that are matched to variables with an
equal name); if yes a new TacletApp is returned that equals this
TacletApp except that the name conflict is resolved by replacing the
instantiation of one of the conflict-causing SchemaVariables by a
bound SchemaVariable with a new name;
if the check is negative, the same TacletApp is returned.
a conflict resolved TacletApp, remainder equal to this TacletApp |
| resolveCollisionVarSV | | protected static SVInstantiations resolveCollisionVarSV(Taclet taclet, SVInstantiations insts)(Code) | | resolves collisions between bound SchemaVariables in an SVInstantiation
Parameters:
insts - the original SVInstantiations the resolved SVInstantiations |
| rule | | public Rule rule()(Code) | | returns the rule the application information is collected for
the Rule the application information is collected for |
| setAllInstantiations | | abstract protected TacletApp setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)(Code) | | creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
| setIfFormulaInstantiations | | public TacletApp setIfFormulaInstantiations(ListOfIfFormulaInstantiation p_list, Services p_services, Constraint p_userConstraint)(Code) | | Creates a new Taclet application by matching the given formulas
against the formulas of the if sequent, adding SV
instantiations, constraints and metavariables as needed. This
will fail if the if formulas have already been instantiated.
|
| setInstantiation | | abstract protected TacletApp setInstantiation(SVInstantiations svi)(Code) | | creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the old ones
Parameters:
svi - the SVInstantiations whose entries are the neededinstantiations the new Taclet application |
| setMatchConditions | | abstract protected TacletApp setMatchConditions(MatchConditions mc)(Code) | | creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
| setPosInOccurrence | | public PosTacletApp setPosInOccurrence(PosInOccurrence pos)(Code) | | returns a new PosTacletApp that is equal to this TacletApp except
that the position is set to the given PosInOccurrence
Parameters:
pos - the PosInOccurrence of the newl created PosTacletApp the new TacletApp |
| sufficientlyComplete | | abstract public boolean sufficientlyComplete()(Code) | | true iff the taclet instantiation can be made completeusing metavariables |
| taclet | | public Taclet taclet()(Code) | | returns the taclet the application information is collected for
the Taclet the application information is collected for |
| tryToInstantiate | | public TacletApp tryToInstantiate(Goal goal, Services services)(Code) | | A TacletApp with this.sufficientlyComplete() or null |
| uninstantiatedVars | | public SetOfSchemaVariable uninstantiatedVars()(Code) | | returns the variables that have not yet been instantiated and
need to be instantiated to apply the Taclet. (These are not all
SchemaVariables like the one that appear only in the addrule
sections)
SetOfSchemaVariable with SchemaVariables that have notbeen instantiated yet |
| varSVNameConflict | | public SchemaVariable varSVNameConflict()(Code) | | returns the bound SchemaVariable that causes a name conflict (i.e. there are
two matched bound SchemaVariables that are matched to variables with an
equal name, the returned SchemaVariable is (an arbitrary) one of these
SchemaVariables) or null if there is no such conflict
null iff there is no conflict and one of theconflict-causing bound SchemaVariables |
|
|