Bump to Lean v4.31, add patch for more Raylean bindings

Changes

4 changed files (+167/-67)

• Main.lean
  • @@ -1,14 +1,12 @@
    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})"⟩ + instance : ToString Vector3 := ⟨fun a ↦ s!"({a.x}, {a.y}, {a.z})"⟩ instance : Add Vector3 where add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
  • @@ -59,11 +57,11 @@ def BuildingVariant.ofString? : String → Option BuildingVariant
    | _ => none structure Building where + variant : BuildingVariant pos : Nat3 size : Nat3 entrance : Nat3 exit : Nat3 - variant : BuildingVariant occupants : Nat deriving Lean.ToJson, Lean.FromJson
  • @@ -83,8 +81,7 @@ def Building.color (b : Building) :=
    | .shop => Color.Raylean.purple | .factory => Color.Raylean.green - /-- Vehicle is synonymous with person in this game -/ - structure Vehicle where + structure Peep where home : Nat work : Nat pos : Nat3
  • @@ -132,8 +129,13 @@ def dz : Vector Int 24 :=
    def 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⟩ - def Point.empty : Point := - ⟨.replicate 24 .none, .replicate 24 .none⟩ + instance : Lean.ToJson StdGen where + toJson x := Lean.toJson (x.1, x.2) + + instance : Lean.FromJson StdGen where + fromJson? j := do + let (x : Nat × Nat) ← Lean.fromJson? j + return ⟨x.1, x.2⟩ instance [BEq α] [Hashable α] [Lean.ToJson α] : Lean.ToJson (Std.HashSet α) where toJson := List.toJson ∘ Std.HashSet.toList
  • @@ -147,9 +149,9 @@ instance [BEq α] [Hashable α] [Lean.ToJson α] [Lean.ToJson β] : Lean.ToJson
    instance [BEq α] [Hashable α] [Lean.FromJson α] [Lean.FromJson β] : Lean.FromJson (Std.HashMap α β) where fromJson? j := .ofList <$> List.fromJson? j - -- TODO: routing table for each building, reverse grid + -- TODO: Money? Eh can do that later structure State where - rng : Nat + rng : StdGen speed : Nat day : Nat time : Nat
  • @@ -157,12 +159,14 @@ structure State where
    grid : Std.HashMap Nat3 Point buildings : Array Building dists : Array (Std.HashMap Nat3 Nat) + peeps : Array Peep occupied : Std.HashSet Nat3 - vehicles : Array Vehicle deriving Lean.ToJson, Lean.FromJson - makeLenses State - -- TODO open that namespace? + /-- 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]⟩ + `(modify fun s ↦ { s with $lval := $fn s.$field }) /-- Generate array of street names at compile time -/ elab "get_street_names" : term => do
  • @@ -179,64 +183,102 @@ theorem queue_dequeue_isSome_if_not_isEmpty {q : Std.Queue α} (h : ¬q.isEmpty)
    grind · grind - /-- Precompute distances to each destination using BFS -/ - def mkDist : StateM State Unit := do - let mut dists : Array (Std.HashMap Nat3 Nat) := #[] - let s ← get - for building in s.buildings do - -- TODO refactor this into its own func - let mut q : Std.Queue Nat3 := .enqueue building.entrance .empty - let mut dist : Std.HashMap Nat3 Nat := .ofList [(building.entrance, 0)] - while hq : ¬q.isEmpty do - let uq := q.dequeue?.get (queue_dequeue_isSome_if_not_isEmpty hq) - let u := uq.1 - q := uq.2 - let d := dist[u]! - if hs : s.grid.contains u then - for hi : i in List.range 24 do - let v := appd u i - match (s.grid[u]'hs).ein[i]'(by grind) with - | .low => - if !dist.contains v then - dist := dist.insert u (d + 1) - q := q.enqueue v - | .high => - if !dist.contains v then - dist := dist.insert v (d + 1) - q := q.enqueue v - if hs : s.grid.contains v then - match (s.grid[v]'hs).ein[i]'(by grind) with - | .high => - let v' := appd u i - if !dist.contains v' then - dist := dist.insert v' (d + 1) - q := q.enqueue v' - | _ => - pure () - | .none => - pure () - dists := dists.push dist - -- TODO update dists in state - - -- TODO + /-- Precompute distances to `start` using BFS -/ + def mkDist (g : Std.HashMap Nat3 Point) (start : Nat3) := Id.run do + let mut q := Std.Queue.enqueue start .empty + let mut dist := Std.HashMap.ofList [(start, 0)] + while hq : ¬q.isEmpty do + let uq := q.dequeue?.get (queue_dequeue_isSome_if_not_isEmpty hq) + let u := uq.1 + q := uq.2 + let d := dist[u]! + if hs : g.contains u then + for hi : i in List.range 24 do + let v := appd u i + match (g[u]'hs).ein[i]'(by grind) with + | .low => + if !dist.contains v then + dist := dist.insert u (d + 1) + q := q.enqueue v + | .high => + if !dist.contains v then + dist := dist.insert v (d + 1) + q := q.enqueue v + -- Try traveling another unit in direction `i` + if hs : g.contains v then + match (g[v]'hs).ein[i]'(by grind) with + | .high => + let v' := appd u i + if !dist.contains v' then + dist := dist.insert v' (d + 1) + q := q.enqueue v' + | _ => + pure () + | .none => + pure () + return dist + + /-- Precompute all distances -/ + def mkDists : StateM State Unit := do + modifyf dists (fun _ ↦ #[]) + for building in (← get).buildings do + modifyf dists (·.push <| mkDist (← get).grid building.entrance) + + /-- Generate a random nat in [0, n) (with a slight bias towards smaller numbers) + `randNat` is more sophisticated but doesn't bundle a bounds proof, so let's just use modulo for simplicity + -/ + def rand (n : Nat) (hn : 0 < n := by grind) : StateM State (Fin n) := do + let (ret, rng) := stdNext (← get).rng + modifyf rng (fun _ ↦ rng) + return ⟨ret % n, Nat.mod_lt ret hn⟩ + + /-- Shuffle an array using the Fisher-Yates algorithm -/ + def Array.shuffle (A : Array α) : StateM State (Array α) := do + let mut A' := A.toVector + for hi : i in [1:A'.size] do + let j ← rand (i + 1) + A' := A'.swap i j + return A'.toArray + + /-- Run one iteration of the game randomly -/ def tick : StateM State Unit := do - -- Randomize list of vehicles using Fisher-Yates + let peeps ← (← get).peeps.shuffle + for peep in peeps do + -- TODO -- For each vehicle, if has dest then look at dist table and iterate through all possible moves + -- If at dest then remove -- Cannot do a move if occupied currently or after this tick -- Do that move -- Set the new list of vehicles with the new position and direction (for animating) - modify <| over State.Lens.time (· + 1) + if 12 * 60 * 60 < (← get).time then + modifyf time (fun _ ↦ 0) + modifyf day (· + 1) + else + modifyf time (· + 1) def Nat3.toVector3 (p : Nat3) : Vector3 := ⟨p.x.toFloat / 10, p.y.toFloat / 10, p.z.toFloat / 10⟩ + /-- Draw the game state -/ 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 - s.origin.toVector3 + s / 2.0 - drawCubeV o s b.color - drawCubeWiresV o s .black + let size := b.size.toVector3 + let pos := b.pos.toVector3 - s.origin.toVector3 + 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 + -- 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 + | .none => + pure () + | .low => + + def getInput (stdin : IO.FS.Stream) := do IO.print "> "
  • @@ -249,6 +291,7 @@ def loadState (path : String) : IO State := do
    .ofExcept <| Lean.fromJson? json -- TODO: Build roads + -- TODO: rename roads def handleCmd (cmd : String) : StateT State IO Unit := do match cmd.split ' ' |>.toStringList with | ["s", path] =>
  • @@ -256,13 +299,16 @@ def handleCmd (cmd : String) : StateT State IO Unit := do
    | ["l", path] => set <| ← loadState path | ["v", speed] => - modify <| set State.Lens.speed <| String.toNat! speed + modifyf speed fun _ ↦ String.toNat! speed + | ["i"] => + IO.println s!"Population: {(← get).peeps.size}" | "b" :: variant :: dims => + -- TODO refactor into own function, check collisions, update dists 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), 0⟩) + modifyf buildings (·.push ⟨⟨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" | _ =>
  • @@ -302,8 +348,8 @@ def main : IO Unit := do
    setConfigFlags 0x00002004 initWindow screenWidth screenHeight "LeanTTD" setTargetFPS fps - _ ← gameLoop.run { - rng := 0 + gameLoop.run' { + rng := mkStdGen (← IO.rand 0 (2 ^ 32)) speed := 1 day := 0 time := 0
  • @@ -312,5 +358,5 @@ def main : IO Unit := do
    dists := #[] buildings := #[] occupied := .ofList [] - vehicles := #[] + peeps := #[] }
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.30.0 + leanprover/lean4:v4.31.0
• lens.patch (new)
  • @@ -0,0 +1,20 @@
    + diff --git a/Lens/Elab.lean b/Lens/Elab.lean + index 9d9c1bc..98a708d 100644 + --- a/Lens/Elab.lean + +++ b/Lens/Elab.lean + @@ -21,12 +21,9 @@ elab "makeLenses" structIdent:ident : command => do + let fieldNameIdent := mkIdent field.fieldName + let some decl := env.find? (field.projFn) + | throwErrorAt structIdent s!"Could not find project function {field.projFn}" + - let (some fieldTypeName, some fieldTypeArgs) := (← liftTermElabM (liftMetaM ( + - forallTelescope decl.type fun _ body + - => pure (body.getAppFn.constName?, body.getAppArgs.mapM (·.constName?))))) + - | throwErrorAt structIdent "Not a structure name" + - let d ← fieldTypeArgs.mapM fun argName => `($(mkIdent argName)) + - let fieldTypeNameIdent := Syntax.mkCApp fieldTypeName d + + let fieldTypeNameIdent : Term ← liftTermElabM <| liftMetaM <| + + forallTelescope decl.type fun _ body => + + Lean.PrettyPrinter.delab body + let lensName := mkIdent field.fieldName + let newVal := mkIdent <| Name.mkSimple "newVal" + let l ←
