From 2e020c1f29b6938a6ca414ce47c66a003e6c3909 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 4 Jan 2024 10:31:55 -0800
Subject: [PATCH]  feat: hover info for `rcases h : ...` (#486)

* feat: hover info for `rcases h : ...`

* fix
---
 Std/Tactic/RCases.lean | 27 +++++++++++++++++----------
 lean-toolchain         |  2 +-
 test/rcases.lean       |  5 +++++
 3 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/Std/Tactic/RCases.lean b/Std/Tactic/RCases.lean
index 37157ad50c..904a39154b 100644
--- a/Std/Tactic/RCases.lean
+++ b/Std/Tactic/RCases.lean
@@ -487,10 +487,15 @@ The terminating continuation used in `rcasesCore` and `rcasesContinue`. We speci
 `α` to `Array MVarId` to collect the list of goals, and given the list of `clears`, it attempts to
 clear them from the goal and adds the goal to the list.
 -/
-def finish (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
+def finish (toTag : Array (Ident × FVarId) := #[])
+  (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
   (gs : Array MVarId) : TermElabM (Array MVarId) := do
   let cs : Array Expr := (clears.map fs.get).filter Expr.isFVar
-  gs.push <$> tryClearMany' g (cs.map Expr.fvarId!)
+  let g ← tryClearMany' g (cs.map Expr.fvarId!)
+  g.withContext do
+    for (stx, fvar) in toTag do
+      Term.addLocalVarInfo stx (fs.get fvar)
+  return gs.push g
 
 open Elab
 
@@ -511,7 +516,7 @@ partial def RCasesPatt.parse (stx : Syntax) : MetaM RCasesPatt :=
 -- extracted from elabCasesTargets
 /-- Generalize all the arguments as specified in `args` to fvars if they aren't already -/
 def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
-    MetaM (Array Expr × MVarId) := do
+    MetaM (Array Expr × Array FVarId × MVarId) := do
   let argsToGeneralize := args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
   let (fvarIdsNew, goal) ← goal.generalize argsToGeneralize
   let mut result := #[]
@@ -522,14 +527,14 @@ def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
     else
       result := result.push (mkFVar fvarIdsNew[j]!)
       j := j+1
-  pure (result, goal)
+  pure (result, fvarIdsNew[j:], goal)
 
 /--
 Given a list of targets of the form `e` or `h : e`, and a pattern, match all the targets
 against the pattern. Returns the list of produced subgoals.
 -/
-def rcases (tgts : Array (Option Name × Syntax))
-    (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
+def rcases (tgts : Array (Option Ident × Syntax))
+  (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
   let pats ← match tgts.size with
   | 0 => return [g]
   | 1 => pure [pat]
@@ -541,9 +546,11 @@ def rcases (tgts : Array (Option Name × Syntax))
       pure (.typed ref pat (← Term.exprToSyntax ty), some ty)
     | _ => pure (pat, none)
     let expr ← Term.ensureHasType ty (← Term.elabTerm tgt ty)
-    pure (pat, { expr, xName? := pat.name?, hName? : GeneralizeArg })
-  let (vs, g) ← generalizeExceptFVar g args
-  (·.toList) <$> rcasesContinue g {} #[] #[] (pats.zip vs).toList finish
+    pure (pat, { expr, xName? := pat.name?, hName? := hName?.map (·.getId) : GeneralizeArg })
+  let (vs, hs, g) ← generalizeExceptFVar g args
+  let toTag := tgts.filterMap (·.1) |>.zip hs
+  let gs ← rcasesContinue g {} #[] #[] (pats.zip vs).toList (finish (toTag := toTag))
+  pure gs.toList
 
 /--
 The `obtain` tactic in the no-target case. Given a type `T`, create a goal `|- T` and
@@ -688,7 +695,7 @@ elab (name := rcases) tk:"rcases" tgts:casesTarget,* pat:((" with " rcasesPatLo)
   | #[] => pure $ RCasesPatt.tuple tk []
   | _ => throwUnsupportedSyntax
   let tgts := tgts.getElems.map fun tgt =>
-    (if tgt.raw[0].isNone then none else some tgt.raw[0][0].getId, tgt.raw[1])
+    (if tgt.raw[0].isNone then none else some ⟨tgt.raw[0][0]⟩, tgt.raw[1])
   let g ← getMainGoal
   g.withContext do replaceMainGoal (← RCases.rcases tgts pat g)
 
diff --git a/lean-toolchain b/lean-toolchain
index 3f21e50bd4..400a8aac3f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:nightly-2023-12-24
diff --git a/test/rcases.lean b/test/rcases.lean
index 14e33afe30..f1c4039205 100644
--- a/test/rcases.lean
+++ b/test/rcases.lean
@@ -188,6 +188,11 @@ example (h : a ≤ 2 ∨ 2 < a) : True := by
   · guard_hyp ha1 : a ≤ 2; trivial
   · guard_hyp ha2 : 3 ≤ a; trivial
 
+example (a : Nat) : True := by
+  rcases h : a with _ | n
+  · guard_hyp h : a = 0; trivial
+  · guard_hyp h : a = n + 1; trivial
+
 inductive BaseType : Type where
   | one