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: package de.uka.ilkd.key.gui.assistant;
017:
018: import javax.swing.AbstractButton;
019:
020: import de.uka.ilkd.key.gui.IconFactory;
021: import de.uka.ilkd.key.rule.RuleApp;
022:
023: /**
024: * The proof assistant AI receives input descriptions {@link AIInput}
025: * from the {@link ProofAssistantController}. These descriptions are
026: * analyzed, an action {@link AIAction} is chosen and send back to the
027: * controller which interprets the action.
028: */
029: public class ProofAssistantAI {
030:
031: /**
032: * dictionary of the ai
033: */
034: private ProofAssistantDictionary dict;
035:
036: /**
037: * action that does noting
038: */
039: private static final AIAction DO_NOTHING = new DoNothing();
040:
041: /**
042: * creates and initializes the AI, i.e. loads the dictionary
043: */
044: public ProofAssistantAI() {
045: dict = new ProofAssistantDictionary();
046: }
047:
048: /**
049: * analyzes the given input and decides about the action to be
050: * taken
051: * @param input the AIInput to be evaluated
052: * @return the action to be performed, e.g. display a text in the
053: * user interface, set prover options etc.
054: */
055: public AIAction analyze(AIInput input) {
056: AIAction action = null;
057: switch (input.getInputID()) {
058: case AIInput.RULE_APPLICATION_EVENT:
059: action = analyzeRuleAppEvent(((RuleEventInput) input)
060: .getRuleApp());
061: break;
062: case AIInput.TOOLBAR_EVENT:
063: action = analyzeToolBarEvent(((PressedButtonEventInput) input)
064: .getPressedButton());
065: break;
066: case AIInput.MENUBAR_EVENT:
067: action = analyzeMenuBarEvent(((PressedButtonEventInput) input)
068: .getPressedButton());
069: break;
070: default:
071: action = DO_NOTHING;
072: }
073:
074: return action;
075: }
076:
077: /**
078: * Analyzes and reacts on the given rule app, e.g. looks up the
079: * rule name in the dictionary and sends back a hint to be displayed
080: * by the proof assistent GUI
081: * @param app the RuleApp to be analyzed
082: * @return the action to be executed by the controller
083: */
084: private AIAction analyzeRuleAppEvent(RuleApp app) {
085: AIAction result = null;
086:
087: final String tip = dict.get("rules", app.rule().name()
088: .toString());
089: if (tip != null) {
090: result = new DisplayTextAction(tip);
091: } else {
092: result = DO_NOTHING;
093: }
094:
095: return result;
096: }
097:
098: /**
099: * Analyzes an event emitted by the toolbar. At the moment a
100: * simple action event is handed over.
101: * @param button the AbstractButton that has been pressed
102: * @return the action to be executed by the controller
103: */
104: private AIAction analyzeToolBarEvent(AbstractButton button) {
105: final String toolBar = "toolbar";
106: AIAction result = DO_NOTHING;
107:
108: if ("Apply Heuristics".equals(button.getText())) {
109: result = new DisplayTextAction(""
110: + dict.get(toolBar, "applyHeuristics"));
111: } else if ("Run Simplify".equals(button.getText())) {
112: result = new DisplayTextAction(""
113: + dict.get(toolBar, "runSIMPLIFY"));
114: } else if ("Run ICS".equals(button.getText())) {
115: result = new DisplayTextAction(""
116: + dict.get(toolBar, "runICS"));
117: } else if ("Goal Back".equals(button.getText())) {
118: result = new DisplayTextAction(""
119: + dict.get(toolBar, "goalBack"));
120: } else if (IconFactory.reuseLogo() == button.getIcon()) {
121: result = new DisplayTextAction(""
122: + dict.get(toolBar, "reuse"));
123: }
124:
125: return result;
126: }
127:
128: /**
129: * Called to analyze an action performed by the menu bar.
130: * @param button the Abstractbutton which has been pressed/selected
131: * @return the action to be executed by the controller
132: */
133: private AIAction analyzeMenuBarEvent(AbstractButton button) {
134: final String menuBar = "menu";
135: AIAction result = DO_NOTHING;
136:
137: if ("File".equals(button.getText())) {
138: result = new DisplayTextAction(dict.get(menuBar, "file"));
139: } else if ("View".equals(button.getText())) {
140: result = new DisplayTextAction(dict.get(menuBar, "view"));
141: } else if ("Proof".equals(button.getText())) {
142: result = new DisplayTextAction(dict.get(menuBar, "proof"));
143: } else if ("Options".equals(button.getText())) {
144: result = new DisplayTextAction(dict.get(menuBar, "options"));
145: } else if ("Tools".equals(button.getText())) {
146: result = new DisplayTextAction(dict.get(menuBar, "tools"));
147: }
148:
149: return result;
150: }
151:
152: }
|