public class TermTacletAppIndexCacheSet
extends java.lang.Object
TermTacletAppIndex
.
Basically, this is a mapping from terms to objects of
TermTacletAppIndex
, following the idea that the same taclets
will be applicable to an occurrence of the same term in different places.
There are different categories of locations/areas in a term that have to be
separated, because different taclets could be applicable. These are:
TermTacletAppIndexCacheSet.isAcceptedOperator
). In this case
we also have to distinguish different prefixes of a position, i.e., different
sets of variables that are bound above a position.ITermTacletAppIndexCache.descend
.Modifier and Type | Class and Description |
---|---|
private class |
TermTacletAppIndexCacheSet.BelowProgCache |
private class |
TermTacletAppIndexCacheSet.BelowUpdateCache |
private class |
TermTacletAppIndexCacheSet.TopLevelCache |
Modifier and Type | Field and Description |
---|---|
private ITermTacletAppIndexCache |
antecCache
the toplevel caches for the antecedent and the succedent.
|
private ITermTacletAppIndexCache |
belowProgCacheEmptyPrefix
cache for locations that are below programs, but not in the scope of
binders
|
private LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache> |
belowProgCaches
caches for locations that are both below programs and in the scope of
binders. this is a mapping from
IList
to BelowProgCache |
private ITermTacletAppIndexCache |
belowUpdateCacheEmptyPrefix
cache for locations that are below updates, but not below programs or in
the scope of binders
|
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> |
cache |
private static int |
MAX_CACHE_ENTRIES
max. instances of
ITermTacletAppIndexCache that are kept
in this set (e.g., for different prefixes of quantified variables) |
private static ITermTacletAppIndexCache |
noCache
dummy cache that is not caching at all, and from which no other cache is
reachable
|
private ITermTacletAppIndexCache |
succCache |
private ITermTacletAppIndexCache |
topLevelCacheEmptyPrefix
cache for locations that are not below updates, programs or in the scope
of binders
|
private LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache> |
topLevelCaches
caches for locations that are not below updates or programs, but in the
scope of binders. this is a mapping from
IList to TopLevelCache |
Constructor and Description |
---|
TermTacletAppIndexCacheSet(java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache) |
Modifier and Type | Method and Description |
---|---|
ITermTacletAppIndexCache |
getAntecCache() |
private ITermTacletAppIndexCache |
getBelowProgCache(ImmutableList<QuantifiableVariable> prefix) |
private ITermTacletAppIndexCache |
getBelowUpdateCache(ImmutableList<QuantifiableVariable> prefix) |
ITermTacletAppIndexCache |
getNoCache() |
ITermTacletAppIndexCache |
getSuccCache() |
private ITermTacletAppIndexCache |
getTopLevelCache(ImmutableList<QuantifiableVariable> prefix) |
private boolean |
isAcceptedOperator(Operator op) |
boolean |
isRelevantTaclet(Taclet t) |
private boolean |
isUpdateTargetPos(Term t,
int subtermIndex) |
private static final int MAX_CACHE_ENTRIES
ITermTacletAppIndexCache
that are kept
in this set (e.g., for different prefixes of quantified variables)private static final ITermTacletAppIndexCache noCache
private final ITermTacletAppIndexCache antecCache
private final ITermTacletAppIndexCache succCache
private final ITermTacletAppIndexCache topLevelCacheEmptyPrefix
private final LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache> topLevelCaches
IList
to TopLevelCache
private final ITermTacletAppIndexCache belowUpdateCacheEmptyPrefix
private final ITermTacletAppIndexCache belowProgCacheEmptyPrefix
private final LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache> belowProgCaches
IList
to BelowProgCache
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache
public TermTacletAppIndexCacheSet(java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)
public ITermTacletAppIndexCache getAntecCache()
public ITermTacletAppIndexCache getSuccCache()
public ITermTacletAppIndexCache getNoCache()
public boolean isRelevantTaclet(Taclet t)
true
iff t
is a taclet that might
possibly be cached by any of the caches of this setprivate ITermTacletAppIndexCache getTopLevelCache(ImmutableList<QuantifiableVariable> prefix)
prefix
(which
might be empty)private ITermTacletAppIndexCache getBelowProgCache(ImmutableList<QuantifiableVariable> prefix)
prefix
(which might be empty)private ITermTacletAppIndexCache getBelowUpdateCache(ImmutableList<QuantifiableVariable> prefix)
prefix
(which might be empty)private boolean isUpdateTargetPos(Term t, int subtermIndex)
true
if the head operator of t
is
an update and subtermIndex
is the number of the
target subterm of the updateprivate boolean isAcceptedOperator(Operator op)
true
if op
is an operator below
which we are caching