Add bindings for getScreenWidth and getScreenHeight

Changes

3 changed files (+57/-24)

• Main.lean
  • @@ -339,21 +339,21 @@ -- TODO update dists
    -- Add peeps def addRoad (start : Nat3) (dir length : Nat) (isHigh : Bool) : StateM State Unit := do - let name := - (if h : (← get).grid.contains start then - (← get).grid[start].name - else - street_names[rand street_names.size]) + -- let name := + -- (if h : (← get).grid.contains start then + -- (← get).grid[start].name + -- else + -- street_names[rand street_names.size]) let mut u := start - let newp : Point := ⟨name, - , .replicate 27 .none⟩ - for i in List.range length do - modifyf grid (fun g ↦ - if h : g.contains u then - g.modify u fun p ↦ { p with eout := p.eout.set! dir .low } - else - g.insert u ⟨ .⟩ - ) + -- let newp : Point := ⟨name, + -- , .replicate 27 .none⟩ + -- for i in List.range length do + -- modifyf grid (fun g ↦ + -- if h : g.contains u then + -- g.modify u fun p ↦ { p with eout := p.eout.set! dir .low } + -- else + -- g.insert u ⟨ .⟩ + -- ) def diff (a b : Nat) := if a < b then b - a else a - b
  • @@ -368,6 +368,7 @@ set <| ← loadState path
    | ["v", speed] => setf speed (String.toNat! speed) | ["i"] => + -- TODO IO.println s!"Population: {(← get).peeps.size}" | "b" :: variant :: dims => -- TODO refactor into own function, check collisions, update dists
  • @@ -375,7 +376,7 @@ 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 - addBuilding ⟨⟨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 =>
  • @@ -414,8 +415,7 @@ for (pos, pt) in s.grid do
    if (2 * pos.x + pos.z) % 20 == 0 then -- https://www.raylib.com/examples/core/loader.html?name=core_world_screen let pos2D ← getWorldToScreen (pos.toVector3Shift s) camera - -- TODO these numbers are wrong - let dir := pt.eout[4] != .none || pt.eout[19] != .none + let dir := pt.eout[di 1 0 0] != .none || pt.eout[di (-1) 0 0] != .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 27 do
  • @@ -452,8 +452,13 @@ projection := .perspective
    } let stdin ← IO.getStdin let mut task ← IO.asTask <| getInput stdin + let mut start : Option (Nat3 × Bool) := none while !(← windowShouldClose) do camera ← updateCamera camera .thirdPerson + if (← isMouseButtonPressed MouseButton.left) then do + let pos ← getMousePosition + if (← isMouseButtonPressed MouseButton.right) then do + let pos ← getMousePosition if ← IO.hasFinished task then let cmd ← (.ofExcept task.get) try
  • @@ -467,7 +472,7 @@ setf ticks 0
    else modifyf ticks (· + 1) renderFrame do - drawFPS (screenWidth - 100) 10 + drawFPS ((← getScreenWidth) - 100) 10 clearBackground Color.white renderWithCamera camera do let s ← get
• README.md
  • @@ -6,7 +6,7 @@ ## Building
    To build this using Nix (least painful trust me), just run `nix build`. - On NixOS you can also build this by hardcoding the directory of `libraylib.so` in `lakefile.toml` and running `lake build`, which can be much faster due to caching. + On NixOS you can also build this by hardcoding the directory of `libraylib.so` in `lakefile.toml` (for instance `moreLinkArgs = ["-L/nix/store/2ndddyrjb1ahx05kmsjqvzkagz1bdmpk-raylib-6.0/lib", "-lraylib"]`) and running `lake build`, which can be much faster due to caching. Otherwise, install Raylib and run `lake build` and hope for the best. It probably won't work, but you can give it a try.
• raylean.patch
  • @@ -1,5 +1,5 @@
    diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c - index 902a945..17da156 100644 + index 902a945..ab55a4b 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,7 +19,22 @@ +// }
    lean_obj_res initWindow(lean_obj_arg width, lean_obj_arg height, b_lean_obj_arg title) { - @@ -402,6 +402,20 @@ lean_obj_res beginMode3D(lean_obj_arg camera) { + @@ -336,6 +336,14 @@ lean_obj_res closeWindow(void) { + return IO_UNIT; + } + + +lean_obj_res getScreenWidth(void) { + + return lean_io_result_mk_ok(lean_uint32_to_nat(GetScreenWidth())); + +} + + + +lean_obj_res getScreenHeight(void) { + + return lean_io_result_mk_ok(lean_uint32_to_nat(GetScreenHeight())); + +} + + + lean_obj_res beginDrawing(void) { + BeginDrawing(); + return IO_UNIT; + @@ -402,6 +410,20 @@ lean_obj_res beginMode3D(lean_obj_arg camera) { return IO_UNIT; }
  • @@ -41,10 +56,23 @@ 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..908f271 100644 + index e0818b6..f84deda 100644 --- a/lean/Raylean/Core.lean +++ b/lean/Raylean/Core.lean - @@ -43,6 +43,9 @@ opaque beginMode3D : (camera : @& Camera3D) → IO Unit + @@ -15,6 +15,12 @@ opaque closeWindow : IO Unit + @[extern "windowShouldClose"] + opaque windowShouldClose : IO Bool + + +@[extern "getScreenWidth"] + +opaque getScreenWidth : IO Nat + + + +@[extern "getScreenHeight"] + +opaque getScreenHeight : IO Nat + + + /- Cursor-related functions -/ + + @[extern "disableCursor"] + @@ -43,6 +49,9 @@ opaque beginMode3D : (camera : @& Camera3D) → IO Unit @[extern "endMode3D"] opaque endMode3D : IO Unit
  • @@ -54,7 +82,7 @@ +
    /- Timing-related functions -/ @[extern "setTargetFPS"] - @@ -112,6 +115,12 @@ opaque drawText : (text : @& String) → (posX : Nat) → (posY : Nat) → (font + @@ -112,6 +121,12 @@ opaque drawText : (text : @& String) → (posX : Nat) → (posY : Nat) → (font /- Basic geometric 3D shapes drawing functions -/