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.java.Services;
014: import de.uka.ilkd.key.logic.IteratorOfTerm;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.PosInOccurrence;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.TermBuilder;
019: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
020: import de.uka.ilkd.key.logic.op.Function;
021: import de.uka.ilkd.key.logic.op.RigidFunction;
022: import de.uka.ilkd.key.logic.sort.Sort;
023: import de.uka.ilkd.key.proof.Goal;
024: import de.uka.ilkd.key.rule.RuleApp;
025: import de.uka.ilkd.key.strategy.TopRuleAppCost;
026: import de.uka.ilkd.key.strategy.termfeature.TermFeature;
027:
028: public abstract class SuperTermGenerator implements TermGenerator {
029:
030: private final TermFeature cond;
031:
032: protected SuperTermGenerator(TermFeature cond) {
033: this .cond = cond;
034: }
035:
036: public static TermGenerator upwards(TermFeature cond) {
037: return new SuperTermGenerator(cond) {
038: protected IteratorOfTerm createIterator(
039: PosInOccurrence focus) {
040: return new UpwardsIterator(focus);
041: }
042: };
043: }
044:
045: public static TermGenerator upwardsWithIndex(TermFeature cond) {
046: return new SuperTermWithIndexGenerator(cond) {
047: protected IteratorOfTerm createIterator(
048: PosInOccurrence focus) {
049: return new UpwardsIterator(focus);
050: }
051: };
052: }
053:
054: public IteratorOfTerm generate(RuleApp app, PosInOccurrence pos,
055: Goal goal) {
056: return createIterator(pos);
057: }
058:
059: protected abstract IteratorOfTerm createIterator(
060: PosInOccurrence focus);
061:
062: protected Term generateOneTerm(Term super term, int child) {
063: return super term;
064: }
065:
066: private boolean generateFurther(Term t) {
067: return !(cond.compute(t) instanceof TopRuleAppCost);
068: }
069:
070: abstract static class SuperTermWithIndexGenerator extends
071: SuperTermGenerator {
072: private Services services;
073: private Function binFunc;
074:
075: protected SuperTermWithIndexGenerator(TermFeature cond) {
076: super (cond);
077: }
078:
079: public IteratorOfTerm generate(RuleApp app,
080: PosInOccurrence pos, Goal goal) {
081: if (services == null) {
082: services = goal.proof().getServices();
083: final IntegerLDT numbers = services.getTypeConverter()
084: .getIntegerLDT();
085:
086: binFunc = new RigidFunction(new Name(
087: "SuperTermGenerated"), Sort.ANY, new Sort[] {
088: Sort.ANY, numbers.getNumberSymbol().sort() });
089: }
090:
091: return createIterator(pos);
092: }
093:
094: protected Term generateOneTerm(Term super term, int child) {
095: final Term index = TermBuilder.DF.zTerm(services, ""
096: + child);
097: return TermBuilder.DF.func(binFunc, super term, index);
098: }
099: }
100:
101: class UpwardsIterator implements IteratorOfTerm {
102: private PosInOccurrence currentPos;
103:
104: private UpwardsIterator(PosInOccurrence startPos) {
105: this .currentPos = startPos;
106: }
107:
108: public boolean hasNext() {
109: return currentPos != null && !currentPos.isTopLevel();
110: }
111:
112: public Term next() {
113: final int child = currentPos.getIndex();
114: currentPos = currentPos.up();
115: final Term res = generateOneTerm(currentPos.subTerm(),
116: child);
117: if (!generateFurther(res))
118: currentPos = null;
119: return res;
120: }
121: }
122:
123: }
|