feat: add context and term data to goals

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -222,7 +222,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
         let goal ← ci.runMetaM lctx' do
           Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
         let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
-        return some { goal with range }
+        return some { goal with range, term := ⟨ti⟩ }
       else
         return none
 
@@ -230,7 +230,7 @@ def handlePlainTermGoal (p : PlainTermGoalParams)
     : RequestM (RequestTask (Option PlainTermGoal)) := do
   let t ← getInteractiveTermGoal p
   return t.map <| Except.map <| Option.map fun goal =>
-    { goal := toString goal.toInteractiveGoal.pretty
+    { goal := toString goal.pretty
       range := goal.range
     }
 

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -46,25 +46,25 @@ The intended usage of this is for the infoview to pass the `InfoWithCtx` which
 was stored for a particular `SubexprInfo` tag in a `TaggedText` generated with `ppExprTagged`.
  -/
 def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
-    | ⟨i⟩ => RequestM.asTask do
-      i.ctx.runMetaM i.info.lctx do
-        let type? ← match (← i.info.type?) with
-          | some type => some <$> ppExprTagged type
-          | none => pure none
-        let exprExplicit? ← match i.info with
-          | Elab.Info.ofTermInfo ti =>
-            let ti ← ppExprTagged ti.expr (explicit := true)
-            -- remove top-level expression highlight
-            pure <| some <| match ti with
-              | .tag _ tt => tt
-              | tt => tt
-          | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
-          | _ => pure none
-        return {
-          type := type?
-          exprExplicit := exprExplicit?
-          doc := ← i.info.docString? : InfoPopup
-        }
+  | ⟨i⟩ => RequestM.asTask do
+    i.ctx.runMetaM i.info.lctx do
+      let type? ← match (← i.info.type?) with
+        | some type => some <$> ppExprTagged type
+        | none => pure none
+      let exprExplicit? ← match i.info with
+        | Elab.Info.ofTermInfo ti =>
+          let ti ← ppExprTagged ti.expr (explicit := true)
+          -- remove top-level expression highlight
+          pure <| some <| match ti with
+            | .tag _ tt => tt
+            | tt => tt
+        | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
+        | _ => pure none
+      return {
+        type := type?
+        exprExplicit := exprExplicit?
+        doc := ← i.info.docString? : InfoPopup
+      }
 
 builtin_initialize
   registerBuiltinRpcProcedure

src/Lean/Widget/Basic.lean

@@ -14,13 +14,17 @@ This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInte
 The purpose of `InfoWithCtx` is to carry over information about delaborated
 `Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
 functionality is purpose-specific to showing the contents of infoview popups.
--/
+
+NOTE: This type is for internal use in the infoview. It should not be used in user widgets. -/
 structure InfoWithCtx where
   ctx  : Elab.ContextInfo
   info : Elab.Info
   deriving TypeName
 
 deriving instance TypeName for MessageData
+deriving instance TypeName for LocalContext
+deriving instance TypeName for Elab.ContextInfo
+deriving instance TypeName for Elab.TermInfo
 
 instance : ToJson FVarId := ⟨fun f => toJson f.name⟩
 instance : ToJson MVarId := ⟨fun f => toJson f.name⟩

src/Lean/Widget/Diff.lean

@@ -238,8 +238,7 @@ def diffInteractiveGoal (useAfter : Bool) (g₀ : MVarId) (i₁ : InteractiveGoa
   let lctx₀ := md₀.lctx |>.sanitizeNames.run' {options := (← getOptions)}
   let hs₁ ← diffHypotheses useAfter lctx₀ i₁.hyps
   let i₁ := {i₁ with hyps := hs₁}
-  let some g₁ := i₁.mvarId?
-    | throwError "Expected InteractiveGoal to have an mvarId"
+  let g₁ := i₁.mvarId
   let t₀ ← instantiateMVars <|← inferType (Expr.mvar g₀)
   let some md₁ := (← getMCtx).findDecl? g₁
     | throwError "Unknown goal {g₁}"
@@ -265,8 +264,7 @@ def diffInteractiveGoals (useAfter : Bool) (info : Elab.TacticInfo) (igs₁ : In
        | some xs => xs.contains after
        | none => false
     let goals ← igs₁.goals.mapM (fun ig₁ => do
-      let some g₁ := ig₁.mvarId?
-        | throwError "error: goal not found"
+      let g₁ := ig₁.mvarId
       withGoalCtx (g₁ : MVarId) (fun _lctx₁ _md₁ => do
         -- if the goal is present on the previous version then continue
         if goals₀.any (fun g₀ => g₀ == g₁) then

src/Lean/Widget/InteractiveCode.lean

@@ -29,12 +29,13 @@ inductive DiffTag where
 structure SubexprInfo where
   /-- The `Elab.Info` node with the semantics of this part of the output. -/
   info : WithRpcRef InfoWithCtx
-  /-- The position of this subexpression within the top-level expression.
-  See `Lean.SubExpr`. -/
+  /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/
   subexprPos : Lean.SubExpr.Pos
   -- TODO(WN): add fields for semantic highlighting
   -- kind : Lsp.SymbolKind
-  /-- Ask the renderer to highlight this node in the given color. -/
+  /-- In certain situations such as when goal states change between positions in a tactic-mode proof,
+  we can show subexpression-level diffs between two expressions. This field asks the renderer to
+  display the subexpression as in a diff view (e.g. red/green like `git diff`). -/
   diffStatus? : Option DiffTag := none
   deriving RpcEncodable
 
@@ -53,7 +54,7 @@ def CodeWithInfos.pretty (tt : CodeWithInfos) :=
   tt.stripTags
 
 def SubexprInfo.withDiffTag (tag : DiffTag) (c : SubexprInfo) : SubexprInfo :=
-  {c with diffStatus? := some tag }
+  { c with diffStatus? := some tag }
 
 /-- Tags pretty-printed code with infos from the delaborator. -/
 partial def tagCodeInfos (ctx : Elab.ContextInfo) (infos : SubExpr.PosMap Elab.Info) (tt : TaggedText (Nat × Nat))

src/Lean/Widget/InteractiveGoal.lean

@@ -8,16 +8,16 @@ import Lean.Meta.PPGoal
 import Lean.Widget.InteractiveCode
 import Lean.Data.Lsp.Extra
 
-/-! RPC procedures for retrieving tactic and term goals with embedded `CodeWithInfos`. -/
+/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
 
 namespace Lean.Widget
 open Server
 
-/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered as `h₁ h₂ : α`.
-We call this a 'hypothesis bundle'. -/
+/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
+as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
+booleans to save space in the json encoding. -/
 structure InteractiveHypothesisBundle where
-  /-- The user-friendly name for each hypothesis.
-  If anonymous then the name is inaccessible and hidden. -/
+  /-- The user-friendly name for each hypothesis. -/
   names : Array Name
   /-- The ids for each variable. Should have the same length as `names`. -/
   fvarIds : Array FVarId
@@ -25,42 +25,53 @@ structure InteractiveHypothesisBundle where
   /-- The value, in the case the hypothesis is a `let`-binder. -/
   val? : Option CodeWithInfos := none
   /-- The hypothesis is a typeclass instance. -/
-  isInstance : Bool
+  isInstance? : Option Bool := none
   /-- The hypothesis is a type. -/
-  isType : Bool
+  isType? : Option Bool := none
   /-- If true, the hypothesis was not present on the previous tactic state.
-      Uses `none` instead of `some false` to save space in the json encoding. -/
+  Only present in tactic-mode goals. -/
   isInserted? : Option Bool := none
   /-- If true, the hypothesis will be removed in the next tactic state.
-      Uses `none` instead of `some false` to save space in the json encoding.  -/
-  isRemoved?  : Option Bool := none
-  deriving Inhabited, RpcEncodable
-
-structure InteractiveGoal where
-  hyps      : Array InteractiveHypothesisBundle
-  type      : CodeWithInfos
-  userName? : Option String
-  goalPrefix : String
-  /-- Identifies the goal (ie with the unique
-  name of the MVar that it is a goal for.)
-  This is none when we are showing a term goal. -/
-  mvarId? : Option MVarId := none
-  /-- If true, the goal was not present on the previous tactic state.
-      Uses `none` instead of `some false` to save space in the json encoding.  -/
-  isInserted?: Option Bool := none
-  /-- If true, the goal will be removed on the next tactic state.
-      Uses `none` instead of `some false` to save space in the json encoding. -/
+  Only present in tactic-mode goals. -/
   isRemoved? : Option Bool := none
   deriving Inhabited, RpcEncodable
 
-namespace InteractiveGoal
+/-- The shared parts of interactive term-mode and tactic-mode goals. -/
+structure InteractiveGoalCore where
+  hyps : Array InteractiveHypothesisBundle
+  /-- The target type. -/
+  type : CodeWithInfos
+  /-- Metavariable context that the goal is well-typed in. -/
+  ctx : WithRpcRef Elab.ContextInfo
+  deriving Inhabited
 
-private def addLine (fmt : Format) : Format :=
-  if fmt.isNil then fmt else fmt ++ Format.line
+/-- An interactive tactic-mode goal. -/
+structure InteractiveGoal extends InteractiveGoalCore where
+  /-- The name `foo` in `case foo`, if any. -/
+  userName? : Option String
+  /-- The symbol to display before the target type. Usually `⊢` but `conv` goals use `∣`
+  and it could be extended. -/
+  goalPrefix : String
+  /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/
+  mvarId : MVarId
+  /-- If true, the goal was not present on the previous tactic state. -/
+  isInserted? : Option Bool := none
+  /-- If true, the goal will be removed on the next tactic state. -/
+  isRemoved? : Option Bool := none
+  deriving Inhabited, RpcEncodable
 
-def pretty (g : InteractiveGoal) : Format := Id.run do
+/-- An interactive term-mode goal. -/
+structure InteractiveTermGoal extends InteractiveGoalCore where
+  /-- Syntactic range of the term. -/
+  range : Lsp.Range
+  /-- Information about the term whose type is the term-mode goal. -/
+  term : WithRpcRef Elab.TermInfo
+  deriving Inhabited, RpcEncodable
+
+def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
+    (goalPrefix : String) : Format := Id.run do
   let indent := 2 -- Use option
-  let mut ret := match g.userName? with
+  let mut ret := match userName? with
     | some userName => f!"case {userName}"
     | none          => Format.nil
   for hyp in g.hyps do
@@ -80,23 +91,16 @@ def pretty (g : InteractiveGoal) : Format := Id.run do
       | none =>
         ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
   ret := addLine ret
-  ret ++ f!"{g.goalPrefix}{Format.nest indent g.type.stripTags}"
+  ret ++ f!"{goalPrefix}{Format.nest indent g.type.stripTags}"
+where
+  addLine (fmt : Format) : Format :=
+    if fmt.isNil then fmt else fmt ++ Format.line
+  
+def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
+  g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
 
-end InteractiveGoal
-
-/-- This is everything needed to render an interactive term goal in the infoview. -/
-structure InteractiveTermGoal where
-  hyps      : Array InteractiveHypothesisBundle
-  type      : CodeWithInfos
-  range     : Lsp.Range
-  deriving Inhabited, RpcEncodable
-
-namespace InteractiveTermGoal
-
-def toInteractiveGoal (g : InteractiveTermGoal) : InteractiveGoal :=
-  { g with userName? := none, goalPrefix := "⊢ " }
-
-end InteractiveTermGoal
+def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
+  g.toInteractiveGoalCore.pretty none ""
 
 structure InteractiveGoals where
   goals : Array InteractiveGoal
@@ -109,18 +113,21 @@ instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
 instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
 
 open Meta in
-def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle) (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) : MetaM (Array InteractiveHypothesisBundle) := do
+/-- Extend an array of hypothesis bundles with another bundle. -/
+def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
+    (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) :
+    MetaM (Array InteractiveHypothesisBundle) := do
   if ids.size == 0 then
     throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
   let fvarIds := ids.map Prod.snd
   let names := ids.map Prod.fst
   return hyps.push {
-    names      := names
-    fvarIds    := fvarIds
-    type       := (← ppExprTagged type)
-    val?       := (← value?.mapM ppExprTagged)
-    isInstance := (← isClass? type).isSome
-    isType     := (← instantiateMVars type).isSort
+    names
+    fvarIds
+    type        := (← ppExprTagged type)
+    val?        := (← value?.mapM ppExprTagged)
+    isInstance? := if (← isClass? type).isSome then true else none
+    isType?     := if (← instantiateMVars type).isSort then true else none
   }
 
 open Meta in
@@ -132,7 +139,6 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
   let lctx := mvarDecl.lctx |>.sanitizeNames.run' {options := (← getOptions)}
   withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
 
-
 open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
@@ -180,11 +186,12 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
       | Name.anonymous => none
       | name           => some <| toString name.eraseMacroScopes
     return {
-      hyps,
-      type := goalFmt,
-      userName?,
-      goalPrefix := getGoalPrefix mvarDecl,
-      mvarId? := some mvarId
+      hyps
+      type := goalFmt
+      ctx := ⟨← Elab.ContextInfo.save⟩
+      userName?
+      goalPrefix := getGoalPrefix mvarDecl
+      mvarId
     }
 
 end Lean.Widget