public abstract class TacletIndex
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private static class |
TacletIndex.PrefixOccurrences
Inner class to track the occurrences of prefix elements in java blocks
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
antecList
contains antecedent Taclets
|
private static java.lang.Object |
DEFAULT_PROGSV_KEY |
private static java.lang.Object |
DEFAULT_SV_KEY |
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 |
---|---|
(package private) |
TacletIndex()
constructs empty rule index
|
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) |
(package private) |
TacletIndex(java.lang.Iterable<Taclet> tacletSet)
creates a new TacletIndex with the given Taclets as initial contents.
|
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
|
private void |
addToSet(ImmutableList<NoPosTacletApp> list,
java.util.Set<NoPosTacletApp> result) |
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.
|
private ImmutableList<NoPosTacletApp> |
getFindTaclet(ImmutableList<NoPosTacletApp> taclets,
RuleFilter filter,
PosInOccurrence pos,
Services services)
returns a list of Taclets and instantiations from the given list of
taclets with
respect to term and the filter object.
|
private static java.lang.Object |
getIndexObj(FindTaclet tac) |
private ImmutableList<NoPosTacletApp> |
getJavaTacletList(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map,
ProgramElement pe,
TacletIndex.PrefixOccurrences prefixOccurrences)
returns a selection from the given map with NoPosTacletApps relevant for
the given program element.
|
private ImmutableList<NoPosTacletApp> |
getList(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map,
Term term,
boolean ignoreUpdates)
creates and returns a selection from the given map of NoPosTacletApps
that are compatible with the given term.
|
private ImmutableList<NoPosTacletApp> |
getListHelp(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map,
Term term,
boolean ignoreUpdates,
TacletIndex.PrefixOccurrences prefixOccurrences) |
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.
|
private ImmutableList<NoPosTacletApp> |
getTopLevelTaclets(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> findTaclets,
RuleFilter filter,
PosInOccurrence pos,
Services services) |
private void |
insertToMap(NoPosTacletApp tacletApp,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map) |
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
|
private ImmutableList<NoPosTacletApp> |
merge(ImmutableList<NoPosTacletApp> first,
ImmutableList<NoPosTacletApp> second)
merges the two list in an execution time optimal manner
|
void |
remove(NoPosTacletApp tacletApp)
removes a Taclet with the given instantiation information from this index.
|
private void |
removeFromMap(NoPosTacletApp tacletApp,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map) |
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() |
private static final java.lang.Object DEFAULT_SV_KEY
private static final java.lang.Object DEFAULT_PROGSV_KEY
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
TacletIndex()
TacletIndex(java.lang.Iterable<Taclet> tacletSet)
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)
private static java.lang.Object getIndexObj(FindTaclet tac)
private void insertToMap(NoPosTacletApp tacletApp, java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map)
private void removeFromMap(NoPosTacletApp tacletApp, java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map)
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
private void addToSet(ImmutableList<NoPosTacletApp> list, java.util.Set<NoPosTacletApp> result)
public java.util.Set<NoPosTacletApp> allNoPosTacletApps()
private ImmutableList<NoPosTacletApp> getFindTaclet(ImmutableList<NoPosTacletApp> taclets, RuleFilter filter, PosInOccurrence pos, Services services)
services
- the Services object encapsulating information
about the java datastructures like (static)types etc.protected abstract ImmutableList<NoPosTacletApp> matchTaclets(ImmutableList<NoPosTacletApp> tacletApps, RuleFilter p_filter, PosInOccurrence pos, Services services)
private ImmutableList<NoPosTacletApp> getJavaTacletList(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map, ProgramElement pe, TacletIndex.PrefixOccurrences prefixOccurrences)
map
- the map to select the NoPosTacletApps frompe
- the program element that is used to retrieve the tacletsprefixOcc
- the PrefixOccurrence object used to keep track of the
occuring prefix elementsprivate ImmutableList<NoPosTacletApp> getListHelp(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map, Term term, boolean ignoreUpdates, TacletIndex.PrefixOccurrences prefixOccurrences)
private final ImmutableList<NoPosTacletApp> merge(ImmutableList<NoPosTacletApp> first, ImmutableList<NoPosTacletApp> second)
first
- the first listsecond
- the second listprivate ImmutableList<NoPosTacletApp> getList(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> map, Term term, boolean ignoreUpdates)
map
- the map from where to select the tacletsterm
- the term that is used to find the selectionpublic 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.private ImmutableList<NoPosTacletApp> getTopLevelTaclets(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> findTaclets, RuleFilter filter, PosInOccurrence pos, Services services)
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