feat: preserve nonDep flag at LocalDecl.ldecl

src/Lean/LocalContext.lean

@@ -11,65 +11,65 @@ namespace Lean
 
 inductive LocalDecl
 | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo)
-| ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr)
+| ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool)
 
 @[export lean_mk_local_decl]
 def mkLocalDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : LocalDecl :=
 LocalDecl.cdecl index fvarId userName type bi
 @[export lean_mk_let_decl]
 def mkLetDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : LocalDecl :=
-LocalDecl.ldecl index fvarId userName type val
+LocalDecl.ldecl index fvarId userName type val false
 @[export lean_local_decl_binder_info]
 def LocalDecl.binderInfoEx : LocalDecl → BinderInfo
 | LocalDecl.cdecl _ _ _ _ bi => bi
 | _                          => BinderInfo.default
 
 namespace LocalDecl
-instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _)⟩
+instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) false⟩
 
 def isLet : LocalDecl → Bool
-| cdecl _ _ _ _ _ => false
-| ldecl _ _ _ _ _ => true
+| cdecl _ _ _ _ _   => false
+| ldecl _ _ _ _ _ _ => true
 
 def index : LocalDecl → Nat
-| cdecl idx _ _ _ _ => idx
-| ldecl idx _ _ _ _ => idx
+| cdecl idx _ _ _ _   => idx
+| ldecl idx _ _ _ _ _ => idx
 
 def setIndex : LocalDecl → Nat → LocalDecl
-| cdecl _  id n t bi, idx => cdecl idx id n t bi
-| ldecl _  id n t v,  idx => ldecl idx id n t v
+| cdecl _  id n t bi,   idx => cdecl idx id n t bi
+| ldecl _  id n t v nd, idx => ldecl idx id n t v nd
 
 def fvarId : LocalDecl → FVarId
-| cdecl _ id _ _ _ => id
-| ldecl _ id _ _ _ => id
+| cdecl _ id _ _ _   => id
+| ldecl _ id _ _ _ _ => id
 
 def userName : LocalDecl → Name
-| cdecl _ _ n _ _ => n
-| ldecl _ _ n _ _ => n
+| cdecl _ _ n _ _   => n
+| ldecl _ _ n _ _ _ => n
 
 def type : LocalDecl → Expr
-| cdecl _ _ _ t _ => t
-| ldecl _ _ _ t _ => t
+| cdecl _ _ _ t _   => t
+| ldecl _ _ _ t _ _ => t
 
 def binderInfo : LocalDecl → BinderInfo
-| cdecl _ _ _ _ bi => bi
-| ldecl _ _ _ _ _  => BinderInfo.default
+| cdecl _ _ _ _ bi  => bi
+| ldecl _ _ _ _ _ _ => BinderInfo.default
 
 def value? : LocalDecl → Option Expr
-| cdecl _ _ _ _ _ => none
-| ldecl _ _ _ _ v => some v
+| cdecl _ _ _ _ _   => none
+| ldecl _ _ _ _ v _ => some v
 
 def value : LocalDecl → Expr
-| cdecl _ _ _ _ _ => panic! "let declaration expected"
-| ldecl _ _ _ _ v => v
+| cdecl _ _ _ _ _   => panic! "let declaration expected"
+| ldecl _ _ _ _ v _ => v
 
 def updateUserName : LocalDecl → Name → LocalDecl
-| cdecl index id _ type bi,  userName => cdecl index id userName type bi
-| ldecl index id _ type val, userName => ldecl index id userName type val
+| cdecl index id _ type bi,     userName => cdecl index id userName type bi
+| ldecl index id _ type val nd, userName => ldecl index id userName type val nd
 
 def updateBinderInfo : LocalDecl → BinderInfo → LocalDecl
 | cdecl index id n type _,  bi => cdecl index id n type bi
