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.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.visitor.Visitor;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /**
023: * Positive.
024: */
025:
026: public class Positive extends Operator {
027:
028: /**
029: * Positive.
030: * @param expr the Expression
031: */
032: public Positive(Expression expr) {
033: super (expr);
034: }
035:
036: /**
037: * Positive.
038: * @param children an ExtList with all children of this node
039: */
040: public Positive(ExtList children) {
041: super (children);
042: }
043:
044: /**
045: * Get arity.
046: * @return the int value.
047: */
048:
049: public int getArity() {
050: return 1;
051: }
052:
053: /**
054: * Get precedence.
055: * @return the int value.
056: */
057:
058: public int getPrecedence() {
059: return 1;
060: }
061:
062: /**
063: * Get notation.
064: * @return the int value.
065: */
066:
067: public int getNotation() {
068: return PREFIX;
069: }
070:
071: /**
072: * Checks if this operator is left or right associative. Ordinary
073: * unary operators are right associative.
074: * @return <CODE>true</CODE>, if the operator is left associative,
075: * <CODE>false</CODE> otherwise.
076: */
077:
078: public boolean isLeftAssociative() {
079: return false;
080: }
081:
082: /** calls the corresponding method of a visitor in order to
083: * perform some action/transformation on this element
084: * @param v the Visitor
085: */
086: public void visit(Visitor v) {
087: v.performActionOnPositive(this );
088: }
089:
090: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
091: p.printPositive(this );
092: }
093:
094: public KeYJavaType getKeYJavaType(Services services,
095: ExecutionContext ec) {
096: return services.getTypeConverter().getPromotedType(
097: getExpressionAt(0).getKeYJavaType(services, ec));
098: }
099:
100: }
|