//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
//---------------------------------------------------------------------------------------------
// BoogiePL - Absy.cs
//---------------------------------------------------------------------------------------------

namespace Microsoft.Boogie {
  using System;
  using System.Collections;
  using System.Diagnostics;
  using System.Linq;
  using System.Collections.Generic;
  using Microsoft.Boogie.AbstractInterpretation;
  using System.Diagnostics.Contracts;

  //=====================================================================
  //---------------------------------------------------------------------
  // Types
  [ContractClass(typeof(TypeContracts))]
  public abstract class Type : Absy {
    public Type(IToken/*!*/ token)
      : base(token) {
      Contract.Requires(token != null);
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively. Applying Clone to a type will return
    // a type in which all bound variables have been replaced with new
    // variables, whereas free variables have not changed

    public override Absy Clone() {
      Contract.Ensures(Contract.Result<Absy>() != null);
      return this.Clone(new Dictionary<TypeVariable/*!*/, TypeVariable/*!*/>());
    }

    public abstract Type/*!*/ Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap);

    /// <summary>
    /// Clones the type, but only syntactically.  Anything resolved in the source
    /// type is left unresolved (that is, with just the name) in the destination type.
    /// </summary>
    public abstract Type/*!*/ CloneUnresolved();

    //-----------  Linearisation  ----------------------------------

    public void Emit(TokenTextWriter stream) {
      Contract.Requires(stream != null);
      this.Emit(stream, 0);
    }

    public abstract void Emit(TokenTextWriter/*!*/ stream, int contextBindingStrength);

    [Pure]
    public override string ToString() {
      Contract.Ensures(Contract.Result<string>() != null);
      System.IO.StringWriter buffer = new System.IO.StringWriter();
      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/false, /*pretty=*/ false)) {
        this.Emit(stream);
      }
      return buffer.ToString();
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (ReferenceEquals(this, that))
        return true;
      Type thatType = that as Type;
      return thatType != null && this.Equals(thatType,
                                             new List<TypeVariable>(),
                                             new List<TypeVariable>());
    }

    [Pure]
    public abstract bool Equals(Type/*!*/ that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables);

    // used to skip leading type annotations (subexpressions of the
    // resulting type might still contain annotations)
    internal virtual Type/*!*/ Expanded {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);

        return this;
      }
    }

    //-----------  Unification of types  -----------

    /// <summary>
    /// Add a constraint that this==that, if possible, and return true.
    /// If not possible, return false (which may have added some partial constraints).
    /// No error is printed.
    /// </summary>
    public bool Unify(Type that) {
      Contract.Requires(that != null);
      return Unify(that, new List<TypeVariable>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());
    }

    public abstract bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
      // an idempotent substitution that describes the
      // unification result up to a certain point
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier);


    [Pure]
    public static bool IsIdempotent(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
      Contract.Requires(cce.NonNullDictionaryAndValues(unifier));
      return unifier.Values.All(val => val.FreeVariables.All(var => !unifier.ContainsKey(var)));
    }


#if OLD_UNIFICATION    
    // Compute a most general unification of two types. null is returned if
    // no such unifier exists. The unifier is not allowed to subtitute any
    // type variables other than the ones in "unifiableVariables"
    public IDictionary<TypeVariable!, Type!> Unify(Type! that,
                                                   List<TypeVariable>! unifiableVariables) {
      Dictionary<TypeVariable!, Type!>! result = new Dictionary<TypeVariable!, Type!> ();
      try {
        this.Unify(that, unifiableVariables,
                   new List<TypeVariable> (), new List<TypeVariable> (), result);
      } catch (UnificationFailedException) {
        return null;
      }
      return result;
    }

    // Compute an idempotent most general unifier and add the result to the argument
    // unifier. The result is true iff the unification succeeded
    public bool Unify(Type! that,
                      List<TypeVariable>! unifiableVariables,
                      // given mappings that need to be taken into account
                      // the old unifier has to be idempotent as well
                      IDictionary<TypeVariable!, Type!>! unifier)
      {
 Contract.Requires(Contract.ForAll(unifier.Keys , key=> unifiableVariables.Has(key)));
 Contract.Requires(IsIdempotent(unifier));
      try {
        this.Unify(that, unifiableVariables,
                   new List<TypeVariable> (), new List<TypeVariable> (), unifier);
      } catch (UnificationFailedException) {
        return false;
      }
      return true;
    }

    public abstract void Unify(Type! that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               // an idempotent substitution that describes the
                               // unification result up to a certain point
                               IDictionary<TypeVariable!, Type!>! result);
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public abstract Type/*!*/ Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst);

    //-----------  Hashcodes  ----------------------------------

    // Hack to be able to access the hashcode of superclasses further up
    // (from the subclasses of this class)
    [Pure]
    protected int GetBaseHashCode() {
      return base.GetHashCode();
    }

    [Pure]
    public override int GetHashCode() {
      return this.GetHashCode(new List<TypeVariable>());
    }

    [Pure]
    public abstract int GetHashCode(List<TypeVariable>/*!*/ boundVariables);

    //-----------  Resolution  ----------------------------------

    public override void Resolve(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      System.Diagnostics.Debug.Fail("Type.Resolve should never be called." +
                                    " Use Type.ResolveType instead");
    }

    public abstract Type/*!*/ ResolveType(ResolutionContext/*!*/ rc);

    public override void Typecheck(TypecheckingContext tc) {
      //Contract.Requires(tc != null);
      System.Diagnostics.Debug.Fail("Type.Typecheck should never be called");
    }

    // determine the free variables in a type, in the order in which the variables occur
    public abstract List<TypeVariable>/*!*/ FreeVariables {
      get;
    }

    // determine the free type proxies in a type, in the order in which they occur
    public abstract List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get;
    }

    protected static void AppendWithoutDups<A>(List<A> a, List<A> b) {
      Contract.Requires(b != null);
      Contract.Requires(a != null);
      foreach (A x in b)
        if (!a.Contains(x))
          a.Add(x);
    }

    public bool IsClosed {
      get {
        return FreeVariables.Count == 0;
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    // the following methods should be used instead of simple casts or the
    // C# "is" operator, because they handle type synonym annotations and
    // type proxies correctly

    public virtual bool IsBasic {
      get {
        return false;
      }
    }
    public virtual bool IsInt {
      get {
        return false;
      }
    }
    public virtual bool IsReal {
      get {
        return false;
      }
    }
    public virtual bool IsFloat {
      get {
        return false;
      }
    }
    public virtual bool IsBool {
      get {
        return false;
      }
    }

    public virtual bool IsVariable {
      get {
        return false;
      }
    }
    public virtual TypeVariable/*!*/ AsVariable {
      get {
        Contract.Ensures(Contract.Result<TypeVariable>() != null);

        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.AsVariable should never be called
      }
    }
    public virtual bool IsCtor {
      get {
        return false;
      }
    }
    public virtual CtorType/*!*/ AsCtor {
      get {
        Contract.Ensures(Contract.Result<CtorType>() != null);

        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.AsCtor should never be called
      }
    }
    public virtual bool IsMap {
      get {
        return false;
      }
    }
    public virtual MapType/*!*/ AsMap {
      get {
        Contract.Ensures(Contract.Result<MapType>() != null);

        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.AsMap should never be called
      }
    }
    public virtual int MapArity {
      get {

        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.MapArity should never be called
      }
    }
    public virtual bool IsUnresolved {
      get {
        return false;
      }
    }
    public virtual UnresolvedTypeIdentifier/*!*/ AsUnresolved {
      get {
        Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);

        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.AsUnresolved should never be called
      }
    }

    public virtual bool isFloat {
      get {
        return false;
      }
    }
    public virtual int FloatExponent
    {
      get
      {
        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.FloatExponent should never be called
      }
    }
    public virtual int FloatSignificand {
      get {
        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.FloatSignificand should never be called
      }
    }
    public virtual bool IsBv {
      get {
        return false;
      }
    }
    public virtual int BvBits {
      get {
        {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        } // Type.BvBits should never be called
      }
    }

    public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int);
    public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real);
    public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool);
    private static BvType[] bvtypeCache;

    static public BvType GetBvType(int sz) {
      Contract.Requires(0 <= sz);
      Contract.Ensures(Contract.Result<BvType>() != null);

      if (bvtypeCache == null) {
        bvtypeCache = new BvType[128];
      }
      if (sz < bvtypeCache.Length) {
        BvType t = bvtypeCache[sz];
        if (t == null) {
          t = new BvType(sz);
          bvtypeCache[sz] = t;
        }
        return t;
      } else {
        return new BvType(sz);
      }
    }

    static public FloatType GetFloatType(int sig, int exp) {
      Contract.Requires(0 <= exp);
      Contract.Requires(0 <= sig);
      Contract.Ensures(Contract.Result<FloatType>() != null);

      return new FloatType(sig, exp);
    }

    //------------ Match formal argument types on actual argument types
    //------------ and return the resulting substitution of type variables

#if OLD_UNIFICATION
    public static IDictionary<TypeVariable!, Type!>!
                  MatchArgumentTypes(List<TypeVariable>! typeParams,
                                     List<Type>! formalArgs,
                                     List<Expr>! actualArgs,
                                     List<Type> formalOuts,
                                     List<IdentifierExpr> actualOuts,
                                     string! opName,
                                     TypecheckingContext! tc)
      {
 Contract.Requires(formalArgs.Length == actualArgs.Length);
 Contract.Requires(formalOuts == null <==> actualOuts == null);
 Contract.Requires(formalOuts != null ==> formalOuts.Length == actualOuts.Length);
      List<TypeVariable>! boundVarSeq0 = new List<TypeVariable> ();
      List<TypeVariable>! boundVarSeq1 = new List<TypeVariable> ();
      Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();

      for (int i = 0; i < formalArgs.Length; ++i) {
        try {
          Type! actualType = cce.NonNull((!)actualArgs[i]).Type;
          // if the type variables to be matched occur in the actual
          // argument types, something has gone very wrong
          Contract.Assert(forall{TypeVariable! var in typeParams);
                        !actualType.FreeVariables.Has(var)};
          formalArgs[i].Unify(actualType,
                              typeParams,
                              boundVarSeq0, boundVarSeq1,
                              subst);
        } catch (UnificationFailedException) {
          tc.Error(actualArgs[i],
                   "invalid type for argument {0} in {1}: {2} (expected: {3})",
                   i, opName, actualArgs[i].Type,
                   // we insert the type parameters that have already been
                   // chosen to get a more precise error message
                   formalArgs[i].Substitute(subst));
          // the bound variable sequences should be empty ...
          // so that we can continue with the unification
          Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0);
        }
      }
      
      if (formalOuts != null) {
        for (int i = 0; i < formalOuts.Length; ++i) {
          try {
            Type! actualType = cce.NonNull((!)actualOuts[i]).Type;
            // if the type variables to be matched occur in the actual
            // argument types, something has gone very wrong
            Contract.Assert(forall{TypeVariable! var in typeParams);
                          !actualType.FreeVariables.Has(var)};
            formalOuts[i].Unify(actualType,
                                typeParams,
                                boundVarSeq0, boundVarSeq1,
                                subst);
          } catch (UnificationFailedException) {
            tc.Error(actualOuts[i],
                     "invalid type for result {0} in {1}: {2} (expected: {3})",
                     i, opName, actualOuts[i].Type,
                     // we insert the type parameters that have already been
                     // chosen to get a more precise error message
                     formalOuts[i].Substitute(subst));
            // the bound variable sequences should be empty ...
            // so that we can continue with the unification
            Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0);
          }
        }
      }

      // we only allow type parameters to be substituted
      Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var)));

      return subst;
    }
