From b7cc5aaf57a8b3de6c8f532dfe45c6b52df5d539 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 24 Jan 2023 14:09:34 +0100 Subject: [PATCH] show hints --- client/src/components/infoview/goals.tsx | 48 +++++++++------- client/src/components/infoview/info.tsx | 9 +-- client/src/components/infoview/rpcApi.ts | 15 +++++ server/leanserver/GameServer/RpcHandlers.lean | 56 +++++++++++-------- 4 files changed, 80 insertions(+), 48 deletions(-) create mode 100644 client/src/components/infoview/rpcApi.ts diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index d40fbb1..1a290bf 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -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 =
Prove: - +
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) =>
{m.message}
) + + if (goal.goal.userName) { return
- case {goal.userName} + case {goal.goal.userName} {filter.reverse && goalLi} - {hyps.map((h, i) => )} + {hyps.map((h, i) => )} {!filter.reverse && goalLi} + {hints}
} else return
{filter.reverse && goalLi} - {hyps.map((h, i) => )} + {hyps.map((h, i) => )} {!filter.reverse && goalLi} + {hints}
}) 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 } /** diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 3bed742..8899f82 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -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={termGoal !== undefined ? {goals: [{goal:termGoal, messages: []}]} : undefined} /> {userWidgets.map(widget =>
{widget.name} - goal.goal) : []} termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
)} @@ -152,7 +153,7 @@ interface InfoDisplayProps { pos: DocumentPosition; status: InfoStatus; messages: InteractiveDiagnostic[]; - goals?: InteractiveGoals; + goals?: GameInteractiveGoals; termGoal?: InteractiveTermGoal; error?: string; userWidgets: UserWidgetInstance[]; diff --git a/client/src/components/infoview/rpcApi.ts b/client/src/components/infoview/rpcApi.ts new file mode 100644 index 0000000..f07cece --- /dev/null +++ b/client/src/components/infoview/rpcApi.ts @@ -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[]; +} diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index 1ce3777..791ef7f 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -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