001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: // This file is taken from the RECODER library, which is protected by the LGPL,
012: // and modified.
013: /** This class is part of the AST RECODER builds when it parses and resolves Java
014: * programs with meta constructs and schema variables. It is transformed by
015: * SchemaRecoder2KeY
016: * to a subclass of ...rule.metaconstruct.ProgramMetaConstruct.
017: */package de.uka.ilkd.key.java.recoderext;
018:
019: import recoder.java.Expression;
020: import recoder.java.ProgramElement;
021: import recoder.java.SourceVisitor;
022: import recoder.java.reference.TypeReference;
023:
024: public class RKeYMetaConstructType extends TypeReference implements
025: KeYRecoderExtension {
026:
027: /**
028: Child
029: */
030: protected Expression child = null;
031: protected String myname = "";
032:
033: protected RKeYMetaConstructType(RKeYMetaConstructType proto) {
034: super (proto);
035: if (proto.child != null) {
036: child = (Expression) proto.child.deepClone();
037: }
038: }
039:
040: public RKeYMetaConstructType() {
041: }
042:
043: /**
044: Returns the number of children of this node.
045: @return an int giving the number of children of this node
046: */
047: public int getChildCount() {
048: int result = 0;
049: if (child != null)
050: result++;
051: return result;
052: }
053:
054: /**
055: Returns the child at the specified index in this node's "virtual"
056: child array
057: @param index an index into this node's "virtual" child array
058: @return the program element at the given position
059: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
060: of bounds
061: */
062: public ProgramElement getChildAt(int index) {
063: if (child != null) {
064: if (index == 0)
065: return child;
066: }
067: throw new ArrayIndexOutOfBoundsException();
068: }
069:
070: public int getChildPositionCode(ProgramElement child0) {
071: // role 0: child
072: if (child0 == child) {
073: return 0;
074: }
075: return -1;
076: }
077:
078: public int getIndexOfChild(ProgramElement pe) {
079: if (pe == child) {
080: return 0;
081: }
082: return -1;
083: }
084:
085: public int getIndexOfChild(int posCode) {
086: if (posCode == getChildPositionCode(child)) {
087: return 0;
088: }
089: return -1;
090: }
091:
092: public int getRoleOfChild(int i) {
093: if (i == 0)
094: return getChildPositionCode(child);
095: return -1;
096: }
097:
098: /**
099: * sets a String myname of this meta construct like 'unwind-loop'
100: * @param s the String
101: */
102: public void setName(String s) {
103: myname = s;
104: }
105:
106: public String getName0() {
107: return myname;
108: }
109:
110: /**
111: Get child.
112: @return the expression.
113: */
114:
115: public Expression getChild() {
116: return child;
117: }
118:
119: /**
120: Set child.
121: @param expression a expression.
122: */
123:
124: public void setChild(Expression expression) {
125: child = expression;
126: }
127:
128: /**
129: Get the number of expression in this container.
130: @return the number of expressions.
131: */
132:
133: public int getExpressionCount() {
134: return (child != null) ? 1 : 0;
135: }
136:
137: /*
138: Return the expression at the specified index in this node's
139: "virtual" expression array.
140: @param index an index for a expression.
141: @return the expression with the given index.
142: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
143: of bounds.
144: */
145:
146: public Expression getExpressionAt(int index) {
147: if (child != null && index == 0) {
148: return child;
149: }
150: throw new ArrayIndexOutOfBoundsException();
151: }
152:
153: //don't think we need it
154: public void accept(SourceVisitor v) {
155: }
156:
157: //???
158: public Object deepClone() {
159: return null;
160: }
161:
162: }
|