diff --git a/client/public/worker.js b/client/public/worker.js index 822f8a7..201124f 100644 --- a/client/public/worker.js +++ b/client/public/worker.js @@ -2,7 +2,6 @@ var stderrBuffer = "" var messageBuffer = [] var initialized = false; -var pointer = null; var headerMode = true; var header=""; @@ -16,7 +15,7 @@ function flushMessageBuffer(){ if (initialized) { while(messageBuffer.length > 0) { var msg = messageBuffer.shift(); - Module.ccall('send_message', 'void', ['string', 'pointer'], [msg, pointer]); + Module.ccall('send_message', 'void', ['string'], [msg]); } } } @@ -58,7 +57,7 @@ var Module = { }], "noInitialRun": true, "onRuntimeInitialized": () => { - pointer = Module.ccall('main', 'pointer', [], []); + Module.ccall('main', 'void', [], []); initialized = true; if (stderrBuffer !== "") { console.log(stderrBuffer); diff --git a/server/GameServer.lean b/server/GameServer.lean index e329fed..9cb6218 100644 --- a/server/GameServer.lean +++ b/server/GameServer.lean @@ -5,8 +5,9 @@ import GameServer.Game Game "TestGame" Title "Hello Test" -MakeGame +World "Test" +Level 1 + +Statement : 1 = 1 := sorry -#eval do - let env ← (Lean.getEnv : Lean.MetaM _) - return (gameExt.getState env).size +MakeGame diff --git a/server/GameServer/WasmServer.lean b/server/GameServer/WasmServer.lean index 795c53a..efe9692 100644 --- a/server/GameServer/WasmServer.lean +++ b/server/GameServer/WasmServer.lean @@ -11,10 +11,12 @@ open Lsp open JsonRpc open System.Uri -def ServerState := GameServerState +structure WasmServerState := + initParams? : Option InitializeParams + gameServerState : GameServerState @[export game_make_state] -unsafe def makeState : IO (ServerState) := do +unsafe def makeState : IO WasmServerState := do let e ← IO.getStderr try Lean.enableInitializersExecution @@ -25,7 +27,7 @@ unsafe def makeState : IO (ServerState) := do { module := `Init : Import }, { module := `GameServer : Import } ] {} 0 --← createEnv gameDir module, - game := "TEST", + game := `TestGame, gameDir := "test", inventory := #[] difficulty := 0 @@ -46,7 +48,7 @@ unsafe def makeState : IO (ServerState) := do -- let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) -- let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) e.putStrLn s!"{gameJson}" - return state + return ⟨none, state⟩ catch err => e.putStrLn s!"Import error: {err}" throw err @@ -87,27 +89,59 @@ def initializeServer (id : RequestID) : IO Unit := do return () -@[export game_send_message] -unsafe def sendMessage (s : String) (state : ServerState) : IO Unit := do +def mkContext (state : WasmServerState) : IO ServerContext := do + let i ← IO.getStdin let o ← IO.getStdout + let e ← IO.getStderr + let srcSearchPath ← searchPathRef.get + let references ← IO.mkRef (← loadReferences) + let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap) + let workerPath := "no-worker-path" + let some initParams := state.initParams? + | throwServerError "no yet initialized" + return { + hIn := i + hOut := o + hLog := e + args := [] + fileWorkersRef := fileWorkersRef + initParams + workerPath + srcSearchPath + references + } + +def runGameServerM (x : GameServerM α) (state : WasmServerState) : IO (α × WasmServerState) := do + let (res, gameServerState) ← ReaderT.run + (StateT.run x state.gameServerState) + (← mkContext state) + return (res, {state with gameServerState}) + +def readParams (params? : Option Json.Structured) [FromJson α] : IO α := + let j := toJson params? + match fromJson? j with + | Except.ok v => pure v + | Except.error inner => throw $ userError s!"Unexpected param '{j.compress}' \n{inner}" + +@[export game_send_message] +unsafe def sendMessage (s : String) (state : WasmServerState) : IO WasmServerState := do let e ← IO.getStderr try let m ← readMessage s match m with | Message.request id "initialize" params? => + let p : InitializeParams ← readParams params? initializeServer id - | Message.request id "info" _ => - - let some game := (gameExt.getState state.env).find? `TestGame - | throwServerError "Game not found" - let gameJson : Json := toJson game - -- Add world sizes to Json object - -- let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) - -- let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) - e.putStrLn s!"{gameJson}" - o.writeLspResponse ⟨id, gameJson⟩ - | _ => pure () --throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" - + return {state with initParams? := some p} + | _ => + let (isGameEv, state) ← runGameServerM (Game.handleServerEvent (.clientMsg m)) state + if isGameEv then + return state + else + match m with + | _ => + e.putStrLn s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" + return state catch err => e.putStrLn s!"Server error: {err}" - return () + return state diff --git a/server/main.c b/server/main.c index 9f9fedd..9bf6a57 100644 --- a/server/main.c +++ b/server/main.c @@ -14,7 +14,7 @@ lean_object * state; lean_object * io_world; -lean_object * main() { +void main() { lean_initialize(); lean_initialize_runtime_module(); lean_object * res; @@ -27,21 +27,26 @@ lean_object * main() { } else { lean_io_result_show_error(res); lean_dec(res); - return 0; // do not access Lean declarations if initialization failed + return; // do not access Lean declarations if initialization failed } lean_io_mark_end_initialization(); res = game_make_state(io_world); if (lean_io_result_is_ok(res)) { state = lean_io_result_get_value(res); - return state; } else { lean_io_result_show_error(res); lean_dec(res); - return 0; // do not access Lean declarations if initialization failed + return; // do not access Lean declarations if initialization failed } } -void send_message(char* msg, lean_object * state){ +void send_message(char* msg){ lean_object * s = lean_mk_string(msg); - game_send_message(s, state, io_world); + lean_object * res = game_send_message(s, state, io_world); + if (lean_io_result_is_ok(res)) { + state = lean_io_result_get_value(res); + } else { + lean_io_result_show_error(res); + lean_dec(res); + } }