feat: add declName? to TermElabM context

src/Init/Lean/Elab/Command.lean

@@ -196,12 +196,13 @@ fun stx => withMacroExpansion stx.val $ do
   stx ← exp stx.val;
   elabCommand stx
 
-private def mkTermContext (ctx : Context) (s : State) : Term.Context :=
+private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context :=
 let scope := s.scopes.head!;
 { config         := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
   fileName       := ctx.fileName,
   fileMap        := ctx.fileMap,
   cmdPos         := ctx.cmdPos,
+  declName?      := declName?,
   macroStack     := ctx.macroStack,
   currMacroScope := ctx.currMacroScope,
   currNamespace  := scope.currNamespace,
@@ -225,10 +226,10 @@ match result with
 instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
 ⟨throw $ arbitrary _⟩
 
-@[inline] def runTermElabM {α} (elab : Array Expr → TermElabM α) : CommandElabM α := do
+@[inline] def runTermElabM {α} (declName? : Option Name) (elab : Array Expr → TermElabM α) : CommandElabM α := do
 ctx ← read;
 s ← get;
-match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s)).run (mkTermState s) with
+match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s declName?)).run (mkTermState s) with
 | EStateM.Result.ok a newS                            => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
 | EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
 | EStateM.Result.error Term.Exception.postpone newS   => unreachable!
@@ -475,7 +476,7 @@ fun n => do
   -- `variable` bracktedBinder
   let binder := n.getArg 1;
   -- Try to elaborate `binder` for sanity checking
-  runTermElabM $ fun _ => Term.elabBinder binder $ fun _ => pure ();
+  runTermElabM none $ fun _ => Term.elabBinder binder $ fun _ => pure ();
   modifyScope $ fun scope => { varDecls := scope.varDecls.push binder, .. scope }
 
 @[builtinCommandElab «variables»] def elabVariables : CommandElab :=
@@ -483,13 +484,13 @@ fun n => do
   -- `variables` bracktedBinder+
   let binders := (n.getArg 1).getArgs;
   -- Try to elaborate `binders` for sanity checking
-  runTermElabM $ fun _ => Term.elabBinders binders $ fun _ => pure ();
+  runTermElabM none $ fun _ => Term.elabBinders binders $ fun _ => pure ();
   modifyScope $ fun scope => { varDecls := scope.varDecls ++ binders, .. scope }
 
 @[builtinCommandElab «check»] def elabCheck : CommandElab :=
 fun stx => do
   let term := stx.getArg 1;
-  runTermElabM $ fun _ => do
+  runTermElabM none $ fun _ => do
     e    ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
     type ← Term.inferType stx.val e;

src/Init/Lean/Elab/Declaration.lean

@@ -94,7 +94,7 @@ withDeclId declId $ fun name => do
   declName          ← mkDeclName modifiers name;
   applyAttributes stx declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
   explictLevelNames ← getLevelNames;
-  decl ← runTermElabM $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
+  decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
     type ← Term.elabType typeStx;
     Term.synthesizeSyntheticMVars false;
     type ← Term.instantiateMVars typeStx type;

src/Init/Lean/Elab/Definition.lean

@@ -127,7 +127,7 @@ withDeclId view.declId $ fun name => do
   declName          ← mkDeclName view.modifiers name;
   applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
   explictLevelNames ← getLevelNames;
-  decl? ← runTermElabM $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
+  decl? ← runTermElabM declName $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
     match view.type? with
     | some typeStx => do
       type ← Term.elabType typeStx;

src/Init/Lean/Elab/Term.lean

@@ -22,6 +22,7 @@ structure Context extends Meta.Context :=
 (fileMap         : FileMap)
 (cmdPos          : String.Pos)
 (currNamespace   : Name)
+(declName?       : Option Name     := none)
 (levelNames      : List Name       := [])
 (openDecls       : List OpenDecl   := [])
 (macroStack      : List Syntax     := [])
@@ -217,6 +218,7 @@ instance LVal.hasToString : HasToString LVal :=
 
 def getEnv : TermElabM Environment := do s ← get; pure s.env
 def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
+def getDeclName? : TermElabM (Option Name) := do ctx ← read; pure ctx.declName?
 def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace
 def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls
 def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx