show hints

2023-01-24 14:09:34 +01:00
parent 8175d32a3c
commit b7cc5aaf57
4 changed files with 80 additions and 48 deletions
@@ -6,20 +6,21 @@ import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, Interac
 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';

 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
    return h.indexOf('✝') >= 0;
 }

-function goalToString(g: InteractiveGoal): string {
+function goalToString(g: GameInteractiveGoal): string {
    let ret = ''

-    if (g.userName) {
-        ret += `case ${g.userName}\n`
+    if (g.goal.userName) {
+        ret += `case ${g.goal.userName}\n`
    }

-    for (const h of g.hyps) {
+    for (const h of g.goal.hyps) {
        const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ')
        ret += `${names} : ${TaggedText_stripTags(h.type)}`
        if (h.val) {
@@ -28,12 +29,12 @@ function goalToString(g: InteractiveGoal): string {
        ret += '\n'
    }

-    ret += `⊢ ${TaggedText_stripTags(g.type)}`
+    ret += `⊢ ${TaggedText_stripTags(g.goal.type)}`

    return ret
 }

-export function goalsToString(goals: InteractiveGoals): string {
+export function goalsToString(goals: GameInteractiveGoals): string {
    return goals.goals.map(goalToString).join('\n\n')
 }

@@ -111,7 +112,7 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
 }

 interface GoalProps {
-    goal: InteractiveGoal
+    goal: GameInteractiveGoal
    filter: GoalFilterState
 }

@@ -121,44 +122,49 @@ interface GoalProps {
 export const Goal = React.memo((props: GoalProps) => {
    const { goal, filter } = props

-    const prefix = goal.goalPrefix ?? 'Prove: '
-    const filteredList = getFilteredHypotheses(goal.hyps, filter);
+    const prefix = goal.goal.goalPrefix ?? 'Prove: '
+    const filteredList = getFilteredHypotheses(goal.goal.hyps, filter);
    const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
    const locs = React.useContext(LocationsContext)
    const goalLocs = React.useMemo(() =>
-        locs && goal.mvarId ?
-            { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
+        locs && goal.goal.mvarId ?
+            { ...locs, subexprTemplate: { mvarId: goal.goal.mvarId, loc: { target: '' }}} :
            undefined,
-        [locs, goal.mvarId])
+        [locs, goal.goal.mvarId])
    const goalLi = <div key={'goal'}>
        <strong className="goal-vdash">Prove: </strong>
        <LocationsContext.Provider value={goalLocs}>
-            <InteractiveCode fmt={goal.type} />
+            <InteractiveCode fmt={goal.goal.type} />
        </LocationsContext.Provider>
    </div>

    let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
-    if (props.goal.isInserted) cn += 'b--inserted '
-    if (props.goal.isRemoved) cn += 'b--removed '
+    if (props.goal.goal.isInserted) cn += 'b--inserted '
+    if (props.goal.goal.isRemoved) cn += 'b--removed '

-    if (goal.userName) {
+    // TODO: make this prettier
+    const hints = goal.messages.map((m) => <div>{m.message}</div>)
+
+    if (goal.goal.userName) {
        return <details open className={cn}>
            <summary className='mv1 pointer'>
-                <strong className="goal-case">case </strong>{goal.userName}
+                <strong className="goal-case">case </strong>{goal.goal.userName}
            </summary>
            {filter.reverse && goalLi}
-            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
+            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.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.mvarId} key={i} />)}
+        {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.goal.mvarId} key={i} />)}
        {!filter.reverse && goalLi}
+        {hints}
    </div>
 })

 interface GoalsProps {
-    goals: InteractiveGoals
+    goals: GameInteractiveGoals
    filter: GoalFilterState
 }

@@ -179,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?: InteractiveGoals
+    goals?: GameInteractiveGoals
 }

 /**
@@ -11,6 +11,7 @@ import { lspDiagToInteractive, MessagesList } from './messages';
 import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic,
    InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
    RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
+import { GameInteractiveGoal, GameInteractiveGoals } 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';
@@ -76,7 +77,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
 interface InfoDisplayContentProps extends PausableProps {
    pos: DocumentPosition;
    messages: InteractiveDiagnostic[];
-    goals?: InteractiveGoals;
+    goals?: GameInteractiveGoals;
    termGoal?: InteractiveTermGoal;
    error?: string;
    userWidgets: UserWidgetInstance[];
@@ -120,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: [termGoal]} : undefined} />
+            goals={termGoal !== undefined ? {goals: [{goal:termGoal, messages: []}]} : 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 : []} termGoal={termGoal}
+                <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal.goal) : []} termGoal={termGoal}
                    selectedLocations={selectedLocs} widget={widget}/>
            </details>
        )}
@@ -152,7 +153,7 @@ interface InfoDisplayProps {
    pos: DocumentPosition;
    status: InfoStatus;
    messages: InteractiveDiagnostic[];
-    goals?: InteractiveGoals;
+    goals?: GameInteractiveGoals;
    termGoal?: InteractiveTermGoal;
    error?: string;
    userWidgets: UserWidgetInstance[];
@@ -0,0 +1,15 @@
+import { InteractiveGoals, InteractiveGoal } from '@leanprover/infoview-api';
+
+export interface GameMessage {
+  message: string;
+  spoiler: boolean;
+}
+
+export interface GameInteractiveGoal {
+  goal: InteractiveGoal;
+  messages: GameMessage[];
+}
+
+export interface GameInteractiveGoals {
+  goals: GameInteractiveGoal[];
+}
@@ -100,7 +100,7 @@ def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool :=

 open Meta in
 /-- Find all messages whose trigger matches the current goal -/
-def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.FS.Stream) : MetaM (Array GameMessage) := do
+def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array GameMessage) := do
  goal.withContext do
    let level ← getLevelByFileName doc.meta.mkInputContext.fileName
    let messages ← level.messages.filterMapM fun message => do
@@ -109,7 +109,6 @@ def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.
      if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
      then
        let lctx ← getLCtx -- Local context of the `goal`
-        hLog.putStr s!"{← declMvars.mapM inferType} =?= {← lctx.getFVars.mapM inferType}"
        if ← matchDecls declMvars lctx.getFVars
        then
          return some { message := message.message, spoiler := message.spoiler }
@@ -117,8 +116,22 @@ def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.
      else return none
    return messages

+structure GameInteractiveGoal where
+  goal : InteractiveGoal
+  messages: Array GameMessage
+  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 Widget.InteractiveGoals)) := do
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option GameInteractiveGoals)) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
@@ -127,29 +140,26 @@ 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 Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List GameInteractiveGoals ← 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
-          let goals ← ci.runMetaM {} (do
-            let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
-            let goals ← goals.mapM Widget.goalToInteractive
-            return {goals}
-          )
+          let goals ← ci.runMetaM {} do
+            return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
+          let goals ← ci.runMetaM {} do
+             goals.mapM fun goal => do
+              let messages ← findMessages goal doc
+              return {goal := ← Widget.goalToInteractive goal, messages}
          -- compute the goal diff
-          let goals ← ciAfter.runMetaM {} (do
-              try
-                Widget.diffInteractiveGoals useAfter ti goals
-              catch _ =>
-                -- fail silently, since this is just a bonus feature
-                return goals
-          )
-          -- TODO: add hints
-          -- let goals ← ci.runMetaM {} $ goals.mapM fun goal => do
-          --   let messages ← findMessages goal doc hLog
-          --   return ← goal.toGameGoal messages
-          return goals
-        return some <| goals.foldl (· ++ ·) ∅
+          -- let goals ← ciAfter.runMetaM {} (do
+          --     try
+          --       Widget.diffInteractiveGoals useAfter ti goals
+          --     catch _ =>
+          --       -- fail silently, since this is just a bonus feature
+          --       return goals
+          -- )
+          return {goals}
+        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
      else
        return none

@@ -157,7 +167,7 @@ builtin_initialize
  registerBuiltinRpcProcedure
    `Game.getInteractiveGoals
    Lsp.PlainGoalParams
-    (Option InteractiveGoals)
+    (Option GameInteractiveGoals)
    getInteractiveGoals

 structure Diagnostic where