//==============================================================================
//	
//	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.*;
import parser.type.TypeBool;
import parser.visitor.*;
import prism.PrismLangException;

public class ExpressionFilter extends Expression
{
	/**
	 * Types of filter, for expressions of the form "filter(op, prop, states)",
	 * with filter states "states" being optional (denoting "true").
	 */ 
	public enum FilterOperator {
		/** Minimum value of prop over all filter states */
		MIN ("min"),
		/** Maximum value of prop over all filter states */
		MAX ("max"),
		/** True for the filter states that yield the minimum value of prop */
		ARGMIN ("argmin"),
		/** True for the filter states that yield the maximum value of prop */
		ARGMAX ("argmax"),
		/** Number of filter states for which prop is true */
		COUNT ("count"),
		/** Sum of the value of prop for all filter states */
		SUM ("sum"),
		/** Average of the value of prop over all filter states */
		AVG ("avg"),
		/** Value of prop for the first (lowest-indexed) filter state */
		FIRST ("first"),
		/** Range (interval) of values of prop over all filter states */
		RANGE ("range"),
		/** True iff prop is true for all filter states */
		FORALL ("forall"),
		/** True iff prop is true for some filter states */
		EXISTS ("exists"),
		/** Print the (non-zero) values to the log */
		PRINT ("print"),
		/** Print all (including zero) values to the log */
		PRINTALL ("printall"),
		/** Value for the single filter state (if there is more than one, this is an error) */
		STATE ("state");
		public final String keyword;
		FilterOperator(final String keyword) {
			this.keyword = keyword;
		}
	};

	// Operator used in filter
	// (and string representation of)
	private FilterOperator opType;
	private String opName;
	// Expression that filter is applied to
	private Expression operand;
	// Expression defining states that filter is over
	// (optional; can be null, denoting "true")
	private Expression filter;
	
	// Filter can be invisible, meaning it is not actually displayed
	// by toString(). This is used to add filters to P/R/S operators that
	// were created with old-style filter syntax. 
	private boolean invisible = false;
	// Whether or not an explanation should be displayed when model checking
	private boolean explanationEnabled = true;
	// Do we need to store a copy of the results vector when model checking this?
	private boolean storeVector = false;
	// whether this is a filter over parameters
	private boolean param = false;
	

	// Constructors

	public ExpressionFilter(String opName, Expression operand)
	{
		this(opName, operand, null);
	}

	public ExpressionFilter(String opName, Expression operand, Expression filter)
	{
		setOperator(opName);
		setOperand(operand);
		setFilter(filter);
	}

	// Set methods

	public void setOperator(String opName)
	{
		this.opName = opName;
		for (FilterOperator op : FilterOperator.values()) {
			if (op.keyword.equals(opName)) {
				opType = op;
				return;
			}
		}
		// handle shorthands
		if ("+".equals(opName)) {
			opType = FilterOperator.SUM;
		} else if ("&".equals(opName)) {
			opType = FilterOperator.FORALL;
		} else if ("|".equals(opName)) {
			opType = FilterOperator.EXISTS;
		} else {
			opType = null;
		}
	}

	public void setOperand(Expression operand)
	{
		this.operand = operand;
	}
	
	public void setFilter(Expression filter)
	{
		this.filter = filter;
	}
	
	public void setInvisible(boolean invisible)
	{
		this.invisible = invisible;
	}
	
	public void setExplanationEnabled(boolean explanationEnabled)
	{
		this.explanationEnabled = explanationEnabled;
	}
	
	public void setStoreVector(boolean storeVector)
	{
		this.storeVector = storeVector;
	}
	
	public void setParam()
	{
		param = true;
	}

	// Get methods

	public FilterOperator getOperatorType()
	{
		return opType;
	}

	public String getOperatorName()
	{
		return opName;
	}

	public Expression getOperand()
	{
		return operand;
	}

	public Expression getFilter()
	{
		return filter;
	}

	public boolean isInvisible()
	{
		return invisible;
	}

	public boolean getExplanationEnabled()
	{
		return explanationEnabled;
	}
	
	public boolean getStoreVector()
	{
		return storeVector;
	}
	
	public boolean isParam()
	{
		return param;
	}
	
	// Methods required for Expression:

	@Override
	public boolean isConstant()
	{
		// Note: In some sense, ExpressionFilters are (often) constant since they return the same
		// value for every state. But the actual value is model dependent, so they are not
		// considered to be constants.
		return false;
	}

	@Override
	public boolean isProposition()
	{
		return false;
	}
	
	@Override
	public Object evaluate(EvaluateContext ec) throws PrismLangException
	{
		throw new PrismLangException("Cannot evaluate a filter without a model");
	}

