using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
using IToken = Microsoft.Boogie.IToken;

namespace Microsoft.Dafny
{
  public abstract class IRewriter
  {
    protected readonly ErrorReporter reporter;

    public IRewriter(ErrorReporter reporter) {
      Contract.Requires(reporter != null);
      this.reporter = reporter;
    }

    internal virtual void PreResolve(ModuleDefinition m) {
      Contract.Requires(m != null);
    }

    internal virtual void PostResolve(ModuleDefinition m) {
      Contract.Requires(m != null);
    }

    // After SCC/Cyclicity/Recursivity analysis:
    internal virtual void PostCyclicityResolve(ModuleDefinition m) {
      Contract.Requires(m != null);
    }
  }

  public class AutoGeneratedToken : TokenWrapper
  {
    public AutoGeneratedToken(Boogie.IToken wrappedToken)
      : base(wrappedToken)
    {
      Contract.Requires(wrappedToken != null);
    }
  }

  public class TriggerGeneratingRewriter : IRewriter {
    internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {
      Contract.Requires(reporter != null);
    }

    internal override void PostCyclicityResolve(ModuleDefinition m) {
      var finder = new Triggers.QuantifierCollector(reporter);
        
      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
        finder.Visit(decl, false);
      }
      
      var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext);
      foreach (var quantifierCollection in finder.quantifierCollections) {
        quantifierCollection.ComputeTriggers(triggersCollector);
        quantifierCollection.CommitTriggers();
      }
    }
  }

  internal class QuantifierSplittingRewriter : IRewriter {
    internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) {
      Contract.Requires(reporter != null);
    }

    internal override void PostResolve(ModuleDefinition m) {
      var splitter = new Triggers.QuantifierSplitter();
      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
        splitter.Visit(decl);
      }
      splitter.Commit();
    }
  }

  /// <summary>
  /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
  /// into a class.  From the user's perspective, what needs to be done is simply:
  ///  - mark the class with {:autocontracts}
  ///  - declare a function (or predicate) called Valid()
  ///  
  /// AutoContracts will then:
  ///
  /// Declare:
  ///    ghost var Repr: set(object);
  ///
  /// For function/predicate Valid(), insert:
  ///    reads this, Repr;
  /// Into body of Valid(), insert (at the beginning of the body):
  ///    this in Repr && null !in Repr
  /// and also insert, for every array-valued field A declared in the class:
  ///    (A != null ==> A in Repr) &&
  /// and for every field F of a class type T where T has a field called Repr, also insert:
  ///    (F != null ==> F in Repr && F.Repr SUBSET Repr && this !in Repr)
  /// Except, if A or F is declared with {:autocontracts false}, then the implication will not
  /// be added.
  ///
  /// For every constructor, add:
  ///    modifies this;
  ///    ensures Valid() && fresh(Repr - {this});
  /// At the end of the body of the constructor, add:
  ///    Repr := {this};
  ///    if (A != null) { Repr := Repr + {A}; }
  ///    if (F != null) { Repr := Repr + {F} + F.Repr; }
  ///
  /// For every method, add:
  ///    requires Valid();
  ///    modifies Repr;
  ///    ensures Valid() && fresh(Repr - old(Repr));
  /// At the end of the body of the method, add:
  ///    if (A != null) { Repr := Repr + {A}; }
  ///    if (F != null) { Repr := Repr + {F} + F.Repr; }
  /// </summary>
  public class AutoContractsRewriter : IRewriter
  {
    public AutoContractsRewriter(ErrorReporter reporter)
      : base(reporter) {
      Contract.Requires(reporter != null);
    }

    internal override void PreResolve(ModuleDefinition m) {
      foreach (var d in m.TopLevelDecls) {
        bool sayYes = true;
        if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {
          ProcessClassPreResolve((ClassDecl)d);
        }
      }
    }

    void ProcessClassPreResolve(ClassDecl cl) {
      // Add:  ghost var Repr: set<object>;
      // ...unless a field with that name is already present
      if (!cl.Members.Exists(member => member is Field && member.Name == "Repr")) {
        Type ty = new SetType(true, new ObjectType());
        cl.Members.Add(new Field(new AutoGeneratedToken(cl.tok), "Repr", true, ty, null));
      }

      foreach (var member in cl.Members) {
        bool sayYes = true;
        if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {
          // the user has excluded this member
          continue;
        }
        if (member.RefinementBase != null) {
          // member is inherited from a module where it was already processed
          continue;
        }
        Boogie.IToken tok = new AutoGeneratedToken(member.tok);
        if (member is Function && member.Name == "Valid" && !member.IsStatic) {
          var valid = (Function)member;
          // reads this;
          valid.Reads.Add(new FrameExpression(tok, new ThisExpr(tok), null));
          // reads Repr;
          valid.Reads.Add(new FrameExpression(tok, new MemberSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null));
        } else if (member is Constructor) {
          var ctor = (Constructor)member;
          // modifies this;
          ctor.Mod.Expressions.Add(new FrameExpression(tok, new ImplicitThisExpr(tok), null));
          // ensures Valid();
          ctor.Ens.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List<Expression>())));
          // ensures fresh(Repr - {this});
          var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, new BinaryExpr(tok, BinaryExpr.Opcode.Sub,
            new MemberSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"),
            new SetDisplayExpr(tok, true, new List<Expression>() { new ThisExpr(tok) })));
          ctor.Ens.Insert(1, new MaybeFreeExpression(freshness));
        } else if (member is Method && !member.IsStatic) {
          var m = (Method)member;
          // requires Valid();
          m.Req.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List<Expression>())));
          // If this is a mutating method, we should also add a modifies clause and a postcondition, but we don't do that if it's
          // a simple query method.  However, we won't know if it's a simple query method until after resolution, so we'll add the
          // rest of the spec then.
        }
      }
    }

    internal override void PostResolve(ModuleDefinition m) {
      foreach (var d in m.TopLevelDecls) {
        bool sayYes = true;
        if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {
          ProcessClassPostResolve((ClassDecl)d);
        }
      }
    }

    void ProcessClassPostResolve(ClassDecl cl) {
      // Find all fields of a reference type, and make a note of whether or not the reference type has a Repr field.
      // Also, find the Repr field and the function Valid in class "cl"
      Field ReprField = null;
      Function Valid = null;
      var subobjects = new List<Tuple<Field, Field>>();
      foreach (var member in cl.Members) {
        var field = member as Field;
        if (field != null) {
          bool sayYes = true;
          if (field.Name == "Repr") {
            ReprField = field;
          } else if (Attributes.ContainsBool(field.Attributes, "autocontracts", ref sayYes) && !sayYes) {
            // ignore this field
          } else if (field.Type is ObjectType) {
            subobjects.Add(new Tuple<Field, Field>(field, null));
          } else if (field.Type.IsRefType) {
            var rcl = (ClassDecl)((UserDefinedType)field.Type).ResolvedClass;
            Field rRepr = null;
            foreach (var memb in rcl.Members) {
              var f = memb as Field;
              if (f != null && f.Name == "Repr") {
                rRepr = f;
                break;
              }
            }
            subobjects.Add(new Tuple<Field, Field>(field, rRepr));
          }
        } else if (member is Function && member.Name == "Valid" && !member.IsStatic) {
          var fn = (Function)member;
          if (fn.Formals.Count == 0 && fn.ResultType.IsBoolType) {
            Valid = fn;
          }
        }
      }
      Contract.Assert(ReprField != null);  // we expect there to be a "Repr" field, since we added one in PreResolve

      Boogie.IToken clTok = new AutoGeneratedToken(cl.tok);
      Type ty = UserDefinedType.FromTopLevelDecl(clTok, cl);
      var self = new ThisExpr(clTok);
      self.Type = ty;
      var implicitSelf = new ImplicitThisExpr(clTok);
      implicitSelf.Type = ty;
      var Repr = new MemberSelectExpr(clTok, implicitSelf, "Repr");
      Repr.Member = ReprField;
      Repr.Type = ReprField.Type;
      var cNull = new LiteralExpr(clTok);
      cNull.Type = new ObjectType();

      foreach (var member in cl.Members) {
        bool sayYes = true;
        if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {
          continue;
        }
        Boogie.IToken tok = new AutoGeneratedToken(member.tok);
        if (member is Function && member.Name == "Valid" && !member.IsStatic) {
          var valid = (Function)member;
          if (valid.IsGhost && valid.ResultType.IsBoolType) {
            Expression c;
            if (valid.RefinementBase == null) {
              var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr);  // this in Repr
              var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, cNull, Repr);  // null !in Repr
              c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c0, c1);
            } else {
              c = new LiteralExpr(tok, true);
              c.Type = Type.Bool;
            }

            foreach (var ff in subobjects) {
              if (ff.Item1.RefinementBase != null) {
                // the field has been inherited from a refined module, so don't include it here
                continue;
              }
              var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null);
              var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);
              var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);
              if (ff.Item2 == null) {
                // F != null ==> F in Repr  (so, nothing else to do)
              } else {
                // F != null ==> F in Repr && F.Repr <= Repr && this !in F.Repr
                var FRepr = new MemberSelectExpr(tok, F, ff.Item2.Name);
                FRepr.Member = ff.Item2;
                FRepr.Type = ff.Item2.Type;
                var c2 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.Subset, FRepr, Repr);
                var c3 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, self, FRepr);
                c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c1, BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c2, c3));
              }
              c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c, BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.Imp, c0, c1));
            }

            if (valid.Body == null) {
              valid.Body = c;
            } else {
              valid.Body = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c, valid.Body);
            }
          }

        } else if (member is Constructor) {
          var ctor = (Constructor)member;
          if (ctor.Body != null) {
            var bodyStatements = ((BlockStmt)ctor.Body).Body;
            // Repr := {this};
            var e = new SetDisplayExpr(tok, true, new List<Expression>() { self });
            e.Type = new SetType(true, new ObjectType());
            Statement s = new AssignStmt(tok, tok, Repr, new ExprRhs(e));
            s.IsGhost = true;
            bodyStatements.Add(s);

            AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
          }

        } else if (member is Method && !member.IsStatic) {
          var m = (Method)member;
          if (Valid != null && !IsSimpleQueryMethod(m)) {
            if (member.RefinementBase == null) {
              // modifies Repr;
              m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null));
              // ensures Valid();
              var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());
              valid.Function = Valid;
              valid.Type = Type.Bool;
              // Add the identity substitution to this call
              valid.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
              foreach (var p in cl.TypeArgs) {
                valid.TypeArgumentSubstitutions.Add(p, new UserDefinedType(p)); 
              }
              m.Ens.Insert(0, new MaybeFreeExpression(valid));
              // ensures fresh(Repr - old(Repr));
              var e0 = new OldExpr(tok, Repr);
              e0.Type = Repr.Type;
              var e1 = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, Repr, e0);
              e1.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference;
              e1.Type = Repr.Type;
              var freshness = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Fresh, e1);
              freshness.Type = Type.Bool;
              m.Ens.Insert(1, new MaybeFreeExpression(freshness));
            }

            if (m.Body != null) {
              var bodyStatements = ((BlockStmt)m.Body).Body;
              AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
            }
          }
        }
      }
    }

    void AddSubobjectReprs(Boogie.IToken tok, List<Tuple<Field, Field>> subobjects, List<Statement> bodyStatements,
      Expression self, Expression implicitSelf, Expression cNull, Expression Repr) {
      // TODO: these assignments should be included on every return path

      foreach (var ff in subobjects) {
        var F = Resolver.NewMemberSelectExpr(tok, implicitSelf, ff.Item1, null);  // create a resolved MemberSelectExpr
        Expression e = new SetDisplayExpr(tok, true, new List<Expression>() { F });
        e.Type = new SetType(true, new ObjectType());  // resolve here
        var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);
        rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here
        rhs.Type = Repr.Type;  // resolve here
        if (ff.Item2 == null) {
          // Repr := Repr + {F}  (so, nothing else to do)
        } else {
          // Repr := Repr + {F} + F.Repr
          var FRepr = Resolver.NewMemberSelectExpr(tok, F, ff.Item2, null);  // create resolved MemberSelectExpr
          rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, rhs, FRepr);
          rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here
          rhs.Type = Repr.Type;  // resolve here
        }
        // Repr := Repr + ...;
        Statement s = new AssignStmt(tok, tok, Repr, new ExprRhs(rhs));
        s.IsGhost = true;
        // wrap if statement around s
        e = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);
        var thn = new BlockStmt(tok, tok, new List<Statement>() { s });
        thn.IsGhost = true;
        s = new IfStmt(tok, tok, false, e, thn, null);
        s.IsGhost = true;
        // finally, add s to the body
        bodyStatements.Add(s);
      }
    }

    bool IsSimpleQueryMethod(Method m) {
      // A simple query method has out parameters, its body has no effect other than to assign to them,
      // and the postcondition does not explicitly mention the pre-state.
      return m.Outs.Count != 0 && m.Body != null && LocalAssignsOnly(m.Body) &&
        m.Ens.TrueForAll(mfe => !MentionsOldState(mfe.E));
    }

    bool LocalAssignsOnly(Statement s) {
      Contract.Requires(s != null);
      if (s is AssignStmt) {
        var ss = (AssignStmt)s;
        return ss.Lhs.Resolved is IdentifierExpr;
      } else if (s is ConcreteUpdateStatement) {
        var ss = (ConcreteUpdateStatement)s;
        return ss.Lhss.TrueForAll(e => e.Resolved is IdentifierExpr);
      } else if (s is CallStmt) {
        return false;
      } else {
        foreach (var ss in s.SubStatements) {
          if (!LocalAssignsOnly(ss)) {
            return false;
          }
        }
      }
      return true;
    }

    /// <summary>
    /// Returns true iff 'expr' is a two-state expression, that is, if it mentions "old(...)" or "fresh(...)".
    /// </summary>
    static bool MentionsOldState(Expression expr) {
      Contract.Requires(expr != null);
      if (expr is OldExpr) {
        return true;
      } else if (expr is UnaryOpExpr && ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh) {
        return true;
      }
      foreach (var ee in expr.SubExpressions) {
        if (MentionsOldState(ee)) {
          return true;
        }
      }
      return false;
    }

    public static BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {
      var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);
      p.ResolvedOp = rop;  // resolve here
      p.Type = Type.Bool;  // resolve here
      return p;
    }
  }


  /// <summary>
  /// For any function foo() with the :opaque attribute,
  /// hide the body, so that it can only be seen within its
  /// recursive clique (if any), or if the programmer
  /// specifically asks to see it via the reveal_foo() lemma
  /// </summary>
  public class OpaqueFunctionRewriter : IRewriter {
    protected Dictionary<Function, Function> fullVersion; // Given an opaque function, retrieve the full
    protected Dictionary<Function, Function> original;    // Given a full version of an opaque function, find the original opaque version
    protected Dictionary<Lemma, Function> revealOriginal; // Map reveal_* lemmas back to their original functions

    public OpaqueFunctionRewriter(ErrorReporter reporter)
      : base(reporter) {
      Contract.Requires(reporter != null);

      fullVersion = new Dictionary<Function, Function>();
      original = new Dictionary<Function, Function>();
      revealOriginal = new Dictionary<Lemma, Function>();
    }

    internal override void PreResolve(ModuleDefinition m) {
      foreach (var d in m.TopLevelDecls) {
        if (d is ClassDecl) {
          DuplicateOpaqueClassFunctions((ClassDecl)d);
        }
      }
    }    

    internal override void PostResolve(ModuleDefinition m) {
      // Fix up the ensures clause of the full version of the function,
      // since it may refer to the original opaque function      
      foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) {        
        if (isFullVersion(fn)) {  // Is this a function we created to supplement an opaque function?                  
          OpaqueFunctionVisitor visitor = new OpaqueFunctionVisitor();
          var context = new OpaqueFunctionContext(original[fn], fn);

          foreach (Expression ens in fn.Ens) {
            visitor.Visit(ens, context);
          }
        } 
      }

      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
        if (decl is Lemma) {
          var lem = (Lemma)decl;
          if (revealOriginal.ContainsKey(lem)) {
            fixupRevealLemma(lem, revealOriginal[lem]);
            fixupTypeArguments(lem, revealOriginal[lem]);
          }
        }
      }
    }

    internal override void PostCyclicityResolve(ModuleDefinition m) {
      // Add layer quantifier if the function is recursive 
      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
        if (decl is Lemma) {
          var lem = (Lemma)decl;
          if (revealOriginal.ContainsKey(lem)) {
            needsLayerQuantifier(lem, revealOriginal[lem]);
          }
        }
      }
    }
  
    // Is f the full version of an opaque function?
    public bool isFullVersion(Function f) {
      return original.ContainsKey(f);
    }
    
    // In case we change how opacity is denoted
    public bool isOpaque(Function f) {
      return fullVersion.ContainsKey(f);
    }

    public Function OpaqueVersion(Function f) {
      Function ret;
      original.TryGetValue(f, out ret);
      return ret;
    }

    public Function FullVersion(Function f) {
      Function ret;
      fullVersion.TryGetValue(f, out ret);
      return ret;
    }

    // Trims the body from the original function and then adds an internal,
    // full version, along with a lemma connecting the two
    protected void DuplicateOpaqueClassFunctions(ClassDecl c) {
      List<MemberDecl> newDecls = new List<MemberDecl>();
      foreach (MemberDecl member in c.Members) {
        if (member is Function) {
          var f = (Function)member;

          if (!Attributes.Contains(f.Attributes, "opaque")) {
            // Nothing to do
          } else if (f.IsProtected) {
            reporter.Error(MessageSource.Rewriter, f.tok, ":opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)");
          } else if (!RefinementToken.IsInherited(f.tok, c.Module)) {
            // Create a copy, which will be the internal version with a full body
            // which will allow us to verify that the ensures are true
            var cloner = new Cloner();
            var fWithBody = cloner.CloneFunction(f, "#" + f.Name + "_FULL");  
            newDecls.Add(fWithBody);
            fullVersion.Add(f, fWithBody);
            original.Add(fWithBody, f);

            var newToken = new Boogie.Token(f.tok.line, f.tok.col);
            newToken.filename = f.tok.filename;
            newToken._val = fWithBody.Name;
            newToken._kind = f.tok.kind;
            newToken._pos = f.tok.pos;
            fWithBody.tok = (f.tok is IncludeToken) ? new IncludeToken(newToken) : (Boogie.IToken)newToken;

            // Annotate the new function so we remember that we introduced it
            fWithBody.Attributes = new Attributes("opaque_full", new List<Expression>(), fWithBody.Attributes);
            fWithBody.Attributes = new Attributes("auto_generated", new List<Expression>(), fWithBody.Attributes);

            // Create a lemma to allow the user to selectively reveal the function's body          
            // That is, given:
            //   function {:opaque} foo(x:int, y:int) : int
            //     requires 0 <= x < 5;
            //     requires 0 <= y < 5;
            //     ensures foo(x, y) < 10;
            //   { x + y }
            // We produce:
            //   lemma {:axiom} {:auto_generated} reveal_foo()
            //     ensures forall x:int, y:int {:trigger foo(x,y)} :: 0 <= x < 5 && 0 <= y < 5 ==> foo(x,y) == foo_FULL(x,y);
            Expression reqExpr = new LiteralExpr(f.tok, true);
            foreach (Expression req in f.Req) {
              Expression newReq = cloner.CloneExpr(req);
              reqExpr = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, reqExpr, newReq);
            }

            List<TypeParameter> typeVars = new List<TypeParameter>();
            foreach (TypeParameter tp in f.TypeArgs) {
              typeVars.Add(cloner.CloneTypeParam(tp));
            }

            var boundVars = f.Formals.ConvertAll(formal => new BoundVar(formal.tok, formal.Name, cloner.CloneType(formal.Type)));

            // Build the implication connecting the function's requires to the connection with the revealed-body version
            Func<Function, Expression> func_builder = func =>
              new ApplySuffix(func.tok,
                new NameSegment(func.tok, func.Name, null),
                func.Formals.ConvertAll(x => (Expression)new IdentifierExpr(func.tok, x.Name)));
            var oldEqualsNew = new BinaryExpr(f.tok, BinaryExpr.Opcode.Eq, func_builder(f), func_builder(fWithBody));
            var requiresImpliesOldEqualsNew = new BinaryExpr(f.tok, BinaryExpr.Opcode.Imp, reqExpr, oldEqualsNew);            

            MaybeFreeExpression newEnsures;
            if (f.Formals.Count > 0) {
              // Build an explicit trigger for the forall, so Z3 doesn't get confused
              Expression trigger = func_builder(f);
              List<Expression> args = new List<Expression>();
              args.Add(trigger);
              Attributes attrs = new Attributes("trigger", args, null);

              // Also specify that this is a type quantifier
              attrs = new Attributes("typeQuantifier", new List<Expression>(), attrs);

              newEnsures = new MaybeFreeExpression(new ForallExpr(f.tok, typeVars, boundVars, null, requiresImpliesOldEqualsNew, attrs));
            } else {
              // No need for a forall
              newEnsures = new MaybeFreeExpression(oldEqualsNew);
            }
            var newEnsuresList = new List<MaybeFreeExpression>();
            newEnsuresList.Add(newEnsures);

            // Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body
            Attributes lemma_attrs = new Attributes("axiom", new List<Expression>(), null);
            lemma_attrs = new Attributes("auto_generated", new List<Expression>(), lemma_attrs);

            var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),
                                    new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,
                                    new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
            newDecls.Add(reveal);
            revealOriginal[reveal] = f;

            // Update f's body to simply call the full version, so we preserve recursion checks, decreases clauses, etc.
            f.Body = func_builder(fWithBody);
          }
        }
      }
      c.Members.AddRange(newDecls);
    }    

    protected class OpaqueFunctionContext {
      public Function original;   // The original declaration of the opaque function
      public Function full;       // The version we added that has a body

      public OpaqueFunctionContext(Function Orig, Function Full) {
        original = Orig;
        full = Full;
      }
    }

    class OpaqueFunctionVisitor : TopDownVisitor<OpaqueFunctionContext> {
      protected override bool VisitOneExpr(Expression expr, ref OpaqueFunctionContext context) {
        if (expr is FunctionCallExpr) {
          var e = (FunctionCallExpr)expr;

          if (e.Function == context.original) { // Attempting to call the original opaque function
            // Redirect the call to the full version and its type-argument substitution map
            // First, do some sanity checks:
            Contract.Assert(e.TypeArgumentSubstitutions.Count == context.original.EnclosingClass.TypeArgs.Count + context.original.TypeArgs.Count);
            Contract.Assert(context.original.EnclosingClass == context.full.EnclosingClass);
            Contract.Assert(context.original.TypeArgs.Count == context.full.TypeArgs.Count);
            if (context.full.TypeArgs.Count != 0) {
              var newTypeArgsSubst = new Dictionary<TypeParameter, Type>();
              context.original.EnclosingClass.TypeArgs.ForEach(tp => newTypeArgsSubst.Add(tp, e.TypeArgumentSubstitutions[tp]));
              for (int i = 0; i < context.original.TypeArgs.Count; i++) {
                var tpOrig = context.original.TypeArgs[i];
                var tpFull = context.full.TypeArgs[i];
                newTypeArgsSubst.Add(tpFull, e.TypeArgumentSubstitutions[tpOrig]);
              }
              e.TypeArgumentSubstitutions = newTypeArgsSubst;
            }
            e.Function = context.full;
          }
        }
        return true;
      }
    }

    // If the function is recursive, make the reveal lemma quantifier a layerQuantifier
    protected void needsLayerQuantifier(Lemma lem, Function fn) {
      var origForall = lem.Ens[0].E as ForallExpr;
      if (origForall != null && fn.IsRecursive) {
        var newAttrib = new Attributes("layerQuantifier", new List<Expression>(), origForall.Attributes);
        var newForall = new ForallExpr(origForall.tok, origForall.TypeArgs, origForall.BoundVars, origForall.Range, origForall.Term, newAttrib);
        newForall.Type = Type.Bool;
        lem.Ens[0] = new MaybeFreeExpression(newForall);
      }
    }

    // This is for the reveal_F function. The ensures clause looks like this:
    // 
    //     ensures forall<A,B> x : T<A,B> :: F(x) == F_FULL(x)
    //
    // But the type argument substitutions for F and F_FULL are way off, so 
    // we use this function to make a substitution to the type variables the
    // forall quantifier binds.
    protected void fixupTypeArguments(Lemma lem, Function fn) {
      var origForall = lem.Ens[0].E as ForallExpr;
      if (origForall != null) {
        Contract.Assert(origForall.TypeArgs.Count == fn.TypeArgs.Count);
        fixupTypeArguments(lem.Ens[0].E, fn, origForall.TypeArgs);
      }
    }

    // Type argument substitution for the fn_FULL function using the orginal 
    // fn function.
    protected void fixupTypeArguments(Expression expr, Function fn, List<TypeParameter> qparams) {
      FunctionCallExpr e;
      if (((e = expr as FunctionCallExpr) != null) && (e.Function == fullVersion[fn])) {
        var newTypeArgsSubst = new Dictionary<TypeParameter, Type>();
        fn.EnclosingClass.TypeArgs.ForEach(tp => newTypeArgsSubst.Add(tp, e.TypeArgumentSubstitutions[tp]));
        for (int i = 0; i < e.Function.TypeArgs.Count; i++) {
          newTypeArgsSubst.Add(e.Function.TypeArgs[i], new UserDefinedType(qparams[i]));
        }
        e.TypeArgumentSubstitutions = newTypeArgsSubst;
      }
      foreach (var ee in expr.SubExpressions) {
        fixupTypeArguments(ee, fn, qparams);
      }
    }

    protected void fixupRevealLemma(Lemma lem, Function fn) {
      if (fn.Req.Count == 0) {
        return;
      }

      // DR: Note: I don't know of any example that actually gets to these lines below: 

      // Consolidate the requirements
      Expression reqs = Expression.CreateBoolLiteral(fn.tok, true);
      foreach (var expr in fn.Req) {
        reqs = Expression.CreateAnd(reqs, expr);
      }

      if (fn.Formals.Count == 0)
      {
          lem.Ens[0] = new MaybeFreeExpression(Expression.CreateImplies(reqs, lem.Ens[0].E));
          return;
      }

      var origForall = (ForallExpr)lem.Ens[0].E;
      var origImpl = (BinaryExpr)origForall.Term;

      // Substitute the forall's variables for those of the fn
      var formals = fn.Formals.ConvertAll<NonglobalVariable>(x => (NonglobalVariable)x);
      var typeMap = Util.Dict<TypeParameter, Type>(fn.TypeArgs, Util.Map(origForall.TypeArgs, x => new UserDefinedType(x)));
      reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs, typeMap);

      var newImpl = Expression.CreateImplies(reqs, origImpl.E1);
      //var newForall = Expression.CreateQuantifier(origForall, true, newImpl);
      var newForall = new ForallExpr(origForall.tok, origForall.TypeArgs, origForall.BoundVars, origForall.Range, newImpl, origForall.Attributes);
      newForall.Type = Type.Bool;

      lem.Ens[0] = new MaybeFreeExpression(newForall);
    }

  }


  /// <summary>
  /// Automatically accumulate requires for function calls within a function body, 
  /// if requested via {:autoreq}
  /// </summary>
  public class AutoReqFunctionRewriter : IRewriter {
    Function parentFunction;
    OpaqueFunctionRewriter opaqueInfo;
    bool containsMatch; // TODO: Track this per-requirement, rather than per-function

    public AutoReqFunctionRewriter(ErrorReporter reporter, OpaqueFunctionRewriter o)
      : base(reporter) {
      Contract.Requires(reporter != null);
      this.opaqueInfo = o;
    }

    internal override void PostResolve(ModuleDefinition m) {
      var components = m.CallGraph.TopologicallySortedComponents();

      foreach (var scComponent in components) {  // Visit the call graph bottom up, so anything we call already has its prequisites calculated
        if (scComponent is Function) {
          Function fn = (Function)scComponent;
          if (Attributes.ContainsBoolAtAnyLevel(fn, "autoReq")) {
            parentFunction = fn;  // Remember where the recursion started
            containsMatch = false;  // Assume no match statements are involved

            if (!opaqueInfo.isOpaque(fn)) { // It's a normal function
              List<Expression> auto_reqs = new List<Expression>();

              // First handle all of the requirements' preconditions
              foreach (Expression req in fn.Req) {
                auto_reqs.AddRange(generateAutoReqs(req));
              }
              fn.Req.InsertRange(0, auto_reqs); // Need to come before the actual requires
              addAutoReqToolTipInfoToFunction("pre", fn, auto_reqs);

              // Then the body itself, if any          
              if (fn.Body != null) {
                auto_reqs = generateAutoReqs(fn.Body);
                fn.Req.AddRange(auto_reqs);
                addAutoReqToolTipInfoToFunction("post", fn, auto_reqs);
              }
            } else {  // Opaque functions need special handling
              // The opaque function's requirements are the same as for the _FULL version,
              // so we don't need to generate them again.  We do, however, need to swap
              // the function's variables for those of the FULL version

              List<Expression> fnVars = new List<Expression>();
              foreach (var formal in fn.Formals) {
                var id = new IdentifierExpr(formal.tok, formal.Name);
                id.Var = formal;  // resolve here
                id.Type = formal.Type;  // resolve here
                fnVars.Add(id);
              }

              var new_reqs = new List<Expression>();
              foreach (var req in opaqueInfo.FullVersion(fn).Req) {
                new_reqs.Add(subVars(opaqueInfo.FullVersion(fn).Formals, fnVars, req, null));
              }

              fn.Req.Clear();
              fn.Req.AddRange(new_reqs);
            }
          }
        }
        else if (scComponent is Method)
        {
            Method method = (Method)scComponent;
            if (Attributes.ContainsBoolAtAnyLevel(method, "autoReq"))
            {
                parentFunction = null;
                containsMatch = false; // Assume no match statements are involved

                List<MaybeFreeExpression> auto_reqs = new List<MaybeFreeExpression>();
                foreach (MaybeFreeExpression req in method.Req)
                {
                    List<Expression> local_auto_reqs = generateAutoReqs(req.E);
                    foreach (Expression local_auto_req in local_auto_reqs)
                    {
                        auto_reqs.Add(new MaybeFreeExpression(local_auto_req, !req.IsFree));
                    }
                }
                method.Req.InsertRange(0, auto_reqs); // Need to come before the actual requires
                addAutoReqToolTipInfoToMethod("pre", method, auto_reqs);
            }
        }
      }
    }

    Expression subVars(List<Formal> formals, List<Expression> values, Expression e, Expression f_this) {
      Contract.Assert(formals != null);
      Contract.Assert(values != null);
      Contract.Assert(formals.Count == values.Count);
      Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
      Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();

      for (int i = 0; i < formals.Count; i++) {
        substMap.Add(formals[i], values[i]);
      }

      Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);
      return sub.Substitute(e);
    }

    public void addAutoReqToolTipInfoToFunction(string label, Function f, List<Expression> reqs) {
      string prefix = "auto requires " + label + " ";
      string tip = "";

      string sep = "";
      foreach (var req in reqs) {
        if (containsMatch) {  // Pretty print the requirements
          tip += sep + prefix + Printer.ExtendedExprToString(req) + ";";
        } else {
          tip += sep + prefix + Printer.ExprToString(req) + ";";
        }
        sep = "\n";
      }

      if (!tip.Equals("")) {
        reporter.Info(MessageSource.Rewriter, f.tok, tip);
        if (DafnyOptions.O.AutoReqPrintFile != null) {
          using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {
            writer.WriteLine(f.Name);
            writer.WriteLine("\t" + tip);
          }
        }
      }
    }

    public void addAutoReqToolTipInfoToMethod(string label, Method method, List<MaybeFreeExpression> reqs) {
      string tip = "";

      foreach (var req in reqs) {
        string prefix = "auto ";
        if (req.IsFree) {
          prefix += "free ";
        }
        prefix += " requires " + label + " ";
        if (containsMatch) {  // Pretty print the requirements
          tip += prefix + Printer.ExtendedExprToString(req.E) + ";\n";
        } else {
          tip += prefix + Printer.ExprToString(req.E) + ";\n";
        }
      }

      if (!tip.Equals("")) {
        reporter.Info(MessageSource.Rewriter, method.tok, tip);
        if (DafnyOptions.O.AutoReqPrintFile != null) {
          using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {
            writer.WriteLine(method.Name);
            writer.WriteLine("\t" + tip);
          }
        }
      }
    }

    // Stitch a list of expressions together with logical ands
    Expression andify(Bpl.IToken tok, List<Expression> exprs) {
      Expression ret = Expression.CreateBoolLiteral(tok, true); 

      foreach (var expr in exprs) {        
        ret = Expression.CreateAnd(ret, expr);
      }   

      return ret;
    }
   
    List<Expression> gatherReqs(Function f, List<Expression> args, Expression f_this) {
      List<Expression> translated_f_reqs = new List<Expression>();

      if (f.Req.Count > 0) {
        Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable,Expression>();
        Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter,Type>();

        for (int i = 0; i < f.Formals.Count; i++) {
          substMap.Add(f.Formals[i], args[i]);
        }

        foreach (var req in f.Req) {
          Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);          
          translated_f_reqs.Add(sub.Substitute(req));         
        }
      }

      return translated_f_reqs;
    }

    List<Expression> generateAutoReqs(Expression expr) {
      List<Expression> reqs = new List<Expression>();

      if (expr is LiteralExpr) {      
      } else if (expr is ThisExpr) {
      } else if (expr is IdentifierExpr) {
      } else if (expr is SetDisplayExpr) {
        SetDisplayExpr e = (SetDisplayExpr)expr;

        foreach (var elt in e.Elements) {
          reqs.AddRange(generateAutoReqs(elt));
        }
      } else if (expr is MultiSetDisplayExpr) {
        MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
        foreach (var elt in e.Elements) {
          reqs.AddRange(generateAutoReqs(elt));
        }
      } else if (expr is SeqDisplayExpr) {
        SeqDisplayExpr e = (SeqDisplayExpr)expr;
        foreach (var elt in e.Elements) {
          reqs.AddRange(generateAutoReqs(elt));
        }
      } else if (expr is MapDisplayExpr) {
        MapDisplayExpr e = (MapDisplayExpr)expr;

        foreach (ExpressionPair p in e.Elements) {
          reqs.AddRange(generateAutoReqs(p.A));
          reqs.AddRange(generateAutoReqs(p.B));        
        }
      } else if (expr is MemberSelectExpr) {
        MemberSelectExpr e = (MemberSelectExpr)expr;
        Contract.Assert(e.Member != null && e.Member is Field);

        reqs.AddRange(generateAutoReqs(e.Obj));       
      } else if (expr is SeqSelectExpr) {
        SeqSelectExpr e = (SeqSelectExpr)expr;

        reqs.AddRange(generateAutoReqs(e.Seq));
        if (e.E0 != null) {
          reqs.AddRange(generateAutoReqs(e.E0));
        }

        if (e.E1 != null) {
          reqs.AddRange(generateAutoReqs(e.E1));
        }
      } else if (expr is SeqUpdateExpr) {
        SeqUpdateExpr e = (SeqUpdateExpr)expr;
        reqs.AddRange(generateAutoReqs(e.Seq));
        reqs.AddRange(generateAutoReqs(e.Index));
        reqs.AddRange(generateAutoReqs(e.Value));
      } else if (expr is DatatypeUpdateExpr) {
        foreach (var ee in expr.SubExpressions) {
          reqs.AddRange(generateAutoReqs(ee));
        }
      } else if (expr is FunctionCallExpr) {
        FunctionCallExpr e = (FunctionCallExpr)expr;

        // All of the arguments need to be satisfied
        foreach (var arg in e.Args) {
          reqs.AddRange(generateAutoReqs(arg));
        }

        if (parentFunction != null && ModuleDefinition.InSameSCC(e.Function, parentFunction)) {
          // We're making a call within the same SCC, so don't descend into this function
        } else {
          reqs.AddRange(gatherReqs(e.Function, e.Args, e.Receiver));
        }
      } else if (expr is DatatypeValue) {         
        DatatypeValue dtv = (DatatypeValue)expr;
        Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved
        for (int i = 0; i < dtv.Arguments.Count; i++) {
          Expression arg = dtv.Arguments[i];
          reqs.AddRange(generateAutoReqs(arg));
        }              
      } else if (expr is OldExpr) {  
      } else if (expr is MatchExpr) {
        MatchExpr e = (MatchExpr)expr;
        containsMatch = true;
        reqs.AddRange(generateAutoReqs(e.Source));
        
        List<MatchCaseExpr> newMatches = new List<MatchCaseExpr>();
        foreach (MatchCaseExpr caseExpr in e.Cases) {
          //MatchCaseExpr c = new MatchCaseExpr(caseExpr.tok, caseExpr.Id, caseExpr.Arguments, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));
          //c.Ctor = caseExpr.Ctor; // resolve here
          MatchCaseExpr c = Expression.CreateMatchCase(caseExpr, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));
          newMatches.Add(c);
        }
        
        reqs.Add(Expression.CreateMatch(e.tok, e.Source, newMatches, e.Type));
      } else if (expr is MultiSetFormingExpr) {
        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
        reqs.AddRange(generateAutoReqs(e.E));
      } else if (expr is UnaryExpr) {
        UnaryExpr e = (UnaryExpr)expr;
        Expression arg = e.E;                
        reqs.AddRange(generateAutoReqs(arg));
      } else if (expr is BinaryExpr) {
        BinaryExpr e = (BinaryExpr)expr;
  
        switch (e.ResolvedOp) {
          case BinaryExpr.ResolvedOpcode.Imp:
          case BinaryExpr.ResolvedOpcode.And:
            reqs.AddRange(generateAutoReqs(e.E0));
            foreach (var req in generateAutoReqs(e.E1)) {
              // We only care about this req if E0 is true, since And short-circuits              
              reqs.Add(Expression.CreateImplies(e.E0, req));  
            }
            break;

          case BinaryExpr.ResolvedOpcode.Or:
            reqs.AddRange(generateAutoReqs(e.E0));
            foreach (var req in generateAutoReqs(e.E1)) {
              // We only care about this req if E0 is false, since Or short-circuits              
              reqs.Add(Expression.CreateImplies(Expression.CreateNot(e.E1.tok, e.E0), req));
            }
            break;

          default:
            reqs.AddRange(generateAutoReqs(e.E0));
            reqs.AddRange(generateAutoReqs(e.E1));
            break;
        }   
      } else if (expr is TernaryExpr) {
        var e = (TernaryExpr)expr;

        reqs.AddRange(generateAutoReqs(e.E0));
        reqs.AddRange(generateAutoReqs(e.E1));
        reqs.AddRange(generateAutoReqs(e.E2));
      } else if (expr is LetExpr) {
        var e = (LetExpr)expr;

        if (e.Exact) {
          foreach (var rhs in e.RHSs) {
            reqs.AddRange(generateAutoReqs(rhs));
          }
          var new_reqs = generateAutoReqs(e.Body);
          if (new_reqs.Count > 0) {                 
            reqs.Add(Expression.CreateLet(e.tok, e.LHSs, e.RHSs, andify(e.tok, new_reqs), e.Exact));
          }
        } else {
          // TODO: Still need to figure out what the right choice is here:
          // Given: var x :| g(x); f(x, y) do we:
          //    1) Update the original statement to be: var x :| g(x) && WP(f(x,y)); f(x, y)
          //    2) Add forall x :: g(x) ==> WP(f(x, y)) to the function's requirements
          //    3) Current option -- do nothing.  Up to the spec writer to fix
        }
      } else if (expr is NamedExpr) {
        reqs.AddRange(generateAutoReqs(((NamedExpr)expr).Body));
      } else if (expr is QuantifierExpr) {
        QuantifierExpr e = (QuantifierExpr)expr;

        // See LetExpr for issues with the e.Range

        var auto_reqs = generateAutoReqs(e.Term);
        if (auto_reqs.Count > 0) {
            Expression allReqsSatisfied = andify(e.Term.tok, auto_reqs);
            Expression allReqsSatisfiedAndTerm = Expression.CreateAnd(allReqsSatisfied, e.Term);
            e.UpdateTerm(allReqsSatisfiedAndTerm);
            reporter.Info(MessageSource.Rewriter, e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&");
        }
      } else if (expr is SetComprehension) {
        var e = (SetComprehension)expr;
        // Translate "set xs | R :: T" 

        // See LetExpr for issues with the e.Range
        //reqs.AddRange(generateAutoReqs(e.Range));
        var auto_reqs = generateAutoReqs(e.Term);
        if (auto_reqs.Count > 0) {
          reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, new List<TypeParameter>(), e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));
        }      
      } else if (expr is MapComprehension) {
        var e = (MapComprehension)expr;
        // Translate "map x | R :: T" into
        // See LetExpr for issues with the e.Range
        //reqs.AddRange(generateAutoReqs(e.Range));        
        var auto_reqs = generateAutoReqs(e.Term);
        if (auto_reqs.Count > 0) {
          reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, new List<TypeParameter>(), e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));
        }
      } else if (expr is StmtExpr) {
        var e = (StmtExpr)expr;
        reqs.AddRange(generateAutoReqs(e.E));
      } else if (expr is ITEExpr) {
        ITEExpr e = (ITEExpr)expr;
        reqs.AddRange(generateAutoReqs(e.Test));        
        reqs.Add(Expression.CreateITE(e.Test, andify(e.Thn.tok, generateAutoReqs(e.Thn)), andify(e.Els.tok, generateAutoReqs(e.Els))));
      } else if (expr is ConcreteSyntaxExpression) {
        var e = (ConcreteSyntaxExpression)expr;
        reqs.AddRange(generateAutoReqs(e.ResolvedExpression));
      } else {
        //Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
      }

      return reqs;
    }
  }



  /// <summary>
  /// Replace all occurrences of attribute {:timeLimitMultiplier X} with {:timeLimit Y}
  /// where Y = X*default-time-limit or Y = X*command-line-time-limit
  /// </summary>
  public class TimeLimitRewriter : IRewriter
  {
    public TimeLimitRewriter(ErrorReporter reporter)
      : base(reporter) {
      Contract.Requires(reporter != null);
    }

    internal override void PreResolve(ModuleDefinition m) {
      foreach (var d in m.TopLevelDecls) {
        if (d is ClassDecl) {
          var c = (ClassDecl)d;
          foreach (MemberDecl member in c.Members)  {
            if (member is Function || member is Method) {
              // Check for the timeLimitMultiplier attribute
              if (Attributes.Contains(member.Attributes, "timeLimitMultiplier")) {
                Attributes attrs = member.Attributes;
                foreach (var attr in attrs.AsEnumerable()) {
                  if (attr.Name == "timeLimitMultiplier") {
                    if (attr.Args.Count == 1 && attr.Args[0] is LiteralExpr) {
                      var arg = attr.Args[0] as LiteralExpr;
                      System.Numerics.BigInteger value = (System.Numerics.BigInteger)arg.Value;
                      if (value.Sign > 0) {
                        int current_limit = DafnyOptions.O.ProverKillTime > 0 ? DafnyOptions.O.ProverKillTime : 10;  // Default to 10 seconds
                        attr.Args[0] = new LiteralExpr(attr.Args[0].tok, value * current_limit);
                        attr.Name = "timeLimit";
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }


  class MatchCaseExprSubstituteCloner : Cloner
  {
    private List<CasePattern> patternSubst;
    private BoundVar oldvar;
    private BoundVar var;

    // the cloner is called after resolving the body of matchexpr, trying
    // to replace casepattern in the body that has been replaced by bv
    public MatchCaseExprSubstituteCloner(List<CasePattern> subst, BoundVar var) {
      this.patternSubst = subst;
      this.oldvar = null;
      this.var = var;
    }

    public MatchCaseExprSubstituteCloner(BoundVar oldvar, BoundVar var) {
      this.patternSubst = null;
      this.oldvar = oldvar;
      this.var = var;
    }

    public override BoundVar CloneBoundVar(BoundVar bv) {
      // replace bv with this.var if bv == oldvar
      BoundVar bvNew;
      if (oldvar != null && bv.Name.Equals(oldvar.Name)) {
        bvNew = new BoundVar(new AutoGeneratedToken(bv.tok), var.Name, CloneType(bv.Type));
      } else {
        bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));
      }
      bvNew.IsGhost = bv.IsGhost;
      return bvNew;
    }

    public override NameSegment CloneNameSegment(Expression expr) {
      var e = (NameSegment)expr;
      if (oldvar != null && e.Name.Equals(oldvar.Name)) {
        return new NameSegment(new AutoGeneratedToken(e.tok), var.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
      } else {
        return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
      }
    }

    public override Expression CloneApplySuffix(ApplySuffix e) {
      // if the ApplySuffix matches the CasePattern, then replace it with the BoundVar.
      CasePattern cp = null;
      if (FindMatchingPattern(e, out cp)) {
        if (this.var.tok is MatchCaseToken) {
          Contract.Assert(e.Args.Count == cp.Arguments.Count);
          for (int i = 0; i < e.Args.Count; i++) {
            ((MatchCaseToken)this.var.tok).AddVar(e.Args[i].tok, cp.Arguments[i].Var, false);
          }
        }
        return new NameSegment(new AutoGeneratedToken(e.tok), this.var.Name, null);
      } else {
        return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));
      }
    }

    private bool FindMatchingPattern(ApplySuffix e, out CasePattern pattern) {
      pattern = null;
      if (patternSubst == null) {
        return false;
      }
      Expression lhs = e.Lhs;
      if (!(lhs is NameSegment)) {
        return false;
      }
      string applyName = ((NameSegment)lhs).Name;
      foreach (CasePattern cp in patternSubst) {
        string ctorName = cp.Id;
        if (!(applyName.Equals(ctorName)) || (e.Args.Count != cp.Arguments.Count)) {
          continue;
        }
        bool found = true;
        for (int i = 0; i < e.Args.Count; i++) {
          var arg1 = e.Args[i];
          var arg2 = cp.Arguments[i];
          if (arg1.Resolved is IdentifierExpr) {
            var bv1 = ((IdentifierExpr)arg1.Resolved).Var;
            if (bv1 != arg2.Var) {
              found = false;
            }
          } else {
            found = false;
          }
        }
        if (found) {
          pattern = cp;
          return true;
        }
      }
      return false;
    }
  }

  // MatchCaseToken is used to record BoundVars that are consolidated due to rewrite of
  // nested match patterns. We want to record the original BoundVars that are consolidated
  // so that they will show up in the IDE correctly.
  public class MatchCaseToken : AutoGeneratedToken
  {
    public readonly List<Tuple<IToken, BoundVar, bool>> varList;
    public MatchCaseToken(IToken tok)
      : base(tok) {
      varList = new List<Tuple<IToken, BoundVar, bool>>();
    }

    public void AddVar(IToken tok, BoundVar var, bool isDefinition) {
      varList.Add(new Tuple<IToken, BoundVar, bool>(tok, var, isDefinition));
    }
  }

  // A cloner that replace the original token with AutoGeneratedToken.
  class AutoGeneratedTokenCloner : Cloner
  {
    public override IToken Tok(IToken tok) {
      return new AutoGeneratedToken(tok);
    }
  }

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

  public class InductionRewriter : IRewriter {
    internal InductionRewriter(ErrorReporter reporter) : base(reporter) {
      Contract.Requires(reporter != null);
    }

    internal override void PostCyclicityResolve(ModuleDefinition m) {
      if (DafnyOptions.O.Induction == 0) {
        // Don't bother inferring :induction attributes.  This will also have the effect of not warning about malformed :induction attributes
      } else {
        foreach (var decl in m.TopLevelDecls) {
          if (decl is ClassDecl) {
            var cl = (ClassDecl)decl;
            foreach (var member in cl.Members) {
              if (member is FixpointLemma) {
                var method = (FixpointLemma)member;
                ProcessMethodExpressions(method);
                ComputeLemmaInduction(method.PrefixLemma);
                ProcessMethodExpressions(method.PrefixLemma);
              } else if (member is Method) {
                var method = (Method)member;
                ComputeLemmaInduction(method);
                ProcessMethodExpressions(method);
              } else if (member is FixpointPredicate) {
                var function = (FixpointPredicate)member;
                ProcessFunctionExpressions(function);
                ProcessFunctionExpressions(function.PrefixPredicate);
              } else if (member is Function) {
                var function = (Function)member;
                ProcessFunctionExpressions(function);
              }
            }
          } else if (decl is NewtypeDecl) {
            var nt = (NewtypeDecl)decl;
            if (nt.Constraint != null) {
              var visitor = new Induction_Visitor(this);
              visitor.Visit(nt.Constraint);
            }
          }
        }
      }
    }

    void ProcessMethodExpressions(Method method) {
      Contract.Requires(method != null);
      var visitor = new Induction_Visitor(this);
      method.Req.ForEach(mfe => visitor.Visit(mfe.E));
      method.Ens.ForEach(mfe => visitor.Visit(mfe.E));
      if (method.Body != null) {
        visitor.Visit(method.Body);
      }
    }

    void ProcessFunctionExpressions(Function function) {
      Contract.Requires(function != null);
      var visitor = new Induction_Visitor(this);
      function.Req.ForEach(visitor.Visit);
      function.Ens.ForEach(visitor.Visit);
      if (function.Body != null) {
        visitor.Visit(function.Body);
      }
    }

    void ComputeLemmaInduction(Method method) {
      Contract.Requires(method != null);
      if (method.Body != null && method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 && !(method is FixpointLemma)) {
        var specs = new List<Expression>();
        method.Req.ForEach(mfe => specs.Add(mfe.E));
        method.Ens.ForEach(mfe => specs.Add(mfe.E));
        ComputeInductionVariables(method.tok, method.Ins, specs, method, ref method.Attributes);
      }
    }

    void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs, Method lemma, ref Attributes attributes) where VarType : class, IVariable {
      Contract.Requires(tok != null);
      Contract.Requires(boundVars != null);
      Contract.Requires(searchExprs != null);
      Contract.Requires(DafnyOptions.O.Induction != 0);

      var args = Attributes.FindExpressions(attributes, "induction");  // we only look at the first one we find, since it overrides any other ones
      if (args == null) {
        if (DafnyOptions.O.Induction < 2) {
          // No explicit induction variables and we're asked not to infer anything, so we're done
          return;
        } else if (DafnyOptions.O.Induction == 2 && lemma != null) {
          // We're asked to infer induction variables only for quantifiers, not for lemmas
          return;
        }
        // GO INFER below (only select boundVars)
      } else if (args.Count == 0) {
        // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables
        // GO INFER below (all boundVars)
      } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) {
        // {:induction false} or {:induction true}
        if (!(bool)((LiteralExpr)args[0]).Value) {
          // we're told not to infer anything
          return;
        }
        // GO INFER below (all boundVars)
      } else {
        // Here, we're expecting the arguments to {:induction args} to be a sublist of "boundVars".
        var goodArguments = new List<Expression>();
        var i = 0;
        foreach (var arg in args) {
          var ie = arg.Resolved as IdentifierExpr;
          if (ie != null) {
            var j = boundVars.FindIndex(i, v => v == ie.Var);
            if (i <= j) {
              goodArguments.Add(ie);
              i = j;
              continue;
            }
            if (0 <= boundVars.FindIndex(v => v == ie.Var)) {
              reporter.Warning(MessageSource.Rewriter, arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute",
                lemma != null ? "lemma parameter" : "bound variable", lemma != null ? "lemma" : "quantifier");
              return;
            }
          }
          reporter.Warning(MessageSource.Rewriter, arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute",
            i == 0 ? "'false' or 'true' or " : "",
            lemma != null ? "lemma parameter" : "bound variable");
          return;
        }
        // The argument list was legal, so let's use it for the _induction attribute
        attributes = new Attributes("_induction", goodArguments, attributes);
        return;
      }

      // Okay, here we go, coming up with good induction setting for the given situation
      var inductionVariables = new List<Expression>();
      foreach (IVariable n in boundVars) {
        if (!n.Type.IsTypeParameter && (args != null || searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n)))) {
          inductionVariables.Add(new IdentifierExpr(n));
        }
      }
      if (inductionVariables.Count != 0) {
        // We found something usable, so let's record that in an attribute
        attributes = new Attributes("_induction", inductionVariables, attributes);
        // And since we're inferring something, let's also report that in a hover text.
        var s = Printer.OneAttributeToString(attributes, "induction");
        if (lemma is PrefixLemma) {
          s = lemma.Name + " " + s;
        }
        reporter.Info(MessageSource.Rewriter, tok, s);
      }
    }
    class Induction_Visitor : BottomUpVisitor
    {
      readonly InductionRewriter IndRewriter;
      public Induction_Visitor(InductionRewriter inductionRewriter) {
        Contract.Requires(inductionRewriter != null);
        IndRewriter = inductionRewriter;
      }
      protected override void VisitOneExpr(Expression expr) {
        var q = expr as QuantifierExpr;
        if (q != null && q.SplitQuantifier == null) {
          IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, null, ref q.Attributes);
        }
      }
      void VisitInductionStmt(Statement stmt) {
        Contract.Requires(stmt != null);
        // visit a selection of subexpressions
        if (stmt is AssertStmt) {
          var s = (AssertStmt)stmt;
          Visit(s.Expr);
        }
        // recursively visit all substatements
        foreach (var s in stmt.SubStatements) {
          VisitInductionStmt(s);
        }
      }
    }

    /// <summary>
    /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.
    /// More precisely:
    ///   DafnyInductionHeuristic      Return 'true'
    ///   -----------------------      -------------
    ///        0                       always
    ///        1    if 'n' occurs as   any subexpression (of 'expr')
    ///        2    if 'n' occurs as   any subexpression of          any index argument of an array/sequence select expression or any                       argument to a recursive function
    ///        3    if 'n' occurs as   a prominent subexpression of  any index argument of an array/sequence select expression or any                       argument to a recursive function
    ///        4    if 'n' occurs as   any subexpression of                                                                       any                       argument to a recursive function
    ///        5    if 'n' occurs as   a prominent subexpression of                                                               any                       argument to a recursive function
    ///        6    if 'n' occurs as   a prominent subexpression of                                                               any decreases-influencing argument to a recursive function
    /// Parameter 'n' is allowed to be a ThisSurrogate.
    /// </summary>
    public static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {
      switch (DafnyOptions.O.InductionHeuristic) {
        case 0: return true;
        case 1: return Translator.ContainsFreeVariable(expr, false, n);
        default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);
      }
    }

    /// <summary>
    /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or
    /// not 'expr' has prominent status in its context.
    /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).
    /// Parameter 'n' is allowed to be a ThisSurrogate.
    /// </summary>
    static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) {
      Contract.Requires(expr != null);
      Contract.Requires(n != null);

      // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
      var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

      if (expr is IdentifierExpr) {
        var e = (IdentifierExpr)expr;
        return exprIsProminent && e.Var == n;
      } else if (expr is SeqSelectExpr) {
        var e = (SeqSelectExpr)expr;
        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) ||  // this subexpression does not acquire "prominent" status
          (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) ||  // this one does (unless arrays/sequences are excluded)
          (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q));    // ditto
      } else if (expr is MultiSelectExpr) {
        var e = (MultiSelectExpr)expr;
        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
        return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||
          e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
      } else if (expr is FunctionCallExpr) {
        var e = (FunctionCallExpr)expr;
        // For recursive functions:  arguments are "prominent"
        // For non-recursive function:  arguments are "prominent" if the call is
        var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;
        var decr = e.Function.Decreases.Expressions;
        bool variantArgument;
        if (DafnyOptions.O.InductionHeuristic < 6) {
          variantArgument = rec;
        } else {
          // The receiver is considered to be "variant" if the function is recursive and the receiver participates
          // in the effective decreases clause of the function.  The receiver participates if it's a free variable
          // of a term in the explicit decreases clause.
          variantArgument = rec && decr.Exists(ee => Translator.ContainsFreeVariable(ee, true, null));
        }
        if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) {
          return true;
        }
        Contract.Assert(e.Function.Formals.Count == e.Args.Count);
        for (int i = 0; i < e.Function.Formals.Count; i++) {
          var f = e.Function.Formals[i];
          var exp = e.Args[i];
          if (DafnyOptions.O.InductionHeuristic < 6) {
            variantArgument = rec;
          } else if (rec) {
            // The argument position is considered to be "variant" if the function is recursive and...
            // ... it has something to do with why the callee is well-founded, which happens when...
            if (f is ImplicitFormal) {
              // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or
              variantArgument = true;
            } else if (decr.Exists(ee => Translator.ContainsFreeVariable(ee, false, f))) {
              // ... it participates in the effective decreases clause of the function, which happens when it is
              // a free variable of a term in the explicit decreases clause, or
              variantArgument = true;
            } else {
              // ... the callee is a prefix predicate.
              variantArgument = true;
            }
          }
          if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {
            return true;
          }
        }
        return false;
      } else if (expr is TernaryExpr) {
        var e = (TernaryExpr)expr;
        switch (e.Op) {
          case TernaryExpr.Opcode.PrefixEqOp:
          case TernaryExpr.Opcode.PrefixNeqOp:
            return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) ||
              VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) ||
              VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent);
          default:
            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected ternary expression
        }
      } else if (expr is DatatypeValue) {
        var e = (DatatypeValue)expr;
        var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype
        return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
      } else if (expr is UnaryExpr) {
        var e = (UnaryExpr)expr;
        // both Not and SeqLength preserve prominence
        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);
      } else if (expr is BinaryExpr) {
        var e = (BinaryExpr)expr;
        bool q;
        switch (e.ResolvedOp) {
          case BinaryExpr.ResolvedOpcode.Add:
          case BinaryExpr.ResolvedOpcode.Sub:
          case BinaryExpr.ResolvedOpcode.Mul:
          case BinaryExpr.ResolvedOpcode.Div:
          case BinaryExpr.ResolvedOpcode.Mod:
          case BinaryExpr.ResolvedOpcode.Union:
          case BinaryExpr.ResolvedOpcode.Intersection:
          case BinaryExpr.ResolvedOpcode.SetDifference:
          case BinaryExpr.ResolvedOpcode.Concat:
            // these operators preserve prominence
            q = exprIsProminent;
            break;
          default:
            // whereas all other binary operators do not
            q = subExprIsProminent;
            break;
        }
        return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||
          VarOccursInArgumentToRecursiveFunction(e.E1, n, q);
      } else if (expr is StmtExpr) {
        var e = (StmtExpr)expr;
        // ignore the statement
        return VarOccursInArgumentToRecursiveFunction(e.E, n);

      } else if (expr is ITEExpr) {
        var e = (ITEExpr)expr;
        return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) ||  // test is not "prominent"
          VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) ||  // but the two branches are
          VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent);
      } else if (expr is OldExpr ||
                 expr is ConcreteSyntaxExpression ||
                 expr is BoxingCastExpr ||
                 expr is UnboxingCastExpr) {
        foreach (var exp in expr.SubExpressions) {
          if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) {  // maintain prominence
            return true;
          }
        }
        return false;
      } else {
        // in all other cases, reset the prominence status and recurse on the subexpressions
        foreach (var exp in expr.SubExpressions) {
          if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) {
            return true;
          }
        }
        return false;
      }
    }
  }
}