| java.lang.Object
 de.uka.ilkd.key.rule.TacletApp
de.uka.ilkd.key.rule.PosTacletApp
| PosTacletApp | | public class PosTacletApp extends TacletApp (Code) | | A position taclet application object, contains already the information to
which term/formula of the sequent the taclet is attached. The position
information has been determined by matching the find-part of the
corresponding taclet against the term described by the position
information. If such a match has not been performed or a taclet is a no find
taclet, a no position taclet object (
de.uka.ilkd.key.rule.NoPosTacletApp ) is used to keep track of the (partial)
instantiation information.
|
| Method Summary | |
| public TacletApp | addInstantiation(SchemaVariable sv, Term term, boolean interesting)
| | public TacletApp | addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)
| | public TacletApp | addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)
| | public TacletApp | addInstantiation(SVInstantiations svi)
| | public boolean | complete()
returns true iff all necessary informations are collected, so
that the Taclet can be applied. | | protected SetOfQuantifiableVariable | contextVars(SchemaVariable sv)
| | public static PosTacletApp | createPosTacletApp(FindTaclet taclet, PosInOccurrence pos)
| | public static PosTacletApp | createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, PosInOccurrence pos)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored. | | public static PosTacletApp | createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, Constraint matchConstraint, SetOfMetavariable matchNewMetavariables, PosInOccurrence pos)
| | public static PosTacletApp | createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, Constraint matchConstraint, SetOfMetavariable matchNewMetavariables, ListOfIfFormulaInstantiation ifInstantiations, PosInOccurrence pos)
| | public static PosTacletApp | createPosTacletApp(FindTaclet taclet, MatchConditions matchCond, PosInOccurrence pos)
| | public boolean | equals(Object o)
| | public int | hashCode()
| | public PosInOccurrence | posInOccurrence()
| | protected TacletApp | setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)
| | protected TacletApp | setInstantiation(SVInstantiations svi)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the old ones. | | protected TacletApp | setMatchConditions(MatchConditions mc)
| | public boolean | sufficientlyComplete()
| | public String | toString()
|
| addInstantiation | | 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 | | public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code) | | adds a new instantiation to this TacletApp
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pe - the ProgramElement the SV is instantiated with the new TacletApp |
| addInstantiation | | public TacletApp addInstantiation(SVInstantiations svi)(Code) | | creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and the ones of this TacletApp
Parameters:
svi - the SVInstantiations whose entries are the neededinstantiations the new Taclet application |
| complete | | 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. |
| createPosTacletApp | | public static PosTacletApp createPosTacletApp(FindTaclet taclet, PosInOccurrence pos)(Code) | | creates a PosTacletApp for the given taclet
and a position information and CHECKS variable conditions as well as it
resolves collisions
Parameters:
taclet - the FindTaclet
Parameters:
pos - the PosInOccurrence storing the position where to apply the Taclet new PosTacletApp or null if conditions (assertions) have been hurted |
| createPosTacletApp | | public static PosTacletApp createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, PosInOccurrence pos)(Code) | | creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored. For matching
use the method "setIfFormulaInstantiations".
Parameters:
taclet - the FindTaclet
Parameters:
instantiations - the SVInstantiations
Parameters:
pos - the PosInOccurrence storing the position where to apply the Taclet new PosTacletApp or null if conditions (assertions) have been hurted |
| hashCode | | public int hashCode()(Code) | | |
| posInOccurrence | | public PosInOccurrence posInOccurrence()(Code) | | returns the PositionInOccurrence (representing a ConstrainedFormula and
a position in the corresponding formula)
the PosInOccurrence |
| setAllInstantiations | | 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
|
| setInstantiation | | 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 | | 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
|
| sufficientlyComplete | | public boolean sufficientlyComplete()(Code) | | true iff the taclet instantiation can be made completeusing metavariables |
| Methods inherited from de.uka.ilkd.key.rule.TacletApp | public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)(Code)(Java Doc)
public TacletApp addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code)(Java Doc)
public TacletApp addInstantiation(SchemaVariable sv, Name name)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SVInstantiations svi)(Code)(Java Doc)
public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code)(Java Doc)
protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)(Code)(Java Doc)
protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)(Code)(Java Doc)
protected SetOfSchemaVariable calculateNeededNonInstantiatedSV()(Code)(Java Doc)
protected SetOfSchemaVariable calculateNonInstantiatedSV()(Code)(Java Doc)
protected boolean canUseMVAPosteriori(SchemaVariable p_var, Term p_term)(Code)(Java Doc)
public boolean canUseMVAPriori(SchemaVariable p_var)(Code)(Java Doc)
public static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)(Code)(Java Doc)
protected static SetOfQuantifiableVariable collectBoundVarsAbove(PosInOccurrence pos)(Code)(Java Doc)
abstract public boolean complete()(Code)(Java Doc)
public Constraint constraint()(Code)(Java Doc)
abstract protected SetOfQuantifiableVariable contextVars(SchemaVariable sv)(Code)(Java Doc)
public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, boolean interesting, Services services)(Code)(Java Doc)
public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, Sort sort, boolean interesting)(Code)(Java Doc)
public TacletApp createSkolemFunctions(Namespace p_func_ns, Services services)(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
public ListOfGoal execute(Goal goal, Services services)(Code)(Java Doc)
public Namespace extendVarNamespaceForSV(Namespace var_ns, SchemaVariable sv)(Code)(Java Doc)
public ListOfTacletApp findIfFormulaInstantiations(Sequent p_seq, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
public Sort getRealSort(SchemaVariable p_sv, Services services)(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public ListOfIfFormulaInstantiation ifFormulaInstantiations()(Code)(Java Doc)
public boolean ifInstsComplete()(Code)(Java Doc)
protected static boolean ifInstsCorrectSize(Taclet p_taclet, ListOfIfFormulaInstantiation p_list)(Code)(Java Doc)
public TacletApp instantiateWithMV(Goal p_goal)(Code)(Java Doc)
public SVInstantiations instantiations()(Code)(Java Doc)
public boolean instsSufficientlyComplete()(Code)(Java Doc)
public boolean isDependingOnModifiesSV(SchemaVariable sv)(Code)(Java Doc)
public MatchConditions matchConditions()(Code)(Java Doc)
public SetOfSchemaVariable neededUninstantiatedVars()(Code)(Java Doc)
public SetOfMetavariable newMetavariables()(Code)(Java Doc)
abstract public PosInOccurrence posInOccurrence()(Code)(Java Doc)
public TacletApp prepareUserInstantiation()(Code)(Java Doc)
protected static SVInstantiations replaceInstantiation(Taclet taclet, SVInstantiations insts, SchemaVariable varSV)(Code)(Java Doc)
protected static SVInstantiations resolveCollisionVarSV(Taclet taclet, SVInstantiations insts)(Code)(Java Doc)
public Rule rule()(Code)(Java Doc)
abstract protected TacletApp setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)(Code)(Java Doc)
public TacletApp setIfFormulaInstantiations(ListOfIfFormulaInstantiation p_list, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
abstract protected TacletApp setInstantiation(SVInstantiations svi)(Code)(Java Doc)
abstract protected TacletApp setMatchConditions(MatchConditions mc)(Code)(Java Doc)
public PosTacletApp setPosInOccurrence(PosInOccurrence pos)(Code)(Java Doc)
abstract public boolean sufficientlyComplete()(Code)(Java Doc)
public Taclet taclet()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
public TacletApp tryToInstantiate(Goal goal, Services services)(Code)(Java Doc)
public SetOfSchemaVariable uninstantiatedVars()(Code)(Java Doc)
public SchemaVariable varSVNameConflict()(Code)(Java Doc)
|
|
|