#else
    public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/
                  MatchArgumentTypes(List<TypeVariable>/*!*/ typeParams,
                                     List<Type>/*!*/ formalArgs,
                                     IList<Expr>/*!*/ actualArgs,
                                     List<Type> formalOuts,
                                     List<IdentifierExpr> actualOuts,
                                     string/*!*/ opName,
                                     TypecheckingContext/*!*/ tc) {
      Contract.Requires(typeParams != null);
      Contract.Requires(formalArgs != null);
      Contract.Requires(actualArgs != null);
      Contract.Requires(opName != null);
      Contract.Requires(tc != null);
      Contract.Requires(formalArgs.Count == actualArgs.Count);
      Contract.Requires((formalOuts == null) == (actualOuts == null));
      Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Count);
      Contract.Requires(tc == null || opName != null);//Redundant
      Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

      // requires "actualArgs" and "actualOuts" to have been type checked

      Dictionary<TypeVariable/*!*/, Type/*!*/> subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      foreach (TypeVariable/*!*/ tv in typeParams) {
        Contract.Assert(tv != null);
        TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
        subst.Add(tv, proxy);
      }

      for (int i = 0; i < formalArgs.Count; i++) {
        Type formal = formalArgs[i].Substitute(subst);
        Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type);
        // if the type variables to be matched occur in the actual
        // argument types, something has gone very wrong
        Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index])));

        if (!formal.Unify(actual)) {
          Contract.Assume(tc != null);  // caller expected no errors
          Contract.Assert(opName != null);  // follows from precondition
          tc.Error(cce.NonNull(actualArgs[i]),
                   "invalid type for argument {0} in {1}: {2} (expected: {3})",
                   i, opName, actual, formalArgs[i]);
        }
      }

      if (formalOuts != null) {
        for (int i = 0; i < formalOuts.Count; ++i) {
          Type formal = formalOuts[i].Substitute(subst);
          Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type);
          // if the type variables to be matched occur in the actual
          // argument types, something has gone very wrong
          Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !actual.FreeVariables.Contains(typeParams[var])));

          if (!formal.Unify(actual)) {
            Contract.Assume(tc != null);  // caller expected no errors
            Contract.Assert(opName != null);  // follows from precondition
            tc.Error(actualOuts[i],
                     "invalid type for out-parameter {0} in {1}: {2} (expected: {3})",
                     i, opName, actual, formal);
          }
        }
      }

      return subst;
    }
#endif

    //------------  Match formal argument types of a function or map
    //------------  on concrete types, substitute the result into the
    //------------  result type. Null is returned for type errors

    public static List<Type> CheckArgumentTypes(List<TypeVariable>/*!*/ typeParams,
                                             out List<Type/*!*/>/*!*/ actualTypeParams,
                                             List<Type>/*!*/ formalIns,
                                             IList<Expr>/*!*/ actualIns,
                                             List<Type>/*!*/ formalOuts,
                                             List<IdentifierExpr> actualOuts,
                                             IToken/*!*/ typeCheckingSubject,
                                             string/*!*/ opName,
                                             TypecheckingContext/*!*/ tc)
      // requires "actualIns" and "actualOuts" to have been type checked
    {
      Contract.Requires(typeParams != null);
      
      Contract.Requires(formalIns != null);
      Contract.Requires(formalOuts != null);
      Contract.Requires(actualIns != null);
      Contract.Requires(typeCheckingSubject != null);
      Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));
      actualTypeParams = new List<Type/*!*/>();

      if (formalIns.Count != actualIns.Count) {
        tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",
                 opName, actualIns.Count);
        // if there are no type parameters, we can still return the result
        // type and hope that the type checking proceeds
        return typeParams.Count == 0 ? formalOuts : null;
      } else if (actualOuts != null && formalOuts.Count != actualOuts.Count) {
        tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",
                 opName, actualOuts.Count);
        // if there are no type parameters, we can still return the result
        // type and hope that the type checking proceeds
        actualTypeParams = new List<Type>();
        return typeParams.Count == 0 ? formalOuts : null;
      }

      int previousErrorCount = tc.ErrorCount;
      IDictionary<TypeVariable/*!*/, Type/*!*/> subst =
        MatchArgumentTypes(typeParams, formalIns, actualIns,
                           actualOuts != null ? formalOuts : null, actualOuts, opName, tc);
      Contract.Assert(cce.NonNullDictionaryAndValues(subst));
      foreach (TypeVariable/*!*/ var in typeParams) {
        Contract.Assert(var != null);
        actualTypeParams.Add(subst[var]);
      }

      List<Type>/*!*/ actualResults = new List<Type>();
      foreach (Type/*!*/ t in formalOuts) {
        Contract.Assert(t != null);
        actualResults.Add(t.Substitute(subst));
      }
      List<TypeVariable> resultFreeVars = FreeVariablesIn(actualResults);
      if (previousErrorCount != tc.ErrorCount) {
        // errors occured when matching the formal arguments
        // in case we have been able to substitute all type parameters,
        // we can still return the result type and hope that the
        // type checking proceeds in a meaningful manner
        if (typeParams.All(param => !resultFreeVars.Contains(param)))
          return actualResults;
        else
          // otherwise there is no point in returning the result type,
          // type checking would only get confused even further
          return null;
      }

      Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !resultFreeVars.Contains(typeParams[index])));
      return actualResults;
    }

    ///////////////////////////////////////////////////////////////////////////

    // about the same as Type.CheckArgumentTypes, but without
    // detailed error reports
    public static Type/*!*/ InferValueType(List<TypeVariable>/*!*/ typeParams,
                                       List<Type>/*!*/ formalArgs,
                                       Type/*!*/ formalResult,
                                       List<Type>/*!*/ actualArgs) {
      Contract.Requires(typeParams != null);
      Contract.Requires(formalArgs != null);
      Contract.Requires(formalResult != null);
      Contract.Requires(actualArgs != null);
      Contract.Ensures(Contract.Result<Type>() != null);

      IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
        InferTypeParameters(typeParams, formalArgs, actualArgs);
      Contract.Assert(cce.NonNullDictionaryAndValues(subst));

      Type/*!*/ res = formalResult.Substitute(subst);
      Contract.Assert(res != null);
      // all type parameters have to be substituted with concrete types
      List<TypeVariable>/*!*/ resFreeVars = res.FreeVariables;
      Contract.Assert(resFreeVars != null);
      Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !resFreeVars.Contains(typeParams[var])));
      return res;
    }

#if OLD_UNIFICATION
    public static IDictionary<TypeVariable!, Type!>!
                  InferTypeParameters(List<TypeVariable>! typeParams,
                                      List<Type>! formalArgs,
                                      List<Type>! actualArgs)
      {
 Contract.Requires(formalArgs.Length == actualArgs.Length);
      
      List<TypeVariable>! boundVarSeq0 = new List<TypeVariable> ();
      List<TypeVariable>! boundVarSeq1 = new List<TypeVariable> ();
      Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();

      for (int i = 0; i < formalArgs.Length; ++i) {
        try {
          Contract.Assert(forall{TypeVariable! var in typeParams);
                        !actualArgs[i].FreeVariables.Has(var)};
          formalArgs[i].Unify(actualArgs[i], typeParams,
                              boundVarSeq0, boundVarSeq1, subst);
        } catch (UnificationFailedException) {
          System.Diagnostics.Debug.Fail("Type unification failed: " +
                                        formalArgs[i] + " vs " + actualArgs[i]);
        }
      }

      // we only allow type parameters to be substituted
      Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var)));
      return subst;
    }
#else
    /// <summary>
    /// like Type.CheckArgumentTypes, but assumes no errors
    /// (and only does arguments, not results; and takes actuals as List<Type>, not List<Expr>)
    /// </summary>
    public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/
                  InferTypeParameters(List<TypeVariable>/*!*/ typeParams,
                                      List<Type>/*!*/ formalArgs,
                                      List<Type>/*!*/ actualArgs) {
      Contract.Requires(typeParams != null);
      Contract.Requires(formalArgs != null);
      Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count);
      Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

      
      List<Type> proxies = new List<Type>();
      Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      foreach (TypeVariable/*!*/ tv in typeParams) {
        Contract.Assert(tv != null);
        TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
        proxies.Add(proxy);
        subst.Add(tv, proxy);
      }

      for (int i = 0; i < formalArgs.Count; i++) {
        Type formal = formalArgs[i].Substitute(subst);
        Type actual = actualArgs[i];
        // if the type variables to be matched occur in the actual
        // argument types, something has gone very wrong
        Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index])));

        if (!formal.Unify(actual)) {
          Contract.Assume(false);  // caller expected no errors
        }
      }

      return subst;
    }
#endif

    //-----------  Helper methods to deal with bound type variables  ---------------

    public static void EmitOptionalTypeParams(TokenTextWriter stream, List<TypeVariable> typeParams) {
      Contract.Requires(typeParams != null);
      Contract.Requires(stream != null);
      if (typeParams.Count > 0) {
        stream.Write("<");
        typeParams.Emit(stream, ","); // default binding strength of 0 is ok
        stream.Write(">");
      }
    }

    // Sort the type parameters according to the order of occurrence in the argument types
    public static List<TypeVariable>/*!*/ SortTypeParams(List<TypeVariable>/*!*/ typeParams, List<Type>/*!*/ argumentTypes, Type resultType) {
      Contract.Requires(typeParams != null);
      Contract.Requires(argumentTypes != null);
      Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

      Contract.Ensures(Contract.Result<List<TypeVariable>>().Count == typeParams.Count);
      if (typeParams.Count == 0) {
        return typeParams;
      }

      List<TypeVariable> freeVarsInUse = FreeVariablesIn(argumentTypes);
      if (resultType != null) {
        freeVarsInUse.AppendWithoutDups(resultType.FreeVariables);
      }
      // "freeVarsInUse" is already sorted, but it may contain type variables not in "typeParams".
      // So, project "freeVarsInUse" onto "typeParams":
      List<TypeVariable> sortedTypeParams = new List<TypeVariable>();
      foreach (TypeVariable/*!*/ var in freeVarsInUse) {
        Contract.Assert(var != null);
        if (typeParams.Contains(var)) {
          sortedTypeParams.Add(var);
        }
      }

      if (sortedTypeParams.Count < typeParams.Count)
        // add the type parameters not mentioned in "argumentTypes" in
        // the end of the list (this can happen for quantifiers)
        sortedTypeParams.AppendWithoutDups(typeParams);

      return sortedTypeParams;
    }

    // Check that each of the type parameters occurs in at least one argument type.
    // Return true if some type parameters appear only among "moreArgumentTypes" and
    // not in "argumentTypes".
    [Pure]
    public static bool CheckBoundVariableOccurrences(List<TypeVariable>/*!*/ typeParams,
                                                     List<Type>/*!*/ argumentTypes,
                                                     List<Type> moreArgumentTypes,
                                                     IToken/*!*/ resolutionSubject,
                                                     string/*!*/ subjectName,
                                                     ResolutionContext/*!*/ rc) {
      Contract.Requires(typeParams != null);
      Contract.Requires(argumentTypes != null);
      Contract.Requires(resolutionSubject != null);
      Contract.Requires(subjectName != null);
      Contract.Requires(rc != null);
      List<TypeVariable> freeVarsInArgs = FreeVariablesIn(argumentTypes);
      List<TypeVariable> moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes);
      bool someTypeParamsAppearOnlyAmongMo = false;
      foreach (TypeVariable/*!*/ var in typeParams) {
        Contract.Assert(var != null);
        if (rc.LookUpTypeBinder(var.Name) == var)  // avoid to complain twice about variables that are bound multiple times
        {
          if (freeVarsInArgs.Contains(var)) {
            // cool
          } else if (moFreeVarsInArgs != null && moFreeVarsInArgs.Contains(var)) {
            someTypeParamsAppearOnlyAmongMo = true;
          } else {
            rc.Error(resolutionSubject,
                 "type variable must occur in {0}: {1}",
                 subjectName, var);
          }
        }
      }
      return someTypeParamsAppearOnlyAmongMo;
    }

    [Pure]
    public static List<TypeVariable> FreeVariablesIn(List<Type> arguments) {
      Contract.Requires(arguments != null);
      Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
      List<TypeVariable>/*!*/ res = new List<TypeVariable>();
      foreach (Type/*!*/ t in arguments) {
        Contract.Assert(t != null);
        res.AppendWithoutDups(t.FreeVariables);
      }
      return res;
    }
  }
  [ContractClassFor(typeof(Type))]
  public abstract class TypeContracts : Type {
    public TypeContracts() :base(null){

    }
    public override List<TypeProxy> FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        throw new NotImplementedException();
      }
    }
    public override List<TypeVariable> FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
        throw new NotImplementedException();
      }
    }
    public override Type Clone(IDictionary<TypeVariable, TypeVariable> varMap) {
      Contract.Requires(cce.NonNullDictionaryAndValues(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);

      throw new NotImplementedException();
    }
    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);

      throw new NotImplementedException();
    }
    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      Contract.Requires(stream != null);
      throw new NotImplementedException();
    }
    public override bool Equals(Type that, List<TypeVariable> thisBoundVariables, List<TypeVariable> thatBoundVariables) {
      Contract.Requires(that != null);
      Contract.Requires(thisBoundVariables != null);
      Contract.Requires(thatBoundVariables != null);
      throw new NotImplementedException();
    }
    public override bool Unify(Type that, List<TypeVariable> unifiableVariables, IDictionary<TypeVariable, Type> unifier) {
      Contract.Requires(that != null);
      Contract.Requires(unifiableVariables != null);
      Contract.Requires(cce.NonNullDictionaryAndValues(unifier));
      Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Contains(key)));
      Contract.Requires(IsIdempotent(unifier));
      throw new NotImplementedException();
    }
    public override Type Substitute(IDictionary<TypeVariable, Type> subst) {
      Contract.Requires(cce.NonNullDictionaryAndValues(subst));
      Contract.Ensures(Contract.Result<Type>() != null);

      throw new NotImplementedException();
    }
    public override Type ResolveType(ResolutionContext rc) {
      Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);

      throw new NotImplementedException();
    }
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      Contract.Requires(boundVariables != null);
      throw new NotImplementedException();
    }
  }
  //=====================================================================

  public class BasicType : Type {
    public readonly SimpleType T;
    public BasicType(IToken/*!*/ token, SimpleType t)
      : base(token) {
      Contract.Requires(token != null);
      T = t;
    }
    public BasicType(SimpleType t)
      : base(Token.NoToken) {
      T = t;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively.

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      // BasicTypes are immutable anyway, we do not clone
      return this;
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      // no parentheses are necessary for basic types
      stream.SetToken(this);
      stream.Write("{0}", this);
    }

    [Pure]
    public override string ToString() {
      Contract.Ensures(Contract.Result<string>() != null);
      switch (T) {
        case SimpleType.Int:
          return "int";
        case SimpleType.Real:
          return "real";
        case SimpleType.Bool:
          return "bool";
      }
      Debug.Assert(false, "bad type " + T);
      {
        Contract.Assert(false);
        throw new cce.UnreachableException();
      } // make compiler happy
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      // shortcut
      Type thatType = that as Type;
      if (thatType == null)
        return false;
      BasicType thatBasicType = TypeProxy.FollowProxy(thatType.Expanded) as BasicType;
      return thatBasicType != null && this.T == thatBasicType.T;
    }

    [Pure]
    public override bool Equals(Type that, List<TypeVariable> thisBoundVariables, List<TypeVariable> thatBoundVariables) {
      //Contract.Requires(thatBoundVariables != null);
      //Contract.Requires(thisBoundVariables != null);
      //Contract.Requires(that != null);
      return this.Equals(that);
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type that, List<TypeVariable> unifiableVariables, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(that != null);
      //Contract.Requires(cce.NonNullElements(unifier));
      // an idempotent substitution that describes the
      // unification result up to a certain point

      that = that.Expanded;
      if (that is TypeProxy || that is TypeVariable) {
        return that.Unify(this, unifiableVariables, unifier);
      } else {
        return this.Equals(that);
      }
    }

#if OLD_UNIFICATION
    public override void Unify(Type! that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!>! result) {
      that = that.Expanded;
      if (that is TypeVariable) {
        that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result);
      } else {
        if (!this.Equals(that))
          throw UNIFICATION_FAILED;
      }
    }
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      return this.T.GetHashCode();
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      // nothing to resolve
      return this;
    }

    // determine the free variables in a type, in the order in which the variables occur
    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

        return new List<TypeVariable>();  // basic type are closed
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        return new List<TypeProxy/*!*/>();
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsBasic {
      get {
        return true;
      }
    }
    public override bool IsInt {
      get {
        return this.T == SimpleType.Int;
      }
    }
    public override bool IsReal {
      get {
        return this.T == SimpleType.Real;
      }
    }
    public override bool IsBool {
      get {
        return this.T == SimpleType.Bool;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitBasicType(this);
    }
  }

  //=====================================================================

  //Note that the functions in this class were directly copied from the BV class just below
  public class FloatType : Type { 
    public readonly int Significand; //Size of Significand in bits
    public readonly int Exponent; //Size of exponent in bits

    public FloatType(IToken token, int significand, int exponent)
      : base(token) {
      Contract.Requires(token != null);
      Significand = significand;
      Exponent = exponent;
    }

    public FloatType(int significand, int exponent)
      : base(Token.NoToken) {
      Significand = significand;
      Exponent = exponent;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively.

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap)
    {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      // FloatTypes are immutable anyway, we do not clone
      return this;
    }

    public override Type CloneUnresolved()
    {
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength)
    {
      //Contract.Requires(stream != null);
      // no parentheses are necessary for bitvector-types
      stream.SetToken(this);
      stream.Write("{0}", this);
    }

    public override string ToString()
    {
      Contract.Ensures(Contract.Result<string>() != null);
      return "float" + Significand + "e" + Exponent;
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type/*!*/ that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables)
    {
      FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType;
      return thatFloatType != null && this.Significand == thatFloatType.Significand && this.Exponent == thatFloatType.Exponent;
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
      // an idempotent substitution that describes the
      // unification result up to a certain point
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier)
    {
      //Contract.Requires(that != null);
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(cce.NonNullElements(unifier));
      that = that.Expanded;
      if (that is TypeProxy || that is TypeVariable) {
        return that.Unify(this, unifiableVariables, unifier); 
      }
      else {
        return this.Equals(that); 
      }
    }

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst)
    {
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables)
    {
      return this.Significand.GetHashCode() + this.Exponent.GetHashCode();
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc)
    {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      // nothing to resolve
      return this;
    }

    // determine the free variables in a type, in the order in which the variables occur
    public override List<TypeVariable>/*!*/ FreeVariables
    {
      get
      {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

        return new List<TypeVariable>();  // bitvector-type are closed
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies
    {
      get
      {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        return new List<TypeProxy/*!*/>();
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsFloat {
      get {
        return true;
      }
    }
    public override int FloatSignificand {
      get {
        return Significand;
      }
    }
    public override int FloatExponent {
      get {
        return Exponent;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor)
    {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitFloatType(this);
    }

  }

  //=====================================================================

  public class BvType : Type {
    public readonly int Bits;

    public BvType(IToken token, int bits)
      : base(token) {
      Contract.Requires(token != null);
      Bits = bits;
    }

    public BvType(int bits)
      : base(Token.NoToken) {
      Bits = bits;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively.

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      // BvTypes are immutable anyway, we do not clone
      return this;
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      // no parentheses are necessary for bitvector-types
      stream.SetToken(this);
      stream.Write("{0}", this);
    }

    [Pure]
    public override string ToString() {
      Contract.Ensures(Contract.Result<string>() != null);
      return "bv" + Bits;
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type/*!*/ that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables) {
      //Contract.Requires(thisBoundVariables != null);
      //Contract.Requires(thatBoundVariables != null);
      //Contract.Requires(that != null);
      BvType thatBvType = TypeProxy.FollowProxy(that.Expanded) as BvType;
      return thatBvType != null && this.Bits == thatBvType.Bits;
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
      // an idempotent substitution that describes the
      // unification result up to a certain point
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
      //Contract.Requires(that != null);
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(cce.NonNullElements(unifier));
      that = that.Expanded;
      if (that is TypeProxy || that is TypeVariable) {
        return that.Unify(this, unifiableVariables, unifier);
      } else {
        return this.Equals(that);
      }
    }

#if OLD_UNIFICATION
    public override void Unify(Type that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!> result){
Contract.Requires(result != null);
Contract.Requires(that != null);
      that = that.Expanded;
      if (that is TypeVariable) {
        that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result);
      } else {
        if (!this.Equals(that))
          throw UNIFICATION_FAILED;
      }
    }
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      return this.Bits.GetHashCode();
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      // nothing to resolve
      return this;
    }

    // determine the free variables in a type, in the order in which the variables occur
    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

        return new List<TypeVariable>();  // bitvector-type are closed
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        return new List<TypeProxy/*!*/>();
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsBv {
      get {
        return true;
      }
    }
    public override int BvBits {
      get {
        return Bits;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitBvType(this);
    }
  }

  //=====================================================================

  // An AST node containing an identifier and a sequence of type arguments, which
  // will be turned either into a TypeVariable, into a CtorType or into a BvType
  // during the resolution phase
  public class UnresolvedTypeIdentifier : Type {
    public readonly string/*!*/ Name;
    public readonly List<Type>/*!*/ Arguments;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Name != null);
      Contract.Invariant(Arguments != null);
    }


    public UnresolvedTypeIdentifier(IToken token, string name)
      : this(token, name, new List<Type>()) {
      Contract.Requires(name != null);
      Contract.Requires(token != null);
    }

    public UnresolvedTypeIdentifier(IToken token, string name, List<Type> arguments)
      : base(token) {
      Contract.Requires(arguments != null);
      Contract.Requires(name != null);
      Contract.Requires(token != null);
      this.Name = name;
      this.Arguments = arguments;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.Clone(varMap));
      }
      return new UnresolvedTypeIdentifier(tok, Name, newArgs);
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.CloneUnresolved());
      }
      return new UnresolvedTypeIdentifier(tok, Name, newArgs);
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables) {
      //Contract.Requires(thisBoundVariables != null);
      //Contract.Requires(thatBoundVariables != null);
      //Contract.Requires(that != null);
      System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Equals should never be called");
      return false; // to make the compiler happy      
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type that,
                               List<TypeVariable>/*!*/ unifiableVariables,
                               IDictionary<TypeVariable/*!*/, Type/*!*/> result) {
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(cce.NonNullElements(result));
      //Contract.Requires(that != null);
      {
        Contract.Assert(false);
        throw new cce.UnreachableException();
      } // UnresolvedTypeIdentifier.Unify should never be called
    }

