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.logic.op.IUpdateOperator;
016: import de.uka.ilkd.key.logic.op.Metavariable;
017: import de.uka.ilkd.key.logic.op.Modality;
018: import de.uka.ilkd.key.logic.op.Op;
019: import de.uka.ilkd.key.logic.op.Operator;
020: import de.uka.ilkd.key.pp.ConstraintSequentPrintFilter;
021: import de.uka.ilkd.key.rule.*;
022: import de.uka.ilkd.key.util.Debug;
023:
024: /**
025: * Class whose objects represent an index of taclet apps for one particular
026: * position within a formula, and that also contain references to the indices of
027: * direct subformulas
028: */
029: public class TermTacletAppIndex {
030: /** the term for which NoPosTacletApps are kept in this index node */
031: private final Term term;
032: /** NoPosTacletApps for this term */
033: private final ListOfNoPosTacletApp localTacletApps;
034: /** indices for subterms */
035: private final ListOfTermTacletAppIndex subtermIndices;
036: /** the constraint that is used to extend the considered term below
037: * metavariables */
038: private final Constraint displayConstraint;
039: /** */
040: private final RuleFilter ruleFilter;
041:
042: /**
043: * Create a TermTacletAppIndex
044: */
045: private TermTacletAppIndex(Term term,
046: ListOfNoPosTacletApp localTacletApps,
047: ListOfTermTacletAppIndex subtermIndices,
048: Constraint displayConstraint, RuleFilter ruleFilter) {
049: this .term = term;
050: this .subtermIndices = subtermIndices;
051: this .localTacletApps = localTacletApps;
052: this .displayConstraint = displayConstraint;
053: this .ruleFilter = ruleFilter;
054: }
055:
056: private TermTacletAppIndex getSubIndex(int subterm) {
057: return subtermIndices.take(subterm).head();
058: }
059:
060: /**
061: * collects all RewriteTacletInstantiations for the given
062: * heuristics in a subterm of the constrainedFormula described by a
063: * PosInOccurrence
064: * @param pos the PosInOccurrence to focus
065: * @param services the Services object encapsulating information
066: * about the java datastructures like (static)types etc.
067: * @return list of all possible instantiations
068: */
069: private static ListOfNoPosTacletApp getRewriteTaclet(
070: PosInOccurrence pos, RuleFilter filter, Services services,
071: Constraint userConstraint, TacletIndex tacletIndex) {
072:
073: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
074:
075: Constraint c = pos.constrainedFormula().constraint();
076:
077: if (pos.termBelowMetavariable() != null) {
078: c = c.unify(pos.constrainedFormula().formula().subAt(
079: pos.posInTerm()), pos.termBelowMetavariable(),
080: services);
081: if (!c.isSatisfiable())
082: return SLListOfNoPosTacletApp.EMPTY_LIST;
083: }
084:
085: final IteratorOfNoPosTacletApp rewriteIterator = tacletIndex
086: .getRewriteTaclet(pos, c, filter, services,
087: userConstraint).iterator();
088:
089: while (rewriteIterator.hasNext()) {
090: NoPosTacletApp tacletApp = rewriteIterator.next();
091: result = result.prepend(tacletApp);
092: }
093:
094: return result;
095: }
096:
097: /**
098: * collects all FindTaclets with instantiations for the given
099: * heuristics and position
100: * @param pos the PosInOccurrence to focus
101: * @param services the Services object encapsulating information
102: * about the java datastructures like (static)types etc.
103: * @return list of all possible instantiations
104: */
105: private static ListOfNoPosTacletApp getFindTaclet(
106: PosInOccurrence pos, RuleFilter filter, Services services,
107: Constraint userConstraint, TacletIndex tacletIndex) {
108: ListOfNoPosTacletApp tacletInsts = SLListOfNoPosTacletApp.EMPTY_LIST;
109: if (pos.isTopLevel()) {
110: if (pos.isInAntec()) {
111: tacletInsts = tacletInsts.prepend(antecTaclet(pos,
112: filter, services, userConstraint, tacletIndex));
113: } else {
114: tacletInsts = tacletInsts.prepend(succTaclet(pos,
115: filter, services, userConstraint, tacletIndex));
116: }
117: } else {
118: tacletInsts = tacletInsts.prepend(getRewriteTaclet(pos,
119: filter, services, userConstraint, tacletIndex));
120: }
121: return tacletInsts;
122: }
123:
124: /**
125: * collects all AntecedentTaclet instantiations for the given
126: * heuristics and ConstrainedFormula
127: * @param pos the PosInOccurrence of the ConstrainedFormula
128: * the taclets have to be connected to
129: * (pos must point to the top level formula, i.e. <tt>pos.isTopLevel()</tt> must be true)
130: * @param services the Services object encapsulating information
131: * about the java datastructures like (static)types etc.
132: * @return list of all possible instantiations
133: */
134: private static ListOfNoPosTacletApp antecTaclet(
135: PosInOccurrence pos, RuleFilter filter, Services services,
136: Constraint userConstraint, TacletIndex tacletIndex) {
137: return tacletIndex.getAntecedentTaclet(pos, filter, services,
138: userConstraint);
139: }
140:
141: /**
142: * collects all SuccedentTaclet instantiations for the given
143: * heuristics and ConstrainedFormula
144: * @param pos the PosInOccurrence of the ConstrainedFormula
145: * the taclets have to be connected to
146: * (pos must point to the top level formula,
147: * i.e. <tt>pos.isTopLevel()</tt> must be true)
148: * @param services the Services object encapsulating information
149: * about the java datastructures like (static)types etc.
150: * @return list of all possible instantiations
151: */
152: private static ListOfNoPosTacletApp succTaclet(PosInOccurrence pos,
153: RuleFilter filter, Services services,
154: Constraint userConstraint, TacletIndex tacletIndex) {
155: return tacletIndex.getSuccedentTaclet(pos, filter, services,
156: userConstraint);
157: }
158:
159: /**
160: * Check whether the given term is a metavariable, and replace it
161: * with a concrete term provided that such a term is determined by
162: * the user constraint
163: * @return A <code>PosInOccurrence</code> object in which
164: * eventually the metavariable has been replaced with a term as
165: * given by the user constraint. In any case the object points to
166: * the same position of a term as the <code>pos</code> parameter
167: */
168: private static PosInOccurrence handleDisplayConstraint(
169: PosInOccurrence pos, Constraint displayConstraint) {
170:
171: final Term localTerm = pos.subTerm();
172:
173: final Operator op = localTerm.op();
174: if (op instanceof Metavariable) {
175: if (pos.termBelowMetavariable() == null) {
176: final Term metaTerm = displayConstraint
177: .getInstantiation((Metavariable) op);
178: if (metaTerm.op() != op)
179: return pos.setTermBelowMetavariable(metaTerm);
180: }
181: }
182:
183: return pos;
184: }
185:
186: /**
187: * Descend and create indices for each of the direct subterms of
188: * the given term
189: * @param pos pointer to the term/formula for whose subterms
190: * indices are to be created
191: * @return list of the index objects
192: */
193: private static ListOfTermTacletAppIndex createSubIndices(
194: PosInOccurrence pos, Services services,
195: Constraint userConstraint, Constraint displayConstraint,
196: TacletIndex tacletIndex, NewRuleListener listener,
197: RuleFilter filter, ITermTacletAppIndexCache indexCache) {
198: ListOfTermTacletAppIndex result = SLListOfTermTacletAppIndex.EMPTY_LIST;
199: final Term localTerm = pos.subTerm();
200:
201: int i = localTerm.arity();
202:
203: while (i-- != 0)
204: result = result
205: .prepend(createHelp(pos.down(i), services,
206: userConstraint, displayConstraint,
207: tacletIndex, listener, filter, indexCache
208: .descend(localTerm, i)));
209:
210: return result;
211: }
212:
213: /**
214: * Create an index for the given term
215: *
216: * @param pos
217: * Pointer to the term/formula for which an index is to be
218: * created. <code>pos</code> has to be a top-level term
219: * position
220: * @return the index object
221: */
222: public static TermTacletAppIndex create(PosInOccurrence pos,
223: Services services, Constraint userConstraint,
224: TacletIndex tacletIndex, NewRuleListener listener,
225: RuleFilter filter, TermTacletAppIndexCacheSet indexCaches) {
226: Debug.assertTrue(pos.isTopLevel(),
227: "Someone tried to create a term index for a real "
228: + "subterm");
229: // This depends on the active implementation of
230: // <code>SequentPrintFilter</code>, and has to be compatible
231: // with the displayed sequent
232: final Constraint localDisplayConstraint = ConstraintSequentPrintFilter
233: .determineDisplayConstraint(pos.constrainedFormula(),
234: userConstraint);
235:
236: final ITermTacletAppIndexCache indexCache = determineIndexCache(
237: pos, indexCaches, localDisplayConstraint);
238:
239: return createHelp(pos, services, userConstraint,
240: localDisplayConstraint, tacletIndex, listener, filter,
241: indexCache);
242: }
243:
244: private static ITermTacletAppIndexCache determineIndexCache(
245: PosInOccurrence pos,
246: TermTacletAppIndexCacheSet indexCaches,
247: final Constraint localDisplayConstraint) {
248: if (!localDisplayConstraint.isBottom())
249: return indexCaches.getNoCache();
250:
251: if (pos.isInAntec())
252: return indexCaches.getAntecCache();
253: else
254: return indexCaches.getSuccCache();
255: }
256:
257: private static TermTacletAppIndex createHelp(PosInOccurrence pos,
258: Services services, Constraint userConstraint,
259: Constraint displayConstraint, TacletIndex tacletIndex,
260: NewRuleListener listener, RuleFilter filter,
261: ITermTacletAppIndexCache indexCache) {
262: pos = handleDisplayConstraint(pos, displayConstraint);
263: final Term localTerm = pos.subTerm();
264:
265: final TermTacletAppIndex cached = indexCache
266: .getIndexForTerm(localTerm);
267: if (cached != null) {
268: cached.reportTacletApps(pos, listener);
269: return cached;
270: }
271:
272: final ListOfNoPosTacletApp localApps = getFindTaclet(pos,
273: filter, services, userConstraint, tacletIndex);
274:
275: final ListOfTermTacletAppIndex subIndices = createSubIndices(
276: pos, services, userConstraint, displayConstraint,
277: tacletIndex, listener, filter, indexCache);
278:
279: fireRulesAdded(listener, localApps, pos);
280:
281: final TermTacletAppIndex res = new TermTacletAppIndex(
282: localTerm, localApps, subIndices, displayConstraint,
283: filter);
284: indexCache.putIndexForTerm(localTerm, res);
285:
286: return res;
287: }
288:
289: /**
290: * Create a new tree of indices that additionally contain the taclets that
291: * are selected by <code>filter</code>
292: * @param filter The taclets that are supposed to be added
293: * @param pos Pointer to the term/formula for which an index is to
294: * be created. <code>pos</code> has to be a top-level term
295: * position
296: * @return the index object
297: */
298: public TermTacletAppIndex addTaclets(RuleFilter filter,
299: PosInOccurrence pos, Services services,
300: Constraint userConstraint, TacletIndex tacletIndex,
301: NewRuleListener listener) {
302: RuleFilter effectiveFilter = new AndRuleFilter(filter,
303: ruleFilter);
304:
305: return addTacletsHelp(effectiveFilter, pos, services,
306: userConstraint, tacletIndex, listener);
307: }
308:
309: private TermTacletAppIndex addTacletsHelp(RuleFilter filter,
310: PosInOccurrence pos, Services services,
311: Constraint userConstraint, TacletIndex tacletIndex,
312: NewRuleListener listener) {
313: pos = handleDisplayConstraint(pos, displayConstraint);
314:
315: final ListOfTermTacletAppIndex newSubIndices = addTacletsSubIndices(
316: filter, pos, services, userConstraint, tacletIndex,
317: listener);
318:
319: final ListOfNoPosTacletApp additionalApps = getFindTaclet(pos,
320: filter, services, userConstraint, tacletIndex);
321:
322: fireRulesAdded(listener, additionalApps, pos);
323:
324: return new TermTacletAppIndex(term, localTacletApps
325: .prepend(additionalApps), newSubIndices,
326: displayConstraint, ruleFilter);
327: }
328:
329: private ListOfTermTacletAppIndex addTacletsSubIndices(
330: RuleFilter filter, PosInOccurrence pos, Services services,
331: Constraint userConstraint, TacletIndex tacletIndex,
332: NewRuleListener listener) {
333: ListOfTermTacletAppIndex result = SLListOfTermTacletAppIndex.EMPTY_LIST;
334: final IteratorOfTermTacletAppIndex subIt = subtermIndices
335: .iterator();
336:
337: int i = 0;
338: while (subIt.hasNext()) {
339: final TermTacletAppIndex oldSubIndex = subIt.next();
340: final TermTacletAppIndex newSubIndex = oldSubIndex
341: .addTacletsHelp(filter, pos.down(i), services,
342: userConstraint, tacletIndex, listener);
343: result = result.append(newSubIndex);
344: ++i;
345: }
346:
347: return result;
348: }
349:
350: /**
351: * Recursively update the term index, starting at <code>this</code> and
352: * descending along the given path iterator to the term position below which
353: * a modification was performed
354: * @param pathToModification an iterator that walks from the root of the
355: * formula to the position of modification
356: * @return
357: */
358: private TermTacletAppIndex updateHelp(
359: PIOPathIterator pathToModification, Services services,
360: Constraint userConstraint, TacletIndex tacletIndex,
361: NewRuleListener listener,
362: ITermTacletAppIndexCache indexCache) {
363:
364: pathToModification.next();
365:
366: // Below the position of modification everything has to be rebuilt
367: final boolean completeRebuild = !pathToModification.hasNext();
368: final PosInOccurrence pos = pathToModification
369: .getPosInOccurrence();
370:
371: if (completeRebuild)
372: return updateCompleteRebuild(pos, services, userConstraint,
373: tacletIndex, listener, indexCache);
374:
375: final Term newTerm = pathToModification.getSubTerm();
376:
377: final TermTacletAppIndex cached = indexCache
378: .getIndexForTerm(newTerm);
379: if (cached != null) {
380: cached.reportTacletApps(pathToModification, listener);
381: return cached;
382: }
383:
384: final ListOfTermTacletAppIndex newSubIndices = updateSubIndexes(
385: pathToModification, services, userConstraint,
386: tacletIndex, listener, indexCache);
387:
388: final TermTacletAppIndex res = updateLocalApps(pos, newTerm,
389: services, userConstraint, tacletIndex, listener,
390: newSubIndices);
391:
392: indexCache.putIndexForTerm(newTerm, res);
393: return res;
394: }
395:
396: private TermTacletAppIndex updateCompleteRebuild(
397: PosInOccurrence pos, Services services,
398: Constraint userConstraint, TacletIndex tacletIndex,
399: NewRuleListener listener,
400: ITermTacletAppIndexCache indexCache) {
401: final Term newTerm = pos.subTerm();
402: final Operator newOp = newTerm.op();
403:
404: if (newOp instanceof Modality && newOp == term.op()
405: && newTerm.sub(0).equals(term.sub(0))) {
406: // only the program within a modal operator has changed, but not the
407: // formula after the modal operator. in this case, the formula after
408: // the modality does not have to be rematched. also consider
409: // <code>FindTacletAppContainer.independentSubformulas</code>
410: return updateLocalApps(pos, newTerm, services,
411: userConstraint, tacletIndex, listener,
412: subtermIndices);
413: }
414:
415: return createHelp(pos, services, userConstraint,
416: displayConstraint, tacletIndex, listener, ruleFilter,
417: indexCache);
418: }
419:
420: private TermTacletAppIndex updateLocalApps(PosInOccurrence pos,
421: Term newSubterm, Services services,
422: Constraint userConstraint, TacletIndex tacletIndex,
423: NewRuleListener listener,
424: ListOfTermTacletAppIndex newSubIndices) {
425: final ListOfNoPosTacletApp localApps = getFindTaclet(pos,
426: ruleFilter, services, userConstraint, tacletIndex);
427:
428: fireRulesAdded(listener, localApps, pos);
429:
430: return new TermTacletAppIndex(newSubterm, localApps,
431: newSubIndices, displayConstraint, ruleFilter);
432: }
433:
434: private ListOfTermTacletAppIndex updateSubIndexes(
435: PIOPathIterator pathToModification, Services services,
436: Constraint userConstraint, TacletIndex tacletIndex,
437: NewRuleListener listener,
438: ITermTacletAppIndexCache indexCache) {
439: ListOfTermTacletAppIndex newSubIndices = subtermIndices;
440:
441: final Term newTerm = pathToModification.getSubTerm();
442: final int child = pathToModification.getChild();
443:
444: if (newTerm.op() instanceof IUpdateOperator) {
445: final int targetPos = ((IUpdateOperator) newTerm.op())
446: .targetPos();
447: if (child != targetPos) {
448: newSubIndices = updateIUpdateTarget(newSubIndices,
449: targetPos, pathToModification
450: .getPosInOccurrence().down(targetPos),
451: services, userConstraint, tacletIndex,
452: listener, indexCache
453: .descend(newTerm, targetPos));
454: }
455: }
456:
457: return updateOneSubIndex(newSubIndices, pathToModification,
458: services, userConstraint, tacletIndex, listener,
459: indexCache.descend(newTerm, child));
460: }
461:
462: /**
463: * Update the target formula/term of an update (which has position
464: * <code>subtermPos</code> in the complete formula). This is necessary
465: * whenever a part of the update has changed, because this also changes the
466: * update context of taclet apps in the target.
467: */
468: private ListOfTermTacletAppIndex updateIUpdateTarget(
469: ListOfTermTacletAppIndex oldSubindices, int updateTarget,
470: PosInOccurrence targetPos, Services services,
471: Constraint userConstraint, TacletIndex tacletIndex,
472: NewRuleListener listener,
473: ITermTacletAppIndexCache indexCache) {
474:
475: ListOfTermTacletAppIndex subindices = oldSubindices
476: .take(updateTarget);
477: final TermTacletAppIndex toBeRemoved = subindices.head();
478: final Term targetTerm = toBeRemoved.term;
479: subindices = subindices.tail();
480:
481: final TermTacletAppIndex newSubIndex;
482:
483: if (targetTerm.op() instanceof Modality) {
484: // it is enough to update the local rule apps of the target, because
485: // all apps below the modality have to be independent of update
486: // contexts anyway. this is a very common case, because updates
487: // usually occur in front of programs
488: newSubIndex = toBeRemoved.updateLocalApps(targetPos,
489: targetTerm, services, userConstraint, tacletIndex,
490: listener, toBeRemoved.subtermIndices);
491: } else {
492: // the target is updated completely otherwise
493: newSubIndex = createHelp(targetPos, services,
494: userConstraint, toBeRemoved.displayConstraint,
495: tacletIndex, listener, toBeRemoved.ruleFilter,
496: indexCache);
497: }
498:
499: return prepend(subindices.prepend(newSubIndex), oldSubindices,
500: updateTarget);
501: }
502:
503: /**
504: * Update the subtree of indices the given iterator
505: * <code>pathToModification</code> descends to
506: */
507: private ListOfTermTacletAppIndex updateOneSubIndex(
508: ListOfTermTacletAppIndex oldSubindices,
509: PIOPathIterator pathToModification, Services services,
510: Constraint userConstraint, TacletIndex tacletIndex,
511: NewRuleListener listener,
512: ITermTacletAppIndexCache indexCache) {
513:
514: final int child = pathToModification.getChild();
515:
516: ListOfTermTacletAppIndex subindices = oldSubindices.take(child);
517: final TermTacletAppIndex toBeUpdated = subindices.head();
518: subindices = subindices.tail();
519:
520: final TermTacletAppIndex newSubIndex = toBeUpdated.updateHelp(
521: pathToModification, services, userConstraint,
522: tacletIndex, listener, indexCache);
523:
524: return prepend(subindices.prepend(newSubIndex), oldSubindices,
525: child);
526: }
527:
528: /**
529: * Prepend the first <code>n</code> elements of <code>toAdd</code> to
530: * <code>initialList</code>
531: */
532: private static ListOfTermTacletAppIndex prepend(
533: ListOfTermTacletAppIndex initialList,
534: ListOfTermTacletAppIndex toAdd, int n) {
535: if (n <= 0)
536: return initialList;
537: if (n == 1)
538: return initialList.prepend(toAdd.head());
539: return prepend(initialList, toAdd.tail(), n - 1).prepend(
540: toAdd.head());
541: }
542:
543: /**
544: * Updates the TermTacletAppIndex after a change at or below
545: * position <code>pos</code>
546: * @param pos Pointer to the term/formula where a change occurred
547: * @return the updated index object
548: */
549: public TermTacletAppIndex update(PosInOccurrence pos,
550: Services services, Constraint userConstraint,
551: TacletIndex tacletIndex, NewRuleListener listener,
552: TermTacletAppIndexCacheSet indexCaches) {
553:
554: final ITermTacletAppIndexCache indexCache = determineIndexCache(
555: pos, indexCaches, displayConstraint);
556:
557: final PIOPathIterator it = pos.iterator();
558: return updateHelp(it, services, userConstraint, tacletIndex,
559: listener, indexCache);
560: }
561:
562: /**
563: * @return the sub-index for the given position
564: */
565: private TermTacletAppIndex descend(PosInOccurrence pos) {
566: if (pos.isTopLevel())
567: return this ;
568:
569: final PIOPathIterator it = pos.iterator();
570: TermTacletAppIndex res = this ;
571:
572: while (true) {
573: final int child = it.next();
574: if (child == -1)
575: return res;
576:
577: res = res.getSubIndex(child);
578: }
579: }
580:
581: /**
582: * @return all taclet apps for the given position
583: */
584: public ListOfNoPosTacletApp getTacletAppAt(PosInOccurrence pos,
585: RuleFilter p_filter) {
586: TermTacletAppIndex index = descend(pos);
587: return filter(p_filter, index.localTacletApps);
588: }
589:
590: /**
591: * @return all taclet apps for or below the given position
592: */
593: public ListOfTacletApp getTacletAppAtAndBelow(PosInOccurrence pos,
594: RuleFilter filter) {
595: return descend(pos).collectTacletApps(pos, filter);
596: }
597:
598: /**
599: * Class that is used to convert <code>NoPosTacletApp</code>s to
600: * <code>PosTacletApp</code>s via the method
601: * <code>reportTacletApps</code>
602: */
603: private static class CollectTacletAppListener implements
604: NewRuleListener {
605: private ListOfTacletApp res = SLListOfTacletApp.EMPTY_LIST;
606: private final RuleFilter filter;
607:
608: public CollectTacletAppListener(RuleFilter p_filter) {
609: filter = p_filter;
610: }
611:
612: public ListOfTacletApp getResult() {
613: return res;
614: }
615:
616: public void ruleAdded(RuleApp app, PosInOccurrence pos) {
617: if (filter.filter((app.rule()))) {
618: final TacletApp tacletApp = TacletAppIndex
619: .createTacletApp((NoPosTacletApp) app, pos);
620: if (tacletApp != null) {
621: res = res.prepend(tacletApp);
622: }
623: }
624: }
625: }
626:
627: /**
628: * Collect all taclet apps that are stored by <code>this</code> (and by
629: * the sub-indices of <code>this</code>). <code>NoPosTacletApp</code>s are
630: * converted to <code>PosTacletApp</code>s using the parameter
631: * <code>pos</code>
632: * @param pos The position of this index
633: * @return a list of all taclet apps
634: */
635: private ListOfTacletApp collectTacletApps(PosInOccurrence pos,
636: RuleFilter p_filter) {
637: pos = handleDisplayConstraint(pos, displayConstraint);
638:
639: final CollectTacletAppListener listener = new CollectTacletAppListener(
640: p_filter);
641:
642: reportTacletApps(pos, listener);
643:
644: return listener.getResult();
645: }
646:
647: /**
648: * Report all <code>NoPosTacletApp</code> s that are stored by
649: * <code>this</code> (and by the sub-indices of <code>this</code>).
650: *
651: * @param pos
652: * The position of this index
653: * @param listener
654: * The listener to which the taclet apps found are supposed to be
655: * reported
656: * @return a list of all taclet apps
657: */
658: public void reportTacletApps(PosInOccurrence pos,
659: NewRuleListener listener) {
660: pos = handleDisplayConstraint(pos, displayConstraint);
661: fireRulesAdded(listener, localTacletApps, pos);
662:
663: final IteratorOfTermTacletAppIndex it = subtermIndices
664: .iterator();
665: int subterm = 0;
666: while (it.hasNext()) {
667: it.next().reportTacletApps(pos.down(subterm), listener);
668: ++subterm;
669: }
670: }
671:
672: /**
673: * Report all taclet apps that are affected by a modification of the term
674: * under consideration at place <code>pathToModification</code>. These are
675: * the taclet above and below the place of modification, and the taclets
676: * whose update context has changed.
677: */
678: private void reportTacletApps(PIOPathIterator pathToModification,
679: NewRuleListener listener) {
680: final PosInOccurrence pos = pathToModification
681: .getPosInOccurrence();
682: if (!pathToModification.hasNext()) {
683: reportTacletApps(pos, listener);
684: return;
685: }
686:
687: fireRulesAdded(listener, localTacletApps, pos);
688: final Term subTerm = pos.subTerm();
689: final int nextSubtermIndex = pathToModification.getChild();
690:
691: if (subTerm.op() instanceof IUpdateOperator) {
692: final int targetPos = ((IUpdateOperator) subTerm.op())
693: .targetPos();
694: if (nextSubtermIndex != targetPos)
695: getSubIndex(targetPos).reportTacletApps(
696: pos.down(targetPos), listener);
697: }
698:
699: pathToModification.next();
700: getSubIndex(nextSubtermIndex).reportTacletApps(
701: pathToModification, listener);
702: }
703:
704: private static void fireRulesAdded(NewRuleListener listener,
705: ListOfNoPosTacletApp taclets, PosInOccurrence pos) {
706: IteratorOfNoPosTacletApp it = taclets.iterator();
707:
708: while (it.hasNext())
709: listener.ruleAdded(it.next(), pos);
710: }
711:
712: /**
713: * @return filtered list
714: */
715: public static ListOfNoPosTacletApp filter(RuleFilter p_filter,
716: ListOfNoPosTacletApp taclets) {
717: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
718:
719: while (taclets != SLListOfNoPosTacletApp.EMPTY_LIST) {
720: final NoPosTacletApp app = taclets.head();
721: taclets = taclets.tail();
722: if (p_filter.filter(app.taclet()))
723: result = result.prepend(app);
724: }
725:
726: return result;
727: }
728: }
|