001: //Copyright (c) Janna Khegai 2004, 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: /**
019: * represents a position in the AST in Haskell notation together
020: * with a flag that indicates whether at least one constraint does not hold or
021: * if all hold (correct/incorrect).
022: * Class is immutable.
023: */
024: class LinPosition {
025: /**
026: * a position in the AST in Haskell notation
027: */
028: final public String position;
029:
030: /**
031: * true means green, false means red (janna guesses)
032: */
033: final public boolean correctPosition;
034:
035: /**
036: * creates a LinPosition
037: * @param p the position in the AST in Haskell notation like [0,1,2]
038: * @param cor false iff there are violated constraints
039: */
040: LinPosition(String p, boolean cor) {
041: position = p;
042: correctPosition = cor;
043: }
044:
045: /**
046: * Creates a position string in Haskell notation for the argument
047: * number nr of this node.
048: * @param nr The number of the wanted argument
049: * @return the position string for the nrth child
050: */
051: public String childPosition(int nr) {
052: return calculateChildPosition(this .position, nr);
053: }
054:
055: /**
056: * Creates a position string in Haskell notation for the argument
057: * number nr for the position pos
058: * @param pos The position of the to be parent
059: * @param nr The number of the wanted argument
060: * @return the position string for the nrth child of pos
061: */
062: protected static String calculateChildPosition(String pos, int nr) {
063: if ("[]".equals(pos)) {
064: return "[" + nr + "]";
065: } else {
066: return pos.trim().substring(0, pos.length() - 1) + "," + nr
067: + "]";
068: }
069: }
070:
071: /**
072: * Creates a position string in Haskell notation for the argument
073: * number nr for the position pos' parent, i.e. brethren number nr.
074: * Example: calculateBrethrenPosition("[0,0,1]", 3).equals("[0,0,3]")
075: * @param pos The position of a brethren of the wanted
076: * @param nr The number of the wanted brethren
077: * @return the position string for the nrth brother of pos
078: */
079: protected static String calculateBrethrenPosition(String pos, int nr) {
080: if ("[]".equals(pos)) {
081: return "[]"; //no brethren possible here
082: } else if (pos.lastIndexOf(',') == -1) {
083: return "[" + nr + "]"; //one below top
084: } else {
085: final String newPos = pos.substring(0,
086: pos.lastIndexOf(',') + 1)
087: + nr + "]";
088: return newPos;
089: }
090:
091: }
092:
093: /**
094: * compares two position strings and returns true, if superPosition is
095: * a prefix of subPosition, that is, if subPosition is in a subtree of
096: * superPosition
097: * @param superPosition the position String in Haskell notation
098: * ([0,1,0,4]) of the to-be super-branch of subPosition
099: * @param subPosition the position String in Haskell notation
100: * ([0,1,0,4]) of the to-be (grand-)child-branch of superPosition
101: * @return true iff superPosition denotes an ancestor of subPosition
102: */
103: public static boolean isSubtreePosition(
104: final LinPosition super Position,
105: final LinPosition subPosition) {
106: if (super Position == null || subPosition == null) {
107: return false;
108: }
109: String super Pos = super Position.position;
110: String subPos = subPosition.position;
111: if (super Pos.length() < 2 || subPos.length() < 2) {
112: return false;
113: }
114: super Pos = super Pos.substring(1, super Pos.length() - 1);
115: subPos = subPos.substring(1, subPos.length() - 1);
116: boolean result = subPos.startsWith(super Pos);
117: return result;
118: }
119:
120: /**
121: * Returns the biggest position of first and second.
122: * Each word in the linearization area has the corresponding
123: * position in the tree. The position-notion is taken from
124: * GF-Haskell, where empty position ("[]")
125: * represents tree-root, "[0]" represents first child of the root,
126: * "[0,0]" represents the first grandchild of the root etc.
127: * So comparePositions("[0]","[0,0]")="[0]"
128: */
129: public static String maxPosition(String first, String second) {
130: String common = "[]";
131: int i = 1;
132: while ((i < Math.min(first.length() - 1, second.length() - 1))
133: && (first.substring(0, i + 1).equals(second.substring(
134: 0, i + 1)))) {
135: common = first.substring(0, i + 1);
136: i += 2;
137: }
138: if (common.charAt(common.length() - 1) == ']') {
139: return common;
140: } else {
141: return common + "]";
142: }
143: }
144:
145: /**
146: * @return The Haskell position string for the parent of this position.
147: * If self is already the top node, [] is returned.
148: */
149: public String parentPosition() {
150: if (this .position.equals("[]")) {
151: return this .position;
152: } else if (this .position.lastIndexOf(',') == -1) {
153: return "[]"; //one below top
154: } else {
155: final String newPos = this .position.substring(0,
156: this .position.lastIndexOf(','))
157: + "]";
158: return newPos;
159: }
160: }
161:
162: public String toString() {
163: return position + (correctPosition ? " correct" : " incorrect");
164: }
165: }
|