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: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
15: import de.uka.ilkd.key.logic.op.ListOfQuantifiableVariable;
16:
17: /**
18: * The abstract superclass of caches for taclet app indexes that are separated
19: * by different prefixes of bound variables. This class simply stores a
20: * <code>ListOfQuantifiableVariable</code> and offers a couple of access
21: * functions to this list.
22: */
23: abstract class PrefixTermTacletAppIndexCache implements
24: ITermTacletAppIndexCache {
25:
26: private final ListOfQuantifiableVariable prefix;
27:
28: protected PrefixTermTacletAppIndexCache(
29: ListOfQuantifiableVariable prefix) {
30: this .prefix = prefix;
31: }
32:
33: protected ListOfQuantifiableVariable getPrefix() {
34: return prefix;
35: }
36:
37: protected ListOfQuantifiableVariable getExtendedPrefix(
38: ArrayOfQuantifiableVariable extension) {
39: ListOfQuantifiableVariable res = prefix;
40: for (int i = 0; i != extension.size(); ++i)
41: res = res.prepend(extension.getQuantifiableVariable(i));
42: return res;
43: }
44:
45: protected ListOfQuantifiableVariable getExtendedPrefix(Term t,
46: int subtermIndex) {
47: return getExtendedPrefix(t.varsBoundHere(subtermIndex));
48: }
49:
50: }
|