#if OLD_UNIFICATION
    public override void Unify(Type that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!> result){
Contract.Requires(result != null);
Contract.Requires(that != null);
      System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Unify should never be called");
    }
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      {
        Contract.Assert(false);
        throw new cce.UnreachableException();
      } // UnresolvedTypeIdentifier.Substitute should never be called
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      {
        Contract.Assert(false);
        throw new cce.UnreachableException();
      } // UnresolvedTypeIdentifier.GetHashCode should never be called
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      // first case: the type name denotes a bitvector-type or float-type
      if (Name.StartsWith("bv") && Name.Length > 2) {
        bool is_bv = true;
        for (int i = 2; i < Name.Length; ++i) {
          if (!char.IsDigit(Name[i])) {
            is_bv = false;
            break;
          }
        }
        if (is_bv) {
          if (Arguments.Count > 0) {
            rc.Error(this,
                     "bitvector types must not be applied to arguments: {0}",
                     Name);
          }
          return new BvType(tok, int.Parse(Name.Substring(2)));
        }
      }

      if (Name.StartsWith("float") && Name.Length > 5)
      {
        bool is_float = true;
        int i = 5;
        for (; is_float && Name[i] != 'e'; i++)
          if (i >= Name.Length-1 || !char.IsDigit(Name[i])) //There must be an e
            is_float = false;
        int mid = i;
        i++;
        for (; i < Name.Length && is_float; i++)
          if (!char.IsDigit(Name[i]))
            is_float = false;
        if (is_float) {
          if (Arguments.Count > 0) {
            rc.Error(this,
                     "float types must not be applied to arguments: {0}",
                     Name);
          }
          return new FloatType(tok, int.Parse(Name.Substring(5, mid-5)), int.Parse(Name.Substring(mid+1)));
        }
      }

      // second case: the identifier is resolved to a type variable
      TypeVariable var = rc.LookUpTypeBinder(Name);
      if (var != null) {
        if (Arguments.Count > 0) {
          rc.Error(this,
                   "type variables must not be applied to arguments: {0}",
                   var);
        }
        return var;
      }

      // third case: the identifier denotes a type constructor and we
      // recursively resolve the arguments
      TypeCtorDecl ctorDecl = rc.LookUpType(Name);
      if (ctorDecl != null) {
        if (Arguments.Count != ctorDecl.Arity) {
          rc.Error(this,
                   "type constructor received wrong number of arguments: {0}",
                   ctorDecl);
          return this;
        }
        return new CtorType(tok, ctorDecl, ResolveArguments(rc));
      }

      // fourth case: the identifier denotes a type synonym
      TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name);
      if (synDecl != null) {
        if (Arguments.Count != synDecl.TypeParameters.Count) {
          rc.Error(this,
                   "type synonym received wrong number of arguments: {0}",
                   synDecl);
          return this;
        }
        List<Type>/*!*/ resolvedArgs = ResolveArguments(rc);
        Contract.Assert(resolvedArgs != null);

        return new TypeSynonymAnnotation(this.tok, synDecl, resolvedArgs);

      }

      // otherwise: this name is not declared anywhere
      rc.Error(this, "undeclared type: {0}", Name);
      return this;
    }

    private List<Type> ResolveArguments(ResolutionContext rc) {
      Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<List<Type>>() != null);
      List<Type>/*!*/ resolvedArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        resolvedArgs.Add(t.ResolveType(rc));
      }
      return resolvedArgs;
    }

    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

        return new List<TypeVariable>();
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        return new List<TypeProxy/*!*/>();
      }
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      stream.SetToken(this);
      // PR: should unresolved types be syntactically distinguished from resolved types?
      CtorType.EmitCtorType(this.Name, Arguments, stream, contextBindingStrength);
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsUnresolved {
      get {
        return true;
      }
    }
    public override UnresolvedTypeIdentifier/*!*/ AsUnresolved {
      get {
        Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);
        return this;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitUnresolvedTypeIdentifier(this);
    }
  }

  //=====================================================================

  public class TypeVariable : Type {
    public readonly string/*!*/ Name;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Name != null);
    }


    public TypeVariable(IToken token, string name)
      : base(token) {
      Contract.Requires(name != null);
      Contract.Requires(token != null);
      this.Name = name;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      // if this variable is mapped to some new variable, we take the new one
      // otherwise, return this
      TypeVariable res;
      varMap.TryGetValue(this, out res);
      if (res == null)
        return this;
      else
        return res;
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      return this;
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables) {
      //Contract.Requires(thisBoundVariables != null);
      //Contract.Requires(thatBoundVariables != null);
      //Contract.Requires(that != null);
      TypeVariable thatAsTypeVar = TypeProxy.FollowProxy(that.Expanded) as TypeVariable;

      if (thatAsTypeVar == null)
        return false;

      int thisIndex = thisBoundVariables.LastIndexOf(this);
      int thatIndex = thatBoundVariables.LastIndexOf(thatAsTypeVar);
      return (thisIndex >= 0 && thisIndex == thatIndex) ||
             (thisIndex == -1 && thatIndex == -1 &&
              Object.ReferenceEquals(this, thatAsTypeVar));
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
      // an idempotent substitution that describes the
      // unification result up to a certain point
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
      //Contract.Requires(that != null);
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(cce.NonNullElements(unifier));
      that = that.Expanded;
      if (that is TypeProxy && !(that is ConstrainedProxy))
        return that.Unify(this, unifiableVariables, unifier);

      if (this.Equals(that))
        return true;

      if (unifiableVariables.Contains(this)) {
        Type previousSubst;
        unifier.TryGetValue(this, out previousSubst);
        if (previousSubst == null) {
          return addSubstitution(unifier, that);
        } else {
          // we have to unify the old instantiation with the new one
          return previousSubst.Unify(that, unifiableVariables, unifier);
        }
      }

      // this cannot be instantiated with anything
      // but that possibly can ...

      TypeVariable tv = that as TypeVariable;

      return tv != null &&
             unifiableVariables.Contains(tv) &&
             that.Unify(this, unifiableVariables, unifier);
    }

    // TODO: the following might cause problems, because when applying substitutions
    // to type proxies the substitutions are not propagated to the proxy
    // constraints (right now at least)
    private bool addSubstitution(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ oldSolution,
      // the type that "this" is instantiated with
                                 Type/*!*/ newSubst) {
      Contract.Requires(cce.NonNullDictionaryAndValues(oldSolution));
      Contract.Requires(newSubst != null);
      Contract.Requires(!oldSolution.ContainsKey(this));

      Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ newMapping = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      // apply the old (idempotent) substitution to the new instantiation
      Type/*!*/ substSubst = newSubst.Substitute(oldSolution);
      Contract.Assert(substSubst != null);
      // occurs check
      if (substSubst.FreeVariables.Contains(this))
        return false;
      newMapping.Add(this, substSubst);

      // apply the new substitution to the old ones to ensure idempotence
      List<TypeVariable/*!*/>/*!*/ keys = new List<TypeVariable/*!*/>();
      keys.AddRange(oldSolution.Keys);
      foreach (TypeVariable/*!*/ var in keys) {
        Contract.Assert(var != null);
        oldSolution[var] = oldSolution[var].Substitute(newMapping);
      }
      oldSolution.Add(this, substSubst);

      Contract.Assert(IsIdempotent(oldSolution));
      return true;
    }

#if OLD_UNIFICATION
    public override void Unify(Type that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!> result){
Contract.Requires(result != null);
Contract.Requires(that != null);
      that = that.Expanded;
      int thisIndex = thisBoundVariables.LastIndexOf(this);
      if (thisIndex == -1) {
        // this is not a bound variable and can possibly be matched on that
        // that must not contain any bound variables
        List<TypeVariable>! thatFreeVars = that.FreeVariables;
        if (thatBoundVariables.Any(var=> thatFreeVars.Has(var)))
          throw UNIFICATION_FAILED;

        // otherwise, in case that is a typevariable it cannot be bound and
        // we can just check for equality
        if (this.Equals(that))
          return;

        if (!unifiableVariables.Has(this)) {
          // this cannot be instantiated with anything
          // but that possibly can ...
          if ((that is TypeVariable) &&
               unifiableVariables.Has(that as TypeVariable)) {
            that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result);
            return;
          } else {
            throw UNIFICATION_FAILED;
          }
        }

        Type previousSubst;
        result.TryGetValue(this, out previousSubst);
        if (previousSubst == null) {
          addSubstitution(result, that);
        } else {
          // we have to unify the old instantiation with the new one
          previousSubst.Unify(that, unifiableVariables, thisBoundVariables, thatBoundVariables, result);
        }
      } else {
        // this is a bound variable, that also has to be one (with the same index)
        if (!(that is TypeVariable) ||
            thatBoundVariables.LastIndexOf(that) != thisIndex)
          throw UNIFICATION_FAILED;
      }      
    }

