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

import java.util.ArrayList;

import java.util.Iterator;

import java.util.LinkedList;

import java.util.Stack;

import org.momut.ooas.ast.AstNodeTypeEnum;

import org.momut.ooas.ast.IAst;

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

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

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.expressions.LeafExpression.LeafTypeEnum;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

import org.momut.ooas.parser.ParserError;

import org.momut.ooas.parser.ParserMessage;

import org.momut.ooas.parser.ParserState;

import org.momut.ooas.parser.ParserWarning;

import org.momut.ooas.parser.SymbolTable;

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

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

/// <summary>

/// Requires: ReplaceOpaqueVisitor

///

/// After we have an AST without any Opaquetypes, we still need to replace all the

/// UnresolvedIdentifierExpressions. We also need to compute the expression types,

/// which is also necessary to resolve all the identifiers. So, this visitor

/// goes over all expressions and

///   - resolves all identifiers

///   - calculates resulting types (incl. coercion)

/// </summary>

public final class OoaResolveExpressionsVisitor extends OoaCompleteAstTraversalVisitor

{

        // we allow for free variable in expressions. collect them here.

        private final Stack<SymbolTable> m_freeVariables = new Stack<SymbolTable>();

        private Expression m_entryExpression = null;

        // helpers that replace the old expression in the AST by the new one.

        private void ReplaceExpression(IAst parent, Expression subElement, Expression newExpression)

        {

                switch (parent.nodeType())

                {

                        case identifier:

                                ReplaceExpressionInIdentifier((Identifier)parent, subElement, newExpression);

                                break;

                        case statement:

                                ReplaceExpressionInStatement((Statement)parent, subElement, newExpression);

                                break;

                        default:

                                throw new NotImplementedException();

                }

        }

        private void ReplaceExpressionInIdentifier(Identifier identifier, Expression subElement, Expression newExpression)

        {

                switch (identifier.kind())

                {

                        case AttributeIdentifier:

                                final AttributeIdentifier ident = (AttributeIdentifier)identifier;

                                assert(ident.initializer() == subElement); // ref equ.

                                ident.SetInitializer(newExpression);

                                break;

                        case Constant:

                                final ConstantIdentifier aconst = (ConstantIdentifier)identifier;

                                assert(aconst.Value() == subElement); // ref equ

                                aconst.SetValue(newExpression);

                                if (newExpression.kind() != ExpressionKind.Value)

                                        Error(aconst.Value(), String.format("%s not a constant!", aconst.tokenText()));

                                break;

                        default:

                                throw new NotImplementedException();

                }

        }

        private void ReplaceExpressionInStatement(Statement statement, Expression subElement, Expression newExpression)

        {

                switch (statement.kind())

                {

                        case GuardedCommand:

                                final GuardedCommand gc = (GuardedCommand)statement;

                                assert(gc.guard() == subElement); // ref eq

                                gc.SetGuard(newExpression);

                        break;

                        case SeqBlock:

                                final SeqBlock sqblock = (SeqBlock)statement;

                                assert(sqblock.filter() == subElement); // ref eq

                                sqblock.SetFilter(null);

                                // we convert the filter to a guarded command...

                                final SeqBlock implseq = new SeqBlock(sqblock.line(), sqblock.pos());

                                implseq.SetStatements(sqblock.statements());

                                final GuardedCommand implguard = new GuardedCommand(newExpression, implseq, sqblock.line(), sqblock.pos());

                                sqblock.SetStatements(new LinkedList<Statement>());

                                sqblock.AddStatement(implguard);

                                break;

                        case Assignment:

                                final Assignment zw = (Assignment)statement;

                                boolean found = false;

                                if (zw.nondetExpression() == subElement) // ref eq

                                {

                                        zw.SetNondetExpression(newExpression);

                                        found = true;

                                }

                                else

                                {

                                        int cntr = 0;

                                        while (cntr < zw.places().size()) {

                                                if (zw.places().get(cntr) == subElement) { // ref eq

                                                        zw.places().set(cntr, newExpression);

                                                        found = true;

                                                        break;

                                                }

                                                cntr ++;

                                        }

                                        if (!found) {

                                                cntr = 0;

                                                while (cntr < zw.values().size()) {

                                                        if (zw.values().get(cntr) == subElement) { // ref eq.

                                                                zw.values().set(cntr, newExpression);

                                                                found = true;

                                                                break;

                                                        }

                                                        cntr ++;

                                                }

                                        }

                                }

                                assert(found);

                                break;

                        case MethodCall:

                                final Call call = (Call)statement;

                                assert(call.callExpression() == subElement); // ref eq.

                                call.SetCallExpression(newExpression);

                                break;

                        default:

                                throw new NotImplementedException();

                }

        }

        // helper that returns null and adds an error message in the parserstate errorlist.

        private Expression Error(Expression expression, String p)

        {

                final ParserError error = new ParserError(m_ParserState.filename,

                                expression.line(), expression.pos(), p);

                m_ParserState.AddErrorMessage(error);

                return null;

        }

        private void Info(Expression expression, String p)

        {

                final ParserMessage msg = new ParserMessage(m_ParserState.filename,

                                expression.line(), expression.pos(), p);

                m_ParserState.AddMessage(msg);

        }

        // helper that adds a warning message to the output

        private void Warning(Identifier expression, String p)

        {

                final ParserWarning warning = new ParserWarning(m_ParserState.filename,

                                expression.line(), expression.column(), p);

                m_ParserState.AddWarningMessage(warning);

        }

        private void Warning(Expression expression, String p)

        {

                final ParserWarning warning = new ParserWarning(m_ParserState.filename,

                                expression.line(), expression.pos(), p);

                m_ParserState.AddWarningMessage(warning);

        }

        private final ArrayList<TupleConstructor> m_matcherList = new ArrayList<TupleConstructor>();

        ///

        ///   Resolve Expressions

        ///

        private Expression ResolveExpression(TernaryOperator expression)

        {

                if (expression.kind() == ExpressionKind.conditional)

                {

                        final Expression left = ResolveExpression(expression.left());

                        Expression mid = ResolveExpression(expression.mid());

                        Expression right = ResolveExpression(expression.right());

                        if (left == null || mid == null || right == null)

                                return null;

                        if (left.type() == null || left.type().kind() != TypeKind.BoolType)

                                return Error(expression, "Conditional: Condition not a bool");

                        if (mid.type() == null || right.type() == null)

                                return Error(expression, "Conditional: Then or Else branch has void-type");

                        final UlyssesType acover = UlyssesType.CoverType(mid.type(), right.type());

                        if (acover == null)

                                return Error(expression, String.format(

                                        "Conditional: Then and Else branch must be of same type. (%s <> %s)",

                                        mid.type().toString(), right.type().toString()));

                        if (!UlyssesType.TypeEqual(acover, mid.type()))

                        {

                                mid = new UnaryOperator(ExpressionKind.Cast, mid, mid.line(), mid.pos());

                                mid.SetType(acover);

                        }

                        if (!UlyssesType.TypeEqual(acover, right.type()))

                        {

                                right = new UnaryOperator(ExpressionKind.Cast, right, right.line(), right.pos());

                                right.SetType(acover);

                        }

                        expression.SetLeftChild(left);

                        expression.SetMidChild(mid);

                        expression.SetRightChild(right);

                        expression.SetType(mid.type());

                        return expression;

                }

                else if (expression.kind() == ExpressionKind.foldLR || expression.kind() == ExpressionKind.foldRL)

                {

                        CallExpression leftcall = expression.left().kind() != ExpressionKind.Call

                                ? new CallExpression(expression.left(), new ArrayList<Expression>(), expression.line(),

                                        expression.pos(), expression.definingScope())

                                : (CallExpression)expression.left();

                        leftcall = (CallExpression)ResolveExpression(leftcall, true);

                        if (leftcall == null)

                                return null;

                        final Expression afun = ResolveExpression(leftcall.child());

                        leftcall.SetChild(afun);

                        if (afun == null || afun.type() == null || afun.type().kind() != TypeKind.FunctionType)

                                return Error(expression, "Fold/Map operation needs a method or named action as LHS");

                        final FunctionType funType = (FunctionType)afun.type();

                        if (funType.returnType() == null && expression.mid() != null)

                                return Error(expression, "Fold operation needs a method with matching return type");

                        if (funType.returnType() != null && expression.mid() == null)

                                Warning(expression, "Map operation will discard result of function");

                        final boolean isMap = expression.mid() == null;

                        Expression mid = expression.mid();

                        if (!isMap)

                        {

                                mid = ResolveExpression(mid);

                                if ((funType.parameter().size() - leftcall.arguments().size()) != 2)

                                        return Error(expression, "Function used in fold operation needs 2 not-instantiated parameters");

                        } else if ((funType.parameter().size() - leftcall.arguments().size()) != 1)

                                return Error(expression, "Function used in map operation needs one not-instantiated parameter");

                        final Expression right = ResolveExpression(expression.right());

                        if (right == null || right.type() == null || right.type().kind() != TypeKind.ListType)

                                return Error(expression, "Fold/Map operation needs list as RHS");

                        if (!isMap)

                        {

                                final int nextToLast = funType.parameter().size() - 2;

                                final UlyssesType initCover = UlyssesType.CoverType(funType.parameter().get(nextToLast), mid.type());

                                if (initCover == null)

                                        return Error(expression, "Next to last parameter does not match initializer type in map operation.");

                                if (!UlyssesType.TypeEqual(mid.type(), initCover))

                                        mid = new UnaryOperator(ExpressionKind.Cast, mid, mid.line(), mid.pos());

                                mid.SetType(initCover);

                                //List<Expression> args = new List<Expression> ();

                                leftcall.arguments().add(new IdentifierExpression(new ParameterIdentifier("_result", initCover, null), 0, 0));

                                leftcall.arguments().add(new IdentifierExpression(new ParameterIdentifier("_elem", funType.parameter().peekLast(), null), 0, 0));

                                //leftcall.SetArguments(args);

                        }

                        // UlyssesType listCover = UlyssesType.CoverType(funType.parameter.Last.Value, ((ListType)right.type).innerType);

                        // if (listCover == null)

                        if (!UlyssesType.TypeEqual(funType.parameter().peekLast(), ((ListType)right.type()).innerType()))

                                return Error(expression, "Last paramter does not match inner-type of list in fold/map operation");

                        expression.SetLeftChild(leftcall);

                        expression.SetMidChild(mid);

                        expression.SetRightChild(right);

                        if (!isMap)

                                expression.SetType(funType.returnType());

                        else

                                expression.SetType(new NullType());

                        return expression;

                } else

                        throw new ArgumentException();

        }

        private Expression ResolveExpression(ForallQuantifier expression)

        {

                final Expression child = ResolveExpression(expression.child());

                if (child == null)

                        return null;

                expression.SetType(new BoolType(null));

                expression.SetChild(child);

                return expression;

        }

        private Expression ResolveExpression(ExistsQuantifier expression)

        {

                final Expression child = ResolveExpression(expression.child());

                if (child == null)

                        return null;

                expression.SetType(new BoolType(null));

                expression.SetChild(child);

                return expression;

        }

