/**
  *
  *                      OOAS Compiler (Deprecated)
  *
  * Copyright 2015, Institute for Software Technology, Graz University of
  * Technology. Portions are copyright 2015 by the AIT Austrian Institute
  * of Technology. All rights reserved.
  *
  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
  *
  * Please notice that this version of the OOAS compiler is considered de-
  * precated. Only the Java version is maintained.
  *
  * Contributors:
  *               Willibald Krenn (TU Graz/AIT)
  *               Stefan Tiran (TU Graz/AIT)
  */

using System;
using System.Collections.Generic;
using Antlr.Runtime;

namespace TUG.Mogentes
{
    public enum ExpressionKind
    {
        /*tern.*/
        conditional,
        /*map binary*/
        domresby, domresto, rngresby, rngresto, munion,
        /*set/list binary*/
        conc, diff, inter, elemin, notelemin, subset, union,
        /*numeric binary*/
        div, greater, greaterequal, idiv, less, lessequal, minus, mod, pow, prod, sum,
        /*bool binary*/
        and, biimplies, implies, or,
        /*other binary*/
        equal, notequal, seqmod_mapoverride,
        /*map unary*/
        dom, range, merge,
        /*set/list unary*/
        card, dconc, dinter, dunion, elems, head, inds, len, tail,
        /*unary numberic*/
        unminus, unplus, not, abs,
        /*unary quantors*/
        forall, exists,
        /*Constructors*/
        ListConstr, SetConstr, MapConstr, TupleConstr, ObjectConstr, QValConstr,
        /* constant, identifier */
        Value, Identifier, UnresolvedIdentifier, Type,
        /* tuple access and method call */
        TupleMapAccess, Call,
        /* point operator */
        Access,
        /* primed */
        Primed,
        /* cast */
        Cast,
        /* fold */
        foldLR, foldRL
    }

    /*
    public enum UnaryOperatorType { unminus, unplus, not, abs }
    public enum SetListUnaryOperatorType { card, dconc, dinter, dunion, elems, head, inds, len, tail }
    public enum MapUnaryOperatorType { dom, range, merge }
    public enum BinaryOperatorType { equal, notequal, seqmod_mapoverride }
    public enum BoolBinaryOperatorType { and, biimplies, implies, or }
    public enum NumericBinaryOperatorType { div, greater, greaterequal, idiv, less, lessequal, minus, mod, pow, prod, sum }
    public enum SetListBinaryOperatorType { conc, diff, inter, elemin, notelemin, subset, union }
    public enum MapBinaryOperatorType { domresby, domresto, rngresby, rngresto, munion }
    */

    ///////////////////////////////////////////////
    ///  Expressions
    ///
    /// Note: Since we allow expression of the form
    /// myTuple(a,b) = hd x, where a and b are newly
    /// introduced placeholders, the expression knows
    /// about local variables.
    /// Scoping: Consider following expression
    ///     3 > a and myTuple(b,d) = hd e and b < 5
    /// which gives
    ///             and
    ///          /       \   
    ///         /         and
    ///        /        /     \ 
    ///       >        =        <
    ///      / \      /  \     /  \ 
    ///     3   a  (b,d)  e   b    5
    ///  the scope of b and d is defined by the binary
    ///  expression that has the leaf within its left child
    ///  (== the second 'and'). 
    ///  Local variables may only be introduced in constructors
    ///  of sets, lists, and tuples. Therefore the type is 
    ///  known.


    public abstract class Expression : UlyssesBasicClass, IAst
    {
        protected ExpressionKind m_kind;
        protected UlyssesType m_type;
        protected int m_line;
        protected int m_pos;
        protected SymbolTable m_freeVariables;
        protected List<FunctionIdentifier> m_callTargets;

        public ExpressionKind kind { get { return m_kind; } }
        public UlyssesType type { get { return m_type; } }
        public int line { get { return m_line; } }
        public int pos { get { return m_pos; } }
        public SymbolTable freeVariables { get { return m_freeVariables; } }
        public List<FunctionIdentifier> callTargets { get { return m_callTargets; } }