#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      Type res;
      if (subst.TryGetValue(this, out res)) {
        Contract.Assert(res != null);
        return res;
      } else {
        return this;
      }
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      int thisIndex = boundVariables.LastIndexOf(this);
      if (thisIndex == -1)
        return GetBaseHashCode();
      return thisIndex * 27473671;
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      // never put parentheses around variables
      stream.SetToken(this);
      stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      //Contract.Ensures(Contract.Result<Type>() != null);
      // nothing to resolve
      return this;
    }

    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
        return new List<TypeVariable> { this };
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        return new List<TypeProxy/*!*/>();
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsVariable {
      get {
        return true;
      }
    }
    public override TypeVariable/*!*/ AsVariable {
      get {
        Contract.Ensures(Contract.Result<TypeVariable>() != null);
        return this;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      //Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitTypeVariable(this);
    }
  }

  //=====================================================================

  public class TypeProxy : Type {
    static int proxies = 0;
    protected readonly string/*!*/ Name;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Name != null);
    }


    public TypeProxy(IToken token, string givenName)
      : this(token, givenName, "proxy") {
      Contract.Requires(givenName != null);
      Contract.Requires(token != null);
    }

    protected TypeProxy(IToken token, string givenName, string kind)
      : base(token) {
      Contract.Requires(kind != null);
      Contract.Requires(givenName != null);
      Contract.Requires(token != null);
      Name = givenName + "$" + kind + "#" + proxies;
      proxies++;
    }

    private Type proxyFor;
    public Type ProxyFor {
      // apply path shortening, and then return the value of proxyFor
      get {
        TypeProxy anotherProxy = proxyFor as TypeProxy;
        if (anotherProxy != null && anotherProxy.proxyFor != null) {
          // apply path shortening by bypassing "anotherProxy" (and possibly others)
          proxyFor = anotherProxy.ProxyFor;
          Contract.Assert(proxyFor != null);
        }
        return proxyFor;
      }
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Everything)]
    public static Type FollowProxy(Type t) {
      Contract.Requires(t != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Ensures(!(Contract.Result<Type>() is TypeProxy) || ((TypeProxy)Contract.Result<Type>()).proxyFor == null);
      if (t is TypeProxy) {
        Type p = ((TypeProxy)t).ProxyFor;
        if (p != null) {
          return p;
        }
      }
      return t;
    }

    protected void DefineProxy(Type ty) {
      Contract.Requires(ty != null);
      Contract.Requires(ProxyFor == null);
      // follow ty down to the leaf level, so that we can avoid creating a cycle
      ty = FollowProxy(ty);
      if (!object.ReferenceEquals(this, ty)) {
        proxyFor = ty;
      }
    }

    //-----------  Cloning  ----------------------------------

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.Clone(varMap);
      } else {
        return new TypeProxy(this.tok, this.Name);  // the clone will have a name that ends with $proxy<n>$proxy<m>
      }
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      return new TypeProxy(this.tok, this.Name);  // the clone will have a name that ends with $proxy<n>$proxy<m>
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables) {
      //Contract.Requires(thisBoundVariables != null);
      //Contract.Requires(thatBoundVariables != null);
      //Contract.Requires(that != null);
      if (object.ReferenceEquals(this, that)) {
        return true;
      }
      Type p = ProxyFor;
      if (p != null) {
        return p.Equals(that, thisBoundVariables, thatBoundVariables);
      } else {
        // This proxy could be made to be equal to anything, so what to return?
        return false;
      }
    }

    //-----------  Unification of types  -----------

    // determine whether the occurs check fails: this is a strict subtype of that
    protected bool ReallyOccursIn(Type that) {
      Contract.Requires(that != null);
      that = FollowProxy(that.Expanded);
      return that.FreeProxies.Contains(this) &&
             (that.IsCtor || that.IsMap && this != that && this.ProxyFor != that);
    }

    public override bool Unify(Type that,
                               List<TypeVariable>/*!*/ unifiableVariables,
                               IDictionary<TypeVariable/*!*/, Type/*!*/> result) {
      //Contract.Requires(cce.NonNullElements(result));
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(that != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.Unify(that, unifiableVariables, result);
      } else {
        // unify this with that
        if (this.ReallyOccursIn(that))
          return false;
        DefineProxy(that.Expanded);
        return true;
      }
    }

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.Substitute(subst);
      } else {
        return this;
      }
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.GetHashCode(boundVariables);
      } else {
        return GetBaseHashCode();
      }
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      Type p = ProxyFor;
      if (p != null) {
        p.Emit(stream, contextBindingStrength);
      } else {
        // no need for parentheses
        stream.SetToken(this);
        stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
      }
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.ResolveType(rc);
      } else {
        return this;
      }
    }

    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

        Type p = ProxyFor;
        if (p != null) {
          return p.FreeVariables;
        } else {
          return new List<TypeVariable>();
        }
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        Type p = ProxyFor;
        if (p != null) {
          return p.FreeProxies;
        } else {
          List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*/>();
          res.Add(this);
          return res;
        }
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsBasic {
      get {
        Type p = ProxyFor;
        return p != null && p.IsBasic;
      }
    }
    public override bool IsInt {
      get {
        Type p = ProxyFor;
        return p != null && p.IsInt;
      }
    }
    public override bool IsReal {
      get {
        Type p = ProxyFor;
        return p != null && p.IsReal;
      }
    }
    public override bool IsFloat {
      get {
        Type p = ProxyFor;
        return p != null && p.IsFloat;
      }
    }
    public override bool IsBool {
      get {
        Type p = ProxyFor;
        return p != null && p.IsBool;
      }
    }

    public override bool IsVariable {
      get {
        Type p = ProxyFor;
        return p != null && p.IsVariable;
      }
    }
    public override TypeVariable/*!*/ AsVariable {
      get {
        Contract.Ensures(Contract.Result<TypeVariable>() != null);

        Type p = ProxyFor;
        Contract.Assume(p != null);
        return p.AsVariable;
      }
    }

    public override bool IsCtor {
      get {
        Type p = ProxyFor;
        return p != null && p.IsCtor;
      }
    }
    public override CtorType/*!*/ AsCtor {
      get {
        Contract.Ensures(Contract.Result<CtorType>() != null);

        Type p = ProxyFor;
        Contract.Assume(p != null);
        return p.AsCtor;
      }
    }
    public override bool IsMap {
      get {
        Type p = ProxyFor;
        return p != null && p.IsMap;
      }
    }
    public override MapType/*!*/ AsMap {
      get {
        Contract.Ensures(Contract.Result<MapType>() != null);

        Type p = ProxyFor;
        Contract.Assume(p != null);
        return p.AsMap;
      }
    }
    public override int MapArity {
      get {
        Type p = ProxyFor;
        Contract.Assume(p != null);
        return p.MapArity;
      }
    }
    public override bool IsUnresolved {
      get {
        Type p = ProxyFor;
        return p != null && p.IsUnresolved;
      }
    }
    public override UnresolvedTypeIdentifier/*!*/ AsUnresolved {
      get {
        Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);

        Type p = ProxyFor;
        Contract.Assume(p != null);
        return p.AsUnresolved;
      }
    }

    public override bool IsBv {
      get {
        Type p = ProxyFor;
        return p != null && p.IsBv;
      }
    }
    public override int BvBits {
      get {
        Type p = ProxyFor;
        Contract.Assume(p != null);
        return p.BvBits;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitTypeProxy(this);
    }
  }

  public abstract class ConstrainedProxy : TypeProxy {
    protected ConstrainedProxy(IToken token, string givenName, string kind)
      : base(token, givenName, kind) {
      Contract.Requires(kind != null);
      Contract.Requires(givenName != null);
      Contract.Requires(token != null);
    }
  }

  /// <summary>
  /// Each instance of this class represents a set of bitvector types.  In particular, it represents
  /// a bitvector type bvN iff
  ///   minBits ATMOST N  and
  ///   foreach constraint (t0,t1), the types represented by t0 and t1 are bitvector types whose
  ///   number of bits add up to N.
  /// This means that the size of a BvTypeProxy p is constrained not only by p.minBits, but also
  /// by the size of various t0 and t1 types that are transitively part of BvTypeProxy constraints.
  /// If such a t0 or t1 were to get its ProxyFor field defined, then p would have to be further
  /// constrained too.  This doesn't seem like it would ever occur in a Boogie 2 program, because:
  ///   the only place where a BvTypeProxy with constraints can occur is as the type of a
  ///   BvConcatExpr, and
  ///   the types of all local variables are explicitly declared, which means that the types of
  ///   subexpressions of a BvConcatExpr are not going to change other than via the type of the
  ///   BvConcatExpr.
  /// So, this implementation of BvTypeProxy does not keep track of where a BvTypeProxy may occur
  /// transitively in some other BvTypeProxy's constraints.
  /// </summary>
  public class BvTypeProxy : ConstrainedProxy {
    public int MinBits;
    List<BvTypeConstraint/*!*/> constraints;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(constraints, true));
    }

    class BvTypeConstraint {
      public Type/*!*/ T0;
      public Type/*!*/ T1;
      public BvTypeConstraint(Type t0, Type t1) {
        Contract.Requires(t1 != null);
        Contract.Requires(t0 != null);
        Contract.Requires(t0.IsBv && t1.IsBv);
        T0 = t0;
        T1 = t1;
      }
    }

    public BvTypeProxy(IToken token, string name, int minBits)
      : base(token, name, "bv" + minBits + "proxy") {
      Contract.Requires(name != null);
      Contract.Requires(token != null);
      this.MinBits = minBits;
    }

    /// <summary>
    /// Requires that any further constraints to be placed on t0 and t1 go via the object to
    /// be constructed.
    /// </summary>
    public BvTypeProxy(IToken token, string name, Type t0, Type t1)
      : base(token, name, "bvproxy") {
      Contract.Requires(t1 != null);
      Contract.Requires(t0 != null);
      Contract.Requires(name != null);
      Contract.Requires(token != null);
      Contract.Requires(t0.IsBv && t1.IsBv);
      t0 = FollowProxy(t0);
      t1 = FollowProxy(t1);
      this.MinBits = MinBitsFor(t0) + MinBitsFor(t1);
      List<BvTypeConstraint/*!*/> list = new List<BvTypeConstraint/*!*/>();
      list.Add(new BvTypeConstraint(t0, t1));
      this.constraints = list;
    }

    /// <summary>
    /// Construct a BvTypeProxy like p, but with minBits.
    /// </summary>
    private BvTypeProxy(BvTypeProxy p, int minBits)
      : base(p.tok, p.Name, "") {
      Contract.Requires(p != null);
      this.MinBits = minBits;
      this.constraints = p.constraints;
    }

    private BvTypeProxy(IToken token, string name, int minBits, List<BvTypeConstraint/*!*/> constraints)
      : base(token, name, "") {
      Contract.Requires(cce.NonNullElements(constraints, true));
      Contract.Requires(name != null);
      Contract.Requires(token != null);
      this.MinBits = minBits;
      this.constraints = constraints;
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Everything)]
    private static int MinBitsFor(Type t) {
      Contract.Requires(t != null);
      Contract.Requires(t.IsBv);
      Contract.Ensures(0 <= Contract.Result<int>());

      if (t is TypeSynonymAnnotation) {
        return MinBitsFor(((TypeSynonymAnnotation)t).ExpandedType);
      }

      if (t is BvType) {
        return t.BvBits;
      } else {
        return ((BvTypeProxy)t).MinBits;
      }
    }

    //-----------  Cloning  ----------------------------------

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.Clone(varMap);
      } else {
        return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints);  // the clone will have a name that ends with $bvproxy<n>$bvproxy<m>
      }
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints);  // the clone will have a name that ends with $bvproxy<n>$bvproxy<m>
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type that,
                               List<TypeVariable> unifiableVariables,
                               IDictionary<TypeVariable, Type> result) {
      //Contract.Requires(cce.NonNullElements(result));
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(that != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.Unify(that, unifiableVariables, result);
      }

      // unify this with that, if possible
      that = that.Expanded;
      that = FollowProxy(that);

      if (this.ReallyOccursIn(that))
        return false;

      TypeVariable tv = that as TypeVariable;

      if (tv != null && unifiableVariables.Contains(tv))
        return that.Unify(this, unifiableVariables, result);

      if (object.ReferenceEquals(this, that)) {
        return true;
      } else if (that is BvType) {
        if (MinBits <= that.BvBits) {
          if (constraints != null) {
            foreach (BvTypeConstraint btc in constraints) {
              int minT1 = MinBitsFor(btc.T1);
              int left = IncreaseBits(btc.T0, that.BvBits - minT1);
              left = IncreaseBits(btc.T1, minT1 + left);
              Contract.Assert(left == 0);  // because it should always be possible to increase the total size of a BvTypeConstraint pair (t0,t1) arbitrarily
            }
          }
          DefineProxy(that);
          return true;
        }
      } else if (that is BvTypeProxy) {
        BvTypeProxy bt = (BvTypeProxy)that;
        // keep the proxy with the stronger constraint (that is, the higher minBits), but if either
        // has a constraints list, then concatenate both constraints lists and define the previous
        // proxies to the new one
        if (this.constraints != null || bt.constraints != null) {
          List<BvTypeConstraint/*!*/> list = new List<BvTypeConstraint/*!*/>();
          if (this.constraints != null) {
            list.AddRange(this.constraints);
          }
          if (bt.constraints != null) {
            list.AddRange(bt.constraints);
          }
          BvTypeProxy np = new BvTypeProxy(this.tok, this.Name, Math.Max(this.MinBits, bt.MinBits), list);
          this.DefineProxy(np);
          bt.DefineProxy(np);
        } else if (this.MinBits <= bt.MinBits) {
          this.DefineProxy(bt);
        } else {
          bt.DefineProxy(this);
        }
        return true;
      } else if (that is ConstrainedProxy) {
        // only bitvector proxies can be unified with this BvTypeProxy
        return false;
      } else if (that is TypeProxy) {
        // define:  that.ProxyFor := this;
        return that.Unify(this, unifiableVariables, result);
      }
      return false;
    }

    private static int IncreaseBits(Type t, int to) {
      Contract.Requires(t != null);
      Contract.Requires(t.IsBv && 0 <= to && MinBitsFor(t) <= to);
      Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= to);

      if(t is TypeSynonymAnnotation) {
        return IncreaseBits(((TypeSynonymAnnotation)t).ExpandedType, to);
      }

      t = FollowProxy(t);
      if (t is BvType) {
        return to - t.BvBits;
      } else {
        BvTypeProxy p = (BvTypeProxy)t;
        Contract.Assert(p.MinBits <= to);
        if (p.MinBits < to) {
          BvTypeProxy q = new BvTypeProxy(p, to);
          p.DefineProxy(q);
        }
        return 0;  // we were able to satisfy the request completely
      }
    }

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      if (this.ProxyFor == null) {
        // check that the constraints are clean and do not contain any
        // of the substituted variables (otherwise, we are in big trouble)
        Contract.Assert(Contract.ForAll(constraints, c =>
               Contract.ForAll(subst.Keys, var =>
                      !c.T0.FreeVariables.Contains(var) && !c.T1.FreeVariables.Contains(var))));
      }
      return base.Substitute(subst);
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsBv {
      get {
        return true;
      }
    }
    public override int BvBits {
      get {
        // This method is supposed to return the number of bits supplied, but unless the proxy has been resolved,
        // we only have a lower bound on the number of bits supplied.  But this method is not supposed to be
        // called until type checking has finished, at which time the minBits is stable.
        Type p = ProxyFor;
        if (p != null) {
          return p.BvBits;
        } else {
          return MinBits;
        }
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitBvTypeProxy(this);
    }
  }

  // Proxy representing map types with a certain arity. Apart from the arity,
  // a number of constraints on the index and value type of the map type may
  // be known (such constraints result from applied select and store operations).
  // Because map type can be polymorphic (in the most general case, each index or
  // value type is described by a separate type parameter) any combination of
  // constraints can be satisfied.
  public class MapTypeProxy : ConstrainedProxy {
    public readonly int Arity;
    private readonly List<Constraint>/*!*/ constraints = new List<Constraint>();
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(constraints != null);
    }


    // each constraint specifies that the given combination of argument/result
    // types must be a possible instance of the formal map argument/result types
    private struct Constraint {
      public readonly List<Type>/*!*/ Arguments;
      public readonly Type/*!*/ Result;
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(Arguments != null);
        Contract.Invariant(Result != null);
      }


      public Constraint(List<Type> arguments, Type result) {
        Contract.Requires(result != null);
        Contract.Requires(arguments != null);
        Arguments = arguments;
        Result = result;
      }

      public Constraint Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
        Contract.Requires(cce.NonNullDictionaryAndValues(varMap));
        List<Type>/*!*/ args = new List<Type>();
        foreach (Type/*!*/ t in Arguments) {
          Contract.Assert(t != null);
          args.Add(t.Clone(varMap));
        }
        Type/*!*/ res = Result.Clone(varMap);
        Contract.Assert(res != null);
        return new Constraint(args, res);
      }

      public bool Unify(MapType that,
                        List<TypeVariable>/*!*/ unifiableVariables,
                        IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
        Contract.Requires(unifiableVariables != null);
        Contract.Requires(cce.NonNullDictionaryAndValues(result));
        Contract.Requires(that != null);
        Contract.Requires(Arguments.Count == that.Arguments.Count);
        Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
        foreach (TypeVariable/*!*/ tv in that.TypeParameters) {
          Contract.Assert(tv != null);
          TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
          subst.Add(tv, proxy);
        }

        bool good = true;
        for (int i = 0; i < that.Arguments.Count; i++) {
          Type t0 = that.Arguments[i].Substitute(subst);
          Type t1 = this.Arguments[i];
          good &= t0.Unify(t1, unifiableVariables, result);
        }
        good &= that.Result.Substitute(subst).Unify(this.Result, unifiableVariables, result);
        return good;
      }
    }

    public MapTypeProxy(IToken token, string name, int arity)
      : base(token, name, "mapproxy") {
      Contract.Requires(name != null);
      Contract.Requires(token != null);
      Contract.Requires(0 <= arity);
      this.Arity = arity;
    }

    private void AddConstraint(Constraint c) {
      Contract.Requires(c.Arguments.Count == Arity);

      Type f = ProxyFor;
      MapType mf = f as MapType;
      if (mf != null) {
        bool success = c.Unify(mf, new List<TypeVariable>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());
        Contract.Assert(success);
        return;
      }

      MapTypeProxy mpf = f as MapTypeProxy;
      if (mpf != null) {
        mpf.AddConstraint(c);
        return;
      }

      Contract.Assert(f == null);  // no other types should occur as specialisations of this proxy

      constraints.Add(c);
    }

    public Type CheckArgumentTypes(List<Expr>/*!*/ actualArgs,
                                   out TypeParamInstantiation/*!*/ tpInstantiation,
                                   IToken/*!*/ typeCheckingSubject,
                                   string/*!*/ opName,
                                   TypecheckingContext/*!*/ tc) {
      Contract.Requires(actualArgs != null);
      Contract.Requires(typeCheckingSubject != null);
      Contract.Requires(opName != null);
      Contract.Requires(tc != null);
      Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);

      

      Type f = ProxyFor;
      MapType mf = f as MapType;
      if (mf != null)
        return mf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc);

      MapTypeProxy mpf = f as MapTypeProxy;
      if (mpf != null)
        return mpf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc);

      Contract.Assert(f == null);  // no other types should occur as specialisations of this proxy

      // otherwise, we just record the constraints given by this usage of the map type
      List<Type>/*!*/ arguments = new List<Type>();
      foreach (Expr/*!*/ e in actualArgs) {
        Contract.Assert(e != null);
        arguments.Add(e.Type);
      }
      Type/*!*/ result = new TypeProxy(tok, "result");
      Contract.Assert(result != null);
      AddConstraint(new Constraint(arguments, result));

      List<Type>/*!*/ argumentsResult = new List<Type>();
      foreach (Expr/*!*/ e in actualArgs) {
        Contract.Assert(e != null);
        argumentsResult.Add(e.Type);
      }
      argumentsResult.Add(result);

      tpInstantiation = new MapTypeProxyParamInstantiation(this, argumentsResult);
      return result;
    }

    //-----------  Cloning  ----------------------------------

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      Type p = ProxyFor;
      if (p != null) {
        return p.Clone(varMap);
      } else {
        MapTypeProxy p2 = new MapTypeProxy(tok, Name, Arity);
        foreach (Constraint c in constraints)
          p2.AddConstraint(c.Clone(varMap));
        return p2;  // the clone will have a name that ends with $mapproxy<n>$mapproxy<m> (hopefully)
      }
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      Type p = ProxyFor;
      if (p != null) {
        p.Emit(stream, contextBindingStrength);
      } else {
        stream.Write("[");
        string/*!*/ sep = "";
        for (int i = 0; i < Arity; ++i) {
          stream.Write(sep);
          sep = ", ";
          stream.Write("?");
        }
        stream.Write("]?");
      }
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
      //Contract.Requires(that != null);
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(cce.NonNullElements(result));
      Type p = ProxyFor;
      if (p != null) {
        return p.Unify(that, unifiableVariables, result);
      }

      // unify this with that, if possible
      that = that.Expanded;
      that = FollowProxy(that);

      if (this.ReallyOccursIn(that))
        return false;

      TypeVariable tv = that as TypeVariable;

      if (tv != null && unifiableVariables.Contains(tv))
        return that.Unify(this, unifiableVariables, result);

      if (object.ReferenceEquals(this, that)) {
        return true;
      } else if (that is MapType) {
        MapType mapType = (MapType)that;
        if (mapType.Arguments.Count == Arity) {
          bool good = true;
          foreach (Constraint c in constraints)
            good &= c.Unify(mapType, unifiableVariables, result);
          if (good) {
            DefineProxy(mapType);
            return true;
          }
        }
      } else if (that is MapTypeProxy) {
        MapTypeProxy mt = (MapTypeProxy)that;
        if (mt.Arity == this.Arity) {
          // we propagate the constraints of this proxy to the more specific one
          foreach (Constraint c in constraints)
            mt.AddConstraint(c);
          DefineProxy(mt);
          return true;
        }
      } else if (that is ConstrainedProxy) {
        // only map-type proxies can be unified with this MapTypeProxy
        return false;
      } else if (that is TypeProxy) {
        // define:  that.ProxyFor := this;
        return that.Unify(this, unifiableVariables, result);
      }
      return false;
    }

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      if (this.ProxyFor == null) {
        // check that the constraints are clean and do not contain any
        // of the substituted variables (otherwise, we are in big trouble)
        Contract.Assert(Contract.ForAll(constraints, c =>
               Contract.ForAll(subst.Keys, var =>
               Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Contains(var)) &&
                     !c.Result.FreeVariables.Contains(var))));
      }
      return base.Substitute(subst);
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsMap {
      get {
        return true;
      }
    }
    public override MapType/*!*/ AsMap {
      get {
        Contract.Ensures(Contract.Result<MapType>() != null);

        Type p = ProxyFor;
        if (p != null) {
          return p.AsMap;
        } else {
          {
            Contract.Assert(false);
            throw new cce.UnreachableException();
          } // what to do now?
        }
      }
    }
    public override int MapArity {
      get {
        return Arity;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitMapTypeProxy(this);
    }
  }

  //=====================================================================

  // Used to annotate types with type synoyms that were used in the
  // original unresolved types. Such types should be considered as
  // equivalent to ExpandedType, the annotations are only used to enable
  // better pretty-printing
  public class TypeSynonymAnnotation : Type {
    public Type/*!*/ ExpandedType;

    public readonly List<Type>/*!*/ Arguments;
    // is set during resolution and determines whether the right number of arguments is given
    public readonly TypeSynonymDecl/*!*/ Decl;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(ExpandedType != null);
      Contract.Invariant(Arguments != null);
      Contract.Invariant(Decl != null);
    }


    public TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List<Type>/*!*/ arguments)
      : base(token) {
      Contract.Requires(token != null);
      Contract.Requires(decl != null);
      Contract.Requires(arguments != null);
      Contract.Requires(arguments.Count == decl.TypeParameters.Count);
      this.Decl = decl;
      this.Arguments = arguments;

      // build a substitution that can be applied to the definition of
      // the type synonym
      IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
        new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      for (int i = 0; i < arguments.Count; ++i)
        subst.Add(decl.TypeParameters[i], arguments[i]);

      ExpandedType = decl.Body.Substitute(subst);
    }

    private TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List<Type>/*!*/ arguments,
                                  Type/*!*/ expandedType)
      : base(token) {
      Contract.Requires(token != null);
      Contract.Requires(decl != null);
      Contract.Requires(arguments != null);
      Contract.Requires(expandedType != null);

      this.Decl = decl;
      this.Arguments = arguments;
      this.ExpandedType = expandedType;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.Clone(varMap));
      }
      Type/*!*/ newExpandedType = ExpandedType.Clone(varMap);
      Contract.Assert(newExpandedType != null);
      return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType);
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.CloneUnresolved());
      }
      return new TypeSynonymAnnotation(tok, Decl, newArgs);
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type/*!*/ that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables) {
      //Contract.Requires(that != null);
      //Contract.Requires(thisBoundVariables != null);
      //Contract.Requires(thatBoundVariables != null);
      return ExpandedType.Equals(that, thisBoundVariables, thatBoundVariables);
    }

    // used to skip leading type annotations
    internal override Type/*!*/ Expanded {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);

        return ExpandedType.Expanded;
      }
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
      //Contract.Requires(that != null);
      //Contract.Requires(unifiableVariables != null);
      //Contract.Requires(cce.NonNullElements(result));
      return ExpandedType.Unify(that, unifiableVariables, result);
    }

