Start working on console interface

Changes

2 changed files (+48/-2)

• Main.lean
  • @@ -1,6 +1,8 @@
    import Lean.Data.Json + import Lens import Raylean + open Lens open Raylean Types namespace Raylean
  • @@ -49,6 +51,14 @@ inductive BuildingVariant
    | factory deriving Lean.ToJson, Lean.FromJson + def BuildingVariant.ofString? : String → Option BuildingVariant + | "h" | "house" => some .house + | "a" | "apartment" => some .apartment + | "o" | "office" => some .office + | "s" | "shop" => some .shop + | "f" | "factory" => some .factory + | _ => none + structure Building where pos : Nat3 size : Nat3
  • @@ -103,15 +113,20 @@ def Point.empty : Point :=
    abbrev Grid := Vector (Vector (Vector Point (M + 1)) (N + 1)) (N + 1) + -- TODO: routing table for each building, reverse grid structure State where + rng : Nat day : Nat time : Nat grid : Grid buildings : Array Building deriving Lean.ToJson, Lean.FromJson - def tick (g : Grid) : Grid := Id.run do - return g + 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
  • @@ -133,6 +148,27 @@ def render (s : State) : IO Unit := do
    drawCubeV o s b.color drawCubeWiresV o s .black + 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) := + match cmd.split ' ' |>.toStringList with + | "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 + else + s + | _ => + s + 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
  • @@ -147,13 +183,21 @@ def main : IO Unit := do
    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 + task ← IO.asTask <| getInput stdin renderFrame do drawFPS (screenWidth - 100) 10 clearBackground Color.white
• README.md
  • @@ -12,6 +12,8 @@ Otherwise, install Raylib and run `lake build` and hope for the best. It probabl
    To build a (huge) precompiled bundle that can run on any Linux distro, run `nix bundle .#packages.x86_64-linux.default`. + I recommend running the game with `rlwrap` for a slightly nicer console. + ## Random notes Rewrite (a small subset of) OpenTTD in Lean!