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.Services;
016: import de.uka.ilkd.key.java.TypeConverter;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.expression.Operator;
019: import de.uka.ilkd.key.java.reference.ExecutionContext;
020: import de.uka.ilkd.key.java.visitor.Visitor;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: /**
024: * Shift right.
025: * @author <TT>AutoDoc</TT>
026: */
027: public class ShiftRight extends Operator {
028:
029: /**
030: * Shift right.
031: */
032: public ShiftRight() {
033: }
034:
035: /**
036: * Shift right.
037: * @param lhs an expression.
038: * @param rhs an expression.
039: */
040: public ShiftRight(Expression lhs, Expression rhs) {
041: super (lhs, rhs);
042: }
043:
044: /**
045: * Constructor for the transformation of COMPOST ASTs to KeY.
046: * The first occurrence of an Expression in the given list is taken as
047: * the left hand side
048: * of the expression, the second occurrence is taken as the right hand
049: * side of the expression.
050: * @param children the children of this AST element as KeY classes.
051: */
052: public ShiftRight(ExtList children) {
053: super (children);
054: }
055:
056: /**
057: * Get arity.
058: * @return the int value.
059: */
060:
061: public int getArity() {
062: return 2;
063: }
064:
065: /**
066: * Get precedence.
067: * @return the int value.
068: */
069:
070: public int getPrecedence() {
071: return 4;
072: }
073:
074: /**
075: * Get notation.
076: * @return the int value.
077: */
078:
079: public int getNotation() {
080: return INFIX;
081: }
082:
083: /** calls the corresponding method of a visitor in order to
084: * perform some action/transformation on this element
085: * @param v the Visitor
086: */
087: public void visit(Visitor v) {
088: v.performActionOnShiftRight(this );
089: }
090:
091: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
092: p.printShiftRight(this );
093: }
094:
095: public KeYJavaType getKeYJavaType(Services javaServ,
096: ExecutionContext ec) {
097: final TypeConverter tc = javaServ.getTypeConverter();
098: return tc.getPromotedType(tc.getKeYJavaType(
099: (Expression) getChildAt(0), ec));
100: }
101: }
|