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 java.util.HashSet;
014: import java.util.Iterator;
015:
016: import de.uka.ilkd.key.java.*;
017: import de.uka.ilkd.key.java.statement.LabeledStatement;
018: import de.uka.ilkd.key.java.statement.MethodFrame;
019: import de.uka.ilkd.key.java.statement.SynchronizedBlock;
020: import de.uka.ilkd.key.java.statement.Try;
021: import de.uka.ilkd.key.logic.*;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.logic.sort.GenericSort;
024: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
025: import de.uka.ilkd.key.logic.sort.Sort;
026: import de.uka.ilkd.key.rule.*;
027: import de.uka.ilkd.key.rule.inst.SVInstantiations;
028: import de.uka.ilkd.key.util.Debug;
029:
030: /**
031: * manages all applicable Taclets (more precisely: Taclets with
032: * instantiations but without position information, the ???NoPosTacletApp???s)
033: * at one node. It is a persistent
034: * implementation. Taclets can be added because the Taclets allow to
035: * introduce new rules during runtime. It offers selective get methods
036: * for different kinds of rules.
037: */
038: public class TacletIndex {
039:
040: /** @link aggregation
041: * @label known rules
042: * @supplierCardinality **/
043: /*#Taclet lnkTaclet;*/
044:
045: /** contains rewrite Taclets */
046: public HashMapFromObjectToListOfNoPosTacletApp rwList = new HashMapFromObjectToListOfNoPosTacletApp();
047:
048: /** contains antecedent Taclets */
049: private HashMapFromObjectToListOfNoPosTacletApp antecList = new HashMapFromObjectToListOfNoPosTacletApp();
050:
051: /** contains succedent Taclets */
052: private HashMapFromObjectToListOfNoPosTacletApp succList = new HashMapFromObjectToListOfNoPosTacletApp();
053:
054: /** contains NoFind-Taclets */
055: private ListOfNoPosTacletApp noFindList = SLListOfNoPosTacletApp.EMPTY_LIST;
056:
057: /**
058: * keeps track of no pos taclet apps with partial
059: * instantiations
060: */
061: private HashSet partialInstantiatedRuleApps = new HashSet();
062:
063: // reused object to store prefix occurrences when retrieving
064: // taclets with java blocks.
065: private PrefixOccurrences prefixOccurrences = new PrefixOccurrences();
066:
067: /** constructs empty rule index */
068: public TacletIndex() {
069: }
070:
071: /**
072: * creates a new TacletIndex with the given Taclets as initial contents.
073: */
074: public TacletIndex(SetOfTaclet tacletSet) {
075: setTaclets(tacletSet);
076: }
077:
078: private TacletIndex(HashMapFromObjectToListOfNoPosTacletApp rwList,
079: HashMapFromObjectToListOfNoPosTacletApp antecList,
080: HashMapFromObjectToListOfNoPosTacletApp succList,
081: ListOfNoPosTacletApp noFindList,
082: HashSet partialInstantiatedRuleApps) {
083: this .rwList = rwList;
084: this .antecList = antecList;
085: this .succList = succList;
086: this .noFindList = noFindList;
087: this .partialInstantiatedRuleApps = partialInstantiatedRuleApps;
088: }
089:
090: private Object getIndexObj(FindTaclet tac) {
091: Object indexObj;
092: final Term indexTerm = tac.find();
093: if (!indexTerm.javaBlock().isEmpty()) {
094: final JavaProgramElement prg = indexTerm.javaBlock()
095: .program();
096: indexObj = ((StatementBlock) prg).getStatementAt(0);
097: if (!(indexObj instanceof SchemaVariable)) {
098: indexObj = indexObj.getClass();
099: }
100: } else {
101: indexObj = indexTerm.op();
102: if (indexObj instanceof AnonymousUpdate) {
103: //indexed independent of arity
104: indexObj = AnonymousUpdate.class;
105: }
106: if (indexObj instanceof QuanUpdateOperator) {
107: //indexed independent of arity
108: indexObj = QuanUpdateOperator.class;
109: }
110: if (indexObj instanceof SortDependingSymbol) {
111: // indexed independent of sort
112: indexObj = ((SortDependingSymbol) indexObj).getKind();
113: }
114: if (indexObj instanceof NRFunctionWithExplicitDependencies) {
115: // indexed independent of dependencies
116: indexObj = NRFunctionWithExplicitDependencies.class;
117: }
118: if (indexObj instanceof AccessOp) {
119: indexObj = AccessOp.class;
120: }
121: }
122: if (indexObj instanceof SchemaVariable) {
123: if (((SchemaVariable) indexObj).isTermSV()
124: || ((SchemaVariable) indexObj).isFormulaSV()) {
125: indexObj = ((SortedSchemaVariable) indexObj).sort();
126: if (indexObj instanceof GenericSort)
127: indexObj = GenericSort.class;
128: } else if (((SchemaVariable) indexObj).isProgramSV()) {
129: indexObj = SchemaOp.PROGSVOP;
130: } else {
131: indexObj = SchemaOp.DEFAULTSVOP;
132: }
133: }
134: return indexObj;
135: }
136:
137: private void insertToMap(NoPosTacletApp tacletApp,
138: HashMapFromObjectToListOfNoPosTacletApp map) {
139: Object indexObj = getIndexObj((FindTaclet) tacletApp.taclet());
140: ListOfNoPosTacletApp opList = map.get(indexObj);
141: if (opList == null) {
142: opList = SLListOfNoPosTacletApp.EMPTY_LIST
143: .prepend(tacletApp);
144: } else {
145: opList = opList.prepend(tacletApp);
146: }
147: map.put(indexObj, opList);
148: }
149:
150: private void removeFromMap(NoPosTacletApp tacletApp,
151: HashMapFromObjectToListOfNoPosTacletApp map) {
152: Object op = getIndexObj((FindTaclet) tacletApp.taclet());
153: ListOfNoPosTacletApp opList = map.get(op);
154: if (opList != null) {
155: opList = opList.removeAll(tacletApp);
156: if (opList == SLListOfNoPosTacletApp.EMPTY_LIST) {
157: map.remove(op);
158: } else {
159: map.put(op, opList);
160: }
161: }
162: }
163:
164: /**
165: * sets the Taclets in this index and removes the old ones
166: * @param tacletList the new taclets for this index
167: */
168: public void setTaclets(SetOfTaclet tacletList) {
169: rwList = new HashMapFromObjectToListOfNoPosTacletApp();
170: antecList = new HashMapFromObjectToListOfNoPosTacletApp();
171: succList = new HashMapFromObjectToListOfNoPosTacletApp();
172: noFindList = SLListOfNoPosTacletApp.EMPTY_LIST;
173: addTaclets(tacletList);
174: }
175:
176: /**
177: * sets the Taclets with instantiation info
178: * in this index and removes the old ones
179: * @param tacletAppList the new NoPosTacletApps for this index
180: */
181: public void setTaclets(SetOfNoPosTacletApp tacletAppList) {
182: rwList = new HashMapFromObjectToListOfNoPosTacletApp();
183: antecList = new HashMapFromObjectToListOfNoPosTacletApp();
184: succList = new HashMapFromObjectToListOfNoPosTacletApp();
185: noFindList = SLListOfNoPosTacletApp.EMPTY_LIST;
186: addTaclets(tacletAppList);
187: }
188:
189: /**
190: * adds a set of Taclets to this index
191: * @param tacletList the taclets to be added
192: */
193: public void addTaclets(SetOfTaclet tacletList) {
194: IteratorOfTaclet it = tacletList.iterator();
195: while (it.hasNext()) {
196: add(it.next());
197: }
198: }
199:
200: /**
201: * adds a set of NoPosTacletApp to this index
202: * @param tacletAppList the NoPosTacletApps to be added
203: */
204: public void addTaclets(SetOfNoPosTacletApp tacletAppList) {
205: IteratorOfNoPosTacletApp it = tacletAppList.iterator();
206: while (it.hasNext()) {
207: add(it.next());
208: }
209: }
210:
211: /**
212: * adds a new Taclet to this index.
213: * If rule instance is not known rule is not added
214: * @param rule the Taclet to be added
215: */
216: public void add(Taclet rule) {
217: // always added. There no way the creation of the TacletApp fails because
218: // there are no instantiations
219: add(NoPosTacletApp.createNoPosTacletApp(rule));
220: }
221:
222: /** adds a new Taclet with instantiation information to this index.
223: * If rule instance is not known rule is not added
224: * @param tacletApp the Taclet and its instantiation info to be added
225: */
226: public void add(NoPosTacletApp tacletApp) {
227: Taclet rule = tacletApp.taclet();
228: if (rule instanceof RewriteTaclet) {
229: insertToMap(tacletApp, rwList);
230: } else if (rule instanceof AntecTaclet) {
231: insertToMap(tacletApp, antecList);
232: } else if (rule instanceof SuccTaclet) {
233: insertToMap(tacletApp, succList);
234: } else if (rule instanceof NoFindTaclet) {
235: noFindList = noFindList.prepend(tacletApp);
236: } else {
237: // should never be reached
238: Debug.fail("Tried to add an unknown type of Taclet");
239: }
240:
241: if (tacletApp.instantiations() != SVInstantiations.EMPTY_SVINSTANTIATIONS) {
242: partialInstantiatedRuleApps.add(tacletApp);
243: }
244: }
245:
246: /**
247: * removes the given NoPosTacletApps from this index
248: * @param tacletAppList the NoPosTacletApps to be removed
249: */
250: public void removeTaclets(SetOfNoPosTacletApp tacletAppList) {
251: IteratorOfNoPosTacletApp it = tacletAppList.iterator();
252: while (it.hasNext()) {
253: remove(it.next());
254: }
255: }
256:
257: /** removes a Taclet with the given instantiation information from this index.
258: * @param tacletApp the Taclet and its instantiation info to be removed
259: */
260: public void remove(NoPosTacletApp tacletApp) {
261: Taclet rule = tacletApp.taclet();
262: if (rule instanceof RewriteTaclet) {
263: removeFromMap(tacletApp, rwList);
264: } else if (rule instanceof AntecTaclet) {
265: removeFromMap(tacletApp, antecList);
266: } else if (rule instanceof SuccTaclet) {
267: removeFromMap(tacletApp, succList);
268: } else if (rule instanceof NoFindTaclet) {
269: noFindList = noFindList.removeAll(tacletApp);
270: } else {
271: // should never be reached
272: Debug.fail("Tried to remove an unknown type of Taclet");
273: }
274:
275: if (tacletApp.instantiations() != SVInstantiations.EMPTY_SVINSTANTIATIONS) {
276: // Debug.assertTrue(partialInstantiatedRuleApps.contains(tacletApp));
277: partialInstantiatedRuleApps.remove(tacletApp);
278: }
279: }
280:
281: /** copies the index */
282: public TacletIndex copy() {
283: return new TacletIndex(
284: (HashMapFromObjectToListOfNoPosTacletApp) rwList
285: .clone(),
286: (HashMapFromObjectToListOfNoPosTacletApp) antecList
287: .clone(),
288: (HashMapFromObjectToListOfNoPosTacletApp) succList
289: .clone(), noFindList,
290: (HashSet) partialInstantiatedRuleApps.clone());
291: }
292:
293: /** clones the index */
294: public Object clone() {
295: return this .copy();
296: }
297:
298: private SetOfNoPosTacletApp addToSet(ListOfNoPosTacletApp list,
299: SetOfNoPosTacletApp set) {
300: IteratorOfNoPosTacletApp it = list.iterator();
301: while (it.hasNext()) {
302: set = set.add(it.next());
303: }
304: return set;
305: }
306:
307: public SetOfNoPosTacletApp allNoPosTacletApps() {
308: SetOfNoPosTacletApp tacletAppSet = SetAsListOfNoPosTacletApp.EMPTY_SET;
309: IteratorOfListOfNoPosTacletApp it0 = rwList.values();
310: while (it0.hasNext()) {
311: tacletAppSet = addToSet(it0.next(), tacletAppSet);
312: }
313: IteratorOfListOfNoPosTacletApp it1 = antecList.values();
314: while (it1.hasNext()) {
315: tacletAppSet = addToSet(it1.next(), tacletAppSet);
316: }
317: IteratorOfListOfNoPosTacletApp it2 = succList.values();
318: while (it2.hasNext()) {
319: tacletAppSet = addToSet(it2.next(), tacletAppSet);
320: }
321: IteratorOfNoPosTacletApp it3 = noFindList.iterator();
322: while (it3.hasNext()) {
323: tacletAppSet = tacletAppSet.add(it3.next());
324: }
325: return tacletAppSet;
326: }
327:
328: /** returns a list of Taclets and instantiations from the given list of
329: * taclets with
330: * respect to term and the filter object.
331: * @param services the Services object encapsulating information
332: * about the java datastructures like (static)types etc.
333: */
334: private ListOfNoPosTacletApp getFindTaclet(
335: ListOfNoPosTacletApp taclets, RuleFilter filter,
336: PosInOccurrence pos, Constraint termConstraint,
337: Services services, Constraint userConstraint) {
338: return matchTaclets(taclets, filter, pos, termConstraint,
339: services, userConstraint);
340: }
341:
342: /**
343: * Filter the given list of taclet apps, and match their find
344: * parts at the given position of the sequent
345: */
346: private ListOfNoPosTacletApp matchTaclets(
347: ListOfNoPosTacletApp taclets, RuleFilter p_filter,
348: PosInOccurrence pos, Constraint termConstraint,
349: Services services, Constraint userConstraint) {
350:
351: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
352: if (taclets == null) {
353: return result;
354: }
355:
356: final IteratorOfNoPosTacletApp it = taclets.iterator();
357: while (it.hasNext()) {
358: final NoPosTacletApp tacletApp = it.next();
359:
360: if (!p_filter.filter(tacletApp.taclet())) {
361: continue;
362: }
363:
364: final NoPosTacletApp newTacletApp = tacletApp.matchFind(
365: pos, termConstraint, services, userConstraint);
366:
367: if (newTacletApp != null) {
368: result = result.prepend(newTacletApp);
369: }
370: }
371: return result;
372: }
373:
374: /**
375: * returns a selection from the given map with NoPosTacletApps relevant for
376: * the given program element. Occurring prefix elements are tracked and
377: * taclet applications for them are added.
378: * @param map the map to select the NoPosTacletApps from
379: * @param pe the program element that is used to retrieve the taclets
380: * @param prefixOcc the PrefixOccurrence object used to keep track of the
381: * occuring prefix elements
382: */
383: private ListOfNoPosTacletApp getJavaTacletList(
384: HashMapFromObjectToListOfNoPosTacletApp map,
385: ProgramElement pe, PrefixOccurrences prefixOcc) {
386: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
387: if (pe instanceof ProgramPrefix) {
388: int next = prefixOcc.occurred(pe);
389: NonTerminalProgramElement nt = (NonTerminalProgramElement) pe;
390: if (next < nt.getChildCount()) {
391: return getJavaTacletList(map, nt.getChildAt(next),
392: prefixOcc);
393: }
394: } else {
395: result = map.get(pe.getClass());
396: if (result == null) {
397: result = SLListOfNoPosTacletApp.EMPTY_LIST;
398: }
399: }
400: return result.prepend(prefixOccurrences.getList(map));
401: }
402:
403: private ListOfNoPosTacletApp getListHelp(
404: HashMapFromObjectToListOfNoPosTacletApp map, Term term) {
405: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
406:
407: if (term.op() instanceof Metavariable) {
408: //%% HACK: just take any term operators
409: final IteratorOfObject it = map.keyIterator();
410: while (it.hasNext()) {
411: final Object o = it.next();
412: if (o instanceof Operator)
413: result = result.prepend(map.get(o));
414: }
415: }
416:
417: if (term.op() instanceof IUpdateOperator) {
418: result = getListHelp(map, ((IUpdateOperator) term.op())
419: .target(term));
420: return result;
421: }
422:
423: if (!term.javaBlock().isEmpty()) {
424: prefixOccurrences.reset();
425: StatementBlock sb = (StatementBlock) term.javaBlock()
426: .program();
427: result = getJavaTacletList(map, sb.getStatementAt(0),
428: prefixOccurrences);
429: }
430:
431: if (!term.javaBlock().isEmpty()
432: || term.op() instanceof ProgramVariable) {
433: ListOfNoPosTacletApp schemaList = map
434: .get(SchemaOp.PROGSVOP);
435: if (schemaList != null) {
436: result = result.prepend(schemaList);
437: }
438: }
439:
440: ListOfNoPosTacletApp inMap;
441:
442: if (term.op() instanceof NRFunctionWithExplicitDependencies)
443: inMap = map.get(NRFunctionWithExplicitDependencies.class);
444: else if (term.op() instanceof SortDependingSymbol)
445: inMap = map
446: .get(((SortDependingSymbol) term.op()).getKind());
447: else if (term.op() instanceof AccessOp) {
448: inMap = map.get(AccessOp.class);
449: } else {
450: inMap = map.get(term.op());
451: }
452: if (inMap != null) {
453: result = result.prepend(inMap);
454: }
455: ListOfNoPosTacletApp schemaList = SLListOfNoPosTacletApp.EMPTY_LIST;
456: ListOfNoPosTacletApp schemaList0 = map.get(term.sort());
457: if (schemaList0 != null) {
458: schemaList = schemaList0;
459: }
460:
461: schemaList0 = map.get(SchemaOp.DEFAULTSVOP);
462: if (schemaList0 != null) {
463: schemaList = schemaList.prepend(schemaList0);
464: }
465:
466: schemaList0 = map.get(GenericSort.class);
467: if (schemaList0 != null) {
468: schemaList = schemaList.prepend(schemaList0);
469: }
470:
471: result = result.prepend(schemaList);
472: return result;
473: }
474:
475: /**
476: * creates and returns a selection from the given map of NoPosTacletApps
477: * that are compatible with the given term. It is assumed that the map
478: * (key -> value mapping)
479: * (1) contains keys with the top operator of its value, if no java
480: * block is involved on top level of the value and no update is on top level
481: * (2) contains keys with the class of its top Java operator of its
482: * value's java block, if a java block is involved on the top level
483: * (3) contains keys with the special 'operators' PROGSVOP and
484: * DEFAULTSVOP if the top Java operator or top operator (resp.) of the
485: * value is a program (or variable, resp.) schema variable.
486: * (4) contains keys with the sort of the value if this is an other
487: * schema variable.
488: * If updates are on top level, they are ignored; and indexing starts on
489: * the first level beneath updates.
490: * @param map the map from where to select the taclets
491: * @param term the term that is used to find the selection
492: */
493: private ListOfNoPosTacletApp getList(
494: HashMapFromObjectToListOfNoPosTacletApp map, Term term) {
495: if (term.op() instanceof AnonymousUpdate) {
496: ListOfNoPosTacletApp l = map.get(AnonymousUpdate.class);
497: if (l != null)
498: return getListHelp(map, term).append(l);
499: }
500: if (term.op() instanceof QuanUpdateOperator) {
501: ListOfNoPosTacletApp l = map.get(QuanUpdateOperator.class);
502: if (l != null)
503: return getListHelp(map, term).append(l);
504: }
505: return getListHelp(map, term);
506: }
507:
508: /** get all Taclets for the antecedent.
509: * @param filter Only return taclets the filter selects
510: * @param pos the PosOfOccurrence describing the formula for which to look
511: * for top level taclets
512: * @param services the Services object encapsulating information
513: * about the java datastructures like (static)types etc.
514: * @return ListOfNoPosTacletApp containing all applicable rules
515: * and the corresponding instantiations to get the rule fit.
516: */
517: public ListOfNoPosTacletApp getAntecedentTaclet(
518: PosInOccurrence pos, RuleFilter filter, Services services,
519: Constraint userConstraint) {
520: return getTopLevelTaclets(antecList, filter, pos, services,
521: userConstraint);
522: }
523:
524: /** get all Taclets for the succedent.
525: * @param filter Only return taclets the filter selects
526: * @param pos the PosOfOccurrence describing the formula for which to look
527: * for top level taclets
528: * @param services the Services object encapsulating information
529: * about the java datastructures like (static)types etc.
530: * @return ListOfNoPosTacletApp containing all applicable rules
531: * and the corresponding instantiations to get the rule fit.
532: */
533: public ListOfNoPosTacletApp getSuccedentTaclet(PosInOccurrence pos,
534: RuleFilter filter, Services services,
535: Constraint userConstraint) {
536:
537: return getTopLevelTaclets(succList, filter, pos, services,
538: userConstraint);
539: }
540:
541: private ListOfNoPosTacletApp getTopLevelTaclets(
542: HashMapFromObjectToListOfNoPosTacletApp findTaclets,
543: RuleFilter filter, PosInOccurrence pos, Services services,
544: Constraint userConstraint) {
545:
546: //TODO: afer KeY 1.0 replace the if statement with assert pos.isTopLevel
547: // but currently I don't want to change the methods behaviour
548: if (!pos.isTopLevel())
549: return SLListOfNoPosTacletApp.EMPTY_LIST;
550:
551: final Constraint termConstraint = pos.constrainedFormula()
552: .constraint();
553: return getFindTaclet(getList(rwList, pos.subTerm()), filter,
554: pos, termConstraint, services, userConstraint).prepend(
555: getFindTaclet(getList(findTaclets, pos.subTerm()),
556: filter, pos, termConstraint, services,
557: userConstraint));
558: }
559:
560: /** get all Rewrite-Taclets.
561: * @param filter Only return taclets the filter selects
562: * @param term the Term the Taclet is connected to
563: * @param services the Services object encapsulating information
564: * about the java datastructures like (static)types etc.
565: * @return ListOfNoPosTacletApp containing all applicable rules
566: * and the corresponding instantiations to get the rule fit.
567: */
568: public ListOfNoPosTacletApp getRewriteTaclet(PosInOccurrence pos,
569: Constraint termConstraint, RuleFilter filter,
570: Services services, Constraint userConstraint) {
571: return matchTaclets(getList(rwList, pos.subTerm()), filter,
572: pos, termConstraint, services, userConstraint);
573: }
574:
575: /** get all Taclets having no find expression.
576: * @param filter Only return taclets the filter selects
577: * @param services the Services object encapsulating information
578: * about the java datastructures like (static)types etc.
579: * @return ListOfNoPosTacletApp containing all applicable
580: * rules and an empty part for the instantiations because no
581: * instantiations are necessary.
582: */
583: public ListOfNoPosTacletApp getNoFindTaclet(RuleFilter filter,
584: Services services, Constraint userConstraint) {
585: return matchTaclets(noFindList, filter, null,
586: Constraint.BOTTOM, services, userConstraint);
587: }
588:
589: /**
590: * returns a NoPosTacletApp whose Taclet has a name that equals the given
591: * name. If more Taclets have the same name an arbitrary Taclet with that
592: * name is returned.
593: * @param name the name to lookup
594: * @return the found NoPosTacletApp or null if no matching Taclet is there
595: */
596: public NoPosTacletApp lookup(Name name) {
597: IteratorOfNoPosTacletApp it = allNoPosTacletApps().iterator();
598: while (it.hasNext()) {
599: NoPosTacletApp tacletApp = it.next();
600: if (tacletApp.taclet().name().equals(name)) {
601: return tacletApp;
602: }
603: }
604: return null;
605: }
606:
607: /**
608: * returns a NoPosTacletApp whose Taclet has a name that equals the given
609: * name. If more Taclets have the same name an arbitrary Taclet with that
610: * name is returned.
611: * @param name the name to lookup
612: * @return the found NoPosTacletApp or null if no matching Taclet is there
613: */
614: public NoPosTacletApp lookup(String name) {
615: return lookup(new Name(name));
616: }
617:
618: /**
619: * returns a list with all partial instantiated no pos taclet apps
620: * @return list with all partial instantiated NoPosTacletApps
621: */
622: public ListOfNoPosTacletApp getPartialInstantiatedApps() {
623: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
624: final Iterator it = partialInstantiatedRuleApps.iterator();
625: while (it.hasNext()) {
626: result = result.prepend((NoPosTacletApp) it.next());
627: }
628: return result;
629: }
630:
631: /** toString */
632: public String toString() {
633: StringBuffer sb = new StringBuffer();
634: sb.append("TacletIndex with applicable rules: ");
635: sb.append("ANTEC\n " + antecList);
636: sb.append("\nSUCC\n " + succList);
637: sb.append("\nREWRITE\n " + rwList);
638: sb.append("\nNOFIND\n " + noFindList);
639: return sb.toString();
640: }
641:
642: private static class SchemaOp implements Operator {
643:
644: static SchemaOp DEFAULTSVOP = new SchemaOp();
645: static SchemaOp PROGSVOP = new SchemaOp();
646:
647: private static final Name name = new Name("SVOp");
648: private static final Sort svOpSort = new PrimitiveSort(
649: new Name("SVOp"));
650:
651: private SchemaOp() {
652: }
653:
654: public Name name() {
655: return name;
656: }
657:
658: /**
659: * checks whether the top level structure of the given @link Term
660: * is syntactically valid, given the assumption that the top level
661: * operator of the term is the same as this Operator. The
662: * assumption that the top level operator and the term are equal
663: * is NOT checked.
664: * @return true iff the top level structure of
665: * the @link Term is valid.
666: */
667: public boolean validTopLevel(Term term) {
668: return true;
669: }
670:
671: /**
672: * determines the sort of a @link Term with this Operator as top
673: * operator. The assumption that this Operator and the top level
674: * operator are equal is NOT checked.
675: * @return the sort of the
676: * given Term assumed the top level operator correspnds to this
677: * operator.
678: */
679: public Sort sort(Term[] term) {
680: return svOpSort;
681: }
682:
683: /** @return arity of the Operator as int */
684: public int arity() {
685: return 0;
686: }
687:
688: /**
689: * @return true if the value of "term" having this operator as
690: * top-level operator and may not be changed by modalities
691: */
692: public boolean isRigid(Term term) {
693: return false;
694: }
695:
696: /**
697: * These operators will not be used for matching and so always return null.
698: */
699: public MatchConditions match(SVSubstitute subst,
700: MatchConditions mc, Services services) {
701: return null;
702: }
703:
704: }
705:
706: /**
707: * Inner class to track the occurrences of prefix elements in java blocks
708: */
709: private static class PrefixOccurrences {
710:
711: /**
712: * the classes that represent prefix elements of a java block
713: */
714: static final Class[] prefixClasses = new Class[] {
715: StatementBlock.class, LabeledStatement.class,
716: Try.class, MethodFrame.class, SynchronizedBlock.class };
717:
718: /**
719: * number of prefix types
720: */
721: static final int PREFIXTYPES = prefixClasses.length;
722:
723: /**
724: * field that marks iff the prefix elements have already occurred
725: */
726: private boolean[] occurred = new boolean[PREFIXTYPES];
727:
728: /**
729: * fields to indicate the position of the next relevant child (the next
730: * possible prefix element or real statement
731: */
732: static final int[] nextChild = new int[] { 0, 1, 0, 1, 1 };
733:
734: PrefixOccurrences() {
735: reset();
736: }
737:
738: /**
739: * resets the occurred field to 'nothing has occurred'
740: */
741: public void reset() {
742: for (int i = 0; i < PREFIXTYPES; i++) {
743: occurred[i] = false;
744: }
745: }
746:
747: /**
748: * notification that the given program element has occurred. The occurred
749: * fields are subsequently set.
750: * @param pe the occurred program element
751: * @return the number of the next possible prefix element
752: */
753: public int occurred(ProgramElement pe) {
754: for (int i = 0; i < PREFIXTYPES; i++) {
755: if (prefixClasses[i].isInstance(pe)) {
756: occurred[i] = true;
757: if (pe instanceof MethodFrame) {
758: return (((MethodFrame) pe).getProgramVariable() == null) ? 1
759: : 2;
760: } else {
761: return nextChild[i];
762: }
763: }
764: }
765: return -1;
766: }
767:
768: /**
769: * creates a selection of the given NoPosTacletApp map that comply with the
770: * occurred prefix elements
771: * @param map a map to select from
772: */
773: public ListOfNoPosTacletApp getList(
774: HashMapFromObjectToListOfNoPosTacletApp map) {
775: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
776: for (int i = 0; i < PREFIXTYPES; i++) {
777: if (occurred[i]) {
778: ListOfNoPosTacletApp inMap = map
779: .get(prefixClasses[i]);
780: if (inMap != null) {
781: result = result.prepend(inMap);
782: }
783: }
784: }
785: return result;
786: }
787:
788: }
789:
790: }
|