//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
// This file specifies the expression language used by the Abstract
// Interpretation Framework.
//
//   expressions   e  ::=  x              variables
//                      |  f(e1,...,en)   uninterpreted functions
//                      |  \x:t.e         lambda expressions
//
//   types         t  ::= b                   user-defined/built-in base types
//                      | t1 * ... * tn -> t' function type

namespace Microsoft.AbstractInterpretationFramework
{
    using System.Collections;
    using Microsoft.Contracts;

    //----------------------------- Expressions -----------------------------

    /// <summary>
    ///  An interface for expressions.  This expression language is specified
    ///  by interfaces to allow the client to be able to use their existing
    ///  AST nodes as AIF expressions.
    /// 
    ///  This only serves as a place for operations on expressions.  Clients
    ///  should implement directly either IVariable or IFunApp.
    /// </summary>
    public interface IExpr
    {
        /// <summary>
        /// Execute a visit over the expression.
        /// </summary>
        /// <param name="visitor">The expression visitor.</param>
        /// <returns>The result of the visit.</returns>
        [Pure] object DoVisit(ExprVisitor! visitor);

        // TODO: Type checking of the expressions.
    }

    /// <summary>
    ///  An interface for variables.
    /// 
    ///  This interface should be implemented by the client.
    /// </summary>
    public interface IVariable : IExpr
    {
      string! Name { get; }    // Each client must define the name for variables
    }

    /// <summary>
    ///  An interface for function applications.
    /// 
    ///  This interface should be implemented by the client.
    /// </summary>
    public interface IFunApp : IExpr
    {
        IFunctionSymbol! FunctionSymbol { get; }
        IList/*<IExpr!>*/! Arguments
        {
            [Pure][Rep] get
            ensures result.IsReadOnly;
            ;
        }