#if OLD_UNIFICATION
    public override void Unify(Type! that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!>! result) {
      ExpandedType.Unify(that, unifiableVariables,
                         thisBoundVariables, thatBoundVariables, result);
    }
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      if (subst.Count == 0)
        return this;
      List<Type> newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.Substitute(subst));
      }
      Type/*!*/ newExpandedType = ExpandedType.Substitute(subst);
      Contract.Assert(newExpandedType != null);
      return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType);
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      return ExpandedType.GetHashCode(boundVariables);
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      stream.SetToken(this);
      CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type> resolvedArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        resolvedArgs.Add(t.ResolveType(rc));
      }
      return new TypeSynonymAnnotation(tok, Decl, resolvedArgs);
    }

    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

        return ExpandedType.FreeVariables;
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
        return ExpandedType.FreeProxies;
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsBasic {
      get {
        return ExpandedType.IsBasic;
      }
    }
    public override bool IsInt {
      get {
        return ExpandedType.IsInt;
      }
    }
    public override bool IsReal
    {
      get
      {
        return ExpandedType.IsReal;
      }
    }
    public override bool IsFloat
    {
      get
      {
        return ExpandedType.IsFloat;
      }
    }
    public override bool IsBool {
      get {
        return ExpandedType.IsBool;
      }
    }

    public override bool IsVariable {
      get {
        return ExpandedType.IsVariable;
      }
    }
    public override TypeVariable/*!*/ AsVariable {
      get {
        Contract.Ensures(Contract.Result<TypeVariable>() != null);
        return ExpandedType.AsVariable;
      }
    }
    public override bool IsCtor {
      get {
        return ExpandedType.IsCtor;
      }
    }
    public override CtorType/*!*/ AsCtor {
      get {
        Contract.Ensures(Contract.Result<CtorType>() != null);
        return ExpandedType.AsCtor;
      }
    }
    public override bool IsMap {
      get {
        return ExpandedType.IsMap;
      }
    }
    public override MapType/*!*/ AsMap {
      get {
        Contract.Ensures(Contract.Result<MapType>() != null);
        return ExpandedType.AsMap;
      }
    }
    public override bool IsUnresolved {
      get {
        return ExpandedType.IsUnresolved;
      }
    }
    public override UnresolvedTypeIdentifier/*!*/ AsUnresolved {
      get {
        Contract.Ensures(Contract.Result<UnresolvedTypeIdentifier>() != null);

        return ExpandedType.AsUnresolved;
      }
    }

    public override bool IsBv {
      get {
        return ExpandedType.IsBv;
      }
    }
    public override int BvBits {
      get {
        return ExpandedType.BvBits;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitTypeSynonymAnnotation(this);
    }
  }

  //=====================================================================

  public class CtorType : Type {
    public readonly List<Type>/*!*/ Arguments;
    // is set during resolution and determines whether the right number of arguments is given
    public readonly TypeCtorDecl/*!*/ Decl;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Arguments != null);
      Contract.Invariant(Decl != null);
    }


    public CtorType(IToken/*!*/ token, TypeCtorDecl/*!*/ decl, List<Type>/*!*/ arguments)
      : base(token) {
      Contract.Requires(token != null);
      Contract.Requires(decl != null);
      Contract.Requires(arguments != null);
      Contract.Requires(arguments.Count == decl.Arity);
      this.Decl = decl;
      this.Arguments = arguments;
    }

    public bool IsDatatype() {
      return QKeyValue.FindBoolAttribute(Decl.Attributes, "datatype");
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.Clone(varMap));
      }
      return new CtorType(tok, Decl, newArgs);
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.CloneUnresolved());
      }
      return new CtorType(tok, Decl, newArgs);
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      Type thatType = that as Type;
      if (thatType == null)
        return false;
      thatType = TypeProxy.FollowProxy(thatType.Expanded);
      // shortcut
      CtorType thatCtorType = thatType as CtorType;
      if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))
        return false;
      if (Arguments.Count == 0)
        return true;
      return base.Equals(thatType);
    }

    [Pure]
    public override bool Equals(Type/*!*/ that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables) {
      that = TypeProxy.FollowProxy(that.Expanded);
      CtorType thatCtorType = that as CtorType;
      if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))
        return false;
      for (int i = 0; i < Arguments.Count; ++i) {
        if (!Arguments[i].Equals(thatCtorType.Arguments[i],
                                 thisBoundVariables, thatBoundVariables))
          return false;
      }
      return true;
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
      that = that.Expanded;
      if (that is TypeProxy || that is TypeVariable)
        return that.Unify(this, unifiableVariables, result);

      CtorType thatCtorType = that as CtorType;
      if (thatCtorType == null || !thatCtorType.Decl.Equals(Decl)) {
        return false;
      } else {
        bool good = true;
        for (int i = 0; i < Arguments.Count; ++i)
          good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result);
        return good;
      }
    }