        private Expression ResolveExpression(ListConstructor expression)

        {

                UlyssesType type = null;

                ListType restype = null;

                Expression comprehension = null;

                if (expression.comprehension() != null)

                {

                        comprehension = ResolveExpressionNewScope(expression.comprehension());

                        if (comprehension == null)

                                return null;

                        if (comprehension.type() == null)

                                return Error(expression, "List comprehension has void expression");

                        if (comprehension.type().kind() != TypeKind.BoolType)

                                return Error(expression, "List comprehension has to be bool-expression");

                        expression.SetComprehension(comprehension);

                        if (expression.elements().size() != 1)

                                return Error(expression, "List comprehension expects one initializer expression");

                }

                final ArrayList<Expression> newitems = new ArrayList<Expression>();

                if (expression.elements().size() == 0 || expression.elements().get(0) == null || (

                        expression.elements().get(0).kind() == ExpressionKind.Value &&

                        expression.elements().get(0) instanceof ValueExpression<?> &&

                        ((ValueExpression<?>)expression.elements().get(0)).value() == null))

                {

                        // empty list

                        type = new NullType();

                }

                else

                {

                        final ArrayList<Expression> tmpitems = new ArrayList<Expression>();

                        for (final Expression item: expression.elements())

                        {

                                final Expression element = ResolveExpression(item);

                                if (element == null)

                                        return null;

                                if (element.type() == null)

                                        return Error(expression, "Void expression in list initializer");

                                if (element.kind() == ExpressionKind.Value &&

                                    element instanceof ValueExpression<?> &&

                                    ((ValueExpression<?>)element).value() == null)

                                {

                                        return Error(expression, "Not-In-List (nil) values not allowed in a list");

                                }

                                // calculate the type we're constructing

                                if (type == null)

                                        type = element.type();

                                type = UlyssesType.CoverType(type, element.type());

                                if (type == null)

                                        return Error(expression, "List constructor needs matching types");

                                tmpitems.add(element);

                        }

                        // now we have the resulting type - we still need to insert casts that might be necessary

                        for (final Expression item: tmpitems)

                        {

                                if (!UlyssesType.TypeEqual(item.type(), type))

                                {

                                        final Expression cast = new UnaryOperator(ExpressionKind.Cast, item, item.line(), item.pos());

                                        cast.SetType(type);

                                        newitems.add(cast);

                                }

                                else

                                        newitems.add(item);

                        }

                }

                expression.SetElements(newitems);

                if (comprehension == null)

                        restype = new ListType(type, newitems.size(), null);

                else

                        restype = new ListType(type, -1, null); // we do not know anything about the bound

                expression.SetType(restype);

                return expression;

        }

        private Expression ResolveExpression(SetConstructor expression)

        {

                UlyssesType type = null;

                ListType restype = null;

                Expression comprehension = null;

                if (expression.comprehension() != null)

                {

                        comprehension = ResolveExpressionNewScope(expression.comprehension());

                        if (comprehension == null)

                                return null;

                        if (comprehension.type() == null)

                                return Error(expression, "Set comprehension has void expression");

                        if (comprehension.type().kind() != TypeKind.BoolType)

                                return Error(expression, "Set comprehension has to be bool-expression");

                        expression.SetComprehension(comprehension);

                        if (expression.items().size() != 1)

                                return Error(expression, "Set comprehension expects one initializer expression");

                }

                final ArrayList<Expression> newitems = new ArrayList<Expression>();

                for (final Expression item: expression.items())

                {

                        final Expression element = ResolveExpression(item);

                        if (element == null)

                                return null;

                        if (element.type() == null)

                                return Error(expression, "Void expression in set initializer");

                        if (type == null)

                                type = element.type();

                        type = UlyssesType.CoverType(type, element.type());

                        if (type == null)

                                return Error(expression, "Set initializer needs matching types");

                        newitems.add(element);

                }

                expression.SetItems(newitems);

                restype = new ListType(type, newitems.size(), null);

                expression.SetType(restype);

                return expression;

        }

        private Expression ResolveExpression(MapConstructor expression)

        {

                UlyssesType domain = null;

                UlyssesType range = null;

                final ArrayList<MapConstructor.MapItem> newitems = new ArrayList<MapConstructor.MapItem>();

                for(final MapItem item: expression.items())

                {

                        final Expression domexpr = ResolveExpression(item.key);

                        if (domexpr == null)

                                return null;

                        if (domexpr.type() == null)

                                return Error(expression, "Domain initializing expression void");

                        if (domain == null)

                                domain = domexpr.type();

                        final Expression rangeexpr = ResolveExpression(item.value);

                        if (rangeexpr == null)

                                return null;

                        if (rangeexpr.type() == null)

                                return Error(expression, "Range initializing expression void");

                        if (range == null)

                                range = rangeexpr.type();

                        domain = UlyssesType.CoverType(domain, domexpr.type());

                        range = UlyssesType.CoverType(range, rangeexpr.type());

                        if (domain == null)

                                return Error(expression, "Types of domain expressions do not match");

                        if (range == null)

                                return Error(expression, "Types of range expressions do not match");

                        newitems.add(new MapConstructor.MapItem(domexpr, rangeexpr));

                }

                expression.SetItems(newitems);

                final MapType resulttype = new MapType(domain, range, newitems.size(), null);

                expression.SetType(resulttype);

                return expression;

        }

        private Expression ResolveExpression(TupleConstructor expression)