        /// <summary>
        ///  Provides a method to create a new uninterpreted function
        ///  with the same function symbol but with the arguments with
        ///  args.
        /// </summary>
        /// <param name="args">The new arguments.</param>
        /// <returns>A copy of the function with the new arguments.</returns>
        IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)
        //TODO  requires this.Arguments.Count == args.Count;
        ;
    }

    /// <summary>
    ///  An interface for anonymous functions (i.e., lambda expressions)
    /// </summary>
    public interface IFunction : IExpr
    {
        IVariable! Param { get; }
        AIType! ParamType { get; }
        IExpr! Body { get; }

        IFunction! CloneWithBody(IExpr! body);
    }

    /// <summary>
    /// An abstract class that provides an interface for expression visitors.
    /// </summary>
    public abstract class ExprVisitor
    {
        public abstract object Default(IExpr! expr);

        public virtual object VisitVariable(IVariable! var)
        {
            return Default(var);
        }

        public virtual object VisitFunApp(IFunApp! funapp)
        {
            return Default(funapp);
        }

        public virtual object VisitFunction(IFunction! fun)
        {
            return Default(fun);
        }
    }

    /// <summary>
    ///  A utility class for dealing with expressions.
    /// </summary>
    public sealed class ExprUtil
    {
        /// <summary>
        ///  Yield an expression that is 'inexpr' with 'var' replaced by 'subst'.
        /// </summary>
        /// <param name="subst">The expression to substitute.</param>
        /// <param name="var">The variable to substitute for.</param>
        /// <param name="inexpr">The expression to substitute into.</param>
        public static IExpr! Substitute(IExpr! subst, IVariable! var, IExpr! inexpr)
        {
            IExpr result = null;

            if (inexpr is IVariable)
            {
                result = inexpr.Equals(var) ? subst : inexpr;
            }
            else if (inexpr is IFunApp)
            {
                IFunApp! funapp = (IFunApp!)inexpr;
                IList newargs = null;
                newargs = new ArrayList{ IExpr! arg in funapp.Arguments; Substitute(subst, var, arg) };
                result = funapp.CloneWithArguments(newargs);
            }
            else if (inexpr is IFunction)
            {
                IFunction! fun = (IFunction!)inexpr;

                if (fun.Param.Equals(var))
                    result = fun;
                else
                    result = fun.CloneWithBody(Substitute(subst, var, fun.Body));
            }
            else
            {
                assert false;
            }

            return result;
        }
        
        
        //
        // Poor man's pattern matching.
        //
        // The methods below implement pattern matching for AI expressions.
        //
        // Example Usage:
        //   Match(e, Prop.Imp,
        //            (Matcher)delegate (IExpr e) { return Match(e, Prop.And, out x, out y); }
        //            out z)
        //   which sees if 'e' matches Prop.Imp(Prop.And(x,y),z) binding x,y,z to the subtrees.
        //
        public delegate bool Matcher(IExpr! expr);
        
        private static IFunApp/*?*/ MatchFunctionSymbol(IExpr! expr, IFunctionSymbol! f)
        {
            IFunApp app = expr as IFunApp;
            if (app != null)
            {
                if (app.FunctionSymbol.Equals(f))
                    return app;
                else
                    return null;
            }
            else
                return null;
        }
        
        public static bool Match(IExpr! expr, IFunctionSymbol! f, params Matcher[]! subs)
        {
            IFunApp app = MatchFunctionSymbol(expr,f);
            if (app != null)
            {
                int i = 0; // Note ***0***
                foreach (Matcher! s in subs)
                {
                    if (!s((IExpr!)app.Arguments[i])) { return false; }
                    i++;
                }
                return true;
            }
            else { return false; }
        }
        
        // Unary Binding
        public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, params Matcher[]! subs)
        {
            arg0 = null;
        
            IFunApp app = MatchFunctionSymbol(expr,f);
            if (app != null)
            {
                arg0 = (IExpr!)app.Arguments[0];
                
                int i = 1; // Note ***1***
                foreach (Matcher! s in subs)
                {
                    if (!s((IExpr!)app.Arguments[i])) { return false; }
                    i++;
                }
                return true;
            }
            else { return false; }
        }
        
        // Binary Binding       
        public static bool Match(IExpr! expr, IFunctionSymbol! f, Matcher! sub0, out IExpr arg1, params Matcher[]! subs)
        {
            arg1 = null;
        
            IFunApp app = MatchFunctionSymbol(expr,f);
            if (app != null)
            {
                if (!sub0((IExpr!)app.Arguments[0])) { return false; }
            
                arg1 = (IExpr!)app.Arguments[1];
                
                int i = 2; // Note ***2***
                foreach (Matcher! s in subs)
                {
                    if (!s((IExpr!)app.Arguments[i])) { return false; }
                    i++;
                }
                return true;
            }
            else { return false; }
        }
        
        public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, params Matcher[]! subs)
        {
            arg0 = null;
            arg1 = null;
        
            IFunApp app = MatchFunctionSymbol(expr,f);
            if (app != null)
            {
                arg0 = (IExpr!)app.Arguments[0];
                arg1 = (IExpr!)app.Arguments[1];
                
                int i = 2; // Note ***2***
                foreach (Matcher! s in subs)
                {
                    if (!s((IExpr!)app.Arguments[i])) { return false; }
                    i++;
                }
                return true;
            }
            else { return false; }
        }

        // Ternary Binding
        public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]! subs)
        {
            arg0 = null;
            arg1 = null;
            arg2 = null;
        
            IFunApp app = MatchFunctionSymbol(expr,f);
            if (app != null)
            {
                arg0 = (IExpr!)app.Arguments[0];
                arg1 = (IExpr!)app.Arguments[1];
                arg2 = (IExpr!)app.Arguments[2];
                
                int i = 3; // Note ***3***
                foreach (Matcher! s in subs)
                {
                    if (!s((IExpr!)app.Arguments[i])) { return false; }
                    i++;
                }
                return true;
            }
            else { return false; }
        }

        /// <summary>
        ///  Not intended to be instantiated.
        /// </summary>
        private ExprUtil() { }
    }

    //------------------------------ Symbols --------------------------------

    /// <summary>
    ///  An interface for function symbols.  Constants are represented by
    ///  0-ary function symbols.
    /// 
    ///  This interface should be implemented by abstract domains, but client
    ///  expressions need keep track of function symbols.
    /// </summary>
    public interface IFunctionSymbol
    {
        AIType! AIType { [Rep][ResultNotNewlyAllocated]
                         get; }
    }

    /// <summary>
    ///  The type of the arguments to ExprUtil.Match, a poor man's pattern
    ///  matching.
    /// </summary>
    public interface IMatchable
    {
    }

    //-------------------------------- Types --------------------------------

    /// <summary>
    ///  Types.
    /// </summary>
    public interface AIType
    {
    }

    /// <summary>
    ///  Function type constructor.
    /// </summary>
    public sealed class FunctionType : AIType
    {
        /*[Own]*/ private readonly IList/*<Type!>*/! argTypes;
        /*[Own]*/ private readonly AIType! retType;

        public FunctionType(params AIType[]! types)
          requires types.Length >= 2;
        {
            AIType type = types[types.Length-1];
            assume type != null;
            this.retType = type;
            ArrayList argTypes = new ArrayList();
            for (int i = 0; i < types.Length-1; i++)
            {
                 type = types[i];
                 assume type != null;
                 argTypes.Add(types);
            }
            this.argTypes = ArrayList.ReadOnly(argTypes);
        }

        public IList/*<AIType!>*/! Arguments
        {
            [Pure][Rep]
            get 
              ensures result.IsReadOnly;
            {
                return argTypes;
            }
        }

        public int Arity
        {
            get { return argTypes.Count; }
        }

        public AIType! ReturnType
        {
            get { return retType; }
        }

        /* TODO Do we have the invariant that two functions are equal iff they're the same object.
        public override bool Equals(object o)
        {
            if (o != null && o is FunctionType)
            {
                FunctionType other = (FunctionType) o;
                
                if (Arity == other.Arity
                    && ReturnType.Equals(other.ReturnType))
                {
                    for (int i = 0; i < Arity; i++)
                    {
                        if (!argTypes[i].Equals(other.argTypes[i]))
                            return false;
                    }
                    return true;
                } 
                else
                    return false;
            }
            else
                return false;
        }
        */
    }

    //------------------------------ Queries -------------------------------

    public enum Answer { Yes, No, Maybe };
    
    /// <summary>
    ///  An interface that specifies a queryable object that can answer
    ///  whether a predicate holds.
    /// </summary>
    public interface IQueryable
    {
        /// <summary>
        ///  Answers the query whether the given predicate holds.
        /// </summary>
        /// <param name="pred">The given predicate.</param>
        /// <returns>Yes, No, or Maybe.</returns>
        Answer CheckPredicate(IExpr! pred);

        /// <summary>
        ///  A simplified interface for disequalities.  One can always
        ///  implement this by calling CheckPredicate, but it may be
        ///  more efficient with this method.
        /// </summary>
        Answer CheckVariableDisequality(IVariable! var1, IVariable! var2);
    }
    
    public static class QueryUtil
    {
        public static Answer Negate(Answer ans)
        {
            switch (ans)
            {
              case Answer.Yes:
                return Answer.No;
              case Answer.No:
                return Answer.Yes;
              default:
                return Answer.Maybe;
            }
        }
    }

    //----------------------------- Exceptions -----------------------------

    public class TypeError : CheckedException
    {
    }
}