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: /**
019: * @author daniels
020: * This Class represents a parsed node in the GF AST.
021: * It knows about types, bound variables, funs.
022: * But nothing about printnames. That's what AstNodeData is for.
023: */
024: class GfAstNode {
025: /**
026: * contains the types of the bound variables in the order of their occurence
027: */
028: protected final String[] boundTypes;
029: /**
030: * contains the names of the bound variables in the order of their occurence
031: */
032: protected final String[] boundNames;
033: /**
034: * The type of this AST node
035: */
036: private final String type;
037:
038: /**
039: * @return The type of this AST node
040: */
041: protected String getType() {
042: return type;
043: }
044:
045: /**
046: * the fun represented in this AST node
047: */
048: private final String fun;
049:
050: /**
051: * @return the fun represented in this AST node.
052: * Can be a metavariable like "?1"
053: */
054: protected String getFun() {
055: return fun;
056: }
057:
058: /**
059: * @return true iff the node is a metavariable, i.e. open and not
060: * yet refined.
061: */
062: protected boolean isMeta() {
063: return fun.startsWith("?");
064: }
065:
066: /**
067: * the line that was used to build this node
068: */
069: private final String line;
070:
071: /**
072: * @return the line that was used to build this node
073: */
074: protected String getLine() {
075: return line;
076: }
077:
078: /**
079: * The constraint attached to this node
080: */
081: public final String constraint;
082:
083: /**
084: * feed this constructor the line that appears in the GF AST and
085: * it will get chopped at the right points.
086: * @param line The line from GF without the * in the beginning.
087: */
088: protected GfAstNode(final String line) {
089: this .line = line.trim();
090: final int index = this .line.lastIndexOf(" : ");
091: String typeString = this .line.substring(index + 3);
092: final int constraintIndex = typeString.indexOf(" {");
093: if (constraintIndex > -1) {
094: this .constraint = typeString.substring(constraintIndex + 1)
095: .trim();
096: this .type = typeString.substring(0, constraintIndex).trim();
097: } else {
098: this .constraint = "";
099: this .type = typeString;
100: }
101: String myFun = this .line.substring(0, index);
102: if (myFun.startsWith("\\(")) {
103: final int end = myFun.lastIndexOf(") -> ");
104: String boundPart = myFun.substring(2, end);
105: String[] bounds = boundPart.split("\\)\\s*\\,\\s*\\(");
106: this .boundNames = new String[bounds.length];
107: this .boundTypes = new String[bounds.length];
108: for (int i = 0; i < bounds.length; i++) {
109: //System.out.print("+" + bounds[i] + "-");
110: int colon = bounds[i].indexOf(" : ");
111: this .boundNames[i] = bounds[i].substring(0, colon);
112: this .boundTypes[i] = bounds[i].substring(colon + 3);
113: //System.out.println(boundNames[i] + " ;; " + boundTypes[i]);
114: }
115: myFun = myFun.substring(end + 5);
116: } else {
117: this .boundNames = new String[0];
118: this .boundTypes = new String[0];
119: }
120: this .fun = myFun;
121: }
122:
123: public String toString() {
124: return this.line;
125: }
126: }
|