From 1f137297562deabc114feef05f0f3e09eeb83b3a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 23 Jun 2022 13:54:08 +0200 Subject: [PATCH] feat: show term goal at end of term as well --- src/Lean/Server/InfoUtils.lean | 37 +++---------------- tests/lean/interactive/plainTermGoal.lean | 1 + .../plainTermGoal.lean.expected.out | 29 +++++++++------ 3 files changed, 24 insertions(+), 43 deletions(-) diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index f055e01b7b..0252bf9956 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -141,9 +141,11 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI infos.toArray.getMax? (fun a b => a.1 > b.1) |>.map fun (_, ci, i) => (ci, i) /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/ -partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) : Option (ContextInfo × Info) := Id.run do +partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) : Option (ContextInfo × Info) := Id.run do let results := t.visitM (m := Id) (postNode := fun ctx i _ results => do - let results := results.bind (·.getD []) + let mut results := results.bind (·.getD []) + if omitAppFns && i.stx.isOfKind ``Parser.Term.app && i.stx[0].isIdent then + results := results.filter (·.2.2.stx != i.stx[0]) if results.isEmpty && (i matches Info.ofFieldInfo _ || i.toElabInfo?.isSome) && i.contains hoverPos includeStop then let r := i.range?.get! let priority := @@ -299,36 +301,9 @@ where cs.any (hasNestedTactic pos tailPos) | _ => false -/-- -Find info nodes that should be used for the term goal feature. - -The main complication concerns applications -like `f a b` where `f` is an identifier. -In this case, the term goal at `f` -should be the goal for the full application `f a b`. - -Therefore we first gather the position of -these head function symbols such as `f`, -and later ignore identifiers at these positions. --/ partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) := - let headFns : Std.HashSet String.Pos := t.foldInfo (init := {}) fun _ i headFns => - if let some pos := getHeadFnPos? i.stx then - headFns.insert pos - else - headFns - t.smallestInfo? fun i => Id.run do - if i.contains hoverPos then - if let Info.ofTermInfo ti := i then - return !ti.stx.isIdent || !headFns.contains i.pos?.get! - false - where - /- Returns the position of the head function symbol, if it is an identifier. -/ - getHeadFnPos? (s : Syntax) (foundArgs := false) : Option String.Pos := - match s with - | `(($s)) => getHeadFnPos? s foundArgs - | `($f $as*) => getHeadFnPos? f (foundArgs := foundArgs || !as.isEmpty) - | stx => if foundArgs && stx.isIdent then stx.getPos? else none + -- In the case `f a b`, where `f` is an identifier, the term goal at `f` should be the goal for the full application `f a b`. + hoverableInfoAt? t hoverPos (includeStop := true) (omitAppFns := true) partial def InfoTree.hasSorry : InfoTree → IO Bool := go none diff --git a/tests/lean/interactive/plainTermGoal.lean b/tests/lean/interactive/plainTermGoal.lean index 40934a1857..0c2082187b 100644 --- a/tests/lean/interactive/plainTermGoal.lean +++ b/tests/lean/interactive/plainTermGoal.lean @@ -16,6 +16,7 @@ example : Option Unit := do example (m n : Nat) : m < n := Nat.lt_trans _ _ --^ $/lean/plainTermGoal + --^ $/lean/plainTermGoal example : True := sorry --^ $/lean/plainTermGoal diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out index 2850ddf973..f4855befc2 100644 --- a/tests/lean/interactive/plainTermGoal.lean.expected.out +++ b/tests/lean/interactive/plainTermGoal.lean.expected.out @@ -34,32 +34,37 @@ {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}}, "goal": "m n : Nat\n⊢ ?m m n < n"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, - "position": {"line": 19, "character": 18}} + "position": {"line": 16, "character": 18}} {"range": - {"start": {"line": 19, "character": 18}, "end": {"line": 19, "character": 23}}, + {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}}, + "goal": "m n : Nat\n⊢ ?m m n < n"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 20, "character": 18}} +{"range": + {"start": {"line": 20, "character": 18}, "end": {"line": 20, "character": 23}}, "goal": "⊢ True"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, - "position": {"line": 23, "character": 2}} + "position": {"line": 24, "character": 2}} {"range": - {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 74}}, + {"start": {"line": 24, "character": 2}, "end": {"line": 24, "character": 74}}, "goal": "⊢ ∀ (n : Nat), n < n + 42"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, - "position": {"line": 23, "character": 6}} + "position": {"line": 24, "character": 6}} {"range": - {"start": {"line": 23, "character": 6}, "end": {"line": 23, "character": 7}}, + {"start": {"line": 24, "character": 6}, "end": {"line": 24, "character": 7}}, "goal": "⊢ Nat"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, - "position": {"line": 29, "character": 6}} + "position": {"line": 30, "character": 6}} {"range": - {"start": {"line": 29, "character": 6}, "end": {"line": 29, "character": 18}}, + {"start": {"line": 30, "character": 6}, "end": {"line": 30, "character": 18}}, "goal": "n : Nat\n⊢ ∀ (n m : Nat), n + m = m + n"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, - "position": {"line": 31, "character": 8}} + "position": {"line": 32, "character": 8}} {"range": - {"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 26}}, + {"start": {"line": 32, "character": 8}, "end": {"line": 32, "character": 26}}, "goal": "n : Nat\n⊢ n < n + 1"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, - "position": {"line": 34, "character": 14}} + "position": {"line": 35, "character": 14}} {"range": - {"start": {"line": 34, "character": 14}, "end": {"line": 34, "character": 15}}, + {"start": {"line": 35, "character": 14}, "end": {"line": 35, "character": 15}}, "goal": "n : Nat\n⊢ Nat"}