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