From c29da66c5a27356504dc1e764b3da759faa8cd73 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 22 Mar 2022 05:10:51 -0700 Subject: [PATCH] fix: annotate binders in `intro` for hover / go to def --- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/Tactic/BuiltinTactic.lean | 27 +++++++----- tests/lean/interactive/hover.lean | 14 ++++++ .../lean/interactive/hover.lean.expected.out | 44 +++++++++++++++++++ 4 files changed, 76 insertions(+), 11 deletions(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index b3325ca855..4dd205d8b1 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -136,7 +136,7 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit := registerCustomErrorIfMVar type ref "failed to infer binder type" -private def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do +def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do addTermInfo (isBinder := true) stx fvar private def ensureAtomicBinderName (binderView : BinderView) : TermElabM Unit := diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index e80ec4712e..fe9775cfba 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -146,17 +146,20 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do match stx with - | `(tactic| intro) => introStep `_ - | `(tactic| intro $h:ident) => introStep h.getId - | `(tactic| intro _) => introStep `_ + | `(tactic| intro) => introStep none `_ + | `(tactic| intro $h:ident) => introStep h h.getId + | `(tactic| intro _%$tk) => introStep tk `_ | `(tactic| intro $pat:term) => evalTactic (← `(tactic| intro h; match h with | $pat:term => ?_; try clear h)) | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*)) | _ => throwUnsupportedSyntax where - introStep (n : Name) : TacticM Unit := - liftMetaTactic fun mvarId => do - let (_, mvarId) ← Meta.intro mvarId n - pure [mvarId] + introStep (ref : Option Syntax) (n : Name) : TacticM Unit := do + let fvar ← liftMetaTacticAux fun mvarId => do + let (fvar, mvarId) ← Meta.intro mvarId n + pure (fvar, [mvarId]) + if let some stx := ref then + withMainContext do + Term.addLocalVarInfo stx (mkFVar fvar) @[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do let matchAlts := stx[1] @@ -168,9 +171,13 @@ where | `(tactic| intros) => liftMetaTactic fun mvarId => do let (_, mvarId) ← Meta.intros mvarId return [mvarId] - | `(tactic| intros $ids*) => liftMetaTactic fun mvarId => do - let (_, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList - return [mvarId] + | `(tactic| intros $ids*) => do + let fvars ← liftMetaTacticAux fun mvarId => do + let (fvars, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList + return (fvars, [mvarId]) + withMainContext do + for stx in ids, fvar in fvars do + Term.addLocalVarInfo stx (mkFVar fvar) | _ => throwUnsupportedSyntax @[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx => diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index f20073889f..1a44249f99 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -141,3 +141,17 @@ example : Type 0 := Nat def foo.bar : Nat := 1 --^ textDocument/hover --^ textDocument/hover + +example : Nat → Nat → Nat := + fun x y => + --^ textDocument/hover + --v textDocument/definition + x + --^ textDocument/hover + +example : Nat → Nat → Nat := by + intro x y + --^ textDocument/hover + --v textDocument/definition + exact x + --^ textDocument/hover diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 06e34dd5d2..a690ba0e70 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -179,3 +179,47 @@ null {"start": {"line": 140, "character": 4}, "end": {"line": 140, "character": 11}}, "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 145, "character": 6}} +{"range": + {"start": {"line": 145, "character": 6}, "end": {"line": 145, "character": 7}}, + "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 148, "character": 4}} +[{"targetUri": "file://hover.lean", + "targetSelectionRange": + {"start": {"line": 145, "character": 6}, + "end": {"line": 145, "character": 7}}, + "targetRange": + {"start": {"line": 145, "character": 6}, + "end": {"line": 145, "character": 7}}, + "originSelectionRange": + {"start": {"line": 148, "character": 4}, + "end": {"line": 148, "character": 5}}}] +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 148, "character": 4}} +{"range": + {"start": {"line": 148, "character": 4}, "end": {"line": 148, "character": 5}}, + "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 152, "character": 8}} +{"range": + {"start": {"line": 152, "character": 8}, "end": {"line": 152, "character": 9}}, + "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 155, "character": 8}} +[{"targetUri": "file://hover.lean", + "targetSelectionRange": + {"start": {"line": 152, "character": 8}, + "end": {"line": 152, "character": 9}}, + "targetRange": + {"start": {"line": 152, "character": 8}, + "end": {"line": 152, "character": 9}}, + "originSelectionRange": + {"start": {"line": 155, "character": 8}, + "end": {"line": 155, "character": 9}}}] +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 155, "character": 8}} +{"range": + {"start": {"line": 155, "character": 8}, "end": {"line": 155, "character": 9}}, + "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}