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

namespace Microsoft.Dafny
{
  [ContractClass(typeof(IRewriterContracts))]
  public interface IRewriter
  {
    void PreResolve(ModuleDefinition m);
    void PostResolve(ModuleDefinition m);
    // After SCC/Cyclicity/Recursivity analysis:
    void PostCyclicityResolve(ModuleDefinition m);
  }
  [ContractClassFor(typeof(IRewriter))]
  abstract class IRewriterContracts : IRewriter
  {
    public void PreResolve(ModuleDefinition m) {
      Contract.Requires(m != null);
    }
    public void PostResolve(ModuleDefinition m) {
      Contract.Requires(m != null);
    }
    public void PostCyclicityResolve(ModuleDefinition m) {
      Contract.Requires(m != null);
    }
  }

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

  /// <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 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(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, 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.
        }
      }
    }

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

    public void PostCyclicityResolve(ModuleDefinition m) { 
    }

    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, new List<Expression>() { self });
            e.Type = new SetType(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, new List<Expression>() { F });
        e.Type = new SetType(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, 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 {
    readonly ResolutionErrorReporter reporter;
    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(ResolutionErrorReporter reporter)
      : base() {
      this.reporter = reporter;
      fullVersion = new Dictionary<Function, Function>();
      original = new Dictionary<Function, Function>();
      revealOriginal = new Dictionary<Lemma, Function>();
    }

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

    public 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]);
          }
        }
      }
    }

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

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

            List<BoundVar> boundVars = new List<BoundVar>();
            foreach (Formal formal in f.Formals) {
              boundVars.Add(new BoundVar(f.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);

            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;
    Resolver resolver;
    OpaqueFunctionRewriter opaqueInfo;
    bool containsMatch; // TODO: Track this per-requirement, rather than per-function

    public AutoReqFunctionRewriter(Resolver r, OpaqueFunctionRewriter o) {
      this.resolver = r;
      this.opaqueInfo = o;
    }

    public void PreResolve(ModuleDefinition m) { 
    }    

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

    public void PostCyclicityResolve(ModuleDefinition m) { 
    }

    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("")) {
        resolver.ReportAdditionalInformation(f.tok, tip, f.tok.val.Length);
        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("")) {
        resolver.ReportAdditionalInformation(method.tok, tip, method.tok.val.Length);
        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 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);
            resolver.ReportAdditionalInformation(e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&", e.tok.val.Length);
        }
      } 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 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;
                for (; attrs != null; attrs = attrs.Prev) {
                  if (attrs.Name == "timeLimitMultiplier") {
                    if (attrs.Args.Count == 1 && attrs.Args[0] is LiteralExpr) {
                      var arg = attrs.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
                        attrs.Args[0] = new LiteralExpr(attrs.Args[0].tok, value * current_limit);
                        attrs.Name = "timeLimit";
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }

    public void PostResolve(ModuleDefinition m)
    {
      // Nothing to do here
    }

    public void PostCyclicityResolve(ModuleDefinition m) {
      // Nothing to do here
    }

  }
}