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: //This file is part of KeY - Integrated Deductive Software Design
010: //Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: //Universitaet Koblenz-Landau, Germany
012: //Chalmers University of Technology, Sweden
013: //
014: //The KeY system is protected by the GNU General Public License.
015: //See LICENSE.TXT for details.
016: //
017: //
018:
019: package de.uka.ilkd.key.proof;
020:
021: import java.util.*;
022:
023: import javax.swing.tree.DefaultMutableTreeNode;
024: import javax.swing.tree.DefaultTreeModel;
025: import javax.swing.tree.MutableTreeNode;
026:
027: import de.uka.ilkd.key.casetool.ModelMethod;
028: import de.uka.ilkd.key.proof.mgt.Contract;
029: import de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt;
030: import de.uka.ilkd.key.proof.mgt.RuleJustification;
031: import de.uka.ilkd.key.proof.mgt.RuleJustificationBySpec;
032: import de.uka.ilkd.key.rule.*;
033:
034: public class RuleTreeModel extends DefaultTreeModel {
035:
036: protected Goal goal;
037: protected MutableTreeNode axiomTacletRoot = new DefaultMutableTreeNode(
038: "Taclet Base");
039: protected MutableTreeNode builtInRoot = new DefaultMutableTreeNode(
040: "Built-In");
041: protected MutableTreeNode lemmaRoot = new DefaultMutableTreeNode(
042: "Lemmas");
043: protected MutableTreeNode methcontrRoot = new DefaultMutableTreeNode(
044: "Method Contracts");
045: protected MutableTreeNode contrRoot = new DefaultMutableTreeNode(
046: "DL Contracts");
047: protected MutableTreeNode proveableTacletsRoot = new DefaultMutableTreeNode(
048: "Auxiliary Taclets");
049:
050: public RuleTreeModel(Goal g) {
051: super (new DefaultMutableTreeNode("Rule Base"));
052: this .goal = g;
053: insertAsLast(builtInRoot, (MutableTreeNode) getRoot());
054: insertAsLast(axiomTacletRoot, (MutableTreeNode) getRoot());
055: insertAsLast(lemmaRoot, (MutableTreeNode) getRoot());
056: insertAsLast(proveableTacletsRoot, lemmaRoot);
057: insertAsLast(methcontrRoot, lemmaRoot);
058: insertAsLast(contrRoot, lemmaRoot);
059: if (g != null)
060: rulesForGoal(g);
061: }
062:
063: private void insertAsLast(MutableTreeNode ins,
064: MutableTreeNode parent) {
065: insertNodeInto(ins, parent, parent.getChildCount());
066: }
067:
068: /** groups subsequent insertions with the same name under a new node */
069: private void insertAndGroup(MutableTreeNode ins,
070: MutableTreeNode parent) {
071: DefaultMutableTreeNode insNode = (DefaultMutableTreeNode) ins;
072: if (parent.getChildCount() > 0) {
073: DefaultMutableTreeNode lastNode = (DefaultMutableTreeNode) parent
074: .getChildAt(parent.getChildCount() - 1);
075: if (getName(insNode).equals(getName(lastNode))) {
076: if (lastNode.getChildCount() == 0) {
077: removeNodeFromParent(lastNode);
078: MutableTreeNode oldParent = parent;
079: parent = new DefaultMutableTreeNode(
080: getName(insNode));
081: insertAsLast(parent, oldParent);
082: insertAsLast(lastNode, parent);
083: } else {
084: parent = lastNode;
085: }
086: }
087: }
088: insertAsLast(ins, parent);
089: }
090:
091: private String getName(DefaultMutableTreeNode t1) {
092: if (t1.getUserObject() instanceof Taclet) {
093: return ((Taclet) t1.getUserObject()).displayName();
094: } else {
095: return t1.toString();
096: }
097: }
098:
099: private void rulesForGoal(Goal g) {
100: IteratorOfBuiltInRule rit = getBuiltInIndex().rules()
101: .iterator();
102: while (rit.hasNext()) {
103: BuiltInRule br = rit.next();
104: insertAsLast(new DefaultMutableTreeNode(br), builtInRoot);
105: }
106: List apps = sort(getTacletIndex().allNoPosTacletApps());
107: Iterator it = apps.iterator();
108: while (it.hasNext()) {
109: NoPosTacletApp app = (NoPosTacletApp) it.next();
110: RuleJustification just = mgt().getJustification(app);
111: if (just == null)
112: continue; // do not break system because of this
113: if (just.isAxiomJustification()) {
114: insertAndGroup(
115: new DefaultMutableTreeNode(app.taclet()),
116: axiomTacletRoot);
117: } else if (just instanceof RuleJustificationBySpec) {
118: RuleJustificationBySpec specJust = (RuleJustificationBySpec) just;
119: Contract ct = specJust.getContract();
120: if (ct.getObjectOfContract() instanceof ModelMethod) {
121: insertMethodNodeInto((ModelMethod) ct
122: .getObjectOfContract(), ct);
123: } else if (ct.getObjectOfContract() instanceof NoPosTacletApp) {
124: insertAndGroup(new DefaultMutableTreeNode(app
125: .taclet()), proveableTacletsRoot);
126: } else {
127: insertAsLast(new DefaultMutableTreeNode(ct),
128: contrRoot);
129: }
130: }
131: }
132: }
133:
134: private List sort(SetOfNoPosTacletApp apps) {
135: List l = new ArrayList(apps.size());
136: IteratorOfNoPosTacletApp it = apps.iterator();
137: int i = 0;
138: while (it.hasNext()) {
139: l.add(i++, it.next());
140: }
141: Collections.sort(l, new Comparator() {
142: public int compare(Object o1, Object o2) {
143: Taclet t1 = ((NoPosTacletApp) o1).taclet();
144: Taclet t2 = ((NoPosTacletApp) o2).taclet();
145: return (t1.displayName().compareTo(t2.displayName()));
146: }
147: });
148: return l;
149: }
150:
151: private void insertMethodNodeInto(ModelMethod meth, Contract ct) {
152: MutableTreeNode methNode = null;
153: for (int i = 0; i < methcontrRoot.getChildCount(); i++) {
154: if (((DefaultMutableTreeNode) methcontrRoot.getChildAt(i))
155: .getUserObject().equals(meth)) {
156: methNode = (MutableTreeNode) methcontrRoot
157: .getChildAt(i);
158: }
159: }
160: if (methNode == null) {
161: methNode = new DefaultMutableTreeNode(meth);
162: insertAsLast(methNode, methcontrRoot);
163: }
164: insertAsLast(new DefaultMutableTreeNode(ct), methNode);
165: }
166:
167: private TacletIndex getTacletIndex() {
168: return goal.ruleAppIndex().tacletIndex();
169: }
170:
171: private BuiltInRuleIndex getBuiltInIndex() {
172: RuleAppIndex ri = goal.ruleAppIndex();
173: return ri.builtInRuleAppIndex().builtInRuleIndex();
174: }
175:
176: public ProofCorrectnessMgt mgt() {
177: return goal.proof().mgt();
178: }
179:
180: public void setSelectedGoal(Goal g) {
181: goal = g;
182: }
183:
184: public Goal getGoal() {
185: return goal;
186: }
187:
188: }
|