refactor: add options for controlling whether variables are included or not at mkLambdaFVars and mkForallFVars

src/Lean/Elab/Declaration.lean

@@ -67,7 +67,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
     Term.synthesizeSyntheticMVarsNoPostponing
     let type ← instantiateMVars type
     let type ← mkForallFVars xs type
-    let (type, _) ← mkForallUsedOnly vars type
+    let type ← mkForallFVars vars type (usedOnly := true)
     let (type, _) ← Term.levelMVarToParam type
     let usedParams  := collectLevelParams {} type |>.params
     match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with

src/Lean/Meta/Basic.lean

@@ -376,11 +376,11 @@ def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl := do
     setNGen newS.ngen;
     throwError "failed to create binder due to failure when reverting variable dependencies"
 
-def mkForallFVars (xs : Array Expr) (e : Expr) : MetaM Expr :=
-  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkForall xs e
+def mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) : MetaM Expr :=
+  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkForall xs e usedOnly usedLetOnly
 
-def mkLambdaFVars (xs : Array Expr) (e : Expr) : MetaM Expr :=
-  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkLambda xs e
+def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) : MetaM Expr :=
+  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly
 
 def mkLetFVars (xs : Array Expr) (e : Expr) : MetaM Expr :=
   mkLambdaFVars xs e
@@ -389,9 +389,6 @@ def mkArrow (d b : Expr) : MetaM Expr := do
   let n ← mkFreshUserName `x
   return Lean.mkForall n BinderInfo.default d b
 
-def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MetaM (Expr × Nat) := do
-  if xs.isEmpty then pure (e, 0) else liftMkBindingM <| MetavarContext.mkForallUsedOnly xs e
-
 def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : MetaM Expr :=
   if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.elimMVarDeps xs e preserveOrder
 

src/Lean/MetavarContext.lean

@@ -954,8 +954,9 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
 
 /--
   Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
-  If `usedOnly == false` then `forall` and `lambda` are created only for used variables. -/
-@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) : M (Expr × Nat) := do
+  If `usedOnly == false` then `forall` and `lambda` expressions are created only for used variables.
+  If `usedLetOnly == false` then `let` expressions are created only for used (let-) variables. -/
+@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) : M (Expr × Nat) := do
   let e ← abstractRange xs xs.size e
   xs.size.foldRevM
     (fun i (p : Expr × Nat) => do
@@ -973,7 +974,7 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
         else
           pure (e.lowerLooseBVars 1 1, num)
       | LocalDecl.ldecl _ _ n type value nonDep =>
-        if e.hasLooseBVar 0 then
+        if !usedLetOnly || e.hasLooseBVar 0 then
           let type  ← abstractRange xs i type
           let value ← abstractRange xs i value
           pure (mkLet n type value e nonDep, num + 1)
@@ -991,20 +992,17 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBinding
 def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun _ =>
   MkBinding.revert xs mvarId preserveOrder
 
-def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) : MkBindingM (Expr × Nat) := fun lctx =>
-  MkBinding.mkBinding isLambda lctx xs e usedOnly false
+def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) : MkBindingM (Expr × Nat) := fun lctx =>
+  MkBinding.mkBinding isLambda lctx xs e usedOnly usedLetOnly false
 
-@[inline] def mkLambda (xs : Array Expr) (e : Expr) : MkBindingM Expr := do
-  let (e, _) ← mkBinding true xs e
+@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) : MkBindingM Expr := do
+  let (e, _) ← mkBinding (isLambda := true) xs e usedOnly usedLetOnly
   pure e
 
-@[inline] def mkForall (xs : Array Expr) (e : Expr) : MkBindingM Expr := do
-  let (e, _) ← mkBinding false xs e
+@[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) : MkBindingM Expr := do
+  let (e, _) ← mkBinding (isLambda := false) xs e usedOnly usedLetOnly
   pure e
 
-@[inline] def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MkBindingM (Expr × Nat) := do
-  mkBinding false xs e true
-
 /--
   `isWellFormed mctx lctx e` return true if
   - All locals in `e` are declared in `lctx`

tests/lean/docStr.lean.expected.out

@@ -208,11 +208,11 @@ namedPattern :=
       endPos := { line := 159, column := 29 },
       endCharUtf16 := 29 } }
 Lean.Meta.forallTelescopeReducing :=
-  { range := { pos := { line := 673, column := 0 },
+  { range := { pos := { line := 670, column := 0 },
       charUtf16 := 0,
-      endPos := { line := 674, column := 58 },
+      endPos := { line := 671, column := 58 },
       endCharUtf16 := 58 },
-    selectionRange := { pos := { line := 673, column := 4 },
+    selectionRange := { pos := { line := 670, column := 4 },
       charUtf16 := 4,
-      endPos := { line := 673, column := 27 },
+      endPos := { line := 670, column := 27 },
       endCharUtf16 := 27 } }

tests/lean/mvar3.lean

@@ -4,7 +4,7 @@ open Lean
 
 def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
     : Except MetavarContext.MkBinding.Exception (MetavarContext × NameGenerator × Expr) :=
-match MetavarContext.mkLambda xs e lctx { mctx := mctx, ngen := ngen } with
+match MetavarContext.mkLambda xs e false true lctx { mctx := mctx, ngen := ngen } with
 | EStateM.Result.ok e s    => Except.ok (s.mctx, s.ngen, e)
 | EStateM.Result.error e s => Except.error e
 

tests/lean/run/meta2.lean

@@ -185,7 +185,7 @@ do print "----- tst11 -----";
      checkM $ not <$> (mkLambdaFVars #[x] x >>= isType);
      checkM $ not <$> (mkLambdaFVars #[x] nat >>= isType);
      let t ← mkEq x (mkNatLit 0);
-     let (t, _) ← mkForallUsedOnly #[x] t;
+     let t ← mkForallFVars #[x] t (usedOnly := true);
      print t;
      checkM $ isType t;
      pure ();
@@ -356,32 +356,6 @@ do print "----- tst23 -----";
 
 #eval tst23
 
-def tst25 : MetaM Unit :=
-do print "----- tst25 -----";
-   withLocalDeclD `α type $ fun α =>
-   withLocalDeclD `β type $ fun β =>
-   withLocalDeclD `σ type $ fun σ => do {
-     let (t1, n) ← mkForallUsedOnly #[α, β, σ] $ ← mkArrow α β;
-     print t1;
-     checkM $ pure $ n == 2;
-     let (t2, n) ← mkForallUsedOnly #[α, β, σ] $ ← mkArrow α (← mkArrow β σ);
-     checkM $ pure $ n == 3;
-     print t2;
-     let (t3, n) ← mkForallUsedOnly #[α, β, σ] $ α;
-     checkM $ pure $ n == 1;
-     print t3;
-     let (t4, n) ← mkForallUsedOnly #[α, β, σ] $ σ;
-     checkM $ pure $ n == 1;
-     print t4;
-     let (t5, n) ← mkForallUsedOnly #[α, β, σ] $ nat;
-     checkM $ pure $ n == 0;
-     print t5;
-     pure ()
-   };
-   pure ()
-
-#eval tst25
-
 def tst26 : MetaM Unit := do
 print "----- tst26 -----";
 let m1 ← mkFreshExprMVar (← mkArrow nat nat);