refactor: move Closure.lean to Meta

We will need to improve the support for let-decls. We will use
the new `trackZeta`.

src/Lean/Elab/Print.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.FoldConsts
 import Lean.Elab.Command
 
 namespace Lean

src/Lean/Elab/Structure.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Closure
 import Lean.Elab.Command
 import Lean.Elab.DeclModifiers
 import Lean.Elab.DeclUtil

src/Lean/Meta.lean

@@ -22,3 +22,4 @@ import Lean.Meta.GeneralizeTelescope
 import Lean.Meta.EqnCompiler
 import Lean.Meta.ReduceEval
 import Lean.Meta.Partial
+import Lean.Meta.Closure

src/Lean/Meta/Basic.lean

@@ -9,7 +9,6 @@ import Lean.Class
 import Lean.ReducibilityAttrs
 import Lean.Util.Trace
 import Lean.Util.RecDepth
-import Lean.Util.Closure
 import Lean.Compiler.InlineAttrs
 import Lean.Meta.Exception
 import Lean.Meta.TransparencyMode
@@ -910,41 +909,6 @@ modifyMCtx fun mctx => mctx.assignLevel mvarId u
 def whnfD [MonadLiftT MetaM n] (e : Expr) : n Expr :=
 withTransparency TransparencyMode.default $ whnf e
 
-private def mkAuxDefinitionImp (name : Name) (type : Expr) (value : Expr) (zeta : Bool) : MetaM Expr := do
-opts  ← getOptions;
-mctx  ← getMCtx;
-lctx  ← getLCtx;
-match Closure.mkValueTypeClosure mctx lctx type value zeta with
-| Except.error ex  => throwError ex
-| Except.ok result  => do
-  env ← getEnv;
-  let decl := Declaration.defnDecl {
-    name     := name,
-    lparams  := result.levelParams.toList,
-    type     := result.type,
-    value    := result.value,
-    hints    := ReducibilityHints.regular (getMaxHeight env result.value + 1),
-    isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value
-  };
-  setMCtx result.mctx;
-  addAndCompile decl;
-  pure $ mkAppN (mkConst name result.levelClosure.toList) result.exprClosure
-
-/--
-  Create an auxiliary definition with the given name, type and value.
-  The parameters `type` and `value` may contain free and meta variables.
-  A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
-  returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
-  and `t_j`s are free and meta variables `type` and `value` depend on. -/
-def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : m Expr := liftMetaM do
-mkAuxDefinitionImp name type value zeta
-
-/-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
-def mkAuxDefinitionFor (name : Name) (value : Expr) : m Expr := liftMetaM do
-type ← inferType value;
-let type := type.headBeta;
-mkAuxDefinition name type value
-
 def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): m Unit := liftMetaM do
 env ← getEnv;
 match Compiler.setInlineAttribute env declName kind with

src/Lean/Meta/Closure.lean

@@ -7,8 +7,11 @@ import Std.ShareCommon
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Util.FoldConsts
+import Lean.Meta.Basic
 
 namespace Lean
+namespace Meta
+
 namespace Closure
 
 structure Context :=
@@ -218,6 +221,45 @@ pure {
   exprClosure  := r.exprClosure,
   mctx         := r.mctx
 }
-
 end Closure
+
+variables {m : Type → Type} [MonadLiftT MetaM m]
+
+private def mkAuxDefinitionImp (name : Name) (type : Expr) (value : Expr) (zeta : Bool) : MetaM Expr := do
+opts  ← getOptions;
+mctx  ← getMCtx;
+lctx  ← getLCtx;
+match Closure.mkValueTypeClosure mctx lctx type value zeta with
+| Except.error ex  => throwError ex
+| Except.ok result  => do
+  env ← getEnv;
+  let decl := Declaration.defnDecl {
+    name     := name,
+    lparams  := result.levelParams.toList,
+    type     := result.type,
+    value    := result.value,
+    hints    := ReducibilityHints.regular (getMaxHeight env result.value + 1),
+    isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value
+  };
+  setMCtx result.mctx;
+  addAndCompile decl;
+  pure $ mkAppN (mkConst name result.levelClosure.toList) result.exprClosure
+
+/--
+  Create an auxiliary definition with the given name, type and value.
+  The parameters `type` and `value` may contain free and meta variables.
+  A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
+  returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
+  and `t_j`s are free and meta variables `type` and `value` depend on. -/
+def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : m Expr := liftMetaM do
+mkAuxDefinitionImp name type value zeta
+
+/-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
+def mkAuxDefinitionFor (name : Name) (value : Expr) : m Expr := liftMetaM do
+type ← inferType value;
+let type := type.headBeta;
+mkAuxDefinition name type value
+
+
+end Meta
 end Lean

src/Lean/Meta/EqnCompiler/Match.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Util.CollectLevelParams
 import Lean.Meta.Check
+import Lean.Meta.Closure
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.GeneralizeTelescope
 import Lean.Meta.EqnCompiler.MVarRenaming

tests/lean/run/meta7.lean

@@ -31,6 +31,9 @@ lambdaTelescope c.value?.get! fun xs body =>
     let ys := ys.toList.map mkFVar;
     print ys;
     check $ pure $ ys.length == 2;
+    mkAuxDefinitionFor `foo body;
     pure ()
 
 #eval tst1
+
+#print foo