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.Constraint;
015: import de.uka.ilkd.key.logic.PosInOccurrence;
016: import de.uka.ilkd.key.logic.Sequent;
017: import de.uka.ilkd.key.logic.SequentChangeInfo;
018: import de.uka.ilkd.key.rule.*;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /** the class manages the available TacletApps. This index has to be
022: * used if one wants to ask for the available taclet application at a
023: * specific position (or the whole sequent if taclet is a nofind
024: * rule). This means all taclet applications that have a position
025: * information are managed by this index. For all others the class
026: * TacletIndex is used. This index uses also the TacletIndex to
027: * calculate new TacletApps.
028: */
029:
030: public class TacletAppIndex {
031:
032: private final TacletIndex tacletIndex;
033:
034: private SemisequentTacletAppIndex antecIndex;
035: private SemisequentTacletAppIndex succIndex;
036:
037: private TermTacletAppIndexCacheSet indexCaches;
038:
039: private Goal goal;
040:
041: /**
042: * Object to which the appearance of new taclet apps is reported
043: */
044: private NewRuleListener newRuleListener = NullNewRuleListener.INSTANCE;
045:
046: /**
047: * Filter that is used to restrict the set of taclets that are considered as
048: * possible members of this index. This is used to distinguish between
049: * <code>TacletAppIndex</code> s exclusively for automatic or interactive
050: * taclets.
051: */
052: private RuleFilter ruleFilter;
053:
054: /** The sequent with the formulas for which taclet indices are hold by
055: * this object. Invariant: <code>seq != null</code> implies that the
056: * indices <code>antecIndex</code>, <code>succIndex</code> are up to date
057: * for the sequent <code>seq</code> */
058: private Sequent seq;
059:
060: public TacletAppIndex(TacletIndex tacletIndex) {
061: this (tacletIndex, null, null, null, null, TacletFilter.TRUE,
062: new TermTacletAppIndexCacheSet());
063: }
064:
065: private TacletAppIndex(TacletIndex tacletIndex,
066: SemisequentTacletAppIndex antecIndex,
067: SemisequentTacletAppIndex succIndex, Goal goal,
068: Sequent seq, RuleFilter ruleFilter,
069: TermTacletAppIndexCacheSet indexCaches) {
070: this .tacletIndex = tacletIndex;
071: this .antecIndex = antecIndex;
072: this .succIndex = succIndex;
073: this .goal = goal;
074: this .seq = seq;
075: this .ruleFilter = ruleFilter;
076: this .indexCaches = indexCaches;
077: }
078:
079: public void setNewRuleListener(NewRuleListener p_newRuleListener) {
080: newRuleListener = p_newRuleListener;
081: }
082:
083: private NewRuleListener getNewRulePropagator() {
084: return newRuleListener;
085: }
086:
087: public void setRuleFilter(RuleFilter p_ruleFilter) {
088: if (p_ruleFilter != ruleFilter) {
089: ruleFilter = p_ruleFilter;
090: clearAndDetachCache();
091: }
092: }
093:
094: private RuleFilter getRuleFilter() {
095: return ruleFilter;
096: }
097:
098: /**
099: * returns a new TacletAppIndex with a given TacletIndex
100: */
101: TacletAppIndex copyWithTacletIndex(TacletIndex p_tacletIndex) {
102: return new TacletAppIndex(p_tacletIndex, antecIndex, succIndex,
103: getGoal(), getSequent(), ruleFilter, indexCaches);
104: }
105:
106: /**
107: * Set the goal association of this index to the given object
108: * <code>p_goal</code>. If the sequent of the new goal differs from the
109: * former one (attribute <code>seq</code>), the index will be rebuilt as
110: * soon as data is requested from it.
111: */
112: public void setup(Goal p_goal) {
113: goal = p_goal;
114: }
115:
116: /**
117: * Delete all cached information about taclet apps. This also makes the
118: * index cache of this index independent from the caches of other indexes
119: * (expensive)
120: */
121: public void clearAndDetachCache() {
122: clearIndexes();
123: createNewIndexCache();
124: }
125:
126: public void clearIndexes() {
127: seq = null; // This leads to a delayed rebuild
128: antecIndex = null;
129: succIndex = null;
130: }
131:
132: private void createNewIndexCache() {
133: indexCaches = new TermTacletAppIndexCacheSet();
134: if (antecIndex != null)
135: antecIndex.setIndexCache(indexCaches);
136: if (succIndex != null)
137: succIndex.setIndexCache(indexCaches);
138: }
139:
140: /**
141: * Forces all delayed computations to be performed, so that
142: * the cache is fully up-to-date (NewRuleListener gets informed)
143: */
144: public void fillCache() {
145: ensureIndicesExist();
146: }
147:
148: private void createAllFromGoal() {
149: this .seq = getNode().sequent();
150:
151: antecIndex = new SemisequentTacletAppIndex(getSequent(), true,
152: getServices(), getUserConstraint(), tacletIndex(),
153: getNewRulePropagator(), getRuleFilter(), indexCaches);
154: succIndex = new SemisequentTacletAppIndex(getSequent(), false,
155: getServices(), getUserConstraint(), tacletIndex(),
156: getNewRulePropagator(), getRuleFilter(), indexCaches);
157: }
158:
159: private void ensureIndicesExist() {
160: Debug.assertFalse(getGoal() == null,
161: "TacletAppIndex does not know to which goal it "
162: + "refers");
163:
164: if (!isUpToDateForGoal())
165: // Indices are not up to date
166: createAllFromGoal();
167: }
168:
169: /**
170: * @return true iff this index currently is up to date with respect to the
171: * sequent of the associated goal; this does not detect other modifications
172: * like an altered user constraint
173: */
174: private boolean isUpToDateForGoal() {
175: return getGoal() != null && getSequent() == getNode().sequent();
176: }
177:
178: private SemisequentTacletAppIndex getIndex(PosInOccurrence pos) {
179: ensureIndicesExist();
180: return pos.isInAntec() ? antecIndex : succIndex;
181: }
182:
183: private ListOfTacletApp getFindTacletWithPos(PosInOccurrence pos,
184: TacletFilter filter, Services services,
185: Constraint userConstraint) {
186: Debug.assertFalse(pos == null);
187: ListOfNoPosTacletApp tacletInsts = getFindTaclet(pos, filter,
188: services, userConstraint);
189: return createTacletApps(tacletInsts, pos);
190: }
191:
192: /** returns the set of rule applications
193: * at the given position of the given sequent.
194: * @param pos the PosInOccurrence to focus
195: */
196: public ListOfTacletApp getTacletAppAt(PosInOccurrence pos,
197: TacletFilter filter, Services services,
198: Constraint userConstraint) {
199: ListOfTacletApp sal = getFindTacletWithPos(pos, filter,
200: services, userConstraint);
201: return prepend(sal, getNoFindTaclet(filter, services,
202: userConstraint));
203: }
204:
205: /** creates TacletApps out of each single NoPosTacletApp object
206: * @param tacletInsts the list of NoPosTacletApps the TacletApps are to
207: * be created from
208: * @param pos the PosInOccurrence to focus
209: * @return list of all created TacletApps
210: */
211: static ListOfTacletApp createTacletApps(
212: ListOfNoPosTacletApp tacletInsts, PosInOccurrence pos) {
213: ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
214: IteratorOfNoPosTacletApp it = tacletInsts.iterator();
215: while (it.hasNext()) {
216: NoPosTacletApp tacletApp = it.next();
217: if (tacletApp.taclet() instanceof FindTaclet) {
218: PosTacletApp newTacletApp = tacletApp
219: .setPosInOccurrence(pos);
220: if (newTacletApp != null) {
221: result = result.prepend(newTacletApp);
222: }
223: } else {
224: result = result.prepend(tacletApp);
225: }
226: }
227: return result;
228: }
229:
230: static TacletApp createTacletApp(NoPosTacletApp tacletApp,
231: PosInOccurrence pos) {
232: if (tacletApp.taclet() instanceof FindTaclet) {
233: PosTacletApp newTacletApp = tacletApp
234: .setPosInOccurrence(pos);
235: if (newTacletApp != null) {
236: return newTacletApp;
237: } else {
238: return null;
239: }
240: } else {
241: return tacletApp;
242: }
243: }
244:
245: /**
246: * collects all NoFindTacletInstantiations
247: * @param services the Services object encapsulating information
248: * about the java datastructures like (static)types etc.
249: * @return list of all possible instantiations
250: */
251: public ListOfNoPosTacletApp getNoFindTaclet(TacletFilter filter,
252: Services services, Constraint userConstraint) {
253: RuleFilter effectiveFilter = new AndRuleFilter(filter,
254: ruleFilter);
255: return tacletIndex().getNoFindTaclet(effectiveFilter, services,
256: userConstraint);
257: }
258:
259: /**
260: * collects all RewriteTacletInstantiations in a subterm of the
261: * constrainedFormula described by a
262: * PosInOccurrence
263: * @param pos the PosInOccurrence to focus
264: * @param services the Services object encapsulating information
265: * about the java datastructures like (static)types etc.
266: * @return list of all possible instantiations
267: */
268: public ListOfNoPosTacletApp getRewriteTaclet(PosInOccurrence pos,
269: TacletFilter filter, Services services,
270: Constraint userConstraint) {
271:
272: final IteratorOfNoPosTacletApp it = getFindTaclet(pos, filter,
273: services, userConstraint).iterator();
274:
275: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
276:
277: while (it.hasNext()) {
278: final NoPosTacletApp tacletApp = it.next();
279: if (tacletApp.taclet() instanceof RewriteTaclet)
280: result = result.prepend(tacletApp);
281: }
282:
283: return result;
284: }
285:
286: /**
287: * collects all FindTaclets with instantiations and position
288: * @param pos the PosInOccurrence to focus
289: * @param services the Services object encapsulating information
290: * about the java datastructures like (static)types etc.
291: * @return list of all possible instantiations
292: */
293: public ListOfNoPosTacletApp getFindTaclet(PosInOccurrence pos,
294: TacletFilter filter, Services services,
295: Constraint userConstraint) {
296: return getIndex(pos).getTacletAppAt(pos, filter);
297: }
298:
299: /**
300: * returns the rule applications at the given PosInOccurrence and at all
301: * Positions below this. The method calls getTacletAppAt for all the
302: * Positions below.
303: * @param pos the position where to start from
304: * @param services the Services object encapsulating information
305: * about the java datastructures like (static)types etc.
306: * @return the possible rule applications
307: */
308: public ListOfTacletApp getTacletAppAtAndBelow(PosInOccurrence pos,
309: TacletFilter filter, Services services,
310: Constraint userConstraint) {
311: final ListOfTacletApp findTaclets = getIndex(pos)
312: .getTacletAppAtAndBelow(pos, filter);
313: return prepend(findTaclets, getNoFindTaclet(filter, services,
314: userConstraint));
315: }
316:
317: /**
318: * called if a formula has been replaced
319: * @param sci SequentChangeInfo describing the change of the sequent
320: */
321: public void sequentChanged(Goal goal, SequentChangeInfo sci) {
322: if (sci.getOriginalSequent() != getSequent())
323: // we are not up to date and have to rebuild everything (lazy)
324: clearIndexes();
325: else
326: updateIndices(sci);
327: }
328:
329: private void updateIndices(SequentChangeInfo sci) {
330: seq = sci.sequent();
331:
332: antecIndex = antecIndex.sequentChanged(sci, getServices(),
333: getUserConstraint(), tacletIndex(),
334: getNewRulePropagator());
335:
336: succIndex = succIndex.sequentChanged(sci, getServices(),
337: getUserConstraint(), tacletIndex(),
338: getNewRulePropagator());
339: }
340:
341: /**
342: * updates the internal caches after a new Taclet with instantiation
343: * information has been added to the TacletIndex.
344: * @param tacletApp the partially instantiated Taclet to add
345: */
346: public void addedNoPosTacletApp(NoPosTacletApp tacletApp) {
347: if (indexCaches.isRelevantTaclet(tacletApp.taclet())) {
348: // we must flush the index cache, and we must no longer use a cache
349: // that we share with other instances of <code>TacletAppIndex</code>
350: // (that maybe live of different goals)
351: createNewIndexCache();
352: }
353:
354: if (!isUpToDateForGoal()) {
355: // we are not up to date and have to rebuild everything (lazy)
356: clearIndexes();
357: return;
358: }
359:
360: if (tacletApp.taclet() instanceof NoFindTaclet) {
361: if (ruleFilter.filter(tacletApp.taclet()))
362: getNewRulePropagator().ruleAdded(tacletApp, null);
363: return;
364: }
365:
366: final SetRuleFilter newTaclets = new SetRuleFilter();
367: newTaclets.addRuleToSet(tacletApp.taclet());
368:
369: antecIndex = antecIndex.addTaclets(newTaclets, getSequent(),
370: getServices(), getUserConstraint(), tacletIndex(),
371: getNewRulePropagator());
372: succIndex = succIndex.addTaclets(newTaclets, getSequent(),
373: getServices(), getUserConstraint(), tacletIndex(),
374: getNewRulePropagator());
375: }
376:
377: /**
378: * updates the internal caches after a Taclet with instantiation
379: * information has been removed from the TacletIndex.
380: * @param tacletApp the partially instantiated Taclet to remove
381: */
382: public void removedNoPosTacletApp(NoPosTacletApp tacletApp) {
383: if (indexCaches.isRelevantTaclet(tacletApp.taclet())) {
384: // we must flush the index cache, and we must no longer use a cache
385: // that we share with other instances of <code>TacletAppIndex</code>
386: // (that maybe live of different goals)
387: clearAndDetachCache();
388: } else {
389: clearIndexes();
390: }
391: }
392:
393: public String toString() {
394: return "TacletAppIndex with indexing, getting Taclets from"
395: + " TacletIndex " + tacletIndex();
396: }
397:
398: // helper because ListOfNoPosTacletApp is no ListOfTacletApp
399: private static ListOfTacletApp prepend(ListOfTacletApp l1,
400: ListOfNoPosTacletApp l2) {
401: IteratorOfNoPosTacletApp it = l2.iterator();
402: while (it.hasNext()) {
403: l1 = l1.prepend(it.next());
404: }
405: return l1;
406: }
407:
408: private Goal getGoal() {
409: return goal;
410: }
411:
412: private Sequent getSequent() {
413: return seq;
414: }
415:
416: private Constraint getUserConstraint() {
417: return getProof().getUserConstraint().getConstraint();
418: }
419:
420: private Services getServices() {
421: return getProof().getServices();
422: }
423:
424: private Proof getProof() {
425: return getNode().proof();
426: }
427:
428: private Node getNode() {
429: return getGoal().node();
430: }
431:
432: /**
433: * returns the Taclet index for this ruleAppIndex.
434: */
435: public TacletIndex tacletIndex() {
436: return tacletIndex;
437: }
438:
439: /**
440: * Reports all cached rule apps.
441: * Calls ruleAdded on the given NewRuleListener for
442: * every cached taclet app.
443: */
444: public void reportRuleApps(NewRuleListener l, Services services,
445: Constraint userConstraint) {
446: if (antecIndex != null)
447: antecIndex.reportRuleApps(l);
448: if (succIndex != null)
449: succIndex.reportRuleApps(l);
450:
451: final IteratorOfNoPosTacletApp it = getNoFindTaclet(
452: TacletFilter.TRUE, services, userConstraint).iterator();
453: while (it.hasNext())
454: l.ruleAdded(it.next(), null);
455: }
456: }
|