//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package parser.ast;

import param.BigRational;
import parser.EvaluateContext;
import parser.type.TypeInt;
import parser.visitor.ASTVisitor;
import prism.PrismLangException;

public class ExpressionBinaryOp extends Expression
{
	// Operator constants
	public static final int IMPLIES = 1;
	public static final int IFF = 2;
	public static final int OR = 3;
	public static final int AND = 4;
	public static final int EQ = 5;
	public static final int NE = 6;
	public static final int GT = 7;
	public static final int GE = 8;
	public static final int LT = 9;
	public static final int LE = 10;
	public static final int PLUS = 11;
	public static final int MINUS = 12;
	public static final int TIMES = 13;
	public static final int DIVIDE = 14;
	// Operator symbols
	public static final String opSymbols[] = { "", "=>", "<=>", "|", "&", "=", "!=", ">", ">=", "<", "<=", "+", "-", "*", "/" };
	// Operator type testers
	public static boolean isLogical(int op) { return op==IMPLIES || op==IFF || op==OR || op==AND; }
	public static boolean isRelOp(int op) { return op==EQ || op==NE || op==GT ||  op==GE || op==LT || op==LE; }
	public static boolean isArithmetic(int op) { return op==PLUS || op==MINUS || op==TIMES ||  op==DIVIDE; }
	
	// Operator
	protected int op = 0;
	// Pair of operands
	protected Expression operand1 = null;
	protected Expression operand2 = null;

	// Constructors

	public ExpressionBinaryOp()
	{
	}

	public ExpressionBinaryOp(int op, Expression operand1, Expression operand2)
	{
		this.operand1 = operand1;
		this.operand2 = operand2;
		this.op = op;
	}

	// Set methods

	public void setOperator(int i)
	{
		op = i;
	}

	/**
	 * Set the operator from the operator symbol.
	 */
	public void setOperator(String s) throws PrismLangException
	{
		for (int i = 1; i < opSymbols.length; i++) {
			if (opSymbols[i].equals(s)) {
				setOperator(i);
				return;
			}
		}
		throw new PrismLangException("Unknown binary operator '" + s + "'");
	}

	public void setOperand1(Expression e1)
	{
		operand1 = e1;
	}

	public void setOperand2(Expression e2)
	{
		operand2 = e2;
	}

	// Get methods

	public int getOperator()
	{
		return op;
	}

	public String getOperatorSymbol()
	{
		return opSymbols[op];
	}

	public Expression getOperand1()
	{
		return operand1;
	}

	public Expression getOperand2()
	{
		return operand2;
	}

	// Methods required for Expression:

	@Override
	public boolean isConstant()
	{
		return operand1.isConstant() && operand2.isConstant();
	}

	@Override
	public boolean isProposition()
	{
		return operand1.isProposition() && operand2.isProposition();
	}

