Rename to MonotoniCity

Changes

6 changed files (+98/-30)

• Main.lean
  • @@ -14,6 +14,9 @@ instance : Add Vector3 where
    instance : Sub Vector3 where sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩ + instance : HMul Float Vector3 Vector3 where + hMul c a := ⟨a.x * c, a.y * c, a.z * c⟩ + instance : HMul Vector3 Float Vector3 where hMul a c := ⟨a.x * c, a.y * c, a.z * c⟩
  • @@ -81,18 +84,30 @@ def Building.color (b : Building) :=
    | .shop => Color.Raylean.purple | .factory => Color.Raylean.green + instance : Lean.ToJson (Fin n) where + toJson := Lean.toJson ∘ Fin.val + + instance : Lean.FromJson (Fin n) where + fromJson? j := do + let m ← Lean.fromJson? j + if h : m < n then + return ⟨m, h⟩ + else + throw s!"expected val less than {n}, got {m}" + structure Peep where home : Nat work : Nat pos : Nat3 dest : Nat3 + dir : Fin 24 deriving Lean.ToJson, Lean.FromJson inductive Road | none | low | high - deriving Lean.ToJson, Lean.FromJson + deriving BEq, Lean.ToJson, Lean.FromJson instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where toJson := Array.toJson ∘ Vector.toArray
  • @@ -126,7 +141,7 @@ def dz : Vector Int 24 :=
    -- `i` and `23 - i` should be in opposite directions #guard (List.range 24 |>.mapFinIdx fun i _ hi ↦ dx[i] == (-dx[23 - i]) && dy[i] == (-dy[23 - i]) && dz[i] == (-dz[23 - i])).and - def appd (p : Nat3) (i : Nat) (hi : i < 24 := by grind) : Nat3 := + def Nat3.appd (p : Nat3) (i : Nat) (hi : i < 24 := by grind) : Nat3 := ⟨p.x + dx[i] |>.toNat, p.y + dy[i] |>.toNat, p.z + dz[i] |>.toNat⟩ instance : Lean.ToJson StdGen where
  • @@ -152,6 +167,7 @@ instance [BEq α] [Hashable α] [Lean.FromJson α] [Lean.FromJson β] : Lean.Fro
    -- TODO: Money? Eh can do that later structure State where rng : StdGen + ticks : Nat speed : Nat day : Nat time : Nat
  • @@ -163,6 +179,9 @@ structure State where
    occupied : Std.HashSet Nat3 deriving Lean.ToJson, Lean.FromJson + instance [Monad m] : MonadLift (StateM σ ·) (StateT σ m ·) where + monadLift x := modifyGet <| StateT.run x + /-- Macro for easily updating a specific field of the state -/ macro "modifyf" field:ident fn:term : term => let lval := ⟨.node .none `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode]⟩
  • @@ -194,7 +213,7 @@ def mkDist (g : Std.HashMap Nat3 Point) (start : Nat3) := Id.run do
    let d := dist[u]! if hs : g.contains u then for hi : i in List.range 24 do - let v := appd u i + let v := u.appd i match (g[u]'hs).ein[i]'(by grind) with | .low => if !dist.contains v then
  • @@ -208,7 +227,7 @@ def mkDist (g : Std.HashMap Nat3 Point) (start : Nat3) := Id.run do
    if hs : g.contains v then match (g[v]'hs).ein[i]'(by grind) with | .high => - let v' := appd u i + let v' := u.appd i if !dist.contains v' then dist := dist.insert v' (d + 1) q := q.enqueue v'
  • @@ -241,7 +260,7 @@ def Array.shuffle (A : Array α) : StateM State (Array α) := do
    return A'.toArray /-- Run one iteration of the game randomly -/ - def tick : StateM State Unit := do + def doTick : StateM State Unit := do let peeps ← (← get).peeps.shuffle for peep in peeps do -- TODO
  • @@ -259,26 +278,37 @@ def tick : StateM State Unit := do
    def Nat3.toVector3 (p : Nat3) : Vector3 := ⟨p.x.toFloat / 10, p.y.toFloat / 10, p.z.toFloat / 10⟩ + def Nat3.toVector3Shift (p : Nat3) (s : State) : Vector3 := + p.toVector3 - s.origin.toVector3 + /-- Draw the game state -/ - def render (s : State) : IO Unit := do + def render (s : State) (camera : Camera3D) : IO Unit := do for b in s.buildings do let size := b.size.toVector3 - let pos := b.pos.toVector3 - s.origin.toVector3 + size / 2.0 + let pos := b.pos.toVector3Shift s + size / 2.0 drawCubeV pos size b.color drawCubeWiresV pos size .black for (pos, pt) in s.grid do - if pos.x % 10 == 0 && pos.z % 10 == 0 then + if (2 * pos.x + pos.z) % 20 == 0 then -- https://www.raylib.com/examples/core/loader.html?name=core_world_screen - - drawText - let pos' := pos.toVector3 - s.origin.toVector3 - for i in [:24] do - match pt.eout[i] with + let pos2D ← getWorldToScreen (pos.toVector3Shift s) camera + let dir := pt.eout[4] != .none || pt.eout[19] != .none + drawText s!"{if dir then pos.x else pos.z} {pt.name} Street" pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 20 Color.black + let posV3 := pos.toVector3Shift s + for hi : i in List.range 24 do + -- TODO choose better colors + match pt.eout[i]'(by grind) with | .none => pure () | .low => - - + drawLine3D posV3 (pos.appd i |>.toVector3Shift s) Color.black + | .high => + drawLine3D posV3 (pos.appd i |>.toVector3Shift s) Color.Raylean.gray + for p in s.peeps do + if p.pos != p.dest then + -- Unfortunately we can't use `Nat3.toVector3` here because they're `Int`s + let pos := p.pos.toVector3Shift s + (s.ticks.toFloat / (fps / 3 / s.speed).toFloat) * (Vector3.mk (.ofInt dx[p.dir] / 10) (.ofInt dy[p.dir] / 10) (.ofInt dz[p.dir] / 10)) + drawCube pos 0.05 0.05 0.08 Color.Raylean.lime def getInput (stdin : IO.FS.Stream) := do IO.print "> "
  • @@ -290,6 +320,14 @@ def loadState (path : String) : IO State := do
    let json ← .ofExcept <| Lean.Json.parse serialized .ofExcept <| Lean.fromJson? json + def addBuilding (b : Building) : StateM State Unit := do + modifyf buildings (·.push b) + -- TODO check collisions + -- TODO update dists + + def addRoad (start stop : Nat3) (isHigh : Bool) : StateM State Unit := do + sorry + -- TODO: Build roads -- TODO: rename roads def handleCmd (cmd : String) : StateT State IO Unit := do
  • @@ -308,9 +346,14 @@ def handleCmd (cmd : String) : StateT State IO Unit := do
    if h : dims.length = 6 && variant.isSome then let dims := dims.map String.toNat! have : dims.length = 6 := by grind - modifyf buildings (·.push ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind), 0⟩) + addBuilding ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind), 0⟩ else throw <| .userError "Failed to parse build command" + | "r" :: dims => + if h : dims.length = 6 then + let dims := dims.map String.toNat! + have : dims.length = 6 := by grind + | _ => throw <| .userError "Command not found"
  • @@ -333,23 +376,29 @@ def gameLoop : StateT State IO Unit := do
    catch e => IO.println e task ← IO.asTask <| getInput stdin + if fps / 3 / (← get).speed ≤ (← get).ticks then + doTick + modifyf ticks (fun _ ↦ 0) + else + modifyf ticks (· + 1) renderFrame do drawFPS (screenWidth - 100) 10 clearBackground Color.white renderWithCamera camera do let s ← get drawGrid (s.origin.x / 10) 1 - render s + render s camera 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" + initWindow screenWidth screenHeight "MonotoniCity" setTargetFPS fps gameLoop.run' { rng := mkStdGen (← IO.rand 0 (2 ^ 32)) + ticks := 0 speed := 1 day := 0 time := 0
• README.md
  • @@ -1,6 +1,6 @@
    - # LeanTTD + # MonotoniCity - An OpenTTD-like game written in Lean + A city building and transport simulation game written in Lean ## Building
  • @@ -73,3 +73,8 @@ https://www.raylib.com/cheatsheet/cheatsheet.html
    The street names are from https://github.com/rossburton/barnum/blob/master/source-data/street-names.txt + + + ## Why the name? + + `monotonicity` is a tactic in Lean.
• flake.nix
  • @@ -11,7 +11,7 @@
    in { packages.${system}.default = pkgs.leanPackages.buildLakePackage { - pname = "leanttd"; + pname = "monotonicity"; src = self; version = "0.1"; lakeHash = "sha256-z/yuuwpGutWWC1++ZJ189If4TGgJunpwNCh9NGasnRo=";
  • @@ -31,7 +31,7 @@
    }; apps.${system}.default = { type = "app"; - program = "${self.packages.${system}.default}/bin/leanttd"; + program = "${self.packages.${system}.default}/bin/monotonicity"; }; formatter.${system} = pkgs.nixfmt-tree; };
• lake-manifest.json
  • @@ -21,6 +21,6 @@
    "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.lean"}], - "name": "LeanTTD", + "name": "MonotoniCity", "lakeDir": ".lake", "fixedToolchain": false}
• lakefile.toml
  • @@ -1,9 +1,9 @@
    - name = "LeanTTD" + name = "MonotoniCity" version = "0.1.0" - defaultTargets = ["leanttd"] + defaultTargets = ["monotonicity"] [[lean_exe]] - name = "leanttd" + name = "monotonicity" root = "Main" moreLinkArgs = ["-lraylib"]
• raylean.patch
  • @@ -1,5 +1,5 @@
    diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c - index 902a945..bb36469 100644 + index 902a945..17da156 100644 --- a/c/raylib_bindings.c +++ b/c/raylib_bindings.c @@ -314,11 +314,11 @@ static inline Camera2D camera2D_of_arg(lean_obj_arg camera) {
  • @@ -19,10 +19,14 @@ index 902a945..bb36469 100644
    lean_obj_res initWindow(lean_obj_arg width, lean_obj_arg height, b_lean_obj_arg title) { - @@ -402,6 +402,16 @@ lean_obj_res beginMode3D(lean_obj_arg camera) { + @@ -402,6 +402,20 @@ lean_obj_res beginMode3D(lean_obj_arg camera) { return IO_UNIT; } + +lean_obj_res getWorldToScreen (lean_obj_arg position, lean_obj_arg camera) { + + return lean_io_result_mk_ok(vector2_obj_mk(GetWorldToScreen(vector3_of_arg(position), camera3D_of_arg(camera)))); + +} + + +lean_obj_res drawLine3D(lean_obj_arg startPos, lean_obj_arg endPos, lean_obj_arg color) { + DrawLine3D(vector3_of_arg(startPos), vector3_of_arg(endPos), color_of_arg(color)); + return IO_UNIT;
  • @@ -37,10 +41,20 @@ index 902a945..bb36469 100644
    double length, lean_obj_arg color) { DrawCube(vector3_of_arg(position), width, height, length, diff --git a/lean/Raylean/Core.lean b/lean/Raylean/Core.lean - index e0818b6..787a1f9 100644 + index e0818b6..908f271 100644 --- a/lean/Raylean/Core.lean +++ b/lean/Raylean/Core.lean - @@ -112,6 +112,12 @@ opaque drawText : (text : @& String) → (posX : Nat) → (posY : Nat) → (font + @@ -43,6 +43,9 @@ opaque beginMode3D : (camera : @& Camera3D) → IO Unit + @[extern "endMode3D"] + opaque endMode3D : IO Unit + + +@[extern "getWorldToScreen"] + +opaque getWorldToScreen : (position : @& Vector3) → (camera : @& Camera3D) → IO Vector2 + + + /- Timing-related functions -/ + + @[extern "setTargetFPS"] + @@ -112,6 +115,12 @@ opaque drawText : (text : @& String) → (posX : Nat) → (posY : Nat) → (font /- Basic geometric 3D shapes drawing functions -/