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 de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.reference.ExecutionContext;
016: import de.uka.ilkd.key.util.ExtList;
017:
018: /**
019: * Operator base class.
020: * @author AL
021: */
022:
023: public abstract class Operator extends JavaNonTerminalProgramElement
024: implements Expression, ExpressionContainer {
025:
026: /**
027: * Children.
028: */
029: protected final ArrayOfExpression children;
030:
031: /**
032: * Relative positioning of the operator.
033: */
034:
035: public static final int PREFIX = 0;
036: public static final int INFIX = 1;
037: public static final int POSTFIX = 2;
038:
039: public Operator() {
040: this .children = null;
041: }
042:
043: /**
044: Operator.
045: @param lhs an expression.
046: @param rhs an expression.
047: */
048: public Operator(Expression lhs, Expression rhs) {
049: this .children = new ArrayOfExpression(new Expression[] { lhs,
050: rhs });
051: }
052:
053: /**
054: * Constructor for the transformation of COMPOST ASTs to KeY.
055: * @param children the children of this AST element as KeY classes.
056: * In this case the order of the children is IMPORTANT.
057: * May contain:
058: * 2 of Expression (the first Expression as left hand
059: * side, the second as right hand side),
060: * Comments
061: *
062: */
063: public Operator(ExtList children) {
064: super (children);
065: this .children = new ArrayOfExpression((Expression[]) children
066: .collect(Expression.class));
067: }
068:
069: /**
070: * Operator.
071: * @param unaryChild an expression.
072: */
073:
074: public Operator(Expression unaryChild) {
075: this .children = new ArrayOfExpression(unaryChild);
076: }
077:
078: /**
079: * Operator.
080: * @param arguments an array of expression.
081: */
082:
083: public Operator(Expression[] arguments) {
084: this .children = new ArrayOfExpression(arguments);
085: }
086:
087: /**
088: * getArity() == getASTchildren().size()
089: */
090: public abstract int getArity();
091:
092: /** 0 is the "highest" precedence (obtained by parantheses),
093: * 13 the "lowest".
094: */
095:
096: public abstract int getPrecedence();
097:
098: /**
099: * @return true, if a has a higher priority (a lower precendence value)
100: * than b.
101: */
102:
103: public static boolean precedes(Operator a, Operator b) {
104: return a.getPrecedence() < b.getPrecedence();
105: }
106:
107: /**
108: * @return INFIX, PREFIX, or POSTFIX.
109: */
110: public abstract int getNotation();
111:
112: /**
113: * Checks if this operator is left or right associative. The associativity
114: * defines the order in which the arguments are evaluated (left-to-right
115: * or right-to-left). The default is left associative. Unary operators,
116: * assignments and conditionals are right associative.
117: * @return <CODE>true</CODE>, if the operator is left associative,
118: * <CODE>false</CODE> otherwise.
119: */
120: public boolean isLeftAssociative() {
121: return true;
122: }
123:
124: public SourceElement getFirstElement() {
125: switch (getNotation()) {
126: case INFIX:
127: case POSTFIX:
128: return children.getExpression(0).getFirstElement();
129: case PREFIX:
130: default:
131: return this ;
132: }
133: }
134:
135: public SourceElement getLastElement() {
136: switch (getNotation()) {
137: case INFIX:
138: case PREFIX:
139: return children.getExpression(getArity() - 1)
140: .getLastElement();
141: case POSTFIX:
142: default:
143: return this ;
144: }
145: }
146:
147: /**
148: * Returns the number of children of this node.
149: * @return an int giving the number of children of this node
150: */
151:
152: public int getChildCount() {
153: return (children != null) ? children.size() : 0;
154: }
155:
156: /**
157: * Returns the child at the specified index in this node's "virtual"
158: * child array
159: * @param index an index into this node's "virtual" child array
160: * @return the program element at the given position
161: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
162: * of bounds
163: */
164: public ProgramElement getChildAt(int index) {
165: if (children != null) {
166: return children.getExpression(index);
167: }
168: throw new ArrayIndexOutOfBoundsException();
169: }
170:
171: /**
172: * Get the number of expressions in this container.
173: * @return the number of expressions.
174: */
175:
176: public int getExpressionCount() {
177: return (children != null) ? children.size() : 0;
178: }
179:
180: /*
181: Return the expression at the specified index in this node's
182: "virtual" expression array.
183: @param index an index for an expression.
184: @return the expression with the given index.
185: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
186: of bounds.
187: */
188:
189: public Expression getExpressionAt(int index) {
190: if (children != null) {
191: return children.getExpression(index);
192: }
193: throw new ArrayIndexOutOfBoundsException();
194: }
195:
196: /** return arguments */
197: public ArrayOfExpression getArguments() {
198: return children;
199: }
200:
201: // has to be changed
202: public boolean isToBeParenthesized() {
203: return false;
204: }
205:
206: /** overriden from JavaProgramElement.
207: */
208: public String reuseSignature(Services services, ExecutionContext ec) {
209: return super .reuseSignature(services, ec)
210: + "("
211: + services.getTypeConverter().getKeYJavaType(this , ec)
212: .getName() + ")";
213: }
214:
215: public abstract KeYJavaType getKeYJavaType(Services javaServ,
216: ExecutionContext ec);
217:
218: }
|