public abstract class TacletIndex extends 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 HashMap<Object,ImmutableList<NoPosTacletApp>> |
antecList
contains antecedent Taclets
|
private static Object |
DEFAULT_PROGSV_KEY |
private static Object |
DEFAULT_SV_KEY |
protected ImmutableList<NoPosTacletApp> |
noFindList
contains NoFind-Taclets
|
protected HashSet<NoPosTacletApp> |
partialInstantiatedRuleApps
keeps track of no pos taclet apps with partial
instantiations
|
private TacletIndex.PrefixOccurrences |
prefixOccurrences |
protected HashMap<Object,ImmutableList<NoPosTacletApp>> |
rwList
contains rewrite Taclets
|
protected HashMap<Object,ImmutableList<NoPosTacletApp>> |
succList
contains succedent Taclets
|
Modifier | Constructor and Description |
---|---|
(package private) |
TacletIndex()
constructs empty rule index
|
protected |
TacletIndex(HashMap<Object,ImmutableList<NoPosTacletApp>> rwList,
HashMap<Object,ImmutableList<NoPosTacletApp>> antecList,
HashMap<Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
(package private) |
TacletIndex(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(Iterable<NoPosTacletApp> tacletAppList)
adds a set of NoPosTacletApp to this index
|
private void |
addToSet(ImmutableList<NoPosTacletApp> list,
Set<NoPosTacletApp> result) |
Set<NoPosTacletApp> |
allNoPosTacletApps() |
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 Object |
getIndexObj(FindTaclet tac) |
private ImmutableList<NoPosTacletApp> |
getJavaTacletList(HashMap<Object,ImmutableList<NoPosTacletApp>> map,
ProgramElement pe,
TacletIndex.PrefixOccurrences prefixOcc)
returns a selection from the given map with NoPosTacletApps relevant for
the given program element.
|
private ImmutableList<NoPosTacletApp> |
getList(HashMap<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(HashMap<Object,ImmutableList<NoPosTacletApp>> map,
Term term,
boolean ignoreUpdates) |
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(HashMap<Object,ImmutableList<NoPosTacletApp>> findTaclets,
RuleFilter filter,
PosInOccurrence pos,
Services services) |
private void |
insertToMap(NoPosTacletApp tacletApp,
HashMap<Object,ImmutableList<NoPosTacletApp>> map) |
NoPosTacletApp |
lookup(Name name)
returns a NoPosTacletApp whose Taclet has a name that equals the given
name.
|
NoPosTacletApp |
lookup(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.
|
private void |
removeFromMap(NoPosTacletApp tacletApp,
HashMap<Object,ImmutableList<NoPosTacletApp>> map) |
void |
removeTaclets(Iterable<NoPosTacletApp> tacletAppList)
removes the given NoPosTacletApps from this index
|
static ImmutableSet<NoPosTacletApp> |
toNoPosTacletApp(Iterable<Taclet> rule) |
String |
toString() |
private static final Object DEFAULT_SV_KEY
private static final Object DEFAULT_PROGSV_KEY
protected HashMap<Object,ImmutableList<NoPosTacletApp>> rwList
protected HashMap<Object,ImmutableList<NoPosTacletApp>> antecList
protected HashMap<Object,ImmutableList<NoPosTacletApp>> succList
protected ImmutableList<NoPosTacletApp> noFindList
protected HashSet<NoPosTacletApp> partialInstantiatedRuleApps
private final TacletIndex.PrefixOccurrences prefixOccurrences
TacletIndex()
TacletIndex(Iterable<Taclet> tacletSet)
protected TacletIndex(HashMap<Object,ImmutableList<NoPosTacletApp>> rwList, HashMap<Object,ImmutableList<NoPosTacletApp>> antecList, HashMap<Object,ImmutableList<NoPosTacletApp>> succList, ImmutableList<NoPosTacletApp> noFindList, HashSet<NoPosTacletApp> partialInstantiatedRuleApps)
private static Object getIndexObj(FindTaclet tac)
private void insertToMap(NoPosTacletApp tacletApp, HashMap<Object,ImmutableList<NoPosTacletApp>> map)
private void removeFromMap(NoPosTacletApp tacletApp, HashMap<Object,ImmutableList<NoPosTacletApp>> map)
public void addTaclets(Iterable<NoPosTacletApp> tacletAppList)
tacletAppList
- the NoPosTacletApps to be addedpublic static ImmutableSet<NoPosTacletApp> toNoPosTacletApp(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(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()
private void addToSet(ImmutableList<NoPosTacletApp> list, Set<NoPosTacletApp> result)
public 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(HashMap<Object,ImmutableList<NoPosTacletApp>> map, ProgramElement pe, TacletIndex.PrefixOccurrences prefixOcc)
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(HashMap<Object,ImmutableList<NoPosTacletApp>> map, Term term, boolean ignoreUpdates)
private ImmutableList<NoPosTacletApp> getList(HashMap<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(HashMap<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(String name)
name
- the name to lookuppublic ImmutableList<NoPosTacletApp> getPartialInstantiatedApps()