Merge pull request #46 from paulcadman/session-2024-11-18

Session 2024-11-18

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
- "name": "«lean-raylib»",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "01f4969b6e861db6a99261ea5eadd5a9bb63011b",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "01f4969b6e861db6a99261ea5eadd5a9bb63011b",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
+ "name": "raylean",
  "lakeDir": ".lake"}

lakefile.lean

@@ -3,6 +3,8 @@ open System Lake DSL
 
 def optionUseBundle : Bool := get_config? bundle == some "on"
 
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ "01f4969b6e861db6a99261ea5eadd5a9bb63011b" -- Lean v4.14.0-rc1
+
 package «raylean» where
   srcDir := "lean"
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0-rc1

lean/ECS/Components.lean

@@ -100,7 +100,7 @@ It can also be used as:
 
 to delete every `a` component.
 --/
-inductive Not (α : Type) :=
+inductive Not (α : Type) where
   | Not
 
 

lean/Examples/BouncingBall.lean

@@ -20,7 +20,7 @@ structure Config where
   velocity : Vector2
   deriving Inhabited
 
-inductive Circle :=
+inductive Circle where
   | Circle
 
 -- Brings `World` and `initWorld` into scope

lean/Examples/JessicaCantSwim.lean

@@ -50,7 +50,7 @@ def main : IO Unit := do
     let keys ← getKeys
     let emits := game.emit
     let events: List Types.Msg := List.map (λ key => Types.Msg.Key key) keys
-    game := game.step delta (List.join [events, emits])
+    game := game.step delta (List.flatten [events, emits])
     let drawings := game.view
     let ⟨ ⟨ ox, oy ⟩, ⟨ tx, ty ⟩, r, z ⟩ := game.camera
     renderFrame do

lean/Examples/JessicaCantSwim/Game.lean

@@ -45,7 +45,7 @@ private def Game.update (game: Game) (msg: Types.Msg): Game :=
   }
 
 def Game.view (game: Game): List Draw.Draw :=
-  List.join [
+  List.flatten [
     -- Add your new Model here:
     game.wetsand.view,
     game.shells.view,
@@ -55,7 +55,7 @@ def Game.view (game: Game): List Draw.Draw :=
   ]
 
 def Game.emit (game: Game): List Types.Msg :=
-  List.join [
+  List.flatten [
     -- Add your new Model here:
     game.ocean.emit,
     game.wetsand.emit,

lean/Examples/Selector.lean

@@ -68,20 +68,20 @@ structure DemoRenderInfo where
 
 /-- Construct a DemoRenderInfo for each Demo --/
 def demoRenderInfos : Array DemoRenderInfo :=
-  let f {n : Nat} (idx : Fin n) (demo : Demo) :=
+  let f (idx : Nat) (demo : Demo) :=
     let demoInfo := mkDemoInfo demo
     let yOffset := idx * optionHeight
     let rect : Rectangle :=
       { x := 0
       , y := yOffset.toFloat
       , width := screenWidth.toFloat
       , height := optionHeight.toFloat }
-    let color := if idx.val % 2 == 0 then lightSelectorColor else darkSelectorColor
+    let color := if idx % 2 == 0 then lightSelectorColor else darkSelectorColor
     let render := do
       drawRectangleRec rect color
       drawText demoInfo.title (Nat.div screenWidth 3) (yOffset + Nat.div optionHeight 2) textSize selectorTextColor
     let isClicked (pos : Vector2) := checkCollisionPointRec pos rect
-    {start := demoInfo.start, render, isClicked}
+    {start := demoInfo.start, render, isClicked : DemoRenderInfo}
   Demo.all.mapIdx f
 
 /-- Start the selector --/

lean/Raylean/Graphics2D/Image.lean

@@ -0,0 +1,47 @@
+import Raylean
+import Batteries
+
+open Raylean.Types
+
+structure Location where
+  x : Rat
+  y : Rat
+
+def Image (α : Type) : Type := Location → α
+
+def lift0 (a : α) : Image α := Function.const _ a
+
+def lift1 (f : α → β) : (Image α → Image β) := fun g => f ∘ g
+
+def lift2 (f : α → β → γ) : (Image α → Image β → Image γ) :=
+  fun ia ib => fun l => f (ia l) (ib l)
+
+def monochrome (a : α) := lift0 a
+
+def blend (a1 a2 : Color) : Color :=
+  if a1.a == 0 then a2 else a1
+
+def over [BEq α] [Inhabited α] (a1 a2 : α) : α :=
+  if a1 == default then a2 else a1
+
+def overi [BEq α] [Inhabited α] (i1 i2 : Image α) : Image α := lift2 over i1 i2
+
+def blendi (i1 i2 : Image Color) : Image Color := lift2 blend i1 i2
+
+def condi (c : Image Bool) (ia1 ia2 : Image α) : Image α :=
+  fun l => if c l then ia1 l else ia2 l
+
+def emptyImage : Image Color := monochrome Color.transparent
+
+def crop (c : Image Bool) (im : Image Color) : Image Color := condi c im emptyImage
+
+def transform (f : Location → Location) (i : Image Color) : Image Color := i ∘ f
+
+instance [i : Inhabited α] : Inhabited (Image α) where
+  default := monochrome i.default
+
+instance [BEq α] [Inhabited α] [Append α] : Append (Image α) where
+  append : Image α → Image α → Image α := overi
+
+instance : Append (Image Color) where
+  append : Image Color → Image Color → Image Color := blendi

lean/Raylean/Types.lean

@@ -80,6 +80,9 @@ def black       := { r:=0, g:=0, b:=0, a:=255 : Color }
 def magenta     := { r := 255, g := 0, b := 255, a := 255 : Color  }
 def transparent := { r:=0, g:=0, b:=0, a:=0 : Color }
 
+instance : Inhabited Color where
+ default := transparent
+
 namespace Raylean
 
 def lightgray  := { r := 200, g := 200, b := 200, a := 255 : Color  }