From ef63f40531410a4773444c3e0d2feb66f60f4e8f Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 30 Nov 2022 14:40:20 +0100
Subject: [PATCH] custom goal display

---
 client/src/components/Infoview.tsx            |  8 +-
 client/src/components/TacticState.tsx         | 11 ++-
 server/leanserver/GameServer/FileWorker.lean  |  1 +
 server/leanserver/GameServer/RpcHandlers.lean | 84 +++++++++++++++++++
 4 files changed, 96 insertions(+), 8 deletions(-)
 create mode 100644 server/leanserver/GameServer/RpcHandlers.lean

diff --git a/client/src/components/Infoview.tsx b/client/src/components/Infoview.tsx
index 53ea5b5..b6b1ba1 100644
--- a/client/src/components/Infoview.tsx
+++ b/client/src/components/Infoview.tsx
@@ -4,6 +4,7 @@ import { EditorApi } from '@leanprover/infoview-api'
 import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import * as ls from 'vscode-languageserver-protocol'
+import TacticState from './TacticState';
 
 // TODO: move into Lean 4 web
 function toLanguageServerPosition (pos: monaco.Position): ls.Position {
@@ -17,13 +18,14 @@ function Infoview({ ready, editor, editorApi, uri, leanClient } : {ready: boolea
     const rpcSession = await editorApi.createRpcSession(uri)
     const fetchInteractiveGoals = () => {
       const pos = toLanguageServerPosition(editor.getPosition())
-      leanClient.sendRequest("$/lean/rpc/call", {"method":"Lean.Widget.getInteractiveGoals",
+      leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getGoals",
         "params":{"textDocument":{uri}, "position": pos},
         "sessionId":rpcSession,
         "textDocument":{uri},
         "position": pos
       }).then(({ goals }) => {
         setGoals(goals)
+        console.log(goals)
       }).catch((err) => {
         console.error(err)
       })
@@ -44,7 +46,9 @@ function Infoview({ ready, editor, editorApi, uri, leanClient } : {ready: boolea
   }, [ready])
    // Lean.Widget.getInteractiveGoals
 
-  return (<div>Number of Goals: {goals !== null ? goals.length : "None"}</div>)
+  return (<div>
+    <TacticState goals={goals} errors={[]} completed={false}></TacticState>
+  </div>)
 }
 
 export default Infoview
diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx
index 2e158c6..5442cd8 100644
--- a/client/src/components/TacticState.tsx
+++ b/client/src/components/TacticState.tsx
@@ -18,9 +18,9 @@ function Goal({ goal }) {
       {hasObject && <Box><Typography>Objects</Typography>
         <List>
           {goal.objects.map((item) =>
-            <ListItem key={item[0]}>
-              <Typography color="primary" sx={{ mr: 1 }}>{item[0]}</Typography> :
-              <Typography color="secondary" sx={{ ml: 1 }}>{item[1]}</Typography>
+            <ListItem key={item.userName}>
+              <Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
+              <Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
             </ListItem>)}
         </List></Box>}
       {hasAssumption && <Box><Typography>Assumptions</Typography>
@@ -33,9 +33,9 @@ function Goal({ goal }) {
     </Box>)
 }
 
-function TacticState({ goals, errors, lastTactic, completed }) {
+function TacticState({ goals, errors, completed }) {
   const hasError = typeof errors === "object" && errors.length > 0
-  const hasGoal = typeof goals === "object" && goals.length > 0
+  const hasGoal = goals !== null && goals.length > 0
   const hasManyGoal = hasGoal && goals.length > 1
   var col = ""
   var msg = ""
@@ -54,7 +54,6 @@ function TacticState({ goals, errors, lastTactic, completed }) {
       {hasGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5">Current goal</Typography> <Goal goal={goals[0]} /></Paper>}
       {completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
       {hasError && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5" color="error">Spell invocation failed</Typography>
-        <Typography sx={{ my: 1 }}>{lastTactic}</Typography>
         <Typography component="pre" sx={{ my: 1 }}>{col}{msg}</Typography>
         <Typography>Use the undo button to go back to a sane state.</Typography>
         </Paper>}
diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index a9cdfa4..f9466dd 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -2,6 +2,7 @@
 
 import Lean
 import GameServer.EnvExtensions
+import GameServer.RpcHandlers
 
 namespace MyModule
 open Lean
diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
new file mode 100644
index 0000000..294426b
--- /dev/null
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -0,0 +1,84 @@
+import Lean
+
+open Lean
+open Server
+open Widget
+open RequestM
+open Meta
+
+
+/-! ## GameGoal -/
+
+structure GameLocalDecl where
+  userName : Name
+  type : String
+deriving FromJson, ToJson
+
+structure GameGoal where
+  objects : List GameLocalDecl
+  assumptions : List GameLocalDecl
+  goal : String
+deriving FromJson, ToJson
+
+
+def Lean.MVarId.toGameGoal (goal : MVarId) : MetaM GameGoal := do
+match (← getMCtx).findDecl? goal with
+| none          => throwError "unknown goal"
+| some mvarDecl => do
+  -- toGameGoalAux below will sort local declarations from the context of goal into data and assumptions,
+  -- discarding auxilliary declarations
+  let rec toGameGoalAux : List (Option LocalDecl) → MetaM (List LocalDecl × List LocalDecl)
+  | (some decl)::t => withLCtx mvarDecl.lctx mvarDecl.localInstances do
+    let (o, a) ← toGameGoalAux t
+    if decl.isAuxDecl then
+      return (o, a)
+    if (← inferType decl.type).isProp then
+      return (o, decl::a)
+    else
+      return (decl::o, a)
+  | none:: t => toGameGoalAux t
+  | [] => return ([], [])
+  withLCtx mvarDecl.lctx mvarDecl.localInstances do
+    let (objects, assumptions) ← toGameGoalAux mvarDecl.lctx.decls.toList
+    let objects ← objects.mapM fun decl => do
+      return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) }
+    let assumptions ← assumptions.mapM fun decl => do
+      return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) }
+    return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type) }
+
+
+namespace GameServer
+
+
+/-- `Game.getGoals` client<-server reply. -/
+structure PlainGoal where
+  /-- The pretty-printed goals, empty if all accomplished. -/
+  goals : Array GameGoal
+  deriving FromJson, ToJson
+
+def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal)) := do
+  let doc ← readDoc
+  let text := doc.meta.text
+  let hoverPos := text.lspPosToUtf8Pos p.position
+  -- NOTE: use `>=` since the cursor can be *after* the input
+  withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
+    (notFoundX := return none) fun snap => do
+      if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
+        let goals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+          let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
+          let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
+          let goals ← ci.runMetaM {} $ goals.mapM fun goal => do
+            return ← goal.toGameGoal
+          return goals
+        return some { goals := goals.foldl (· ++ ·) ∅ }
+      else
+        return none
+
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Game.getGoals
+    Lsp.PlainGoalParams
+    (Option PlainGoal)
+    getGoals
+
+end GameServer