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 applicationpackage de.uka.ilkd.key.ocl.gf;
010:
011: package de.uka.ilkd.key.ocl.gf;
012:
013: import java.util.Collections;
014: import java.util.HashSet;
015: import java.util.Iterator;
016: import java.util.Vector;
017: import java.util.logging.Level;
018: import java.util.logging.Logger;
019:
020: /**
021: * This class is an unclean hack.
022: * The whole refinement menu architecture expected, that everything is probed,
023: * when the refinement menu is getting created.
024: * But for getting only subtype correct properties of self needs a number of
025: * calls to GF, which could be deferred to not make things slower than they
026: * already are.
027: * This deferred probing is done in this class.
028: * @author daniels
029: *
030: */
031: class SelfPropertiesCommand extends LinkCommand {
032: private final static Logger logger = Logger
033: .getLogger(SelfPropertiesCommand.class.getName());
034: private final GfCapsule gfCapsule;
035: private final LinPosition focusPos;
036: private final String toAppend;
037: private final boolean isAbstract;
038: private final HashSet processedSubcats;
039: private final PrintnameManager printnameManager;
040:
041: /**
042: * A simple setter constructor, no calculation done here.
043: * @param manager The printname manager, that knows, how the properties
044: * of self should be listed in the refinement menu
045: * @param gfCapsule The reader/writer abstraction from GF
046: * @param focusPos The position of the GF focus
047: * @param isAbstract if Abstract is the current menu language
048: * @param toAppend If something should be appended to the command
049: * @param processedSubcats Here, the subcat for self is put into
050: */
051: public SelfPropertiesCommand(final PrintnameManager manager,
052: GfCapsule gfCapsule, LinPosition focusPos,
053: boolean isAbstract, String toAppend,
054: HashSet processedSubcats) {
055: super (PrintnameManager.SELF_SUBCAT, manager);
056: this .gfCapsule = gfCapsule;
057: this .printnameManager = manager;
058: this .focusPos = focusPos;
059: this .processedSubcats = processedSubcats;
060: this .toAppend = toAppend;
061: this .isAbstract = isAbstract;
062: }
063:
064: /**
065: * @return a Vector of RealCommand containing the suitable properties
066: * of self at the current focus position.
067: * Subtyping is taken into account, so only properties with a subtype
068: * of the supertype of the coerce above (at other places this method
069: * is not applicable) show up in this menu.
070: * The method used is similiar to the one for Instances below a coerce.
071: */
072: Vector produceSubmenu() {
073: logger.fine("SelfPropertiesCommand asked to produce a menu");
074: //HashSet to prevent duplicates
075: final HashSet commands = new HashSet();
076: RefinementMenuCollector rmc = new RefinementMenuCollector(
077: gfCapsule);
078: //move to the subtype witness argument
079: final String collectSubtypesCommand = "mp "
080: + LinPosition.calculateBrethrenPosition(
081: focusPos.position, 2);
082: final Vector possibleSubtypes = rmc
083: .readRefinementMenu(collectSubtypesCommand);
084: String undoString = "";
085: int undos = 0;
086: //for the case, that there is only one possible refinement at all
087: //which gets automatically filled in
088: final StringBuffer singleReplacement = new StringBuffer();
089: //loop through the offered Subtype refinements
090: for (Iterator it = possibleSubtypes.iterator(); it.hasNext();) {
091: StringTuple nextCommand = (StringTuple) it.next();
092: if (!nextCommand.first.trim().startsWith("r")) {
093: //no ac, d, rc or whatever wanted here. Only refine.
094: continue;
095: }
096: final String commandPrefix = undoString + nextCommand.first
097: + " ;; mp " + focusPos.position + " ;; ";
098: logger.finer("commandPrefix: " + commandPrefix);
099: Vector futureRefinements = new Vector();
100: undos = addSelfProperties(futureRefinements, commandPrefix,
101: singleReplacement);
102: undos += 2; // to undo commandPrefix
103: undoString = "u " + undos + " ;; "; //for all following runs we want an undo before it
104: // Vector nextRefinements = rmc.readRefinementMenu(collectRefinementsCommand);
105: commands.addAll(futureRefinements);
106: }
107: final String cleanupCommand = "u " + (undos + 1); //undo the last command and also the first mp
108: rmc.readRefinementMenu(cleanupCommand); //no harm done here, collector won't get reused
109: Vector result = new Vector();
110: for (Iterator it = commands.iterator(); it.hasNext();) {
111: StringTuple st = (StringTuple) it.next();
112: if ((commands.size() == 1)
113: && (st instanceof ChainCommandTuple)) {
114: //the case when only one property is available at all.
115: //Then this will automatically be selected
116: //To compensate for that, singleRefinement is used.
117: //This will be just one refinement, otherwise, we
118: //wouldn't be in this branch.
119: //This refinement does not contain the actual r
120: //command and therefore needs one undo step less
121: ChainCommandTuple cct = (ChainCommandTuple) st;
122: st = new ChainCommandTuple(
123: singleReplacement.toString(), cct.second,
124: cct.fun, cct.subcat, cct.undoSteps - 1);
125: }
126: GFCommand gfcommand;
127: if (st instanceof ChainCommandTuple) {
128: ChainCommandTuple cct = (ChainCommandTuple) st;
129: gfcommand = new RealCommand(st.first, processedSubcats,
130: printnameManager, st.second, isAbstract,
131: toAppend, cct.undoSteps, cct.fun, cct.subcat);
132: } else {
133: gfcommand = new RealCommand(st.first, processedSubcats,
134: printnameManager, st.second, isAbstract,
135: toAppend);
136: }
137: result.add(gfcommand);
138: }
139: Collections.sort(result);
140: return result;
141: }
142:
143: /**
144: * Probes for the properties of self, that could be filled in at
145: * the current focus position.
146: * If it finds any, these are added to result.
147: * @param result The Vector, that will get filled with the collected
148: * chain commands
149: * @param commandPrefix The prefix, that is to be prepended to the
150: * probing command. Used for refining with a Subtype witness and a
151: * mp to the Instance position, where this method expects to start.
152: * @param singleReplacement This is a hack for cases, when GF refines
153: * an refinement automatically. If that happens only for one subtype,
154: * then GF would fill that in automatically even when the supertype is
155: * open. Therefore, it must be omitted in the actual command.
156: * But this situation can only be checked after all subtypes have been
157: * probed.
158: * @return the number of undo steps needed to undo the probing command
159: * (without prefix, that is handled by the caller)
160: */
161: private int addSelfProperties(final Vector result,
162: final String commandPrefix,
163: final StringBuffer singleReplacement) {
164: //solve in between to avoid some typing errors by closing some type arguments
165: final String probeCommand = "r core.implPropCall ;; mp "
166: + focusPos.childPosition(2)
167: + " ;; r core.self ;; solve ;; mp "
168: + focusPos.childPosition(3);
169: final String deleteAppendix = " ;; d";
170: final RefinementMenuCollector rmc = new RefinementMenuCollector(
171: gfCapsule);
172: final String actualProbeCommand = commandPrefix + probeCommand
173: + deleteAppendix;
174: logger
175: .finer("&&& actual probe command:: "
176: + actualProbeCommand);
177: Vector futureRefinements = rmc
178: .readRefinementMenu(actualProbeCommand);
179: final int undos = 5;
180: for (Iterator it = futureRefinements.iterator(); it.hasNext();) {
181: StringTuple st = (StringTuple) it.next();
182: if (st.first.startsWith("r")) { //is a refinement, no ac or d
183: String newCommand;
184: //add the command that came before
185: final int cmdUndos;
186: if (futureRefinements.size() == 1) {
187: //the case, when only one property is defined in the grammar:
188: singleReplacement.append(probeCommand
189: + " ;; c solve");
190: }
191: newCommand = probeCommand + " ;; " + st.first
192: + " ;; c solve";
193: cmdUndos = 6;
194: // now extract the fun of the property
195: String fun = st.first.substring(1).trim();
196: ChainCommandTuple cct = new ChainCommandTuple(
197: newCommand, st.second, fun,
198: PrintnameManager.SELF_SUBCAT, cmdUndos);
199: if (logger.isLoggable(Level.FINE)) {
200: logger.finer("added " + cct);
201: }
202: result.add(cct);
203: }
204: }
205: return undos;
206: }
207: }
|