OoasTools

/**

  *

  *                      OOAS Compiler

  *

  *       Copyright 2015, AIT Austrian Institute of Technology.

  * This code is based on the C# Version of the OOAS Compiler, which is

  * copyright 2015 by the Institute of Software Technology, Graz University

  * of Technology with portions copyright by the AIT Austrian Institute of

  * Technology. All rights reserved.

  *

  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.

  *

  * If you modify the file please update the list of contributors below to in-

  * clude your name. Please also stick to the coding convention of using TABs

  * to do the basic (block-level) indentation and spaces for anything after

  * that. (Enable the display of special chars and it should be pretty obvious

  * what this means.) Also, remove all trailing whitespace.

  *

  * Contributors:

  *               Willibald Krenn (AIT)

  *               Stephan Zimmerer (AIT)

  *               Markus Demetz (AIT)

  *               Christoph Czurda (AIT)

  *

  */

package org.momut.ooas.parser;

import java.util.LinkedHashMap;

import java.util.LinkedList;

import java.util.List;

import org.antlr.runtime.MismatchedTokenException;

import org.antlr.runtime.Parser;

import org.antlr.runtime.RecognitionException;

import org.antlr.runtime.RecognizerSharedState;

import org.antlr.runtime.Token;

import org.antlr.runtime.TokenStream;

import org.momut.ooas.ast.IScope;

import org.momut.ooas.ast.expressions.AccessExpression;

import org.momut.ooas.ast.expressions.BinaryOperator;

import org.momut.ooas.ast.expressions.CallExpression;

import org.momut.ooas.ast.expressions.ExistsQuantifier;

import org.momut.ooas.ast.expressions.Expression;

import org.momut.ooas.ast.expressions.ExpressionKind;

import org.momut.ooas.ast.expressions.ForallQuantifier;

import org.momut.ooas.ast.expressions.IdentifierExpression;

import org.momut.ooas.ast.expressions.LeafExpression;

import org.momut.ooas.ast.expressions.ListConstructor;

import org.momut.ooas.ast.expressions.MapConstructor;

import org.momut.ooas.ast.expressions.ObjectConstructor;

import org.momut.ooas.ast.expressions.Quantifier;

import org.momut.ooas.ast.expressions.SetConstructor;

import org.momut.ooas.ast.expressions.TernaryOperator;

import org.momut.ooas.ast.expressions.TupleConstructor;

import org.momut.ooas.ast.expressions.TupleMapAccessExpression;

import org.momut.ooas.ast.expressions.UnaryOperator;

import org.momut.ooas.ast.expressions.UnresolvedIdentifierExpression;

import org.momut.ooas.ast.expressions.ValueExpression;

import org.momut.ooas.ast.identifiers.AttributeIdentifier;

import org.momut.ooas.ast.identifiers.ConstantIdentifier;

import org.momut.ooas.ast.identifiers.EnumIdentifier;

import org.momut.ooas.ast.identifiers.ExpressionVariableIdentifier;

import org.momut.ooas.ast.identifiers.FunctionIdentifier;

import org.momut.ooas.ast.identifiers.Identifier;

import org.momut.ooas.ast.identifiers.IdentifierKind;

import org.momut.ooas.ast.identifiers.IdentifierList;

import org.momut.ooas.ast.identifiers.LocalVariableIdentifier;

import org.momut.ooas.ast.identifiers.MainModule;

import org.momut.ooas.ast.identifiers.MethodIdentifier;

import org.momut.ooas.ast.identifiers.NamedActionIdentifier;

import org.momut.ooas.ast.identifiers.ParameterIdentifier;

import org.momut.ooas.ast.identifiers.SelfTypeIdentifier;

import org.momut.ooas.ast.identifiers.TypeIdentifier;

import org.momut.ooas.ast.statements.AbortStatement;

import org.momut.ooas.ast.statements.Assignment;

import org.momut.ooas.ast.statements.Block;

import org.momut.ooas.ast.statements.BreakStatement;

import org.momut.ooas.ast.statements.Call;

import org.momut.ooas.ast.statements.GuardedCommand;

import org.momut.ooas.ast.statements.KillStatement;

import org.momut.ooas.ast.statements.NondetBlock;

import org.momut.ooas.ast.statements.PrioBlock;

import org.momut.ooas.ast.statements.SeqBlock;

import org.momut.ooas.ast.statements.SkipStatement;

import org.momut.ooas.ast.statements.Statement;

import org.momut.ooas.ast.types.BoolType;

import org.momut.ooas.ast.types.CharType;

import org.momut.ooas.ast.types.EnumType;

import org.momut.ooas.ast.types.FloatType;

import org.momut.ooas.ast.types.FunctionType;

import org.momut.ooas.ast.types.IntType;

import org.momut.ooas.ast.types.ListType;

import org.momut.ooas.ast.types.MapType;

import org.momut.ooas.ast.types.OoActionSystemType;