        public Expression(ExpressionKind aKind, int line, int pos)
        {
            m_kind = aKind;
            m_line = line;
            m_pos = pos;
            m_callTargets = new List<FunctionIdentifier>();
        }

        public Expression(Expression toCopy)
        {
            m_kind = toCopy.m_kind;
            m_line = toCopy.m_line;
            m_pos = toCopy.m_pos;
            m_callTargets = new List<FunctionIdentifier>(toCopy.callTargets);
            m_type = toCopy.m_type;
            m_freeVariables = new SymbolTable(toCopy.m_freeVariables);
        }

        public virtual Expression Clone()
        {
            throw new NotImplementedException();
        }

        public void SetType(UlyssesType aType)
        {
            if (aType == null)
                throw new ArgumentException();
            m_type = aType;
        }

        public void SetFreeVariables(SymbolTable aSymTab)
        {
            m_freeVariables = aSymTab;
        }

        public List<ExpressionVariableIdentifier> GetUninitializedFreeVariables()
        {
            List<ExpressionVariableIdentifier> result = new List<ExpressionVariableIdentifier>();
            if (m_freeVariables != null)
                foreach (var v in m_freeVariables.symbolList)
                {
                    ExpressionVariableIdentifier id = (ExpressionVariableIdentifier)v;
                    if (id.initialized == false)
                        result.Add(id);
                }
            return result;
        }


        #region IAst Member

        public AstNodeTypeEnum nodeType { get { return AstNodeTypeEnum.expression; } }

        public virtual void Accept(IAstVisitor visitor)
        {
            throw new NotImplementedException();
        }

        #endregion


        /// <summary>
        /// Calculates the arithmetic cover, i.e. the return type of the operation, given two types.
        /// This is different from the cover-method defined at the type level.
        /// Note: We do saturating operations on the type boundaries.
        /// </summary>
        public static UlyssesType ArithmeticCover(UlyssesType type1, UlyssesType type2, ExpressionKind op)
        {
            if (!type1.IsNumeric() || (type2 != null && !type2.IsNumeric()))
                throw new ArgumentException();

            if (type1 is ValuedEnumType)
                type1 = ((ValuedEnumType)type1).getIntType();
            if (type2 is ValuedEnumType)
                type2 = ((ValuedEnumType)type2).getIntType();

            AbstractRange result;
            AbstractRange rangeType1 = null;
            AbstractRange rangeType2 = null;
            AbstractOperations operations;
            bool resultIsFloat = type1.kind == TypeKind.FloatType
                                || op == ExpressionKind.div
                                || (type2 != null && type2.kind == TypeKind.FloatType);
            if (resultIsFloat)
            {
                rangeType1 = new DoubleRange(
                    type1.kind == TypeKind.IntType ? ((IntType)type1).rangeHigh : ((FloatType)type1).high,
                    type1.kind == TypeKind.IntType ? ((IntType)type1).rangeLow : ((FloatType)type1).low);
                if (type2 != null)
                {
                    rangeType2 = new DoubleRange(
                        type2.kind == TypeKind.IntType ? ((IntType)type2).rangeHigh : ((FloatType)type2).high,
                        type2.kind == TypeKind.IntType ? ((IntType)type2).rangeLow : ((FloatType)type2).low);
                }
                operations = new SaturatedDoubleOperations();
            }
            else
            {
                rangeType1 = new IntegerRange(((IntType)type1).rangeHigh, ((IntType)type1).rangeLow);
                rangeType2 = new IntegerRange(((IntType)type2).rangeHigh, ((IntType)type2).rangeLow);
                operations = new SaturatedIntegerOperations();
            }

            switch (op)
            {
                case ExpressionKind.pow:
                case ExpressionKind.prod:
                case ExpressionKind.unminus:
                case ExpressionKind.unplus:
                case ExpressionKind.minus:
                case ExpressionKind.sum:
                case ExpressionKind.div:
                    result = operations.GenericArithmeticCover(rangeType1, rangeType2, op);
                    break;

                case ExpressionKind.idiv:
                    if (resultIsFloat)
                        throw new ArgumentException();
                    System.Diagnostics.Debug.Assert(type2 != null);
                    result = operations.GenericArithmeticCover(rangeType1, rangeType2, op);
                    break;
                case ExpressionKind.mod:
                    if (resultIsFloat)
                        throw new ArgumentException();
                    System.Diagnostics.Debug.Assert(type2 != null);
                    result = new IntegerRange(((IntegerRange)rangeType2).max - 1, 0);
                    break;

                default:
                    throw new NotImplementedException();
            }

            if (resultIsFloat)
                return new FloatType(((DoubleRange)result).min, ((DoubleRange)result).max, FloatType.defaultPrecision, null);
            else
                // this is crude, but see whether it works..
                return new IntType(((IntegerRange)result).min, ((IntegerRange)result).max, null);
        }