	@Override
	public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException
	{
		throw new PrismLangException("Cannot evaluate a filter without a model");
	}

	@Override
	public boolean returnsSingleValue()
	{
		// Most filters return a single value, but there are some exceptions...
		if (opType == FilterOperator.PRINT) return false;
		else if (opType == FilterOperator.PRINTALL) return false;
		else if (opType == FilterOperator.ARGMIN) return false;
		else if (opType == FilterOperator.ARGMAX) return false;
		else if (param) return false;
		else return true;
	}
	
	// Methods required for ASTElement:

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

	@Override
	public Expression deepCopy()
	{
		ExpressionFilter e;
		e = new ExpressionFilter(opName, operand.deepCopy(), filter == null ? null : filter.deepCopy());
		e.setInvisible(invisible);
		e.setType(type);
		e.setPosition(this);
		e.param = this.param;

		return e;
	}
	
	// Standard methods
	
	@Override
	public String toString()
	{
		String s = "";
		if (invisible)
			return operand.toString();
		s += (param ? "paramfilter(" : "filter(") + opName + ", " + operand;
		if (filter != null)
			s += ", " + filter;
		s += ")";
		return s;
	}

	@Override
	public int hashCode()
	{
		final int prime = 31;
		int result = 1;
		result = prime * result + (explanationEnabled ? 1231 : 1237);
		result = prime * result + ((filter == null) ? 0 : filter.hashCode());
		result = prime * result + (invisible ? 1231 : 1237);
		result = prime * result + ((opName == null) ? 0 : opName.hashCode());
		result = prime * result + ((opType == null) ? 0 : opType.hashCode());
		result = prime * result + ((operand == null) ? 0 : operand.hashCode());
		result = prime * result + (param ? 1231 : 1237);
		result = prime * result + (storeVector ? 1231 : 1237);
		return result;
	}

	@Override
	public boolean equals(Object obj)
	{
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		ExpressionFilter other = (ExpressionFilter) obj;
		if (explanationEnabled != other.explanationEnabled)
			return false;
		if (filter == null) {
			if (other.filter != null)
				return false;
		} else if (!filter.equals(other.filter))
			return false;
		if (invisible != other.invisible)
			return false;
		if (opName == null) {
			if (other.opName != null)
				return false;
		} else if (!opName.equals(other.opName))
			return false;
		if (opType != other.opType)
			return false;
		if (operand == null) {
			if (other.operand != null)
				return false;
		} else if (!operand.equals(other.operand))
			return false;
		if (param != other.param)
			return false;
		if (storeVector != other.storeVector)
			return false;
		return true;
	}
	
	/**
	 * Wrap a "default" ExpressionFilter around an Expression representing a property to be model checked,
	 * in order to pick out a single value (the final result of model checking) from a vector of values for all states.
	 * See the PRISM manual (or check the code below) to see the definition of the "default" filter.
	 * If the expression is already an ExpressionFilter (of the right kind), nothing is done.
	 * Note that we need to know whether the model has multiple initial states, because this affects the default filter.  
	 * @param expr Expression to be model checked
	 * @param singleInit Does the model on which it is being checked have a single initial states? 
	 */
	public static ExpressionFilter addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException
	{
		ExpressionFilter exprFilter = null;
		
		// The final result of model checking will be a single value. If the expression to be checked does not
		// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
		// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
		// return single values and have to be treated in this way.
		if (!expr.returnsSingleValue()) {
			// New filter depends on expression type and number of initial states.
			// Boolean expressions...
			if (expr.getType() instanceof TypeBool) {
				// Result is true iff true for all initial states
				exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init"));
			}
			// Non-Boolean (double or integer) expressions...
			else {
				// Result is for the initial state, if there is just one,
				// or the range over all initial states, if multiple
				if (singleInit) {
					exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init"));
				} else {
					exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init"));
				}
			}
		}
		// Even, when the expression does already return a single value, if the the outermost operator
		// of the expression is not a filter, we still need to wrap a new filter around it.
		// e.g. 2*filter(...) or 1-P=?[...{...}]
		// This because the final result of model checking is only stored when we process a filter.
		else if (!(expr instanceof ExpressionFilter)) {
			// We just pick the first value (they are all the same)
			exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init"));
			// We stop any additional explanation being displayed to avoid confusion.
			exprFilter.setExplanationEnabled(false);
		}
		// Finalise filter (if created) and return
		if (exprFilter != null) {
			// Make it invisible (not that it will be displayed)
			exprFilter.setInvisible(true);
			// Compute type of new filter expression (will be same as child)
			exprFilter.typeCheck();
			return exprFilter;
		} else {
			// If no new filter was created, we no expr is an ExpressionFilter
			return (ExpressionFilter) expr;
		}
	}
}

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