01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.proof;
12:
13: import de.uka.ilkd.key.logic.Term;
14:
15: /**
16: * The general interface for caches for accelerating
17: * <code>TermTacletAppIndex</code>.
18: *
19: * @see TermTacletAppIndexCacheSet
20: */
21: public interface ITermTacletAppIndexCache {
22:
23: /**
24: * @return the taclet app index for the term <code>t</code>, or
25: * <code>null</code> if no index for this term was found in the
26: * cache
27: */
28: TermTacletAppIndex getIndexForTerm(Term t);
29:
30: /**
31: * Put the taclet app index <code>index</code> for the term <code>t</code>
32: * in the cache
33: */
34: void putIndexForTerm(Term t, TermTacletAppIndex index);
35:
36: /**
37: * Determine the cache that is responsible for locations within the
38: * <code>subtermIndex</code>'th subterm of the term <code>t</code>
39: * (assuming that <code>this</code> cache is responsible for the location
40: * of the term <code>t</code>). This method is used in
41: * <code>TermTacletAppIndex</code> when recursively constructing the index
42: * for a given term.
43: */
44: ITermTacletAppIndexCache descend(Term t, int subtermIndex);
45:
46: }
|