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.termgenerator;
12:
13: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
14: import de.uka.ilkd.key.logic.IteratorOfTerm;
15: import de.uka.ilkd.key.logic.PosInOccurrence;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.rule.RuleApp;
19:
20: /**
21: * Term generator that enumerates the formulas of the current
22: * sequent/antecedent/succedent.
23: */
24: public abstract class SequentFormulasGenerator implements TermGenerator {
25:
26: protected SequentFormulasGenerator() {
27: }
28:
29: public static SequentFormulasGenerator antecedent() {
30: return new SequentFormulasGenerator() {
31: protected IteratorOfConstrainedFormula generateForIt(
32: Goal goal) {
33: return goal.sequent().antecedent().iterator();
34: }
35: };
36: }
37:
38: public static SequentFormulasGenerator succedent() {
39: return new SequentFormulasGenerator() {
40: protected IteratorOfConstrainedFormula generateForIt(
41: Goal goal) {
42: return goal.sequent().succedent().iterator();
43: }
44: };
45: }
46:
47: public static SequentFormulasGenerator sequent() {
48: return new SequentFormulasGenerator() {
49: protected IteratorOfConstrainedFormula generateForIt(
50: Goal goal) {
51: return goal.sequent().iterator();
52: }
53: };
54: }
55:
56: protected abstract IteratorOfConstrainedFormula generateForIt(
57: Goal goal);
58:
59: public IteratorOfTerm generate(RuleApp app, PosInOccurrence pos,
60: Goal goal) {
61: return new Iterator(generateForIt(goal));
62: }
63:
64: private static class Iterator implements IteratorOfTerm {
65: private final IteratorOfConstrainedFormula forIt;
66:
67: public boolean hasNext() {
68: return forIt.hasNext();
69: }
70:
71: public Term next() {
72: return forIt.next().formula();
73: }
74:
75: public Iterator(IteratorOfConstrainedFormula forIt) {
76: this.forIt = forIt;
77: }
78: }
79: }
|