#if OLD_UNIFICATION
    public override void Unify(Type! that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!>! result) {
      that = that.Expanded;
      if (that is TypeVariable) {
        that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result);
        return;
      }

      CtorType thatCtorType = that as CtorType;
      if (thatCtorType == null || !thatCtorType.Decl.Equals(Decl))
        throw UNIFICATION_FAILED;
      for (int i = 0; i < Arguments.Length; ++i)
        Arguments[i].Unify(thatCtorType.Arguments[i],
                           unifiableVariables,
                           thisBoundVariables, thatBoundVariables,
                           result);
    }
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      if (subst.Count == 0)
        return this;
      List<Type> newArgs = new List<Type>();
      lock (Arguments)
      {
        foreach (Type/*!*/ t in Arguments)
        {
          Contract.Assert(t != null);
          newArgs.Add(t.Substitute(subst));
        }
      }
      return new CtorType(tok, Decl, newArgs);
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      int res = 1637643879 * Decl.GetHashCode();
      foreach (Type/*!*/ t in Arguments.ToArray()) {
        Contract.Assert(t != null);
        res = res * 3 + t.GetHashCode(boundVariables);
      }
      return res;
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      stream.SetToken(this);
      EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
    }

    internal static void EmitCtorType(string name, List<Type> args, TokenTextWriter stream, int contextBindingStrength) {
      Contract.Requires(stream != null);
      Contract.Requires(args != null);
      Contract.Requires(name != null);
      int opBindingStrength = args.Count > 0 ? 0 : 2;
      if (opBindingStrength < contextBindingStrength)
        stream.Write("(");

      stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name));
      int i = args.Count;
      foreach (Type/*!*/ t in args) {
        Contract.Assert(t != null);
        stream.Write(" ");
        // use a lower binding strength for the last argument
        // to allow map-types without parentheses
        t.Emit(stream, i == 1 ? 1 : 2);
        i = i - 1;
      }

      if (opBindingStrength < contextBindingStrength)
        stream.Write(")");
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      List<Type> resolvedArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        resolvedArgs.Add(t.ResolveType(rc));
      }
      return new CtorType(tok, Decl, resolvedArgs);
    }

    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        List<TypeVariable>/*!*/ res = new List<TypeVariable>();
        foreach (Type/*!*/ t in Arguments.ToArray()) {
          Contract.Assert(t != null);
          res.AppendWithoutDups(t.FreeVariables);
        }
        return res;
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*/>();
        foreach (Type/*!*/ t in Arguments.ToArray()) {
          Contract.Assert(t != null);
          AppendWithoutDups(res, t.FreeProxies);
        }
        return res;
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsCtor {
      get {
        return true;
      }
    }
    public override CtorType/*!*/ AsCtor {
      get {
        return this;
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitCtorType(this);
    }
  }

  //=====================================================================

  public class MapType : Type {
    // an invariant is that each of the type parameters has to occur as
    // free variable in at least one of the arguments
    public readonly List<TypeVariable>/*!*/ TypeParameters;
    public readonly List<Type>/*!*/ Arguments;
    public Type/*!*/ Result;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(TypeParameters != null);
      Contract.Invariant(Arguments != null);
      Contract.Invariant(Result != null);
    }


    public MapType(IToken/*!*/ token, List<TypeVariable>/*!*/ typeParameters, List<Type>/*!*/ arguments, Type/*!*/ result)
      : base(token) {
      Contract.Requires(token != null);
      Contract.Requires(typeParameters != null);
      Contract.Requires(arguments != null);
      Contract.Requires(result != null);

      this.TypeParameters = typeParameters;
      this.Result = result;
      this.Arguments = arguments;
    }

    //-----------  Cloning  ----------------------------------
    // We implement our own clone-method, because bound type variables
    // have to be created in the right way. It is /not/ ok to just clone
    // everything recursively

    public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {
      //Contract.Requires(cce.NonNullElements(varMap));
      Contract.Ensures(Contract.Result<Type>() != null);
      IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ newVarMap =
        new Dictionary<TypeVariable/*!*/, TypeVariable/*!*/>();
      foreach (KeyValuePair<TypeVariable/*!*/, TypeVariable/*!*/> p in varMap) {
        Contract.Assert(cce.NonNullElements(p));
        if (!TypeParameters.Contains(p.Key))
          newVarMap.Add(p);
      }

      List<TypeVariable>/*!*/ newTypeParams = new List<TypeVariable>();
      foreach (TypeVariable/*!*/ var in TypeParameters) {
        Contract.Assert(var != null);
        TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name);
        Contract.Assert(newVar != null);
        newVarMap.Add(var, newVar);
        newTypeParams.Add(newVar);
      }

      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.Clone(newVarMap));
      }
      Type/*!*/ newResult = Result.Clone(newVarMap);
      Contract.Assert(newResult != null);

      return new MapType(this.tok, newTypeParams, newArgs, newResult);
    }

    public override Type CloneUnresolved() {
      Contract.Ensures(Contract.Result<Type>() != null);
      List<TypeVariable>/*!*/ newTypeParams = new List<TypeVariable>();
      foreach (TypeVariable/*!*/ var in TypeParameters) {
        Contract.Assert(var != null);
        TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name);
        Contract.Assert(newVar != null);
        newTypeParams.Add(newVar);
      }

      List<Type>/*!*/ newArgs = new List<Type>();
      foreach (Type/*!*/ t in Arguments) {
        Contract.Assert(t != null);
        newArgs.Add(t.CloneUnresolved());
      }
      Type/*!*/ newResult = Result.CloneUnresolved();
      Contract.Assert(newResult != null);

      return new MapType(this.tok, newTypeParams, newArgs, newResult);
    }

    //-----------  Equality  ----------------------------------

    [Pure]
    public override bool Equals(Type/*!*/ that,
                                List<TypeVariable>/*!*/ thisBoundVariables,
                                List<TypeVariable>/*!*/ thatBoundVariables)
    {
      that = TypeProxy.FollowProxy(that.Expanded);
      MapType thatMapType = that as MapType;
      if (thatMapType == null ||
          this.TypeParameters.Count != thatMapType.TypeParameters.Count ||
          this.Arguments.Count != thatMapType.Arguments.Count)
        return false;

      thisBoundVariables = thisBoundVariables.ToList();
      foreach (TypeVariable/*!*/ var in this.TypeParameters)
      {
        Contract.Assert(var != null);
        thisBoundVariables.Add(var);
      }
      thatBoundVariables = thatBoundVariables.ToList();
      foreach (TypeVariable/*!*/ var in thatMapType.TypeParameters)
      {
        Contract.Assert(var != null);
        thatBoundVariables.Add(var);
      }

      for (int i = 0; i < Arguments.Count; ++i)
      {
        if (!Arguments[i].Equals(thatMapType.Arguments[i],
                                 thisBoundVariables, thatBoundVariables))
          return false;
      }

      return this.Result.Equals(thatMapType.Result,
                                thisBoundVariables, thatBoundVariables);
    }

    //-----------  Unification of types  -----------

    public override bool Unify(Type/*!*/ that,
                               List<TypeVariable>/*!*/ unifiableVariables,
                               IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {
      that = that.Expanded;
      if (that is TypeProxy || that is TypeVariable)
        return that.Unify(this, unifiableVariables, result);

      MapType thatMapType = that as MapType;
      if (thatMapType == null ||
          this.TypeParameters.Count != thatMapType.TypeParameters.Count ||
          this.Arguments.Count != thatMapType.Arguments.Count)
        return false;

      // treat the bound variables of the two map types as equal...
      Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst0 =
        new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =
        new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      List<TypeVariable> freshies = new List<TypeVariable>();
      for (int i = 0; i < this.TypeParameters.Count; i++) {
        TypeVariable tp0 = this.TypeParameters[i];
        TypeVariable tp1 = thatMapType.TypeParameters[i];
        TypeVariable freshVar = new TypeVariable(tp0.tok, tp0.Name);
        freshies.Add(freshVar);
        subst0.Add(tp0, freshVar);
        subst1.Add(tp1, freshVar);
      }
      // ... and then unify the domain and range types
      bool good = true;
      for (int i = 0; i < this.Arguments.Count; i++) {
        Type t0 = this.Arguments[i].Substitute(subst0);
        Type t1 = thatMapType.Arguments[i].Substitute(subst1);
        good &= t0.Unify(t1, unifiableVariables, result);
      }
      Type r0 = this.Result.Substitute(subst0);
      Type r1 = thatMapType.Result.Substitute(subst1);
      good &= r0.Unify(r1, unifiableVariables, result);

      // Finally, check that none of the bound variables has escaped
      if (good && freshies.Count != 0) {
        // This is done by looking for occurrences of the fresh variables in the
        // non-substituted types ...
        List<TypeVariable> freeVars = this.FreeVariables;
        foreach (TypeVariable fr in freshies)
          if (freeVars.Contains(fr)) {
            return false;
          }  // fresh variable escaped
        freeVars = thatMapType.FreeVariables;
        foreach (TypeVariable fr in freshies)
          if (freeVars.Contains(fr)) {
            return false;
          }  // fresh variable escaped

        // ... and in the resulting unifier of type variables
        foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in result) {
          Contract.Assert(cce.NonNullElements(pair));
          freeVars = pair.Value.FreeVariables;
          foreach (TypeVariable fr in freshies)
            if (freeVars.Contains(fr)) {
              return false;
            }  // fresh variable escaped          
        }
      }

      return good;
    }

#if OLD_UNIFICATION
    public override void Unify(Type! that,
                               List<TypeVariable>! unifiableVariables,
                               List<TypeVariable>! thisBoundVariables,
                               List<TypeVariable>! thatBoundVariables,
                               IDictionary<TypeVariable!, Type!>! result) {
      that = that.Expanded;
      if (that is TypeVariable) {
        that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result);
        return;
      }

      MapType thatMapType = that as MapType;
      if (thatMapType == null ||
          this.TypeParameters.Length != thatMapType.TypeParameters.Length ||
          this.Arguments.Length != thatMapType.Arguments.Length)
        throw UNIFICATION_FAILED;

      // ensure that no collisions occur
      if (this.collisionsPossible(result)) {
        ((MapType)this.Clone())
          .Unify(that, unifiableVariables,
                 thisBoundVariables, thatBoundVariables, result);
        return;
      }
      if (thatMapType.collisionsPossible(result))
        thatMapType = (MapType)that.Clone();

      foreach(TypeVariable/*!*/ var in this.TypeParameters){
Contract.Assert(var != null);
        thisBoundVariables.Add(var);}
      foreach(TypeVariable/*!*/ var in thatMapType.TypeParameters){
Contract.Assert(var != null);
        thatBoundVariables.Add(var);}

      try {

        for (int i = 0; i < Arguments.Length; ++i)
          Arguments[i].Unify(thatMapType.Arguments[i],
                             unifiableVariables,
                             thisBoundVariables, thatBoundVariables,
                             result);
        Result.Unify(thatMapType.Result,
                     unifiableVariables,
                     thisBoundVariables, thatBoundVariables,
                     result);

      } finally {
        // make sure that the bound variables are removed again
        for (int i = 0; i < this.TypeParameters.Length; ++i) {
          thisBoundVariables.Remove();
          thatBoundVariables.Remove();
        }
      }            
    }
