custom interactive goal data types

client/src/components/infoview/goals.tsx

@@ -2,11 +2,11 @@
 
 import * as React from 'react'
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
+import { InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
 import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
-import { GameInteractiveGoal, GameInteractiveGoals } from './rpcApi';
+import { InteractiveGoal, InteractiveGoals } from './rpcApi';
 import { Hints } from './hints';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
@@ -14,14 +14,14 @@ function isInaccessibleName(h: string): boolean {
     return h.indexOf('✝') >= 0;
 }
 
-function goalToString(g: GameInteractiveGoal): string {
+function goalToString(g: InteractiveGoal): string {
     let ret = ''
 
-    if (g.goal.userName) {
-        ret += `case ${g.goal.userName}\n`
+    if (g.userName) {
+        ret += `case ${g.userName}\n`
     }
 
-    for (const h of g.goal.hyps) {
+    for (const h of g.hyps) {
         const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ')
         ret += `${names} : ${TaggedText_stripTags(h.type)}`
         if (h.val) {
@@ -30,12 +30,12 @@ function goalToString(g: GameInteractiveGoal): string {
         ret += '\n'
     }
 
-    ret += `⊢ ${TaggedText_stripTags(g.goal.type)}`
+    ret += `⊢ ${TaggedText_stripTags(g.type)}`
 
     return ret
 }
 
-export function goalsToString(goals: GameInteractiveGoals): string {
+export function goalsToString(goals: InteractiveGoals): string {
     return goals.goals.map(goalToString).join('\n\n')
 }
 
@@ -113,7 +113,7 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
 }
 
 interface GoalProps {
-    goal: GameInteractiveGoal
+    goal: InteractiveGoal
     filter: GoalFilterState
 }
 
@@ -123,48 +123,48 @@ interface GoalProps {
 export const Goal = React.memo((props: GoalProps) => {
     const { goal, filter } = props
 
-    const prefix = goal.goal.goalPrefix ?? 'Prove: '
-    const filteredList = getFilteredHypotheses(goal.goal.hyps, filter);
+    const prefix = goal.goalPrefix ?? 'Prove: '
+    const filteredList = getFilteredHypotheses(goal.hyps, filter);
     const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
     const locs = React.useContext(LocationsContext)
     const goalLocs = React.useMemo(() =>
-        locs && goal.goal.mvarId ?
-            { ...locs, subexprTemplate: { mvarId: goal.goal.mvarId, loc: { target: '' }}} :
+        locs && goal.mvarId ?
+            { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
             undefined,
-        [locs, goal.goal.mvarId])
+        [locs, goal.mvarId])
     const goalLi = <div key={'goal'}>
         <strong className="goal-vdash">Prove: </strong>
         <LocationsContext.Provider value={goalLocs}>
-            <InteractiveCode fmt={goal.goal.type} />
+            <InteractiveCode fmt={goal.type} />
         </LocationsContext.Provider>
     </div>
 
     let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
-    if (props.goal.goal.isInserted) cn += 'b--inserted '
-    if (props.goal.goal.isRemoved) cn += 'b--removed '
+    if (props.goal.isInserted) cn += 'b--inserted '
+    if (props.goal.isRemoved) cn += 'b--removed '
 
     const hints = <Hints hints={goal.hints} />
 
-    if (goal.goal.userName) {
+    if (goal.userName) {
         return <details open className={cn}>
             <summary className='mv1 pointer'>
-                <strong className="goal-case">case </strong>{goal.goal.userName}
+                <strong className="goal-case">case </strong>{goal.userName}
             </summary>
             {filter.reverse && goalLi}
-            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.goal.mvarId} key={i} />)}
+            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
             {!filter.reverse && goalLi}
             {hints}
         </details>
     } else return <div className={cn}>
         {filter.reverse && goalLi}
-        {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.goal.mvarId} key={i} />)}
+        {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
         {!filter.reverse && goalLi}
         {hints}
     </div>
 })
 
 interface GoalsProps {
-    goals: GameInteractiveGoals
+    goals: InteractiveGoals
     filter: GoalFilterState
 }
 
@@ -185,7 +185,7 @@ interface FilteredGoalsProps {
      * When this is `undefined`, the component will not appear at all but will remember its state
      * by virtue of still being mounted in the React tree. When it does appear again, the filter
      * settings and collapsed state will be as before. */
-    goals?: GameInteractiveGoals
+    goals?: InteractiveGoals
 }
 
 /**

client/src/components/infoview/info.tsx

@@ -8,10 +8,10 @@ import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, d
     mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { lspDiagToInteractive, MessagesList } from './messages';
-import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic,
-    InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
+import { getInteractiveTermGoal, InteractiveDiagnostic,
+    UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
     RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
-import { GameInteractiveGoal, GameInteractiveGoals } from './rpcApi';
+import { InteractiveGoal, InteractiveGoals } from './rpcApi';
 import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget'
 import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
@@ -77,7 +77,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
 interface InfoDisplayContentProps extends PausableProps {
     pos: DocumentPosition;
     messages: InteractiveDiagnostic[];
-    goals?: GameInteractiveGoals;
+    goals?: InteractiveGoals;
     termGoal?: InteractiveTermGoal;
     error?: string;
     userWidgets: UserWidgetInstance[];
@@ -121,11 +121,11 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             {goals && <Goals filter={{ reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }} key='goals' goals={goals} />}
         </LocationsContext.Provider>
         <FilteredGoals headerChildren='Expected type' key='term-goal'
-            goals={termGoal !== undefined ? {goals: [{goal:termGoal, hints: []}]} : undefined} />
+            goals={termGoal !== undefined ? {goals: [termGoal as any]} : undefined} />
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
                 <summary className='mv2 pointer'>{widget.name}</summary>
-                <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal.goal) : []} termGoal={termGoal}
+                <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal) : []} termGoal={termGoal}
                     selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
@@ -153,7 +153,7 @@ interface InfoDisplayProps {
     pos: DocumentPosition;
     status: InfoStatus;
     messages: InteractiveDiagnostic[];
-    goals?: GameInteractiveGoals;
+    goals?: InteractiveGoals;
     termGoal?: InteractiveTermGoal;
     error?: string;
     userWidgets: UserWidgetInstance[];

client/src/components/infoview/rpcApi.ts

@@ -1,15 +1,27 @@
-import { InteractiveGoals, InteractiveGoal } from '@leanprover/infoview-api';
+import { ContextInfo, InteractiveHypothesisBundle, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
 
 export interface GameHint {
   text: string;
   hidden: boolean;
 }
 
-export interface GameInteractiveGoal {
-  goal: InteractiveGoal;
+export interface InteractiveGoalCore {
+  hyps: InteractiveHypothesisBundle[];
+  type: CodeWithInfos;
+  /** Present since server version 1.1.2. */
+  ctx?: ContextInfo;
+}
+
+export interface InteractiveGoal extends InteractiveGoalCore {
+  userName?: string;
+  goalPrefix?: string;
+  /** Present since server version 1.1.2. */
+  mvarId?: MVarId;
+  isInserted?: boolean;
+  isRemoved?: boolean;
   hints: GameHint[];
 }
 
-export interface GameInteractiveGoals {
-  goals: GameInteractiveGoal[];
+export interface InteractiveGoals {
+  goals: InteractiveGoal[];
 }

server/leanserver/GameServer/InteractiveGoal.lean

@@ -0,0 +1,197 @@
+/- This file is mostly copied from `Lean/Widget/InteractiveGoal.lean`. -/
+
+import Lean.Widget.InteractiveGoal
+
+/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
+
+namespace GameServer
+open Lean Lean.Widget Lean.Server
+
+structure GameHint where
+  text : String
+  hidden : Bool
+deriving FromJson, ToJson
+
+/-- 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. -/
+  names : Array Name
+  /-- The ids for each variable. Should have the same length as `names`. -/
+  fvarIds : Array FVarId
+  type : CodeWithInfos
+  /-- The value, in the case the hypothesis is a `let`-binder. -/
+  val? : Option CodeWithInfos := none
+  /-- The hypothesis is a typeclass instance. -/
+  isInstance? : Option Bool := none
+  /-- The hypothesis is a type. -/
+  isType? : Option Bool := none
+  /-- If true, the hypothesis was not present on the previous tactic state.
+  Only present in tactic-mode goals. -/
+  isInserted? : Option Bool := none
+  /-- If true, the hypothesis will be removed in the next tactic state.
+  Only present in tactic-mode goals. -/
+  isRemoved? : Option Bool := none
+  deriving Inhabited, RpcEncodable
+
+/-- 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
+
+/-- 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
+  hints : Array GameHint := #[]
+  deriving RpcEncodable
+
+/-- 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 RpcEncodable
+
+def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
+    (goalPrefix : String) : Format := Id.run do
+  let indent := 2 -- Use option
+  let mut ret := match userName? with
+    | some userName => f!"case {userName}"
+    | none          => Format.nil
+  for hyp in g.hyps do
+    ret := addLine ret
+    let names := hyp.names
+        |>.toList
+        |>.filter (not ∘ Name.isAnonymous)
+        |>.map toString
+        |> " ".intercalate
+    match names with
+    | "" =>
+      ret := ret ++ Format.group f!":{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
+    | _ =>
+      match hyp.val? with
+      | some val =>
+        ret := ret ++ Format.group f!"{names} : {hyp.type.stripTags} :={Format.nest indent (Format.line ++ val.stripTags)}"
+      | none =>
+        ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
+  ret := addLine ret
+  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
+
+def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
+  g.toInteractiveGoalCore.pretty none "⊢ "
+
+structure InteractiveGoals where
+  goals : Array InteractiveGoal
+  deriving RpcEncodable
+
+def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
+  goals := l.goals ++ r.goals
+
+instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
+instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
+
+open Meta in
+/-- 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
+    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
+variable [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadOptions n] [MonadMCtx n] in
+def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α) : n α := do
+  let mctx ← getMCtx
+  let some mvarDecl := mctx.findDecl? goal
+    | throwError "unknown goal {goal.name}"
+  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) (hints : Array GameHint): MetaM InteractiveGoal := do
+  let ppAuxDecls := pp.auxDecls.get (← getOptions)
+  let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
+  let showLetValues := pp.showLetValues.get (← getOptions)
+  withGoalCtx mvarId fun lctx mvarDecl => do
+    let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
+        : MetaM (Array InteractiveHypothesisBundle) :=
+      if ids.isEmpty then
+        pure hyps
+      else
+        match type? with
+        | none      => pure hyps
+        | some type => addInteractiveHypothesisBundle hyps ids type
+    let mut varNames : Array (Name × FVarId) := #[]
+    let mut prevType? : Option Expr := none
+    let mut hyps : Array InteractiveHypothesisBundle := #[]
+    for localDecl in lctx do
+      if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then
+        continue
+      else
+        match localDecl with
+        | LocalDecl.cdecl _index fvarId varName type _ _ =>
+          let varName := varName.simpMacroScopes
+          let type ← instantiateMVars type
+          if prevType? == none || prevType? == some type then
+            varNames := varNames.push (varName, fvarId)
+          else
+            hyps ← pushPending varNames prevType? hyps
+            varNames := #[(varName, fvarId)]
+          prevType? := some type
+        | LocalDecl.ldecl _index fvarId varName type val _ _ => do
+          let varName := varName.simpMacroScopes
+          hyps ← pushPending varNames prevType? hyps
+          let type ← instantiateMVars type
+          let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
+          hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val?
+          varNames := #[]
+          prevType? := none
+    hyps ← pushPending varNames prevType? hyps
+    let goalTp ← instantiateMVars mvarDecl.type
+    let goalFmt ← ppExprTagged goalTp
+    let userName? := match mvarDecl.userName with
+      | Name.anonymous => none
+      | name           => some <| toString name.eraseMacroScopes
+    return {
+      hyps
+      type := goalFmt
+      ctx := ⟨← Elab.ContextInfo.save⟩
+      userName?
+      goalPrefix := getGoalPrefix mvarDecl
+      mvarId
+      hints
+    }
+
+end GameServer

server/leanserver/GameServer/RpcHandlers.lean

@@ -1,5 +1,6 @@
 import Lean
 import GameServer.EnvExtensions
+import GameServer.InteractiveGoal
 
 open Lean
 open Server
@@ -10,11 +11,6 @@ open Meta
 
 /-! ## GameGoal -/
 
-structure GameHint where
-  text : String
-  hidden : Bool
-deriving FromJson, ToJson
-
 namespace GameServer
 
 -- TODO: Find a better way to pass on the file name?
@@ -72,22 +68,8 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array
       else return none
     return hints
 
-structure GameInteractiveGoal where
-  goal : InteractiveGoal
-  hints: Array GameHint
-  deriving RpcEncodable
-
-structure GameInteractiveGoals where
-  goals : Array GameInteractiveGoal
-  deriving RpcEncodable
-
-def GameInteractiveGoals.append (l r : GameInteractiveGoals) : GameInteractiveGoals where
-  goals := l.goals ++ r.goals
-
-instance : Append GameInteractiveGoals := ⟨GameInteractiveGoals.append⟩
-
 open RequestM in
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option GameInteractiveGoals)) := do
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
@@ -96,7 +78,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals : List GameInteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
           let ciAfter := { ci with mctx := ti.mctxAfter }
           let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
           -- compute the interactive goals
@@ -105,7 +87,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           let goals ← ci.runMetaM {} do
              goals.mapM fun goal => do
               let hints ← findHints goal doc
-              return {goal := ← Widget.goalToInteractive goal, hints}
+              return ← goalToInteractive goal hints
           -- compute the goal diff
           -- let goals ← ciAfter.runMetaM {} (do
           --     try
@@ -123,7 +105,7 @@ builtin_initialize
   registerBuiltinRpcProcedure
     `Game.getInteractiveGoals
     Lsp.PlainGoalParams
-    (Option GameInteractiveGoals)
+    (Option InteractiveGoals)
     getInteractiveGoals
 
 end GameServer