        {

                final TupleType typeToConstruct = (TupleType)expression.tupleType().type();

                if (expression.values().size() != typeToConstruct.innerTypes().size())

                        return Error(expression, String.format("Tuple constructor has wrong arity. (%s <> %s)",

                                typeToConstruct.innerTypes().size(), expression.values().size()));

                //TupleType resulttype = new TupleType(null);

                final ArrayList<Expression> newvalexprs = new ArrayList<Expression>();

                final Iterator<UlyssesType> innerTargetType = typeToConstruct.innerTypes().iterator();

                int freeVarCount = 0;

                for (final Expression initexpr: expression.values())

                {

                        final UlyssesType innerTargetTypeValue = innerTargetType.next();

                        Expression newval = ResolveExpression(initexpr);

                        if (newval == null)

                                return null;

                        if (newval.type() == null)

                                return Error(expression, "Element has void type");

                        if (newval.type().kind() == TypeKind.Any)

                        {

                                // free var - so set type.

                                final AnyType freevar = (AnyType)newval.type();

                                freevar.VariableIdentifier().SetType(innerTargetTypeValue);

                                freevar.VariableIdentifier().SetInitialized(true);

                                freeVarCount++;

                        }

                        else

                        {

                                final UlyssesType acover = UlyssesType.CoverType(innerTargetTypeValue, newval.type());

                                if (acover == null || !UlyssesType.TypeEqualByKind(innerTargetTypeValue, acover))

                                        return Error(expression,

                                                String.format("Element in tuple constructor has non-matching type (%s <> %s)",

                                                                innerTargetTypeValue.toString(), newval.type().toString()));

                                if (!UlyssesType.TypeEqual(acover, newval.type()))

                                {

                                        newval = new UnaryOperator(ExpressionKind.Cast, newval, newval.line(), newval.pos());

                                        newval.SetType(acover);

                                }

                                if (UlyssesType.FirstTypeLessRange(innerTargetTypeValue, acover)) {

                                        Warning(expression,

                                                String.format("Tuple constructor may over/underflow: %s := %s",

                                                                innerTargetTypeValue.toString(), acover.toString()));

                                        newval = new UnaryOperator(ExpressionKind.Cast, newval, newval.line(), newval.pos());

                                        newval.SetType(innerTargetTypeValue);

                                }

                        }

                        newvalexprs.add(newval);

                        //resulttype.AddType(newval.type);

                }

                if (freeVarCount > 0)

                {

                        if (freeVarCount != expression.values().size())

                                return Error(expression, String.format("Tuple constructor must have 0 or #elems (%s) free variables", expression.values().size()));

                        else

                        {

                                expression.SetIsMatcher(true); // mark this tuple constructor as matcher, since this is the only thing it does..

                                m_matcherList.add(expression); // matcher has to be bound by one equality

                        }

                }

                expression.SetTupleValues(newvalexprs);

                //expression.SetType(resulttype);

                expression.SetType(typeToConstruct); // the constructor always will create the correct type!

                return expression;

        }

        private Expression ResolveExpression(QValConstructor expression)

        {

                Expression basevalue = null;

                Expression rangevalue = null;

                basevalue = ResolveExpression(expression.value()[0]);

                if (basevalue == null || basevalue.kind() != ExpressionKind.Access

                    || basevalue.type() == null || basevalue.type().kind() != TypeKind.QrType)

                        return Error(expression, "Landmark expected.");

                expression.SetType(basevalue.type());

                expression.SetValue(basevalue);

                if (expression.value().length == 2)

                {

                        rangevalue = ResolveExpression(expression.value()[1]);

                        if (rangevalue == null || rangevalue.kind() != ExpressionKind.Access

                            || rangevalue.type() == null || rangevalue.type().kind() != TypeKind.QrType)

                                return Error(expression, "Landmark expected.");

                        if (!UlyssesType.TypeEqual(basevalue.type(), rangevalue.type()))

                                return Error(expression, String.format("Quantity spaces do not match: %s <> %s",

                                                basevalue.type().toString(),

                                                rangevalue.type().toString()));

                        expression.AddRange(rangevalue);

                }

                return expression;

        }

        private Expression ResolveExpression(IdentifierExpression expression)

        {

                // nothing to do here, since we do not have any consts that may be

                // folded

                if ((expression.identifier().kind() == IdentifierKind.MethodIdentifier

                       || expression.identifier().kind() == IdentifierKind.NamedActionIdentifier)

                    && !m_entryExpression.callTargets().contains(expression.identifier()))

                {

                        m_entryExpression.callTargets().add((FunctionIdentifier)expression.identifier());

                }

                return expression;

        }

        private Expression ResolveExpression(UnresolvedIdentifierExpression expression)

