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.operator;
012:
013: import de.uka.ilkd.key.java.Expression;
014: import de.uka.ilkd.key.java.PrettyPrinter;
015: import de.uka.ilkd.key.java.ProgramElement;
016: import de.uka.ilkd.key.java.reference.TypeReference;
017: import de.uka.ilkd.key.java.visitor.Visitor;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /**
021: * Type cast.
022: *
023: */
024:
025: public class TypeCast extends TypeOperator {
026:
027: /**
028: * Type cast.
029: */
030:
031: public TypeCast() {
032: }
033:
034: /**
035: * Note: The ordering of the arguments does not match the syntactical
036: * appearance of a Java type case, but the order in the superclass
037: * TypeOperator. However, getASTChildren yields them in the right
038: * order.
039: */
040: public TypeCast(Expression child, TypeReference typeref) {
041: super (child, typeref);
042: }
043:
044: /**
045: * Constructor for the transformation of COMPOST ASTs to KeY.
046: * @param children the children of this AST element as KeY classes.
047: */
048: public TypeCast(ExtList children) {
049: super (children);
050: }
051:
052: /**
053: * Returns the number of children of this node.
054: * @return an int giving the number of children of this node
055: */
056:
057: public int getChildCount() {
058: int result = 0;
059: if (typeReference != null)
060: result++;
061: if (children != null)
062: result += children.size();
063: return result;
064: }
065:
066: /**
067: * Returns the child at the specified index in this node's "virtual"
068: * child array
069: * @param index an index into this node's "virtual" child array
070: * @return the program element at the given position
071: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
072: * of bounds
073: */
074:
075: public ProgramElement getChildAt(int index) {
076: int len;
077: if (typeReference != null) {
078: if (index == 0)
079: return typeReference;
080: index--;
081: }
082: if (children != null) {
083: len = children.size();
084: if (len > index) {
085: return children.getExpression(index);
086: }
087: index -= len;
088: }
089: throw new ArrayIndexOutOfBoundsException();
090: }
091:
092: /**
093: * Get arity.
094: * @return the int value.
095: */
096:
097: public int getArity() {
098: return 1;
099: }
100:
101: /**
102: * Get precedence.
103: * @return the int value.
104: */
105:
106: public int getPrecedence() {
107: return 1;
108: }
109:
110: /**
111: * Get notation.
112: * @return the int value.
113: */
114:
115: public int getNotation() {
116: return PREFIX;
117: }
118:
119: /**
120: * Checks if this operator is left or right associative. Type casts
121: * are right associative.
122: * @return <CODE>true</CODE>, if the operator is left associative,
123: * <CODE>false</CODE> otherwise.
124: */
125:
126: public boolean isLeftAssociative() {
127: return false;
128: }
129:
130: /** calls the corresponding method of a visitor in order to
131: * perform some action/transformation on this element
132: * @param v the Visitor
133: */
134: public void visit(Visitor v) {
135: v.performActionOnTypeCast(this );
136: }
137:
138: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
139: p.printTypeCast(this);
140: }
141: }
|