        public override string ToString()
        {
            OoaPrintVisitor visitor = new OoaPrintVisitor(null);
            this.Accept(visitor);
            return visitor.ToString();
        }
    }


    ///////////////////////////////////////////////
    ///  === Leaf Expressions ===
    ///  
    public enum LeafTypeEnum { unset, boolean, integer, real, chr, qval, reference, identifier, type, complex }
    public abstract class LeafExpression : Expression
    {
        protected LeafTypeEnum m_valueType;

        public LeafTypeEnum valueType { get { return m_valueType; } }

        public LeafExpression(LeafTypeEnum avalueType, ExpressionKind aKind, int line, int pos)
            : base(aKind, line, pos)
        {
            m_valueType = avalueType;
        }

        public LeafExpression(LeafExpression toCopy)
            : base(toCopy)
        {
            m_valueType = toCopy.m_valueType;
        }
    }



    ///////////////////////////////////////////////
    ///  Some constant bool, int, float, char,
    ///  qval or nil value
    ///  
    public sealed class ValueExpression<T> : LeafExpression
    {
        private T m_value;

        public T value { get { return m_value; } }

        public ValueExpression(T aValue, int line, int pos)
            : base(LeafTypeEnum.unset, ExpressionKind.Value, line, pos)
        {
            m_value = aValue;
            if (typeof(T) == typeof(int))
                m_valueType = LeafTypeEnum.integer;
            else if (typeof(T) == typeof(bool))
                m_valueType = LeafTypeEnum.boolean;
            else if (typeof(T) == typeof(double))
                m_valueType = LeafTypeEnum.real;
            else if (typeof(T) == typeof(char))
                m_valueType = LeafTypeEnum.chr;
            else if (typeof(T).IsSubclassOf(typeof(QrType)))
                m_valueType = LeafTypeEnum.qval;
            else if (typeof(T).IsClass)
                m_valueType = LeafTypeEnum.reference;
            else
                throw new ArgumentException();
        }

        public ValueExpression(ValueExpression<T> toCopy)
            : base(toCopy)
        {
            m_value = toCopy.m_value;
        }

        public override Expression Clone()
        {
            return new ValueExpression<T>(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit<T>(this);
        }
    }


    ///////////////////////////////////////////////
    ///  Some identifier
    ///  
    public class IdentifierExpression : LeafExpression
    {
        protected Identifier m_identifier;
        protected bool m_self;

        public Identifier identifier { get { return m_identifier; } }
        public bool isSelf { get { return m_self; } }

        public IdentifierExpression(Identifier anIdentifier, int line, int pos)
            : base(LeafTypeEnum.identifier, ExpressionKind.Identifier, line, pos)
        {
            m_identifier = anIdentifier;
            if (anIdentifier != null)
                m_type = m_identifier.type;
            m_self = false;
        }

        public IdentifierExpression(IdentifierExpression toCopy)
            : base(toCopy)
        {
            m_identifier = toCopy.m_identifier;
            m_self = toCopy.m_self;
        }

        public override Expression Clone()
        {
            return new IdentifierExpression(this);
        }