-| ldecl _ _ _ _ _, _           => panic! "unexpected let declaration"
+| ldecl _ _ _ _ _ _, _         => panic! "unexpected let declaration"
 
 def toExpr (decl : LocalDecl) : Expr :=
 mkFVar decl.fvarId
@@ -106,11 +106,11 @@ match lctx with
   { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
 @[export lean_local_ctx_mk_let_decl]
-def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) : LocalContext :=
+def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep := false) : LocalContext :=
 match lctx with
 | { fvarIdToDecl := map, decls := decls } =>
   let idx  := decls.size;
-  let decl := LocalDecl.ldecl idx fvarId userName type value;
+  let decl := LocalDecl.ldecl idx fvarId userName type value nonDep;
   { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
 /- Low level API -/
@@ -310,11 +310,11 @@ xs.size.foldRev (fun i b =>
       Lean.mkLambda n bi ty b
     else
       Lean.mkForall n bi ty b
-  | some (LocalDecl.ldecl _ _ n ty val) =>
+  | some (LocalDecl.ldecl _ _ n ty val nonDep) =>
     if b.hasLooseBVar 0 then
       let ty  := ty.abstractRange i xs;
       let val := val.abstractRange i xs;
-      mkLet n ty val b
+      mkLet n ty val b nonDep
     else
       b.lowerLooseBVars 1 1
   | none => panic! "unknown free variable") b

src/Lean/Meta/Basic.lean

@@ -358,10 +358,10 @@ match localDecl with
   | LocalDecl.cdecl idx id n type bi  => do
     type ← instantiateMVars type;
     pure $ LocalDecl.cdecl idx id n type bi
-  | LocalDecl.ldecl idx id n type val => do
+  | LocalDecl.ldecl idx id n type val nonDep => do
     type ← instantiateMVars type;
     val ← instantiateMVars val;
-    pure $ LocalDecl.ldecl idx id n type val
+    pure $ LocalDecl.ldecl idx id n type val nonDep
 
 @[inline] private def liftMkBindingM {α} (x : MetavarContext.MkBindingM α) : MetaM α := do
 mctx ← getMCtx;

src/Lean/Meta/Check.lean

@@ -19,7 +19,7 @@ _ ← getLevel e; pure ()
 def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
 lctx ← getLCtx;
 match lctx.find? fvarId with
-| some (LocalDecl.ldecl _ n t v b) => do
+| some (LocalDecl.ldecl _ n t v b _) => do
   vType ← inferType v;
   throwError $
      "invalid let declaration, term" ++ indentExpr v
@@ -37,7 +37,7 @@ lambdaTelescope e $ fun xs b => do
     | LocalDecl.cdecl _ _ _ t _ => do
       ensureType t;
       check t
-    | LocalDecl.ldecl _ _ _ t v => do
+    | LocalDecl.ldecl _ _ _ t v _ => do
       ensureType t;
       check t;
       vType ← inferType v;

src/Lean/Meta/EqnCompiler/Match.lean

@@ -18,8 +18,8 @@ namespace Match
 def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
 if d.fvarId == fvarId then d
 else match d with
-  | LocalDecl.cdecl idx id n type bi  => LocalDecl.cdecl idx id n (type.replaceFVarId fvarId e) bi
-  | LocalDecl.ldecl idx id n type val => LocalDecl.ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e)
+  | LocalDecl.cdecl idx id n type bi => LocalDecl.cdecl idx id n (type.replaceFVarId fvarId e) bi
+  | LocalDecl.ldecl idx id n type val nonDep => LocalDecl.ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e) nonDep
 
 inductive Pattern : Type
 | inaccessible (e : Expr) : Pattern

src/Lean/Meta/ExprDefEq.lean

@@ -400,7 +400,7 @@ if ctx.mvarDecl.lctx.containsFVar fvar then pure fvar
 else do
   let lctx := ctxMeta.lctx;
   match lctx.findFVar? fvar with
-  | some (LocalDecl.ldecl _ _ _ _ v) => visit check v
+  | some (LocalDecl.ldecl _ _ _ _ v _) => visit check v
   | _ =>
     if ctx.fvars.contains fvar then pure fvar
     else do
