001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.strategy.termgenerator;
012:
013: import de.uka.ilkd.key.logic.IteratorOfTerm;
014: import de.uka.ilkd.key.logic.ListOfTerm;
015: import de.uka.ilkd.key.logic.PosInOccurrence;
016: import de.uka.ilkd.key.logic.SLListOfTerm;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.proof.Goal;
019: import de.uka.ilkd.key.rule.RuleApp;
020: import de.uka.ilkd.key.strategy.TopRuleAppCost;
021: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
022: import de.uka.ilkd.key.strategy.termfeature.TermFeature;
023:
024: /**
025: * Term generator that enumerates the subterms or subformulas of a given term.
026: * Similarly to <code>RecSubTermFeature</code>, a term feature can be given
027: * that determines when traversal should be stopped, i.e., when one should not
028: * descend further into a term.
029: */
030: public abstract class SubtermGenerator implements TermGenerator {
031:
032: private final TermFeature cond;
033: private final ProjectionToTerm completeTerm;
034:
035: private SubtermGenerator(ProjectionToTerm completeTerm,
036: TermFeature cond) {
037: this .cond = cond;
038: this .completeTerm = completeTerm;
039: }
040:
041: /**
042: * Left-traverse the subterms of a term in depth-first order. Each term is
043: * returned before its proper subterms.
044: */
045: public static TermGenerator leftTraverse(ProjectionToTerm cTerm,
046: TermFeature cond) {
047: return new SubtermGenerator(cTerm, cond) {
048: public IteratorOfTerm generate(RuleApp app,
049: PosInOccurrence pos, Goal goal) {
050: return new LeftIterator(getTermInst(app, pos, goal));
051: }
052: };
053: }
054:
055: /**
056: * Right-traverse the subterms of a term in depth-first order. Each term is
057: * returned before its proper subterms.
058: */
059: public static TermGenerator rightTraverse(ProjectionToTerm cTerm,
060: TermFeature cond) {
061: return new SubtermGenerator(cTerm, cond) {
062: public IteratorOfTerm generate(RuleApp app,
063: PosInOccurrence pos, Goal goal) {
064: return new RightIterator(getTermInst(app, pos, goal));
065: }
066: };
067: }
068:
069: protected Term getTermInst(RuleApp app, PosInOccurrence pos,
070: Goal goal) {
071: return completeTerm.toTerm(app, pos, goal);
072: }
073:
074: private boolean descendFurther(Term t) {
075: return !(cond.compute(t) instanceof TopRuleAppCost);
076: }
077:
078: abstract class Iterator implements IteratorOfTerm {
079: protected ListOfTerm termStack;
080:
081: public Iterator(Term t) {
082: termStack = SLListOfTerm.EMPTY_LIST.prepend(t);
083: }
084:
085: public boolean hasNext() {
086: return !termStack.isEmpty();
087: }
088: }
089:
090: class LeftIterator extends Iterator {
091: public LeftIterator(Term t) {
092: super (t);
093: }
094:
095: public Term next() {
096: final Term res = termStack.head();
097: termStack = termStack.tail();
098:
099: if (descendFurther(res)) {
100: for (int i = res.arity() - 1; i >= 0; --i)
101: termStack = termStack.prepend(res.sub(i));
102: }
103:
104: return res;
105: }
106: }
107:
108: class RightIterator extends Iterator {
109: public RightIterator(Term t) {
110: super (t);
111: }
112:
113: public Term next() {
114: final Term res = termStack.head();
115: termStack = termStack.tail();
116:
117: if (descendFurther(res)) {
118: for (int i = 0; i != res.arity(); ++i)
119: termStack = termStack.prepend(res.sub(i));
120: }
121:
122: return res;
123: }
124: }
125: }
|