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

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

  using Set = GSet<object>;

  //---------------------------------------------------------------------
  // Quantifiers and general binders
  //---------------------------------------------------------------------

  public enum BinderKind {
    Forall,
    Exists,
    Lambda
  }
  [ContractClassFor(typeof(BinderExpr))]
  abstract class BinderExprContracts : BinderExpr {
    public override BinderKind Kind {
      get {
        throw new NotImplementedException();
      }
    }
    public BinderExprContracts():base(null,null,null,null,null,false){
  }

    public override Type ShallowType {
      get {
        throw new NotImplementedException();
      }
    }
  }
  [ContractClass(typeof(BinderExprContracts))]
  public abstract class BinderExpr : Expr {
    public List<TypeVariable>/*!*/ TypeParameters;
    public List<Variable>/*!*/ Dummies;
    public QKeyValue Attributes;
    // FIXME: Protect the above Fields
    public Expr _Body;
    public Expr/*!*/ Body {
      get {
        return _Body;
      }
      set {
        if (Immutable)
          throw new InvalidOperationException ("Cannot change the Body of an immutable BinderExpr");

        _Body = value;
      }
    }
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(TypeParameters != null);
      Contract.Invariant(Dummies != null);
      Contract.Invariant(Body != null);
    }

    public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable)
      : base(tok, immutable) {
      Contract.Requires(tok != null);
      Contract.Requires(typeParameters != null);
      Contract.Requires(dummies != null);
      Contract.Requires(body != null);
      Contract.Requires(dummies.Count + typeParameters.Count > 0);
      TypeParameters = typeParameters;
      Dummies = dummies;
      Attributes = kv;
      _Body = body;
      if (immutable)
        CachedHashCode = ComputeHashCode();
    }

    abstract public BinderKind Kind {
      get;
    }

    protected static bool CompareAttributesAndTriggers = false;

    public static bool EqualWithAttributesAndTriggers(object a, object b) {
      CompareAttributesAndTriggers = true;
      var res = object.Equals(a, b);
      Contract.Assert(CompareAttributesAndTriggers);
      CompareAttributesAndTriggers = false;
      return res;
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object obj) {
      return BinderEquals(obj);
    }

    public bool BinderEquals(object obj) {
      if (obj == null) {
        return false;
      }
      if (!(obj is BinderExpr) ||
          this.Kind != ((BinderExpr) obj).Kind) {
        return false;
      }

      var other = (BinderExpr) obj;

      return this.TypeParameters.SequenceEqual(other.TypeParameters)
             && this.Dummies.SequenceEqual(other.Dummies)
             && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))
             && object.Equals(this.Body, other.Body);
    }

    [Pure]
    public override int GetHashCode()
    {
      if (Immutable)
        return CachedHashCode;
      else
        return ComputeHashCode();
    }

    [Pure]
    public override int ComputeHashCode() {
      // Note, we don't hash triggers and attributes

      // DO NOT USE Dummies.GetHashCode() because we want structurally
      // identical Expr to have the same hash code **not** identical references
      // to have the same hash code.
      int h = 0;
      foreach (var dummyVar in this.Dummies) {
        h = ( 53 * h ) + dummyVar.GetHashCode();
      }

      h ^= this.Body.GetHashCode();

      // DO NOT USE TypeParameters.GetHashCode() because we want structural
      // identical Expr to have the same hash code **not** identical references
      // to have the same hash code.
      int h2 = 0;
      foreach (var typeParam in this.TypeParameters) {
        h2 = ( 97 * h2 ) + typeParam.GetHashCode();
      }

      h = h * 5 + h2;
      h *= ((int)Kind + 1);
      return h;
    }

    protected virtual void EmitTypeHint(TokenTextWriter stream) {
      Contract.Requires(stream != null);
    }

    protected virtual void EmitTriggers(TokenTextWriter stream) {
      Contract.Requires(stream != null);
    }

    public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
      //Contract.Requires(stream != null);
      stream.push();
      stream.Write(this, "({0}", Kind.ToString().ToLower());
      this.EmitTypeHint(stream);
      Type.EmitOptionalTypeParams(stream, TypeParameters);
      stream.Write(this, " ");
      this.Dummies.Emit(stream, true);
      stream.Write(" :: ");
      stream.sep();
      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
        kv.Emit(stream);
        stream.Write(" ");
      }
      this.EmitTriggers(stream);
      stream.sep();

      this.Body.Emit(stream);
      stream.Write(")");
      stream.pop();
    }

    protected virtual void ResolveTriggers(ResolutionContext rc) {
      Contract.Requires(rc != null);
    }

    public override void Resolve(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      if (rc.TriggerMode) {
        rc.Error(this, "quantifiers are not allowed in triggers");
      }

      int previousTypeBinderState = rc.TypeBinderState;
      try {
        foreach (TypeVariable/*!*/ v in TypeParameters) {
          Contract.Assert(v != null);
          rc.AddTypeBinder(v);
        }

        rc.PushVarContext();
        foreach (Variable/*!*/ v in Dummies) {
          Contract.Assert(v != null);
          v.Register(rc);
          v.Resolve(rc);
        }
        for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
          kv.Resolve(rc);
        }
        this.ResolveTriggers(rc);
        Body.Resolve(rc);
        rc.PopVarContext();

        // establish a canonical order of the type parameters
        this.TypeParameters = Type.SortTypeParams(TypeParameters, new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);

      } finally {
        rc.TypeBinderState = previousTypeBinderState;
      }
    }

    public override void ComputeFreeVariables(Set freeVars) {
      //Contract.Requires(freeVars != null);
      ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Attributes, freeVars);
    }

    public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters, List<Variable> dummies, Expr body, QKeyValue attributes, Set freeVars) {
      Contract.Requires(dummies != null);
      Contract.Requires(body != null);

      foreach (var v in dummies) {
        Contract.Assert(v != null);
        Contract.Assert(!freeVars[v]);
      }
      body.ComputeFreeVariables(freeVars);
      for (var a = attributes; a != null; a = a.Next) {
        foreach (var o in a.Params) {
          var e = o as Expr;
          if (e != null) {
            e.ComputeFreeVariables(freeVars);
          }
        }
      }
      foreach (var v in dummies) {
        freeVars.AddRange(v.TypedIdent.Type.FreeVariables);
      }
      freeVars.RemoveRange(dummies);
      freeVars.RemoveRange(typeParameters);
    }

    protected List<TypeVariable> GetUnmentionedTypeParameters() {
      Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
      List<TypeVariable>/*!*/ dummyParameters = Type.FreeVariablesIn(new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));
      Contract.Assert(dummyParameters != null);
      List<TypeVariable>/*!*/ unmentionedParameters = new List<TypeVariable>();
      foreach (TypeVariable/*!*/ var in TypeParameters) {
        Contract.Assert(var != null);
        if (!dummyParameters.Contains(var))
          unmentionedParameters.Add(var);
      }
      return unmentionedParameters;
    }
  }

  public class QKeyValue : Absy {
    public readonly string/*!*/ Key;
    private readonly List<object/*!*/>/*!*/ _params;  // each element is either a string or an Expr

    public void AddParam(object p)
    {
      Contract.Requires(p != null);
      this._params.Add(p);
    }

    public void AddParams(IEnumerable<object> ps)
    {
      Contract.Requires(cce.NonNullElements(ps));
      this._params.AddRange(ps);
    }

    public void ClearParams()
    {
      this._params.Clear();
    }

    public IList<object> Params
    {
      get
      {
        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));
        Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);
        return this._params.AsReadOnly();
      }
    }

    public QKeyValue Next;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Key != null);
      Contract.Invariant(cce.NonNullElements(this._params));
    }

    public QKeyValue(IToken tok, string key, IList<object/*!*/>/*!*/ parameters, QKeyValue next)
      : base(tok) {
      Contract.Requires(key != null);
      Contract.Requires(tok != null);
      Contract.Requires(cce.NonNullElements(parameters));
      Key = key;
      this._params = new List<object>(parameters);
      Next = next;
    }

    public void Emit(TokenTextWriter stream) {
      Contract.Requires(stream != null);
      stream.Write("{:");
      stream.Write(Key);
      string sep = " ";
      foreach (object p in Params) {
        stream.Write(sep);
        sep = ", ";
        if (p is string) {
          stream.Write("\"");
          stream.Write((string)p);
          stream.Write("\"");
        } else {
          ((Expr)p).Emit(stream);
        }
      }
      stream.Write("}");
    }

    public override void Resolve(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      foreach (object p in Params) {
        if (p is Expr) {
          ((Expr)p).Resolve(rc);
        }
      }
    }

    public override void Typecheck(TypecheckingContext tc) {
      //Contract.Requires(tc != null);
      foreach (object p in Params) {
        if (p is Expr) {
          ((Expr)p).Typecheck(tc);
        }
      }
    }
    public void AddLast(QKeyValue other) {
      Contract.Requires(other != null);
      QKeyValue current = this;
      while (current.Next != null) {
        current = current.Next;
      }
      current.Next = other;
    }
    // Look for {:name string} in list of attributes.
    [Pure]
    public static string FindStringAttribute(QKeyValue kv, string name) {
      Contract.Requires(name != null);
      for (; kv != null; kv = kv.Next) {
        if (kv.Key == name) {
          if (kv.Params.Count == 1 && kv.Params[0] is string) {
            return (string)kv.Params[0];
          }
        }
      }
      return null;
    }
    // Look for {:name expr} in list of attributes.
    public static Expr FindExprAttribute(QKeyValue kv, string name) {
      Contract.Requires(name != null);
      for (; kv != null; kv = kv.Next) {
        if (kv.Key == name) {
          if (kv.Params.Count == 1 && kv.Params[0] is Expr) {
            return (Expr)kv.Params[0];
          }
        }
      }
      return null;
    }
    // Return 'true' if {:name true} or {:name} is an attribute in 'kv'
    public static bool FindBoolAttribute(QKeyValue kv, string name) {
      Contract.Requires(name != null);
      for (; kv != null; kv = kv.Next) {
        if (kv.Key == name) {
          return kv.Params.Count == 0 ||
            (kv.Params.Count == 1 && kv.Params[0] is LiteralExpr && ((LiteralExpr)kv.Params[0]).IsTrue);
        }
      }
      return false;
    }

    public static int FindIntAttribute(QKeyValue kv, string name, int defl) {
      Contract.Requires(name != null);
      Expr e = FindExprAttribute(kv, name);
      LiteralExpr l = e as LiteralExpr;
      if (l != null && l.isBigNum)
        return l.asBigNum.ToIntSafe;
      return defl;
    }

    public override Absy Clone() {
      List<object> newParams = new List<object>();
      foreach (object o in Params)
        newParams.Add(o);
      return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
    }

    public override Absy StdDispatch(StandardVisitor visitor) {
      return visitor.VisitQKeyValue(this);
    }

    public override bool Equals(object obj) {
      var other = obj as QKeyValue;
      if (other == null) {
        return false;
      } else {
        return Key == other.Key && object.Equals(Params, other.Params) &&
               (Next == null
                 ? other.Next == null
                 : object.Equals(Next, other.Next));
      }
    }

    public override int GetHashCode() {
      throw new NotImplementedException();
    }
  }

  public class Trigger : Absy {
    public readonly bool Pos;
    [Rep]
    private List<Expr>/*!*/ tr;

    public IList<Expr>/*!*/ Tr
    {
      get
      {
        Contract.Ensures(Contract.Result<IList<Expr>>() != null);
        Contract.Ensures(Contract.Result<IList<Expr>>().Count >= 1);
        Contract.Ensures(this.Pos || Contract.Result<IList<Expr>>().Count == 1);
        return this.tr.AsReadOnly();
      }
      set
      {
        Contract.Requires(value != null);
        Contract.Requires(value.Count >= 1);
        Contract.Requires(this.Pos || value.Count == 1);
        this.tr = new List<Expr>(value);
      }
    }

    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(this.tr != null);
      Contract.Invariant(this.tr.Count >= 1);
      Contract.Invariant(Pos || this.tr.Count == 1);
    }

    public Trigger Next;

    public Trigger(IToken/*!*/ tok, bool pos, IEnumerable<Expr>/*!*/ tr, Trigger next = null)
      : base(tok) {
      Contract.Requires(tok != null);
      Contract.Requires(tr != null);
      Contract.Requires(tr.Count() >= 1);
      Contract.Requires(pos || tr.Count() == 1);
      this.Pos = pos;
      this.Tr = new List<Expr>(tr);
      this.Next = next;
    }

    public void Emit(TokenTextWriter stream) {
      Contract.Requires(stream != null);
      stream.SetToken(this);
      Contract.Assert(this.Tr.Count >= 1);
      string/*!*/ sep = Pos ? "{ " : "{:nopats ";
      foreach (Expr/*!*/ e in this.Tr) {
        Contract.Assert(e != null);
        stream.Write(sep);
        sep = ", ";
        e.Emit(stream);
      }
      stream.Write(" }");
    }
    public override void Resolve(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      rc.TriggerMode = true;
      foreach (Expr/*!*/ e in this.Tr) {
        Contract.Assert(e != null);
        e.Resolve(rc);

        // just a variable by itself is not allowed
        if (e is IdentifierExpr) {
          rc.Error(e, "a matching pattern must be more than just a variable by itself: {0}", e);
        }

        // the free-variable check is performed in the surrounding quantifier expression (because that's
        // where the bound variables are known)
      }
      rc.TriggerMode = false;
    }

    /// <summary>
    /// Add to "freeVars" the free variables in the triggering expressions.
    /// </summary>
    public void ComputeFreeVariables(Set /*Variable*/ freeVars) {
      Contract.Requires(freeVars != null);
      foreach (Expr/*!*/ e in this.Tr) {
        Contract.Assert(e != null);
        e.ComputeFreeVariables(freeVars);
      }
    }

    public override void Typecheck(TypecheckingContext tc) {
      //Contract.Requires(tc != null);
      foreach (Expr/*!*/ e in this.Tr) {
        Contract.Assert(e != null);
        e.Typecheck(tc);
      }
    }

    public void AddLast(Trigger other) {
      Trigger current = this;
      while (current.Next != null) {
        current = current.Next;
      }
      current.Next = other;
    }

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

    public override bool Equals(object obj) {
      var other = obj as Trigger;
      if (other == null) {
        return false;
      } else {
        return this.Tr.SequenceEqual(other.Tr) && 
          (Next == null ? other.Next == null : object.Equals(Next, other.Next));
      }
    }

    public override int GetHashCode() {
      throw new NotImplementedException();
    }
  }

  public class ForallExpr : QuantifierExpr {
    public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,
                      List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)
      : base(tok, typeParams, dummies, kv, triggers, body, immutable) {
      Contract.Requires(tok != null);
      Contract.Requires(typeParams != null);
      Contract.Requires(dummies != null);
      Contract.Requires(body != null);
      Contract.Requires(dummies.Count + typeParams.Count > 0);
    }
    public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)
      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {
      Contract.Requires(body != null);
      Contract.Requires(dummies != null);
      Contract.Requires(tok != null);
      Contract.Requires(dummies.Count > 0);
    }
    public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)
      : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {
      Contract.Requires(body != null);
      Contract.Requires(dummies != null);
      Contract.Requires(tok != null);
      Contract.Requires(dummies.Count > 0);
    }
    public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable=false)
      : base(tok, typeParams, dummies, null, null, body, immutable) {
      Contract.Requires(body != null);
      Contract.Requires(dummies != null);
      Contract.Requires(typeParams != null);
      Contract.Requires(tok != null);
      Contract.Requires(dummies.Count + typeParams.Count > 0);
    }

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

    public override BinderKind Kind {
      get {
        return BinderKind.Forall;
      }
    }
  }

  public class ExistsExpr : QuantifierExpr {
    public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ dummies,
                      QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)
      : base(tok, typeParams, dummies, kv, triggers, body, immutable) {
      Contract.Requires(tok != null);
      Contract.Requires(typeParams != null);
      Contract.Requires(dummies != null);
      Contract.Requires(body != null);
      Contract.Requires(dummies.Count + typeParams.Count > 0);
    }
    public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)
      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {
      Contract.Requires(body != null);
      Contract.Requires(dummies != null);
      Contract.Requires(tok != null);
      Contract.Requires(dummies.Count > 0);
    }
    public ExistsExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)
      : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {
      Contract.Requires(body != null);
      Contract.Requires(dummies != null);
      Contract.Requires(tok != null);
      Contract.Requires(dummies.Count > 0);
    }

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

    public override BinderKind Kind {
      get {
        return BinderKind.Exists;
      }
    }
  }

  public abstract class QuantifierExpr : BinderExpr {
    public Trigger Triggers;

    static int SkolemIds = -1;
    public static int GetNextSkolemId() {
      return System.Threading.Interlocked.Increment(ref SkolemIds);
    }

    public readonly int SkolemId;

    public QuantifierExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
                          List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable)
      : base(tok, typeParameters, dummies, kv, body, immutable) {
      Contract.Requires(tok != null);
      Contract.Requires(typeParameters != null);
      Contract.Requires(dummies != null);
      Contract.Requires(body != null);
      Contract.Requires(dummies.Count + typeParameters.Count > 0);

      Contract.Assert((this is ForallExpr) || (this is ExistsExpr));

      Triggers = triggers;
      SkolemId = GetNextSkolemId();
    }

    protected override void EmitTriggers(TokenTextWriter stream) {
      //Contract.Requires(stream != null);
      stream.push();
      for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
        tr.Emit(stream);
        stream.Write(" ");
        stream.sep();
      }
      stream.pop();
    }

    // if the user says ( forall x :: forall y ::  ... ) and specifies *no* triggers, we transform it to
    // (forall x, y ::  ... ) which may help the prover to pick trigger terms
    //
    // (Note: there used to be a different criterion here, which allowed merging when triggers were specified, which could cause prover errors due to resulting unbound variables in the triggers)
    private void MergeAdjecentQuantifier() {
      QuantifierExpr qbody = Body as QuantifierExpr;
      if (!(qbody != null && (qbody is ForallExpr) == (this is ForallExpr) && Triggers == null)) {
        return;
      }
      qbody.MergeAdjecentQuantifier();
      if (this.Triggers != null || qbody.Triggers != null) {
        return;
      }
      Body = qbody.Body;
      TypeParameters.AddRange(qbody.TypeParameters);
      Dummies.AddRange(qbody.Dummies);
      Triggers = qbody.Triggers;
      if (qbody.Attributes != null) {
        if (Attributes == null) {
          Attributes = qbody.Attributes;
        } else {
          QKeyValue p = Attributes;
          while (p.Next != null) {
            p = p.Next;
          }
          p.Next = qbody.Attributes;
        }
      }
    }

    #region never triggers
    private class NeverTriggerCollector : ReadOnlyVisitor {
      QuantifierExpr/*!*/ parent;
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(parent != null);
      }

      public NeverTriggerCollector(QuantifierExpr p) {
        Contract.Requires(p != null);
        parent = p;
      }

      public override Expr VisitNAryExpr(NAryExpr node) {
        //Contract.Requires(node != null);
        Contract.Ensures(Contract.Result<Expr>() != null);
        FunctionCall fn = node.Fun as FunctionCall;
        if (fn != null && cce.NonNull(fn.Func).NeverTrigger) {
          parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> { node} , parent.Triggers);
        }
        return base.VisitNAryExpr(node);
      }
      public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {
        // don't go into quantifier expression or its triggers, since the terms in there may have more bound variables
        // (note, with only the VisitBinderExpr override below, we'd still be visiting triggers, which we don't want to do)
        return node;
      }
      public override BinderExpr VisitBinderExpr(BinderExpr node) {
        // don't go into binder expression, since the terms in there may have more bound variables
        return node;
      }
    }

    private bool neverTriggerApplied;
    private void ApplyNeverTriggers() {
      if (neverTriggerApplied) {
        return;
      }
      neverTriggerApplied = true;

      for (Trigger t = Triggers; t != null; t = t.Next) {
        if (t.Pos) {
          return;
        }
      }

      NeverTriggerCollector visitor = new NeverTriggerCollector(this);
      visitor.VisitExpr(Body);
    }
    #endregion

    protected override void ResolveTriggers(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
        int prevErrorCount = rc.ErrorCount;
        tr.Resolve(rc);
        if (prevErrorCount == rc.ErrorCount) {
          // for positive triggers, make sure all bound variables are mentioned
          if (tr.Pos) {
            Set /*Variable*/ freeVars = new Set /*Variable*/ ();
            tr.ComputeFreeVariables(freeVars);
            foreach (Variable/*!*/ v in Dummies) {
              Contract.Assert(v != null);
              if (!freeVars[v]) {
                rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
              }
            }
          }
        }
      }
    }

    public override void Resolve(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      int oldErrorCount = rc.ErrorCount;

      this.MergeAdjecentQuantifier();

      base.Resolve(rc);

      if (oldErrorCount == rc.ErrorCount) {
        this.ApplyNeverTriggers();
      }
    }


    public override void Typecheck(TypecheckingContext tc) {
      //Contract.Requires(tc != null);
      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
        kv.Typecheck(tc);
      }
      for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
        tr.Typecheck(tc);
      }
      Body.Typecheck(tc);
      Contract.Assert(Body.Type != null);  // follows from postcondition of Expr.Typecheck
      if (!Body.Type.Unify(Type.Bool)) {
        tc.Error(this, "quantifier body must be of type bool");
      }
      this.Type = Type.Bool;

      // Check that type parameters occur in the types of the
      // dummies, or otherwise in the triggers. This can only be
      // done after typechecking
      List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
      Contract.Assert(unmentionedParameters != null);

      if (unmentionedParameters.Count > 0) {
        // all the type parameters that do not occur in dummy types
        // have to occur in triggers

        for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
          // for positive triggers, make sure all bound variables are mentioned
          if (tr.Pos) {
            Set /*Variable*/ freeVars = new Set /*Variable*/ ();
            tr.ComputeFreeVariables(freeVars);
            foreach (TypeVariable/*!*/ v in unmentionedParameters) {
              Contract.Assert(v != null);
              if (!freeVars[v])
                tc.Error(tr,
                         "trigger does not mention {0}, which does not occur in variables types either",
                         v);
            }
          }
        }
      }
    }
    public override Type/*!*/ ShallowType {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);

        return Type.Bool;
      }
    }

    public override bool Equals(object obj) {
      var other = obj as QuantifierExpr;
      if (other == null) {
        return false;
      } else {
        return this.BinderEquals(obj) && 
          (!CompareAttributesAndTriggers || object.Equals(Triggers, other.Triggers));
      }
    }
  }


  public class LambdaExpr : BinderExpr {
    public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)
      : base(tok, typeParameters, dummies, kv, body, immutable) {
      Contract.Requires(tok != null);
      Contract.Requires(typeParameters != null);
      Contract.Requires(dummies != null);
      Contract.Requires(body != null);
      Contract.Requires(dummies.Count + typeParameters.Count > 0);
    }

    public override BinderKind Kind {
      get {
        return BinderKind.Lambda;
      }
    }

    public override void Resolve(ResolutionContext rc) {
      //Contract.Requires(rc != null);
      base.Resolve(rc);
    }

    public override void Typecheck(TypecheckingContext tc) {
      //Contract.Requires(tc != null);
      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
        kv.Typecheck(tc);
      }
      Body.Typecheck(tc);
      Contract.Assert(Body.Type != null);  // follows from postcondition of Expr.Typecheck

      List<Type>/*!*/ argTypes = new List<Type>();
      foreach (Variable/*!*/ v in Dummies) {
        Contract.Assert(v != null);
        argTypes.Add(v.TypedIdent.Type);
      }
      this.Type = new MapType(this.tok, this.TypeParameters, argTypes, Body.Type);

      // Check that type parameters occur in the types of the
      // dummies, or otherwise in the triggers. This can only be
      // done after typechecking
      List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
      Contract.Assert(unmentionedParameters != null);

      if (unmentionedParameters.Count > 0) {
        tc.Error(this, "the type variable {0} does not occur in types of the lambda parameters", unmentionedParameters[0]);
      }
    }

    private Type mapType;
    public override Type/*!*/ ShallowType {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);

        if (mapType == null) {
          List<Type>/*!*/ argTypes = new List<Type>();
          foreach (Variable/*!*/ v in Dummies) {
            Contract.Assert(v != null);
            argTypes.Add(v.TypedIdent.Type);
          }
          mapType = new MapType(this.tok, this.TypeParameters, argTypes, Body.ShallowType);
        }

        return mapType;
      }
    }

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

  }
}