@@ -527,7 +527,7 @@ partial def check
 | e@(Expr.fvar fvarId _)   =>
   if mvarDecl.lctx.contains fvarId then true
   else match lctx.find? fvarId with
-    | some (LocalDecl.ldecl _ _ _ _ v) => false -- need expensive CheckAssignment.check
+    | some (LocalDecl.ldecl _ _ _ _ v _) => false -- need expensive CheckAssignment.check
     | _ =>
       if fvars.any $ fun x => x.fvarId! == fvarId then true
       else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it

src/Lean/Meta/GeneralizeTelescope.lean

@@ -43,8 +43,8 @@ partial def generalizeTelescopeAux {α} (prefixForNewVars : Name) (k : Array Exp
     | ⟨e@(Expr.fvar fvarId _), type, false⟩ => do
       localDecl ← getLocalDecl fvarId;
       match localDecl with
-      | LocalDecl.cdecl _ _ _ _ _ => generalizeTelescopeAux entries (i+1) nextVarIdx (fvars.push e)
-      | LocalDecl.ldecl _ _ _ _ _ => replace e type
+      | LocalDecl.cdecl _ _ _ _ _   => generalizeTelescopeAux entries (i+1) nextVarIdx (fvars.push e)
+      | LocalDecl.ldecl _ _ _ _ _ _ => replace e type
     | ⟨e, type, modified⟩ => do
       when modified $ unlessM (isTypeCorrect type) $
         throwError $ "failed to create telescope generalizing " ++ (entries.map Entry.expr);

src/Lean/Meta/Tactic/FVarSubst.lean

@@ -67,8 +67,8 @@ end FVarSubst
 end Meta
 
 def LocalDecl.applyFVarSubst (s : Meta.FVarSubst) : LocalDecl → LocalDecl
-| LocalDecl.cdecl i id n t bi => LocalDecl.cdecl i id n (s.apply t) bi
-| LocalDecl.ldecl i id n t v  => LocalDecl.ldecl i id n (s.apply t) (s.apply v)
+| LocalDecl.cdecl i id n t bi   => LocalDecl.cdecl i id n (s.apply t) bi
+| LocalDecl.ldecl i id n t v nd => LocalDecl.ldecl i id n (s.apply t) (s.apply v) nd
 
 abbrev Expr.applyFVarSubst (s : Meta.FVarSubst) (e : Expr) : Expr :=
 s.apply e

src/Lean/MetavarContext.lean

@@ -573,13 +573,13 @@ lctx.foldl
   (fun (result : LocalContext × MetavarContext) ldecl =>
      let (lctx, mctx) := result;
      match ldecl with
-     | LocalDecl.cdecl _ fvarId userName type bi    =>
+     | LocalDecl.cdecl _ fvarId userName type bi =>
        let (type, mctx) := mctx.instantiateMVars type;
        (lctx.mkLocalDecl fvarId userName type bi, mctx)
-     | LocalDecl.ldecl _ fvarId userName type value =>
+     | LocalDecl.ldecl _ fvarId userName type value nonDep =>
        let (type, mctx)  := mctx.instantiateMVars type;
        let (value, mctx) := mctx.instantiateMVars value;
-       (lctx.mkLetDecl fvarId userName type value, mctx))
+       (lctx.mkLetDecl fvarId userName type value nonDep, mctx))
   ({}, mctx)
 
 def instantiateMVarDeclMVars (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext :=
@@ -641,8 +641,8 @@ end DependsOn
   depends on a free variable `x` s.t. `p x` is `true`. -/
 @[inline] def findLocalDeclDependsOn (mctx : MetavarContext) (localDecl : LocalDecl) (p : FVarId → Bool) : Bool :=
 match localDecl with
-| LocalDecl.cdecl _ _ _ type _     => findExprDependsOn mctx type p
-| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
+| LocalDecl.cdecl _ _ _ type _       => findExprDependsOn mctx type p
+| LocalDecl.ldecl _ _ _ type value _ => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
 
 def exprDependsOn (mctx : MetavarContext) (e : Expr) (fvarId : FVarId) : Bool :=
 findExprDependsOn mctx e $ fun fvarId' => fvarId == fvarId'
@@ -776,11 +776,11 @@ xs.size.foldRevM
       let type := type.headBeta;
       type ← abstractRangeAux elimMVarDeps xs i type;
       pure $ Lean.mkForall n bi type e
-    | LocalDecl.ldecl _ _ n type value => do
+    | LocalDecl.ldecl _ _ n type value nonDep => do
       let type := type.headBeta;
       type  ← abstractRangeAux elimMVarDeps xs i type;
       value ← abstractRangeAux elimMVarDeps xs i value;
-      let e := mkLet n type value e;
+      let e := mkLet n type value e nonDep;
       match kind with
       | MetavarKind.syntheticOpaque =>
         -- See "Gruesome details" section in the beginning of the file
@@ -921,11 +921,11 @@ xs.size.foldRevM
           pure (Lean.mkForall n bi type e, num + 1)
       else
         pure (e.lowerLooseBVars 1 1, num)
-    | LocalDecl.ldecl _ _ n type value => do
+    | LocalDecl.ldecl _ _ n type value nonDep => do
       if e.hasLooseBVar 0 then do
         type  ← abstractRange xs i type;
         value ← abstractRange xs i value;
-        pure (mkLet n type value e, num + 1)
+        pure (mkLet n type value e nonDep, num + 1)
       else
         pure (e.lowerLooseBVars 1 1, num))
   (e, 0)

