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: /** this class describes a position in a term
012: */package de.uka.ilkd.key.logic;
013:
014: import de.uka.ilkd.key.util.Debug;
015:
016: public class PosInTerm {
017:
018: /** top level term position */
019: public static final PosInTerm TOP_LEVEL = new PosInTerm();
020:
021: private final PosInTerm prev;
022:
023: /**
024: * the position number
025: */
026: private final int pos;
027:
028: /**
029: * the depth
030: */
031: private final int depth;
032:
033: private final int hashCode;
034:
035: /**
036: * iterator cache
037: */
038: private int[] cache;
039:
040: private PosInTerm(PosInTerm pit, int posNr) {
041: prev = pit;
042: pos = posNr;
043: depth = pit.depth + 1;
044: hashCode = prev.hashCode * 715 + pos;
045: }
046:
047: /**
048: * creates a new PosInTerm
049: * position.
050: */
051: private PosInTerm() {
052: pos = -1;
053: prev = null;
054: depth = 0;
055: hashCode = 13;
056: }
057:
058: /** size of the position list */
059: public int depth() {
060: return depth;
061: }
062:
063: /** descending downwards choosing the n'th subterm, subformula
064: * @param n int describs the chosen subterm
065: * @return Position like old Position but with a deeper
066: * subterm.
067: */
068: public PosInTerm down(int n) {
069: return new PosInTerm(this , n);
070: }
071:
072: public PosInTerm up() {
073: return prev;
074: }
075:
076: /**
077: * @return the number/index of the deepest subterm that this
078: * <code>PosInTerm</code> points to. If the position is top-level,
079: * the result will be <code>-1</code>
080: */
081: public int getIndex() {
082: return pos;
083: }
084:
085: /**
086: * compares this PosInTerm with another PosInTerm
087: * and returns true if both describe the same position
088: */
089: public boolean equals(Object obj) {
090: if (this == obj)
091: return true;
092:
093: if (!(obj instanceof PosInTerm)) {
094: return false;
095: }
096:
097: PosInTerm cmp = (PosInTerm) obj;
098:
099: if (depth != cmp.depth) {
100: return false;
101: }
102:
103: PosInTerm this PIT = this ;
104:
105: while (this PIT != TOP_LEVEL) {
106: if (this PIT.pos != cmp.pos)
107: return false;
108: this PIT = this PIT.prev;
109: cmp = cmp.prev;
110: if (this PIT == cmp)
111: return true;
112: }
113:
114: return true;
115: }
116:
117: /**
118: * get subterm/-formula information. A PosInTerm defining the xn'th
119: * subterm of the x(n-1)'th subterm of ... of the x1'th subterm of a
120: * term returns an iterator subsequently resulting in the list xn...x1.
121: * @return IteratorOfInteger that iterates through the subterms
122: * of a sequent in the reverse order as the PosInTerm has been defined.
123: */
124: public IntIterator reverseIterator() {
125: return new PosIntIterator(this );
126: }
127:
128: /**
129: * returns an iterator defining the position in a term according to
130: * subterm relation. A PosInTerm defining the xn'th subterm of the
131: * x(n-1)'th subterm of ... of the x1'th subterm of a term returns an
132: * iterator subsequently resulting in the list x1...xn.
133: * @return an iterator over the list defining the position in a term.
134: */
135: public IntIterator iterator() {
136: if (cache == null)
137: fillCache();
138: return new PosArrayIntIterator(cache);
139: }
140:
141: private void fillCache() {
142: cache = new int[depth];
143:
144: IntIterator it = reverseIterator();
145: int at = depth - 1;
146:
147: while (it.hasNext()) {
148: cache[at] = it.next();
149: at--;
150: }
151: }
152:
153: public static PosInTerm parseReverseString(String s) {
154: PosInTerm result = TOP_LEVEL;
155: if ("".equals(s)) {
156: return result;
157: }
158: ListOfInteger list = SLListOfInteger.EMPTY_LIST;
159: java.util.StringTokenizer tker = new java.util.StringTokenizer(
160: s, ",", false);
161: while (tker.hasMoreTokens())
162: list = list.prepend(Integer.decode(tker.nextToken()));
163:
164: IteratorOfInteger it = list.iterator();
165: while (it.hasNext()) {
166: result = new PosInTerm(result, it.next().intValue());
167: }
168:
169: return result;
170: }
171:
172: public String integerList(IntIterator it) {
173: String list = "[";
174: while (it.hasNext()) {
175: list += "" + it.next();
176: if (it.hasNext()) {
177: list += ",";
178: }
179: }
180: list += "]";
181: return list;
182: }
183:
184: public String toString() {
185: if (this == TOP_LEVEL) {
186: return "top level";
187: }
188:
189: return "subterm: " + integerList(iterator());
190: }
191:
192: private static class PosIntIterator implements IntIterator {
193: private PosInTerm p;
194:
195: public PosIntIterator(PosInTerm p) {
196: this .p = p;
197: }
198:
199: public boolean hasNext() {
200: return p != null && p != TOP_LEVEL;
201: }
202:
203: public int next() {
204: Debug.assertTrue(p != TOP_LEVEL && p != null);
205: int result = p.pos;
206: p = p.prev;
207: return result;
208: }
209: }
210:
211: private static class PosArrayIntIterator implements IntIterator {
212: private int[] pos;
213: private int next;
214:
215: public PosArrayIntIterator(int[] pos) {
216: this .pos = pos;
217: next = 0;
218:
219: }
220:
221: public boolean hasNext() {
222: return next < pos.length;
223: }
224:
225: public int next() {
226: next++;
227: return pos[next - 1];
228: }
229: }
230:
231: public int hashCode() {
232: return hashCode;
233: }
234: }
|