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.proof;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.rule.ListOfNoPosTacletApp;
016: import de.uka.ilkd.key.rule.ListOfTacletApp;
017:
018: /**
019: * This class holds <code>TermTacletAppIndex</code>s for all formulas of
020: * a semisequent.
021: */
022: public class SemisequentTacletAppIndex {
023: private MapFromConstrainedFormulaToTermTacletAppIndex termIndices = MapAsListFromConstrainedFormulaToTermTacletAppIndex.EMPTY_MAP;
024:
025: private TermTacletAppIndexCacheSet indexCaches;
026:
027: private final RuleFilter ruleFilter;
028:
029: private final Sequent seq;
030: private final boolean antec;
031:
032: /**
033: * Add indices for the given formulas to the map
034: * <code>termIndices</code>. Existing entries are replaced with
035: * the new indices.
036: * Note: destructive, use only when constructing new index
037: */
038: private void addTermIndices(ListOfConstrainedFormula cfmas,
039: Sequent s, Services services, Constraint userConstraint,
040: TacletIndex tacletIndex, NewRuleListener listener) {
041: while (cfmas != SLListOfConstrainedFormula.EMPTY_LIST) {
042: final ConstrainedFormula cfma = cfmas.head();
043: cfmas = cfmas.tail();
044: addTermIndex(cfma, s, services, userConstraint,
045: tacletIndex, listener);
046: }
047: }
048:
049: /**
050: * Add an index for the given formula to the map
051: * <code>termIndices</code>. An existing entry is replaced with
052: * the new one.
053: * Note: destructive, use only when constructing new index
054: */
055: private void addTermIndex(ConstrainedFormula cfma, Sequent s,
056: Services services, Constraint userConstraint,
057: TacletIndex tacletIndex, NewRuleListener listener) {
058: final PosInOccurrence pos = new PosInOccurrence(cfma,
059: PosInTerm.TOP_LEVEL, antec);
060:
061: termIndices = termIndices.put(cfma, TermTacletAppIndex.create(
062: pos, services, userConstraint, tacletIndex, listener,
063: ruleFilter, indexCaches));
064: }
065:
066: /**
067: * Update the index for the given formula, which is supposed to be an
068: * element of the map <code>termIndices</code>, by adding the taclets that
069: * are selected by <code>filter</code>
070: * Note: destructive, use only when constructing new index
071: */
072: private void addTaclets(RuleFilter filter, ConstrainedFormula cfma,
073: Sequent s, Services services, Constraint userConstraint,
074: TacletIndex tacletIndex, NewRuleListener listener) {
075: final TermTacletAppIndex oldIndex = termIndices.get(cfma);
076: assert oldIndex != null : "Term index that is supposed to be updated "
077: + "does not exist";
078:
079: final PosInOccurrence pos = new PosInOccurrence(cfma,
080: PosInTerm.TOP_LEVEL, antec);
081:
082: termIndices = termIndices.put(cfma, oldIndex.addTaclets(filter,
083: pos, services, userConstraint, tacletIndex, listener));
084: }
085:
086: /**
087: * Remove the indices for the given formulas from the map
088: * <code>termIndices</code>.
089: * Note: destructive, use only when constructing new index
090: */
091: private void removeTermIndices(ListOfConstrainedFormula cfmas) {
092: final IteratorOfConstrainedFormula it = cfmas.iterator();
093: while (it.hasNext())
094: removeTermIndex(it.next());
095: }
096:
097: /**
098: * Remove the index for the given formula from the map
099: * <code>termIndices</code>.
100: * Note: destructive, use only when constructing new index
101: */
102: private void removeTermIndex(ConstrainedFormula cfma) {
103: termIndices = termIndices.remove(cfma);
104: }
105:
106: /**
107: * Remove the formulas that are listed as modified by
108: * <code>infos</code>
109: * @return the old indices in the same order as the list
110: * <code>infos</code>
111: * Note: destructive, use only when constructing new index
112: */
113: private ListOfTermTacletAppIndex removeFormulas(
114: ListOfFormulaChangeInfo infos) {
115:
116: ListOfTermTacletAppIndex oldIndices = SLListOfTermTacletAppIndex.EMPTY_LIST;
117:
118: final IteratorOfFormulaChangeInfo infoIt = infos.iterator();
119:
120: while (infoIt.hasNext()) {
121: final FormulaChangeInfo info = infoIt.next();
122: final ConstrainedFormula oldFor = info.getOriginalFormula();
123: final ConstrainedFormula newFor = info.getNewFormula();
124:
125: TermTacletAppIndex oldIndex;
126:
127: if (oldFor.constraint().equals(newFor.constraint())) {
128: oldIndex = termIndices.get(oldFor);
129: } else {
130: // modified constraint, thus we have to rebuild the whole term
131: // index
132: oldIndex = null;
133: }
134: oldIndices = oldIndices.prepend(oldIndex);
135: termIndices = termIndices.remove(oldFor);
136: }
137:
138: return oldIndices.reverse();
139: }
140:
141: /**
142: * Update the given list of term indices according to the list
143: * <code>infos</code> of modification information. Both lists have
144: * to be compatible, i.e. same length and same order. The new
145: * indices are inserted in the map <code>termIndices</code>.
146: * Note: destructive, use only when constructing new index
147: */
148: private void updateTermIndices(ListOfTermTacletAppIndex oldIndices,
149: ListOfFormulaChangeInfo infos, Sequent newSeq,
150: Services services, Constraint userConstraint,
151: TacletIndex tacletIndex, NewRuleListener listener) {
152:
153: final IteratorOfFormulaChangeInfo infoIt = infos.iterator();
154: final IteratorOfTermTacletAppIndex oldIndexIt = oldIndices
155: .iterator();
156:
157: while (infoIt.hasNext()) {
158: final FormulaChangeInfo info = infoIt.next();
159: final ConstrainedFormula newFor = info.getNewFormula();
160: final TermTacletAppIndex oldIndex = oldIndexIt.next();
161:
162: if (oldIndex == null)
163: // completely rebuild the term index
164: addTermIndex(newFor, newSeq, services, userConstraint,
165: tacletIndex, listener);
166: else {
167: final PosInOccurrence oldPos = info
168: .getPositionOfModification();
169: final PosInOccurrence newPos = oldPos
170: .replaceConstrainedFormula(newFor);
171: termIndices = termIndices.put(newFor, oldIndex.update(
172: newPos, services, userConstraint, tacletIndex,
173: listener, indexCaches));
174: }
175: }
176: }
177:
178: private void updateTermIndices(ListOfFormulaChangeInfo infos,
179: Sequent newSeq, Services services,
180: Constraint userConstraint, TacletIndex tacletIndex,
181: NewRuleListener listener) {
182:
183: // remove original indices
184: final ListOfTermTacletAppIndex oldIndices = removeFormulas(infos);
185:
186: updateTermIndices(oldIndices, infos, newSeq, services,
187: userConstraint, tacletIndex, listener);
188: }
189:
190: /**
191: * Create an index object for the semisequent determined by
192: * <code>s</code> and <code>antec</code> that contains term
193: * indices for each formula.
194: * @param antec iff true create an index for the antecedent of
195: * <code>s</code>, otherwise for the succedent
196: */
197: public SemisequentTacletAppIndex(Sequent s, boolean antec,
198: Services services, Constraint userConstraint,
199: TacletIndex tacletIndex, NewRuleListener listener,
200: RuleFilter ruleFilter,
201: TermTacletAppIndexCacheSet indexCaches) {
202: this .seq = s;
203: this .antec = antec;
204: this .ruleFilter = ruleFilter;
205: this .indexCaches = indexCaches;
206: addTermIndices((antec ? s.antecedent() : s.succedent())
207: .toList(), s, services, userConstraint, tacletIndex,
208: listener);
209: }
210:
211: private SemisequentTacletAppIndex(SemisequentTacletAppIndex orig) {
212: this .seq = orig.seq;
213: this .antec = orig.antec;
214: this .ruleFilter = orig.ruleFilter;
215: this .termIndices = orig.termIndices;
216: this .indexCaches = orig.indexCaches;
217: }
218:
219: public SemisequentTacletAppIndex copy() {
220: return new SemisequentTacletAppIndex(this );
221: }
222:
223: /**
224: * Get term index for the formula to which position <code>pos</code> points
225: */
226: private TermTacletAppIndex getTermIndex(PosInOccurrence pos) {
227: return termIndices.get(pos.constrainedFormula());
228: }
229:
230: /**
231: * @return all taclet apps for the given position
232: */
233: public ListOfNoPosTacletApp getTacletAppAt(PosInOccurrence pos,
234: RuleFilter filter) {
235: return getTermIndex(pos).getTacletAppAt(pos, filter);
236: }
237:
238: /**
239: * @return all taclet apps for or below the given position
240: */
241: public ListOfTacletApp getTacletAppAtAndBelow(PosInOccurrence pos,
242: RuleFilter filter) {
243: return getTermIndex(pos).getTacletAppAtAndBelow(pos, filter);
244: }
245:
246: /**
247: * called if a formula has been replaced
248: * @param sci SequentChangeInfo describing the change of the sequent
249: */
250: public SemisequentTacletAppIndex sequentChanged(
251: SequentChangeInfo sci, Services services,
252: Constraint userConstraint, TacletIndex tacletIndex,
253: NewRuleListener listener) {
254: if (sci.hasChanged(antec)) {
255: final SemisequentTacletAppIndex result = copy();
256: result.removeTermIndices(sci.removedFormulas(antec));
257: result.updateTermIndices(sci.modifiedFormulas(antec), sci
258: .sequent(), services, userConstraint, tacletIndex,
259: listener);
260: result.addTermIndices(sci.addedFormulas(antec), sci
261: .sequent(), services, userConstraint, tacletIndex,
262: listener);
263: return result;
264: }
265:
266: return this ;
267: }
268:
269: /**
270: * Create an index that additionally contains the taclets that are selected
271: * by <code>filter</code>
272: * @param filter The taclets that are supposed to be added
273: */
274: public SemisequentTacletAppIndex addTaclets(RuleFilter filter,
275: Sequent s, Services services, Constraint userConstraint,
276: TacletIndex tacletIndex, NewRuleListener listener) {
277: final SemisequentTacletAppIndex result = copy();
278: final IteratorOfConstrainedFormula it = termIndices
279: .keyIterator();
280:
281: while (it.hasNext())
282: result.addTaclets(filter, it.next(), s, services,
283: userConstraint, tacletIndex, listener);
284:
285: return result;
286: }
287:
288: /**
289: * Reports all cached rule apps.
290: * Calls ruleAdded on the given NewRuleListener for
291: * every cached taclet app.
292: */
293: public void reportRuleApps(NewRuleListener l) {
294: final IteratorOfEntryOfConstrainedFormulaAndTermTacletAppIndex it = termIndices
295: .entryIterator();
296:
297: while (it.hasNext()) {
298: final EntryOfConstrainedFormulaAndTermTacletAppIndex entry = it
299: .next();
300: final ConstrainedFormula cfma = entry.key();
301: final TermTacletAppIndex index = entry.value();
302: final PosInOccurrence pio = new PosInOccurrence(cfma,
303: PosInTerm.TOP_LEVEL, antec);
304:
305: index.reportTacletApps(pio, l);
306: }
307: }
308:
309: public void setIndexCache(TermTacletAppIndexCacheSet indexCaches) {
310: this.indexCaches = indexCaches;
311: }
312: }
|