OoasTools

/**

  *

  *                      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);

        }

    }

}