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.pp;
012:
013: import de.uka.ilkd.key.logic.*;
014: import de.uka.ilkd.key.logic.op.Metavariable;
015:
016: /**
017: * A PositionTable describes the start and end positions of substrings
018: * of a String in order to get a PosInSequent from an int describing a
019: * position in a string representing a Term or a Sequent, etc. A
020: * PositionTable therefore represents a table consisting of two
021: * columns of type int (start and end position) and a reference to
022: * another PositionTable representing the position information for
023: * that substring. A PositionTable is valid (in order to support
024: * efficient putting of new entries to the table and an efficient
025: * search for a Position), if the last entry that has been set is (s,
026: * e, x) and the next entry is (s', e', x') with s'>e.
027: *
028: * <p>Positions are reckoned with start positions inclusive and
029: * end positions exclusive. Start and end positions are relative
030: * to each subterm.
031: */
032: public class PositionTable {
033:
034: // the start positions of the direct subterms (or parts of sequent, etc.)
035: protected int[] startPos;
036:
037: //the end positions of the direct subterms (or parts of sequent, etc.)
038: protected int[] endPos;
039:
040: // the PositionTables for the direct subterms (or parts of sequent, etc.)
041: protected PositionTable[] child;
042:
043: // the entry number where the next entry in endPos will be set
044: private int currentEndEntry = 0;
045:
046: // the entry number where the next entry in startPos will be set
047: private int currentStartEntry = 0;
048:
049: // the number of rows in the above arrays. Equals the number of direct
050: // subterms (or parts of sequent, etc.)
051: private final int rows;
052:
053: /**
054: * creates a new PositionTable with the number of subterms (or number of
055: * ConstrainedFormula in a Semisequent, or the number of Semisequents in a
056: * Sequent, etc.)
057: * @param rows the number of direct sub-elements in the term whose
058: * position information is represented by the constructed object.
059: */
060: public PositionTable(int rows) {
061: this .rows = rows;
062: startPos = new int[rows];
063: endPos = new int[rows];
064: child = new PositionTable[rows];
065: for (int i = 0; i < rows; i++) {
066: startPos[i] = -1;
067: endPos[i] = -1;
068: child[i] = null;
069: }
070: }
071:
072: /**
073: * returns the m with startPos[m]<=index<=endPos[m].
074: * -1 if no such m exists.
075: */
076: private int searchEntry(int index) {
077:
078: //linear search:
079: for (int m = 0; m < rows; m++) {
080: if ((startPos[m] <= index) && (index < endPos[m])) {
081: return m;
082: }
083: }
084:
085: //binary search (ordered arrays are precondition!), NOT CHECKED SO FAR:
086: /* int l=0;
087: int r=rows-1;
088: int m;
089: while (r<l) {
090: m=(l+r)/2;
091: if ((startPos[m]<=index) && (endPos[m]>index)) {
092: return m;
093: }
094: if (index<startPos[m]) {
095: r=m;
096: } else {
097: l=m;
098: }
099: }*/
100: return -1;
101: }
102:
103: /**
104: * Returns the path to the `lowest' position table that includes
105: * <code>index</code> in its range.
106: */
107: protected ListOfInteger pathForIndex(int index) {
108: int sub = searchEntry(index);
109: if (sub == -1) {
110: return SLListOfInteger.EMPTY_LIST;
111: } else {
112: return child[sub].pathForIndex(index - startPos[sub])
113: .prepend(new Integer(sub));
114: }
115: }
116:
117: /**
118: * Returns the character range of the `lowest' subtable that
119: * includes <code>index</code> in its range.
120: * @param index the character index to search for.
121: * @param length the length of the whole string corresponding
122: * to this position table. Needed in case it
123: * turns out the index belongs to the top level.
124: */
125: public Range rangeForIndex(int index, int length) {
126: int sub = searchEntry(index);
127: if (sub == -1) {
128: return new Range(0, length);
129: } else {
130: Range r = child[sub].rangeForIndex(index - startPos[sub],
131: endPos[sub] - startPos[sub]);
132: r.start += startPos[sub];
133: r.end += startPos[sub];
134: return r;
135: }
136: }
137:
138: /**
139: * Returns the character range of the first java statement in a
140: * program modality for the `lowest' subtable that includes
141: * <code>index</code> in its range. If the lowest subtable
142: * does not correspond to a program modality, it returns null.
143: */
144: public Range firstStatementRangeForIndex(int index) {
145: int sub = searchEntry(index);
146: if (sub == -1) {
147: return getFirstStatementRange();
148: } else {
149: Range r = child[sub].firstStatementRangeForIndex(index
150: - startPos[sub]);
151: if (r != null) {
152: r.start += startPos[sub];
153: r.end += startPos[sub];
154: }
155: return r;
156: }
157: }
158:
159: /** Returns the character range of the first java statement in a
160: * program modality for <i>this</i>position table. If this
161: * is not a program modality, returns null. Note that this
162: * will be overridden in the subclass
163: * {@link ModalityPositionTable}.
164: */
165: public Range getFirstStatementRange() {
166: return null;
167: }
168:
169: /** Returns the character range for the subtable indicated
170: * by the given integer list.
171: */
172: public Range rangeForPath(ListOfInteger path, int length) {
173: if (path.isEmpty()) {
174: return new Range(0, length);
175: } else {
176: int sub = path.head().intValue();
177: Range r = child[sub].rangeForPath(path.tail(), endPos[sub]
178: - startPos[sub]);
179: r.start += startPos[sub];
180: r.end += startPos[sub];
181: return r;
182: }
183: }
184:
185: /**
186: * sets end in the position table to the next free end entry in the
187: * position
188: * table and sets the given PositionTable as child of the sub-element
189: * finished by putting this end position
190: * @param end char position that ends the sub-element started by the
191: * corresponding start entry in the position table
192: * @param child PositionTable for the sub-element from start to end
193: */
194: public void setEnd(int end, PositionTable child) {
195: endPos[currentEndEntry] = end;
196: this .child[currentEndEntry] = child;
197: currentEndEntry++;
198: }
199:
200: /**
201: * sets start in the position table to the next free start entry in the
202: * position table
203: * @param start char position that starts a sub-element
204: */
205: public void setStart(int start) {
206: startPos[currentStartEntry] = start;
207: currentStartEntry++;
208: }
209:
210: /**
211: * Return of the children of this PositionTable
212: */
213: public PositionTable getChild(int i) {
214:
215: return child[i];
216: }
217:
218: /**
219: * returns a String representation of the position table
220: */
221: public String toString() {
222: String result = "[";
223: for (int i = 0; i < rows; i++) {
224: result = result + "<" + startPos[i] + "," + endPos[i] + ","
225: + child[i] + ">";
226: if (rows - 1 != i)
227: result = result + ",";
228: }
229: return result + "]";
230: }
231:
232: /** Returns a PosInSequent for a given position list,
233: * but without filling in the bounds. It is assumed
234: * that this is a position table which has one child table for
235: * every formula in the printed sequent, and that
236: * <code>posList</code> begins which the number of the formula.
237: * The returned PosInSequent will refer to (a subterm of) one
238: * of the constrained formulae in the sequent.
239: * @param posList the position list that navigates through
240: * the position tables.
241: * @param filter the sequent print filter from that was used to
242: * print the sequent
243: */
244:
245: protected PosInSequent getSequentPIS(ListOfInteger posList,
246: SequentPrintFilter filter) {
247: int cfmaNo = posList.head().intValue();
248: ListOfInteger tail = posList.tail();
249:
250: SequentPrintFilterEntry filterEntry = getFilterEntry(cfmaNo,
251: filter);
252:
253: ConstrainedFormula cfma = filterEntry.getOriginalFormula();
254:
255: PosInOccurrence currentPos = new PosInOccurrence(cfma,
256: PosInTerm.TOP_LEVEL, filter.getSequent().antecedent()
257: .contains(cfma));
258:
259: return child[cfmaNo].getTermPIS(filterEntry, tail, currentPos);
260: }
261:
262: /** Returns a PosInSequent for a given position list, but without
263: * filling in the bounds. It is assumed that this is a position
264: * table corresponding to the Term <code>term</code>, which has
265: * one child table for each subterm.
266: * @param filterEntry the print filter entry that contains
267: * information about which constrained formula we
268: * are in and how the constraint and metavariables
269: * were printed.
270: * @param posList the position list that navigates through
271: * the position tables.
272: * @param pio the PosInOccurrence leading to the current term
273: */
274: private PosInSequent getTermPIS(
275: SequentPrintFilterEntry filterEntry, ListOfInteger posList,
276: PosInOccurrence pio) {
277: if (posList.isEmpty()) {
278: return PosInSequent.createCfmaPos(pio);
279: } else {
280: int subNo = posList.head().intValue();
281: PosInOccurrence subpio = pio.down(subNo);
282: Term subterm = subpio.subTerm();
283:
284: if (subpio.termBelowMetavariable() == null
285: && subterm.op() instanceof Metavariable) {
286: subpio = goInMetavariable((Metavariable) subterm.op(),
287: filterEntry, subpio);
288: }
289: return child[subNo].getTermPIS(filterEntry, posList.tail(),
290: subpio);
291: }
292: }
293:
294: /** Handles the special case for <code>getTermPIS()</code> when
295: * the position moves below a Metavariable. The SequentPrintFilter
296: * can replace Metavariables by their instantiation according to
297: * the user constraint. When the user selects a position
298: * inside such an instantiation, this needs to be recorded.
299: * @param mv a Metavariable
300: * @param filterEntry the print filter entry that contains
301: * information about which constrained formula we
302: * are in and how the constraint and metavariables
303: * were printed.
304: * @param pos the PosInOccurrence leading to the meta variable
305: * @returns the PosInOccurrence with the added information that
306: * we are inside a MV instantiation.
307: */
308: private PosInOccurrence goInMetavariable(Metavariable mv,
309: SequentPrintFilterEntry filterEntry, PosInOccurrence pos) {
310: Term t = filterEntry.getDisplayConstraint()
311: .getInstantiation(mv);
312: if (t.op() != mv) {
313: return pos.setTermBelowMetavariable(t);
314: } else {
315: return pos;
316: }
317: }
318:
319: private static SequentPrintFilterEntry getFilterEntry(int cfmaNo,
320: SequentPrintFilter filter) {
321: int i = cfmaNo;
322: ListOfSequentPrintFilterEntry list = filter.getAntec().append(
323: filter.getSucc());
324: while (i-- != 0)
325: list = list.tail();
326: return list.head();
327: }
328:
329: }
|