	@Override
	public Object evaluate(EvaluateContext ec) throws PrismLangException
	{
		switch (op) {
		case IMPLIES:
			return !operand1.evaluateBoolean(ec) || operand2.evaluateBoolean(ec);
		case IFF:
			return operand1.evaluateBoolean(ec) == operand2.evaluateBoolean(ec);
		case OR:
			return operand1.evaluateBoolean(ec) || operand2.evaluateBoolean(ec);
		case AND:
			return operand1.evaluateBoolean(ec) && operand2.evaluateBoolean(ec);
		case EQ:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				return operand1.evaluateInt(ec) == operand2.evaluateInt(ec);
			} else {
				return operand1.evaluateDouble(ec) == operand2.evaluateDouble(ec);
			}
		case NE:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				return operand1.evaluateInt(ec) != operand2.evaluateInt(ec);
			} else {
				return operand1.evaluateDouble(ec) != operand2.evaluateDouble(ec);
			}
		case GT:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				return operand1.evaluateInt(ec) > operand2.evaluateInt(ec);
			} else {
				return operand1.evaluateDouble(ec) > operand2.evaluateDouble(ec);
			}
		case GE:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				return operand1.evaluateInt(ec) >= operand2.evaluateInt(ec);
			} else {
				return operand1.evaluateDouble(ec) >= operand2.evaluateDouble(ec);
			}
		case LT:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				return operand1.evaluateInt(ec) < operand2.evaluateInt(ec);
			} else {
				return operand1.evaluateDouble(ec) < operand2.evaluateDouble(ec);
			}
		case LE:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				return operand1.evaluateInt(ec) <= operand2.evaluateInt(ec);
			} else {
				return operand1.evaluateDouble(ec) <= operand2.evaluateDouble(ec);
			}
		case PLUS:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				try {
					return Math.addExact(operand1.evaluateInt(ec), operand2.evaluateInt(ec));
				} catch (ArithmeticException e) {
					throw new PrismLangException(e.getMessage(), this);
				}
			} else {
				return operand1.evaluateDouble(ec) + operand2.evaluateDouble(ec);
			}
		case MINUS:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				try {
					return Math.subtractExact(operand1.evaluateInt(ec), operand2.evaluateInt(ec));
				} catch (ArithmeticException e) {
					throw new PrismLangException(e.getMessage(), this);
				}
			} else {
				return operand1.evaluateDouble(ec) - operand2.evaluateDouble(ec);
			}
		case TIMES:
			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
				try {
					return Math.multiplyExact(operand1.evaluateInt(ec), operand2.evaluateInt(ec));
				} catch (ArithmeticException e) {
					throw new PrismLangException(e.getMessage(), this);
				}
			} else {
				return operand1.evaluateDouble(ec) * operand2.evaluateDouble(ec);
			}
		case DIVIDE:
			return operand1.evaluateDouble(ec) / operand2.evaluateDouble(ec);
		}
		throw new PrismLangException("Unknown binary operator", this);
	}
	
	@Override
	public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException
	{
		BigRational v1 = operand1.evaluateExact(ec);
		BigRational v2 = operand2.evaluateExact(ec);

		switch (op) {
		case IMPLIES:
			return BigRational.from(!v1.toBoolean() || v2.toBoolean());
		case IFF:
			return BigRational.from(v1.toBoolean() == v2.toBoolean());
		case OR:
			return BigRational.from(v1.toBoolean() || v2.toBoolean());
		case AND:
			return BigRational.from(v1.toBoolean() && v2.toBoolean());
		case EQ:
			return BigRational.from(v1.equals(v2));
		case NE:
			return BigRational.from(!v1.equals(v2));
		case GT:
			return BigRational.from(v1.compareTo(v2) > 0);
		case GE:
			return BigRational.from(v1.equals(v2) || v1.compareTo(v2) > 0);
		case LT:
			return BigRational.from(v1.compareTo(v2) < 0);
		case LE:
			return BigRational.from(v1.equals(v2) || v1.compareTo(v2) < 0);
		case PLUS:
			return v1.add(v2);
		case MINUS:
			return v1.subtract(v2);
		case TIMES:
			return v1.multiply(v2);
		case DIVIDE:
			return v1.divide(v2);
		}
		throw new PrismLangException("Unknown binary operator", this);
	}


	@Override
	public boolean returnsSingleValue()
	{
		return operand1.returnsSingleValue() && operand2.returnsSingleValue();
	}

	// Methods required for ASTElement:

	@Override
	public Object accept(ASTVisitor v) throws PrismLangException
	{
		return v.visit(this);
	}

	@Override
	public Expression deepCopy()
	{
		ExpressionBinaryOp expr = new ExpressionBinaryOp(op, operand1.deepCopy(), operand2.deepCopy());
		expr.setType(type);
		expr.setPosition(this);
		return expr;
	}

	// Standard methods
	
	@Override
	public String toString()
	{
		return operand1 + opSymbols[op] + operand2;
	}

	@Override
	public int hashCode()
	{
		final int prime = 31;
		int result = 1;
		result = prime * result + op;
		result = prime * result + ((operand1 == null) ? 0 : operand1.hashCode());
		result = prime * result + ((operand2 == null) ? 0 : operand2.hashCode());
		return result;
	}
	@Override
	public boolean equals(Object obj)
	{
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		ExpressionBinaryOp other = (ExpressionBinaryOp) obj;
		if (op != other.op)
			return false;
		if (operand1 == null) {
			if (other.operand1 != null)
				return false;
		} else if (!operand1.equals(other.operand1))
			return false;
		if (operand2 == null) {
			if (other.operand2 != null)
				return false;
		} else if (!operand2.equals(other.operand2))
			return false;
		return true;
	}
}

// ------------------------------------------------------------------------------