#endif

    //-----------  Substitution of free variables with types not containing bound variables  -----------------

    [Pure]
    private bool collisionsPossible(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      Contract.Requires(cce.NonNullDictionaryAndValues(subst));
      // PR: could be written more efficiently
      return TypeParameters.Any(param => subst.ContainsKey(param) || subst.Values.Any(val => val.FreeVariables.Contains(param)));
    }

    public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
      //Contract.Requires(cce.NonNullElements(subst));
      Contract.Ensures(Contract.Result<Type>() != null);
      if (subst.Count == 0)
        return this;

      // there are two cases in which we have to be careful:
      // * a variable to be substituted is shadowed by a variable binder
      // * a substituted term contains variables that are bound in the
      //   type (variable capture)
      //
      // in both cases, we first clone the type to ensure that bound
      // variables are fresh

      if (collisionsPossible(subst)) {
        MapType/*!*/ newType = (MapType)this.Clone();
        Contract.Assert(newType != null);
        Contract.Assert(newType.Equals(this) && !newType.collisionsPossible(subst));
        return newType.Substitute(subst);
      }

      List<Type> newArgs = new List<Type>();
      lock (Arguments)
      {
        foreach (Type/*!*/ t in Arguments)
        {
          Contract.Assert(t != null);
          newArgs.Add(t.Substitute(subst));
        }
      }
      Type/*!*/ newResult = Result.Substitute(subst);
      Contract.Assert(newResult != null);

      return new MapType(tok, TypeParameters, newArgs, newResult);
    }

    //-----------  Hashcodes  ----------------------------------

    [Pure]
    public override int GetHashCode(List<TypeVariable> boundVariables) {
      //Contract.Requires(boundVariables != null);
      int res = 7643761 * TypeParameters.Count + 65121 * Arguments.Count;

      boundVariables = boundVariables.ToList();
      foreach (TypeVariable/*!*/ var in this.TypeParameters) {
        Contract.Assert(var != null);
        boundVariables.Add(var);
      }

      foreach (Type/*!*/ t in Arguments.ToArray()) {
        Contract.Assert(t != null);
        res = res * 5 + t.GetHashCode(boundVariables);
      }
      res = res * 7 + Result.GetHashCode(boundVariables);
      
      return res;
    }

    //-----------  Linearisation  ----------------------------------

    public override void Emit(TokenTextWriter stream, int contextBindingStrength) {
      //Contract.Requires(stream != null);
      stream.SetToken(this);

      const int opBindingStrength = 1;
      if (opBindingStrength < contextBindingStrength)
        stream.Write("(");

      EmitOptionalTypeParams(stream, TypeParameters);

      stream.Write("[");
      Arguments.Emit(stream, ",");        // default binding strength of 0 is ok
      stream.Write("]");
      Result.Emit(stream);                 // default binding strength of 0 is ok

      if (opBindingStrength < contextBindingStrength)
        stream.Write(")");
    }

    //-----------  Resolution  ----------------------------------

    public override Type ResolveType(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      int previousState = rc.TypeBinderState;
      try {
        foreach (TypeVariable/*!*/ v in TypeParameters) {
          Contract.Assert(v != null);
          rc.AddTypeBinder(v);
        }

        List<Type> resolvedArgs = new List<Type>();
        foreach (Type/*!*/ ty in Arguments) {
          Contract.Assert(ty != null);
          resolvedArgs.Add(ty.ResolveType(rc));
        }

        Type resolvedResult = Result.ResolveType(rc);

        CheckBoundVariableOccurrences(TypeParameters,
                                      resolvedArgs, new List<Type> { resolvedResult },
                                      this.tok, "map arguments",
                                      rc);

        // sort the type parameters so that they are bound in the order of occurrence
        List<TypeVariable>/*!*/ sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult);
        Contract.Assert(sortedTypeParams != null);
        return new MapType(tok, sortedTypeParams, resolvedArgs, resolvedResult);
      } finally {
        rc.TypeBinderState = previousState;
      }
    }

    public override List<TypeVariable>/*!*/ FreeVariables {
      get {
        List<TypeVariable>/*!*/ res = FreeVariablesIn(Arguments.ToList());
        Contract.Assert(res != null);
        res.AppendWithoutDups(Result.FreeVariables);
        foreach (TypeVariable/*!*/ v in TypeParameters.ToArray()) {
          Contract.Assert(v != null);
          res.Remove(v);
        }
        return res;
      }
    }

    public override List<TypeProxy/*!*/>/*!*/ FreeProxies {
      get {
        List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*//*!*/>();
        foreach (Type/*!*/ t in Arguments.ToArray()) {
          Contract.Assert(t != null);
          AppendWithoutDups(res, t.FreeProxies);
        }
        AppendWithoutDups(res, Result.FreeProxies);
        return res;
      }
    }

    //-----------  Getters/Issers  ----------------------------------

    public override bool IsMap {
      get {
        return true;
      }
    }
    public override MapType/*!*/ AsMap {
      get {
        return this;
      }
    }
    public override int MapArity {
      get {
        return Arguments.Count;
      }
    }

    //------------  Match formal argument types of the map
    //------------  on concrete types, substitute the result into the
    //------------  result type. Null is returned if so many type checking
    //------------  errors occur that the situation is hopeless

    public Type CheckArgumentTypes(List<Expr>/*!*/ actualArgs,
                                   out TypeParamInstantiation/*!*/ tpInstantiation,
                                   IToken/*!*/ typeCheckingSubject,
                                   string/*!*/ opName,
                                   TypecheckingContext/*!*/ tc) {
      Contract.Requires(actualArgs != null);
      Contract.Requires(typeCheckingSubject != null);
      
      Contract.Requires(opName != null);
      Contract.Requires(tc != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
      List<Type/*!*/>/*!*/ actualTypeParams;
      List<Type> actualResult =
        Type.CheckArgumentTypes(TypeParameters, out actualTypeParams, Arguments, actualArgs,
                                new List<Type> { Result }, null, typeCheckingSubject, opName, tc);
      if (actualResult == null) {
        tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
        return null;
      } else {
        Contract.Assert(actualResult.Count == 1);
        tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams);
        return actualResult[0];
      }
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      //Contract.Requires(visitor != null);
      Contract.Ensures(Contract.Result<Absy>() != null);
      return visitor.VisitMapType(this);
    }
  }

  //---------------------------------------------------------------------

  public enum SimpleType {
    Int,
    Real,
    Bool
  };


  //=====================================================================

  // Interface for representing the instantiations of type parameters of
  // polymorphic functions or maps. We introduce an own interface for this
  // instead of using a simple list or dictionary, because in some cases
  // (due to the type proxies for map types) the actual number and instantiation
  // of type parameters can only be determined very late.
  [ContractClass(typeof(TypeParamInstantiationContracts))]
  public interface TypeParamInstantiation {
    // return what formal type parameters there are
    List<TypeVariable/*!*/>/*!*/ FormalTypeParams {
      get;
    }
    // given a formal type parameter, return the actual instantiation
    Type/*!*/ this[TypeVariable/*!*/ var] {
      get;
    }
  }
  [ContractClassFor(typeof(TypeParamInstantiation))]
  public abstract class TypeParamInstantiationContracts : TypeParamInstantiation {
    #region TypeParamInstantiation Members

    public List<TypeVariable> FormalTypeParams {

      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
        throw new NotImplementedException();
      }
    }

    public Type this[TypeVariable var] {
      get {
        Contract.Requires(var != null);
        Contract.Ensures(Contract.Result<Type>() != null);

        throw new NotImplementedException();
      }
    }

    #endregion
  }


  public class SimpleTypeParamInstantiation : TypeParamInstantiation {
    private readonly List<TypeVariable/*!*/>/*!*/ TypeParams;
    [ContractInvariantMethod]
    void TypeParamsInvariantMethod() {
      Contract.Invariant(cce.NonNullElements(TypeParams));
    }
    private readonly IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ Instantiations;
    [ContractInvariantMethod]
    void InstantiationsInvariantMethod() {
      Contract.Invariant(cce.NonNullDictionaryAndValues(Instantiations));
    }

    public SimpleTypeParamInstantiation(List<TypeVariable/*!*/>/*!*/ typeParams,
                                        IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ instantiations) {
      Contract.Requires(cce.NonNullElements(typeParams));
      Contract.Requires(cce.NonNullDictionaryAndValues(instantiations));
      this.TypeParams = typeParams;
      this.Instantiations = instantiations;
    }

    public static TypeParamInstantiation/*!*/ From(List<TypeVariable> typeParams, List<Type/*!*/>/*!*/ actualTypeParams) {
      Contract.Requires(cce.NonNullElements(actualTypeParams));
      Contract.Requires(typeParams != null);
      Contract.Requires(typeParams.Count == actualTypeParams.Count);
      Contract.Ensures(Contract.Result<TypeParamInstantiation>() != null);

      if (typeParams.Count == 0)
        return EMPTY;

      List<TypeVariable/*!*/>/*!*/ typeParamList = new List<TypeVariable/*!*/>();
      IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      for (int i = 0; i < typeParams.Count; ++i) {
        typeParamList.Add(typeParams[i]);
        dict.Add(typeParams[i], actualTypeParams[i]);
      }
      return new SimpleTypeParamInstantiation(typeParamList, dict);
    }

    public static readonly TypeParamInstantiation EMPTY =
      new SimpleTypeParamInstantiation(new List<TypeVariable/*!*/>(),
                                        new Dictionary<TypeVariable/*!*/, Type/*!*/>());

    // return what formal type parameters there are
    public List<TypeVariable/*!*/>/*!*/ FormalTypeParams {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
        return TypeParams;
      }
    }
    // given a formal type parameter, return the actual instantiation
    public Type/*!*/ this[TypeVariable/*!*/ var] {
      get {
        return Instantiations[var];
      }
    }
  }

  // Implementation of TypeParamInstantiation that refers to the current
  // value of a MapTypeProxy. This means that the values return by the
  // methods of this implementation can change in case the MapTypeProxy
  // receives further unifications.
  class MapTypeProxyParamInstantiation : TypeParamInstantiation {
    private readonly MapTypeProxy/*!*/ Proxy;

    // the argument and result type of this particular usage of the map
    // type. these are necessary to derive the values of the type parameters
    private readonly List<Type>/*!*/ ArgumentsResult;

    // field that is initialised once all necessary information is available
    // (the MapTypeProxy is instantiated to an actual type) and the instantiation
    // of a type parameter is queried
    private IDictionary<TypeVariable/*!*/, Type/*!*/> Instantiations = null;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Proxy != null);
      Contract.Invariant(ArgumentsResult != null);
      Contract.Invariant(Instantiations == null || cce.NonNullDictionaryAndValues(Instantiations));
    }


    public MapTypeProxyParamInstantiation(MapTypeProxy/*!*/ proxy,
                                          List<Type>/*!*/ argumentsResult) {
      Contract.Requires(proxy != null);
      Contract.Requires(argumentsResult != null);
      this.Proxy = proxy;
      this.ArgumentsResult = argumentsResult;
    }

    // return what formal type parameters there are
    public List<TypeVariable/*!*/>/*!*/ FormalTypeParams {
      get {
        MapType realType = Proxy.ProxyFor as MapType;
        if (realType == null)
          // no instantiation of the map type is known, which means
          // that the map type is assumed to be monomorphic
          return new List<TypeVariable/*!*/>();
        else
          return realType.TypeParameters.ToList();
      }
    }

    // given a formal type parameter, return the actual instantiation
    public Type/*!*/ this[TypeVariable/*!*/ var] {
      get {
        // then there has to be an instantiation that is a polymorphic map type
        if (Instantiations == null) {
          MapType realType = Proxy.ProxyFor as MapType;
          Contract.Assert(realType != null);
          List<Type>/*!*/ formalArgs = new List<Type>();
          foreach (Type/*!*/ t in realType.Arguments) {
            Contract.Assert(t != null);
            formalArgs.Add(t);
          }
          formalArgs.Add(realType.Result);
          Instantiations =
            Type.InferTypeParameters(realType.TypeParameters, formalArgs, ArgumentsResult);
        }
        return Instantiations[var];
      }
    }
  }
}