001: package de.uka.ilkd.key.ocl.gf;
002:
003: import java.util.Iterator;
004: import java.util.Vector;
005: import java.util.logging.Logger;
006:
007: /**
008: * This class goes through the tree and tries to close all open Subtype lines.
009: *
010: * Makes heavy use of instance fields instead of parameters and return values.
011: * I justify that with the rather small size of this class.
012: * Because of this this class has to be reinitialized for each run.
013: * @author daniels
014: */
015: class SubtypingProber extends RefinementMenuCollector {
016: private static Logger nogger = Logger
017: .getLogger(SubtypingProber.class.getName());
018: /**
019: * how many undos are needed to clean up behind this probing
020: */
021: protected int undoSteps = 0;
022: /**
023: * the GF AST line by line
024: */
025: protected String[] treeArray = new String[0];
026: /**
027: * the pointer to the line, that has been read last
028: */
029: protected int currentLine;
030:
031: /**
032: * Standard fill-in-the-parameters constructor
033: * @param gfCapsule The encapsulation of GF
034: */
035: public SubtypingProber(GfCapsule gfCapsule) {
036: super (gfCapsule);
037: this .currentLine = 0;
038: }
039:
040: /**
041: * stores the read GF AST in treeArray
042: */
043: protected void readTree() {
044: String treeString = gfCapsule.readTree();
045: this .treeArray = treeString.split("\\n");
046: }
047:
048: /**
049: * looks at the refinement menu for node number lineNumber in the AST
050: * and if there is only one refinement command offered, does
051: * execute this.
052: * @param lineNumber
053: */
054: protected void checkLine(int lineNumber) {
055: String command = "mp [] ;; > " + lineNumber;
056: this .undoSteps += 2;
057: send(command);
058: readGfedit();
059: Vector commands = new Vector();
060: for (Iterator it = this .refinementMenuContent.iterator(); it
061: .hasNext();) {
062: StringTuple next = (StringTuple) it.next();
063: if (next.first.startsWith("r")) {
064: commands.add(next);
065: }
066: }
067: if (commands.size() == 0) {
068: //nothing can be done
069: nogger.fine("no refinement for '"
070: + this .treeArray[lineNumber] + "'");
071: } else if (commands.size() == 1) {
072: StringTuple nextCommand = (StringTuple) commands
073: .lastElement();
074: nogger.fine("one refinement for '"
075: + this .treeArray[lineNumber] + "'");
076: send(nextCommand.first);
077: this .undoSteps += 1;
078: // now new things are in the state,
079: // but since we assume that nothing above lineNumber changes,
080: // that is wanted.
081: readGfedit();
082: } else {
083: nogger.fine(commands.size() + " refinements for '"
084: + this .treeArray[lineNumber] + "'");
085: }
086: }
087:
088: /**
089: * Asks GF for the AST and tries to hunt down all unrefined
090: * Subtype witnesses.
091: * @return the number of undo steps this run needed
092: */
093: public int checkSubtyping() {
094: //solve to try to eliminate many unrefined places
095: send("c solve ;; mp []"); //focus at the top where '*' does not disturb
096: readGfedit();
097: this .undoSteps += 2;
098: for (int i = 3; i < this .treeArray.length; i++) {
099: //the condition gets rechecked every run, and length will only grow
100: //We start at 3 since the witness is the third argument of coerce,
101: //before nothing can happen
102: //(sth. like "n core.Subtype" does not count!
103: //(starting with new category Subtype) )
104: if (this .treeArray[i].indexOf(": Subtype") > -1) {
105: if (!this .treeArray[i - 2].startsWith("?") //both Class arguments refined
106: && !this .treeArray[i - 1].startsWith("?")) {
107: checkLine(i);
108: }
109: }
110: }
111: nogger.fine(this .undoSteps + " individual commands sent");
112: return this.undoSteps;
113: }
114: }
|