/Main.lean at 34ecb06d1066bef2057ea835e8347deddc52aa2c

import Lean.Data.Json
import Lens
import Raylean

open Lens
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

def drawCubeWiresV (pos size : Vector3) (color : Color) :=
  drawCubeWires pos size.x size.y size.z color

end Raylean

def fps := 60
def screenWidth := 960
def screenHeight := 640

/-- Grid side length (each cell is 5m by 5m) -/
def N := 200

/-- Grid height -/
def M := 20

def origin : Vector3 := ⟨N.toFloat / 20, M.toFloat / 20, N.toFloat / 20⟩

instance : Add Vector3 where
  add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

instance : Sub Vector3 where
  sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩

instance : HDiv Vector3 Float Vector3 where
  hDiv a b := ⟨a.x / b, a.y / b, a.z / b⟩

structure Nat3 where
  x : Nat
  y : Nat
  z : Nat
deriving Lean.ToJson, Lean.FromJson

inductive BuildingVariant
  | house
  | apartment
  | office
  | shop
  | 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
  variant : BuildingVariant
deriving Lean.ToJson, Lean.FromJson

def Building.occupants (b : Building) :=
  match b.variant with
  | .house => 1
  | .apartment => b.size.x * b.size.y * b.size.z / 2
  | .office => 0
  | .shop => 0
  | .factory => 0

def Building.color (b : Building) :=
  match b.variant with
  | .house => Color.Raylean.red
  | .apartment => Color.Raylean.orange
  | .office => Color.Raylean.blue
  | .shop => Color.Raylean.purple
  | .factory => Color.Raylean.green

structure Vehicle where
  pos : Nat3
  dest : Nat3


inductive Road
  | none
  | low
  | high
deriving Lean.ToJson, Lean.FromJson

instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where
  toJson := Array.toJson ∘ Vector.toArray

instance [Lean.FromJson α] : Lean.FromJson (Vector α n) where
  fromJson? j := do
    let A : Array α ← Array.fromJson? j
    if h : A.size = n then
      return h ▸ A.toVector
    else
      throw s!"expected size {n}, got {A.size}"

structure Point where
  roads : Vector Road 24
  occupant : Option Nat
deriving Lean.ToJson, Lean.FromJson

def Point.empty : Point :=
  ⟨.replicate 24 .none, none⟩

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

makeLenses State

-- 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⟩

def render (s : State) : IO Unit := do
  for b in s.buildings do
    let p := b.pos.toVector3
    let s := b.size.toVector3
    let o := p - origin + s / 2.0
    drawCubeV o s b.color
    drawCubeWiresV o s .black

def getInput (stdin : IO.FS.Stream) := do
  IO.print "> "
  return (← stdin.getLine).trimAsciiEnd.toString

/-- 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
      modify <| over State.Lens.buildings (·.push ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind)⟩)
    else
      throw <| .userError "Failed to parse build command"
  | _ =>
    throw <| .userError "Command not found"

def gameLoop : StateT State IO Unit := do
  let mut camera : Camera3D := {
    position := ⟨10, 10, 10⟩
    target := ⟨0, 0, 0⟩
    up := ⟨0, 1, 0⟩
    fovy := 45
    projection := .perspective
  }
  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)
      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 (← 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 := #[]
  }