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.statement;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.visitor.Visitor;
015: import de.uka.ilkd.key.util.ExtList;
016:
017: /**
018: * Case.
019: *
020: */
021: public class Case extends BranchImp implements ExpressionContainer {
022:
023: /**
024: * Expression.
025: */
026: protected final Expression expression;
027:
028: /**
029: * Body.
030: */
031: protected final ArrayOfStatement body;
032:
033: /**
034: * Case.
035: */
036: public Case() {
037: this .expression = null;
038: this .body = null;
039: }
040:
041: /**
042: * Case.
043: * @param e an expression.
044: */
045: public Case(Expression e) {
046: this .expression = e;
047: this .body = null;
048: }
049:
050: /**
051: * Case.
052: * @param e an expression.
053: * @param body a statement mutable list.
054: */
055: public Case(Expression e, Statement[] body) {
056: this .body = new ArrayOfStatement(body);
057: this .expression = e;
058: }
059:
060: /**
061: * Constructor for the transformation of COMPOST ASTs to KeY.
062: * @param children the children of this AST element as KeY classes.
063: * May contain: Comments
064: * a Statement (as the statement following case)
065: * Must NOT contain: an Expression indicating the condition of the case
066: * as there are classes that are Expression and Statement, so they might
067: * get mixed up. Use the second parameter of this constructor for the
068: * expression.
069: * @param expr the expression of the case
070: */
071: public Case(ExtList children, Expression expr, PositionInfo pos) {
072: super (children, pos);
073: this .expression = expr;
074: this .body = new ArrayOfStatement((Statement[]) children
075: .collect(Statement.class));
076: }
077:
078: /**
079: * Returns the number of children of this node.
080: * @return an int giving the number of children of this node
081: */
082: public int getChildCount() {
083: int result = 0;
084: if (expression != null)
085: result++;
086: if (body != null)
087: result += body.size();
088: return result;
089: }
090:
091: /**
092: * Returns the child at the specified index in this node's "virtual"
093: * child array
094: * @param index an index into this node's "virtual" child array
095: * @return the program element at the given position
096: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
097: * of bounds
098: */
099: public ProgramElement getChildAt(int index) {
100: int len;
101: if (expression != null) {
102: if (index == 0)
103: return expression;
104: index--;
105: }
106: if (body != null) {
107: len = body.size();
108: if (len > index) {
109: return body.getStatement(index);
110: }
111: index -= len;
112: }
113: throw new ArrayIndexOutOfBoundsException();
114: }
115:
116: /**
117: * Get the number of expressions in this container.
118: * @return the number of expressions.
119: */
120:
121: public int getExpressionCount() {
122: return (expression != null) ? 1 : 0;
123: }
124:
125: /*
126: Return the expression at the specified index in this node's
127: "virtual" expression array.
128: @param index an index for an expression.
129: @return the expression with the given index.
130: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
131: of bounds.
132: */
133: public Expression getExpressionAt(int index) {
134: if (expression != null && index == 0) {
135: return expression;
136: }
137: throw new ArrayIndexOutOfBoundsException();
138: }
139:
140: /**
141: * Get the number of statements in this container.
142: * @return the number of statements.
143: */
144: public int getStatementCount() {
145: return (body != null) ? body.size() : 0;
146: }
147:
148: /*
149: Return the statement at the specified index in this node's
150: "virtual" statement array.
151: @param index an index for a statement.
152: @return the statement with the given index.
153: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
154: of bounds.
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 expression.
165: * @return the expression.
166: */
167: public Expression getExpression() {
168: return expression;
169: }
170:
171: /**
172: * The body may be empty (null), to define a fall-through.
173: * Attaching an {@link EmptyStatement} would create a single ";".
174: */
175: public ArrayOfStatement getBody() {
176: return body;
177: }
178:
179: /** calls the corresponding method of a visitor in order to
180: * perform some action/transformation on this element
181: * @param v the Visitor
182: */
183: public void visit(Visitor v) {
184: v.performActionOnCase(this );
185: }
186:
187: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
188: p.printCase(this);
189: }
190: }
|