fix: hover info for cases h : ... (#3084)

This makes hover info, go to definition, etc work for the `h` in `cases
h : e`. The implementation is similar to that used for the `generalize h
: e = x` tactic.

src/Lean/Elab/Tactic/Induction.lean

@@ -263,7 +263,8 @@ def reorderAlts (alts : Array Alt) (altsSyntax : Array Syntax) : Array Alt := Id
 
 def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altsSyntax : Array Syntax)
     (initialInfo : Info)
-    (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do
+    (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
+    (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
   let hasAlts := altsSyntax.size > 0
   if hasAlts then
     -- default to initial state outside of alts
@@ -301,10 +302,13 @@ where
         let mut (_, altMVarId) ← altMVarId.introN numFields
         match (← Cases.unifyEqs? numEqs altMVarId {}) with
         | none   => pure () -- alternative is not reachable
-        | some (altMVarId', _) =>
+        | some (altMVarId', subst) =>
           (_, altMVarId) ← altMVarId'.introNP numGeneralized
           for fvarId in toClear do
             altMVarId ← altMVarId.tryClear fvarId
+          altMVarId.withContext do
+            for (stx, fvar) in toTag do
+              Term.addLocalVarInfo stx (subst.get fvar)
           let altMVarIds ← applyPreTac altMVarId
           if !hasAlts then
             -- User did not provide alternatives using `|`
@@ -323,7 +327,7 @@ where
           let mut (fvarIds, altMVarId) ← altMVarId.introN numFields (altVars.toList.map getNameOfIdent') (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
           -- Delay adding the infos for the pattern LHS because we want them to nest
           -- inside tacticInfo for the current alternative (in `evalAlt`)
-          let addInfo := do
+          let addInfo : TermElabM Unit := do
             if (← getInfoState).enabled then
               if let some declName := declName? then
                 addConstInfo (getAltNameStx altStx) declName
@@ -336,10 +340,13 @@ where
               throwError "alternative '{altName}' is not needed"
           match (← Cases.unifyEqs? numEqs altMVarId {}) with
           | none => unusedAlt
-          | some (altMVarId', _) =>
+          | some (altMVarId', subst) =>
             (_, altMVarId) ← altMVarId'.introNP numGeneralized
             for fvarId in toClear do
               altMVarId ← altMVarId.tryClear fvarId
+            altMVarId.withContext do
+              for (stx, fvar) in toTag do
+                Term.addLocalVarInfo stx (subst.get fvar)
             let altMVarIds ← applyPreTac altMVarId
             if altMVarIds.isEmpty then
               unusedAlt
@@ -565,16 +572,23 @@ where
       if foundFVars.contains target.fvarId! then
         throwError "target (or one of its indices) occurs more than once{indentExpr target}"
 
-def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
+def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId)) :=
   withMainContext do
-    let args ← targets.mapM fun target => do
-      let hName? := if target[0].isNone then none else some target[0][0].getId
+    let mut hIdents := #[]
+    let mut args := #[]
+    for target in targets do
+      let hName? ← if target[0].isNone then
+        pure none
+      else
+        hIdents := hIdents.push ⟨target[0][0]⟩
+        pure (some target[0][0].getId)
       let expr ← elabTerm target[1] none
-      return { expr, hName? : GeneralizeArg }
+      args := args.push { expr, hName? : GeneralizeArg }
     if (← withMainContext <| args.anyM fun arg => shouldGeneralizeTarget arg.expr <||> pure arg.hName?.isSome) then
       liftMetaTacticAux fun mvarId => do
         let argsToGeneralize ← args.filterM fun arg => shouldGeneralizeTarget arg.expr <||> pure arg.hName?.isSome
         let (fvarIdsNew, mvarId) ← mvarId.generalize argsToGeneralize
+        -- note: fvarIdsNew contains the `x` variables from `args` followed by all the `h` variables
         let mut result := #[]
         let mut j := 0
         for arg in args do
@@ -583,16 +597,18 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
             j := j+1
           else
             result := result.push arg.expr
-        return (result, [mvarId])
+        -- note: `fvarIdsNew[j:]` contains all the `h` variables
+        assert! hIdents.size + j == fvarIdsNew.size
+        return ((result, hIdents.zip fvarIdsNew[j:]), [mvarId])
     else
-      return args.map (·.expr)
+      return (args.map (·.expr), #[])
 
 @[builtin_tactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx =>
   match expandCases? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
     -- leading_parser nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
-    let targets ← elabCasesTargets stx[1].getSepArgs
+    let (targets, toTag) ← elabCasesTargets stx[1].getSepArgs
     let optInductionAlts := stx[3]
     let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
     let alts :=  getAltsOfOptInductionAlts optInductionAlts
@@ -613,7 +629,8 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
       mvarId.withContext do
         ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew
         mvarId.assign result.elimApp
-        ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numEqs := targets.size) (toClear := targetsNew)
+        ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo
+          (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
 
 builtin_initialize
   registerTraceClass `Elab.cases

tests/lean/interactive/hover.lean

@@ -276,6 +276,13 @@ example : 1 = 1 := by
            --^ textDocument/hover
   exact Eq.refl x
 
+example : 1 = 1 := by
+  cases _e : 1 with
+      --^ textDocument/hover
+  | zero => rfl
+  | succ x => rfl
+       --^ textDocument/hover
+
 namespace Foo
 
 export List (nil)

tests/lean/interactive/hover.lean.expected.out

@@ -584,46 +584,58 @@
   "end": {"line": 274, "character": 15}},
  "contents": {"value": "```lean\n_e : 1 = x\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
- "position": {"line": 280, "character": 13}}
+ "position": {"line": 279, "character": 8}}
 {"range":
- {"start": {"line": 280, "character": 13},
-  "end": {"line": 280, "character": 16}},
+ {"start": {"line": 279, "character": 8},
+  "end": {"line": 279, "character": 10}},
+ "contents": {"value": "```lean\n_e : 1 = Nat.zero\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 282, "character": 9}}
+{"range":
+ {"start": {"line": 282, "character": 9},
+  "end": {"line": 282, "character": 10}},
+ "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 287, "character": 13}}
+{"range":
+ {"start": {"line": 287, "character": 13},
+  "end": {"line": 287, "character": 16}},
  "contents":
  {"value":
   "```lean\nList.nil.{u} {α : Type u} : List α\n```\n***\n`[]` is the empty list. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
- "position": {"line": 282, "character": 13}}
+ "position": {"line": 289, "character": 13}}
 {"range":
- {"start": {"line": 282, "character": 11},
-  "end": {"line": 282, "character": 15}},
+ {"start": {"line": 289, "character": 11},
+  "end": {"line": 289, "character": 15}},
  "contents":
  {"value":
   "```lean\nList.cons.{u} {α : Type u} (head : α) (tail : List α) : List α\n```\n***\nIf `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the\nlist whose first element is `a` and with `l` as the rest of the list. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
- "position": {"line": 284, "character": 18}}
+ "position": {"line": 291, "character": 18}}
 {"range":
- {"start": {"line": 284, "character": 17},
-  "end": {"line": 284, "character": 20}},
+ {"start": {"line": 291, "character": 17},
+  "end": {"line": 291, "character": 20}},
  "contents":
  {"value":
   "```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
- "position": {"line": 287, "character": 26}}
+ "position": {"line": 294, "character": 26}}
 {"range":
- {"start": {"line": 287, "character": 25},
-  "end": {"line": 287, "character": 29}},
+ {"start": {"line": 294, "character": 25},
+  "end": {"line": 294, "character": 29}},
  "contents":
  {"value":
   "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
- "position": {"line": 287, "character": 19}}
+ "position": {"line": 294, "character": 19}}
 {"range":
- {"start": {"line": 287, "character": 19},
-  "end": {"line": 287, "character": 22}},
+ {"start": {"line": 294, "character": 19},
+  "end": {"line": 294, "character": 22}},
  "contents":
  {"value":
   "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",