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.PositionInfo;
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.expression.Operator;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.java.reference.TypeReference;
020: import de.uka.ilkd.key.java.reference.TypeReferenceContainer;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: /**
024: * Type operator.
025: * @author <TT>AutoDoc</TT>
026: */
027:
028: public abstract class TypeOperator extends Operator implements
029: TypeReferenceContainer {
030:
031: /**
032: * Type reference.
033: */
034: protected final TypeReference typeReference;
035:
036: /**
037: * Constructor for the transformation of COMPOST ASTs to KeY.
038: * @param children the children of this AST element as KeY classes.
039: * May contain:
040: * a TypeReference (the referred type)
041: * 2 of Expression (the first Expression as left hand
042: * side, the second as right hand side),
043: * Comments
044: */
045: public TypeOperator(ExtList children) {
046: super (children);
047: typeReference = (TypeReference) children
048: .get(TypeReference.class);
049: }
050:
051: /**
052: * Constructor for the transformation of COMPOST ASTs to KeY.
053: * @param children the children of this AST element as KeY classes.
054: * May contain:
055: * a TypeReference (the referred type)
056: * 2 of Expression (the first Expression as left hand
057: * side, the second as right hand side),
058: * Comments
059: */
060: public TypeOperator(ExtList children, PositionInfo pi) {
061: super (children);
062: typeReference = (TypeReference) children
063: .get(TypeReference.class);
064: }
065:
066: public TypeOperator(Expression unaryChild, TypeReference typeref) {
067: super (unaryChild);
068: typeReference = typeref;
069: }
070:
071: public TypeOperator(Expression[] arguments, TypeReference typeref) {
072: super (arguments);
073: typeReference = typeref;
074: }
075:
076: public TypeOperator() {
077: typeReference = null;
078: }
079:
080: /**
081: * Get the number of type references in this container.
082: * @return the number of type references.
083: */
084: public int getTypeReferenceCount() {
085: return (typeReference != null) ? 1 : 0;
086: }
087:
088: /*
089: Return the type reference at the specified index in this node's
090: "virtual" type reference array.
091: @param index an index for a type reference.
092: @return the type reference with the given index.
093: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
094: of bounds.
095: */
096:
097: public TypeReference getTypeReferenceAt(int index) {
098: if (typeReference != null && index == 0) {
099: return typeReference;
100: }
101: throw new ArrayIndexOutOfBoundsException();
102: }
103:
104: /**
105: * Get type reference.
106: * @return the type reference.
107: */
108: public TypeReference getTypeReference() {
109: return typeReference;
110: }
111:
112: public KeYJavaType getKeYJavaType(Services javaServ,
113: ExecutionContext ec) {
114: return getKeYJavaType(javaServ);
115: }
116:
117: public KeYJavaType getKeYJavaType(Services javaServ) {
118: return getTypeReference().getKeYJavaType();
119: }
120:
121: }
|