src/Lean/Util/Closure.lean

@@ -92,9 +92,9 @@ fvarId   ← mkFreshFVarId;
 modify $ fun s => { s with lctxOutput := s.lctxOutput.mkLocalDecl fvarId userName type bi };
 pure $ mkFVar fvarId
 
-def mkLetDecl (userName : Name) (type : Expr) (value : Expr) : ClosureM Expr := do
+def mkLetDecl (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) : ClosureM Expr := do
 fvarId   ← mkFreshFVarId;
-modify $ fun s => { s with lctxOutput := s.lctxOutput.mkLetDecl fvarId userName type value };
+modify $ fun s => { s with lctxOutput := s.lctxOutput.mkLetDecl fvarId userName type value nonDep };
 pure $ mkFVar fvarId
 
 @[inline] def visitExpr (f : Expr → ClosureM Expr) (e : Expr) : ClosureM Expr :=
@@ -140,7 +140,7 @@ partial def collectExprAux : Expr → ClosureM Expr
       x    ← mkLocalDecl userName type bi;
       modify $ fun s => { s with exprClosure := s.exprClosure.push e };
       pure x
-    | some (LocalDecl.ldecl _ _ userName type value) =>
+    | some (LocalDecl.ldecl _ _ userName type value nonDep) =>
       if ctx.zeta then do
         value ← instantiateMVars value;
         collect value
@@ -150,7 +150,7 @@ partial def collectExprAux : Expr → ClosureM Expr
         value ← instantiateMVars value;
         value ← collect value;
         -- Note that let-declarations do not need to be provided to the closure being constructed.
-        mkLetDecl userName type value
+        mkLetDecl userName type value nonDep
   | e => pure e
 
 def collectExpr (e : Expr) : ClosureM Expr := do

src/Lean/Util/PPGoal.lean

@@ -36,7 +36,7 @@ match mctx.findDecl? mvarId with
          else
            let fmt := pushPending varNames prevType? fmt;
            ([varName], some type, fmt)
-       | LocalDecl.ldecl _ _ varName type val =>
+       | LocalDecl.ldecl _ _ varName type val _ =>
          let fmt  := pushPending varNames prevType? fmt;
          let fmt  := addLine fmt;
          let type := instMVars type;