/**
  *
  *                      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 Antlr.Runtime;
using System.Text;
using System.Collections.Generic;
using System.Text.RegularExpressions;

namespace TUG.Mogentes
{

    public class CompilerMessage
    {
        private string m_file;
        private int m_line;
        private int m_column;
        private string m_message;

        public CompilerMessage(string aFile, int aLine, int aColumn, string aMessage)
        {
            m_file = aFile;
            m_line = aLine;
            m_column = aColumn;
            m_message = aMessage;
        }

        public CompilerMessage(string aFile, IToken aSymbol, string aMessage)
        {
            m_file = aFile;
            m_line = aSymbol.Line;
            m_column = aSymbol.CharPositionInLine;
            m_message = aMessage;
        }

        public string file { get { return m_file; } }
        public int line { get { return m_line; } }
        public int column { get { return m_column; } }
        public string message { get { return m_message; } }

    }


    public class ParserError : CompilerMessage
    {
        public ParserError(string aFile, int aLine, int aColumn, string aMessage)
            : base(aFile, aLine, aColumn, aMessage)
        { }

        public ParserError(string aFile, IToken aSymbol, string aMessage)
            : base(aFile, aSymbol, aMessage)
        { }
    }


    public class ParserWarning : CompilerMessage
    {
        public ParserWarning(string aFile, int aLine, int aColumn, string aMessage)
            : base(aFile, aLine, aColumn, aMessage)
        { }

        public ParserWarning(string aFile, IToken aSymbol, string aMessage)
            : base(aFile, aSymbol, aMessage)
        { }
    }

    public class ParserMessage : CompilerMessage
    {
        public ParserMessage(string aFile, int aLine, int aColumn, string aMessage)
            : base(aFile, aLine, aColumn, aMessage)
        { }

        public ParserMessage(string aFile, IToken aSymbol, string aMessage)
            : base(aFile, aSymbol, aMessage)
        { }
    }


    public class ParserState
    {
        public ooaParser parser;
        public ooaLexer lexer;
        public string filename;
        public string namesTypePrefix = String.Empty;
        public bool parsingAttributes;


        public MainModule ooaSystem;

        public IScope currentScope;
        public List<ParserError> listOfParserErrors;
        public List<ParserWarning> listOfParserWarnings;
        public List<ParserMessage> listOfParserMessages;
        public List<OpaqueType> typesToFixUp;

        public ParserState(Program.Options options)
        {
            listOfParserErrors = new List<ParserError>();
            listOfParserWarnings = new List<ParserWarning>();
            listOfParserMessages = new List<ParserMessage>();
            typesToFixUp = new List<OpaqueType>();
            this.filename = options.fileToParse;
            this.namesTypePrefix = options.namedTypePrefix;
            ICharStream input = new ANTLRFileStream(filename, Encoding.ASCII);
            lexer = new ooaLexer(input);
            CommonTokenStream tokens = new CommonTokenStream(lexer);
            parser = new ooaParser(tokens);
            parser.pState = this;
        }

        public void AddErrorMessage(ParserError parserError)
        {
            listOfParserErrors.Add(parserError);
        }
        public void AddWarningMessage(ParserWarning parserWarning)
        {
            listOfParserWarnings.Add(parserWarning);
        }
        public void AddMessage(ParserMessage aMessage)
        {
            listOfParserMessages.Add(aMessage);
        }

        public Identifier Lookup(string symbolName, IScope resolveStack)
        {
            string lkupname = symbolName;
            do
            {
                Identifier result = resolveStack.ResolveIdentifier(lkupname);
                if (result != null)
                    return result;
                resolveStack = resolveStack.GetParentScope();
            } while (resolveStack != null);

            return null;
        }
        public Identifier Lookup(string symbolName)
        {
            return Lookup(symbolName, currentScope);
        }
        public Identifier Lookup(IToken symbolName)
        {
            if (symbolName != null)
                return Lookup(symbolName.Text);
            else
                return null;
        }

        public void PushResolveStack(IScope newScope)
        {
            // some sanity check.
            if (newScope is MethodIdentifier)
                System.Diagnostics.Debug.Assert(currentScope is OoActionSystemType);

            newScope.SetParentScope(currentScope);
            currentScope = newScope;
        }
        public void PopResolveStack()
        {
            currentScope = currentScope.GetParentScope();
        }
    }


    public partial class ooaParser : Parser
    {
        public ParserState pState { get; set; }




        public bool IsRightToLeft(ExpressionKind type)
        {
            return type == ExpressionKind.implies; // implication has right grouping
        }

        public int GetOperatorPrecedence(ExpressionKind type)
        {
            switch (type)
            {
                /*Family of Evaluators*/

                case ExpressionKind.abs:    // T_ABS:
                case ExpressionKind.card:   // T_CARD:
                case ExpressionKind.dom:    // T_DOM:
                case ExpressionKind.range:  // T_RNG:
                case ExpressionKind.merge:  // T_MERGE:
                case ExpressionKind.len:    // T_LEN:
                case ExpressionKind.elems:  // T_ELEMS:
                case ExpressionKind.head:   // T_HEAD:
                case ExpressionKind.tail:   // T_TAIL:
                case ExpressionKind.conc:   // T_CONC:
                case ExpressionKind.inds:   // T_INDS:
                case ExpressionKind.dinter: // T_DINTER:
                case ExpressionKind.dunion: // T_DUNION:
                    return 1;

                case ExpressionKind.domresby:   // T_DOMRESBY:
                case ExpressionKind.domresto:   // T_DOMRESTO:
                case ExpressionKind.rngresby:   // T_RNGRESBY:
                case ExpressionKind.rngresto:   // T_RNGRESTO:
                    return 2;

                case ExpressionKind.div:    // T_DIV:
                case ExpressionKind.idiv:   // T_IDIV:
                case ExpressionKind.mod:    // T_MOD:
                case ExpressionKind.prod:   // T_PROD:
                case ExpressionKind.inter:  // T_INTER:
                    return 3;

                case ExpressionKind.sum:    // T_SUM:
                case ExpressionKind.minus:  // T_MINUS:
                case ExpressionKind.union:  // T_UNION:
                case ExpressionKind.diff:   // T_DIFF:
                case ExpressionKind.munion: // T_MUNION:
                case ExpressionKind.seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:
                    return 4;

                /*Family of Relations*/

                case ExpressionKind.less:
                case ExpressionKind.lessequal:
                case ExpressionKind.greater:
                case ExpressionKind.greaterequal:
                case ExpressionKind.equal:
                case ExpressionKind.notequal:
                case ExpressionKind.subset:
                case ExpressionKind.elemin:
                case ExpressionKind.notelemin:
                    return 5;

                /*Family of Connectives*/

                case ExpressionKind.and:    // T_AND:
                    return 6;

                case ExpressionKind.or:     // T_OR:
                    return 7;

                case ExpressionKind.implies:    // T_IMPLIES:
                    return 8;

                case ExpressionKind.biimplies:  // T_BIIMPLIES:
                    return 9;

                default:
                    throw new NotImplementedException("operator not supported: " + type.ToString());
                // return 0;
            }
        }

        /*taken from antlr homepage:
         http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser
         */
        int findPivot(List<BinaryOperator> operators, int startIndex, int stopIndex)
        {
            int pivot = startIndex;
            int pivotRank = GetOperatorPrecedence(operators[pivot].kind);
            for (int i = startIndex + 1; i <= stopIndex; i++)
            {
                ExpressionKind type = operators[i].kind;
                int current = GetOperatorPrecedence(type);
                bool rtl = IsRightToLeft(type);
                if (current > pivotRank || (current == pivotRank && rtl))
                {
                    pivot = i;
                    pivotRank = current;
                }
            }
            return pivot;
        }

        internal Expression createPrecedenceTree(
            List<Expression> expressions,
            List<BinaryOperator> operators,
            int startIndex,
            int stopIndex)
        {
            if (stopIndex == startIndex)
                return expressions[startIndex];

            int pivot = findPivot(operators, startIndex, stopIndex - 1);

            BinaryOperator result = operators[pivot];
            result.SetLeftChild(createPrecedenceTree(expressions, operators, startIndex, pivot));
            result.SetRightChild(createPrecedenceTree(expressions, operators, pivot + 1, stopIndex));

            return result;
        }

        internal Expression createPrecedenceTree(List<Expression> expressions, List<BinaryOperator> operators)
        {
            return createPrecedenceTree(expressions, operators, 0, expressions.Count - 1);
        }


        /* add error message to state. */
        private void doError(IToken aToken, string aMessage)
        {
            pState.AddErrorMessage(
                new ParserError(pState.filename, aToken, aMessage));
        }

        /* add warning message to state */
        private void doWarning(IToken id1, string p)
        {
            pState.AddWarningMessage(new ParserWarning(pState.filename, id1, p));
        }

        private void doError(string aMessage)
        {
            pState.AddErrorMessage(
                new ParserError(pState.filename, 0, 0, aMessage));
        }

        /* init global state */
        internal void initializeTopLevelParserState()
        {
            pState.ooaSystem = new MainModule();
            pState.PushResolveStack(pState.ooaSystem);
        }


        private IScope GetScope()
        {
            return pState.currentScope;
        }


        /*create a named constant*/
        internal void addNamedConst(IToken aName, Expression anExpr)
        {
            if (pState.currentScope.ResolveIdentifier(aName.Text) == null)
            {
                /* needs to be a constant... */
                ConstantIdentifier aConst = new ConstantIdentifier(aName, anExpr, GetScope());

                OoaResolveExpressionsVisitor resolver = new OoaResolveExpressionsVisitor(pState);
                aConst.Accept(resolver);

                if (aConst.Value == null || aConst.Value.type == null || aConst.Value.kind != ExpressionKind.Value)
                {
                    doError(aName, String.Format("{0} not a constant!", aName.Text));
                }
                else
                {
                    aConst.SetType(aConst.Value.type);
                    pState.currentScope.AddIdentifier(aConst, null);
                }
            }
            else
                doError(aName, String.Format("{0} already defined!", aName.Text));
        }



        /* create a named type; we're on top-level here */
        internal void createNamedType(IToken aName, UlyssesType aType)
        {
            // precond..
            System.Diagnostics.Debug.Assert(aName != null);

            if (aType == null)
            {
                doError(aName, String.Format("{0} lacks a type! (Type not added)", aName.Text));
                return;
            }


            if (pState.currentScope.ResolveIdentifier(aName.Text) == null)
            {
                TypeIdentifier newid = new TypeIdentifier(aName, aType, GetScope());
                aType.SetTypeIdentifier(newid);
                pState.currentScope.AddIdentifier(newid, null);
            }
            else
                doError(aName, String.Format("{0} already defined!", aName.Text));

        }

        /* create basic structure for an ooa-system descr. resolve stack TOS is now ooa-system symbols */
        internal OoActionSystemType createOoaType(IToken refinesSystemName, bool autoCons)
        {
            Identifier refinedSystem = pState.Lookup(refinesSystemName);
            OoActionSystemType refinedSystemType = null;
            if ((refinedSystem != null) && (refinedSystem.type != null))
            {
                if (refinedSystem.type.kind != TypeKind.OoActionSystemType)
                    doError(refinesSystemName,
                            String.Format("{0} not an object oriented action system", refinesSystemName.Text));
                else
                    refinedSystemType = (OoActionSystemType)refinedSystem.type;
            }
            else if (refinesSystemName != null)
            {
                pState.AddErrorMessage(
                    new ParserError(pState.filename, refinesSystemName,
                        String.Format("Type that's being refined ({0}) not found!", refinesSystemName.Text)));
            }

            OoActionSystemType result = new OoActionSystemType(autoCons, refinedSystemType, null);


            // add 'self' to the symbols.. (self is a keyword, so it can't be defined)
            result.AddIdentifier(new SelfTypeIdentifier("self", result, GetScope()), null);



            pState.PushResolveStack(result);
            return result;
        }

        /* remove ooa-system symbols from resolve stack TOS */
        internal void fixupOoaType(OoActionSystemType aTypeSymbol)
        {
            if (aTypeSymbol == null)
                return;

            aTypeSymbol.SetupAnonymousName();
            if (aTypeSymbol != null)
                pState.PopResolveStack();
        }

        internal Expression addCastExpression(Expression e, IToken cid)
        {
            System.Diagnostics.Debug.Assert(e != null);

            Expression result = new UnaryOperator(ExpressionKind.Cast, e, cid.Line, cid.CharPositionInLine);
            result.SetType(new OpaqueType(new TypeIdentifier(cid, null, GetScope())));
            pState.typesToFixUp.Add((OpaqueType)result.type);
            return result;
        }


        /* add a new ooa to the list describing the composition of action systems */
        internal void addToIdentifierList(IdentifierList top, IToken aName)
        {
            System.Diagnostics.Debug.Assert(top != null);

            Identifier aSym = pState.Lookup(aName);
            if (aSym == null)
            {
                doError(aName, String.Format("Could not find ooa-system {0}!", aName.Text));
            }
            else if ((aSym.type == null) || !(aSym.type.kind == TypeKind.OoActionSystemType))
            {
                doError(aName, String.Format("Referenced type ({0}) does not have correct type!", aName.Text));
            }
            else
            {
                OoActionSystemType aType = (OoActionSystemType)aSym.type;
                if (aType.isInSystemDescription)
                    doError(aName, String.Format("Referenced type ({0}) already used in composition!", aName.Text));
                else
                    aType.SetIsInSystemDescription(true);
                top.AddElement(aSym);
            }
        }

        /* does a fixup run after parsing */
        internal void fixUpRun(IdentifierList sysDescr)
        {
            // set system descr.
            pState.ooaSystem.SetSystemDescription(sysDescr);

            // fixup named types
            FixupNamedTypes();
        }

        private void FixupNamedTypes()
        {
            /*named type refs that could not be resolved in the first run, have to
              be resolved now. */
            foreach (var ntype in pState.typesToFixUp)
            {
                if (ntype.resolvedType == null)
                {
                    //ntype.identifier
                    Identifier asym = pState.Lookup(ntype.identifier.tokenText, ntype.identifier.definingScope);
                    if ((asym == null) || (asym.kind != IdentifierKind.TypeIdentifier))
                    {
                        ParserError error = new ParserError(pState.filename, ntype.identifier.line, ntype.identifier.column,
                            String.Format("Can not resolve {0} to a named type", ntype.identifier.tokenText));
                        pState.AddErrorMessage(error);
                    }
                    else
                        ntype.SetResolvedType(asym.type);
                }
            }
            pState.typesToFixUp.Clear();
        }


        private bool TosIsActionSystem()
        {
            return pState.currentScope is OoActionSystemType;
        }


        private int currentLine
        {
            get
            {
                IToken token = input.LT(-1);
                return token == null ? 0 : token.Line;
            }
        }

        private int currentPos
        {
            get
            {
                IToken token = input.LT(-1);
                return token == null ? 0 : token.CharPositionInLine;
            }
        }

        /* add var symbol to the current action system */
        internal void createAttribute(IToken varname, bool isStatic, bool isObs, bool isCtr, UlyssesType aType, Expression anExpr)
        {
            if (!TosIsActionSystem())
                return;

            if (aType == null)
            {
                doError(varname, String.Format("{0} lacks type!", varname.Text));
            }
            if (anExpr == null)
            {
                doError(varname, String.Format("{0} lacks initializer!", varname.Text));
            }
            if (isObs == true || isCtr == true)
                if (aType.kind != TypeKind.QrType)
                    doError(varname, "'obs' or 'ctr' on attributes only allowed for qualitative types");


            AttributeIdentifier var = new AttributeIdentifier(varname, aType, GetScope(), anExpr, isStatic, isObs, isCtr);
            if (pState.currentScope.ResolveIdentifier(varname.Text) == null)
                pState.currentScope.AddIdentifier(var, null);
            else
                doError(varname, String.Format("Can not add {0}: Symbol already defined!", varname.Text));
        }


        /* create a bool type */
        internal BoolType createBoolType()
        {
            return new BoolType(null);
        }

        /* create a char type */
        internal CharType createCharType()
        {
            return new CharType(null);
        }

        /* create an int type */
        internal UlyssesType createIntType(IToken rangeLow, IToken rangeHigh)
        {
            int low = 0;
            int high = 0;

            if (rangeLow.Type == ooaLexer.T_INFTY)
                doError(rangeLow, "Infinity not supported.");
            if (rangeLow.Type == ooaLexer.T_INFTY)
                doError(rangeHigh, "Infinity not supported.");

            if (rangeLow.Type == ooaLexer.T_IDENTIFIER)
            {
                // see whether we can find the constant
                Identifier aconst = pState.currentScope.ResolveIdentifier(rangeLow.Text);
                if (aconst == null || aconst.kind != IdentifierKind.Constant)
                    doError(rangeLow, String.Format("Constant {0} not found", rangeLow.Text));
                else if (aconst.type.kind != TypeKind.IntType)
                    doError(rangeLow, "Constant must be integer");
                else
                    low = ((ValueExpression<int>)((ConstantIdentifier)aconst).Value).value;
            }
            else
                if (!Int32.TryParse(rangeLow.Text, out low))
                    doError(rangeLow, "Can not convert to integer");

            if (rangeHigh.Type == ooaLexer.T_IDENTIFIER)
            {
                // see whether we can find the constant
                Identifier aconst = pState.currentScope.ResolveIdentifier(rangeHigh.Text);
                if (aconst == null || aconst.kind != IdentifierKind.Constant)
                    doError(rangeHigh, String.Format("Constant {0} not found", rangeHigh.Text));
                else if (aconst.type.kind != TypeKind.IntType)
                    doError(rangeHigh, "Constant must be integer");
                else
                    high = ((ValueExpression<int>)((ConstantIdentifier)aconst).Value).value;
            }
            else
                if (!Int32.TryParse(rangeHigh.Text, out high))
                    doError(rangeHigh, "Can not convert to interger");

            if (high < low)
                doError(rangeHigh, "Lower bound greater than upper bound");

            return new IntType(low, high, null);
        }

        /* create a float type */
        internal UlyssesType createFloatType(IToken rangeLow, IToken rangeHigh)
        {
            float low = 0;
            float high = 0;

            if (rangeLow.Type == ooaLexer.T_INFTY)
                doError(rangeLow, "Infinity not supported.");
            if (rangeLow.Type == ooaLexer.T_INFTY)
                doError(rangeHigh, "Infinity not supported.");

            if (rangeLow.Type == ooaLexer.T_IDENTIFIER)
            {
                // see whether we can find the constant
                Identifier aconst = pState.currentScope.ResolveIdentifier(rangeLow.Text);
                if (aconst == null || aconst.kind != IdentifierKind.Constant)
                    doError(rangeLow, String.Format("Constant {0} not found", rangeLow.Text));
                else if (aconst.type.kind != TypeKind.FloatType)
                    doError(rangeLow, "Constant must be float");
                else
                    low = ((ValueExpression<int>)((ConstantIdentifier)aconst).Value).value;
            }
            else if (!float.TryParse(rangeLow.Text, out low))
                doError(rangeLow, "Can not convert to float (single)");

            if (rangeHigh.Type == ooaLexer.T_IDENTIFIER)
            {
                // see whether we can find the constant
                Identifier aconst = pState.currentScope.ResolveIdentifier(rangeHigh.Text);
                if (aconst == null || aconst.kind != IdentifierKind.Constant)
                    doError(rangeHigh, String.Format("Constant {0} not found", rangeHigh.Text));
                else if (aconst.type.kind != TypeKind.FloatType)
                    doError(rangeHigh, "Constant must be integer");
                else
                    high = ((ValueExpression<int>)((ConstantIdentifier)aconst).Value).value;
            }
            else if (!float.TryParse(rangeHigh.Text, out high))
                doError(rangeHigh, "Can not convert to float (single)");

            if (high < low)
                doError(rangeHigh, "Lower bound greater than upper bound");

            /* precision */
            float afterc_low = low - (float)Convert.ToInt32(low);
            float afterc_high = high - (float)Convert.ToInt32(high);
            float precision = afterc_low < afterc_high ? afterc_low : afterc_high;

            return new FloatType(low, high, precision, null);
        }

        /* create a list of an enumerated type */
        internal UlyssesType createListEnumType(IToken alistelem)
        {
            EnumType hiddenEnumType = new EnumType(null);

            ListType result = new ListType(hiddenEnumType, 500, null);
            addToListEnumType(result, alistelem);
            return result;
        }

        /* add a new enum symbol to a list with an anonymous enumerated type */
        internal void addToListEnumType(UlyssesType aTypeSymbol, IToken otherlistelem)
        {
            EnumType enumtype = (EnumType)((ListType)aTypeSymbol).innerType;
            addToEnumType(enumtype, otherlistelem, null);
        }

        /* create a new enumerated type */
        internal UlyssesType createEnumType(IToken aRangeValue, IToken anIntegerValue)
        {
            EnumType result;

            if (anIntegerValue == null)
                result = new EnumType(null);
            else
                result = new ValuedEnumType(null);

            addToEnumType(result, aRangeValue, anIntegerValue);
            return result;
        }

        /* add a new enum symbol to the enumerated type */
        internal void addToEnumType(UlyssesType aTypeSymbol, IToken otherRangeValue, IToken anIntegerValue)
        {
            EnumType anEnum = (EnumType)aTypeSymbol;
            if (anEnum.symbolTable.Defined(otherRangeValue.Text))
            {
                doError(otherRangeValue, String.Format("Element '{0}' already defined!", otherRangeValue.Text));
                return;
            }

            /* for now we allow the usage of enum-ids without specifying the actual enum type,
             * e.g., x = some_enum_id, hence all enum identifier must be globally unique.
             * This decision could be reverted at later time...
             */
            Identifier sym = pState.Lookup(otherRangeValue);
            if (sym != null)
            {
                doError(otherRangeValue, String.Format("Element '{0}' already defined!", otherRangeValue.Text));
                return;
            }

            EnumIdentifier enumval;
            if (anIntegerValue == null)
            {
                if (aTypeSymbol is ValuedEnumType)
                {
                    doError(otherRangeValue, String.Format("Element '{0}' needs integer value!", otherRangeValue.Text));
                    return;
                }

                enumval = new EnumIdentifier(otherRangeValue, (EnumType)aTypeSymbol, GetScope());
            }
            else
            {
                if (!(aTypeSymbol is ValuedEnumType))
                {
                    doError(otherRangeValue, String.Format("Element '{0}' must not have integer value!", otherRangeValue.Text));
                    return;
                }
                enumval = new EnumIdentifier(otherRangeValue, Int32.Parse(anIntegerValue.Text), (EnumType)aTypeSymbol, GetScope());
            }

            ((EnumType)aTypeSymbol).AddEnumSymbol(enumval);

            /* add the enum id to 'global' state */
            pState.currentScope.AddIdentifier(enumval, null);
        }

        /* get a named type */
        internal UlyssesType getNamedType(IToken aType)
        {
            UlyssesType result = null;
            Identifier sym = pState.Lookup(aType);
            if (sym == null)
            {
                /* we might not have seen this type yet - so do a fixup run later */
                result = new OpaqueType(new TypeIdentifier(aType, null, GetScope()));
                pState.typesToFixUp.Add((OpaqueType)result);
            }
            else if (sym.kind == IdentifierKind.TypeIdentifier)
                result = ((TypeIdentifier)sym).type;
            else
                doError(aType, "Not a named type symbol!");

            return result;
        }

        /* create a list type */
        internal UlyssesType createListType(IToken numOfElements, UlyssesType innertype)
        {
            if (innertype == null)
                doError(numOfElements, "List type lacks proper element type (null)");

            int numElems = 0;

            if (numOfElements.Type == ooaLexer.T_IDENTIFIER)
            {
                // see whether we can find the constant
                Identifier aconst = pState.currentScope.ResolveIdentifier(numOfElements.Text);
                if (aconst == null || aconst.kind != IdentifierKind.Constant)
                    doError(numOfElements, String.Format("Constant {0} not found", numOfElements.Text));
                else if (aconst.type.kind != TypeKind.IntType)
                    doError(numOfElements, "Constant must be integer");
                else
                    numElems = ((ValueExpression<int>)((ConstantIdentifier)aconst).Value).value;
            }
            else
            {
                if (!Int32.TryParse(numOfElements.Text, out numElems))
                    doError(numOfElements, "Not an integer");
                if (numElems <= 0)
                    doError(numOfElements, "Number of elements in a list must be >= 1");
            }

            ListType result = new ListType(innertype, numElems, null);
            return result;
        }

        /* create a map type */
        internal UlyssesType createMapType(IToken numOfElements, UlyssesType mapfromtype, UlyssesType maptotype)
        {
            if (mapfromtype == null)
                doError(numOfElements, "Map: From-type not set (null)");
            if (maptotype == null)
                doError(numOfElements, "Map: To-type not set (null)");

            int max = 0;

            if (numOfElements.Type == ooaLexer.T_IDENTIFIER)
            {
                // see whether we can find the constant
                Identifier aconst = pState.currentScope.ResolveIdentifier(numOfElements.Text);
                if (aconst == null || aconst.kind != IdentifierKind.Constant)
                    doError(numOfElements, String.Format("Constant {0} not found", numOfElements.Text));
                else if (aconst.type.kind != TypeKind.IntType)
                    doError(numOfElements, "Constant must be integer");
                else
                    max = ((ValueExpression<int>)((ConstantIdentifier)aconst).Value).value;
            }
            else
                if (!Int32.TryParse(numOfElements.Text, out max))
                    doError(numOfElements, "Not an integer");

            MapType result = new MapType(mapfromtype, maptotype, max, null);
            return result;
        }

        /* create a tuple type */
        internal UlyssesType createTupleType(UlyssesType aType)
        {
            TupleType result = new TupleType(null);
            if (aType == null)
                doError("Unknown inner type.");
            else
                addToTupleType(result, aType);
            return result;
        }

        /* add inner type to tuple */
        internal void addToTupleType(UlyssesType aTypeSymbol, UlyssesType anotherType)
        {
            if (anotherType == null)
                doError("Unknown inner type.");
            else
            {
                TupleType tuple = (TupleType)aTypeSymbol;
                tuple.AddType(anotherType);
            }
        }

        /* create a QR type */
        internal UlyssesType createQrType(IToken alandmark)
        {
            QrType result = new QrType(null);
            addToQrType(result, alandmark);
            return result;
        }

        /* add another landmark to QR type */
        private void addToQrType(UlyssesType aTypeSymbol, IToken otherlandmark)
        {
            Identifier sym = pState.Lookup(otherlandmark);
            if (sym != null)
            {
                doError(otherlandmark, String.Format("Redifinition of {0}", otherlandmark.Text));
                return;
            }

            LandmarkIdentifier lndmrk = new LandmarkIdentifier(otherlandmark, (QrType)aTypeSymbol, GetScope());
            ((QrType)aTypeSymbol).AddLandmark(lndmrk);
        }

        /* gets called after a simple type has been constructed. used to define an internal name*/
        internal void fixupSimpleType(UlyssesType aTypeSymbol)
        {
            if (aTypeSymbol != null)
                aTypeSymbol.SetupAnonymousName();
        }

        /* gets called after a simple or complex type has been constructed. used to define an internal name */
        internal void fixupComplexType(UlyssesType aTypeSymbol)
        {
            if (aTypeSymbol != null)
                aTypeSymbol.SetupAnonymousName();
        }


        /* create a method symbol */
        internal FunctionIdentifier createMethodSymbol(IToken mname)
        {
            Identifier sym = pState.Lookup(mname);
            if (sym != null)
            {
                doError(mname, String.Format("Redefinition of {0}", mname.Text));
                return null;
            }

            FunctionType funtype = new FunctionType(FunctionTypeEnum.Method, new LinkedList<UlyssesType>(), null);
            MethodIdentifier msym = new MethodIdentifier(mname, funtype, GetScope());
            funtype.SetTypeIdentifier(msym);

            pState.currentScope.AddIdentifier(msym, null);

            pState.PushResolveStack(msym);
            return msym;
        }

        /* remove local method symbols from resolution stack again */
        private void popResolveStack(FunctionIdentifier newMethod)
        {
            if (newMethod != null)
                pState.PopResolveStack();
        }


        /* add a return type to a method */
        internal void setMethodReturnType(FunctionIdentifier newMethod, UlyssesType rt)
        {
            if (newMethod == null)
                return;

            if (rt == null)
                doError(String.Format("Method {0} has no return type (null)", newMethod.tokenText));

            /* set return type */
            ((FunctionType)newMethod.type).SetReturnType(rt);


            /* add hidden return parameter */
            if (newMethod.symbolTable.Defined("result"))
            {
                doError(String.Format("Method {0} defines 'result'", newMethod.tokenText));
                return;
            }

            ParameterIdentifier returnval = new ParameterIdentifier("result", rt, GetScope());
            newMethod.symbolTable.AddIdentifier(returnval);
        }

        /* add a parameter to a method */
        internal void addMethodParameter(FunctionIdentifier newMethod, IToken paramName, UlyssesType atype)
        {
            if (newMethod == null)
                return;

            if (atype == null)
                doError(paramName, "Parameter has no type (null)");


            if (newMethod.symbolTable.Defined(paramName.Text) == true)
            {
                doError(paramName, String.Format("Parameter {0} already defined", paramName.Text));
                return;
            }

            // add parameter to scope
            ParameterIdentifier param = new ParameterIdentifier(paramName, atype, GetScope());
            newMethod.AddParameter(param);

            // add type of param to signature
            FunctionType ftype = (FunctionType)newMethod.type;
            ftype.AddParameterType(atype);
        }

        /* set method body of a method */
        internal void addMethodBody(FunctionIdentifier newMethod, Block statements)
        {
            if (newMethod == null)
                return;

            if (statements == null)
                doError(String.Format("{0} has empty body (null)",
                    ((FunctionType)newMethod.type).functionType == FunctionTypeEnum.Method ? "Method" : "Action"));

            newMethod.SetBody(statements);
        }

        /* create a continuous action */
        internal FunctionIdentifier createNamedContinuousAction(IToken cactionname, FunctionTypeEnum actionTypeEnum)
        {
            return createNamedAction(cactionname, actionTypeEnum);
        }

        /* create a named action */
        internal FunctionIdentifier createNamedAction(IToken actionname, FunctionTypeEnum actionType)
        {
            Identifier sym = pState.Lookup(actionname);
            if (sym != null)
            {
                doError(actionname, "Symbol already defined.");
                return null;
            }

            FunctionType atype = new FunctionType(actionType, new LinkedList<UlyssesType>(), null);
            NamedActionIdentifier action = new NamedActionIdentifier(actionname, atype, GetScope());
            atype.SetTypeIdentifier(action);

            pState.currentScope.AddIdentifier(action, null);
            pState.PushResolveStack(action);
            return action;
        }

        /* add body of action */
        internal void addActionBody(FunctionIdentifier newAction, GuardedCommand body)
        {
            // we need a wrapper around the guarded command..
            Block bdy = new SeqBlock(currentLine, currentPos);
            bdy.AddStatement(body);
            addMethodBody(newAction, bdy);
        }

        /* add constraints of cont. action */
        internal void addContinuousActionBody(FunctionIdentifier newAction, GuardedCommand constraints)
        {
            Block bdy = new SeqBlock(currentLine, currentPos);
            bdy.AddStatement(constraints);
            addMethodBody(newAction, bdy);
        }

        /* create a guarded command */
        internal GuardedCommand createGuardedCommandStatement(Expression expr, Block bdy)
        {
            if (bdy == null)
                doError("Guarded command without body (null)!");

            if (expr == null)
                doError("Guarded command without guard (null)!");

            GuardedCommand result = new GuardedCommand(expr, bdy, currentLine, currentPos);
            return result;
        }
        internal GuardedCommand createGuardedCommandStatement(Expression expr, Block bdy, bool isQualitative)
        {
            GuardedCommand result = createGuardedCommandStatement(expr, bdy);
            result.SetIsQualitative(isQualitative);
            return result;
        }

        /* add statements to list */
        internal void addToStatementList(Block top, Statement stmt)
        {
            if (stmt == null)
                doError("Can not add statement: null!");

            top.AddStatement(stmt);
        }

        /* create a Kill statement */
        internal Statement createKillStatement(IToken aname)
        {
            Identifier sym = pState.Lookup(aname);
            if (sym == null)
                doError(aname, "Not defined");

            KillStatement result = new KillStatement(sym, aname.Line, aname.CharPositionInLine);
            return result;
        }

        /* create a Skip statement */
        internal Statement createSkipStatement()
        {
            return new SkipStatement(currentLine, currentPos);
        }

        /* create an Abort statement */
        internal Statement createAbortStatement()
        {
            return new AbortStatement(currentLine, currentPos);
        }

        /* creates a prioritized composition block */
        internal Block createPrioBlock(Block top)
        {
            return new PrioBlock(top, currentLine, currentPos);
        }

        /* creates a nondeterministically composed block */
        internal Block createNondetBlock(Block top)
        {
            return new NondetBlock(top, currentLine, currentPos);
        }

        /* creates a sequentially composed block */
        internal Block createSeqBlock(Block top)
        {
            return new SeqBlock(top, currentLine, currentPos);
        }


        /* adds a filter expression to seq block */
        private void addSeqBlockExpression(Block seqList, Expression sexpr)
        {
            seqList.SetFilter(sexpr); /*gets transformed to guarded command in resolvevisitor!*/
        }


        /* create a self identifier */
        internal IdentifierExpression createSelfIdentifierExpression(IToken self)
        {
            Identifier id = pState.Lookup("self");
            if (id == null)
            {
                doError(self, "Can not resolve 'self'");
                return null;
            }

            IdentifierExpression result = new IdentifierExpression(id, self.Line, self.CharPositionInLine);
            result.setIsSelf(true);
            return result;
        }

        /* build up identifier tree... */
        internal Expression createIdentifierAccessExpression(IdentifierExpression aself, IToken token)
        {
            Identifier someid = pState.Lookup(token.Text, GetScope());
            Identifier self = pState.Lookup("self");

            if (someid != null)
            {
                switch (someid.kind)
                {
                    /* all method and attribute accesses are prefixed by self */
                    case IdentifierKind.AttributeIdentifier:
                    case IdentifierKind.MethodIdentifier:
                        if (self == null)
                            doError(token, "Self access of method: Can not find 'self' symbol! (internal error)");
                        aself = new IdentifierExpression(self, token.Line, token.CharPositionInLine);
                        aself.setIsSelf(true);
                        break;
                    default:
                        break;
                }
            }

            IdentifierExpression ident = new UnresolvedIdentifierExpression(token, GetScope());
            if (aself != null)
                return new AccessExpression(aself, ident, token.Line, token.CharPositionInLine);
            else
                return ident;
        }

        internal AccessExpression addIdentifierAccessExpression(Expression parent, IToken token)
        {
            IdentifierExpression ident = new UnresolvedIdentifierExpression(token, GetScope());
            return new AccessExpression(parent, ident, token.Line, token.CharPositionInLine);
        }

        /* we have a primed id; prime the complete subtree.. */
        internal void setIdentifierExpressionPrimed(ref Expression result, IToken token)
        {
            Expression priming = new UnaryOperator(ExpressionKind.Primed, result, token.Line, token.CharPositionInLine);
            result = priming;
        }

        /* create a fold operation */
        internal Expression createFoldExpression(Expression result, IToken afold, Expression initval, Expression anexpr)
        {
            ExpressionKind akind = ExpressionKind.foldLR;
            if (afold.Type == ooaLexer.T_FOLDLR)
                akind = ExpressionKind.foldLR;
            else if (afold.Type == ooaLexer.T_FOLDRL)
                akind = ExpressionKind.foldRL;
            else
                System.Diagnostics.Debug.Assert(false);

            TernaryOperator op = new TernaryOperator(akind, result, initval, anexpr, currentLine, currentPos, GetScope());
            return op;
        }


        /* create a method access */
        internal CallExpression createMethodAccessExpression(Expression subexpr, List<Expression> m_params, IToken token)
        {
            System.Diagnostics.Debug.Assert(subexpr != null);

            return new CallExpression(subexpr, m_params, token.Line, token.CharPositionInLine, GetScope());
        }

        /* create a tuple or map access */
        internal TupleMapAccessExpression createTupleMapAccessExpression(Expression subexpr, Expression ac, IToken token)
        {
            System.Diagnostics.Debug.Assert(subexpr != null);

            return new TupleMapAccessExpression(subexpr, ac, token.Line, token.CharPositionInLine);
        }

        /* create a method call statement; has to be resolved in a second run */
        internal Statement createCallStatement(Expression aqname)
        {
            return new Call(aqname, currentLine, currentPos);
        }

        /* create a single assignment statement */
        internal Statement createSingleAssignmentStatement(Expression aqname, Expression aexp)
        {
            Assignment result = new Assignment(aqname, aexp, null, currentLine, currentPos);
            return result;
        }

        /* create a multi-assignment statement; has to be resolved in a second run */
        internal Statement createMultipleAssignmentStatementLHS(Expression aqname)
        {
            return new Assignment(aqname, null, null, currentLine, currentPos);
        }

        /* adds an expression to the multi-assign */
        internal void addMutlipleAssignmentStatementRHS(Statement result, Expression mexp)
        {
            ((Assignment)result).AddValue(mexp);
        }

        /* adds a LHS-var to the multi assign */
        internal void addMultipleAssignmentStatementLHS(Statement result, Expression malhs)
        {
            ((Assignment)result).AddPlace(malhs);
        }

        /* pop an assignment statement from the resolve stack */
        internal void popAssignmentOffResolveStack(Statement result)
        {
            System.Diagnostics.Debug.Assert(ReferenceEquals(result, pState.currentScope));
            pState.PopResolveStack();
        }

        /* pushes the assignment statement onto resolve stack. */
        internal void pushAssignmentOnResolveStack(Statement result)
        {
            System.Diagnostics.Debug.Assert(result is Assignment);
            pState.PushResolveStack((Assignment)result);
        }


        /* adds a nondet-assignment constraint */
        internal void addConstraintToAssignment(Statement result, Expression ndexp)
        {
            ((Assignment)result).SetNondetExpression(ndexp);
        }

        /* add a named action call to do-od block */
        internal void addNamedActionCallToBlockList(Block top, IToken aname, List<Expression> m_params, IToken maptoken, Expression amapexpression)
        {
            Identifier id = pState.Lookup(aname);
            if (id == null)
            {
                doError(aname, "Could not find named action");
                return;
            }
            Expression callexpr;
            if (id.kind == IdentifierKind.MethodIdentifier)
            {
                doError(aname, "Method access in do-od block not allowed.");
                return;
                // access via self
                /*
                Identifier self = pState.Lookup("self");
                if (self == null)
                    doError(aname, "Self access of method: Can not find 'self' symbol! (internal error)");
                IdentifierExpression aself = new IdentifierExpression(self, aname.Line, aname.CharPositionInLine);
                aself.setIsSelf(true);
                callexpr = new CallExpression(
                    new AccessExpression(aself,
                        new IdentifierExpression(id, aname.Line, aname.CharPositionInLine), aname.Line, aname.CharPositionInLine),
                        m_params, aname.Line, aname.CharPositionInLine, GetScope());
                 */
            }
            else
                callexpr = new CallExpression(
                   new IdentifierExpression(id, aname.Line, aname.CharPositionInLine),
                       m_params, aname.Line, aname.CharPositionInLine, GetScope());

            if (amapexpression != null)
            {
                ExpressionKind akind = ExpressionKind.foldLR;
                if (maptoken.Type == ooaLexer.T_FOLDLR)
                    akind = ExpressionKind.foldLR;
                else if (maptoken.Type == ooaLexer.T_FOLDRL)
                    akind = ExpressionKind.foldRL;
                else
                    System.Diagnostics.Debug.Assert(false);

                callexpr = new TernaryOperator(akind, callexpr, null, amapexpression,
                    currentLine, currentPos, GetScope());
            }
            Call statement = new Call(callexpr, currentLine, currentPos);
            top.AddStatement(statement);
        }

        /*adds skip statement instead of call to do-od block*/
        internal void addSkipStatementToBlockList(Block top)
        {
            top.AddStatement(new SkipStatement(currentLine, currentPos));
        }


        /* add anonymous action to do-od block */
        internal void addToBlockList(Block top, Statement gcmd)
        {
            if (gcmd != null)
                top.AddStatement(gcmd);
        }

        /* add the do-od block to the action system type */
        internal void addActionBlock(OoActionSystemType aTypeSymbol, Block bl)
        {
            aTypeSymbol.SetDoOdBlock(bl);
        }

        /* push block */
        internal void pushBlockToResolveStack(Block toPush)
        {
            pState.PushResolveStack(toPush);
        }

        /* pop block */
        internal void popBlockFromResolveStack(Block toPop)
        {
            if (toPop != null)
            {
                object anobject = pState.currentScope as Block;
                System.Diagnostics.Debug.Assert(Object.ReferenceEquals(anobject, toPop));

                pState.PopResolveStack();
            }
        }

        /* add block var */
        internal void addBlockVariable(Block seqList, IToken varname, UlyssesType aType)
        {
            if (aType == null)
            {
                doError(varname, String.Format("{0} lacks type!", varname.Text));
            }
            try
            {
                seqList.AddIdentifier(new LocalVariableIdentifier(varname, aType, GetScope()));
            }
            catch (ArgumentException)
            {
                doError(varname, String.Format("{0} redefined!", varname.Text));
            }
        }


        internal QualitativeConstraintStatement createTwoVarConstraintStatement(IToken id1, IToken id2, QualitativeConstraintOperation op)
        {
            Identifier var1 = pState.Lookup(id1);
            if (var1 == null)
            {
                var1 = new ExpressionVariableIdentifier(id1.Text, id1.Line, id1.CharPositionInLine);
                var1.SetType(new AnyType((ExpressionVariableIdentifier)var1));

                GetScope().AddIdentifier(var1, null);

                doWarning(id1, String.Format("Free variable in qualitative constraint: '{0}'.", id1.Text));
            }

            Identifier var2 = pState.Lookup(id2);
            if (var2 == null)
            {
                var2 = new ExpressionVariableIdentifier(id2.Text, id2.Line, id2.CharPositionInLine);
                var2.SetType(new AnyType((ExpressionVariableIdentifier)var2));

                GetScope().AddIdentifier(var2, null);

                doWarning(id1, String.Format("Free variable in qualitative constraint: '{0}'.", id2.Text));
            }

            QualitativeConstraintStatement result = new QualitativeConstraintStatement(var1, var2, op, id1.Line, id1.CharPositionInLine);
            return result;
        }


        internal QualitativeConstraintStatement createQualEqualConstraintStatement(IToken id1, IToken id2)
        {
            return createTwoVarConstraintStatement(id1, id2, QualitativeConstraintOperation.Equal);
        }

        internal QualitativeConstraintStatement createQualArithConstraintStatement(IToken id1, IToken id2, IToken id3, IToken op)
        {
            Identifier var1 = pState.Lookup(id1);
            if (var1 == null)
            {
                var1 = new ExpressionVariableIdentifier(id1.Text, id1.Line, id1.CharPositionInLine);
                var1.SetType(new AnyType((ExpressionVariableIdentifier)var1));

                GetScope().AddIdentifier(var1, null);

                doWarning(id1, String.Format("Free variable in qualitative constraint: '{0}'.", id1.Text));
            }

            Identifier var2 = pState.Lookup(id2);
            if (var2 == null)
            {
                var2 = new ExpressionVariableIdentifier(id2.Text, id2.Line, id2.CharPositionInLine);
                var2.SetType(new AnyType((ExpressionVariableIdentifier)var2));

                GetScope().AddIdentifier(var2, null);

                doWarning(id1, String.Format("Free variable in qualitative constraint: '{0}'.", id2.Text));
            }

            Identifier var3 = pState.Lookup(id3);
            if (var3 == null)
            {
                var3 = new ExpressionVariableIdentifier(id3.Text, id3.Line, id3.CharPositionInLine);
                var3.SetType(new AnyType((ExpressionVariableIdentifier)var3));

                GetScope().AddIdentifier(var3, null);

                doWarning(id1, String.Format("Free variable in qualitative constraint: '{0}'.", id3.Text));
            }
            QualitativeConstraintOperation operation;
            switch (op.Type)
            {
                case ooaParser.T_SUM:
                    operation = QualitativeConstraintOperation.Sum;
                    break;
                case ooaParser.T_DIFF:
                    operation = QualitativeConstraintOperation.Diff;
                    break;
                case ooaParser.T_PROD:
                    operation = QualitativeConstraintOperation.Prod;
                    break;
                default:
                    doError(op, String.Format("'{0}' unknown operation", op.Text));
                    return null;
            }

            QualitativeConstraintStatement result = new QualitativeConstraintStatement(var1, var2, var3, operation, id1.Line, id1.CharPositionInLine);
            return result;
        }

        internal QualitativeConstraintStatement createQualDerivConstraintStatement(IToken id1, IToken derivid)
        {
            return createTwoVarConstraintStatement(id1, derivid, QualitativeConstraintOperation.Deriv);
        }



        /* creates a general binary operator without any children */
        internal BinaryOperator createBinaryOperator(ExpressionKind akind)
        {
            IToken token = input.LT(-1);
            return new BinaryOperator(akind, null, null, token.Line, token.CharPositionInLine);
        }


        /* creates a general unary operator without child */
        internal UnaryOperator createUnaryOperator(ExpressionKind unaryOperatorType)
        {
            IToken token = input.LT(-1);
            return new UnaryOperator(unaryOperatorType, null, token.Line, token.CharPositionInLine);
        }

        /* create a conditional expression */
        internal Expression createConditionalExpression(Expression ce, Expression te, Expression ee, IToken ef)
        {
            return new TernaryOperator(ExpressionKind.conditional, ce, te, ee, ef.Line, ef.CharPositionInLine, GetScope());
        }

        /* create a quantifier expression */
        internal Quantifier createQuantifierExpression(IToken t)
        {
            Quantifier result = null;
            if (t.Type == T_FORALL)
                result = new ForallQuantifier(null, t.Line, t.CharPositionInLine);
            else
                result = new ExistsQuantifier(null, t.Line, t.CharPositionInLine);


            pState.PushResolveStack(result);
            return result;
        }

        /* add a bound variable to the quantifier */
        internal void addBoundVarToQuantifierExpression(Quantifier result, IToken id, UlyssesType id_type)
        {
            /*note: this might be a bit harsh, but for now it's easier to demand uniquely named vars,
                    without any hiding. Could be fixed in searching only the first resolve level for
                    dupes.. 
             */
            Identifier sym = pState.Lookup(id);
            if (sym != null)
                doError(id, String.Format("{0} already defined!", id.Text));
            else
            {
                if (id_type == null)
                    doError(id, String.Format("{0} lacks type (null).", id.Text));
                Identifier newvar = new ExpressionVariableIdentifier(id, id_type, GetScope());
                result.AddIdentifier(newvar, null);
            }
        }

        /* add the expression to the quantifier */
        internal void addExpressionToQuantifier(Quantifier result, Expression e)
        {
            result.SetChild(e);
        }

        /* remove local variables from resolve stack */
        internal void removeBoundVarsFromResolveStack(Quantifier result)
        {
            if (result != null)
                pState.PopResolveStack();
        }


        /* create a bool constant */
        internal LeafExpression createBoolConstant(bool p)
        {
            IToken token = input.LT(-1);
            return new ValueExpression<bool>(p, token.Line, token.CharPositionInLine);
        }

        /* create a nil */
        internal LeafExpression createNullPointerConstant()
        {
            IToken token = input.LT(-1);
            return new ValueExpression<object>(null, token.Line, token.CharPositionInLine);
        }

        /* create a 'self' identifier */
        internal LeafExpression createSelfPointer()
        {
            IToken token = input.LT(-1);
            Identifier self = pState.Lookup("self");
            if (self == null)
            {
                doError(token, "Could not resolve 'self'");
                return new UnresolvedIdentifierExpression(token, GetScope());
            }

            IdentifierExpression result = new IdentifierExpression(self, token.Line, token.CharPositionInLine);
            result.setIsSelf(true);

            return result;
        }

        /* create a float const */
        internal LeafExpression createFloatConstant(IToken t_fl)
        {
            return new ValueExpression<double>(double.Parse(t_fl.Text, System.Globalization.CultureInfo.InvariantCulture), t_fl.Line, t_fl.CharPositionInLine);
        }

        /* create int const */
        internal LeafExpression createIntConstant(IToken t_in)
        {
            return new ValueExpression<int>(int.Parse(t_in.Text), t_in.Line, t_in.CharPositionInLine);
        }

        /* set children of binary operator*/
        internal Expression addBinaryExpression(BinaryOperator binexpr, Expression expr, Expression e2)
        {
            binexpr.SetLeftChild(expr);
            binexpr.SetRightChild(e2);
            return binexpr;
        }

        /* set child of unary expr */
        internal Expression addUnaryExpression(UnaryOperator unexpr, Expression e)
        {
            if (unexpr != null)
            {
                unexpr.SetChild(e);
                return unexpr;
            }
            else
                return e;
        }



        /* create a list */
        internal ListConstructor createInitializedList()
        {
            IToken nexttoken = input.LT(1);
            return new ListConstructor(nexttoken.Line, nexttoken.CharPositionInLine);
        }

        /* add an element to the list */
        internal void addListElement(ListConstructor result, Expression e)
        {
            result.AddElement(e);
        }

        /* push list comprehension vars on resolve stack */
        internal void pushListVarsOnResolveStack(ListConstructor result)
        {
            pState.PushResolveStack(result);
        }

        /* pop list comprehension vars from resolve stack */
        internal void popListVarsFromResolveStack(ListConstructor result)
        {
            if (result != null)
                pState.PopResolveStack();
        }

        /* set list comprehension expression */
        internal void addListComprExpr(ListConstructor result, Expression e)
        {
            result.SetComprehension(e);
        }

        /* add list comprehension variable */
        internal void addListComprVar(ListConstructor result, IToken id, UlyssesType t1)
        {
            Identifier sym = pState.Lookup(id);
            if (sym != null)
            {
                /* see notes in quantifier*/
                doError(id, String.Format("{0} already defined.", id.Text));
            }
            else
            {
                ExpressionVariableIdentifier newvar = new ExpressionVariableIdentifier(id, t1, GetScope());
                result.AddIdentifier(newvar, null);
            }
        }

        /* converts a string into a list of char */
        internal ListConstructor createStringConstant(IToken t_l)
        {
            ListConstructor result = new ListConstructor(t_l.Line, t_l.CharPositionInLine);
            foreach (char c in t_l.Text.Substring(1, t_l.Text.Length - 2))
                result.AddElement(new ValueExpression<char>(c, t_l.Line, t_l.CharPositionInLine));
            return result;
        }

        /* creates an empty map */
        internal Expression createEmptyMap()
        {
            IToken token = input.LT(-1);
            return new MapConstructor(token.Line, token.CharPositionInLine);
        }

        /* create a map and populate it with two items.. */
        internal Expression createMap(Expression e1, Expression e2, IToken am)
        {
            MapConstructor result = new MapConstructor(am.Line, am.CharPositionInLine);
            result.AddItem(e1, e2);
            return result;
        }

        /* add a key/value pair to a map */
        internal void addToMap(Expression map, Expression e3, Expression e4)
        {
            ((MapConstructor)map).AddItem(e3, e4);
        }

        /* create a set */
        internal SetConstructor createSet()
        {
            IToken nexttoken = input.LT(1);
            SetConstructor result = new SetConstructor(nexttoken.Line, nexttoken.CharPositionInLine);
            return result;
        }

        /* add item to set */
        internal void addToSet(Expression result, Expression e2)
        {
            ((SetConstructor)result).AddItem(e2);
        }

        /* remove set comprehension variables from resolution stack */
        internal void popSetVarsFromResolveStack(SetConstructor _set)
        {
            if (_set != null)
                pState.PopResolveStack();
        }

        /* add set comprehension variables to resolution stack */
        internal void pushSetVarsOnResolveStack(SetConstructor _set)
        {
            pState.PushResolveStack(_set);
        }

        /* set comprehension expression fro set */
        internal void addSetComprExpr(SetConstructor _set, Expression epx)
        {
            _set.SetComprehension(epx);
        }

        /* add local set compr. variable */
        internal void addSetComprVar(SetConstructor _set, IToken id1, UlyssesType t1)
        {
            Identifier sym = pState.Lookup(id1);
            if (sym != null)
                doError(id1, String.Format("{0} already defined!", id1.Text));
            else
            {
                ExpressionVariableIdentifier newvar = new ExpressionVariableIdentifier(id1, t1, GetScope());
                _set.AddIdentifier(newvar, null);
            }
        }

        /* check whether identifier p is a tuple type */
        internal bool isTuple(string p)
        {
            Identifier sym = pState.Lookup(p);
            return (sym != null)
                && (sym.kind == IdentifierKind.TypeIdentifier)
                && (sym.type.kind == TypeKind.TupleType);
        }

        /* create an initialized tuple */
        internal Expression createInitializedTuple(IToken aName, System.Collections.Generic.List<Expression> m_params)
        {
            Identifier sym = pState.Lookup(aName);
            if ((sym == null) || !(sym.type is TupleType))
            {
                doError(aName, "Not a tuple type!");
                return null;
            }

            TupleType atuple = (TupleType)sym.type;
            if (atuple.innerTypes.Count != m_params.Count)
            {
                doError(aName, "Number of parameters does not match type definition!");
                return null;
            }

            return new TupleConstructor(sym, m_params, aName.Line, aName.CharPositionInLine);
        }


        /* create an reference expression: (<expression>).xyz */
        internal Expression createExpressionReference(Expression e, Expression aref, IToken atoken)
        {
            AccessExpression result = new AccessExpression(e, aref, atoken.Line, atoken.CharPositionInLine);
            return result;
        }


        /* gets called when we are parsing attributes */
        internal void BeginParsingAttributes()
        {
            pState.parsingAttributes = true;
        }

        /* gets called when we stop parsing attributes */
        internal void EndParsingAttributes()
        {
            pState.parsingAttributes = false;
        }

        /*dummy*/
        internal bool notIsAttributeInitialization()
        {
            return !pState.parsingAttributes;
        }

        /* create a new(anid) constructor */
        private Expression createObject(IToken anid)
        {
            if (!pState.parsingAttributes)
            {
                doError(anid, "Object creation with 'new' only allowed in variable initializers.");
                return null;
            }


            OpaqueType atype = new OpaqueType(new TypeIdentifier(anid, null, GetScope()));
            pState.typesToFixUp.Add(atype);
            return new ObjectConstructor(atype, anid.Line, anid.CharPositionInLine);
        }


        private Expression createNamedObject(IToken anid, IToken aname)
        {
            if (!pState.parsingAttributes)
            {
                doError(anid, "Object creation with 'new' only allowed in variable initializers.");
                return null;
            }

            Regex validid = new Regex("\"[_]*[a-zA-Z][a-zA-Z0-9_]*\"");
            if (!validid.IsMatch(aname.Text))
            {
                doError(aname, "Not a valid identifier");
                return null;
            }

            OpaqueType atype = new OpaqueType(new TypeIdentifier(anid, null, GetScope()));
            pState.typesToFixUp.Add(atype);
            return new ObjectConstructor(atype, aname.Text, anid.Line, anid.CharPositionInLine);
        }


        internal void setQualitativeDerivDec(QValConstructor result)
        {
            result.SetDerivation(QValDeriv.Dec);
        }

        internal void setQualitativeDerivInc(QValConstructor result)
        {
            result.SetDerivation(QValDeriv.Inc);
        }

        internal void setQualitativeDerivSteady(QValConstructor result)
        {
            result.SetDerivation(QValDeriv.Steady);
        }

        internal void setQualitativeDerivDontCare(QValConstructor result)
        {
            result.SetDerivation(QValDeriv.DonTCare);
        }

        internal void setQualitativeValueRangeInfinity(QValConstructor result, bool p)
        {
            throw new NotImplementedException();
        }

        internal void setQualitativeValueRange(QValConstructor result, Expression expr2)
        {
            result.AddRange(expr2);
        }

        internal void setQualitativeValueInfinity(QValConstructor result, bool minus)
        {
            throw new NotImplementedException();
        }

        internal void setQualitativeValueLandmark(QValConstructor result, Expression expr)
        {
            result.SetValue(expr);
        }

        internal void setQualitativeValueDontCare(QValConstructor result)
        {
            throw new NotImplementedException();
        }

        internal QValConstructor createQualitativeValue(IToken aval)
        {
            return new QValConstructor(aval.Line, aval.CharPositionInLine);
        }

        /* add a local variable to a named action */
        internal void addLocalVariableToNamedAction(FunctionIdentifier newMethod, IToken id1, UlyssesType t1)
        {
            if (t1 == null)
            {
                doError(id1, "Variable lacks type");
                return;
            }

            LocalVariableIdentifier lvar = new LocalVariableIdentifier(id1, t1, GetScope());
            newMethod.AddIdentifier(lvar, null);
        }

        /* ====== */
        /* ====== */

        public Dictionary<string, string> readableTokens = new Dictionary<string, string>();


        private void SetUpTokenDictionary()
        {
            if (readableTokens.Count > 0)
                return;
            readableTokens.Add("<invalid>", "<invalid>");
            readableTokens.Add("<EOR>", "<EOR>");
            readableTokens.Add("<DOWN>", "<DOWN>");
            readableTokens.Add("<UP>", "<UP>");
            readableTokens.Add("T_TYPES", "'types'");
            readableTokens.Add("T_SYSTEM", "'system'");
            readableTokens.Add("T_SEMICOLON", "';'");
            readableTokens.Add("T_IDENTIFIER", "<identifier>");
            readableTokens.Add("T_EQUAL", "'='");
            readableTokens.Add("T_PRIO", "'//'");
            readableTokens.Add("T_NONDET", "'[]'");
            readableTokens.Add("T_LPAREN", "'('");
            readableTokens.Add("T_RPAREN", "')'");
            readableTokens.Add("T_LIST", "'list'");
            readableTokens.Add("T_LSQPAREN", "'['");
            readableTokens.Add("T_INTNUMBER", "<integer>");
            readableTokens.Add("T_RSQPAREN", "']'");
            readableTokens.Add("T_OF", "'of'");
            readableTokens.Add("T_COMMA", "','");
            readableTokens.Add("T_MAP", "'map'");
            readableTokens.Add("T_TO", "'to'");
            readableTokens.Add("T_QUANTITY", "'quantity'");
            readableTokens.Add("T_INFTY", "'inf'");
            readableTokens.Add("T_BOOL", "'bool'");
            readableTokens.Add("T_INT", "'int'");
            readableTokens.Add("T_RANGETO", "'..'");
            readableTokens.Add("T_FLOAT", "'float'");
            readableTokens.Add("T_FLOATNUMBER", "<floating point number>");
            readableTokens.Add("T_CHAR", "'char'");
            readableTokens.Add("T_CBRL", "'{'");
            readableTokens.Add("T_CBRR", "'}'");
            readableTokens.Add("T_AUTOCONS", "'autocons'");
            readableTokens.Add("T_VAR", "'var'");
            readableTokens.Add("T_METHODS", "'methods'");
            readableTokens.Add("T_ACTIONS", "'actions'");
            readableTokens.Add("T_DO", "'do'");
            readableTokens.Add("T_OD", "'od'");
            readableTokens.Add("T_STATIC", "'static'");
            readableTokens.Add("T_COLON", "':'");
            readableTokens.Add("T_END", "'end'");
            readableTokens.Add("T_CONT", "'cont'");
            readableTokens.Add("T_CTRL", "'ctr'");
            readableTokens.Add("T_OBS", "'obs'");
            readableTokens.Add("T_REQUIRES", "'requires'");
            readableTokens.Add("T_AND", "'and'");
            readableTokens.Add("T_ABORT", "'abort'");
            readableTokens.Add("T_SKIP", "'skip'");
            readableTokens.Add("T_KILL", "'kill'");
            readableTokens.Add("T_SELF", "'self'");
            readableTokens.Add("T_ASSIGNMENT", "':='");
            readableTokens.Add("T_WITH", "'with'");
            readableTokens.Add("T_IF", "'if'");
            readableTokens.Add("T_THEN", "'then'");
            readableTokens.Add("T_ELSE", "'else'");
            readableTokens.Add("T_FORALL", "'forall'");
            readableTokens.Add("T_EXISTS", "'exists'");
            readableTokens.Add("T_TRUE", "'true'");
            readableTokens.Add("T_FALSE", "'false'");
            readableTokens.Add("T_NIL", "'nil'");
            readableTokens.Add("T_STRINGLITERAL", "'\"<string>\"'");
            readableTokens.Add("T_NEW", "'new'");
            readableTokens.Add("T_BAR", "'|'");
            readableTokens.Add("T_MAPS", "'->'");
            readableTokens.Add("T_PRIMED", "'''");
            readableTokens.Add("T_POINT", "'.'");
            readableTokens.Add("T_NOTEQUAL", "'<>'");
            readableTokens.Add("T_SEQMOD_MAPOVERRIDE", "'++'");
            readableTokens.Add("T_BIIMPLIES", "'<=>'");
            readableTokens.Add("T_IMPLIES", "'=>'");
            readableTokens.Add("T_OR", "'or'");
            readableTokens.Add("T_ABS", "'abs'");
            readableTokens.Add("T_DIV", "'/'");
            readableTokens.Add("T_GREATER", "'>'");
            readableTokens.Add("T_GREATEREQUAL", "'>='");
            readableTokens.Add("T_IDIV", "'div'");
            readableTokens.Add("T_LESS", "'<'");
            readableTokens.Add("T_LESSEQUAL", "'<='");
            readableTokens.Add("T_MINUS", "'-'");
            readableTokens.Add("T_MOD", "'mod'");
            readableTokens.Add("T_POW", "'**'");
            readableTokens.Add("T_PROD", "'*'");
            readableTokens.Add("T_SUM", "'+'");
            readableTokens.Add("T_CONC", "'^'");
            readableTokens.Add("T_DIFF", "'\\'");
            readableTokens.Add("T_INTER", "'inter'");
            readableTokens.Add("T_IN", "'in'");
            readableTokens.Add("T_SET", "'set'");
            readableTokens.Add("T_NOT", "'not'");
            readableTokens.Add("T_SUBSET", "'subset'");
            readableTokens.Add("T_UNION", "'union'");
            readableTokens.Add("T_DOMRESBY", "'<-:'");
            readableTokens.Add("T_DOMRESTO", "'<:'");
            readableTokens.Add("T_RNGRESBY", "':->'");
            readableTokens.Add("T_RNGRESTO", "':>'");
            readableTokens.Add("T_MUNION", "'munion'");
            readableTokens.Add("T_CARD", "'card'");
            readableTokens.Add("T_DCONC", "'conc'");
            readableTokens.Add("T_DINTER", "'dinter'");
            readableTokens.Add("T_DUNION", "'dunion'");
            readableTokens.Add("T_ELEMS", "'elems'");
            readableTokens.Add("T_HEAD", "'hd'");
            readableTokens.Add("T_INDS", "'inds'");
            readableTokens.Add("T_LEN", "'len'");
            readableTokens.Add("T_TAIL", "'tl'");
            readableTokens.Add("T_DOM", "'dom'");
            readableTokens.Add("T_RNG", "'rng'");
            readableTokens.Add("T_MERGE", "'merge'");
            readableTokens.Add("T_WS", "<space>");
            readableTokens.Add("T_COMMENT", "'/*<comment>*/'");
            readableTokens.Add("LINE_COMMENT", "'#<line comment>'");
            readableTokens.Add("T_DIGIT", "<0..9>");
            readableTokens.Add("FLOAT_OR_INT_OR_RANGE", "<float_int_range>");
            readableTokens.Add("T_LETTER", "<a..z,A..Z>");
            readableTokens.Add("'|['", "'|['");
            readableTokens.Add("']|'", "']|'");
            readableTokens.Add("'add'", "'add'");
            readableTokens.Add("'mult'", "'mult'");
            readableTokens.Add("'deriv'", "'deriv'");
            readableTokens.Add("'mon+'", "'mon+'");
            readableTokens.Add("'mon-'", "'mon-'");
            readableTokens.Add("'id'", "'id'");
            readableTokens.Add("'qval'", "'qval'");
            readableTokens.Add("'\"'", "'\"'");
            readableTokens.Add("as", "as");
        }

        /* override routine that displays recongition errors.. */
        public override void DisplayRecognitionError(String[] tokenNames, RecognitionException e)
        {
            int i;
            System.Text.StringBuilder result = new System.Text.StringBuilder();
            SetUpTokenDictionary();


            if (e is MismatchedTokenException)
            {
                result.Append("Found '");
                result.Append(e.Token.Text);
                result.Append("'");
                i = ((MismatchedTokenException)e).Expecting;
                result.Append(" Expected: ");
                result.Append(readableTokens[tokenNames[i]]);
                result.Append(" ("); result.Append(tokenNames[i]); result.Append(") ");

            }
            else
            {
                /*if (e is NoViableAltException)
                {
                    result.Append("Unexpected '");
                    result.Append(e.Token.Text);
                    result.Append("' (");
                    i = ((NoViableAltException)e).UnexpectedType;                    
                    result.Append(tokenNames[i]);
                    result.Append(")");
                }
                else*/
                if (e is RecognitionException)
                {
                    result.Append("Unexpected '");
                    result.Append(e.Token.Text);
                    result.Append("' (");
                    i = ((RecognitionException)e).UnexpectedType;
                    result.Append(tokenNames[i]);
                    result.Append(") ");
                }
                else
                    result.Append(e.Message);
            }

            pState.AddErrorMessage(new ParserError(pState.filename, e.Line, e.CharPositionInLine, result.ToString()));
        }


        /* just run over once */
        public static int FirstPass(ParserState pState)
        {
            pState.parser.ooActionSystems();

            return pState.listOfParserErrors.Count; // + pState.lexer.NumberOfSyntaxErrors;
        }



        /* print syntax tree */
        public static string PrintSyntaxTree(ParserState pState)
        {
            if ((pState != null) && (pState.ooaSystem != null))
            {
                return pState.ooaSystem.ToString();
            }
            else
                return String.Empty;
        }
    }
}