import org.momut.ooas.ast.types.OpaqueType;

import org.momut.ooas.ast.types.TupleType;

import org.momut.ooas.ast.types.TypeKind;

import org.momut.ooas.ast.types.Type;

import org.momut.ooas.ast.types.ValuedEnumType;

import org.momut.ooas.ast.types.FunctionType.FunctionTypeEnum;

import org.momut.ooas.utils.exceptions.ArgumentException;

import org.momut.ooas.utils.exceptions.NotImplementedException;

import org.momut.ooas.visitors.OoaResolveExpressionsVisitor;

public class ooaCustomParser extends Parser

{

        public ParserState pState;

        public boolean IsRightToLeft(ExpressionKind type)

        {

                return type == ExpressionKind.implies; // implication has right grouping

        }

        public int GetOperatorPrecedence(ExpressionKind type)

        {

                switch (type)

                {

                /*Family of Evaluators*/

                case abs:    // T_ABS:

                case card:   // T_CARD:

                case dom:    // T_DOM:

                case range:  // T_RNG:

                case merge:  // T_MERGE:

                case len:    // T_LEN:

                case elems:  // T_ELEMS:

                case head:   // T_HEAD:

                case tail:   // T_TAIL:

                case conc:   // T_CONC:

                case inds:   // T_INDS:

                case dinter: // T_DINTER:

                case dunion: // T_DUNION:

                        return 1;

                case domresby:   // T_DOMRESBY:

                case domresto:   // T_DOMRESTO:

                case rngresby:   // T_RNGRESBY:

                case rngresto:   // T_RNGRESTO:

                        return 2;

                case div:    // T_DIV:

                case idiv:   // T_IDIV:

                case mod:    // T_MOD:

                case prod:   // T_PROD:

                case inter:  // T_INTER:

                        return 3;

                case sum:    // T_SUM:

                case minus:  // T_MINUS:

                case union:  // T_UNION:

                case diff:   // T_DIFF:

                case munion: // T_MUNION:

                case seqmod_mapoverride: // T_SEQMOD_MAPOVERRIDE:

                        return 4;

                        /*Family of Relations*/

                case less:

                case lessequal:

                case greater:

                case greaterequal:

                case equal:

                case notequal:

                case subset:

                case elemin:

                case notelemin:

                        return 5;

                        /*Family of Connectives*/

                case and:    // T_AND:

                        return 6;

                case or:     // T_OR:

                        return 7;

                case implies:    // T_IMPLIES:

                        return 8;

                case 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;

                final BinaryOperator binop = operators.get(pivot);

                int pivotRank = GetOperatorPrecedence(binop.kind());

                for (int i = startIndex + 1; i <= stopIndex; i++)

                {

                        final ExpressionKind type = operators.get(i).kind();

                        final int current = GetOperatorPrecedence(type);

                        final boolean rtl = IsRightToLeft(type);

                        if (current > pivotRank || (current == pivotRank && rtl))

                        {

                                pivot = i;

                                pivotRank = current;

                        }

                }

                return pivot;

        }

        Expression createPrecedenceTree(

                        List<Expression> expressions,

                        List<BinaryOperator> operators,

                        int startIndex,

                        int stopIndex)

        {

                if (stopIndex == startIndex)

                        return expressions.get(startIndex);

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

                final BinaryOperator result = operators.get(pivot);

                result.SetLeftChild(createPrecedenceTree(expressions, operators, startIndex, pivot));

                result.SetRightChild(createPrecedenceTree(expressions, operators, pivot + 1, stopIndex));

                return result;

        }

        Expression createPrecedenceTree(List<Expression> expressions, List<BinaryOperator> operators)

        {

                return createPrecedenceTree(expressions, operators, 0, expressions.size() - 1);

        }

        /* add error message to state. */

        private void doError(Token aToken, String aMessage)

        {

                pState.AddErrorMessage(

                                new ParserError(pState.filename, aToken, aMessage));

        }

//        /* add warning message to state */

//        private void doWarning(Token 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 */

         void initializeTopLevelParserState()

        {

                pState.ooaSystem = new MainModule();

                pState.PushResolveStack(pState.ooaSystem);

        }

        private IScope GetScope()

        {

                return pState.currentScope;

        }

        /*create a named constant*/

         void addNamedConst(Token aName, Expression anExpr)

        {

                if (pState.currentScope.ResolveIdentifier(aName.getText()) == null)

                {

                        /* needs to be a constant... */

                        final ConstantIdentifier aConst = new ConstantIdentifier(aName, anExpr, GetScope());

                        final 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("%s not a constant!", aName.getText()));

                        }

                        else

                        {

                                aConst.SetType(aConst.Value().type());

                                pState.currentScope.AddIdentifier(aConst, null);

                        }

                }

                else

