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: // This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
010: // and Chalmers University of Technology, Sweden
011: //
012: //The KeY system is protected by the GNU General Public License.
013: //See LICENSE.TXT for details.
014: //
015:
016: package de.uka.ilkd.key.rule.export;
017:
018: import java.util.Arrays;
019: import java.util.Comparator;
020: import java.util.HashMap;
021:
022: import de.uka.ilkd.key.logic.Choice;
023: import de.uka.ilkd.key.logic.IteratorOfChoice;
024: import de.uka.ilkd.key.logic.Name;
025: import de.uka.ilkd.key.logic.Named;
026: import de.uka.ilkd.key.proof.*;
027: import de.uka.ilkd.key.rule.*;
028:
029: public class RuleExportModel {
030:
031: // keys: String, values: DisplayNameModelInfo
032: private HashMap string2displayName = new HashMap();
033: // keys: RuleSet, values: RuleSetModelInfo
034: private HashMap ruleSet2info = new HashMap();
035: // keys: String, values: CategoryModelInfo
036: private HashMap category2info = new HashMap();
037: // keys: Choice, values: OptionModelInfo
038: private HashMap choice2info = new HashMap();
039:
040: private ListOfTacletModelInfo taclets;
041: private ListOfRuleSetModelInfo ruleSets;
042: private ListOfDisplayNameModelInfo displayNames;
043: private ListOfOptionModelInfo options;
044: private ListOfCategoryModelInfo categories;
045: private final RuleFilter[] virtualRSFilterArray;
046: private final RuleSetModelInfo[] virtualRSModelInfoArray;
047:
048: private static final String rsClosureDefinition = "Contains all taclets that create zero new goals.";
049: private static final String rsSplitDefinition = "Contains all taclets that create more than one new goal.";
050: private static final String rsUnassignedDefinition = "Contains all taclets that are not assigned an explicit rule set.";
051:
052: public RuleExportModel() {
053: taclets = SLListOfTacletModelInfo.EMPTY_LIST;
054: ruleSets = SLListOfRuleSetModelInfo.EMPTY_LIST;
055: displayNames = SLListOfDisplayNameModelInfo.EMPTY_LIST;
056: options = SLListOfOptionModelInfo.EMPTY_LIST;
057: virtualRSFilterArray = new RuleFilter[] {
058: TacletFilterCloseGoal.INSTANCE,
059: TacletFilterSplitGoal.INSTANCE,
060: new NotRuleFilter(AnyRuleSetTacletFilter.INSTANCE) };
061: virtualRSModelInfoArray = new RuleSetModelInfo[] {
062: new RuleSetModelInfo(
063: new RuleSet(new Name("<closure>")),
064: rsClosureDefinition, true),
065: new RuleSetModelInfo(new RuleSet(new Name("<split>")),
066: rsSplitDefinition, true),
067: new RuleSetModelInfo(new RuleSet(new Name(
068: "<unassigned>")), rsUnassignedDefinition, true) };
069: ruleSets = ruleSets.append(virtualRSModelInfoArray);
070: }
071:
072: private void addIntroducedTaclets(TacletModelInfo tinfo,
073: String filename) {
074: final Taclet t = tinfo.getTaclet();
075: IteratorOfTacletGoalTemplate it = t.goalTemplates().iterator();
076: while (it.hasNext()) {
077: final TacletGoalTemplate gt = it.next();
078:
079: addTaclets(gt.rules(), filename, tinfo);
080: }
081: }
082:
083: public void addTaclet(Taclet t, String filename) {
084: addTaclet(t, filename, null);
085: }
086:
087: private void addTaclet(Taclet t, String filename,
088: TacletModelInfo introducer) {
089: // add taclet
090: final TacletModelInfo tinfo = new TacletModelInfo(t, filename);
091: taclets = taclets.prepend(tinfo);
092: tinfo.setIntroducingTaclet(introducer);
093:
094: addIntroducedTaclets(tinfo, filename);
095:
096: // add display name
097: addDisplayName(tinfo);
098:
099: // add rule sets
100: addRuleSets(tinfo);
101:
102: // add options
103: addOptions(tinfo);
104: }
105:
106: private void addDisplayName(TacletModelInfo tinfo) {
107: final Taclet t = tinfo.getTaclet();
108: DisplayNameModelInfo dninfo = getTacletDisplayName(t);
109: if (dninfo == null) {
110: String s = t.displayName();
111: dninfo = new DisplayNameModelInfo(s);
112: string2displayName.put(s, dninfo);
113: displayNames = displayNames.prepend(dninfo);
114: }
115: dninfo.addTaclet(tinfo);
116: tinfo.setDisplayName(dninfo);
117: }
118:
119: private void addOptions(TacletModelInfo tinfo) {
120: final Taclet t = tinfo.getTaclet();
121: final IteratorOfChoice it = t.getChoices().iterator();
122: while (it.hasNext()) {
123: final Choice c = it.next();
124: OptionModelInfo opt = addOption(c);
125: opt.addTaclet(tinfo);
126: tinfo.addOption(opt);
127: }
128: }
129:
130: private OptionModelInfo addOption(Choice c) {
131: OptionModelInfo opt = (OptionModelInfo) choice2info.get(c);
132: if (opt == null) {
133: opt = new OptionModelInfo(c);
134: choice2info.put(c, opt);
135: options = options.prepend(opt);
136: }
137:
138: CategoryModelInfo cat = addCategory(opt);
139: opt.setCategory(cat);
140: return opt;
141: }
142:
143: private CategoryModelInfo addCategory(OptionModelInfo opt) {
144: final Choice c = opt.getChoice();
145: CategoryModelInfo cat = (CategoryModelInfo) category2info.get(c
146: .category());
147: if (cat == null) {
148: cat = new CategoryModelInfo(c.category());
149: category2info.put(c.category(), cat);
150: }
151: cat.addOption(opt);
152: return cat;
153: }
154:
155: private void addRuleSets(TacletModelInfo tinfo) {
156: final Taclet t = tinfo.getTaclet();
157: // handle regular rule sets
158: final IteratorOfRuleSet it = t.ruleSets();
159: while (it.hasNext()) {
160: final RuleSet rs = it.next();
161: RuleSetModelInfo rsinfo = (RuleSetModelInfo) ruleSet2info
162: .get(rs);
163: if (rsinfo == null) {
164: rsinfo = new RuleSetModelInfo(rs);
165: ruleSet2info.put(rs, rsinfo);
166: ruleSets = ruleSets.prepend(rsinfo);
167: }
168: rsinfo.addTaclet(tinfo);
169: tinfo.addRuleSet(rsinfo);
170: }
171: // handle virtual rule sets
172: for (int n = 0; n < virtualRSFilterArray.length; n++) {
173: if (virtualRSFilterArray[n].filter(t)) {
174: final RuleSetModelInfo rsinfo = virtualRSModelInfoArray[n];
175: rsinfo.addTaclet(tinfo);
176: tinfo.addRuleSet(rsinfo);
177: }
178: }
179: }
180:
181: private void addTaclets(ListOfTaclet tacletList, String filename,
182: TacletModelInfo introducer) {
183: final IteratorOfTaclet it = tacletList.iterator();
184: while (it.hasNext()) {
185: final Taclet t = it.next();
186: addTaclet(t, filename, introducer);
187: }
188: }
189:
190: public void addTaclets(ListOfTaclet tacletList, String filename) {
191: addTaclets(tacletList, filename, null);
192: }
193:
194: public void analyze() {
195: taclets = sortTaclets(taclets);
196:
197: ruleSets = sortRuleSets(ruleSets);
198:
199: options = sortOptions(options);
200:
201: displayNames = sortDisplayNames(displayNames);
202:
203: analyzeDisplayNames();
204:
205: analyzeCategories();
206:
207: analyzeOptions();
208:
209: analyzeRuleSets();
210:
211: analyzeTaclets();
212: }
213:
214: private void analyzeTaclets() {
215: final IteratorOfTacletModelInfo it = taclets();
216: while (it.hasNext()) {
217: final TacletModelInfo t = it.next();
218: t.setOptions(sortOptions(t.getOptions()));
219: t.setRuleSets(sortRuleSets(t.getRuleSets()));
220: }
221: }
222:
223: private void analyzeOptions() {
224: final IteratorOfOptionModelInfo it = options();
225: while (it.hasNext()) {
226: final OptionModelInfo opt = it.next();
227: opt.setTaclets(sortTaclets(opt.getTaclets()));
228: }
229: }
230:
231: private void analyzeDisplayNames() {
232: final IteratorOfDisplayNameModelInfo it = displayNames();
233: while (it.hasNext()) {
234: final DisplayNameModelInfo dn = it.next();
235: dn.setTaclets(sortTaclets(dn.getTaclets()));
236: }
237: }
238:
239: /**
240: *
241: */
242: private void analyzeCategories() {
243: Object[] objArray = category2info.values().toArray();
244: CategoryModelInfo[] catArray = new CategoryModelInfo[objArray.length];
245: for (int n = 0; n < objArray.length; n++) {
246: catArray[n] = (CategoryModelInfo) objArray[n];
247: }
248: Arrays.sort(catArray);
249: categories = SLListOfCategoryModelInfo.EMPTY_LIST
250: .prepend(catArray);
251:
252: IteratorOfCategoryModelInfo it = categories.iterator();
253: while (it.hasNext()) {
254: final CategoryModelInfo cat = it.next();
255: cat.setOptions(sortOptions(cat.getOptions()));
256: }
257: }
258:
259: private void analyzeRuleSets() {
260: ListOfRuleSetModelInfo outer = ruleSets;
261: while (!outer.isEmpty()) {
262: final RuleSetModelInfo ruleSet = outer.head();
263: outer = outer.tail();
264:
265: ruleSet.setTaclets(sortTaclets(ruleSet.getTaclets()));
266:
267: ListOfRuleSetModelInfo inner = outer;
268: while (!inner.isEmpty()) {
269: final RuleSetModelInfo ruleSet2 = inner.head();
270: inner = inner.tail();
271:
272: analyzeRuleSetRelationship(ruleSet, ruleSet2);
273: }
274:
275: }
276: }
277:
278: private void analyzeRuleSetRelationship(RuleSetModelInfo rs,
279: RuleSetModelInfo rs2) {
280: ListOfTacletModelInfo list = rs.getTaclets();
281: ListOfTacletModelInfo list2 = rs2.getTaclets();
282:
283: int a = countOccurences(list, list2);
284: int b = countOccurences(list2, list);
285:
286: if (a == list.size()) {
287: // rule set 1 is a subset of rule set 2
288: if (b == list2.size()) {
289: // both rule sets are equal
290: rs.addEqualSet(rs2);
291: rs2.addEqualSet(rs);
292: } else {
293: // rule set 1 is a true subset of rule set 2
294: rs.addSuperSet(rs2);
295: rs2.addSubSet(rs);
296: }
297: } else if (b == list2.size()) {
298: // rule set 2 is a true subset of rule set 1
299: rs.addSubSet(rs2);
300: rs2.addSuperSet(rs);
301: } else if (a > 0) {
302: // both rule sets intersect
303: rs.addIntersectingSet(rs2);
304: rs2.addIntersectingSet(rs);
305: }
306: }
307:
308: /**
309: * Counts the number of taclets from one list that are contained in a second
310: * list.
311: */
312: private int countOccurences(ListOfTacletModelInfo a,
313: ListOfTacletModelInfo b) {
314: int result = 0;
315:
316: final IteratorOfTacletModelInfo it = a.iterator();
317: while (it.hasNext()) {
318: final TacletModelInfo t = it.next();
319:
320: if (b.contains(t))
321: result++;
322: }
323:
324: return result;
325: }
326:
327: private ListOfRuleSetModelInfo sortRuleSets(
328: ListOfRuleSetModelInfo ruleSetList) {
329: RuleSetModelInfo[] ruleSetArray = ruleSetList.toArray();
330: Arrays.sort(ruleSetArray, new NamedComparator());
331: return SLListOfRuleSetModelInfo.EMPTY_LIST
332: .prepend(ruleSetArray);
333: }
334:
335: private ListOfTacletModelInfo sortTaclets(
336: ListOfTacletModelInfo tacletList) {
337: TacletModelInfo[] tacletArray = tacletList.toArray();
338: Arrays.sort(tacletArray, new NamedComparator());
339: return SLListOfTacletModelInfo.EMPTY_LIST.prepend(tacletArray);
340: }
341:
342: private ListOfOptionModelInfo sortOptions(
343: ListOfOptionModelInfo optionList) {
344: OptionModelInfo[] optionArray = optionList.toArray();
345: Arrays.sort(optionArray, new NamedComparator());
346: return SLListOfOptionModelInfo.EMPTY_LIST.prepend(optionArray);
347: }
348:
349: private ListOfDisplayNameModelInfo sortDisplayNames(
350: ListOfDisplayNameModelInfo displayNames) {
351: DisplayNameModelInfo[] displayNameArray = displayNames
352: .toArray();
353: Arrays.sort(displayNameArray);
354: return SLListOfDisplayNameModelInfo.EMPTY_LIST
355: .prepend(displayNameArray);
356: }
357:
358: public ListOfTacletModelInfo getTaclets() {
359: return taclets;
360: }
361:
362: public IteratorOfTacletModelInfo taclets() {
363: return getTaclets().iterator();
364: }
365:
366: public ListOfRuleSetModelInfo getRuleSets() {
367: return ruleSets;
368: }
369:
370: public IteratorOfRuleSetModelInfo ruleSets() {
371: return getRuleSets().iterator();
372: }
373:
374: public ListOfDisplayNameModelInfo getDisplayNames() {
375: return displayNames;
376: }
377:
378: public IteratorOfDisplayNameModelInfo displayNames() {
379: return displayNames.iterator();
380: }
381:
382: public ListOfOptionModelInfo getOptions() {
383: return options;
384: }
385:
386: public IteratorOfOptionModelInfo options() {
387: return getOptions().iterator();
388: }
389:
390: public ListOfCategoryModelInfo getCategories() {
391: return categories;
392: }
393:
394: public IteratorOfCategoryModelInfo categories() {
395: return categories.iterator();
396: }
397:
398: private DisplayNameModelInfo getTacletDisplayName(Taclet t) {
399: return (DisplayNameModelInfo) string2displayName.get(t
400: .displayName());
401: }
402:
403: private static class NamedComparator implements Comparator {
404:
405: public int compare(Object a, Object b) {
406: return ((Named) a).name().compareTo(((Named) b).name());
407: }
408: }
409: }
|