OoasTools

/**

  *

  *                      OOAS Compiler (Deprecated)

  *

  * Copyright 2015, Institute for Software Technology, Graz University of

  * Technology. Portions are copyright 2015 by the AIT Austrian Institute

  * of Technology. All rights reserved.

  *

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

  *

  * Please notice that this version of the OOAS compiler is considered de-

  * precated. Only the Java version is maintained.

  *

  * Contributors:

  *               Willibald Krenn (TU Graz/AIT)

  *               Stefan Tiran (TU Graz/AIT)

  */

using System;

using System.Collections.Generic;

using System.Text;

namespace TUG.Mogentes

{

    /// <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 sealed class OoaResolveExpressionsVisitor : OoaCompleteAstTraversalVisitor

    {

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

        private 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 AstNodeTypeEnum.identifier:

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

                    break;

                case AstNodeTypeEnum.statement:

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

                    break;

                default:

                    throw new NotImplementedException();

            }

        }

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

        {

            switch (identifier.kind)

            {

                case IdentifierKind.AttributeIdentifier:

                    AttributeIdentifier ident = (AttributeIdentifier)identifier;

                    System.Diagnostics.Debug.Assert(ReferenceEquals(ident.initializer, subElement));

                    ident.SetInitializer(newExpression);

                    break;

                case IdentifierKind.Constant:

                    ConstantIdentifier aconst = (ConstantIdentifier)identifier;

                    System.Diagnostics.Debug.Assert(ReferenceEquals(aconst.Value, subElement));

                    aconst.SetValue(newExpression);

                    if (newExpression.kind != ExpressionKind.Value)

                    {

                        Error(aconst.Value, String.Format("{0} not a constant!", aconst.tokenText));

                    }

                    break;

                default:

                    throw new NotImplementedException();

            }

        }

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

        {

            switch (statement.kind)

            {

                case StatementKind.GuardedCommand:

                    GuardedCommand gc = (GuardedCommand)statement;

                    System.Diagnostics.Debug.Assert(ReferenceEquals(gc.guard, subElement));

                    gc.SetGuard(newExpression);

                    break;

                case StatementKind.SeqBlock:

                    SeqBlock sqblock = (SeqBlock)statement;

                    System.Diagnostics.Debug.Assert(ReferenceEquals(sqblock.filter, subElement));

                    sqblock.SetFilter(null);

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

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

                    implseq.SetStatements(sqblock.statements);

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

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

                    sqblock.AddStatement(implguard);

                    break;

                case StatementKind.Assignment:

                    Assignment zw = (Assignment)statement;

                    bool found = false;

                    if (ReferenceEquals(zw.nondetExpression, subElement))

                    {

                        zw.SetNondetExpression(newExpression);

                        found = true;

                    }

                    else

                    {

                        LinkedListNode<Expression> anode = zw.places.First;

                        while (anode != null)

                        {

                            if (ReferenceEquals(anode.Value, subElement))

                            {

                                anode.Value = newExpression;

                                found = true;

                                break;

                            }

                            anode = anode.Next;

                        }

                        anode = zw.values.First;

                        while (anode != null)

                        {

                            if (ReferenceEquals(anode.Value, subElement))

                            {

                                anode.Value = newExpression;

                                found = true;

                                break;

                            }

                            anode = anode.Next;

                        }

                    }

                    System.Diagnostics.Debug.Assert(found);

                    break;

                case StatementKind.MethodCall:

                    Call call = (Call)statement;

                    System.Diagnostics.Debug.Assert(ReferenceEquals(call.callExpression, subElement));

                    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)

        {

            ParserError error = new ParserError(m_ParserState.filename,

                expression.line, expression.pos, p);

            m_ParserState.AddErrorMessage(error);

            return null;

        }

        private Expression Error(int line, int pos, string p)

        {

            ParserError error = new ParserError(m_ParserState.filename, line, pos, p);

            m_ParserState.AddErrorMessage(error);

            return null;

        }

        // helper that adds a warning message to the output

        private void Warning(Identifier expression, string p)

        {

            ParserWarning warning = new ParserWarning(m_ParserState.filename,

                expression.line, expression.column, p);

            m_ParserState.AddWarningMessage(warning);

        }

        private void Warning(Expression expression, string p)

        {

            ParserWarning warning = new ParserWarning(m_ParserState.filename,

                expression.line, expression.pos, p);

            m_ParserState.AddWarningMessage(warning);

        }

        private void Info(Expression expression, String p)

        {

            ParserMessage msg = new ParserMessage(m_ParserState.filename,

            expression.line, expression.pos, p);

            m_ParserState.AddMessage(msg);

        }

        private List<TupleConstructor> m_matcherList = new List<TupleConstructor>();

        /// 

        ///   Resolve Expressions

        /// 

        private Expression ResolveExpression(TernaryOperator expression)

        {

            if (expression.kind == ExpressionKind.conditional)

            {

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

                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. ({0} <> {1})", 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 List<Expression>(), expression.line,

                        expression.pos, expression.definingScope)

                    : (CallExpression)expression.left;

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

                if (leftcall == null)

                    return null;

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

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

                bool isMap = expression.mid == null;

                Expression mid = expression.mid;

                if (!isMap)

                {

                    mid = ResolveExpression(mid);

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

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

                }

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

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

                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)

                {

                    UlyssesType initCover = UlyssesType.CoverType(funType.parameter.Last.Previous.Value, 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.Last.Value, 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.Last.Value, ((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)

        {

            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)

        {

            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.Count != 1)

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

            }

            List<Expression> newitems = new List<Expression>();

            if (expression.elements.Count == 0 || expression.elements[0] == null || (

                expression.elements[0].kind == ExpressionKind.Value &&

                expression.elements[0] is ValueExpression<object> &&

                ((ValueExpression<object>)expression.elements[0]).value == null))

            {

                // empty list

                type = new NullType();

            }

            else

            {

                List<Expression> tmpitems = new List<Expression>();

                foreach (var item in expression.elements)

                {

                    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 is ValueExpression<object> &&

                        ((ValueExpression<object>)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

                foreach (var item in tmpitems)

                {

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

                    {

                        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.Count, 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.Count != 1)

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

            }

            List<Expression> newitems = new List<Expression>();

            foreach (var item in expression.items)

            {

                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.Count, null);

            expression.SetType(restype);

            return expression;

        }

        private Expression ResolveExpression(MapConstructor expression)

        {

            UlyssesType domain = null;

            UlyssesType range = null;

            List<MapConstructor.MapItem> newitems = new List<MapConstructor.MapItem>();

            foreach (MapConstructor.MapItem item in expression.items)

            {

                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;

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

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

            expression.SetType(resulttype);

            return expression;

        }

        private Expression ResolveExpression(TupleConstructor expression)

        {

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

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

                return Error(expression, String.Format("Tuple constructor has wrong arity. ({0} <> {1})", typeToConstruct.innerTypes.Count, expression.values.Count));

            //TupleType resulttype = new TupleType(null);

            List<Expression> newvalexprs = new List<Expression>();

            LinkedListNode<UlyssesType> innerTargetType = typeToConstruct.innerTypes.First;

            int freeVarCount = 0;

            foreach (var initexpr in expression.values)

            {

                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.

                    AnyType freevar = (AnyType)newval.type;

                    freevar.VariableIdentifier.SetType(innerTargetType.Value);

                    freevar.VariableIdentifier.SetInitialized(true);

                    freeVarCount++;

                }

                else

                {

                    UlyssesType acover = UlyssesType.CoverType(innerTargetType.Value, newval.type);

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

                        return Error(expression, String.Format("Element in tuple constructor has non-matching type ({0} <> {1})", innerTargetType.Value.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(innerTargetType.Value, acover))

                        Warning(expression, String.Format("Tuple constructor may over/underflow: {0} := {1}", innerTargetType.Value.ToString(), acover.ToString()));

                }

                newvalexprs.Add(newval);

                //resulttype.AddType(newval.type);

                innerTargetType = innerTargetType.Next;

            }

            if (freeVarCount > 0)

            {

                if (freeVarCount != expression.values.Count)

                    return Error(expression, String.Format("Tuple constructor must have 0 or #elems ({0}) free variables", expression.values.Count));

                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: {0} <> {1}",

                        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.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 IdentifierKind.TypeIdentifier:

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

                    case IdentifierKind.MethodIdentifier:

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

                        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)

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

                            aself.setIsSelf(true);

                            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 IdentifierKind.NamedActionIdentifier:

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

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

                    case IdentifierKind.Constant:

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

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

                        else

                            return null;

                    default:

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

                }

            }

            else

            {

                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: '{0}'.", freeVar.tokenText));

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

            }

        }

        private Expression ResolveExpression(TupleMapAccessExpression expression)

        {

            Expression child = ResolveExpression(expression.child);

            if (child == null)

                return null;

            Expression arg = ResolveExpression(expression.argument);

            if (arg == null)

                return null;

            System.Diagnostics.Debug.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!");

                }

                TupleType aTuple = (TupleType)child.type;

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

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

                {

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

            }

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

            {

                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]

                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, bool allowFewerParameters)

        {

            // calc type of child

            Expression child = ResolveExpression(expression.child);

            if (child == null)

                return null;

            System.Diagnostics.Debug.Assert(child.type != null);

            expression.SetChild(child);

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

            {

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

            }

            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 is NamedActionIdentifier || callingScope is MethodIdentifier)

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

                    callingScope = callingScope.GetParentScope();

                }

            }

            // check arguments

            int argsSpec = funtype.parameter.Count;

            int argsHave = expression.arguments.Count;

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

            }

            List<Expression> newargs = new List<Expression>();

            LinkedListNode<UlyssesType> demandedArgType = funtype.parameter.First;

            foreach (var arg in expression.arguments)

            {

                Expression newarg = ResolveExpression(arg);

                if (newarg == null)

                    return null;

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

                    Error(arg, String.Format("Undefined variable '{0}'", newarg.GetUninitializedFreeVariables()[0].tokenText));

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

                UlyssesType acover = UlyssesType.CoverType(newarg.type, demandedArgType.Value);

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

                    return Error(arg, String.Format("Argument type does not match; expected: {0} delivered: {1}",

                        demandedArgType.Value.ToString(), newarg.type.ToString()));

                newarg = UnaryOperator.TryCoerceUp(newarg, acover);

                if (UlyssesType.FirstTypeLessRange(demandedArgType.Value, acover))

                {

                    if (constantvalue == null)

                    {

                        Warning(arg, String.Format("Call parameter may over/underflow: {0} := {1}", demandedArgType.Value.ToString(), acover.ToString()));

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

                        cast.SetType(demandedArgType.Value);

                        newarg = cast;

                    }

                    else

                    {

                        Error(arg, String.Format("Call parameter out of range ({0}  := {1})", demandedArgType.Value.ToString(), constantvalue.ToString()));

                    }

                }

                demandedArgType = demandedArgType.Next;

                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 is UnresolvedIdentifierExpression))

            {

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

                expression.SetType(expression.right.type);

                return expression;

            }

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

            bool staticAccess = lhs.kind == ExpressionKind.Type;

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

                FunctionType fun = (FunctionType)atype;

                // check arity

                if (fun.parameter.Count > 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 TypeKind.OoActionSystemType:

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

                    if (anid != null)

                    {

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

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

                        if (staticAccess)

                        {

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

                                (((AttributeIdentifier)anid).isStatic))

                            {

                                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

                            {

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

                                expression.SetRightChild(newrhs);

                            }

                        }

                    }

                    else

                        return Error(access, String.Format("{0} no member of {1}",

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

                    break;

                case TypeKind.EnumeratedType:

                    EnumType anEnum = (EnumType)atype;

                    if (!staticAccess)

                    {

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

                    }

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

                    {

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

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

                        expression.SetRightChild(newrhs);

                    }

                    else

                        return Error(access, String.Format("{0} not contained in enum {1}",

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

                    break;

                case TypeKind.QrType:

                    QrType aQualitativeType = (QrType)atype;

                    if (!staticAccess)

                    {

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

                    }

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

                    {

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

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

                        expression.SetRightChild(newrhs);

                    }

                    else

                        return Error(access, String.Format("{0} not contained in qspace {1}",

                                 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)

        {

            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 ExpressionKind.Primed:

                    expression.SetType(child.type);

                    break;

                /*map unary*/

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

                        ListType innerlist = (ListType)list.innerType;

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

                        ListType innerlist = (ListType)list.innerType;

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

                        ListType innerlist = (ListType)list.innerType;

                        // better upper limit?!

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

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

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

                    break;

                case ExpressionKind.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 ExpressionKind.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");

                    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 ExpressionKind.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 ExpressionKind.unplus:

                    if (!child.type.IsNumeric())

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

                    expression.SetType(child.type);

                    break;

                case ExpressionKind.abs:

                    if (!child.type.IsNumeric())

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

                    expression.SetType(child.type);

                    break;

                case ExpressionKind.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 ExpressionKind.forall:

                    expression.SetType(new BoolType(null));

                    break;

                case ExpressionKind.exists:

                    expression.SetType(new BoolType(null));

                    break;

                default:

                    throw new NotImplementedException();

            }

            expression.SetChild(child);

            return expression;

        }

        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;

            UlyssesType lt = lhs.type;

            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 ExpressionKind.domresby:   // list of A * map A to B -> map A to B

                case ExpressionKind.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 ExpressionKind.rngresby:   // map A to B * list of B -> map A to B

                case ExpressionKind.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");

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

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

                        domMap.maxNumberOfElements + rngMap.maxNumberOfElements, null);

                    expression.SetType(resMap);

                    break;

                /*set/list binary*/

                case ExpressionKind.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. ({0} <> {1})", la.ToString(), lb.ToString()));

                    ListType resultList = new ListType(la.innerType,

                        la.maxNumberOfElements + lb.maxNumberOfElements, null);

                    expression.SetType(resultList);

                    break;

                case ExpressionKind.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.");

                    la = (ListType)lt;

                    lb = (ListType)rt;

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

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

                    expression.SetType(la);

                    break;

                case ExpressionKind.inter:      // 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 intersection expects two lists.");

                    la = (ListType)lt;

                    lb = (ListType)rt;

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

                        return Error(expression, "Set intersection expects two lists of same type.");

                    expression.SetType(la.maxNumberOfElements > lb.maxNumberOfElements ? la : lb);

                    break;

                case ExpressionKind.elemin:     // A * list of A -> bool

                case ExpressionKind.notelemin:  // A * list of A -> bool

                    if (rt.kind != TypeKind.ListType)

                        return Error(expression, "Element (not) in operator expects list-type as RHS.");

                    lb = (ListType)rt;

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

                        return Error(expression, "List and element must be of same type.");

                    expression.SetType(new BoolType(null));

                    break;

                case ExpressionKind.subset:     // list of A * list of A -> bool (does not respect dupes)

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

                        rt.kind != TypeKind.ListType)

                        return Error(expression, "Subset operation expects two lists.");

                    la = (ListType)lt;

                    lb = (ListType)rt;

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

                        return Error(expression, "Subset operation expects two lists of same type.");

                    expression.SetType(new BoolType(null));

                    break;

                case ExpressionKind.union:      // 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 union expects two lists.");

                    la = (ListType)lt;

                    lb = (ListType)rt;

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

                        return rhs;

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

                        return lhs;

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

                        return Error(expression, "Set union expects two lists of same type.");

                    resultList = new ListType(la.innerType,

                        la.maxNumberOfElements + lb.maxNumberOfElements, null);

                    expression.SetType(resultList);

                    break;

                /*numeric binary*/

                case ExpressionKind.pow:

                    if (!lt.IsNumeric() ||

                        !rt.IsNumeric())

                        return Error(expression, "Operator expects LHS and RHS to be numeric");

                    if (lt.kind == TypeKind.IntType

                        && rt.kind == TypeKind.IntType)

                        expression.SetType(lt);

                    else

                        if (lt.kind == TypeKind.FloatType)

                            expression.SetType(lt);

                        else

                        {

                            IntType anint = (IntType)lt;

                            expression.SetType(new FloatType(anint.rangeLow, anint.rangeHigh,

                                FloatType.defaultPrecision, null));

                        }

                    break;

                case ExpressionKind.idiv:

                case ExpressionKind.mod:

                    if (rt.kind != TypeKind.IntType ||

                        lt.kind != TypeKind.IntType)

                        return Error(expression, "Operator expects LHS and RHS to be integer");

                    expression.SetType(Expression.ArithmeticCover(lt, rt, expression.kind));

                    break;

                case ExpressionKind.div:

                    if (!rt.IsNumeric() || !lt.IsNumeric())

                        return Error(expression, "Operator expects LHS and RHS to be numeric");

                    if (lhs.type is ValuedEnumType)

                        lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type).getIntType());

                    if (rhs.type is ValuedEnumType)

                        rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type).getIntType());

                    UlyssesType cover = Expression.ArithmeticCover(lt, rt, expression.kind);

                    expression.SetType(cover);

                    break;

                case ExpressionKind.minus:

                    if (!rt.IsNumeric() || !lt.IsNumeric())

                        return Error(expression, "Operator expects LHS and RHS to be numeric");

                    if (lhs.type is ValuedEnumType)

                        lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type).getIntType());

                    if (rhs.type is ValuedEnumType)

                        rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type).getIntType());

                    cover = Expression.ArithmeticCover(lt, rt, expression.kind);

                    expression.SetType(cover);

                    break;

                case ExpressionKind.prod:

                    if (!rt.IsNumeric() || !lt.IsNumeric())

                        return Error(expression, "Operator expects LHS and RHS to be numeric");

                    if (lhs.type is ValuedEnumType)

                        lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type).getIntType());

                    if (rhs.type is ValuedEnumType)

                        rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type).getIntType());

                    cover = Expression.ArithmeticCover(lt, rt, expression.kind);

                    expression.SetType(cover);

                    break;

                case ExpressionKind.sum:

                    if (!rt.IsNumeric() || !lt.IsNumeric())

                        return Error(expression, "Operator expects LHS and RHS to be numeric");

                    if (lhs.type is ValuedEnumType)

                        lhs = UnaryOperator.TryCoerceUp(lhs, ((ValuedEnumType)lhs.type).getIntType());

                    if (rhs.type is ValuedEnumType)

                        rhs = UnaryOperator.TryCoerceUp(rhs, ((ValuedEnumType)rhs.type).getIntType());

                    cover = Expression.ArithmeticCover(lt, rt, expression.kind);

                    expression.SetType(cover);

                    break;

                case ExpressionKind.greater:

                case ExpressionKind.greaterequal:

                case ExpressionKind.less:

                case ExpressionKind.lessequal:

                    if (!((rt.IsNumeric() && lt.IsNumeric()) || (rt.IsQualitative() && lt.IsQualitative())))

                        return Error(expression, "Operator expects LHS and RHS to be numeric or qualitative");

                    cover = UlyssesType.CoverType(lt, rt);

                    if (cover != null)

                    {

                        lhs = UnaryOperator.TryCoerceUp(lhs, cover);

                        rhs = UnaryOperator.TryCoerceUp(rhs, cover);

                        expression.SetType(new BoolType(null));

                    }

                    else

                        return Error(expression, String.Format("Operator expects LHS and RHS to be of same type ({0} <> {1})", lhs.type.ToString(), rhs.type.ToString()));

                    break;

                /*bool binary*/

                case ExpressionKind.and:

                    if (rt.kind != TypeKind.BoolType ||

                        lt.kind != TypeKind.BoolType)

                        return Error(expression, "Operator expects LHS and RHS of bool.");

                    expression.SetType(rt);

                    // little bit of optimization..

                    if (rhs.kind == ExpressionKind.Value

                        && ((ValueExpression<bool>)rhs).value == false)

                        return rhs;

                    else if (lhs.kind == ExpressionKind.Value

                        && ((ValueExpression<bool>)lhs).value == false)

                        return lhs;

                    // if both are true, then this will be taken care of in constant folding.

                    break;

                case ExpressionKind.biimplies:

                    if (rt.kind != TypeKind.BoolType ||

                        lt.kind != TypeKind.BoolType)

                        return Error(expression, "Operator expects LHS and RHS of bool.");

                    expression.SetType(rt);

                    break;

                case ExpressionKind.implies:

                    if (rt.kind != TypeKind.BoolType ||

                        lt.kind != TypeKind.BoolType)

                        return Error(expression, "Operator expects LHS and RHS of bool.");

                    expression.SetType(rt);

                    // ex falso...

                    if (lhs.kind == ExpressionKind.Value

                        && ((ValueExpression<bool>)lhs).value == false)

                    {

                        Expression shortcut = new ValueExpression<bool>(true, expression.line, expression.pos);

                        shortcut.SetType(lt);

                        return shortcut;

                    }

                    break;

                case ExpressionKind.or:

                    if (rt.kind != TypeKind.BoolType ||

                        lt.kind != TypeKind.BoolType)

                        return Error(expression, "Operator expects LHS and RHS of bool.");

                    expression.SetType(rt);

                    if (rhs.kind == ExpressionKind.Value

                        && ((ValueExpression<bool>)rhs).value == true)

                        return rhs;

                    else if (lhs.kind == ExpressionKind.Value

                        && ((ValueExpression<bool>)lhs).value == true)

                        return lhs;

                    break;

                /*other binary*/

                case ExpressionKind.equal:

                case ExpressionKind.notequal:

                    cover = UlyssesType.CoverType(lt, rt);

                    if (cover != null)

                    {

                        /* see whether we have a tuple-matcher on one side.. */

                        if (expression.kind == ExpressionKind.equal)

                        {

                            if (lhs.kind == ExpressionKind.TupleConstr &&

                                ((TupleConstructor)lhs).isMatcher)

                            {

                                if (rhs.kind == ExpressionKind.TupleConstr &&

                                    ((TupleConstructor)rhs).isMatcher)

                                    return Error(expression, "Free variables on both sides of the equality sign in tuple constructors.");

                                m_matcherList.Remove((TupleConstructor)lhs);

                            }

                            else if (rhs.kind == ExpressionKind.TupleConstr &&

                                    ((TupleConstructor)rhs).isMatcher)

                            {

                                if (lhs.kind == ExpressionKind.TupleConstr &&

                                    ((TupleConstructor)lhs).isMatcher)

                                    return Error(expression, "Free variables on both sides of the equality sign in tuple constructors.");

                                m_matcherList.Remove((TupleConstructor)rhs);

                            }

                        }

                        lhs = UnaryOperator.TryCoerceUp(lhs, cover);

                        rhs = UnaryOperator.TryCoerceUp(rhs, cover);

                        expression.SetType(new BoolType(null));

                    }

                    else

                        return Error(expression, String.Format("Operator expects LHS and RHS to be of same type ({0} <> {1})", lhs.type.ToString(), rhs.type.ToString()));

                    break;

                case ExpressionKind.seqmod_mapoverride:

                    if (rt.kind != TypeKind.MapType)

                        return Error(expression, "Map expected as RHS on sequence modification or map override.");

                    // list of A * map int to A -> list of A or

                    if (lt.kind == TypeKind.ListType)

                    {

                        // we're in sequence modification.

                        domlist = (ListType)lt;

                        rngMap = (MapType)rt;

                        if (rngMap.fromType.kind != TypeKind.IntType)

                            return Error(expression, "Domain of map has to be integer");

                        if (!UlyssesType.TypeEqual(domlist.innerType, rngMap.toType))

                            return Error(expression, "Type of list expected to match range of map");

                        // since we only replace elements in the list (by matching ones from the map),

                        // we're save to return the original list..

                        expression.SetType(lt);

                    }

                    // map A to B * map A to B -> map A to B

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

                    {

                        domMap = (MapType)lt;

                        rngMap = (MapType)rt;

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

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

                            return Error(expression, "Maps need same domain and range types");

                        // since we override entries in the first map:

                        expression.SetType(domMap);

                    }

                    else

                        return Error(expression, "Sequence Modification or Map override expects list or map as LHS");

                    break;

                default:

                    throw new NotImplementedException();

            }

            // set subtrees.

            expression.SetLeftChild(lhs);

            expression.SetRightChild(rhs);

            // we only allow:  a = MyTuple(c,d) style matchers

            if (m_matcherList.Count > 0)

            {

                m_matcherList.Clear();

                return Error(expression, "Free variables in tuple constructor only allowed in expressions of the form 'atuple = ATupleConstructor(free1,free2...)'");

            }

            // try simple constant folding

            return ApplyConstantFolding(expression);

        }

        /// 

        ///  We're also doing a bit of constant folding here.

        /// 

        private Expression ApplyConstantFolding(UnaryOperator expression)

        {

            Expression child = expression.child;

            if (child.type.IsNumeric() && expression.kind == ExpressionKind.Cast)

            {

                switch (expression.type.kind)

                {

                    case TypeKind.FloatType:

                        if (child.type.kind == TypeKind.IntType && child.kind == ExpressionKind.Value)

                        {

                            Expression result = new ValueExpression<double>(((ValueExpression<int>)child).value, child.line, child.pos);

                            result.SetType(expression.type);

                            return result;

                        }

                        break;

                }

            }

            return expression;

        }

        private Expression ApplyConstantFolding(BinaryOperator expression)

        {

            Expression lhs = expression.left;

            Expression rhs = expression.right;

            if (lhs.kind == ExpressionKind.Cast)

            {

                lhs = ApplyConstantFolding((UnaryOperator)lhs);

                expression.SetLeftChild(lhs);

            }

            if (rhs.kind == ExpressionKind.Cast)

            {

                rhs = ApplyConstantFolding((UnaryOperator)rhs);

                expression.SetRightChild(rhs);

            }

            if (lhs.kind == ExpressionKind.Value && rhs.kind == ExpressionKind.Value)

                if (expression.type.kind == TypeKind.FloatType)

                {

                    double fval1 = ((ValueExpression<double>)lhs).value;

                    double fval2 = ((ValueExpression<double>)rhs).value;

                    double result = 0;

                    switch (expression.kind)

                    {

                        case ExpressionKind.sum:

                            result = fval1 + fval2;

                            break;

                        case ExpressionKind.minus:

                            result = fval1 - fval2;

                            break;

                        case ExpressionKind.prod:

                            result = fval1 * fval2;

                            break;

                        case ExpressionKind.div:

                            if (fval2 == 0)

                                return Error(expression, "Division not defined");

                            result = fval1 / fval2;

                            break;

                        default:

                            // bail out, if we can not handle it

                            return expression;

                    }

                    if (result < ((FloatType)expression.type).low

                        || result > ((FloatType)expression.type).high)

                        return Error(expression, "Internal Error: value after constant folding not in float-range!");

                    ValueExpression<double> resexp = new ValueExpression<double>(result, expression.line, expression.pos);

                    resexp.SetType(expression.type);

                    return resexp;

                }

                else if (expression.type.kind == TypeKind.IntType)

                {

                    int val1 = ((ValueExpression<int>)lhs).value;

                    int val2 = ((ValueExpression<int>)rhs).value;

                    int result = 0;

                    switch (expression.kind)

                    {

                        case ExpressionKind.sum:

                            result = val1 + val2;

                            break;

                        case ExpressionKind.minus:

                            result = val1 - val2;

                            break;

                        case ExpressionKind.prod:

                            result = val1 * val2;

                            break;

                        case ExpressionKind.idiv:

                            if (val2 == 0)

                                return Error(expression, "Division not defined.");

                            result = val1 / val2;

                            break;

                        case ExpressionKind.mod:

                            result = val1 % val2;

                            break;

                        default:

                            // bail out, if we can not handle it

                            return expression;

                    }

                    if (result < ((IntType)expression.type).rangeLow

                        || result > ((IntType)expression.type).rangeHigh)

                        return Error(expression, "Internal Error: value after constant folding not in int-range!");

                    ValueExpression<int> intres = new ValueExpression<int>(result, expression.line, expression.pos);

                    intres.SetType(expression.type);

                    return intres;

                }

                else if (expression.type.kind == TypeKind.BoolType)

                {

                    bool result = false;

                    switch (expression.kind)

                    {

                        case ExpressionKind.greater:

                            System.Diagnostics.Debug.Assert(lhs.type.kind == rhs.type.kind);

                            switch (lhs.type.kind)

                            {

                                case TypeKind.IntType:

                                    result = ((ValueExpression<int>)lhs).value >

                                                ((ValueExpression<int>)rhs).value;

                                    break;

                                case TypeKind.FloatType:

                                    result = ((ValueExpression<double>)lhs).value >

                                                ((ValueExpression<double>)rhs).value;

                                    break;

                                default: