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: package de.uka.ilkd.key.gui.nodeviews;
011:
012: import java.awt.Component;
013: import java.awt.event.ActionEvent;
014: import java.awt.event.ActionListener;
015: import java.util.*;
016:
017: import javax.swing.*;
018:
019: import org.apache.log4j.Logger;
020:
021: import de.uka.ilkd.key.gui.KeYMediator;
022: import de.uka.ilkd.key.gui.Main;
023: import de.uka.ilkd.key.gui.UseMethodContractRuleItem;
024: import de.uka.ilkd.key.gui.nodeviews.*;
025: import de.uka.ilkd.key.java.ProgramElement;
026: import de.uka.ilkd.key.logic.*;
027: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
028: import de.uka.ilkd.key.logic.op.ProgramVariable;
029: import de.uka.ilkd.key.logic.op.SchemaVariable;
030: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
031: import de.uka.ilkd.key.logic.sort.Sort;
032: import de.uka.ilkd.key.pp.AbbrevException;
033: import de.uka.ilkd.key.pp.AbbrevMap;
034: import de.uka.ilkd.key.pp.PosInSequent;
035: import de.uka.ilkd.key.rule.*;
036:
037: /**
038: * This class creates a menu with Taclets as entries. The invoker has
039: * to be of type SequentView because of the method call selectedTaclet
040: * that hands over the selected Taclet. The class is used to get all
041: * Taclet that are applicable at a selected position in a sequent.
042: */
043: class TacletMenu extends JMenu {
044:
045: private PosInSequent pos;
046: private SequentView sequentView;
047: private KeYMediator mediator;
048:
049: private TacletAppComparator comp = new TacletAppComparator();
050:
051: static Logger logger = Logger.getLogger(TacletMenu.class.getName());
052:
053: /**
054: * creates empty menu
055: */
056: TacletMenu() {
057: }
058:
059: /** creates a new menu that displays all applicable rules at the given
060: * position
061: * @param sequentView the SequentView that is the parent of this menu
062: * @param findList ListOfTaclet with all applicable FindTaclets
063: * @param rewriteList ListOfTaclet with all applicable RewriteTaclets
064: * @param noFindList ListOfTaclet with all applicable noFindTaclets
065: * @param builtInList ListOfBuiltInRule with all applicable BuiltInRules
066: * @param pos the PosInSequent
067: */
068: TacletMenu(SequentView sequentView, ListOfTacletApp findList,
069: ListOfTacletApp rewriteList, ListOfTacletApp noFindList,
070: ListOfBuiltInRule builtInList, PosInSequent pos) {
071: super ();
072: this .sequentView = sequentView;
073: this .mediator = sequentView.mediator();
074: this .pos = pos;
075: // delete RewriteTaclet from findList because they will be in
076: // the rewrite list and concatenate both lists
077: createTacletMenu(removeRewrites(findList).prepend(rewriteList),
078: noFindList, builtInList, new MenuControl());
079: }
080:
081: /** removes RewriteTaclet from list
082: * @param list the ListOfTaclet from where the RewriteTaclet are
083: * removed
084: * @return list without RewriteTaclets
085: */
086: private ListOfTacletApp removeRewrites(ListOfTacletApp list) {
087: ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
088: IteratorOfTacletApp it = list.iterator();
089:
090: while (it.hasNext()) {
091: TacletApp tacletApp = it.next();
092: Taclet taclet = tacletApp.taclet();
093: result = (taclet instanceof RewriteTaclet ? result : result
094: .prepend(tacletApp));
095: }
096: return result;
097: }
098:
099: /** creates the menu by adding all submenus and items */
100: private void createTacletMenu(ListOfTacletApp find,
101: ListOfTacletApp noFind, ListOfBuiltInRule builtInList,
102: MenuControl control) {
103: addActionListener(control);
104: boolean rulesAvailable = (addSection("Find", sort(find),
105: control));
106: if (pos != null && pos.isSequent()) {
107: rulesAvailable = addSection("NoFind", noFind, control)
108: | rulesAvailable;
109: }
110: if (!rulesAvailable) {
111: createSection("No rules applicable.");
112: }
113:
114: createBuiltInRuleMenu(builtInList, control);
115:
116: createFocussedAutoModeMenu(control);
117:
118: // addPopFrameItem(control);
119:
120: addClipboardItem(control);
121:
122: if (pos != null) {
123: PosInOccurrence occ = pos.getPosInOccurrence();
124: if (occ != null && occ.posInTerm() != null) {
125: Term t = occ.subTerm();
126: createAbbrevSection(t, control);
127:
128: if (t.op() instanceof ProgramVariable) {
129: ProgramVariable var = (ProgramVariable) t.op();
130: if (var.getProgramElementName().getCreationInfo() != null) {
131: createNameCreationInfoSection(control);
132: }
133: }
134: }
135: }
136: }
137:
138: private void createBuiltInRuleMenu(ListOfBuiltInRule builtInList,
139: MenuControl control) {
140:
141: if (builtInList != SLListOfBuiltInRule.EMPTY_LIST) {
142: addSeparator();
143: IteratorOfBuiltInRule it = builtInList.iterator();
144: while (it.hasNext()) {
145: addBuiltInRuleItem(it.next(), control);
146: }
147: }
148: }
149:
150: /**
151: * adds an item for built in rules (e.g. Run Simplify or Update Simplifier)
152: */
153: private void addBuiltInRuleItem(BuiltInRule builtInRule,
154: MenuControl control) {
155: JMenuItem item;
156: if (builtInRule instanceof UseMethodContractRule) {
157: item = new UseMethodContractRuleItem(mediator.mainFrame(),
158: (UseMethodContractRule) builtInRule, mediator
159: .getSelectedProof(), pos
160: .getPosInOccurrence());
161: } else {
162: item = new DefaultBuiltInRuleMenuItem(builtInRule);
163: }
164: item.addActionListener(control);
165: add(item);
166: }
167:
168: private void createFocussedAutoModeMenu(MenuControl control) {
169: addSeparator();
170: JMenuItem item = new FocussedRuleApplicationMenuItem();
171: item.addActionListener(control);
172: add(item);
173: }
174:
175: private ListOfTacletApp sort(ListOfTacletApp finds) {
176: ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
177: List list = new ArrayList(finds.size());
178:
179: IteratorOfTacletApp it = finds.iterator();
180: while (it.hasNext()) {
181: list.add(it.next());
182: }
183:
184: Collections.sort(list, comp);
185:
186: Iterator it2 = list.iterator();
187: while (it2.hasNext()) {
188: result = result.prepend((TacletApp) it2.next());
189: }
190:
191: return result;
192: }
193:
194: private void createAbbrevSection(Term t, MenuControl control) {
195: AbbrevMap scm = mediator.getNotationInfo().getAbbrevMap();
196: JMenuItem sc = null;
197: if (scm.containsTerm(t)) {
198: sc = new JMenuItem("Change abbreviation");
199: sc.addActionListener(control);
200: add(sc);
201: if (scm.isEnabled(t)) {
202: sc = new JMenuItem("Disable abbreviation");
203: } else {
204: sc = new JMenuItem("Enable abbreviation");
205: }
206: } else {
207: sc = new JMenuItem("Create abbreviation");
208: }
209: sc.addActionListener(control);
210: add(sc);
211: }
212:
213: private void createNameCreationInfoSection(MenuControl control) {
214: JMenuItem item = new JMenuItem("View name creation info...");
215: item.addActionListener(control);
216: add(item);
217: }
218:
219: /** creates a non selectable label with the specified name and adds it to
220: * the component followed by the entries of this section
221: * @param title a String the title of the section
222: * @param taclet ListOfTaclet that contains the Taclets belonging to this section
223: * @return true if section has been added (empty sections are not added)
224: */
225: private boolean addSection(String title, ListOfTacletApp taclet,
226: MenuControl control) {
227: if (taclet.size() > 0) {
228: //uncomment if you want submenus with subtitels
229: // insert(createSubMenu(taclet, title, control), 1);
230: // createSection(title);
231: add(createMenuItems(taclet, control));
232: return true;
233: }
234: return false;
235: }
236:
237: /** inserts separator followed from the section's title
238: * @param title a String that contains the title of the section
239: */
240: private void createSection(String title) {
241: //addSeparator();
242: add(new JLabel(title));
243: }
244:
245: private void addPopFrameItem(MenuControl control) {
246: JMenuItem item = new JMenuItem("Pop method frame");
247: item.addActionListener(control);
248: add(item);
249: }
250:
251: private void addClipboardItem(MenuControl control) {
252: addSeparator();
253: JMenuItem item = new JMenuItem("to clipboard");
254: item.addActionListener(control);
255: add(item);
256: }
257:
258: /** adds array of TacletMenuItem to itself*/
259: private void add(TacletMenuItem[] items) {
260: for (int i = 0; i < items.length; i++) {
261: add((Component) items[i]);
262: }
263: }
264:
265: /** creates new TacletMenuItems for each taclet in the list and set
266: * the given MenuControl as their ActionListener
267: * @param taclets ListOfTaclet with the Taclets the items represent
268: * @param control the ActionListener
269: * @return the new MenuItems
270: */
271: private TacletMenuItem[] createMenuItems(ListOfTacletApp taclets,
272: MenuControl control) {
273: List items = new LinkedList();
274: IteratorOfTacletApp it = taclets.iterator();
275:
276: final InsertHiddenTacletMenuItem insHiddenItem = new InsertHiddenTacletMenuItem(
277: mediator.mainFrame(), mediator.getNotationInfo(),
278: mediator.getServices());
279:
280: final InsertionTacletBrowserMenuItem insSystemInvItem = new InsertSystemInvariantTacletMenuItem(
281: mediator.mainFrame(), mediator.getNotationInfo(),
282: mediator.getServices());
283:
284: for (int i = 0; it.hasNext(); i++) {
285: final TacletApp app = it.next();
286:
287: final Taclet taclet = app.taclet();
288: if (insHiddenItem.isResponsible(taclet)) {
289: insHiddenItem.add(app);
290: } else if (insSystemInvItem.isResponsible(taclet)) {
291: insSystemInvItem.add(app);
292: } else {
293: final TacletMenuItem item = new DefaultTacletMenuItem(
294: this , app, mediator.getNotationInfo());
295: item.addActionListener(control);
296: items.add(item);
297: }
298: }
299:
300: if (insHiddenItem.getAppSize() > 0) {
301: items.add(0, insHiddenItem);
302: insHiddenItem.addActionListener(control);
303: }
304:
305: if (insSystemInvItem.getAppSize() > 0) {
306: items.add(0, insSystemInvItem);
307: insSystemInvItem.addActionListener(control);
308: }
309:
310: return (TacletMenuItem[]) items
311: .toArray(new TacletMenuItem[items.size()]);
312: }
313:
314: /** makes submenus invisible */
315: void invisible() {
316: for (int i = 0; i < getMenuComponentCount(); i++) {
317: if (getMenuComponent(i) instanceof JMenu)
318: ((JMenu) getMenuComponent(i)).getPopupMenu()
319: .setVisible(false);
320: }
321: }
322:
323: /** ActionListener */
324: class MenuControl implements ActionListener {
325:
326: private boolean validabbreviation(String s) {
327: if (s == null || s.length() == 0)
328: return false;
329: for (int i = 0; i < s.length(); i++) {
330: if (!((s.charAt(i) <= '9' && s.charAt(i) >= '0')
331: || (s.charAt(i) <= 'z' && s.charAt(i) >= 'a')
332: || (s.charAt(i) <= 'Z' && s.charAt(i) >= 'A') || s
333: .charAt(i) == '_'))
334: return false;
335: }
336: return true;
337: }
338:
339: public void actionPerformed(ActionEvent e) {
340: if (e.getSource() instanceof TacletMenuItem) {
341: ((SequentView) (getPopupMenu().getInvoker()))
342: .selectedTaclet(
343: ((TacletMenuItem) e.getSource())
344: .connectedTo(), pos);
345: } else if (e.getSource() instanceof UseMethodContractRuleItem) {
346: mediator
347: .selectedUseMethodContractRule(((UseMethodContractRuleItem) e
348: .getSource()).getRuleApp());
349: } else if (e.getSource() instanceof BuiltInRuleMenuItem) {
350: mediator.selectedBuiltInRule(((BuiltInRuleMenuItem) e
351: .getSource()).connectedTo(), pos
352: .getPosInOccurrence());
353: } else if (e.getSource() instanceof FocussedRuleApplicationMenuItem) {
354: mediator.getInteractiveProver().startFocussedAutoMode(
355: pos.getPosInOccurrence(),
356: mediator.getSelectedGoal());
357: } else {
358: if (((JMenuItem) e.getSource()).getText().startsWith(
359: "to clipboard")) {
360: Main.copyHighlightToClipboard(sequentView);
361: } else if (((JMenuItem) e.getSource()).getText()
362: .startsWith("Pop method frame")) {
363: // mediator.popMethodFrame();
364: } else if (((JMenuItem) e.getSource()).getText()
365: .startsWith("Disable abbreviation")) {
366: PosInOccurrence occ = pos.getPosInOccurrence();
367: if (occ != null && occ.posInTerm() != null) {
368: mediator.getNotationInfo().getAbbrevMap()
369: .setEnabled(occ.subTerm(), false);
370: sequentView.printSequent();
371: }
372: } else if (((JMenuItem) e.getSource()).getText()
373: .startsWith("Enable abbreviation")) {
374: PosInOccurrence occ = pos.getPosInOccurrence();
375: if (occ != null && occ.posInTerm() != null) {
376: mediator.getNotationInfo().getAbbrevMap()
377: .setEnabled(occ.subTerm(), true);
378: sequentView.printSequent();
379: }
380: } else if (((JMenuItem) e.getSource()).getText()
381: .startsWith("Create abbreviation")) {
382: PosInOccurrence occ = pos.getPosInOccurrence();
383: if (occ != null && occ.posInTerm() != null) {
384: String abbreviation = (String) JOptionPane
385: .showInputDialog(new JFrame(),
386: "Enter abbreviation for term: \n"
387: + occ.subTerm()
388: .toString(),
389: "New Abbreviation",
390: JOptionPane.QUESTION_MESSAGE,
391: null, null, "");
392:
393: try {
394: if (abbreviation != null) {
395: if (!validabbreviation(abbreviation)) {
396: JOptionPane
397: .showMessageDialog(
398: new JFrame(),
399: "Only letters, numbers and '_' are allowed for Abbreviations",
400: "Sorry",
401: JOptionPane.INFORMATION_MESSAGE);
402: } else {
403: mediator.getNotationInfo()
404: .getAbbrevMap().put(
405: occ.subTerm(),
406: abbreviation, true);
407: sequentView.printSequent();
408: }
409: }
410: } catch (AbbrevException sce) {
411: JOptionPane.showMessageDialog(new JFrame(),
412: sce.getMessage(), "Sorry",
413: JOptionPane.INFORMATION_MESSAGE);
414: }
415: }
416:
417: } else if (((JMenuItem) e.getSource()).getText()
418: .startsWith("Change abbreviation")) {
419: PosInOccurrence occ = pos.getPosInOccurrence();
420: if (occ != null && occ.posInTerm() != null) {
421: String abbreviation = (String) JOptionPane
422: .showInputDialog(new JFrame(),
423: "Enter abbreviation for term: \n"
424: + occ.subTerm()
425: .toString(),
426: "Change Abbreviation",
427: JOptionPane.QUESTION_MESSAGE,
428: null, null, mediator
429: .getNotationInfo()
430: .getAbbrevMap()
431: .getAbbrev(
432: occ.subTerm())
433: .substring(1));
434: try {
435: if (abbreviation != null) {
436: if (!validabbreviation(abbreviation)) {
437: JOptionPane
438: .showMessageDialog(
439: new JFrame(),
440: "Only letters, numbers and '_' are allowed for Abbreviations",
441: "Sorry",
442: JOptionPane.INFORMATION_MESSAGE);
443: } else {
444: mediator.getNotationInfo()
445: .getAbbrevMap()
446: .changeAbbrev(
447: occ.subTerm(),
448: abbreviation);
449: sequentView.printSequent();
450: }
451: }
452: } catch (AbbrevException sce) {
453: JOptionPane.showMessageDialog(new JFrame(),
454: sce.getMessage(), "Sorry",
455: JOptionPane.INFORMATION_MESSAGE);
456: }
457: }
458: } else if (((JMenuItem) e.getSource()).getText()
459: .startsWith("View name creation info")) {
460: Term t = pos.getPosInOccurrence().subTerm();
461: ProgramVariable var = (ProgramVariable) t.op();
462: ProgramElementName name = var
463: .getProgramElementName();
464: NameCreationInfo info = name.getCreationInfo();
465: String message;
466: if (info != null) {
467: message = info.infoAsString();
468: } else {
469: message = "No information available.";
470: }
471: JOptionPane.showMessageDialog(null, message,
472: "Name creation info",
473: JOptionPane.INFORMATION_MESSAGE);
474: }
475: }
476: }
477: }
478:
479: static class FocussedRuleApplicationMenuItem extends JMenuItem {
480: public FocussedRuleApplicationMenuItem() {
481: super ("Apply rules automatically here");
482: setToolTipText("<html>Initiates and restricts automatic rule applications on the "
483: + "highlighted formula, term or sequent.<br> "
484: + "'Shift + left mouse click' on the highlighted "
485: + "entity does the same.</html>");
486: }
487:
488: }
489:
490: static class TacletAppComparator implements Comparator {
491:
492: private int countFormulaSV(TacletSchemaVariableCollector c) {
493: int formulaSV = 0;
494: IteratorOfSchemaVariable it = c.varIterator();
495: while (it.hasNext()) {
496: SchemaVariable sv = it.next();
497: if (sv instanceof SortedSchemaVariable) {
498: if (((SortedSchemaVariable) sv).sort() == Sort.FORMULA) {
499: formulaSV++;
500: }
501: }
502: }
503:
504: return formulaSV;
505: }
506:
507: /** this is a rough estimation about the goal complexity. The
508: * complexity depends on the depth of the term to be replaced.
509: * If no such term exists we add a constant (may be refined in
510: * future)
511: */
512: private int measureGoalComplexity(ListOfTacletGoalTemplate l) {
513: int result = 0;
514: IteratorOfTacletGoalTemplate it = l.iterator();
515: while (it.hasNext()) {
516: TacletGoalTemplate gt = it.next();
517: if (gt instanceof RewriteTacletGoalTemplate) {
518: if (((RewriteTacletGoalTemplate) gt).replaceWith() != null) {
519: result += ((RewriteTacletGoalTemplate) gt)
520: .replaceWith().depth();
521: }
522: }
523: if (gt.sequent() != Sequent.EMPTY_SEQUENT) {
524: result += 10;
525: }
526: }
527: return result;
528: }
529:
530: /**
531: * rough approximation of the program complexity
532: */
533: public int programComplexity(JavaBlock b) {
534: if (b == JavaBlock.EMPTY_JAVABLOCK) {
535: return 0;
536: }
537: return new de.uka.ilkd.key.java.visitor.JavaASTWalker(b
538: .program()) {
539: private int counter = 0;
540:
541: protected void doAction(ProgramElement pe) {
542: counter++;
543: }
544:
545: public int getCounter() {
546: counter = 0;
547: start();
548: return counter;
549: }
550: }.getCounter();
551: }
552:
553: public int compare(Object o1, Object o2) {
554: FindTaclet taclet1 = (FindTaclet) (((TacletApp) o1)
555: .taclet());
556: FindTaclet taclet2 = (FindTaclet) (((TacletApp) o2)
557: .taclet());
558:
559: int findComplexity1 = taclet1.find().depth();
560: int findComplexity2 = taclet2.find().depth();
561: findComplexity1 += programComplexity(taclet1.find()
562: .javaBlock());
563: findComplexity2 += programComplexity(taclet2.find()
564: .javaBlock());
565:
566: if (findComplexity1 < findComplexity2) {
567: return -1;
568: } else if (findComplexity1 > findComplexity2) {
569: return 1;
570: }
571:
572: // depth are equal. Number of schemavariables decides
573: TacletSchemaVariableCollector coll1 = new TacletSchemaVariableCollector();
574: taclet1.find().execPostOrder(coll1);
575: int formulaSV1 = countFormulaSV(coll1);
576:
577: TacletSchemaVariableCollector coll2 = new TacletSchemaVariableCollector();
578: taclet2.find().execPostOrder(coll2);
579: int formulaSV2 = countFormulaSV(coll2);
580:
581: int cmpVar1 = -coll1.size() + taclet1.getRuleSets().size();
582: int cmpVar2 = -coll2.size() + taclet2.getRuleSets().size();
583:
584: if (cmpVar1 == cmpVar2) {
585: cmpVar1 = cmpVar1 - formulaSV1;
586: cmpVar2 = cmpVar2 - formulaSV2;
587: }
588:
589: if (cmpVar1 < cmpVar2) {
590: return -1;
591: } else if (cmpVar1 > cmpVar2) {
592: return 1;
593: }
594:
595: if (taclet1.ifSequent() == Sequent.EMPTY_SEQUENT
596: && taclet2.ifSequent() != Sequent.EMPTY_SEQUENT) {
597: return 1;
598: } else if (taclet1.ifSequent() == Sequent.EMPTY_SEQUENT
599: && taclet2.ifSequent() != Sequent.EMPTY_SEQUENT) {
600: return -1;
601: }
602:
603: int goals1 = -taclet1.goalTemplates().size();
604: int goals2 = -taclet2.goalTemplates().size();
605:
606: if (goals1 == goals2) {
607: goals1 = -measureGoalComplexity(taclet1.goalTemplates());
608: goals2 = -measureGoalComplexity(taclet2.goalTemplates());
609: }
610:
611: if (goals1 < goals2) {
612: return -1;
613: } else if (goals1 > goals2) {
614: return 1;
615: }
616:
617: return 0;
618: }
619:
620: }
621:
622: }
|