Cache that is used for accelerating
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:
- Toplevel in the antecedent
- Toplevel in the succedent
- Non-toplevel, but not below updates or programs and not below "bad"
operators that we do not know (defined by
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.
- Below updates, but not below programs. We do not cache at all in such
places.
- Below programs. Again, we also have to distinguish different prefixes of
a position.
- Below other "bad" operators. We do not cache at all in such places.
We identify these different areas with an automaton that walks
from the root of a formula to a subformula or subterm, roughly following the
state design pattern. The transition function is realised by the method
ITermTacletAppIndexCache.descend
.