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: //This program is distributed in the hope that it will be useful,
009: //but WITHOUT ANY WARRANTY; without even the implied warranty of
010: //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
011: //GNU General Public License for more details.
012:
013: //You can either finde the file LICENSE or LICENSE.TXT in the source
014: //distribution or in the .jar file of this application
015:
016: package de.uka.ilkd.key.ocl.gf;
017:
018: import java.util.Enumeration;
019: import java.util.logging.Level;
020: import java.util.logging.Logger;
021:
022: import javax.swing.tree.DefaultMutableTreeNode;
023:
024: /**
025: * Goes through the AST and:
026: * Labels node according to the following:
027: * hidden, if they are a coerce without a constraint
028: * colored, if they are a coerce with a constraint
029: * Saves a reference to the currently selected node
030: * Finds out
031: * if attributes of self should be given an easy access,
032: * if the refinement menu below a coerce should be reduces,
033: * if it should be probed, if self and result are superfluous
034: * in the refinement menu.
035: * if a coerce should be introduced automatically.
036: * Takes a tree and hides the nodes labelled as hidden in another stage.
037: * @author hdaniels
038: */
039: class TreeAnalyser {
040: /**
041: * debug stuff for the tree
042: */
043: private static Logger treeLogger = Logger
044: .getLogger(TreeAnalyser.class.getName());
045: /**
046: * dealing with coerce, when it is inserted and so on
047: */
048: private static Logger coerceLogger = Logger
049: .getLogger(TreeAnalyser.class.getName() + ".coerce");
050:
051: /**
052: * if coerce should get hidden, if all their arguments are refined
053: */
054: private boolean hideCoerce;
055: /**
056: * if coerce should always be hidden,
057: */
058: private boolean hideCoerceAggressive;
059: /**
060: * if the refinement menu should get condensed at all
061: */
062: private boolean coerceReduceRM;
063: /**
064: * if coerce should get introduced automatically at all
065: */
066: private boolean autoCoerce;
067: /**
068: * if result and self should be shown always
069: */
070: private boolean showSelfResult;
071: /**
072: * if properties of self should be probed for
073: */
074: private boolean easyAttributes;
075: /**
076: * If coerces whith both Class arguments
077: */
078: private boolean highlightSubtypingErrors;
079:
080: /**
081: * @param autoCoerce if coerce should get introduced automatically at all
082: * @param coerceReduceRM if the refinement menu should get condensed at all
083: * @param easyAttributes if properties of self should be probed for
084: * @param hideCoerce if coerce should get hidden, if all their arguments are refined
085: * @param hideCoerceAggressive if coerce should always be hidden,
086: * unless there is a GF constraint
087: * @param highlightSubtypingErrors If coerces whith both Class arguments
088: * refined, but not with the Subtype argument should get marked
089: * @param showSelfResult if result and self should be shown always
090: */
091: public TreeAnalyser(boolean autoCoerce, boolean coerceReduceRM,
092: boolean easyAttributes, boolean hideCoerce,
093: boolean hideCoerceAggressive,
094: boolean highlightSubtypingErrors, boolean showSelfResult) {
095: this .autoCoerce = autoCoerce;
096: this .coerceReduceRM = coerceReduceRM;
097: this .easyAttributes = easyAttributes;
098: this .hideCoerce = hideCoerce;
099: this .hideCoerceAggressive = hideCoerceAggressive;
100: this .highlightSubtypingErrors = highlightSubtypingErrors;
101: this .showSelfResult = showSelfResult;
102: }
103:
104: /**
105: * Takes the rootNode of the AST and does some small analysis on it:
106: * Check for missing Subtype witnesses,
107: * check if the Instance menu of a Coerce can be reduced
108: * @param topNode The root or top node of the AST
109: * @return an object that contains the result of this analysis.
110: * Currently this applies only to the selected node.
111: * @see TreeAnalysisResult
112: */
113: TreeAnalysisResult analyseTree(DefaultMutableTreeNode topNode) {
114: //just the initial values
115: String resultCommand = null;
116: int resultUndoSteps = -1;
117: boolean resultReduceCoerce = false;
118: boolean resultProbeSelfResult = false;
119: boolean resultDeleteAlsoAbove = false;
120: boolean resultEasyAttributes = false;
121: TreeAnalysisResult tar = new TreeAnalysisResult(resultCommand,
122: resultUndoSteps, resultReduceCoerce,
123: resultProbeSelfResult, resultDeleteAlsoAbove,
124: resultEasyAttributes, null, null);
125:
126: //doing it depth first, because we have to know the subtypingStatus
127: //of the children of coerce before we analyze coerce itself
128: for (Enumeration e = topNode.depthFirstEnumeration(); e
129: .hasMoreElements();) {
130: DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
131: .nextElement();
132: analyseTreeNode(currNode, tar);
133: }
134: AstNodeData and = (AstNodeData) tar.selectedNode
135: .getUserObject();
136: if ((and.showInstead != -1) && (tar.command == null)) {
137: //if the current node is hidden, move up in the tree,
138: //until a visible node is found
139: DefaultMutableTreeNode tn = (DefaultMutableTreeNode) tar.selectedNode
140: .getParent();
141: AstNodeData dand = null;
142: while (tn != null) {
143: dand = (AstNodeData) tn.getUserObject();
144: if (dand.showInstead == -1) {
145: //found a visible node
146: break;
147: }
148: tn = (DefaultMutableTreeNode) tn.getParent();
149: }
150: if (dand != null) {
151: tar.command = "[tr] mp " + dand.position;
152: tar.undoSteps = 1;
153: } //otherwise give up, can only occur, if coerce is the top node.
154: //And for that, one would have to do a "n Instance" first,
155: //which GF does not even offer.
156: }
157: return tar;
158: }
159:
160: /**
161: * Takes the rootNode of the AST and does some small analysis on it:
162: * Check for missing Subtype witnesses,
163: * check if the Instance menu of a Coerce can be reduced
164: * @param nodeToCheck The node that is to be analysed
165: * @param tar The result, that gets modified
166: * @see TreeAnalysisResult
167: */
168: private void analyseTreeNode(DefaultMutableTreeNode nodeToCheck,
169: TreeAnalysisResult tar) {
170: AstNodeData and = (AstNodeData) nodeToCheck.getUserObject();
171: DefaultMutableTreeNode parent = (DefaultMutableTreeNode) nodeToCheck
172: .getParent();
173: Printname parentPrintname = null;
174: if ((parent != null) && (parent.getUserObject() != null)
175: && (parent.getUserObject() instanceof AstNodeData)) {
176: AstNodeData parentAnd = (AstNodeData) parent
177: .getUserObject();
178: parentPrintname = parentAnd.getPrintname();
179: }
180:
181: if (and.selected) {
182: tar.selectedNode = nodeToCheck;
183: tar.currentNode = and.node;
184: //set the focusPosition to a preliminary value
185: tar.focusPosition = new LinPosition(and.position, true);
186: //rather check too much for null
187: if (this .autoCoerce && (and.node != null)
188: && and.node.isMeta() && (parent != null)
189: && (parent.getUserObject() != null)
190: && (and.node.getType() != null)
191: && (and.node.getType().startsWith("Instance"))) {
192: //check, if a coerce is needed
193: GfAstNode parentNode = ((AstNodeData) parent
194: .getUserObject()).node;
195: if (parentPrintname.getParamAutoCoerce(parent
196: .getIndex(nodeToCheck))) {
197: coerceLogger.fine("Coerceable fun found: "
198: + and.node + " + " + parentNode);
199: //refine with coerce. Do not allow another GF run, so [r]
200: tar.command = "[tr] r core.coerce ;; mp "
201: + LinPosition.calculateChildPosition(
202: and.position, 3);
203: tar.undoSteps = 2; //move there is also sth. to be undone
204: } else if ((parentNode.getFun().indexOf("coerce") > -1)
205: //to avoid getting stuck below a coerce with wrong type arguments
206: //the coerce above is deleted and rerefined.
207:
208: //coerce below a coerce is never done automatically, so the else if is justified,
209: //meaning, that introduced a coerce, we do not have to delete it right a away
210: && parent.getParent() != null
211: && (parent.getParent() instanceof DefaultMutableTreeNode)) {
212: DefaultMutableTreeNode grandParent = (DefaultMutableTreeNode) parent
213: .getParent();
214: if (grandParent != null) {
215: AstNodeData grandParentAnd = (AstNodeData) grandParent
216: .getUserObject();
217: Printname grandParentPrintname = grandParentAnd
218: .getPrintname();
219:
220: if (grandParentPrintname
221: .getParamAutoCoerce(grandParent
222: .getIndex(parent))) {
223: coerceLogger
224: .fine("Auto-Coerce to be un- and redone: "
225: + and.node
226: + " + "
227: + parentNode
228: + " -- "
229: + tar.focusPosition.position);
230: tar.command = "[tr] mp "
231: + tar.focusPosition
232: .parentPosition()
233: + " ;; d ;; mp "
234: + tar.focusPosition
235: .parentPosition()
236: + " ;; r core.coerce ;; mp "
237: + tar.focusPosition.position;
238: tar.undoSteps = 6;
239: }
240: }
241: }
242: }
243:
244: if (coerceReduceRM
245: && (and.node != null)
246: && (and.node.getType() != null)
247: && (parent != null)
248: && (parent.getUserObject() != null)
249: && (((AstNodeData) parent.getUserObject())
250: .getPrintname() != null)
251: && (((AstNodeData) parent.getUserObject())
252: .getPrintname().fun.endsWith("coerce"))
253: && (and.node.getType().startsWith("Instance")) //if coerce, than we are the Instance argument
254: && (((DefaultMutableTreeNode) (parent.getChildAt(2)))
255: .getUserObject() != null)
256: && (parent.getChildAt(2) != null)
257: && ((AstNodeData) ((DefaultMutableTreeNode) (parent
258: .getChildAt(2))).getUserObject()).node
259: .isMeta()) {
260: AstNodeData super TypeAnd = ((AstNodeData) ((DefaultMutableTreeNode) (parent
261: .getChildAt(1))).getUserObject());
262: if (!super TypeAnd.node.isMeta()
263: && (super TypeAnd.node.getFun().indexOf(
264: "OclAnyC") == -1)) {
265: //in these cases, everything goes. No sense in dozends of expensive GF runs then.
266: tar.reduceCoerce = true;
267: }
268: coerceLogger
269: .fine("candidate for coerce reduction found: "
270: + and.node + " + " + parent);
271: }
272:
273: if (showSelfResult && (and.node != null)
274: && (and.node.getType() != null)
275: && (and.node.getType().startsWith("Instance"))
276: && (tar.reduceCoerce //not everything is allowed here
277: // if not below a coerce (covered above) and no constraints
278: || (and.node.getType().indexOf("{") == -1))) {
279: //if there are constraints present, there is no point in probing, since
280: //then either no or every instance is offered.
281: //We do not have to probe then.
282: tar.probeSelfResult = true;
283: }
284:
285: if (easyAttributes && (and.node != null)
286: && (and.node.getType() != null)
287: && (and.node.isMeta())
288: && (and.node.getType().startsWith("Instance"))) {
289: //not much to check here
290: tar.easyAttributes = true;
291: }
292: }
293:
294: //check for subtyping errors
295: if (highlightSubtypingErrors && (and.node != null)
296: && (and.node.getType() != null) && (parent != null)
297: && (and.node.isMeta()) //otherwise GF would complain
298: && (and.node.getType().startsWith("Subtype")) //if coerce, than we are the Subtype argument
299: ) {
300: AstNodeData subtypeAnd = (AstNodeData) (((DefaultMutableTreeNode) (parent
301: .getChildAt(0))).getUserObject());
302: AstNodeData super typeAnd = (AstNodeData) (((DefaultMutableTreeNode) (parent
303: .getChildAt(1))).getUserObject());
304: if ((subtypeAnd != null) && (super typeAnd != null)) {
305: if (!super typeAnd.node.isMeta()
306: && !subtypeAnd.node.isMeta()) {
307: //if one of them is meta, then the situation is not fixed yet,
308: //so don't complain.
309: and.subtypingStatus = false;
310: }
311: }
312: }
313: //hide coerce if possible
314: //if coere is completely filled in (all children not meta),
315: //it will be replaced by child 3.
316: if (hideCoerce && (and.node != null)
317: && (and.node.getType() != null)
318: && (and.node.getFun().endsWith("coerce"))) {
319: /**
320: * if true, then something is unfinished or constrained.
321: * So don't hide that node.
322: */
323: boolean metaChild = false;
324: //check if constraints hold for this node
325: if ((and.constraint != null)
326: && (and.constraint.length() > 0)) {
327: //some constraint holds here.
328: //We must not shroud a possible source for that.
329: metaChild = true;
330: }
331: //This search will only be run once for each coerce:
332: for (int i = 0; i < 3 && !metaChild; i++) {
333: //This is for the more complicated collection
334: //subtyping witnesses.
335: //we do a depthFirst search to find meta nodes.
336: //If they exist, we know that we shouldn't hide this node.
337: for (Enumeration e = ((DefaultMutableTreeNode) nodeToCheck
338: .getChildAt(i)).depthFirstEnumeration(); e
339: .hasMoreElements();) {
340: DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
341: .nextElement();
342: AstNodeData dand = (AstNodeData) currNode
343: .getUserObject();
344: if (!dand.subtypingStatus
345: //hideCoerceAggressive means that just incomplete type arguments are no reason to not hide the node
346: //only subtypingStatus is one because then surely there is an error
347: || (!hideCoerceAggressive && dand.node
348: .isMeta())) {
349: metaChild = true;
350: break; //no need to go further
351: }
352: }
353: if (metaChild) {
354: break;
355: }
356: }
357: //For the Instance argument, we do not have do to a deep search
358: AstNodeData childAnd = (AstNodeData) (((DefaultMutableTreeNode) (nodeToCheck
359: .getChildAt(3))).getUserObject());
360: if (!hideCoerceAggressive && childAnd.node.isMeta()) {
361: //see reasons for hideCoerceAggressive above
362: metaChild = true;
363: }
364:
365: if (!metaChild) {
366: and.showInstead = 3;
367: //now label the type nodes as hidden
368: for (int i = 0; i < 3 && !metaChild; i++) {
369: //This is for the more complicated collection
370: //subtyping witnesses.
371: for (Enumeration e = ((DefaultMutableTreeNode) nodeToCheck
372: .getChildAt(i)).depthFirstEnumeration(); e
373: .hasMoreElements();) {
374: DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
375: .nextElement();
376: AstNodeData dand = (AstNodeData) currNode
377: .getUserObject();
378: dand.showInstead = -2; // tag for hidden without replacement
379: }
380: }
381:
382: }
383:
384: //if we are at a coerce above the selected Instance node,
385: //we want to mark that, so that the d command can be modified
386: if ((and.node != null)
387: && (and.node.getFun().endsWith("coerce"))
388: && (and.showInstead > -1) //only hidden coerce
389: && (((AstNodeData) ((DefaultMutableTreeNode) nodeToCheck
390: .getChildAt(3)).getUserObject()).selected)) {
391: tar.deleteAlsoAbove = true;
392: }
393: }
394: }
395:
396: /**
397: * Removes nodes from the tree that has topNode as its root.
398: * Affected are nodes in which the field showInstead in their
399: * AstNodeData is greater than -1
400: * @param topNode The root of the tree from which nodes should
401: * be removed.
402: * @return The root of the transformed tree.
403: * This might not be topNode, since that node might as well be
404: * removed.
405: */
406: protected static DefaultMutableTreeNode transformTree(
407: DefaultMutableTreeNode topNode) {
408: DefaultMutableTreeNode nextNode = topNode;
409: while (nextNode != null) {
410: AstNodeData and = (AstNodeData) nextNode.getUserObject();
411: if (and.showInstead > -1) {
412: DefaultMutableTreeNode parent = (DefaultMutableTreeNode) nextNode
413: .getParent();
414: if (parent == null) {
415: topNode = (DefaultMutableTreeNode) nextNode
416: .getChildAt(and.showInstead);
417: if (treeLogger.isLoggable(Level.FINE)) {
418: //yeah, I know, variable naming is messed up here because of the assignment above
419: treeLogger.fine("hiding topNode ###" + nextNode
420: + "###, showing instead ###" + topNode
421: + "###");
422: }
423: nextNode = topNode;
424: } else {
425: final int index = parent.getIndex(nextNode);
426: parent.remove(index);
427: DefaultMutableTreeNode instead = (DefaultMutableTreeNode) nextNode
428: .getChildAt(and.showInstead);
429: parent.insert(instead, index);
430: if (treeLogger.isLoggable(Level.FINE)) {
431: treeLogger.fine("hiding node ###" + nextNode
432: + "###, showing instead ###" + instead
433: + "###");
434: }
435: nextNode = instead;
436: }
437: } else {
438: nextNode = nextNode.getNextNode();
439: }
440: }
441: return topNode;
442: }
443:
444: }
|