        public void setIsSelf(bool newValue)
        {
            m_self = newValue;
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetIdentifier(Identifier newIdentifier)
        {
            m_identifier = newIdentifier;
        }
    }

    ///////////////////////////////////////////////
    ///  Some identifier
    ///  
    public class TypeExpression : LeafExpression
    {
        public TypeExpression(UlyssesType atype, int line, int pos)
            : base(LeafTypeEnum.type, ExpressionKind.Type, line, pos)
        {
            m_type = atype;
        }

        public TypeExpression(TypeExpression toCopy)
            : base(toCopy)
        { }

        public override Expression Clone()
        {
            return new TypeExpression(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }
    }

    ///////////////////////////////////////////////
    ///  Some unresolved identifier
    ///  
    public sealed class UnresolvedIdentifierExpression : IdentifierExpression
    {
        private IScope m_scope;
        private string m_tokenText;


        public string tokenText { get { return m_tokenText; } }
        public IScope scope { get { return m_scope; } }

        public UnresolvedIdentifierExpression(IToken identifier, IScope aScope)
            : base(null, identifier.Line, identifier.CharPositionInLine)
        {
            m_kind = ExpressionKind.UnresolvedIdentifier;
            m_tokenText = identifier.Text;
            m_scope = aScope;
        }

        public UnresolvedIdentifierExpression(UnresolvedIdentifierExpression toCopy)
            : base(toCopy)
        {
            m_scope = toCopy.m_scope;
            m_tokenText = toCopy.m_tokenText;
        }

        public override Expression Clone()
        {
            return new UnresolvedIdentifierExpression(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }
    }


    ///////////////////////////////////////////////
    ///  constructors
    ///  
    public abstract class TypeConstructionExpression : LeafExpression
    {
        public TypeConstructionExpression(ExpressionKind aKind, int line, int pos)
            : base(LeafTypeEnum.complex, aKind, line, pos)
        { }
        public TypeConstructionExpression(TypeConstructionExpression toCopy)
            : base(toCopy)
        { }
    }

    public sealed class ObjectConstructor : TypeConstructionExpression
    {
        private List<OoActionSystemInstance> m_instances;
        private int m_currentInstance;
        private string m_fixedObjectName;

        public int currentInstance { get { return m_currentInstance; } }
        public List<OoActionSystemInstance> instances { get { return m_instances; } }
        public string givenObjectName { get { return m_fixedObjectName; } }
        
        public void ResetCurrentInstance() { m_currentInstance = 0; }

        public ObjectConstructor(OpaqueType aType, int line, int pos)
            : base(ExpressionKind.ObjectConstr, line, pos)
        {
            SetType(aType);
            m_instances = new List<OoActionSystemInstance>();
            m_currentInstance = 0;
        }

        public ObjectConstructor(OpaqueType aType, string aName, int line, int pos)
            : base(ExpressionKind.ObjectConstr, line, pos)
        {
            SetType(aType);
            m_instances = new List<OoActionSystemInstance>();
            m_currentInstance = 0;
            m_fixedObjectName = aName;
        }


        public ObjectConstructor(ObjectConstructor toCopy)
            : base(toCopy)
        {
            m_instances = new List<OoActionSystemInstance>( toCopy.m_instances);
            m_currentInstance = toCopy.m_currentInstance;
            m_fixedObjectName = toCopy.m_fixedObjectName;
        }

