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.logic;
012:
013: import de.uka.ilkd.key.logic.op.Metavariable;
014: import de.uka.ilkd.key.util.Debug;
015:
016: /**
017: * This class describes a position in an occurrence of a term. A
018: * ConstrainedFormula and a PosInTerm determine an object of this
019: * class exactly.
020: */
021: public class PosInOccurrence {
022:
023: public static PosInOccurrence findInSequent(Sequent seq,
024: int formulaNumber, PosInTerm pos) {
025: return new PosInOccurrence(seq.getFormulabyNr(formulaNumber),
026: pos, seq.numberInAntec(formulaNumber));
027: }
028:
029: /**
030: * the constrained formula the pos in occurrence describes
031: */
032: private final ConstrainedFormula cfma;
033:
034: private final int hashCode;
035: /**
036: * is true iff the position is in the antecedent of a sequent.
037: */
038: private final boolean inAntec;
039:
040: private final PosInTerm metaPosInTerm;
041:
042: // Descend into metavariables instantiations
043: private final Term metaTerm;
044:
045: /** the position in cfma.formula() */
046: private final PosInTerm posInTerm;
047:
048: /**
049: * The subterm this object points to, or <code>null</code>
050: */
051: private Term subTermCache = null;
052:
053: public PosInOccurrence(ConstrainedFormula cfma,
054: PosInTerm posInTerm, boolean inAntec) {
055: this (cfma, posInTerm, null, null, inAntec);
056: }
057:
058: private PosInOccurrence(ConstrainedFormula cfma,
059: PosInTerm posInTerm, Term metaTerm,
060: PosInTerm metaPosInTerm, boolean inAntec) {
061: this .inAntec = inAntec;
062: this .cfma = cfma;
063: this .posInTerm = posInTerm;
064: this .metaTerm = metaTerm;
065: this .metaPosInTerm = metaPosInTerm;
066: this .hashCode = computeHash();
067: }
068:
069: private int computeHash() {
070: int res = constrainedFormula().hashCode() * 13
071: + posInTerm().hashCode();
072: if (termBelowMetavariable() != null)
073: res += termBelowMetavariable().hashCode() * 13
074: + posInTermBelowMetavariable().hashCode();
075: return res;
076: }
077:
078: /**
079: * returns the ConstrainedFormula that determines the occurrence of
080: * this PosInOccurrence
081: */
082: public ConstrainedFormula constrainedFormula() {
083: return cfma;
084: }
085:
086: /**
087: * @return Depth of the represented position within a formula; top-level
088: * positions (<code>isTopLevel()</code> have depth zero
089: */
090: public int depth() {
091: int res = posInTerm().depth();
092:
093: if (termBelowMetavariable() != null)
094: res += posInTermBelowMetavariable().depth();
095:
096: return res;
097: }
098:
099: /**
100: * creates a new PosInOccurrence that has exactly the same state as this
101: * object except the PosInTerm is new and walked down the specified
102: * subterm, as specified in method down of
103: * {@link de.uka.ilkd.key.logic.PosInTerm}.
104: */
105: public PosInOccurrence down(int i) {
106: if (metaTerm == null)
107: return new PosInOccurrence(cfma, posInTerm.down(i), inAntec);
108: else
109: return new PosInOccurrence(cfma, posInTerm, metaTerm,
110: metaPosInTerm.down(i), inAntec);
111: }
112:
113: /**
114: * compares this PosInOccurrence with another PosInOccurrence
115: * and returns true if both describe the same occurrence
116: */
117: public boolean eqEquals(Object obj) {
118: if (!(obj instanceof PosInOccurrence)) {
119: return false;
120: }
121: final PosInOccurrence cmp = (PosInOccurrence) obj;
122:
123: if (!constrainedFormula().equals(cmp.constrainedFormula())) {
124: return false;
125: }
126:
127: return equalsHelp(cmp);
128: }
129:
130: /**
131: * Contrary to <code>eqEquals</code>, this method returns true only for pio
132: * objects that point to the same (identical) formula
133: * @param obj
134: * @return
135: */
136: public boolean equals(Object obj) {
137: if (!(obj instanceof PosInOccurrence)) {
138: return false;
139: }
140: final PosInOccurrence cmp = (PosInOccurrence) obj;
141:
142: // NB: the class <code>NonDuplicateAppFeature</code> depends on the usage
143: // of <code>!=</code> in this condition
144: if (constrainedFormula() != cmp.constrainedFormula()) {
145: return false;
146: }
147:
148: return equalsHelp(cmp);
149: }
150:
151: private boolean equalsHelp(final PosInOccurrence cmp) {
152: if (isInAntec() == cmp.isInAntec()) {
153: if (!posInTerm().equals(cmp.posInTerm()))
154: return false;
155:
156: if (termBelowMetavariable() == null)
157: return cmp.termBelowMetavariable() == null;
158: else
159: return termBelowMetavariable().equals(
160: cmp.termBelowMetavariable())
161: && posInTermBelowMetavariable().equals(
162: cmp.posInTermBelowMetavariable());
163: }
164: return false;
165: }
166:
167: /**
168: * @return the number/index of the deepest subterm that this
169: * <code>PosInOccurrence</code> points to. If the position is
170: * top-level, the result will be <code>-1</code>
171: */
172: public int getIndex() {
173: if (metaTerm == null || metaPosInTerm == PosInTerm.TOP_LEVEL)
174: return posInTerm.getIndex();
175: return metaPosInTerm.getIndex();
176: }
177:
178: public int hashCode() {
179: return hashCode;
180: }
181:
182: /**
183: * returns true iff the occurrence is in the
184: * antecedent of a sequent.
185: */
186: public boolean isInAntec() {
187: return inAntec;
188: }
189:
190: public boolean isTopLevel() {
191: return posInTerm == PosInTerm.TOP_LEVEL
192: && (metaTerm == null || metaPosInTerm == PosInTerm.TOP_LEVEL);
193: }
194:
195: /**
196: * List all subterms between the root and the position this
197: * objects points to; the first term is the whole term
198: * <code>constrainedFormula().formula()</code>, the last one
199: * <code>subTerm()</code>
200: * @return an iterator that walks from the root of the term to the
201: * position this <code>PosInOccurrence</code>-object points to
202: */
203: public PIOPathIterator iterator() {
204: return new PIOPathIteratorImpl();
205: }
206:
207: /**
208: * The usage of this method is strongly discouraged, use
209: * {@link PosInOccurrence#iterator} instead.
210: * describes the exact occurence of the refered term inside
211: * {@link ConstrainedFormula#formula()}
212: * @returns the position in the formula of the ConstrainedFormula of
213: * this PosInOccurrence.
214: */
215: public PosInTerm posInTerm() {
216: return posInTerm;
217: }
218:
219: /**
220: * The usage of this method is strongly discouraged, use
221: * {@link PosInOccurrence#iterator} instead.
222: */
223: public PosInTerm posInTermBelowMetavariable() {
224: return metaPosInTerm;
225: }
226:
227: /**
228: * Replace the formula this object points to with the new formula given
229: *
230: * @param p_newFormula
231: * the new formula
232: * @return a <code>PosInOccurrence</code> object that points to the same
233: * position within the formula <code>p_newFormula</code> as this
234: * object does within the formula <code>constrainedFormula()</code>.
235: * It is not tested whether this position exists within <code>p_newFormula</code>
236: */
237: public PosInOccurrence replaceConstrainedFormula(
238: ConstrainedFormula p_newFormula) {
239: final PIOPathIterator it = iterator();
240: Term newTerm = p_newFormula.formula();
241: PosInTerm newPosInTerm = PosInTerm.TOP_LEVEL;
242: int depth = 0;
243:
244: while (true) {
245: final int subNr = it.next();
246:
247: if (newTerm.op() instanceof Metavariable
248: && depth == posInTerm().depth()) {
249: // It is necessary to insert a term below the metavariable,
250: // as the iterator still holds further elements
251:
252: return new PosInOccurrence(p_newFormula, posInTerm(),
253: termBelowMetavariable(),
254: posInTermBelowMetavariable(), inAntec);
255: }
256:
257: if (subNr == -1)
258: break;
259:
260: newPosInTerm = newPosInTerm.down(subNr);
261: newTerm = newTerm.sub(subNr);
262: ++depth;
263: }
264:
265: return new PosInOccurrence(p_newFormula, newPosInTerm, inAntec);
266: }
267:
268: /**
269: * If "this" points to a metavariable, a term can be inserted at
270: * this position, allowing to walk down the term further "inside"
271: * the metavariable.
272: */
273: public PosInOccurrence setTermBelowMetavariable(Term p_metaTerm) {
274: if (Debug.ENABLE_ASSERTION) {
275: Debug
276: .assertTrue(
277: metaTerm == null
278: && (constrainedFormula().formula()
279: .subAt(posInTerm).op() instanceof Metavariable)
280: && p_metaTerm.sort().extendsTrans(
281: constrainedFormula()
282: .formula().subAt(
283: posInTerm)
284: .sort()),
285: "Illegal position (no metavariable) or incompatible sorts");
286: }
287:
288: return new PosInOccurrence(cfma, posInTerm, p_metaTerm,
289: PosInTerm.TOP_LEVEL, inAntec);
290: }
291:
292: /**
293: * returns the subterm this object points to
294: */
295: public Term subTerm() {
296: if (subTermCache == null) {
297: if (metaTerm == null)
298: subTermCache = constrainedFormula().formula().subAt(
299: posInTerm);
300: else
301: subTermCache = metaTerm.subAt(metaPosInTerm);
302: }
303: return subTermCache;
304: }
305:
306: /** The usage of this method is strongly discouraged, use
307: * {@link PosInOccurrence#iterator} instead if possible.
308: */
309: public Term termBelowMetavariable() {
310: return metaTerm;
311: }
312:
313: /**
314: * Ascend to the top node of the formula this object points to
315: */
316: public PosInOccurrence topLevel() {
317: if (isTopLevel()) {
318: return this ;
319: }
320: return new PosInOccurrence(cfma, PosInTerm.TOP_LEVEL, inAntec);
321: }
322:
323: /** toString */
324: public String toString() {
325: String res = "Term " + posInTerm() + " of "
326: + constrainedFormula();
327: if (termBelowMetavariable() != null)
328: res += " / Term " + posInTermBelowMetavariable() + " of "
329: + termBelowMetavariable();
330: return res;
331: // formulaNumberInSequent()+" th formula";
332:
333: }
334:
335: /**
336: * Ascend to the parent node
337: */
338: public PosInOccurrence up() {
339: assert !isTopLevel() : "not possible to go up from top level position";
340: if (metaTerm == null || metaPosInTerm == PosInTerm.TOP_LEVEL)
341: return new PosInOccurrence(cfma, posInTerm.up(), inAntec);
342: else
343: return new PosInOccurrence(cfma, posInTerm, metaTerm,
344: metaPosInTerm.up(), inAntec);
345: }
346:
347: private class PIOPathIteratorImpl implements PIOPathIterator {
348: boolean belowMetavariable = false;
349: int child;
350: int count = 0;
351: IntIterator currentPathIt;
352: Term currentSubTerm = null;
353:
354: private PIOPathIteratorImpl() {
355: currentPathIt = posInTerm().iterator();
356: }
357:
358: private PosInTerm firstN(PosInTerm p_pit, int p_n) {
359: IntIterator it = p_pit.iterator();
360: PosInTerm res = PosInTerm.TOP_LEVEL;
361:
362: while (p_n-- != 0)
363: res = res.down(it.next());
364:
365: return res;
366: }
367:
368: /**
369: * @return the number of the next child on the path, or
370: * <code>-1</code> if no further child exists (this is the number
371: * that was also returned by the last call of <code>next()</code>)
372: */
373: public int getChild() {
374: return child;
375: }
376:
377: /**
378: * @return the current position within the term
379: * (i.e. corresponding to the latest <code>next()</code>-call)
380: */
381: public PosInOccurrence getPosInOccurrence() {
382: // the object is created only now to make the method
383: // <code>next()</code> faster
384:
385: final PosInOccurrence pio;
386: if (belowMetavariable) {
387: pio = new PosInOccurrence(cfma, posInTerm, metaTerm,
388: firstN(metaPosInTerm, count - posInTerm.depth()
389: - 1), inAntec);
390: } else {
391: pio = new PosInOccurrence(cfma, firstN(posInTerm,
392: count - 1), inAntec);
393: }
394:
395: return pio;
396: }
397:
398: /**
399: * @return the current subterm this object points to
400: * (i.e. corresponding to the latest <code>next()</code>-call);
401: * this method satisfies
402: * <code>getPosInOccurrence().subTerm()==getSubTerm()</code>
403: */
404: public Term getSubTerm() {
405: return currentSubTerm;
406: }
407:
408: public boolean hasNext() {
409: return currentPathIt != null;
410: }
411:
412: /**
413: * @return the number of the next child on the path, or
414: * <code>-1</code> if no further child exists
415: */
416: public int next() {
417: int res;
418:
419: if (currentSubTerm == null)
420: currentSubTerm = cfma.formula();
421: else
422: currentSubTerm = currentSubTerm.sub(child);
423:
424: if (currentPathIt.hasNext())
425: res = currentPathIt.next();
426: else if (!belowMetavariable
427: && termBelowMetavariable() != null) {
428: belowMetavariable = true;
429: currentPathIt = posInTermBelowMetavariable().iterator();
430: currentSubTerm = termBelowMetavariable();
431:
432: if (currentPathIt.hasNext())
433: res = currentPathIt.next();
434: else {
435: res = -1;
436: currentPathIt = null;
437: }
438: } else {
439: res = -1;
440: currentPathIt = null;
441: }
442:
443: child = res;
444: ++count;
445: return res;
446: }
447: }
448:
449: }
|