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.strategy.feature;
12:
13: import de.uka.ilkd.key.logic.PIOPathIterator;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.op.IUpdateOperator;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.rule.TacletApp;
18:
19: /**
20: * Feature for investigating whether the focus of a rule application is a
21: * top-level formula, a top-level formula of the antecedent or a top-level
22: * formula of the succedent
23: */
24: public abstract class TopLevelFindFeature extends
25: BinaryTacletAppFeature {
26:
27: private static abstract class TopLevelWithoutUpdate extends
28: TopLevelFindFeature {
29: protected abstract boolean matches(PosInOccurrence pos);
30:
31: protected boolean checkPosition(PosInOccurrence pos) {
32: return pos.isTopLevel() && matches(pos);
33: }
34: }
35:
36: private static abstract class TopLevelWithUpdate extends
37: TopLevelFindFeature {
38: protected abstract boolean matches(PosInOccurrence pos);
39:
40: protected boolean checkPosition(PosInOccurrence pos) {
41: if (!pos.isTopLevel()) {
42: final PIOPathIterator it = pos.iterator();
43: while (it.next() != -1) {
44: if (!(it.getSubTerm().op() instanceof IUpdateOperator))
45: return false;
46: }
47: }
48:
49: return matches(pos);
50: }
51: }
52:
53: public final static Feature ANTEC_OR_SUCC = new TopLevelWithoutUpdate() {
54: protected boolean matches(PosInOccurrence pos) {
55: return true;
56: }
57: };
58:
59: public final static Feature ANTEC = new TopLevelWithoutUpdate() {
60: protected boolean matches(PosInOccurrence pos) {
61: return pos.isInAntec();
62: }
63: };
64:
65: public final static Feature SUCC = new TopLevelWithoutUpdate() {
66: protected boolean matches(PosInOccurrence pos) {
67: return !pos.isInAntec();
68: }
69: };
70:
71: public final static Feature ANTEC_OR_SUCC_WITH_UPDATE = new TopLevelWithUpdate() {
72: protected boolean matches(PosInOccurrence pos) {
73: return true;
74: }
75: };
76:
77: public final static Feature ANTEC_WITH_UPDATE = new TopLevelWithUpdate() {
78: protected boolean matches(PosInOccurrence pos) {
79: return pos.isInAntec();
80: }
81: };
82:
83: public final static Feature SUCC_WITH_UPDATE = new TopLevelWithUpdate() {
84: protected boolean matches(PosInOccurrence pos) {
85: return !pos.isInAntec();
86: }
87: };
88:
89: protected boolean filter(TacletApp app, PosInOccurrence pos,
90: Goal goal) {
91: assert pos != null : "Feature is only applicable to rules with find";
92: return checkPosition(pos);
93: }
94:
95: protected abstract boolean checkPosition(PosInOccurrence pos);
96:
97: }
|