• raylean.patch
  • @@ -1,5 +1,5 @@
    diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c - index 902a945..7539506 100644 + index 902a945..bb36469 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,3 +19,37 @@ index 902a945..7539506 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) { + return IO_UNIT; + } + + +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; + +} + + + +lean_obj_res drawPoint3D(lean_obj_arg position, lean_obj_arg color) { + + DrawPoint3D(vector3_of_arg(position), color_of_arg(color)); + + return IO_UNIT; + +} + + + lean_obj_res drawCube(lean_obj_arg position, double width, double height, + 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 + --- a/lean/Raylean/Core.lean + +++ b/lean/Raylean/Core.lean + @@ -112,6 +112,12 @@ opaque drawText : (text : @& String) → (posX : Nat) → (posY : Nat) → (font + + /- Basic geometric 3D shapes drawing functions -/ + + +@[extern "drawLine3D"] + +opaque drawLine3D : (startPos : @& Vector3) → (endPos : @& Vector3) → (color : @& Color) → IO Unit + + + +@[extern "drawPoint3D"] + +opaque drawPoint3D : (position : @& Vector3) → (color : @& Color) → IO Unit + + + @[extern "drawCube"] + opaque drawCube : (position : @& Vector3) → (width : Float) → (height : Float) → (length : Float) → (color : @& Color) -> IO Unit +