        {

                Identifier anid;

                //Identifier self = m_ParserState.Lookup("self");

                if (m_freeVariables.peek().Defined(expression.tokenText()))

                        anid = m_freeVariables.peek().Get(expression.tokenText());

                else

                        anid = m_ParserState.Lookup(expression.tokenText(), expression.scope());

                if (anid != null)

                {

                        switch (anid.kind())

                        {

                        case TypeIdentifier:

                                // only return a TypeExpression if this TypeIdentifier didn't come from a "self"

                                if (anid instanceof SelfTypeIdentifier) {

                                        final IdentifierExpression result = new IdentifierExpression(anid, expression.line(), expression.pos());

                                        result.setIsSelf(true);

                                        return result;

                                } else

                                        return new TypeExpression(anid.type(), expression.line(), expression.pos());

                        case MethodIdentifier:

                                m_entryExpression.callTargets().add((FunctionIdentifier)anid);

                                final SelfTypeIdentifier selfid = (SelfTypeIdentifier)m_ParserState.Lookup("self", expression.scope());

                                if ((selfid != null) && ((OoActionSystemType)(selfid).type()).symbols().Defined(anid))

                                {

                                        // if it's a self access, add a self identifier (needed by cadp backend, e.g.)

                                        // self.<method> is handled in a separate method and does not call us here!! (hence this code is working)

                                        final IdentifierExpression aself = new IdentifierExpression(selfid, expression.line(), expression.pos());

                                        aself.setIsSelf(true);

                                        final AccessExpression localaccess = new AccessExpression(aself, new IdentifierExpression(anid, expression.line(), expression.pos()),

                                                        expression.line(), expression.pos());

                                        ResolveExpression(localaccess);

                                        return localaccess;

                                }

                                else

                                {

                                        return new IdentifierExpression(anid, expression.line(), expression.pos());

                                }

                        case NamedActionIdentifier:

                                m_entryExpression.callTargets().add((FunctionIdentifier)anid);

                                return new IdentifierExpression(anid, expression.line(), expression.pos());

                        case Constant:

                                if (((ConstantIdentifier)anid).Value() != null)

                                        return ((ConstantIdentifier)anid).Value().Clone();

                                else

                                        return null;

                        default:

                                return new IdentifierExpression(anid, expression.line(), expression.pos());

                        }

                }

                else

                {

                        final ExpressionVariableIdentifier freeVar =

                                        new ExpressionVariableIdentifier(expression.tokenText(), expression.line(), expression.pos());

                        freeVar.SetType(new AnyType(freeVar));

                        m_freeVariables.peek().AddIdentifier(freeVar);

                        // add a warning about free variables - do not change text without changing the text in ooaTypeCheckVisitor..

                        Warning(freeVar, String.format("Free variable in expression: '%s'.", freeVar.tokenText()));

                        return new IdentifierExpression(freeVar, expression.line(), expression.pos());

                }

        }

        private Expression ResolveExpression(TupleMapAccessExpression expression)

        {

                final Expression child = ResolveExpression(expression.child());

                if (child == null)

                        return null;

                final Expression arg = ResolveExpression(expression.argument());

                if (arg == null)

                        return null;

                assert(child.type() != null);

                if ((child.kind() != ExpressionKind.Type) && (child.type().kind() == TypeKind.TupleType))

                {

                        if ((arg.kind() != ExpressionKind.Value)

                            || (((LeafExpression)arg).valueType() != LeafTypeEnum.integer))

                        {

                                return Error(expression, "Argument to tuple access must be constant integer value!");

                        }

                        final TupleType aTuple = (TupleType)child.type();

                        @SuppressWarnings("unchecked")

                        final

                        ValueExpression<Integer> aval = (ValueExpression<Integer>)arg;

                        if ((aval.value() < 0) || (aval.value() >= aTuple.innerTypes().size()))

                        {

                                return Error(expression, "Argument to tuple access has to be in range 0..#elems-1");

                        }

//                        LinkedListNode<UlyssesType> anode = aTuple.innerTypes().First;

//                        int target = aval.value();

//                        while (target > 0)

//                        {

//                                target--;

//                                anode = anode.Next;

//                        }

//                        expression.SetType(anode.Value);

                        expression.SetType(aTuple.innerTypes().get(aval.value()));

                }

                else if ((child.kind() != ExpressionKind.Type) && (child.type().kind() == TypeKind.MapType))

                {

                        final MapType amap = (MapType)child.type();

                        expression.SetType(amap.toType());

                }

                else if ((child.kind() != ExpressionKind.Type) && (child.type().kind() == TypeKind.ListType))

                {

                        // we allow element access of lists via list[i]

                        final ListType alist = (ListType)child.type();

                        expression.SetType(alist.innerType());

                }

                else

                {

                        return Error(expression, "Not a list, tuple, or map instance");

                }

                expression.SetArgument(arg);

                expression.SetChild(child);

                return expression;

        }

        private Expression ResolveExpression(CallExpression expression)

        {

                return ResolveExpression(expression, false);

        }

        private Expression ResolveExpression(CallExpression expression, boolean allowFewerParameters)

        {

                // calc type of child

                final Expression child = ResolveExpression(expression.child());

                if (child == null)

                        return null;

                assert(child.type() != null);

                expression.SetChild(child);

                if (child.type().kind() != TypeKind.FunctionType)

                {

                        return Error(expression, "No function to call!");

                }

                final FunctionType funtype = (FunctionType)child.type();

//                // check whether call of named action is allowed

//                if (funtype.functionType() != FunctionTypeEnum.Method)

//                {

//                        // see if call is allowed: must not be called from within a named action

//                        IScope callingScope = expression.scope();

//                        while (callingScope != null)

//                        {

//                                if (callingScope instanceof NamedActionIdentifier || callingScope instanceof MethodIdentifier)

//                                        return Error(expression, "Call of named Action only allowed in do-od block!");

//                                callingScope = callingScope.GetParentScope();

//                        }

//                }

                // check arguments

                final int argsSpec = funtype.parameter().size();

                final int argsHave = expression.arguments().size();

                if (argsHave < argsSpec && !allowFewerParameters)

                {

                        return Error(expression, "Too few parameters in function call");

                }

                if (argsHave > argsSpec)

                {

                        return Error(expression, "Too much parameters in function call");

                }

                final ArrayList<Expression> newargs = new ArrayList<Expression>();

                final Iterator<UlyssesType> demandedArgType = funtype.parameter().iterator();

                for (final Expression arg: expression.arguments())

                {

                        final UlyssesType demandedArgTypeValue = demandedArgType.next();

                        Expression newarg = ResolveExpression(arg);

                        if (newarg == null)

                                return null;

                        if (newarg.GetUninitializedFreeVariables().size() > 0)

                                Error(arg, String.format("Undefined variable '%s'",

                                        newarg.GetUninitializedFreeVariables().get(0).tokenText()));

                        final Expression constantvalue = newarg.kind() == ExpressionKind.Value ? newarg : null;

                        final UlyssesType acover = UlyssesType.CoverType(newarg.type(), demandedArgTypeValue);

                        if (acover == null || !UlyssesType.TypeEqualByKind(demandedArgTypeValue, acover))

                                return Error(arg, String.format("Argument type does not match; expected: %s delivered: %s",

                                                demandedArgTypeValue.toString(), newarg.type().toString()));

                        newarg = UnaryOperator.TryCoerceUp(newarg, acover);

                        if (UlyssesType.FirstTypeLessRange(demandedArgTypeValue, acover))

                        {

                                if (constantvalue == null)

                                {

                                        Warning(arg, String.format("Call parameter may over/underflow: %s := %s",

                                                        demandedArgTypeValue.toString(), acover.toString()));

                                        final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, newarg, newarg.line(), newarg.pos());

                                        cast.SetType(demandedArgTypeValue);

                                        newarg = cast;

                                }

                                else

                                {

                                        Error(arg, String.format("Call parameter out of range (%s  := %s)",

                                                        demandedArgTypeValue.toString(), constantvalue.toString()));

                                }

                        }

                        newargs.add(newarg);

                }

