de.uka.ilkd.key.proof

Class TermTacletAppIndexCacheSet.BelowUpdateCache

java.lang.Object

de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCache

de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet.BelowUpdateCache

All Implemented Interfaces:

ITermTacletAppIndexCache

Enclosing class:

TermTacletAppIndexCacheSet

private class TermTacletAppIndexCacheSet.BelowUpdateCache
extends PrefixTermTacletAppIndexCache

Constructor Summary

Constructors

Constructor and Description
BelowUpdateCache(ImmutableList<QuantifiableVariable> prefix)

Method Summary

Modifier and Type	Method and Description
ITermTacletAppIndexCache	descend(Term t, int subtermIndex) Determine the cache that is responsible for locations within the subtermIndex'th subterm of the term t (assuming that this cache is responsible for the location of the term t).
TermTacletAppIndex	getIndexForTerm(Term t)
void	putIndexForTerm(Term t, TermTacletAppIndex index) Put the taclet app index index for the term t in the cache

Methods inherited from class de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCache

getExtendedPrefix, getExtendedPrefix, getPrefix

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

BelowUpdateCache

public BelowUpdateCache(ImmutableList<QuantifiableVariable> prefix)

Method Detail

descend

public ITermTacletAppIndexCache descend(Term t,
                                        int subtermIndex)

Description copied from interface: ITermTacletAppIndexCache

Determine the cache that is responsible for locations within the subtermIndex'th subterm of the term t (assuming that this cache is responsible for the location of the term t). This method is used in TermTacletAppIndex when recursively constructing the index for a given term.

getIndexForTerm

public TermTacletAppIndex getIndexForTerm(Term t)

Returns:

the taclet app index for the term t, or null if no index for this term was found in the cache

putIndexForTerm

public void putIndexForTerm(Term t,
                            TermTacletAppIndex index)

Description copied from interface: ITermTacletAppIndexCache

Put the taclet app index index for the term t in the cache