Use the state monad

Changes

2 changed files (+46/-38)

• Main.lean
  • @@ -7,6 +7,9 @@ open Raylean Types
    namespace Raylean + -- Helpful for debugging + instance : ToString Vector3 := ⟨fun v ↦ s!"({v.1}, {v.2}, {v.3})"⟩ + /-- This is in Raylib but not Raylean so let's just define it ourselves -/ def drawCubeV (pos size : Vector3) (color : Color) := drawCube pos size.x size.y size.z color
  • @@ -20,8 +23,8 @@ def fps := 60
    def screenWidth := 960 def screenHeight := 640 - /-- Grid side length -/ - def N := 500 + /-- Grid side length (each cell is 5m by 5m) -/ + def N := 200 /-- Grid height -/ def M := 20
  • @@ -124,22 +127,13 @@ deriving Lean.ToJson, Lean.FromJson
    makeLenses State - -- This is a big TODO, probably want to use a state monad here? - def tick (s : State) : State := Id.run do - return s - - - def myroad : Road := .low - - def serialized := Lean.toJson myroad |>.compress - - def blah : Except String Road := Lean.Json.parse serialized >>= Lean.fromJson? + -- TODO + def tick : StateM State Unit := do + modify <| over State.Lens.rng (· + 2) def Nat3.toVector3 (p : Nat3) : Vector3 := ⟨p.x.toFloat / 10, p.y.toFloat / 10, p.z.toFloat / 10⟩ - instance : ToString Vector3 := ⟨fun v ↦ s!"({v.1}, {v.2}, {v.3})"⟩ - def render (s : State) : IO Unit := do for b in s.buildings do let p := b.pos.toVector3
  • @@ -152,29 +146,31 @@ def getInput (stdin : IO.FS.Stream) := do
    IO.print "> " return (← stdin.getLine).trimAsciiEnd.toString - -- TODO error messages - -- Load game - -- Save game - -- Build roads - def handleCmd (s : State) (cmd : String) := + /-- Load game state from file -/ + def loadState (path : String) : IO State := do + let serialized ← IO.FS.readFile path + let json ← .ofExcept <| Lean.Json.parse serialized + .ofExcept <| Lean.fromJson? json + + -- TODO: Build roads + def handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with + | ["s", path] => + IO.FS.writeFile path <| Lean.toJson (← get) |>.compress + | ["l", path] => + set <| ← loadState path | "b" :: variant :: dims => let variant := BuildingVariant.ofString? variant if h : dims.length = 6 && variant.isSome then let dims := dims.map String.toNat! have : dims.length = 6 := by grind - over State.Lens.buildings (fun (b : Array Building) ↦ b.push ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind)⟩) s + modify <| over State.Lens.buildings (·.push ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind)⟩) else - s + throw <| .userError "Failed to parse build command" | _ => - s + throw <| .userError "Command not found" - def main : IO Unit := do - -- This constant is FLAG_WINDOW_HIGHDPI || FLAG_WINDOW_RESIZABLE - -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567 - setConfigFlags 0x00002004 - initWindow screenWidth screenHeight "LeanTTD" - setTargetFPS fps + def gameLoop : StateT State IO Unit := do let mut camera : Camera3D := { position := ⟨10, 10, 10⟩ target := ⟨0, 0, 0⟩
  • @@ -182,26 +178,35 @@ def main : IO Unit := do
    fovy := 45 projection := .perspective } - let mut s : State := { - rng := 0 - day := 0 - time := 0 - grid := Vector.replicate _ (Vector.replicate _ (Vector.replicate _ .empty)) - buildings := #[⟨⟨250, 10, 250⟩, ⟨20, 5, 5⟩, .apartment⟩] - } let stdin ← IO.getStdin let mut task ← IO.asTask <| getInput stdin while !(← windowShouldClose) do camera ← updateCamera camera .thirdPerson if ← IO.hasFinished task then let cmd ← (.ofExcept task.get) - s := handleCmd s cmd - IO.println <| Lean.toJson s.buildings + try + handleCmd cmd + catch e => + IO.println e task ← IO.asTask <| getInput stdin renderFrame do drawFPS (screenWidth - 100) 10 clearBackground Color.white renderWithCamera camera do drawGrid (N / 20) 1 - render s + render (← get) closeWindow + + def main : IO Unit := do + -- This constant is FLAG_WINDOW_HIGHDPI || FLAG_WINDOW_RESIZABLE + -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567 + setConfigFlags 0x00002004 + initWindow screenWidth screenHeight "LeanTTD" + setTargetFPS fps + _ ← gameLoop.run { + rng := 0 + day := 0 + time := 0 + grid := Vector.replicate _ (Vector.replicate _ (Vector.replicate _ .empty)) + buildings := #[] + }
• README.md
  • @@ -67,3 +67,6 @@ WARNING: GLFW: Error: 65542 Description: EGL: Failed to get EGL display: Success
    WARNING: GLFW: Failed to initialize Window WARNING: SYSTEM: Failed to initialize platform INFO: TIMER: Target time per frame: 16.667 milliseconds + + + https://www.raylib.com/cheatsheet/cheatsheet.html