                expression.SetArguments(newargs);

                if (funtype.returnType() != null)

                        expression.SetType(funtype.returnType());

                return expression;

        }

        private Expression ResolveExpression(AccessExpression expression)

        {

                Expression lhs = ResolveExpression(expression.left());

                if (lhs == null)

                        return null;

                if (!(expression.right() instanceof UnresolvedIdentifierExpression))

                {

                        expression.SetRightChild(ResolveExpression(expression.right()));

                        expression.SetType(expression.right().type());

                        return expression;

                }

                final boolean selfAccess = (lhs.kind() == ExpressionKind.Identifier) && ((IdentifierExpression)lhs).isSelf();

                final boolean staticAccess = lhs.kind() == ExpressionKind.Type;

                final UnresolvedIdentifierExpression access = (UnresolvedIdentifierExpression)expression.right();

                // atype could be null...

                UlyssesType atype = lhs.type();

                if ((lhs.kind() == ExpressionKind.Call) && (atype == null))

                {

                        return Error(access, "Can not access return type of void-function");

                }

                else if (atype == null)

                {

                        return Error(access, "Can not access member of a void type");

                }

                // if we did not apply a call expression to a function

                if (atype.kind() == TypeKind.FunctionType)

                {

                        // we can access the return val...

                        final FunctionType fun = (FunctionType)atype;

                        // check arity

                        if (fun.parameter().size() > 0)

                                return Error(access, "Implicit function call not possible: Too few parameters.");

                        // check return type

                        if (fun.returnType() == null)

                                return Error(access, "Can not access return type of void-function!");

                        // call ok

                        atype = fun.returnType();

                        // but add callExpression

                        lhs = new CallExpression(lhs, null, lhs.line(), lhs.pos(), null); // we do not know the scope

                        lhs.SetType(atype);

                }

                // update left child

                expression.SetLeftChild(lhs);

                switch (atype.kind())

                {

                case OoActionSystemType:

                        final Identifier anid = ((OoActionSystemType)atype).ResolveIdentifier(access.tokenText());

                        if (anid != null)

                        {

                                if (anid.kind() == IdentifierKind.MethodIdentifier && !m_entryExpression.callTargets().contains(anid))

                                        m_entryExpression.callTargets().add((FunctionIdentifier)anid);

                                if (staticAccess)

                                {

                                        if ((anid.kind() == IdentifierKind.AttributeIdentifier) &&

                                                        (((AttributeIdentifier)anid).isStatic()))

                                        {

                                                final IdentifierExpression newrhs = new IdentifierExpression(anid, access.line(), access.pos());

                                                expression.SetRightChild(newrhs);

                                        }

                                        else

                                                return Error(access, "Can not access non-static member of an action system");

                                }

                                else

                                {

                                        if (anid.kind() != IdentifierKind.MethodIdentifier && !selfAccess)

                                                return Error(access, "Can only access methods of action system objects");

                                        else

                                        {

                                                final IdentifierExpression newrhs = new IdentifierExpression(anid, access.line(), access.pos());

                                                expression.SetRightChild(newrhs);

                                        }

                                }

                        }

                        else

                                return Error(access, String.format("%s no member of %s",

                                                access.tokenText(), ((OoActionSystemType)atype).identifier().tokenText()));

                        break;

                case EnumeratedType:

                        final EnumType anEnum = (EnumType)atype;

                        if (!staticAccess)

                        {

                                return Error(access, "Enum values can only be accessed statically.");

                        }

                        if (anEnum.symbolTable().Defined(access.tokenText()))

                        {

                                final Identifier enumid = anEnum.symbolTable().Get(access.tokenText());

                                final IdentifierExpression newrhs = new IdentifierExpression(enumid, access.line(), access.pos());

                                expression.SetRightChild(newrhs);

                        }

                        else

                                return Error(access, String.format("%s not contained in enum %s",

                                                access.tokenText(), anEnum.identifier().tokenText()));

                        break;

                case QrType:

                        final QrType aQualitativeType = (QrType)atype;

                        if (!staticAccess)

                        {

                                return Error(access, "QSpace values can only be accessed statically.");

                        }

                        if (aQualitativeType.symbolTable().Defined(access.tokenText()))

                        {

                                final Identifier landmark = aQualitativeType.symbolTable().Get(access.tokenText());

                                final IdentifierExpression newrhs = new IdentifierExpression(landmark, access.line(), access.pos());

                                expression.SetRightChild(newrhs);

                        }

                        else

                                return Error(access, String.format("%s not contained in qspace %s",

                                                access.tokenText(), aQualitativeType.identifier().tokenText()));

                        break;

                default:

                        /*error, we can not access an element with '.' in any other type*/

                        return Error(expression, "Expected: System, Enum, Func, or QR type");

                }

                expression.SetType(expression.right().type());

                return expression;

        }

        private Expression ResolveExpression(UnaryOperator expression)

        {

                final Expression child = ResolveExpression(expression.child());

                // if there was some error, then exit

                if (child == null)

                        return null;

                if (child.type() == null)

                        return Error(expression, "Can not apply unary operator to void-expression");

                switch (expression.kind())

                {

                case Primed:

                        expression.SetType(child.type());

                        break;

                        /*map unary*/

                case dom:           // map A to B -> list of A

                        if (child.type().kind() != TypeKind.MapType)

                                return Error(expression, "Domain operator only applicable to map types.");

                        MapType amap = (MapType)child.type();

                        ListType list = new ListType(amap.fromType(), amap.maxNumberOfElements(), null);

                        expression.SetType(list);

                        break;

                case range:         // map A to B -> list of B

                        if (child.type().kind() != TypeKind.MapType)

                                return Error(expression, "Range operator only applicable to map types.");

                        amap = (MapType)child.type();

                        list = new ListType(amap.toType(), amap.maxNumberOfElements(), null);

                        expression.SetType(list);

                        break;

                case merge:         // list of map A to B -> map A to B

                        if ((child.type().kind() == TypeKind.ListType) &&

                                        (((ListType)child.type()).innerType().kind() == TypeKind.MapType))

                        {

                                expression.SetType(((ListType)child.type()).innerType());

                                break;

                        }

                        else

                                return Error(expression, "Merge operator only applicable to a list of maps");

                        /*set/list unary*/

                case card:       // list of A -> int (does not respect dupes, i.e. dupes do not count)

                        if (child.type().kind() != TypeKind.ListType)

                                return Error(expression, "Cardinality operator only applicable to list types.");

                        expression.SetType(new IntType(0, ((ListType)child.type()).maxNumberOfElements(), null));

                        break;

                case dconc:      // list of list of A -> list of A

                        if ((child.type().kind() == TypeKind.ListType)

                                        && (((ListType)child.type()).innerType().kind() == TypeKind.ListType))

                        {

                                list = (ListType)child.type();

                                final ListType innerlist = (ListType)list.innerType();

                                final int maxnumber = innerlist.maxNumberOfElements() * list.maxNumberOfElements();

                                expression.SetType(new ListType(innerlist.innerType(), maxnumber, null));

                                break;

                        }

                        else

                                return Error(expression, "Distributed Concatenation operator only applicable to list of lists");

                case dinter:     // list of list of A -> list of A (intersection, does not respect dupes)

                        if ((child.type().kind() == TypeKind.ListType)

                                        && (((ListType)child.type()).innerType().kind() == TypeKind.ListType))

                        {

                                list = (ListType)child.type();

                                final ListType innerlist = (ListType)list.innerType();

                                final int maxnumber = innerlist.maxNumberOfElements();

                                expression.SetType(new ListType(innerlist.innerType(), maxnumber, null));

                                break;

                        }

                        else

                                return Error(expression, "Distributed Intersection operator only applicable to list of lists");

                case dunion:     // list of list of A -> list of A (union, does not respect dupes)

                        if ((child.type().kind() == TypeKind.ListType)

                                        && (((ListType)child.type()).innerType().kind() == TypeKind.ListType))

                        {

                                list = (ListType)child.type();

                                final ListType innerlist = (ListType)list.innerType();

                                // better upper limit?!

                                                final int maxnumber = innerlist.maxNumberOfElements() * list.maxNumberOfElements();

                                                expression.SetType(new ListType(innerlist.innerType(), maxnumber, null));

                                                break;

                        }

                        else

                                return Error(expression, "Distributed Union operator only applicable to list of lists");

                case elems:      // list of A -> list of A (does not respect dupes)

                        if (child.type().kind() != TypeKind.ListType)

                                return Error(expression, "Element operator only applicable to list");

                        expression.SetType(child.type());

                        break;

                case head:       // list of A -> A

                        if (child.type().kind() != TypeKind.ListType)

                                return Error(expression, "Head operator only applicable to list");

                        expression.SetType(((ListType)child.type()).innerType());

                        break;

                case inds:       // list of A -> list of int

                        if (child.type().kind() != TypeKind.ListType)

                                return Error(expression, "Indices operator only applicable to list");

                        list = (ListType)child.type();

                        final IntType inner = new IntType(0, list.maxNumberOfElements(), null);

                        expression.SetType(new ListType(inner, list.maxNumberOfElements(), null));

                        break;

                case len:        // list of A -> int (dupes count)

                        if (child.type().kind() != TypeKind.ListType)

                                return Error(expression, "Length operator only applicable to list");

                        list = (ListType)child.type();

                        expression.SetType(new IntType(0, list.maxNumberOfElements(), null));

                        break;

                case tail:       // list of A -> list of A

                        if (child.type().kind() != TypeKind.ListType)

                                return Error(expression, "Tail operator only applicable to list");

                        list = (ListType)child.type();

                        if (list.maxNumberOfElements() == 0)

                                return Error(expression, "Tail operator only applicable to list of length > 0");

                        final int newmaxelems = list.maxNumberOfElements() - 1;

                        if (newmaxelems == 0)

                                Warning(expression, "Tail operator returns empty list.");

                        // set the return type null when list is empty?

                        expression.SetType(new ListType(list.innerType(), newmaxelems, null));

                        break;

                        /*unary numberic*/

                case unminus:

                        if (!child.type().IsNumeric())

                                return Error(expression, "Unary minus only applicable to numeric types");

                        expression.SetType(Expression.ArithmeticCover(child.type(), null, expression.kind()));

                        break;

                case unplus:

                        if (!child.type().IsNumeric())

                                return Error(expression, "Unary plus only applicable to numeric types");

                        expression.SetType(child.type());

                        break;

                case abs:

                        if (!child.type().IsNumeric())

                                return Error(expression, "Abs only applicable to numeric types");

                        expression.SetType(child.type());

                        break;

                case not:

                        if (/*!IsNumeric(child.type) && */

                                        (child.type().kind() != TypeKind.BoolType))

                                return Error(expression, "Not only applicable to bool types");

                        expression.SetType(child.type());

                        break;

                        /*unary quantors*/

                case forall:

                        expression.SetType(new BoolType(null));

                        break;

                case exists:

                        expression.SetType(new BoolType(null));

                        break;

                default:

                        throw new NotImplementedException();

                }

                expression.SetChild(child);

                return expression;

        }

        @SuppressWarnings("unchecked")

        private Expression ResolveExpression(BinaryOperator expression)

        {

                Expression lhs = ResolveExpression(expression.left());

                Expression rhs = ResolveExpression(expression.right());

                // if there was some error, then exit

                if ((lhs == null) || (rhs == null))

                        return null;

                final UlyssesType lt = lhs.type();

                final UlyssesType rt = rhs.type();

                if ((lt == null) || (rt == null))

                        return Error(expression, "Binary operator not applicable to void-type subexpression.");

                switch (expression.kind())

                {

                /*map operators*/

                case domresby:   // list of A * map A to B -> map A to B

                case domresto:   // list of A * map A to B -> map A to B

                        if (lt.kind() != TypeKind.ListType)

                                return Error(expression, "Domain restriction operator expects list on LHS");

                        if (rt.kind() != TypeKind.MapType)

                                return Error(expression, "Domain restriction operator expects map on RHS");

                        ListType domlist = (ListType)lt;

                        MapType domMap = (MapType)rt;

                        if (!UlyssesType.TypeEqual(domlist.innerType(), domMap.fromType()))

                                return Error(expression, "Inner type of list and domain-type of map do not match");

                        // since this is a restriction, maxnumofelems is ok

                        expression.SetType(domMap);

                        break;

                case rngresby:   // map A to B * list of B -> map A to B

                case rngresto:   // map A to B * list of B -> map A to B

                        if (lt.kind() != TypeKind.MapType)

                                return Error(expression, "Range restriction operator expects map on LHS");

                        if (rt.kind() != TypeKind.ListType)

                                return Error(expression, "Rangle restriction operator expects list on RHS");

                        final ListType rangelist = (ListType)rt;

                        domMap = (MapType)lt;

                        if (!UlyssesType.TypeEqual(rangelist.innerType(), domMap.fromType()))

                                return Error(expression, "Inner type of list and rangle-type of map do not match");

                        // since this is a restriction, maxnumofelems is ok

                        expression.SetType(domMap);

                        break;

                case munion:     // map A to B * map A to B -> map A to B

                        if (lt.kind() != TypeKind.MapType ||

                        rt.kind() != TypeKind.MapType)

                                return Error(expression, "Map union expects maps on LHS and RHS");

                        domMap = (MapType)lt;

                        MapType rngMap = (MapType)rt;

                        if (!UlyssesType.TypeEqual(domMap.fromType(), rngMap.fromType()) ||

                                        !UlyssesType.TypeEqual(domMap.toType(), rngMap.toType()))

                                return Error(expression, "Domain and Range types of maps must be equal");

                        // union may change maximum number of elements..

                        final MapType resMap = new MapType(domMap.fromType(), domMap.toType(),

                                        domMap.maxNumberOfElements() + rngMap.maxNumberOfElements(), null);

                        expression.SetType(resMap);

                        break;

                        /*set/list binary*/

                case conc:       // list of A * list of A -> list of A

                        if (lt.kind() != TypeKind.ListType ||

                        rt.kind() != TypeKind.ListType)

                                return Error(expression, "List concatenation expects two lists.");

                        ListType la = (ListType)lt;

                        ListType lb = (ListType)rt;

                        if (lb.innerType().kind() == TypeKind.Null || lb.maxNumberOfElements() == 0)

                                return lhs;

                        if (la.innerType().kind() == TypeKind.Null || la.maxNumberOfElements() == 0)

                                return rhs;

                        if (!UlyssesType.TypeEqual(la.innerType(), lb.innerType()))

                                return Error(expression, String.format("Set/List concatenation expects two lists of same type. (%s <> %s)", la.toString(), lb.toString()));

                        ListType resultList = new ListType(la.innerType(),

                                        la.maxNumberOfElements() + lb.maxNumberOfElements(), null);

                        expression.SetType(resultList);

                        break;

                case diff:       // list of A * list of A -> list of A (does not respect dupes)

                        if (lt.kind() != TypeKind.ListType ||

                        rt.kind() != TypeKind.ListType)

                                return Error(expression, "Set difference expects two lists.");