001: //Copyright (c) Hans-Joachim Daniels 2005
002: //
003: //This program is free software; you can redistribute it and/or modify
004: //it under the terms of the GNU General Public License as published by
005: //the Free Software Foundation; either version 2 of the License, or
006: //(at your option) any later version.
007: //
008: //You can either finde the file LICENSE or LICENSE.TXT in the source
009: //distribution or in the .jar file of this application
010:
011: package de.uka.ilkd.key.ocl.gf;
012:
013: import java.util.HashSet;
014: import java.util.Iterator;
015: import java.util.Vector;
016: import java.util.logging.Level;
017: import java.util.logging.Logger;
018:
019: /**
020: * This class is completely static and cannot be instantiated.
021: * @see #transformRefinementMenu(de.uka.ilkd.key.ocl.gf.TreeAnalysisResult, java.util.Vector, de.uka.ilkd.key.ocl.gf.GfCapsule)
022: * @author hdaniels
023: */
024: class RefinementMenuTransformer {
025: /**
026: * if things are added to or removed from the refinement menu
027: */
028: protected static Logger logger = Logger
029: .getLogger(RefinementMenuTransformer.class.getName());
030:
031: private RefinementMenuTransformer() {
032: //A private constructor enforces the noninstantiability
033: //of "RefinementMenuTransformer".
034: //(See item 3 of "Effective Java".)
035: }
036:
037: /**
038: * Depending on tar, the refinement menu given in raw form in oldMenu
039: * is transformed.
040: * That includes:
041: * - adding properties of self
042: * - producing a reduced version for subtyping below a coerce
043: * where only Instances of subtypes are listed
044: * - probes, if self and result are really applicable
045: * - changes the delete command, when an unrefined Instance
046: * argument of coerce is clicked on, to first delete the
047: * whole coerce to avoid sticking with wrong type arguments.
048: * @param tar TreeAnalyser has decided what to do here. That is followed.
049: * @param oldMenu The original content of the refinement menu.
050: * Is a Vector of StringTuple
051: * @param gfCapsule The encapsulation of GF regarding read/write access
052: * @return The refinement menu in its new form
053: */
054: protected static Vector transformRefinementMenu(
055: TreeAnalysisResult tar, Vector oldMenu, GfCapsule gfCapsule) {
056: //now do fill (or partially empty) the offered commands list
057: final Vector usedCommandVector;
058: if (tar.reduceCoerce) {
059: //is only true if switched on globally.
060: //And if conditions are right.
061: usedCommandVector = produceReducedCoerceRefinementMenu(
062: tar.focusPosition.position, gfCapsule);
063: } else {
064: usedCommandVector = oldMenu;
065: }
066: if (tar.deleteAlsoAbove) {
067: String newPos = tar.focusPosition.parentPosition();
068: StringTuple newDelete = new StringTuple("mp " + newPos
069: + " ;; d",
070: "delete current subtree\\$also delete the encompassing coercion ");
071: exchangeCommand(usedCommandVector, "d", newDelete);
072: }
073: if (tar.probeSelfResult) {
074: probeCompletability(usedCommandVector, tar.focusPosition,
075: gfCapsule);
076: }
077: if (tar.easyAttributes && !tar.reduceCoerce) {
078: addSelfProperties(usedCommandVector, tar.focusPosition,
079: gfCapsule);
080: }
081: return usedCommandVector;
082: }
083:
084: /**
085: * Looks at the subtyping witness of the same coerce as currentPos
086: * and collects the possible refinements for all offered subtypes.
087: * It assumes that argument 0 of coerce is automatically filled in.
088: *
089: * This method is surely <b>slow</b> since a lot of calls to GF is made
090: * here.
091: * @param currentPos musst point to a child of a coerce.
092: * @param gfCapsule The encapsulation of GF regarding read/write access
093: * @return a Vector of StringTuple as readRefinementMenu does.
094: * This Vector can be fed into formRefinementMenu.
095: */
096: private static Vector produceReducedCoerceRefinementMenu(
097: String currentPos, GfCapsule gfCapsule) {
098: final HashSet commands = new HashSet();
099: RefinementMenuCollector rmc = new RefinementMenuCollector(
100: gfCapsule);
101: //move to the subtype witness argument
102: final String collectSubtypesCommand = "mp "
103: + LinPosition.calculateBrethrenPosition(currentPos, 2);
104: Vector possibleSubtypes = rmc
105: .readRefinementMenu(collectSubtypesCommand);
106: String undoString = "";
107: final String undoTemplate = "u 2 ;; ";
108: for (Iterator it = possibleSubtypes.iterator(); it.hasNext();) {
109: StringTuple nextCommand = (StringTuple) it.next();
110: // if (!nextCommand.first.trim().startsWith("r")) {
111: // //no ac, d, rc or whatever wanted here. Only refine.
112: // continue;
113: // }
114: final String collectRefinementsCommand = undoString
115: + nextCommand.first + " ;; mp " + currentPos;
116: undoString = undoTemplate; //for all following runs we want an undo before it
117: Vector nextRefinements = rmc
118: .readRefinementMenu(collectRefinementsCommand);
119: commands.addAll(nextRefinements);
120: }
121: final String cleanupCommand = "u 3"; //undo the last command and also the first mp
122: rmc.readRefinementMenu(cleanupCommand); //no harm done here, collector won't get reused
123: Vector result = new Vector(commands);
124: return result;
125: }
126:
127: /**
128: * checks if result and self make sense in the current context.
129: * if not, they are removed from oldMenu
130: * @param oldMenu A Vector of StringTuple that represents the
131: * commands for the refinement menu
132: * @param focusPos The current position in the AST
133: * @param gfCapsule The encapsulation of GF regarding read/write access
134: */
135: private static void probeCompletability(Vector oldMenu,
136: LinPosition focusPos, GfCapsule gfCapsule) {
137: /**
138: * self and result both take two arguments.
139: * The first is the type, which is fixed
140: * if the second argument is refineable.
141: * Important is the second.
142: * This only is refineable for the real type of self/result
143: */
144: if (focusPos == null) {
145: //sadly, we can't do much
146: return;
147: }
148: final String childPos = focusPos.childPosition(1);
149: final SelfResultProber cp = new SelfResultProber(gfCapsule);
150: for (int i = 0; i < oldMenu.size(); i++) {
151: String cmd = ((StringTuple) oldMenu.elementAt(i)).first;
152: if ((cmd != null)
153: && ((cmd.indexOf("r core.self") > -1) || (cmd
154: .indexOf("r core.result") > -1))) {
155: //the first mp is necessary for the second of self/result.
156: //without, GF will jump to a stupid position
157: String newCommand = "mp " + focusPos.position + " ;; "
158: + cmd + " ;; mp " + childPos;
159: if (!cp.isAutoCompletable(newCommand, 3)) {
160: oldMenu.remove(i);
161: i -= 1;
162: }
163: }
164: }
165: }
166:
167: /**
168: * Probes for the properties of self, that could be filled in at
169: * the current focus position.
170: * If it finds any, these are added to oldMenu
171: * This method will add all offered commands to the refinement menu,
172: * not only for suiting subtypes due to speed reasons.
173: * @param oldMenu A Vector of StringTuple. The menu with the commands
174: * and show texts as given by GF. Gets modified.
175: * @param focusPos The position of the GF focus in the AST
176: * @param gfCapsule The encapsulation of GF regarding read/write access
177: */
178: private static void addSelfProperties(Vector oldMenu,
179: LinPosition focusPos, GfCapsule gfCapsule) {
180: //solve in between to avoid some typing errors by closing some type arguments
181: final String probeCommand = "r core.implPropCall ;; mp "
182: + focusPos.childPosition(2)
183: + " ;; r core.self ;; solve ;; mp "
184: + focusPos.childPosition(3);
185: final String deleteAppendix = " ;; d";
186: final RefinementMenuCollector rmc = new RefinementMenuCollector(
187: gfCapsule);
188: Vector futureRefinements = rmc.readRefinementMenu(probeCommand
189: + deleteAppendix);
190: final int undos = 5;
191: final boolean singleRefinement;
192: if (futureRefinements.size() == 1) {
193: singleRefinement = true;
194: } else {
195: singleRefinement = false;
196: }
197: final String cleanupCommand = "u " + undos;
198: rmc.readRefinementMenu(cleanupCommand); //no harm done here
199: for (Iterator it = futureRefinements.iterator(); it.hasNext();) {
200: StringTuple st = (StringTuple) it.next();
201: if (st.first.startsWith("r")) { //is a refinement, no ac or d
202: String newCommand;
203: //add the command that came before
204: final int cmdUndos;
205: if (singleRefinement) {
206: //that is an exceptional case, but might happen.
207: //Here we don't have to refine the final property
208: //at all, since GF does that automatically
209: newCommand = probeCommand + " ;; c solve";
210: cmdUndos = 5;
211: } else {
212: //here the 'd' is not needed, since we know,
213: //that nothing is refined automatically
214: newCommand = probeCommand + " ;; " + st.first
215: + " ;; c solve";
216: cmdUndos = 6;
217: }
218: // now extract the fun of the property
219: String fun = st.first.substring(1).trim();
220: ChainCommandTuple cct = new ChainCommandTuple(
221: newCommand, st.second, fun,
222: PrintnameManager.SELF_SUBCAT, cmdUndos);
223: if (logger.isLoggable(Level.FINER)) {
224: logger.finer("added " + cct);
225: }
226: oldMenu.add(cct);
227: }
228: }
229: }
230:
231: /**
232: * Goes through oldMenu and if it finds a command in there, where
233: * first.equals(oldCommand), this command is replaced by newCommand.
234: * oldMenu's content thus gets modified.
235: * @param oldMenu a Vector of StringTuple
236: * @param oldCommand a GF command string (what is sent, not the show text)
237: * @param newCommand a StringTuple representing what could be a pait from GF
238: */
239: private static void exchangeCommand(Vector oldMenu,
240: String oldCommand, StringTuple newCommand) {
241: for (int i = 0; i < oldMenu.size(); i++) {
242: StringTuple next = (StringTuple) oldMenu.get(i);
243: if (next.first.equals(oldCommand)) {
244: oldMenu.remove(i);
245: oldMenu.insertElementAt(newCommand, i);
246: }
247: }
248: }
249:
250: }
|