From 5786f5873802ac96eb8b60451b4a7685bfe22733 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 31 May 2021 16:10:55 +0200 Subject: [PATCH] feat: plain term goal request --- src/Lean/Data/Lsp/Extra.lean | 8 +++ src/Lean/Server/FileSource.lean | 3 + src/Lean/Server/FileWorker.lean | 19 ++++++ src/Lean/Server/InfoUtils.lean | 32 ++++++++++ src/Lean/Server/Watchdog.lean | 1 + tests/lean/interactive/plainTermGoal.lean | 33 ++++++++++ .../plainTermGoal.lean.expected.out | 60 +++++++++++++++++++ 7 files changed, 156 insertions(+) create mode 100644 tests/lean/interactive/plainTermGoal.lean create mode 100644 tests/lean/interactive/plainTermGoal.lean.expected.out diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean index bb995a506b..2237e2c71d 100644 --- a/src/Lean/Data/Lsp/Extra.lean +++ b/src/Lean/Data/Lsp/Extra.lean @@ -57,4 +57,12 @@ structure PlainGoal where goals : Array String deriving FromJson, ToJson +structure PlainTermGoalParams extends TextDocumentPositionParams + deriving FromJson, ToJson + +structure PlainTermGoal where + goal : String + range : Range + deriving FromJson, ToJson + end Lean.Lsp diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean index 755f49127c..19018f5306 100644 --- a/src/Lean/Server/FileSource.lean +++ b/src/Lean/Server/FileSource.lean @@ -73,5 +73,8 @@ instance SemanticTokensRangeParams.hasFileSource : FileSource SemanticTokensRang instance PlainGoalParams.hasFileSource : FileSource PlainGoalParams := ⟨fun p => fileSource p.textDocument⟩ +instance : FileSource PlainTermGoalParams where + fileSource p := fileSource p.textDocument + end Lsp end Lean diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 2dc8d239fb..8ed904250d 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -467,6 +467,24 @@ section RequestHandling ⟨text.utf8PosToLspPos <| stx.getPos?.get!, text.utf8PosToLspPos <| stx.getTailPos?.get!⟩ + open Elab in + partial def handlePlainTermGoal (p : PlainTermGoalParams) + : ServerM (Task (Except IO.Error (Except RequestError (Option PlainTermGoal)))) := do + let st ← read + let doc ← st.docRef.get + let text := doc.meta.text + let hoverPos := text.lspPosToUtf8Pos p.position + withWaitFindSnap doc (fun s => s.endPos > hoverPos) + (notFoundX := pure none) fun snap => do + for t in snap.cmdState.infoState.trees do + if let some (ci, Info.ofTermInfo i) := t.termGoalAt? hoverPos then + let goal ← ci.runMetaM i.lctx <| open Meta in do + let ty ← instantiateMVars <|<- inferType i.expr + withPPInaccessibleNames <| Meta.ppGoal (← mkFreshExprMVar ty).mvarId! + let range := if hasRange i.stx then rangeOfSyntax! text i.stx else ⟨p.position, p.position⟩ + return some { goal := toString goal, range } + return none + partial def handleDocumentHighlight (p : DocumentHighlightParams) : ServerM (Task (Except IO.Error (Except RequestError (Array DocumentHighlight)))) := do let doc ← (← read).docRef.get @@ -703,6 +721,7 @@ section MessageHandling | "textDocument/semanticTokens/full" => handle SemanticTokensParams SemanticTokens handleSemanticTokensFull | "textDocument/semanticTokens/range" => handle SemanticTokensRangeParams SemanticTokens handleSemanticTokensRange | "$/lean/plainGoal" => handle PlainGoalParams (Option PlainGoal) handlePlainGoal + | "$/lean/plainTermGoal" => handle PlainTermGoalParams (Option PlainTermGoal) handlePlainTermGoal | _ => throwServerError s!"Got unsupported request: {method}" end MessageHandling diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 65253271bb..632b74fb05 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -189,4 +189,36 @@ 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 ctx i headFns => do + if let some pos := getHeadFnPos? i.stx then + headFns.insert pos + else + headFns + t.smallestInfo? fun i => do + if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then + if pos ≤ hoverPos ∧ hoverPos < tailPos then + if let Info.ofTermInfo ti := i then + return !ti.stx.isIdent || !headFns.contains pos + 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 + end Lean.Elab diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 0a08374485..ce86933b28 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -404,6 +404,7 @@ section MessageHandling | "textDocument/semanticTokens/range" => handle SemanticTokensRangeParams | "textDocument/semanticTokens/full" => handle SemanticTokensParams | "$/lean/plainGoal" => handle PlainGoalParams + | "$/lean/plainTermGoal" => handle PlainTermGoalParams | _ => (←read).hOut.writeLspResponseError { id := id diff --git a/tests/lean/interactive/plainTermGoal.lean b/tests/lean/interactive/plainTermGoal.lean new file mode 100644 index 0000000000..c8e92d2924 --- /dev/null +++ b/tests/lean/interactive/plainTermGoal.lean @@ -0,0 +1,33 @@ + +example : 0 < 2 := + Nat.ltTrans Nat.zeroLtOne (Nat.ltSuccSelf _) + --^ $/lean/plainTermGoal + --^ $/lean/plainTermGoal + --^ $/lean/plainTermGoal + --^ $/lean/plainTermGoal + --^ $/lean/plainTermGoal + +example : OptionM Unit := do + let y : Int ← none + let x ← Nat.zero + --^ $/lean/plainTermGoal + return () + +example (m n : Nat) : m < n := + Nat.ltTrans _ _ + --^ $/lean/plainTermGoal + +example : True := sorry + --^ $/lean/plainTermGoal + +example : ∀ n, n < n + 42 := + fun n => Nat.ltOfLeOfLt (Nat.leAddRight n 41) (Nat.ltSuccSelf _) +--^ $/lean/plainTermGoal + --^ $/lean/plainTermGoal + +example : ∀ n, n < 1 + n := by + intro n + rw [Nat.add_comm] + --^ $/lean/plainTermGoal + exact Nat.ltSuccSelf _ + --^ $/lean/plainTermGoal diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out new file mode 100644 index 0000000000..fd31106641 --- /dev/null +++ b/tests/lean/interactive/plainTermGoal.lean.expected.out @@ -0,0 +1,60 @@ +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 2, "character": 13}} +{"range": + {"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 46}}, + "goal": "⊢ 0 < 2"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 2, "character": 14}} +{"range": + {"start": {"line": 2, "character": 14}, "end": {"line": 2, "character": 27}}, + "goal": "⊢ 0 < 1"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 2, "character": 15}} +{"range": + {"start": {"line": 2, "character": 14}, "end": {"line": 2, "character": 27}}, + "goal": "⊢ 0 < 1"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 2, "character": 29}} +{"range": + {"start": {"line": 2, "character": 28}, "end": {"line": 2, "character": 46}}, + "goal": "⊢ 1 < Nat.succ 1"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 2, "character": 44}} +{"range": + {"start": {"line": 2, "character": 44}, "end": {"line": 2, "character": 45}}, + "goal": "⊢ Nat"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 11, "character": 10}} +{"range": + {"start": {"line": 11, "character": 10}, "end": {"line": 11, "character": 18}}, + "goal": "y : Int\n⊢ Nat"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 16, "character": 16}} +{"range": + {"start": {"line": 16, "character": 16}, "end": {"line": 16, "character": 17}}, + "goal": "m n : Nat\n⊢ ?m m n < n"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 19, "character": 18}} +{"range": + {"start": {"line": 19, "character": 18}, "end": {"line": 19, "character": 23}}, + "goal": "⊢ True"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 23, "character": 2}} +{"range": + {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 66}}, + "goal": "⊢ ∀ (n : Nat), n < n + 42"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 23, "character": 6}} +{"range": + {"start": {"line": 23, "character": 6}, "end": {"line": 23, "character": 7}}, + "goal": "⊢ Type"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 29, "character": 6}} +{"range": + {"start": {"line": 29, "character": 6}, "end": {"line": 29, "character": 18}}, + "goal": "n : Nat\n⊢ ∀ (n m : Nat), n + m = m + n"} +{"textDocument": {"uri": "file://plainTermGoal.lean"}, + "position": {"line": 31, "character": 8}} +{"range": + {"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 24}}, + "goal": "n : Nat\n⊢ n < Nat.succ n"}