public abstract class TacletIndex
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
antecList
contains antecedent Taclets
|
protected ImmutableList<NoPosTacletApp> |
noFindList
contains NoFind-Taclets
|
protected java.util.HashSet<NoPosTacletApp> |
partialInstantiatedRuleApps
keeps track of no pos taclet apps with partial
instantiations
|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
rwList
contains rewrite Taclets
|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
succList
contains succedent Taclets
|
Modifier | Constructor and Description |
---|---|
protected |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
Modifier and Type | Method and Description |
---|---|
void |
add(NoPosTacletApp tacletApp)
adds a new Taclet with instantiation information to this index.
|
void |
add(Taclet taclet)
adds a new Taclet with instantiation information to this index.
|
void |
addTaclets(java.lang.Iterable<NoPosTacletApp> tacletAppList)
adds a set of NoPosTacletApp to this index
|
java.util.Set<NoPosTacletApp> |
allNoPosTacletApps() |
java.lang.Object |
clone()
clones the index
|
abstract TacletIndex |
copy()
copies the index
|
ImmutableList<NoPosTacletApp> |
getAntecedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the antecedent.
|
ImmutableList<NoPosTacletApp> |
getNoFindTaclet(RuleFilter filter,
Services services)
get all Taclets having no find expression.
|
ImmutableList<NoPosTacletApp> |
getPartialInstantiatedApps()
returns a list with all partial instantiated no pos taclet apps
|
ImmutableList<NoPosTacletApp> |
getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Rewrite-Taclets.
|
ImmutableList<NoPosTacletApp> |
getSuccedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the succedent.
|
NoPosTacletApp |
lookup(Name name)
returns a NoPosTacletApp whose Taclet has a name that equals the given
name.
|
NoPosTacletApp |
lookup(java.lang.String name)
returns a NoPosTacletApp whose Taclet has a name that equals the given
name.
|
protected abstract ImmutableList<NoPosTacletApp> |
matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
RuleFilter p_filter,
PosInOccurrence pos,
Services services)
Filter the given list of taclet apps, and match their find
parts at the given position of the sequent
|
void |
remove(NoPosTacletApp tacletApp)
removes a Taclet with the given instantiation information from this index.
|
void |
removeTaclets(java.lang.Iterable<NoPosTacletApp> tacletAppList)
removes the given NoPosTacletApps from this index
|
static ImmutableSet<NoPosTacletApp> |
toNoPosTacletApp(java.lang.Iterable<Taclet> rule) |
java.lang.String |
toString() |
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList
protected ImmutableList<NoPosTacletApp> noFindList
protected java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps
protected TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList, java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList, java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList, ImmutableList<NoPosTacletApp> noFindList, java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps)
public void addTaclets(java.lang.Iterable<NoPosTacletApp> tacletAppList)
tacletAppList
- the NoPosTacletApps to be addedpublic static ImmutableSet<NoPosTacletApp> toNoPosTacletApp(java.lang.Iterable<Taclet> rule)
public void add(Taclet taclet)
taclet
- the Taclet and its instantiation info to be addedpublic void add(NoPosTacletApp tacletApp)
tacletApp
- the Taclet and its instantiation info to be addedpublic void removeTaclets(java.lang.Iterable<NoPosTacletApp> tacletAppList)
tacletAppList
- the NoPosTacletApps to be removedpublic void remove(NoPosTacletApp tacletApp)
tacletApp
- the Taclet and its instantiation info to be removedpublic abstract TacletIndex copy()
public java.lang.Object clone()
clone
in class java.lang.Object
public java.util.Set<NoPosTacletApp> allNoPosTacletApps()
protected abstract ImmutableList<NoPosTacletApp> matchTaclets(ImmutableList<NoPosTacletApp> tacletApps, RuleFilter p_filter, PosInOccurrence pos, Services services)
public ImmutableList<NoPosTacletApp> getAntecedentTaclet(PosInOccurrence pos, RuleFilter filter, Services services)
pos
- the PosOfOccurrence describing the formula for which to look
for top level tacletsfilter
- Only return taclets the filter selectsservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getSuccedentTaclet(PosInOccurrence pos, RuleFilter filter, Services services)
pos
- the PosOfOccurrence describing the formula for which to look
for top level tacletsfilter
- Only return taclets the filter selectsservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getRewriteTaclet(PosInOccurrence pos, RuleFilter filter, Services services)
filter
- Only return taclets the filter selectsservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getNoFindTaclet(RuleFilter filter, Services services)
filter
- Only return taclets the filter selectsservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public NoPosTacletApp lookup(Name name)
name
- the name to lookuppublic NoPosTacletApp lookup(java.lang.String name)
name
- the name to lookuppublic ImmutableList<NoPosTacletApp> getPartialInstantiatedApps()
public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.