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.expression;
012:
013: import java.io.IOException;
014:
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.reference.ExecutionContext;
018: import de.uka.ilkd.key.java.reference.ReferencePrefix;
019: import de.uka.ilkd.key.java.visitor.Visitor;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /** Redundant Parentheses. Modelled as a special "identity" unary "infix"
023: * operator. */
024:
025: public class ParenthesizedExpression extends Operator implements
026: ExpressionStatement, ReferencePrefix {
027:
028: /**
029: * Constructor for the transformation of COMPOST ASTs to KeY.
030: * @param children the children of this AST element as KeY classes.
031: * In this case the order of the children is IMPORTANT.
032: * May contain:
033: * several of Expression (should be one, the first is taken
034: * as parenthesized expression),
035: * Comments
036: */
037: public ParenthesizedExpression(ExtList children) {
038: super (children);
039: }
040:
041: public ParenthesizedExpression(Expression child) {
042: super (child);
043: }
044:
045: /**
046: * Returns the number of children of this node.
047: * @return an int giving the number of children of this node
048: */
049: public int getChildCount() {
050: return (children != null) ? children.size() : 0;
051: }
052:
053: /**
054: * Returns the child at the specified index in this node's "virtual"
055: * child array
056: * @param index an index into this node's "virtual" child array
057: * @return the program element at the given position
058: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
059: * of bounds
060: */
061: public ProgramElement getChildAt(int index) {
062: if (children != null) {
063: return children.getExpression(index);
064: }
065: throw new ArrayIndexOutOfBoundsException();
066: }
067:
068: /**
069: * Get arity.
070: * @return the int value.
071: */
072: public int getArity() {
073: return 1;
074: }
075:
076: /**
077: * Get precedence.
078: * @return the int value.
079: */
080: public int getPrecedence() {
081: return 0;
082: }
083:
084: /**
085: * Get notation.
086: * @return the int value.
087: */
088: public int getNotation() {
089: return INFIX;
090: /* Only unary infix operator;) */
091: }
092:
093: public SourceElement getFirstElement() {
094: return this ;
095: }
096:
097: public SourceElement getLastElement() {
098: return this ;
099: }
100:
101: /** calls the corresponding method of a visitor in order to
102: * perform some action/transformation on this element
103: * @param v the Visitor
104: */
105: public void visit(Visitor v) {
106: v.performActionOnParenthesizedExpression(this );
107: }
108:
109: public void prettyPrint(PrettyPrinter w) throws IOException {
110: w.printParenthesizedExpression(this );
111: }
112:
113: /**
114: * We do not have a prefix, so fake it!
115: * This way we implement ReferencePrefix
116: * @author VK
117: */
118: public ReferencePrefix getReferencePrefix() {
119: return null;
120: }
121:
122: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
123: return this ;
124: }
125:
126: public KeYJavaType getKeYJavaType(Services javaServ,
127: ExecutionContext ec) {
128: return getExpressionAt(0).getKeYJavaType(javaServ, ec);
129: }
130:
131: }
|