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.java.JavaNonTerminalProgramElement;
014: import de.uka.ilkd.key.java.NonTerminalProgramElement;
015: import de.uka.ilkd.key.java.ProgramElement;
016: import de.uka.ilkd.key.util.Debug;
017:
018: /**
019: * this class describes the position of a statement in a program.
020: */
021: public class PosInProgram {
022:
023: /** pos at the beginning of the program */
024: public static final PosInProgram TOP = new PosInProgram();
025:
026: private final PosInProgram prev;
027:
028: /**
029: * the position number
030: */
031: private final int pos;
032:
033: /**
034: * the depth
035: */
036: private final int depth;
037:
038: /**
039: * caches iterator for performance reasons
040: */
041: private int[] cache;
042:
043: private final int hashCode;
044:
045: /**
046: * returns the ProgramElement at the given position
047: * @param pos the PosInProgram
048: * @param prg the ProgramElement we walk through
049: * @return the ProgramElement at the given position
050: * @throws IndexOutOfBoundsException if the given position
051: * refers to a non-existant program
052: */
053: public static ProgramElement getProgramAt(PosInProgram pos,
054: ProgramElement prg) {
055: ProgramElement result = prg;
056: final IntIterator it = pos.iterator();
057: while (it.hasNext()) {
058: if (!(result instanceof NonTerminalProgramElement)) {
059: throw new IndexOutOfBoundsException(
060: "PosInProgram is invalid.");
061: }
062: // getchild at throws an array index out of bound if
063: // it.next refers to a non-existing child
064: result = ((JavaNonTerminalProgramElement) result)
065: .getChildAt(it.next());
066: }
067: return result;
068: }
069:
070: /**
071: * creates a new program position
072: */
073: private PosInProgram(PosInProgram pip, int posNr) {
074: prev = pip;
075: pos = posNr;
076: depth = pip.depth + 1;
077: hashCode = prev.hashCode * 31 + pos;
078: }
079:
080: /**
081: * creates a new PosInProgram
082: * position.
083: */
084: private PosInProgram() {
085: pos = -1;
086: prev = null;
087: depth = 0;
088: hashCode = 17;
089: }
090:
091: /** size of the position list */
092: public int depth() {
093: return depth;
094: }
095:
096: /** descending downwards choosing the n'th statement of the program
097: * @param n the int describes the position of the statement in the block
098: * @return position of the statement
099: */
100: public PosInProgram down(int n) {
101: return new PosInProgram(this , n);
102: }
103:
104: /**
105: * ascends one AST level
106: *
107: */
108: public PosInProgram up() {
109: return this == TOP ? this : prev;
110: }
111:
112: public PosInProgram append(PosInProgram pp) {
113: return add(this , pp);
114: }
115:
116: public PosInProgram prepend(PosInProgram pp) {
117: return add(pp, this );
118: }
119:
120: private PosInProgram add(PosInProgram first, PosInProgram second) {
121: if (first == TOP) {
122: return second;
123: } else if (second == TOP) {
124: return first;
125: }
126:
127: PosInProgram result = first;
128: final IntIterator it = second.iterator();
129: while (it.hasNext()) {
130: result = new PosInProgram(result, it.next());
131: }
132: return result;
133: }
134:
135: /**
136: * compares this PosInProgram with another PosInProgram
137: * and returns true if both describe the same position
138: */
139: public boolean equals(Object obj) {
140: if (this == obj)
141: return true;
142:
143: if (!(obj instanceof PosInProgram)) {
144: return false;
145: }
146:
147: final PosInProgram cmp = (PosInProgram) obj;
148:
149: if (depth != cmp.depth) {
150: return false;
151: }
152:
153: final IntIterator it = reverseIterator();
154: final IntIterator cmpIt = cmp.reverseIterator();
155: while (it.hasNext()) {
156: if (it.next() != cmpIt.next()) {
157: return false;
158: }
159: }
160: return true;
161: }
162:
163: public boolean leq(PosInProgram pip) {
164: final IntIterator longerIt = iterator();
165: final IntIterator shorterIt = pip.iterator();
166:
167: while (shorterIt.hasNext() && longerIt.hasNext()) {
168: if (shorterIt.next() < longerIt.next()) {
169: return false;
170: }
171: }
172:
173: return true;
174: }
175:
176: /**
177: * returns an IteratorOfInteger that iterates through the subterms
178: * of a sequent in the reverse order as the PosInProgram has been defined.
179: * @return IteratorOfInteger that iterates through the subterms
180: * of a sequent in the reverse order as the PosInProgram has been defined.
181: */
182: public IntIterator reverseIterator() {
183: return new PosIntIterator(this );
184: }
185:
186: public int get(int i) {
187: if (i >= depth || i < 0) {
188: throw new ArrayIndexOutOfBoundsException();
189: }
190: if (cache != null) {
191: return cache[i];
192: }
193:
194: PosInProgram previous = this ;
195: int result = this .pos;
196:
197: for (int k = 0; k < depth - i; k++) {
198: result = previous.pos;
199: previous = previous.prev;
200: }
201:
202: return result;
203: }
204:
205: /**
206: * return the last index (or -1 if this == TOP)
207: */
208: public int last() {
209: return pos;
210: }
211:
212: public ProgramElement getProgram(ProgramElement pe) {
213: return getProgramAt(this , pe);
214: }
215:
216: /**
217: * returns an iterator over the list defining the position in a term.
218: * @return an iterator over the list defining the position in a term.
219: */
220: public IntIterator iterator() {
221: if (cache == null) {
222: fillCache();
223: }
224: return new PosArrayIntIterator(cache);
225: }
226:
227: private void fillCache() {
228: cache = new int[depth];
229: if (prev != null && prev.cache != null) {
230: System
231: .arraycopy(prev.cache, 0, cache, 0,
232: prev.cache.length);
233: cache[cache.length - 1] = pos;
234: } else {
235: final IntIterator it = reverseIterator();
236: int at = depth - 1;
237: while (it.hasNext()) {
238: cache[at] = it.next();
239: at--;
240: }
241: }
242: }
243:
244: /** toString */
245: public String toString() {
246: IntIterator it = iterator();
247: String list = "[";
248: while (it.hasNext()) {
249: list += "" + it.next();
250: if (it.hasNext()) {
251: list += ", ";
252: }
253: }
254: return "PosInProgram: " + list;
255: }
256:
257: static class PosIntIterator implements IntIterator {
258: private PosInProgram p;
259:
260: public PosIntIterator(PosInProgram p) {
261: this .p = p;
262: }
263:
264: public boolean hasNext() {
265: return p != null && p != TOP;
266: }
267:
268: public int next() {
269: Debug.assertTrue(p != TOP && p != null);
270: int result = p.pos;
271: p = p.prev;
272: return result;
273: }
274:
275: }
276:
277: static class PosArrayIntIterator implements IntIterator {
278: private final int[] pos;
279: private int next;
280:
281: public PosArrayIntIterator(int[] pos) {
282: this .pos = pos;
283: next = 0;
284:
285: }
286:
287: public boolean hasNext() {
288: return next < pos.length;
289: }
290:
291: public int next() {
292: next++;
293: return pos[next - 1];
294: }
295:
296: }
297:
298: public int hashCode() {
299: return hashCode;
300: }
301: }
|