From d1a15dea03f935457c6b3cbe99af029652a2584f Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 21 Dec 2023 14:39:23 -0800 Subject: [PATCH] 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 | 41 ++++++++++++------ tests/lean/interactive/hover.lean | 7 ++++ .../lean/interactive/hover.lean.expected.out | 42 ++++++++++++------- 3 files changed, 63 insertions(+), 27 deletions(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index a3d8ee1fd0af..85e0489a7bed 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/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 diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index 2c06a3c5b5dd..0bef6295f1f5 100644 --- a/tests/lean/interactive/hover.lean +++ b/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) diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 11bd07180dcd..6dccf2ecf55f 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/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*",