//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using Microsoft.Contracts;
namespace Microsoft.AbstractInterpretationFramework
{
    using System.Collections;
    using System.Diagnostics;
    using System.Compiler.Analysis;
	using Microsoft.Basetypes;

    /// <summary>
    /// Represents an invariant over constant variable assignments.
    /// </summary>
    public class ConstantLattice : MicroLattice 
    {
        enum Value { Top, Bottom, Constant }

        private class Elt : Element
        {
            public Value domainValue;
            public BigNum constantValue; // valid iff domainValue == Value.Constant

            public Elt (Value v) { this.domainValue = v; }

            public Elt (BigNum i) { this.domainValue = Value.Constant; this.constantValue = i; }

            public bool IsConstant { get { return this.domainValue == Value.Constant; } }

            public BigNum Constant { get { return this.constantValue; } } // only when IsConstant

            [Pure][Reads(ReadsAttribute.Reads.Owned)]            
            public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
            {
                return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
            }
            
            public override Element! Clone()
            {
                if (this.IsConstant)
                    return new Elt(constantValue);
                else
                    return new Elt(domainValue);
            }
        }

        readonly IIntExprFactory! factory;

        public ConstantLattice(IIntExprFactory! factory)
        {
            this.factory = factory;
            // base();
        }

        public override Element! Top 
        {
            get { return new Elt(Value.Top); } 
        }

        public override Element! Bottom
        { 
            get { return new Elt(Value.Bottom); } 
        }

        public override bool IsTop (Element! element)
        { 
            Elt e = (Elt)element;
            return e.domainValue == Value.Top; 
        }

        public override bool IsBottom    (Element! element)
        {
            Elt e = (Elt)element;
            return e.domainValue == Value.Bottom; 
        }

        public override Element! NontrivialJoin (Element! first, Element! second)
        {
            Elt a = (Elt)first;
            Elt b = (Elt)second;
            Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
            return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
        }

        public override Element! NontrivialMeet (Element! first, Element! second)
        {
            Elt a = (Elt)first;
            Elt b = (Elt)second;
            Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
            return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
        }
        
        public override Element! Widen (Element! first, Element! second)
        {
            return Join(first,second);
        }

        protected override bool AtMost (Element! first, Element! second) // this <= that
        {
            Elt a = (Elt)first;
            Elt b = (Elt)second;
            return a.Constant.Equals(b.Constant);
        }

        public override IExpr! ToPredicate(IVariable! var, Element! element) {
            return factory.Eq(var, (!)GetFoldExpr(element));
        }

        public override IExpr GetFoldExpr(Element! element) {
            Elt e = (Elt)element;
            assert e.domainValue == Value.Constant;
            return factory.Const(e.constantValue);
        }

        public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
            return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
        }

        public override Element! EvaluatePredicate(IExpr! e) {
      
            IFunApp nary = e as IFunApp;
            if (nary != null) {
                if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
                    IList/*<IExpr!>*/! args = nary.Arguments;
                    assert args.Count == 2;
                    IExpr! arg0 = (IExpr!)args[0];
                    IExpr! arg1 = (IExpr!)args[1];

                    // Look for "x == const" or "const == x".
                    try {
                        if (arg0 is IVariable) {
                            BigNum z;
                            if (Fold(arg1, out z)) {
                                return new Elt(z);
                            }
                        } else if (arg1 is IVariable) {
                            BigNum z;
                            if (Fold(arg0, out z)) {
                                return new Elt(z);
                            }
                        }
                    } catch (System.ArithmeticException) {
                        // fall through and return Top.  (Note, an alternative design may
                        // consider returning Bottom.)
                    }
                }
            }
            return Top;
        }

        /// <summary>
        /// Returns true if "expr" represents a constant integer expressions, in which case
        /// "z" returns as that integer.  Otherwise, returns false, in which case "z" should
        /// not be used by the caller.
        ///
        /// This method throws an System.ArithmeticException in the event that folding the
        /// constant expression results in an arithmetic overflow or division by zero.
        /// </summary>
        private bool Fold(IExpr! expr, out BigNum z)
        {
            IFunApp e = expr as IFunApp;
            if (e == null) {
                z = BigNum.ZERO;
                return false;
            }

            if (e.FunctionSymbol is IntSymbol) {
                z = ((IntSymbol)e.FunctionSymbol).Value;
                return true;

            } else if (e.FunctionSymbol.Equals(Int.Negate)) {
                IList/*<IExpr!>*/! args = e.Arguments;
                assert args.Count == 1;
                IExpr! arg0 = (IExpr!)args[0];

                if (Fold(arg0, out z)) {
                    z = z.Neg;
                    return true;
                }

            } else if (e.Arguments.Count == 2) {
                IExpr! arg0 = (IExpr!)e.Arguments[0];
                IExpr! arg1 = (IExpr!)e.Arguments[1];
                BigNum z0, z1;
                if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
                    if (e.FunctionSymbol.Equals(Int.Add)) {
                        z = z0 + z1;
                    } else if (e.FunctionSymbol.Equals(Int.Sub)) {
                        z = z0 - z1;
                    } else if (e.FunctionSymbol.Equals(Int.Mul)) {
                        z = z0 * z1;
                    } else if (e.FunctionSymbol.Equals(Int.Div)) {
                        z = z0 / z1;
                    } else if (e.FunctionSymbol.Equals(Int.Mod)) {
                        z = z0 % z1;
                    } else {
                        z = BigNum.ZERO;
                        return false;
                    }
                    return true;
                }
            }
            
            z = BigNum.ZERO;
            return false;
        }
    }
}