                        doError(aName, String.format("%s already defined!", aName.getText()));

        }

        /* create a named type; we're on top-level here */

         void createNamedType(Token aName, Type aType)

        {

                // precond..

                assert(aName != null);

                if (aType == null)

                {

                        doError(aName, String.format("%s lacks a type! (Type not added)", aName.getText()));

                        return;

                }

                if (pState.currentScope.ResolveIdentifier(aName.getText()) == null)

                {

                        final TypeIdentifier newid = new TypeIdentifier(aName, aType, GetScope());

                        aType.SetTypeIdentifier(newid);

                        pState.currentScope.AddIdentifier(newid, null);

                }

                else

                        doError(aName, String.format("%s already defined!", aName.getText()));

        }

        /* create basic structure for an ooa-system descr. resolve stack TOS is now ooa-system symbols */

        OoActionSystemType createOoaType(Token refinesSystemName, boolean autoCons)

        {

                final Identifier refinedSystem = pState.Lookup(refinesSystemName);

                OoActionSystemType refinedSystemType = null;

                if ((refinedSystem != null) && (refinedSystem.type() != null))

                {

                        if (refinedSystem.type().kind() != TypeKind.OoActionSystemType)

                                doError(refinesSystemName,

                                                String.format("%s not an object oriented action system", refinesSystemName.getText()));

                        else

                                refinedSystemType = (OoActionSystemType)refinedSystem.type();

                }

                else if (refinesSystemName != null)

                {

                        pState.AddErrorMessage(

                                        new ParserError(pState.filename, refinesSystemName,

                                                        String.format("Type that's being refined (%s) not found!", refinesSystemName.getText())));

                }

                final 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 */

        void fixupOoaType(OoActionSystemType aTypeSymbol)

        {

                if (aTypeSymbol == null)

                        return;

                aTypeSymbol.SetupAnonymousName();

                if (aTypeSymbol != null)

                        pState.PopResolveStack();

        }

        Expression addCastExpression(Expression e, Token cid)

        {

                assert(e != null);

                final Expression result = new UnaryOperator(ExpressionKind.Cast, e, cid.getLine(), cid.getCharPositionInLine());

                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 */

         void addToIdentifierList(IdentifierList top, Token aName)

        {

                assert(top != null);

                final Identifier aSym = pState.Lookup(aName);

                if (aSym == null)

                {

                        doError(aName, String.format("Could not find ooa-system %s!", aName.getText()));

                }

                else if ((aSym.type() == null) || !(aSym.type().kind() == TypeKind.OoActionSystemType))

                {

                        doError(aName, String.format("Referenced type (%s) does not have correct type!", aName.getText()));

                }

                else

                {

                        final OoActionSystemType aType = (OoActionSystemType)aSym.type();

                        if (aType.isInSystemDescription())

                                doError(aName, String.format("Referenced type (%s) already used in composition!", aName.getText()));

                        else

                                aType.SetIsInSystemDescription(true);

                        top.AddElement(aSym);

                }

        }

        /* does a fixup run after parsing */

         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. */

                for (final OpaqueType ntype: pState.typesToFixUp)

                {

                        if (ntype.resolvedType() == null)

                        {

                                //ntype.identifier

                                final Identifier asym = pState.Lookup(ntype.identifier().tokenText(), ntype.identifier().definingScope());

                                if ((asym == null) || (asym.kind() != IdentifierKind.TypeIdentifier))

                                {

                                        final ParserError error = new ParserError(pState.filename, ntype.identifier().line(), ntype.identifier().column(),

                                                        String.format("Can not resolve %s to a named type", ntype.identifier().tokenText()));

                                        pState.AddErrorMessage(error);

                                }

                                else

                                        ntype.SetResolvedType(asym.type());

                        }

                }

                pState.typesToFixUp.clear();

        }

        private boolean TosIsActionSystem()

        {

                return pState.currentScope instanceof OoActionSystemType;

        }

        private int currentLine()

        {

                final Token token = input.LT(-1);

                return token == null ? 0 : token.getLine();

        }

        private int currentPos()

        {

                final Token token = input.LT(-1);

                return token == null ? 0 : token.getCharPositionInLine();

        }

        /* add var symbol to the current action system */

        void createAttribute(Token varname, boolean isStatic, boolean isObs, boolean isCtr, Type aType, Expression anExpr)

        {

                if (!TosIsActionSystem())

                        return;

                if (aType == null)

                {

                        doError(varname, String.format("%s lacks type!", varname.getText()));

                }

                if (anExpr == null)

                {

                        doError(varname, String.format("%s lacks initializer!", varname.getText()));

                }

                if (isObs == true || isCtr == true)

                        doError(varname, "'obs' or 'ctr' on attributes not allowed");

                final AttributeIdentifier var = new AttributeIdentifier(varname, aType, GetScope(), anExpr, isStatic, isObs, isCtr);

                if (pState.currentScope.ResolveIdentifier(varname.getText()) == null)

                        pState.currentScope.AddIdentifier(var, null);

                else

                        doError(varname, String.format("Can not add %s: Symbol already defined!", varname.getText()));

        }

        /* create a boolean type */

        BoolType createBoolType()

        {

                return new BoolType(null);

        }

        /* create a char type */

        CharType createCharType()

        {

                return new CharType(null);

        }

        /* create an int type */

        @SuppressWarnings("unchecked")

        Type createIntType(Token rangeLow, Token rangeHigh)

        {

                int low = 0;

                int high = 0;

                if (rangeLow.getType() == ooaLexer.T_INFTY)

                        doError(rangeLow, "Infinity not supported.");

                if (rangeLow.getType() == ooaLexer.T_INFTY)

                        doError(rangeHigh, "Infinity not supported.");

                if (rangeLow.getType() == ooaLexer.T_IDENTIFIER)

                {

                        // see whether we can find the constant

                        final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeLow.getText());

                        if (aconst == null || aconst.kind() != IdentifierKind.Constant)

                                doError(rangeLow, String.format("Constant %s not found", rangeLow.getText()));

                        else if (aconst.type().kind() != TypeKind.IntType)

                                doError(rangeLow, "Constant must be integer");

                        else

                                low = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

                }

                else

                        try {

                                low = Integer.parseInt(rangeLow.getText());

                        } catch (final NumberFormatException e) {

                                doError(rangeLow, "Can not convert to integer");

                        }

                if (rangeHigh.getType() == ooaLexer.T_IDENTIFIER)

                {

                        // see whether we can find the constant

                        final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeHigh.getText());

                        if (aconst == null || aconst.kind() != IdentifierKind.Constant)

                                doError(rangeHigh, String.format("Constant %s not found", rangeHigh.getText()));

                        else if (aconst.type().kind() != TypeKind.IntType)

                                doError(rangeHigh, "Constant must be integer");

                        else

                                high = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

                }

                else

                        try {

                                high = Integer.parseInt(rangeHigh.getText());

                        } catch (final NumberFormatException e) {

                                doError(rangeLow, "Can not convert to integer");

                        }

                if (high < low)

                        doError(rangeHigh, "Lower bound greater than upper bound");

                return new IntType(low, high, null);

        }

        /* create a float type */

         @SuppressWarnings("unchecked")

        Type createFloatType(Token rangeLow, Token rangeHigh)

        {

                float low = 0;

                float high = 0;

                if (rangeLow.getType() == ooaLexer.T_INFTY)

                        doError(rangeLow, "Infinity not supported.");

                if (rangeLow.getType() == ooaLexer.T_INFTY)

                        doError(rangeHigh, "Infinity not supported.");

                if (rangeLow.getType() == ooaLexer.T_IDENTIFIER)

                {

                        // see whether we can find the constant

                        final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeLow.getText());

                        if (aconst == null || aconst.kind() != IdentifierKind.Constant)

                                doError(rangeLow, String.format("Constant %s not found", rangeLow.getText()));

                        else if (aconst.type().kind() != TypeKind.FloatType)

                                doError(rangeLow, "Constant must be float");

                        else

                                low = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

                }

                else

                        try {

                                low = Float.parseFloat(rangeLow.getText());

                        } catch (final NumberFormatException e) {

                                doError(rangeLow, "Can not convert to float (single)");

                        }

                if (rangeHigh.getType() == ooaLexer.T_IDENTIFIER)

                {

                        // see whether we can find the constant

                        final Identifier aconst = pState.currentScope.ResolveIdentifier(rangeHigh.getText());

                        if (aconst == null || aconst.kind() != IdentifierKind.Constant)

                                doError(rangeHigh, String.format("Constant %s not found", rangeHigh.getText()));

                        else if (aconst.type().kind() != TypeKind.FloatType)

                                doError(rangeHigh, "Constant must be integer");

                        else

                                high = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

                }

                else

                        try {

                                high = Float.parseFloat(rangeHigh.getText());

                        } catch (final NumberFormatException e){

                                doError(rangeHigh, "Can not convert to float (single)");

                        }

                if (high < low)

                        doError(rangeHigh, "Lower bound greater than upper bound");

                /* precision */

                final float afterc_low = low -  (float)Math.floor(low); //(float)Convert.ToInt32(low);

                final float afterc_high = high - (float)Math.floor(high); //(float)Convert.ToInt32(high);

                final float precision = afterc_low < afterc_high ? afterc_low : afterc_high;

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

        }

        /* create a list of an enumerated type */

         Type createListEnumType(Token alistelem)

        {

                final EnumType hiddenEnumType = new EnumType(null);

                final 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 */

         void addToListEnumType(Type aTypeSymbol, Token otherlistelem)

        {

                final EnumType enumtype = (EnumType)((ListType)aTypeSymbol).innerType();

                addToEnumType(enumtype, otherlistelem, null);

        }

        /* create a new enumerated type */

         Type createEnumType(Token aRangeValue, Token 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 */

         void addToEnumType(Type aTypeSymbol, Token otherRangeValue, Token anIntegerValue)

        {

                final EnumType anEnum = (EnumType)aTypeSymbol;

                if (anEnum.symbolTable().Defined(otherRangeValue.getText()))

                {

                        doError(otherRangeValue, String.format("Element '%s' already defined!", otherRangeValue.getText()));

                        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...

                 */

                final Identifier sym = pState.Lookup(otherRangeValue);

                if (sym != null)

                {

                        doError(otherRangeValue, String.format("Element '%s' already defined!", otherRangeValue.getText()));

                        return;

                }

                EnumIdentifier enumval;

                if (anIntegerValue == null)

                {

                        if (aTypeSymbol instanceof ValuedEnumType)

                        {

                                doError(otherRangeValue, String.format("Element '%s' needs integer value!", otherRangeValue.getText()));

                                return;

                        }

                        enumval = new EnumIdentifier(otherRangeValue, (EnumType)aTypeSymbol, GetScope());

                }

                else

                {

                        if (!(aTypeSymbol instanceof ValuedEnumType))

                        {

                                doError(otherRangeValue, String.format("Element '%s' must not have integer value!", otherRangeValue.getText()));

                                return;

                        }

                        enumval = new EnumIdentifier(otherRangeValue, Integer.parseInt(anIntegerValue.getText()), (EnumType)aTypeSymbol, GetScope());

                }

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

                /* add the enum id to 'global' state */

                pState.currentScope.AddIdentifier(enumval, null);

        }

        /* get a named type */

         Type getNamedType(Token aType)

        {

                Type result = null;

                final 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: " + aType.getText());

                return result;

        }

        /* create a list type */

         @SuppressWarnings("unchecked")

        Type createListType(Token numOfElements, Type innertype)

        {

                if (innertype == null)

                        doError(numOfElements, "List type lacks proper element type (null)");

                int numElems = 0;

                if (numOfElements.getType() == ooaLexer.T_IDENTIFIER)

                {

                        // see whether we can find the constant

                        final Identifier aconst = pState.currentScope.ResolveIdentifier(numOfElements.getText());

                        if (aconst == null || aconst.kind() != IdentifierKind.Constant)

                                doError(numOfElements, String.format("Constant %s not found", numOfElements.getText()));

                        else if (aconst.type().kind() != TypeKind.IntType)

                                doError(numOfElements, "Constant must be integer");

                        else

                                numElems = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

                }

                else

                {

                        try {

                                numElems = Integer.parseInt(numOfElements.getText());

                        } catch (final NumberFormatException e) {

                                doError(numOfElements, "Not an integer");

                        }

                        if (numElems <= 0)

                                doError(numOfElements, "Number of elements in a list must be >= 1");

                }

                final ListType result = new ListType(innertype, numElems, null);

                return result;

        }

        /* create a map type */

         @SuppressWarnings("unchecked")

        Type createMapType(Token numOfElements, Type mapfromtype, Type 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.getType() == ooaLexer.T_IDENTIFIER)

                {

                        // see whether we can find the constant

                        final Identifier aconst = pState.currentScope.ResolveIdentifier(numOfElements.getText());

                        if (aconst == null || aconst.kind() != IdentifierKind.Constant)

                                doError(numOfElements, String.format("Constant %s not found", numOfElements.getText()));

                        else if (aconst.type().kind() != TypeKind.IntType)

                                doError(numOfElements, "Constant must be integer");

                        else

                                max = ((ValueExpression<Integer>)((ConstantIdentifier)aconst).Value()).value();

                }

                else

                        try {

                                max = Integer.parseInt(numOfElements.getText());

                        } catch (final NumberFormatException e) {

                                doError(numOfElements, "Not an integer");

                        }

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

                return result;

        }

        /* create a tuple type */

         Type createTupleType(Type aType)

        {

                final TupleType result = new TupleType(null);

                addToTupleType(result, aType);

                return result;

        }

        /* add inner type to tuple */

         void addToTupleType(Type aTypeSymbol, Type anotherType)

        {

                final TupleType tuple = (TupleType)aTypeSymbol;

                if (anotherType != null)

                        tuple.AddType(anotherType);

                else

                        doError("Unknown inner type in tuple");

        }

        /* gets called after a simple type has been constructed. used to define an internal name*/

         void fixupSimpleType(Type aTypeSymbol)

        {

                if (aTypeSymbol != null)

                        aTypeSymbol.SetupAnonymousName();

        }

        /* gets called after a simple or complex type has been constructed. used to define an internal name */

         void fixupComplexType(Type aTypeSymbol)

        {

                if (aTypeSymbol != null)

                        aTypeSymbol.SetupAnonymousName();

        }

        /* create a method symbol */

         FunctionIdentifier createMethodSymbol(Token mname)

        {

                final Identifier sym = pState.Lookup(mname);

                if (sym != null)

                {

                        doError(mname, String.format("Redefinition of %s", mname.getText()));

                        return null;

                }

                final FunctionType funtype = new FunctionType(FunctionTypeEnum.Method, new LinkedList<Type>(), null);

                final MethodIdentifier msym = new MethodIdentifier(mname, funtype, GetScope());

                // funtype.SetTypeIdentifier(msym); -- the type of this function doesn't have a name!

                pState.currentScope.AddIdentifier(msym, null);

                pState.PushResolveStack(msym);

                return msym;

        }

        /* remove local method symbols from resolution stack again */

        protected void popResolveStack(FunctionIdentifier newMethod)

        {

                if (newMethod != null)

                        pState.PopResolveStack();

        }

        /* add a return type to a method */

         void setMethodReturnType(FunctionIdentifier newMethod, Type rt)

        {

                if (newMethod == null)

                        return;

                if (rt == null)

                        doError(String.format("Method %s 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 %s defines 'result'", newMethod.tokenText()));

                        return;

                }

                final ParameterIdentifier returnval = new ParameterIdentifier("result", rt, GetScope());

                newMethod.symbolTable().AddIdentifier(returnval);

        }

        /* add a parameter to a method */

         void addMethodParameter(FunctionIdentifier newMethod, Token paramName, Type atype)

        {

                if (newMethod == null)

                        return;

                if (atype == null)

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

                if (newMethod.symbolTable().Defined(paramName.getText()) == true)

                {

                        doError(paramName, String.format("Parameter '%s' already defined", paramName.getText()));

                        return;

                }

                // add parameter to scope

                final ParameterIdentifier param = new ParameterIdentifier(paramName, atype, GetScope());

                newMethod.AddParameter(param);

                // add type of param to signature

                final FunctionType ftype = (FunctionType)newMethod.type();

                ftype.AddParameterType(atype);

        }

        /* set method body of a method */

         void addMethodBody(FunctionIdentifier newMethod, Block statements)

        {

                if (newMethod == null)

                        return;

                if (statements == null)

                        doError(String.format("%s has empty body (null)",

                                        ((FunctionType)newMethod.type()).functionType() == FunctionTypeEnum.Method ? "Method" : "Action"));

                newMethod.SetBody(statements);

        }

        /* create a continuous action */

         FunctionIdentifier createNamedContinuousAction(Token cactionname, FunctionTypeEnum actionTypeEnum)

        {

                return createNamedAction(cactionname, actionTypeEnum);

        }

        /* create a named action */

         FunctionIdentifier createNamedAction(Token actionname, FunctionTypeEnum actionType)

        {

                final Identifier sym = pState.Lookup(actionname);

                if (sym != null)

                {

                        doError(actionname, String.format("Symbol '%s' already defined.", sym.tokenText()));

                        return null;

                }

                final FunctionType atype = new FunctionType(actionType, new LinkedList<Type>(), null);

                final NamedActionIdentifier action = new NamedActionIdentifier(actionname, atype, GetScope());

                // atype.SetTypeIdentifier(action); -- the type of this action doesn't have a name!

                pState.currentScope.AddIdentifier(action, null);

                pState.PushResolveStack(action);

                return action;

        }

        /* add body of action */

         void addActionBody(FunctionIdentifier newAction, GuardedCommand body)

        {

                // we need a wrapper around the guarded command..

                final Block bdy = new SeqBlock(currentLine(), currentPos());

                addMethodBody(newAction, bdy);

                body.SetParentScope(bdy);

                bdy.AddStatement(body);

        }

        /* add constraints of cont. action */

         void addContinuousActionBody(FunctionIdentifier newAction, GuardedCommand constraints)

        {

                final Block bdy = new SeqBlock(currentLine(), currentPos());

                bdy.AddStatement(constraints);

                addMethodBody(newAction, bdy);

        }

        /* create a guarded command */

         GuardedCommand createGuardedCommandStatement()

         {

                 return new GuardedCommand(null, null, currentLine(), currentPos());

         }

         void addExprAndBlockToGuardedCommand(GuardedCommand cmd, Expression expr, Block bdy)

        {

                if (bdy == null)

                        doError("Guarded command without body (null)!");

                if (expr == null)

                        doError("Guarded command without guard (null)!");

                cmd.SetGuard(expr);

                cmd.SetBody(bdy);

        }

         GuardedCommand createGuardedCommandStatement(Expression expr, Block bdy, boolean isQualitative)

        {

                final GuardedCommand result = createGuardedCommandStatement();

                addExprAndBlockToGuardedCommand(result, expr, bdy);

                result.SetIsQualitative(isQualitative);

                return result;

        }

        /* add statements to list */

         void addToStatementList(Block top, Statement stmt)

        {

                if (stmt == null)

                        doError("Can not add statement: null!");

                top.AddStatement(stmt);

        }

        /* create a Kill statement */

         Statement createKillStatement(Token aname)

        {

                final Identifier sym = pState.Lookup(aname);

                if (sym == null)

                        doError(aname, "Not defined");

                final KillStatement result = new KillStatement(sym, aname.getLine(), aname.getCharPositionInLine());

                return result;

        }

        /* create a Skip statement */

         Statement createSkipStatement()

        {

                return new SkipStatement(currentLine(), currentPos());

        }

        /* create a Break statement */

         Statement createBreakStatement()

        {

                return new BreakStatement(currentLine(), currentPos());

        }

        /* create an Abort statement */

         Statement createAbortStatement()

        {

                return new AbortStatement(currentLine(), currentPos());

        }

        /* creates a prioritized composition block */

         Block createPrioBlock(Block top)

        {

                return new PrioBlock(top, currentLine(), currentPos());

        }

        /* creates a nondeterministically composed block */

         Block createNondetBlock(Block top)

        {

                return new NondetBlock(top, currentLine(), currentPos());

        }

        /* creates a sequentially composed block */

         SeqBlock createSeqBlock(Block top)

        {

                return new SeqBlock(top, currentLine(), currentPos());

        }

        /* adds a filter expression to seq block */

        protected void addSeqBlockExpression(Block seqList, Expression sexpr)

        {

                seqList.SetFilter(sexpr); /*gets transformed to guarded command in resolvevisitor!*/

        }

        /* create a self identifier */

         IdentifierExpression createSelfIdentifierExpression(Token self)

        {

                final Identifier id = pState.Lookup("self");

                if (id == null)

                {

                        doError(self, "Can not resolve 'self'");

                        return null;

                }

                final IdentifierExpression result = new IdentifierExpression(id, self.getLine(), self.getCharPositionInLine());

                result.setIsSelf(true);

                return result;

        }

        /* build up identifier tree... */

         Expression createIdentifierAccessExpression(IdentifierExpression aself, Token token)

        {

                final Identifier someid = pState.Lookup(token.getText(), GetScope());

                final Identifier self = pState.Lookup("self");

                if (someid != null)

                {

                        switch (someid.kind())

                        {

                        /* all method and attribute accesses are prefixed by self */

                        case AttributeIdentifier:

                        case MethodIdentifier:

                                if (self == null)

                                        doError(token, "Self access of method: Can not find 'self' symbol! (internal error)");

                                aself = new IdentifierExpression(self, token.getLine(), token.getCharPositionInLine());

                                aself.setIsSelf(true);

                                break;

                        default:

                                break;

                        }

                }

                final IdentifierExpression ident = new UnresolvedIdentifierExpression(token, GetScope());

                if (aself != null)

                        return new AccessExpression(aself, ident, token.getLine(), token.getCharPositionInLine());

                else

                        return ident;

        }

         AccessExpression addIdentifierAccessExpression(Expression parent, Token token)

        {

                final IdentifierExpression ident = new UnresolvedIdentifierExpression(token, GetScope());

                return new AccessExpression(parent, ident, token.getLine(), token.getCharPositionInLine());

        }

        /* we have a primed id; prime the complete subtree.. */

        Expression setIdentifierExpressionPrimed(Expression oldExpr, Token token)

        {

                return new UnaryOperator(ExpressionKind.Primed, oldExpr, token.getLine(), token.getCharPositionInLine());

        }

        /* create a fold operation */

         Expression createFoldExpression(Expression result, Token afold, Expression initval, Expression anexpr)

        {

                ExpressionKind akind = ExpressionKind.foldLR;

                if (afold.getType() == ooaLexer.T_FOLDLR)

                        akind = ExpressionKind.foldLR;

                else if (afold.getType() == ooaLexer.T_FOLDRL)

                        akind = ExpressionKind.foldRL;

                else

                        assert(false);

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

                return op;

        }

        /* create a method access */

         CallExpression createMethodAccessExpression(Expression subexpr, List<Expression> m_params, Token token)

        {

                assert(subexpr != null);

                return new CallExpression(subexpr, m_params, token.getLine(), token.getCharPositionInLine(), GetScope());

        }

        /* create a tuple or map access */

         TupleMapAccessExpression createTupleMapAccessExpression(Expression subexpr, Expression ac, Token token)

        {

                assert(subexpr != null);

                return new TupleMapAccessExpression(subexpr, ac, token.getLine(), token.getCharPositionInLine());

        }

        /* create a method call statement; has to be resolved in a second run */

         Statement createCallStatement(Expression aqname)

        {

                return new Call(aqname, currentLine(), currentPos());

        }

        /* create a single assignment statement */

         Statement createSingleAssignmentStatement(Expression aqname, Expression aexp)

        {

                final Assignment result = new Assignment(aqname, aexp, null, currentLine(), currentPos());

                return result;

        }

        /* create a multi-assignment statement; has to be resolved in a second run */

         Statement createMultipleAssignmentStatementLHS(Expression aqname)

        {

                return new Assignment(aqname, null, null, currentLine(), currentPos());

        }

        /* adds an expression to the multi-assign */

         void addMutlipleAssignmentStatementRHS(Statement result, Expression mexp)

        {

                ((Assignment)result).AddValue(mexp);

        }

        /* adds a LHS-var to the multi assign */

         void addMultipleAssignmentStatementLHS(Statement result, Expression malhs)

        {

                ((Assignment)result).AddPlace(malhs);

        }

        /* pop an assignment statement from the resolve stack */

         void popAssignmentOffResolveStack(Statement result)

        {

                assert(result == pState.currentScope); // ref eq.

                pState.PopResolveStack();

        }

        /* pushes the assignment statement onto resolve stack. */

         void pushAssignmentOnResolveStack(Statement result)

        {

                assert(result instanceof Assignment);

                pState.PushResolveStack((Assignment)result);

        }

        /* adds a nondet-assignment constraint */

         void addConstraintToAssignment(Statement result, Expression ndexp)

        {

                ((Assignment)result).SetNondetExpression(ndexp);

        }

        /* add a named action call to do-od block */

         void addNamedActionCallToBlockList(Block top, Token aname, List<Expression> m_params, Token maptoken, Expression amapexpression)

        {

                final Identifier id = pState.Lookup(aname);

                if (id == null)

                {

                        doError(aname, String.format("Could not find named action '%s'", aname.getText()));

                        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.getLine(), aname.getCharPositionInLine());

            aself.setIsSelf(true);

            callexpr = new CallExpression(

                new AccessExpression(aself,

                    new IdentifierExpression(id, aname.getLine(), aname.getCharPositionInLine()), aname.getLine(), aname.getCharPositionInLine()),

                    m_params, aname.getLine(), aname.getCharPositionInLine(), GetScope());

                         */

                }

                else

                        callexpr = new CallExpression(

                                        new IdentifierExpression(id, aname.getLine(), aname.getCharPositionInLine()),

                                        m_params, aname.getLine(), aname.getCharPositionInLine(), GetScope());

                if (amapexpression != null)

                {

                        ExpressionKind akind = ExpressionKind.foldLR;

                        if (maptoken.getType() == ooaLexer.T_FOLDLR)

                                akind = ExpressionKind.foldLR;

                        else if (maptoken.getType() == ooaLexer.T_FOLDRL)

                                akind = ExpressionKind.foldRL;

                        else

                                assert(false);

                        callexpr = new TernaryOperator(akind, callexpr, null, amapexpression,

                                        currentLine(), currentPos(), GetScope());

                }

                final Call statement = new Call(callexpr, currentLine(), currentPos());

                top.AddStatement(statement);

        }

        /*adds skip statement instead of call to do-od block*/

         void addSkipStatementToBlockList(Block top)

        {

                top.AddStatement(new SkipStatement(currentLine(), currentPos()));

        }

        /* add anonymous action to do-od block */

         void addToBlockList(Block top, Statement gcmd)

        {

                if (gcmd != null)

                        top.AddStatement(gcmd);

        }

        /* add the do-od block to the action system type */

         void addActionBlock(OoActionSystemType aTypeSymbol, Block bl)

        {

                aTypeSymbol.SetDoOdBlock(bl);

        }

        /* push block */

         void pushBlockToResolveStack(IScope toPush)

        {

                pState.PushResolveStack(toPush);

        }

        /* pop block */

         void popBlockFromResolveStack(IScope toPop)

        {

                if (toPop != null)

                {

                        assert(pState.currentScope == toPop); // ref eq.

                        pState.PopResolveStack();

                }

        }

        /* add block var */

         void addBlockVariable(Block seqList, Token varname, Type aType)

        {

                if (aType == null)

                {

                        doError(varname, String.format("%s lacks type!", varname.getText()));

                }

                try

                {

                        seqList.AddIdentifier(new LocalVariableIdentifier(varname, aType, GetScope()));

                }

                catch (final ArgumentException e)

                {

                        doError(varname, String.format("%s redefined!", varname.getText()));

                }

        }

        /* creates a general binary operator without any children */

         BinaryOperator createBinaryOperator(ExpressionKind akind)

        {

                final Token token = input.LT(-1);

                return new BinaryOperator(akind, null, null, token.getLine(), token.getCharPositionInLine());

        }

        /* creates a general unary operator without child */

         UnaryOperator createUnaryOperator(ExpressionKind unaryOperatorType)

        {

                final Token token = input.LT(-1);

                return new UnaryOperator(unaryOperatorType, null, token.getLine(), token.getCharPositionInLine());

        }

        /* create a conditional expression */

         Expression createConditionalExpression(Expression ce, Expression te, Expression ee, Token ef)

        {

                return new TernaryOperator(ExpressionKind.conditional, ce, te, ee, ef.getLine(), ef.getCharPositionInLine(), GetScope());

        }

        /* create a quantifier expression */

         Quantifier createQuantifierExpression(Token t)

        {

                Quantifier result = null;

                if (t.getType() == ooaLexer.T_FORALL)

                        result = new ForallQuantifier(null, t.getLine(), t.getCharPositionInLine());

                else