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: /* Generated by Together */
012:
013: package de.uka.ilkd.key.logic;
014:
015: import java.util.Stack;
016:
017: import de.uka.ilkd.key.logic.op.*;
018:
019: /**
020: * visitor for <t> execPostOrder </t> of
021: * {@link de.uka.ilkd.key.logic.Term}. Called with that method
022: * on a term, the visitor evaluates all contained substitution terms
023: * by applying a
024: * suitable substitution. Occuring collisions are adequately handled.
025: * REMARK: The current implementation is not very efficient. This
026: * seems to be (at the moment)
027: * not so important, because the operation this class implements will
028: * rarely occur !
029: */
030:
031: public class CollisionDeletingSubstitutionTermApplier extends Visitor {
032:
033: /**
034: * the stack contains the subterms that will be used in getTerm() in Term
035: * in order to build the new term. A boolean value
036: * between or under the subterms on the stack indicate that a term using
037: * these subterms should build a new term instead of using the old one,
038: * because one of its subterms has been built, too.
039: */
040: private Stack subStack; //of Term (and Boolean)
041: private TermFactory tf = TermFactory.DEFAULT;
042: private Boolean newMarker = Boolean.TRUE;
043:
044: public CollisionDeletingSubstitutionTermApplier() {
045: subStack = new Stack(); // of Term
046: }
047:
048: private Term[] neededSubs(int n) {
049: boolean newTerm = false;
050: Term[] result = new Term[n];
051: for (int i = n - 1; i >= 0; i--) {
052: Object top = subStack.pop();
053: if (top == newMarker) {
054: newTerm = true;
055: top = subStack.pop();
056: }
057: result[i] = (Term) top;
058: }
059: if (newTerm
060: && (subStack.empty() || subStack.peek() != newMarker)) {
061: subStack.push(newMarker);
062: }
063: return result;
064: }
065:
066: public void visit(Term visited) {
067: // Sort equality has to be ensured before calling this method
068: MapFromLogicVariableToTerm substToApply;
069: Term resultTerm;
070:
071: // vars bound directly by operator of visited term ...
072: ArrayOfQuantifiableVariable vars = (visited.varsBoundHere(0)
073: .size() == 0) ? visited.varsBoundHere(1) : visited
074: .varsBoundHere(0);
075:
076: if (visited.op() == Op.SUBST) {
077: // get completely processed childs ...
078: Term[] neededsubs = neededSubs(visited.arity());
079: substToApply = MapAsListFromLogicVariableToTerm.EMPTY_MAP;
080: // Replace substVar 'x' by 'KS(s)' if the
081: // SubstitutionTerm has the form {x s} t
082: // and leave other variables unchanged ...
083: substToApply = substToApply.put((LogicVariable) visited
084: .varsBoundHere(1).getQuantifiableVariable(0),
085: neededsubs[0]);
086: IteratorOfEntryOfLogicVariableAndTerm it = substToApply
087: .entryIterator();
088: while (it.hasNext()) {
089: EntryOfLogicVariableAndTerm substitution = it.next();
090: ClashFreeSubst cfSubst = new ClashFreeSubst(
091: substitution.key(), substitution.value());
092: resultTerm = cfSubst.apply(neededsubs[1]);
093: //pop result on stack and mark as new ...
094: subStack.push(resultTerm);
095: if (resultTerm != neededsubs[1]) {
096: subStack.push(newMarker);
097: }
098: }
099: } else {
100: Term[] neededsubs = neededSubs(visited.arity());
101: if (!subStack.empty() && subStack.peek() == newMarker) {
102: subStack.pop(); // delete new marker ...
103: subStack.push(tf.createTerm(visited.op(), neededsubs,
104: vars, visited.javaBlock()));
105: subStack.push(newMarker); // add new marker ...
106:
107: } else {
108: subStack.push(visited);
109: }
110: }
111: }
112:
113: /**
114: * resets (internal) state of the visitor.
115: */
116:
117: public void reset() {
118: subStack = new Stack(); // of Term
119: }
120:
121: /**
122: * delivers the new built term
123: */
124: public Term getTerm() {
125: Object result = subStack.pop();
126: if (result == newMarker) {
127: result = subStack.pop();
128: }
129: return ((Term) result);
130: }
131:
132: }
|