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: package de.uka.ilkd.key.java;
012:
013: import de.uka.ilkd.key.java.declaration.TypeDeclaration;
014: import de.uka.ilkd.key.java.declaration.TypeDeclarationContainer;
015: import de.uka.ilkd.key.java.statement.JavaStatement;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.logic.ArrayOfProgramPrefix;
018: import de.uka.ilkd.key.logic.PosInProgram;
019: import de.uka.ilkd.key.logic.ProgramPrefix;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /**
023: * Statement block.
024: * taken from COMPOST and changed to achieve an immutable structure
025: */
026:
027: public class StatementBlock extends JavaStatement implements
028: StatementContainer, TypeDeclarationContainer, VariableScope,
029: TypeScope, ProgramPrefix {
030:
031: /**
032: * Body.
033: */
034: private final ArrayOfStatement body;
035:
036: /**
037: * contains all program prefix elements below and including itself
038: */
039: private final ArrayOfProgramPrefix prefixElementArray;
040:
041: private PosInProgram firstActiveChildPos = null;
042:
043: public StatementBlock() {
044: body = new ArrayOfStatement();
045: prefixElementArray = new ArrayOfProgramPrefix(this );
046: }
047:
048: /**
049: * Statement block.
050: * @param children an ExtList that contains the children
051: */
052:
053: public StatementBlock(ExtList children) {
054: super (children);
055: body = new ArrayOfStatement((Statement[]) children
056: .collect(Statement.class));
057:
058: prefixElementArray = computePrefixElements(body);
059: }
060:
061: public StatementBlock(ArrayOfStatement as) {
062: body = as;
063: prefixElementArray = computePrefixElements(body);
064: }
065:
066: public StatementBlock(Statement as) {
067: this (new ArrayOfStatement(as));
068: }
069:
070: public StatementBlock(Statement[] body) {
071: this (new ArrayOfStatement(body));
072: }
073:
074: private ArrayOfProgramPrefix computePrefixElements(
075: ArrayOfStatement b) {
076: return computePrefixElements(b, 0, this );
077: }
078:
079: /** computes the prefix elements for the given array of statment block */
080: public static ArrayOfProgramPrefix computePrefixElements(
081: ArrayOfStatement b, int offset, ProgramPrefix current) {
082: final ProgramPrefix[] pp;
083:
084: if (b.size() > 0 && b.getStatement(0) instanceof ProgramPrefix) {
085: final ProgramPrefix prefixElement = (ProgramPrefix) b
086: .getStatement(0);
087:
088: final int prefixLength = ((ProgramPrefix) b.getStatement(0))
089: .getPrefixLength();
090: pp = new ProgramPrefix[prefixLength + 1];
091: prefixElement.getPrefixElements().arraycopy(offset, pp, 1,
092: prefixLength);
093: } else {
094: pp = new ProgramPrefix[1];
095: }
096: pp[0] = current;
097: return new ArrayOfProgramPrefix(pp);
098: }
099:
100: /**
101: * Get body.
102: * @return the statement array wrapper.
103: */
104:
105: public ArrayOfStatement getBody() {
106: return body;
107: }
108:
109: public boolean isEmpty() {
110: return body.size() == 0;
111: }
112:
113: /**
114: * Returns the number of children of this node.
115: * @return an int giving the number of children of this node
116: */
117:
118: public int getChildCount() {
119: return body.size();
120: }
121:
122: /**
123: * Returns the child at the specified index in this node's "virtual"
124: * child array
125: * @param index an index into this node's "virtual" child array
126: * @return the program element at the given position
127: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
128: * of bounds
129: */
130:
131: public ProgramElement getChildAt(int index) {
132: if (body != null) {
133: return body.getStatement(index);
134: }
135: throw new ArrayIndexOutOfBoundsException();
136: }
137:
138: /**
139: * Get the number of statements in this container.
140: * @return the number of statements.
141: */
142:
143: public int getStatementCount() {
144: return body.size();
145: }
146:
147: /*
148: Return the statement at the specified index in this node's
149: "virtual" statement array.
150: @param index an index for a statement.
151: @return the statement with the given index.
152: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
153: of bounds.
154: */
155:
156: public Statement getStatementAt(int index) {
157: if (body != null) {
158: return body.getStatement(index);
159: }
160: throw new ArrayIndexOutOfBoundsException();
161: }
162:
163: /**
164: * Get the number of type declarations in this container.
165: * @return the number of type declarations.
166: */
167:
168: public int getTypeDeclarationCount() {
169: int count = 0;
170: if (body != null) {
171: for (int i = body.size() - 1; i >= 0; i -= 1) {
172: if (body.getStatement(i) instanceof TypeDeclaration) {
173: count += 1;
174: }
175: }
176: }
177: return count;
178: }
179:
180: /*
181: Return the type declaration at the specified index in this node's
182: "virtual" type declaration array.
183: @param index an index for a type declaration.
184: @return the type declaration with the given index.
185: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
186: of bounds.
187: */
188:
189: public TypeDeclaration getTypeDeclarationAt(int index) {
190: if (body != null) {
191: int s = body.size();
192: for (int i = 0; i < s && index >= 0; i++) {
193: Statement st = body.getStatement(i);
194: if (st instanceof TypeDeclaration) {
195: if (index == 0) {
196: return (TypeDeclaration) st;
197: }
198: index -= 1;
199: }
200: }
201: }
202: throw new ArrayIndexOutOfBoundsException();
203: }
204:
205: /** calls the corresponding method of a visitor in order to
206: * perform some action/transformation on this element
207: * @param v the Visitor
208: */
209: public void visit(Visitor v) {
210: v.performActionOnStatementBlock(this );
211: }
212:
213: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
214: p.printStatementBlock(this );
215: }
216:
217: public SourceElement getFirstElement() {
218: if (isEmpty())
219: return this ;
220: final SourceElement e = getBody().getStatement(0);
221: return (e instanceof StatementBlock) ? e.getFirstElement() : e;
222: }
223:
224: public int getPrefixLength() {
225: return prefixElementArray.size();
226: }
227:
228: public ProgramPrefix getPrefixElementAt(int i) {
229: return prefixElementArray.getProgramPrefix(i);
230: }
231:
232: public ArrayOfProgramPrefix getPrefixElements() {
233: return prefixElementArray;
234: }
235:
236: public PosInProgram getFirstActiveChildPos() {
237: if (firstActiveChildPos == null) {
238: firstActiveChildPos = isEmpty() ? PosInProgram.TOP
239: : PosInProgram.TOP.down(0);
240: }
241: return firstActiveChildPos;
242: }
243:
244: }
|