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.HashMap;
016: import java.util.Iterator;
017: import java.util.Stack;
018:
019: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
020: import de.uka.ilkd.key.logic.op.Function;
021: import de.uka.ilkd.key.logic.op.NonRigidFunction;
022: import de.uka.ilkd.key.logic.op.Operator;
023:
024: /**
025: * Only for use in the generation of the translation of an OCL constaint !!!
026: *
027: * creates a mapping of the names of functions (as strings) to the
028: * corresponding functionsymbol (object) ...
029: */
030: public class PostFormulaTransformer extends Visitor {
031:
032: private java.util.Map funcNameSymbolMap;
033: private java.util.Map nonrigidFunctionSymbolMap;
034: private Term computedResult;
035:
036: /**
037: * the stack contains the subterms that will be added in the next step of
038: * execPostOrder in Term in order to build the new term. A boolean value
039: * between or under the subterms on the stack indicate that a term using
040: * these subterms should build a new term instead of using the old one,
041: * because one of its subterms has been built, too.
042: */
043: private Stack subStack; //of Term (and Boolean)
044: private TermFactory tf = TermFactory.DEFAULT;
045: private Boolean newMarker = new Boolean(true);
046:
047: // SUFFIX FOR NEW FUNCTION SYMBOLS ...
048: public final static String NEW_FUNCSYMBOL_SUFFIX = "'";
049:
050: public PostFormulaTransformer(
051: java.util.Set nonrigidFunctionSymbols,
052: java.util.Map funcNameSymbolMap) {
053: this .funcNameSymbolMap = funcNameSymbolMap;
054: computedResult = null;
055: subStack = new Stack(); // of Term
056:
057: // Now we have to initialze the mapping which maps every nonrigid function symbol
058: // in a postcondition onto a new function symbol ...
059: nonrigidFunctionSymbolMap = new HashMap();
060: Function currentFunction, newFunction;
061: String fNameString;
062: String newFuncNameString;
063: Name newFuncName;
064:
065: for (Iterator fSymbIt = nonrigidFunctionSymbols.iterator(); fSymbIt
066: .hasNext();) {
067: currentFunction = (Function) fSymbIt.next();
068: fNameString = currentFunction.name().toString();
069: if (!fNameString.endsWith("@pre")) {
070: // REMARK: @pre-functions will be handled specially in visit(..)-method !
071:
072: newFuncNameString = fNameString + NEW_FUNCSYMBOL_SUFFIX;
073:
074: newFuncName = new Name(newFuncNameString);
075:
076: // System.err.println("created NEW SINGLE NAME == " + newFuncName);
077:
078: newFunction = new NonRigidFunction(newFuncName,
079: currentFunction.sort(), currentFunction
080: .argSort());
081: nonrigidFunctionSymbolMap.put(currentFunction,
082: newFunction);
083:
084: }
085: }
086:
087: }
088:
089: private Term[] neededSubs(int n) {
090: boolean newTerm = false;
091: Term[] result = new Term[n];
092: for (int i = n - 1; i >= 0; i--) {
093: Object top = subStack.pop();
094: if (top == newMarker) {
095: newTerm = true;
096: top = subStack.pop();
097: }
098: result[i] = (Term) top;
099: }
100: if (newTerm
101: && (subStack.empty() || subStack.peek() != newMarker)) {
102: subStack.push(newMarker);
103: }
104: return result;
105: }
106:
107: public void visit(Term visited) {
108:
109: // System.err.println("Currently VISITING : " + visited);
110:
111: boolean changed = false;
112: Function newFunctionSymbol = null;
113: Function functionToReplaceForAtPre;
114:
115: if (visited.op() instanceof Function) {
116: Function currentFunction = (Function) visited.op();
117: newFunctionSymbol = currentFunction;
118: String funcNameString = currentFunction.name().toString();
119: if (funcNameString.endsWith("@pre")) {
120: // we have an @pre-function, therefore we have to check, whether
121: // we must replace
122:
123: // Check whether we already have a corresponding function symbol in the
124: // map from the preconditionFormulas ...
125: String searchFuncName = funcNameString.substring(0,
126: funcNameString.length() - 4);
127:
128: // System.err.println("REPLACING " + funcNameString + "; Searching for : " + searchFuncName);
129:
130: if (funcNameSymbolMap.containsKey(searchFuncName)) {
131: functionToReplaceForAtPre = (Function) funcNameSymbolMap
132: .get(searchFuncName);
133: // System.err.println("FOUND ! REPLACE WITH :" + functionToReplaceForAtPre);
134: } else {
135: // the corresponding function (in the pre state) has not been used in
136: // the preconditionFormula therefore we have to create a new such symbol
137: // and store it in the map ...
138: Name newFuncName = new Name(searchFuncName);
139:
140: functionToReplaceForAtPre = new NonRigidFunction(
141: newFuncName, currentFunction.sort(),
142: currentFunction.argSort());
143: funcNameSymbolMap.put(searchFuncName,
144: functionToReplaceForAtPre);
145:
146: // System.err.println("NOT FOUND ! REPLACE WITH :" + functionToReplaceForAtPre);
147:
148: }
149:
150: newFunctionSymbol = functionToReplaceForAtPre;
151: changed = true;
152: } else {
153: // Check other case in which a function symbol has to be replaced
154: // by a new one:
155: // If we have a rigidFunctionSymbol (but not with @pre)
156: // , we have to replace it by a new
157: // function symbol ( specified in nonrigidFunctionMap ) ...
158:
159: if (nonrigidFunctionSymbolMap
160: .containsKey(currentFunction)) {
161: // we have to replace the current function symbol by
162: // the function symbol specified by the nonrigidFunctionMap ...
163:
164: // System.err.println("REPLACING (rigid) " + funcNameString );
165:
166: newFunctionSymbol = (Function) nonrigidFunctionSymbolMap
167: .get(currentFunction);
168: // System.err.println("REPLACE WITH :" + newFunctionSymbol);
169:
170: changed = true;
171: }
172:
173: }
174:
175: }
176:
177: if (changed
178: && (subStack.empty() || subStack.peek() != newMarker)) {
179: subStack.push(newMarker);
180: }
181:
182: ArrayOfQuantifiableVariable boundVars = ((visited
183: .varsBoundHere(0).size() == 0) ? visited
184: .varsBoundHere(1) : visited.varsBoundHere(0));
185:
186: Term[] neededsubs = neededSubs(visited.arity());
187: if (changed
188: || (!subStack.empty() && subStack.peek() == newMarker)) {
189:
190: //System.err.println("Create new term with : " );
191: //System.err.println("func symbol == : " + newFunctionSymbol );
192: //System.err.println("boundVars == : " + boundVars);
193:
194: Operator newOp;
195: if (changed) {
196: // Take the newly generated function symbol ...
197: newOp = newFunctionSymbol;
198: } else {
199: // Take the existing one ...
200: newOp = visited.op();
201: }
202:
203: subStack.push(tf.createTerm(newOp, neededsubs, boundVars,
204: visited.javaBlock()));
205: } else {
206: subStack.push(visited);
207: }
208:
209: }
210:
211: /**
212: * delivers the new built term
213: */
214: public Term getTerm() {
215: if (computedResult == null) {
216: Object o = null;
217: do {
218: o = subStack.pop();
219: } while (o == newMarker);
220: Term t = (Term) o;
221: if (t != null) {
222: computedResult = t;
223: }
224: }
225: return computedResult;
226: }
227:
228: }
|