        public override Expression Clone()
        {
            return new ObjectConstructor(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void AddInstance(OoActionSystemInstance anInstance)
        {
            m_instances.Add(anInstance);
        }

        public OoActionSystemInstance GetNextInstance()
        {
            OoActionSystemInstance result = m_instances[m_currentInstance];
            m_currentInstance++;
            return result;
        }
    }

    ///////////////////////////////////////////////
    ///  Constructor: List
    ///  
    public sealed class ListConstructor : TypeConstructionExpression, IScope
    {
        private List<Expression> m_elements;
        private IScope m_parentScope;
        private SymbolTable m_comprehensionVars;
        private Expression m_comprehension;
        private bool m_hasComprehension = false;

        public List<Expression> elements { get { return m_elements; } }
        public Expression comprehension { get { return m_comprehension; } }
        public bool hasComprehension { get { return m_hasComprehension; } }
        public SymbolTable comprehensionVariables { get { return m_comprehensionVars; } }

        public ListConstructor(int line, int pos)
            : base(ExpressionKind.ListConstr, line, pos)
        {
            m_elements = new List<Expression>();
            m_comprehensionVars = new SymbolTable();
        }

        public ListConstructor(ListConstructor toCopy)
            : base(toCopy)
        {
            m_elements = new List<Expression>(toCopy.m_elements);
            m_parentScope = toCopy.m_parentScope;
            m_comprehensionVars = new SymbolTable(toCopy.m_comprehensionVars);
            m_comprehension = toCopy.m_comprehension;
            m_hasComprehension = toCopy.m_hasComprehension;
        }

        public override Expression Clone()
        {
            return new ListConstructor(this);
        }

        public void AddElement(Expression anElement)
        {
            m_elements.Add(anElement);
        }

        public void SetComprehension(Expression comprehension)
        {
            m_comprehension = comprehension;
        }

        public void SetHasComprehension(bool flag)
        {
            m_hasComprehension = flag;
        }

        public Identifier ResolveIdentifier(string aName)
        {
            if (m_comprehensionVars.Defined(aName))
                return m_comprehensionVars.Get(aName);
            else
                return null;
        }

        public IScope GetParentScope()
        {
            return m_parentScope;
        }

        public void SetParentScope(IScope parentScope)
        {
            m_parentScope = parentScope;
        }

        public void AddIdentifier(Identifier anIdentifier, object tag)
        {
            m_comprehensionVars.AddIdentifier(anIdentifier);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetElements(List<Expression> newElements)
        {
            m_elements = newElements;
        }

    }

    ///////////////////////////////////////////////
    ///  Constructor: Set
    ///  
    public sealed class SetConstructor : TypeConstructionExpression, IScope
    {
        private List<Expression> m_items;
        private SymbolTable m_comprehensionVars;
        private IScope m_parentScope;
        private Expression m_comprehension;
        private bool m_hasComprehension = false;

        public List<Expression> items { get { return m_items; } }
        public Expression comprehension { get { return m_comprehension; } }
        public bool hasComprehension { get { return m_hasComprehension; } }
        public SymbolTable comprehensionVariables { get { return m_comprehensionVars; } }

        public SetConstructor(int line, int pos)
            : base(ExpressionKind.SetConstr, line, pos)
        {
            m_items = new List<Expression>();
            m_comprehensionVars = new SymbolTable();
        }

        public SetConstructor(SetConstructor toCopy)
            : base(toCopy)
        {
            m_items = new List<Expression>(toCopy.m_items);
            m_comprehensionVars = new SymbolTable(toCopy.m_comprehensionVars);
            m_parentScope = toCopy.m_parentScope;
            m_comprehension = toCopy.m_comprehension;
            m_hasComprehension = toCopy.m_hasComprehension;
        }

        public override Expression Clone()
        {
            return new SetConstructor(this);
        }

        public void AddItem(Expression anItem)
        {
            m_items.Add(anItem);
        }

        public void SetComprehension(Expression anExpr)
        {
            m_comprehension = anExpr;
        }

        public void SetHasComprehension(bool flag)
        {
            m_hasComprehension = flag;
        }

        public Identifier ResolveIdentifier(string aName)
        {
            if (m_comprehensionVars.Defined(aName))
                return m_comprehensionVars.Get(aName);
            else
                return null;
        }

        public IScope GetParentScope()
        {
            return m_parentScope;
        }

        public void SetParentScope(IScope parentScope)
        {
            m_parentScope = parentScope;
        }

        public void AddIdentifier(Identifier anIdentifier, object tag)
        {
            m_comprehensionVars.AddIdentifier(anIdentifier);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetItems(List<Expression> newItems)
        {
            m_items = newItems;
        }

    }

    ///////////////////////////////////////////////
    ///  Constructor: Map
    ///  
    public sealed class MapConstructor : TypeConstructionExpression
    {
        public sealed class MapItem
        {
            public Expression key;
            public Expression value;
            public MapItem(Expression aKey, Expression aValue)
            {
                key = aKey;
                value = aValue;
            }
            public MapItem(MapItem toCopy)
            {
                key = toCopy.key;
                value = toCopy.value;
            }
        }

        private List<MapItem> m_items;

        public List<MapItem> items { get { return m_items; } }

        public MapConstructor(int line, int pos)
            : base(ExpressionKind.MapConstr, line, pos)
        {
            m_items = new List<MapItem>();
        }

        public MapConstructor(MapConstructor toCopy)
            : base(toCopy)
        {
            m_items = new List<MapItem>(toCopy.m_items);
        }

        public override Expression Clone()
        {
            return new MapConstructor(this);
        }

        public void AddItem(Expression mapFrom, Expression mapTo)
        {
            MapItem newitem = new MapItem(mapFrom, mapTo);
            m_items.Add(newitem);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetItems(List<MapItem> newItems)
        {
            m_items = newItems;
        }

    }

    ///////////////////////////////////////////////
    ///  Constructor: Tuple
    ///  
    public sealed class TupleConstructor : TypeConstructionExpression
    {
        private List<Expression> m_values;
        private Identifier m_tupleType;
        private bool m_matcher;

        public List<Expression> values { get { return m_values; } }
        public Identifier tupleType { get { return m_tupleType; } }
        public bool isMatcher { get { return m_matcher; } }


        public TupleConstructor(Identifier aType, System.Collections.Generic.List<Expression> exprs, int line, int pos)
            : base(ExpressionKind.TupleConstr, line, pos)
        {
            m_tupleType = aType;
            m_values = new List<Expression>(exprs);
            m_matcher = false;
        }

        public TupleConstructor(TupleConstructor toCopy)
            : base(toCopy)
        {
            m_values = new List<Expression>(toCopy.m_values);
            m_tupleType = toCopy.m_tupleType;
            m_matcher = toCopy.m_matcher;
        }

        public void SetIsMatcher(bool newVal)
        {
            m_matcher = newVal;
        }

        public override Expression Clone()
        {
            return new TupleConstructor(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetTupleValues(List<Expression> values)
        {
            m_values = values;
        }
    }


    ///////////////////////////////////////////////
    ///  Constructor: Qualitative Value
    ///  
    public enum QValDeriv { DonTCare, Dec, Steady, Inc }
    public sealed class QValConstructor : TypeConstructionExpression
    {
        private Expression[] m_value;
        private QValDeriv m_derivValue;

        public Expression[] value { get { return m_value; } }
        public QValDeriv valueDeriv { get { return m_derivValue; } }


        public QValConstructor(int line, int pos) :
            base(ExpressionKind.QValConstr, line, pos)
        {
            m_value = new Expression[1];
            m_value[0] = null;
            m_derivValue = QValDeriv.DonTCare;
        }

        public QValConstructor(QValConstructor toCopy)
            : base(toCopy)
        {
            m_value = new Expression[toCopy.m_value.Length];
            Array.Copy(toCopy.m_value, m_value, m_value.Length);
            m_derivValue = toCopy.m_derivValue;
        }

        public override Expression Clone()
        {
            return new QValConstructor(this);
        }


        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetValue(Expression aval)
        {
            m_value[0] = aval;
        }

        public void AddRange(Expression toRange)
        {
            Expression currVal = m_value[0];
            m_value = new Expression[2];
            m_value[0] = currVal;
            m_value[1] = toRange;
        }

        public void SetDerivation(QValDeriv newValue)
        {
            m_derivValue = newValue;
        }
    }



    ///////////////////////////////////////////////
    ///  === Binary Operator ===
    ///  
    public class BinaryOperator : Expression
    {
        protected Expression m_left;
        protected Expression m_right;

        public Expression left { get { return m_left; } }
        public Expression right { get { return m_right; } }


        public BinaryOperator(ExpressionKind aKind, Expression left, Expression right, int line, int pos)
            : base(aKind, line, pos)
        {
            m_left = left;
            m_right = right;
        }

        public BinaryOperator(BinaryOperator toCopy)
            : base(toCopy)
        {
            m_left = toCopy.m_left;
            m_right = toCopy.m_right;
        }

        public override Expression Clone()
        {
            return new BinaryOperator(this);
        }

        public void SetRightChild(Expression child)
        {
            m_right = child;
        }

        public void SetLeftChild(Expression child)
        {
            m_left = child;
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

    }


    ///////////////////////////////////////////////
    ///  Element Access (Point operator):  a.b 
    ///  
    public sealed class AccessExpression : BinaryOperator
    {
        public AccessExpression(IdentifierExpression anIdentifier, Expression child, int line, int pos)
            : base(ExpressionKind.Access, anIdentifier, child, line, pos)
        { }

        public AccessExpression(Expression anExpression, Expression child, int line, int pos)
            : base(ExpressionKind.Access, anExpression, child, line, pos)
        { }

        public AccessExpression(AccessExpression toCopy)
            : base(toCopy)
        { }

        public override Expression Clone()
        {
            return new AccessExpression(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

    }



    ///////////////////////////////////////////////
    ///  === Ternary Operator ===
    ///  
    public sealed class TernaryOperator : Expression
    {
        private Expression m_left;
        private Expression m_mid;
        private Expression m_right;
        private IScope m_definingScope;

        public Expression left { get { return m_left; } }
        public Expression mid { get { return m_mid; } }
        public Expression right { get { return m_right; } }
        public IScope definingScope { get { return m_definingScope; } }

        public TernaryOperator(ExpressionKind aKind, Expression left, Expression mid, Expression right, int line, int pos, IScope aScope)
            : base(aKind, line, pos)
        {
            m_left = left;
            m_mid = mid;
            m_right = right;
            m_definingScope = aScope;
        }

        public TernaryOperator(TernaryOperator toCopy)
            : base(toCopy)
        {
            m_left = toCopy.m_left;
            m_mid = toCopy.m_mid;
            m_right = toCopy.m_right;
            m_definingScope = toCopy.definingScope;
        }

        public override Expression Clone()
        {
            return new TernaryOperator(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetLeftChild(Expression newExpression)
        {
            m_left = newExpression;
        }
        public void SetMidChild(Expression newExpression)
        {
            m_mid = newExpression;
        }
        public void SetRightChild(Expression newExpression)
        {
            m_right = newExpression;
        }

    }




    ///////////////////////////////////////////////
    ///  === Unary Operators ===
    ///  
    public class UnaryOperator : Expression
    {
        private Expression m_child;

        public Expression child { get { return m_child; } }

        public UnaryOperator(ExpressionKind aKind, Expression child, int line, int pos)
            : base(aKind, line, pos)
        {
            m_child = child;
        }

        public UnaryOperator(UnaryOperator toCopy)
            : base(toCopy)
        {
            m_child = toCopy.m_child;
        }

        public override Expression Clone()
        {
            return new UnaryOperator(this);
        }

        public void SetChild(Expression child)
        {
            m_child = child;
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public static Expression CoerceUp(Expression anExpr, UlyssesType target)
        {
            if (target == null)
                throw new ArgumentException();

            if (anExpr.kind == ExpressionKind.Value
                && anExpr.type.kind == target.kind)
            {
                // if we are widening the range of a type assigned to a value, then just set the
                // new type and skip constructing a new node.
                anExpr.SetType(target);
                return anExpr;
            }
            else
            {
                UnaryOperator result = new UnaryOperator(ExpressionKind.Cast, anExpr, anExpr.line, anExpr.pos);
                result.SetType(target);
                return result;
            }
        }

        public static Expression TryCoerceUp(Expression anExpr, UlyssesType target)
        {
            if (!UlyssesType.TypeEqual(anExpr.type, target))
            {
                return CoerceUp(anExpr, target);
            }
            else
                return anExpr;
        }

    }


    ///////////////////////////////////////////////
    ///  Tuple and Map Access "[...]"
    ///  
    public sealed class TupleMapAccessExpression : UnaryOperator
    {
        private Expression m_argument;

        public Expression argument { get { return m_argument; } }

        public TupleMapAccessExpression(Expression child, Expression argument, int line, int pos)
            : base(ExpressionKind.TupleMapAccess, child, line, pos)
        {
            m_argument = argument;
        }

        public TupleMapAccessExpression(TupleMapAccessExpression toCopy)
            : base(toCopy)
        {
            m_argument = toCopy.m_argument;
        }


        public override Expression Clone()
        {
            return new TupleMapAccessExpression(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetArgument(Expression newarg)
        {
            if (newarg == null)
                throw new ArgumentException();
            m_argument = newarg;
        }
    }


    ///////////////////////////////////////////////
    ///  Method call  "(....)"
    ///  
    public sealed class CallExpression : UnaryOperator
    {
        private List<Expression> m_arguments;
        private IScope m_CallScope;

        public List<Expression> arguments { get { return m_arguments; } }
        public IScope scope { get { return m_CallScope; } }

        public CallExpression(Expression child, List<Expression> arguments, int line, int pos, IScope aScope)
            : base(ExpressionKind.Call, child, line, pos)
        {
            if (arguments != null)
                m_arguments = arguments;
            else
                m_arguments = new List<Expression>();
            m_CallScope = aScope;
        }

        public CallExpression(CallExpression toCopy)
            : base(toCopy)
        {
            m_arguments = new List<Expression>(toCopy.m_arguments);
            m_CallScope = toCopy.m_CallScope;
        }

        public override Expression Clone()
        {
            return new CallExpression(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }

        public void SetArguments(List<Expression> newArgs)
        {
            m_arguments = newArgs;
        }
    }



    ///////////////////////////////////////////////
    ///  Quantifier
    ///  
    public abstract class Quantifier : UnaryOperator, IScope
    {
        private SymbolTable m_symbols;
        private IScope m_parentScope;

        public SymbolTable symbols { get { return m_symbols; } }


        public Quantifier(ExpressionKind aKind, Expression child, int line, int pos)
            : base(aKind, child, line, pos)
        {
            m_symbols = new SymbolTable();
        }

        public Quantifier(Quantifier toCopy)
            : base(toCopy)
        {
            m_symbols = new SymbolTable(toCopy.m_symbols);
            m_parentScope = toCopy.m_parentScope;
        }


        public Identifier ResolveIdentifier(string aName)
        {
            if (m_symbols.Defined(aName))
                return m_symbols.Get(aName);
            else
                return null;
        }

        public IScope GetParentScope()
        {
            return m_parentScope;
        }

        public void SetParentScope(IScope parentScope)
        {
            m_parentScope = parentScope;
        }

        public void AddIdentifier(Identifier anIdentifier, object tag)
        {
            m_symbols.AddIdentifier(anIdentifier);
        }


    }

    public sealed class ForallQuantifier : Quantifier
    {
        public ForallQuantifier(Expression child, int line, int pos)
            : base(ExpressionKind.forall, child, line, pos)
        { }

        public ForallQuantifier(ForallQuantifier toCopy)
            : base(toCopy) { }

        public override Expression Clone()
        {
            return new ForallQuantifier(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }
    }

    public sealed class ExistsQuantifier : Quantifier
    {
        public ExistsQuantifier(Expression child, int line, int pos)
            : base(ExpressionKind.exists, child, line, pos)
        { }
        public ExistsQuantifier(ExistsQuantifier toCopy)
            : base(toCopy) { }

        public override Expression Clone()
        {
            return new ExistsQuantifier(this);
        }

        public override void Accept(IAstVisitor visitor)
        {
            visitor.visit(this);
        }
    }


}