public abstract class TacletApp extends java.lang.Object implements RuleApp
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.Modifier and Type | Field and Description |
---|---|
protected ImmutableList<IfFormulaInstantiation> |
ifInstantiations
chosen instantiations for the if sequent formulas
|
protected SVInstantiations |
instantiations
contains the instantiations of the schema variables of the Taclet
|
private MatchConditions |
matchConditions
caches a created match condition (instantiations, RenameTable.EMPTY)
|
private ImmutableSet<SchemaVariable> |
missingVars
set of schema variables that appear in the Taclet and need to be
instantiated but are not instantiated yet.
|
private Taclet |
taclet
the taclet for which the application information is collected
|
protected boolean |
updateContextFixed
the update context given by the current instantiations must not be
changed
|
Constructor and Description |
---|
TacletApp(Taclet taclet)
constructs a TacletApp for the given taclet, with an empty instantiation
map
|
TacletApp(Taclet taclet,
SVInstantiations instantiations)
constructs a TacletApp for the given taclet.
|
TacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
addCheckedInstantiation(SchemaVariable sv,
ProgramElement pe,
Services services,
boolean interesting)
checks if the instantiation of
sv with pe is
possible. |
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.
|
TacletApp |
addInstantiation(SchemaVariable sv,
Name name,
Services services) |
abstract TacletApp |
addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
abstract TacletApp |
addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp.
|
abstract TacletApp |
addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations
|
boolean |
admissible(boolean interactive,
ImmutableList<RuleSet> ruleSets) |
protected static ImmutableSet<QuantifiableVariable> |
boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected static ImmutableSet<QuantifiableVariable> |
boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations,
PosInOccurrence pos)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected ImmutableSet<SchemaVariable> |
calculateNonInstantiatedSV()
calculate needed SchemaVariables that have not been instantiated yet.
|
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 ImmutableSet<QuantifiableVariable> |
collectBoundVarsAbove(PosInOccurrence pos)
collects all bound vars that are bound above the subterm described by the
given term position information
|
private java.util.Collection<java.lang.String> |
collectClashNames(SchemaVariable sv,
TermServices services)
Collect names which would result in a clash for a new logical variable.
|
private static ImmutableSet<QuantifiableVariable> |
collectPrefixInstantiations(TacletPrefix pre,
SVInstantiations instantiations)
collects all those logic variable that are instances of the variableSV of
the given prefix
|
private static boolean |
contains(ImmutableArray<QuantifiableVariable> boundVars,
LogicVariable x,
SVInstantiations insts)
returns true iff the instantiation of a bound SchemaVariable contains the
given Logicvariable
|
protected abstract ImmutableSet<QuantifiableVariable> |
contextVars(SchemaVariable sv) |
private ImmutableList<SequentFormula> |
createSemisequentList(Semisequent p_ss) |
TacletApp |
createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
boolean interesting,
Services services)
Create a new constant named "instantiation" and instantiate "sv" with.
|
TacletApp |
createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
Sort sort,
boolean interesting,
Services services) |
boolean |
equals(java.lang.Object o)
compares the given Object with this one and returns true iff both are
from type TacletApp with equal taclets, instantiations and positions.
|
ImmutableList<Goal> |
execute(Goal goal,
Services services)
applies the specified rule at the specified position if all schema
variables have been instantiated
|
Namespace<Function> |
extendedFunctionNameSpace(Namespace<Function> func_ns)
create a new function namespace by adding all newly instantiated skolem
symbols to a new namespace.
|
Namespace<QuantifiableVariable> |
extendVarNamespaceForSV(Namespace<QuantifiableVariable> 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.
|
ImmutableList<TacletApp> |
findIfFormulaInstantiations(Sequent p_seq,
Services p_services)
Find all possible instantiations of the if sequent formulas within the
sequent "p_seq".
|
private ImmutableList<TacletApp> |
findIfFormulaInstantiationsHelp(ImmutableList<SequentFormula> p_ifSeqTail,
ImmutableList<SequentFormula> p_ifSeqTail2nd,
ImmutableList<IfFormulaInstantiation> p_toMatch,
ImmutableList<IfFormulaInstantiation> p_toMatch2nd,
ImmutableList<IfFormulaInstantiation> p_alreadyMatched,
MatchConditions p_matchCond,
Services p_services)
Recursive function for matching the remaining tail of an if sequent
|
private static TacletApp |
forceGenericSortInstantiation(TacletApp app,
SchemaVariable sv,
Services services)
If the sort of the given schema variable is generic, add a condition to
the instantiations of the given taclet app that requires the sort to be
instantiated
|
ProgramElement |
getProgramElement(java.lang.String instantiation,
SchemaVariable sv,
Services services) |
Sort |
getRealSort(SchemaVariable p_sv,
TermServices services) |
private static Term |
getTermBelowQuantifier(SchemaVariable varSV,
Term term)
delivers the term below the (unique) quantifier of a bound SchemaVariable
in the given term.
|
private static Term |
getTermBelowQuantifier(Taclet taclet,
SchemaVariable varSV)
delivers the term below the (unique) quantifier of a bound SchemaVariable
varSV in the find and if-parts of the Taclet
|
int |
hashCode() |
ImmutableList<IfFormulaInstantiation> |
ifFormulaInstantiations() |
boolean |
ifInstsComplete() |
protected static boolean |
ifInstsCorrectSize(Taclet p_taclet,
ImmutableList<IfFormulaInstantiation> p_list) |
SVInstantiations |
instantiations()
returns the instantiations for the application of the Taclet at the
specified position.
|
boolean |
isExecutable(TermServices services) |
boolean |
isInstantiationRequired(SchemaVariable sv)
returns true if the given
SchemaVariable must be explicitly instantiated
it does not check whether sv is already instantiated or not |
MatchConditions |
matchConditions() |
TacletApp |
prepareUserInstantiation(Services services)
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.
|
void |
registerSkolemConstants(NamespaceSet nss) |
private static SVInstantiations |
replaceInstantiation(SVInstantiations insts,
Term t,
SchemaVariable u,
Term y,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable u to the Term (that is a LogicVariable)
y.
|
protected static SVInstantiations |
replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
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,
Services services)
resolves collisions between bound SchemaVariables in an SVInstantiation
|
Rule |
rule()
returns the rule the application information is collected for
|
protected abstract TacletApp |
setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the instantiations,
constraints, new metavariables and if formula instantiations given and
forget the old ones
|
TacletApp |
setIfFormulaInstantiations(ImmutableList<IfFormulaInstantiation> p_list,
Services p_services)
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.
|
protected abstract TacletApp |
setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations and forget the old ones
|
abstract TacletApp |
setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the instantiations,
constraints and new metavariables given by the mc object and forget the
old ones
|
PosTacletApp |
setPosInOccurrence(PosInOccurrence pos,
Services services)
returns a new PosTacletApp that is equal to this TacletApp except that
the position is set to the given PosInOccurrence.
|
Taclet |
taclet()
returns the taclet the application information is collected for
|
java.lang.String |
toString() |
TacletApp |
tryToInstantiate(Services services) |
TacletApp |
tryToInstantiateAsMuchAsPossible(Services services) |
ImmutableSet<SchemaVariable> |
uninstantiatedVars()
returns the variables that have not yet been instantiated and need to be
instantiated to apply the Taclet.
|
SchemaVariable |
varSVNameConflict()
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
|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
complete, posInOccurrence
private final Taclet taclet
protected final SVInstantiations instantiations
private final MatchConditions matchConditions
protected final ImmutableList<IfFormulaInstantiation> ifInstantiations
private volatile ImmutableSet<SchemaVariable> missingVars
protected boolean updateContextFixed
TacletApp(Taclet taclet)
TacletApp(Taclet taclet, SVInstantiations instantiations, ImmutableList<IfFormulaInstantiation> ifInstantiations)
TacletApp(Taclet taclet, SVInstantiations instantiations)
protected static ImmutableSet<QuantifiableVariable> boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)
prefix
- the TacletPrefix of the schemavariableinstantiations
- the SVInstantiations so that the find(if)-expression matchesprotected static ImmutableSet<QuantifiableVariable> boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)
prefix
- the TacletPrefix of the schemavariableinstantiations
- the SVInstantiations so that the find(if)-expression matchespos
- the posInOccurrence describing the position of the
schemavariableprivate static ImmutableSet<QuantifiableVariable> collectPrefixInstantiations(TacletPrefix pre, SVInstantiations instantiations)
pre
- the TacletPrefix of a SchemaVariable that is boundinstantiations
- the SVInstantiations to look atpublic Taclet taclet()
public Rule rule()
public SVInstantiations instantiations()
public MatchConditions matchConditions()
public ImmutableList<IfFormulaInstantiation> ifFormulaInstantiations()
protected static SVInstantiations resolveCollisionVarSV(Taclet taclet, SVInstantiations insts, Services services)
insts
- the original SVInstantiationsprivate static Term getTermBelowQuantifier(SchemaVariable varSV, Term term)
varSV
- the searched Bound Schemavariableterm
- the term to be searched inprivate static Term getTermBelowQuantifier(Taclet taclet, SchemaVariable varSV)
varSV
- the searched bound SchemaVariableprivate static boolean contains(ImmutableArray<QuantifiableVariable> boundVars, LogicVariable x, SVInstantiations insts)
boundVars
- ImmutableArrayx
- the LogicVariable that is looked forinsts
- the SVInstantiations where to get the necessary instantiations
of the bound SchemaVariablesprotected static SVInstantiations replaceInstantiation(Taclet taclet, SVInstantiations insts, SchemaVariable varSV, Services services)
private static SVInstantiations replaceInstantiation(SVInstantiations insts, Term t, SchemaVariable u, Term y, Services services)
public ImmutableList<Goal> execute(Goal goal, Services services)
public boolean isExecutable(TermServices services)
protected ImmutableSet<SchemaVariable> calculateNonInstantiatedSV()
public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)
sv
- the SchemaVariable to be instantiatedterm
- the Term the SchemaVariable is instantiated withpublic ImmutableSet<SchemaVariable> uninstantiatedVars()
public boolean isInstantiationRequired(SchemaVariable sv)
SchemaVariable
must be explicitly instantiated
it does not check whether sv is already instantiated or notsv
- the SchemaVariablepublic final TacletApp tryToInstantiateAsMuchAsPossible(Services services)
public final TacletApp tryToInstantiate(Services services)
private java.util.Collection<java.lang.String> collectClashNames(SchemaVariable sv, TermServices services)
sv
- the schema variable to instantiate with a fresh variable, not
null
services
- the services object, not null
private static TacletApp forceGenericSortInstantiation(TacletApp app, SchemaVariable sv, Services services)
null
if the sort of
sv
is generic and cannot be instantiated (at least
at the time)public Sort getRealSort(SchemaVariable p_sv, TermServices services)
services
- the Services class allowing access to the type modelGenericSortException
- iff p_s is a generic sort which is not yet instantiatedpublic TacletApp createSkolemConstant(java.lang.String instantiation, SchemaVariable sv, boolean interesting, Services services)
services
- the Services class allowing access to the type modelpublic TacletApp createSkolemConstant(java.lang.String instantiation, SchemaVariable sv, Sort sort, boolean interesting, Services services)
public void registerSkolemConstants(NamespaceSet nss)
public abstract TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting, Services services)
sv
- the SchemaVariable to be instantiatedterm
- the Term the SchemaVariable is instantiated withpublic abstract TacletApp addInstantiation(SchemaVariable sv, java.lang.Object[] list, boolean interesting, Services services)
public abstract TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting, Services services)
(sv, pe)
will
result in a valid taclet instantiation, you have to use
addCheckedInstantiation(SchemaVariable, ProgramElement, Services, boolean)
insteadsv
- the SchemaVariable to be instantiatedpe
- the ProgramElement the SV is instantiated withinteresting
- a boolean marking if the instantiation of this sv needs to be
saved for later proof loading (interesting==true
)
or if it can be derived deterministically (e.g. by matching) (
interesting==false
)(sv, pe)
public TacletApp addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)
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.sv
- the SchemaVariable to be instantiatedpe
- the ProgramElement the SV is instantiated withservices
- the Servicesinteresting
- a boolean marking if the instantiation of this sv needs to be
saved for later proof loading (interesting==true
)
or if it can be derived deterministically (e.g. by matching) (
interesting==false
)(sv, pe)
, if the
instantiation results in a valid taclet application otherwise an
exception is thrownIllegalInstantiationException
- exception thrown if sv
cannot be instantiated
with pe
no matter if in general or due to side
conditions posed by this particular applicationpublic TacletApp addInstantiation(SchemaVariable sv, Name name, Services services)
public abstract TacletApp addInstantiation(SVInstantiations svi, Services services)
svi
- the SVInstantiations whose entries are the needed
instantiationsprotected abstract TacletApp setInstantiation(SVInstantiations svi, Services services)
svi
- the SVInstantiations whose entries are the needed
instantiationspublic abstract TacletApp setMatchConditions(MatchConditions mc, Services services)
protected abstract TacletApp setAllInstantiations(MatchConditions mc, ImmutableList<IfFormulaInstantiation> ifInstantiations, Services services)
public TacletApp setIfFormulaInstantiations(ImmutableList<IfFormulaInstantiation> p_list, Services p_services)
public ImmutableList<TacletApp> findIfFormulaInstantiations(Sequent p_seq, Services p_services)
private ImmutableList<TacletApp> findIfFormulaInstantiationsHelp(ImmutableList<SequentFormula> p_ifSeqTail, ImmutableList<SequentFormula> p_ifSeqTail2nd, ImmutableList<IfFormulaInstantiation> p_toMatch, ImmutableList<IfFormulaInstantiation> p_toMatch2nd, ImmutableList<IfFormulaInstantiation> p_alreadyMatched, MatchConditions p_matchCond, Services p_services)
p_ifSeqTail
- tail of the current semisequent as listp_ifSeqTail2nd
- the following semisequent (i.e. antecedent) or nullp_toMatch
- list of the formulas to match the current if semisequent
formulas withp_toMatch2nd
- list of the formulas of the antecedentp_matchCond
- match conditions until now, i.e. after matching the first
formulas of the if sequentprivate ImmutableList<SequentFormula> createSemisequentList(Semisequent p_ss)
public PosTacletApp setPosInOccurrence(PosInOccurrence pos, Services services)
CAUTION: If you call this method, consider to call
NoPosTacletApp.matchFind(PosInOccurrence, Services)
first (if
applicable) as otherwise the TacletApp may become invalid.
(This happened sometimes during interactive proofs).
pos
- the PosInOccurrence of the newl created PosTacletApppublic boolean ifInstsComplete()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
public TacletApp prepareUserInstantiation(Services services)
protected abstract ImmutableSet<QuantifiableVariable> contextVars(SchemaVariable sv)
public Namespace<QuantifiableVariable> extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns, SchemaVariable sv)
sv
- the schema variable to be consideredvar_ns
- the old variable namespacepublic Namespace<Function> extendedFunctionNameSpace(Namespace<Function> func_ns)
func_ns
- the original function namespace, not null
public SchemaVariable varSVNameConflict()
protected static boolean ifInstsCorrectSize(Taclet p_taclet, ImmutableList<IfFormulaInstantiation> p_list)
public boolean admissible(boolean interactive, ImmutableList<RuleSet> ruleSets)
public ProgramElement getProgramElement(java.lang.String instantiation, SchemaVariable sv, Services services)
public static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)
taclet
- the Taclet that is tried to be instantiated. A match for the
find (or/and if) has been found.instantiations
- the SVInstantiations so that the find(if) expression matchespos
- the PosInOccurrence where the Taclet is appliedprotected static ImmutableSet<QuantifiableVariable> collectBoundVarsAbove(PosInOccurrence pos)
pos
- the PosInOccurrence describing a subterm in Term