feat: plain term goal request

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

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

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
 

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

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

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

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"}