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: import de.uka.ilkd.key.util.Debug;
016:
017: /**
018: * An InitialPositionTable is a PositionTable that describes the
019: * beginning of the element/subelement relationship. Thus, an
020: * InitialPositionTable describes the information on where the
021: * semisequents of a sequent are located. It is the root of the tree of
022: * PositionTables and may be asked for a PosInSequent for a given index
023: * position and a given Sequent.
024: *
025: * <p>For simplicity, the an InitialPositionTable has only one row.
026: * The various constrained formulae of a sequent are located
027: * one level below. In other words the whole sequent is not
028: * represented by an empty position list but by the list [0].
029: */
030: public class InitialPositionTable extends PositionTable {
031:
032: private ListOfRange updateRanges = SLListOfRange.EMPTY_LIST;
033:
034: /**
035: * creates a new Initial PositionTable.
036: */
037: public InitialPositionTable() {
038: super (1);
039: }
040:
041: /**
042: * Returns the PosInSequent for a given char position in a
043: * sequent.
044: * @param index the char position that points to the wanted
045: * position in sequent
046: * @param filter the sequent print filter from that was used to
047: * print the sequent
048: *
049: */
050: public PosInSequent getPosInSequent(int index,
051: SequentPrintFilter filter) {
052: if (index < startPos[0] || index >= endPos[0]) {
053: return null;
054: }
055:
056: ListOfInteger posList = pathForIndex(index);
057:
058: PosInSequent pis = getTopPIS(posList, filter);
059:
060: Range r = rangeForIndex(index);
061: pis.setBounds(r);
062: Range firstStatement = firstStatementRangeForIndex(index);
063: if (firstStatement != null) {
064: pis.setFirstJavaStatementRange(firstStatement);
065: }
066: return pis;
067: }
068:
069: /** Returns a PosInSequent for a given position list,
070: * but without filling in the bounds. It is assumed
071: * that this is the top level position table for a sequent.
072: * @param posList the position list that navigates through
073: * the position tables.
074: * @param filter the sequent print filter from that was used to
075: * print the sequent
076: */
077: private PosInSequent getTopPIS(ListOfInteger posList,
078: SequentPrintFilter filter) {
079: if (posList.isEmpty() || posList.tail().isEmpty()) {
080: return PosInSequent.createSequentPos();
081: } else {
082: return child[0].getSequentPIS(posList.tail(), filter);
083: }
084: }
085:
086: /** Returns the path for a given PosInOccurrence. This is
087: * built up from the initial 0, the number of the
088: * ConstrainedFormula in the sequent, the position in the
089: * constrained formula, and possibly inside a Metavariable
090: * instantiation. */
091: public ListOfInteger pathForPosition(PosInOccurrence pio,
092: SequentPrintFilter filter) {
093: ListOfInteger p = SLListOfInteger.EMPTY_LIST;
094:
095: p = prependPathBelowMV(p, pio, entryForCfma(pio
096: .constrainedFormula(), filter));
097: p = prependPathInFormula(p, pio);
098: p = p.prepend(new Integer(indexOfCfma(pio.constrainedFormula(),
099: filter)));
100: p = p.prepend(new Integer(0));
101: return p;
102: }
103:
104: private ListOfInteger prependPathBelowMV(ListOfInteger p,
105: PosInOccurrence pio, SequentPrintFilterEntry entry) {
106: if (pio.posInTermBelowMetavariable() == null
107: || !checkCompatibleDisplayConstraint(pio, entry))
108: return p;
109:
110: IntIterator pit = pio.posInTermBelowMetavariable()
111: .reverseIterator();
112: while (pit.hasNext()) {
113: p = p.prepend(new Integer(pit.next()));
114: }
115:
116: return p;
117: }
118:
119: /**
120: * Check that the term below the metavariable (as determined by the position
121: * <code> pio </code> is compatible with the display constraint, i.e. with
122: * the constraint that governs the shape of the current formula as
123: * displayed. As it is possible to modify the user constraint arbitrarily,
124: * this is not necessarily the case.
125: *
126: * @return true iff the display constraint is compatible with
127: * <code>pio</code>
128: */
129: private boolean checkCompatibleDisplayConstraint(
130: PosInOccurrence pio, SequentPrintFilterEntry entry) {
131: final Term mvTerm = pio.constrainedFormula().formula().subAt(
132: pio.posInTerm());
133: Debug.assertTrue(mvTerm.op() instanceof Metavariable);
134: final Metavariable mv = (Metavariable) mvTerm.op();
135:
136: // The display constraint, joined with the statement that the focussed
137: // metavariable is instantiated with the mounted term.
138: final Constraint c = entry.getDisplayConstraint().unify(mvTerm,
139: pio.termBelowMetavariable(), null);
140: if (!c.isSatisfiable())
141: return false;
142:
143: // the term that is displayed instead of the metavariable
144: final Term displayedTerm = entry.getDisplayConstraint()
145: .getInstantiation(mv);
146: // the term that ought to be displayed according to the term position
147: final Term posTerm = c.getInstantiation(mv);
148:
149: return posTerm.equals(displayedTerm);
150: }
151:
152: private ListOfInteger prependPathInFormula(ListOfInteger p,
153: PosInOccurrence pio) {
154: IntIterator pit = pio.posInTerm().reverseIterator();
155: while (pit.hasNext()) {
156: p = p.prepend(new Integer(pit.next()));
157: }
158: return p;
159: }
160:
161: /** Returns the index of the constrained formula in the sequent
162: * as printed. */
163: private int indexOfCfma(ConstrainedFormula cfma,
164: SequentPrintFilter filter) {
165: ListOfSequentPrintFilterEntry list = filter.getAntec().append(
166: filter.getSucc());
167: int k;
168: for (k = 0; !list.isEmpty(); k++, list = list.tail()) {
169: if (list.head().getOriginalFormula() == cfma) {
170: return k;
171: }
172: }
173: return -1;
174: }
175:
176: /**
177: * Returns the <code>SequentPrintFilterEntry</code> for the given
178: * constrained formula from the <code>filter</code>.
179: */
180: private SequentPrintFilterEntry entryForCfma(
181: ConstrainedFormula cfma, SequentPrintFilter filter) {
182: ListOfSequentPrintFilterEntry list = filter.getAntec().append(
183: filter.getSucc());
184: int k;
185: for (k = 0; !list.isEmpty(); k++, list = list.tail()) {
186: if (list.head().getOriginalFormula() == cfma) {
187: return list.head();
188: }
189: }
190: return null;
191: }
192:
193: /**
194: * Returns the character range of the `lowest' subtable that
195: * includes <code>index</code> in its range.
196: * @param index the character index to search for.
197: */
198: public Range rangeForIndex(int index) {
199: return rangeForIndex(index, endPos[0]);
200: }
201:
202: /** Returns the character range for the subtable indicated
203: * by the given integer list.
204: */
205: public Range rangeForPath(ListOfInteger path) {
206: return rangeForPath(path, endPos[0]);
207: }
208:
209: public void addUpdateRange(Range r) {
210: updateRanges = updateRanges.prepend(r);
211: }
212:
213: public Range[] getUpdateRanges() {
214: return updateRanges.toArray();
215: }
216:
217: }
|