Use Raylean and Raylean.Type namespaces

funexists · Sep 3, 2024 · ef188ef · ef188ef
1 parent 0c09e10
commit ef188ef
Show file tree

Hide file tree

Showing 11 changed files with 54 additions and 11 deletions.
diff --git a/lean/Examples/Camera2DPlatformer.lean b/lean/Examples/Camera2DPlatformer.lean
@@ -5,6 +5,9 @@ open Types
 
 namespace Camera2DPlatformer
 
+open Raylean
+open Raylean.Types
+
 def screenWidth : Nat := 800
 def screenHeight : Nat := 450
 def fps : Nat := 60

diff --git a/lean/Examples/Camera2DPlatformer/Types.lean b/lean/Examples/Camera2DPlatformer/Types.lean
@@ -3,6 +3,8 @@ import Lens
 
 namespace Types
 
+open Raylean.Types
+
 structure Player where
   position : Vector2
   speed : Float

diff --git a/lean/Examples/Camera3D.lean b/lean/Examples/Camera3D.lean
@@ -2,6 +2,9 @@ import «Raylean»
 
 namespace Camera3D
 
+open Raylean
+open Raylean.Types
+
 private def screenWidth : Nat := 1000
 private def screenHeight : Nat := 600
 private def fps : Nat := 120

diff --git a/lean/Examples/InputKeys.lean b/lean/Examples/InputKeys.lean
@@ -2,6 +2,9 @@ import «Raylean»
 
 namespace InputKeys
 
+open Raylean
+open Raylean.Types
+
 private def screenWidth : Nat := 800
 private def screenHeight : Nat := 450
 

diff --git a/lean/Examples/JessicaCantSwim.lean b/lean/Examples/JessicaCantSwim.lean
@@ -9,6 +9,9 @@ import Examples.JessicaCantSwim.Game
 
 namespace JessicaCantSwim
 
+open Raylean
+open Raylean.Types
+
 def getKeys: IO (List Keys.Keys) := do
   let mut keys := #[]
   if (← isKeyDown Key.down)

diff --git a/lean/Examples/Selector.lean b/lean/Examples/Selector.lean
@@ -5,6 +5,9 @@ import Examples.Elab
 
 namespace Selector
 
+open Raylean
+open Raylean.Types
+
 /-- Demos supported in the selector --/
 inductive Demo where
   | jessica

diff --git a/lean/Examples/Window.lean b/lean/Examples/Window.lean
@@ -2,6 +2,9 @@ import «Raylean»
 
 namespace Window
 
+open Raylean.Types
+open Raylean
+
 def screenWidth : Nat := 800
 def screenHeight : Nat := 600
 

diff --git a/lean/Raylean/Core.lean b/lean/Raylean/Core.lean
@@ -1,5 +1,9 @@
 import «Raylean».Types
 
+namespace Raylean
+
+open Raylean.Types
+
 /- Window-related functions -/
 
 @[extern "initWindow"]
@@ -111,20 +115,9 @@ opaque drawCubeWires : (position : Vector3) → (width : Float) → (height : Fl
 @[extern "drawGrid"]
 opaque drawGrid : (slices : Nat) → (spacing : Float) → IO Unit
 
-@[extern "image_width"]
-opaque Image.width (image : @& Image) : Nat
-
-@[extern "image_height"]
-opaque Image.height (image : @& Image) : Nat
 @[extern "loadImage"]
 opaque loadImage : (resourceName : @& String) -> IO Image
 
-@[extern "texture2d_width"]
-opaque Texture2D.width (texture2d : @& Texture2D) : Nat
-
-@[extern "texture2d_height"]
-opaque Texture2D.height (texture2d : @& Texture2D) : Nat
-
 @[extern "loadTextureFromImage"]
 opaque loadTextureFromImage : (image : @& Image) -> IO Texture2D
 

diff --git a/lean/Raylean/Frame.lean b/lean/Raylean/Frame.lean
@@ -1,5 +1,9 @@
 import «Raylean».Core
 
+namespace Raylean
+
+open Raylean.Types
+
 def renderFrame [Monad m] [MonadLiftT IO m] (mkFrame : m Unit) : m Unit := do
     beginDrawing
     mkFrame

diff --git a/lean/Raylean/Math.lean b/lean/Raylean/Math.lean
@@ -1,7 +1,13 @@
 import Raylean.Types
 
+namespace Raylean
+
+namespace Math
+
 namespace Vector2
 
+open Raylean.Types
+
 def add (v1 : Vector2) (v2 : Vector2) : Vector2 :=
   { x := v1.x + v2.x, y := v1.y + v1.y : Vector2 }
 

diff --git a/lean/Raylean/Types.lean b/lean/Raylean/Types.lean
@@ -1,3 +1,7 @@
+namespace Raylean
+
+namespace Types
+
 structure Vector2 where
   x : Float
   y : Float
@@ -125,6 +129,22 @@ private opaque Texture2DP : NonemptyType
 def Texture2D := Texture2DP.type
 instance : Nonempty Texture2D := Texture2DP.property
 
+-- fields of Texture2D defined directly using a namespace must be in the same
+-- namespace as Texture2D
+@[extern "texture2d_width"]
+opaque Texture2D.width (texture2d : @& Texture2D) : Nat
+
+@[extern "texture2d_height"]
+opaque Texture2D.height (texture2d : @& Texture2D) : Nat
+
 private opaque ImageP : NonemptyType
 def Image := ImageP.type
 instance : Nonempty Image := ImageP.property
+
+-- fields of Image defined directly using a namespace must be in the same
+-- namespace as Image
+@[extern "image_width"]
+opaque Image.width (image : @& Image) : Nat
+
+@[extern "image_height"]
+opaque Image.height (image : @& Image) : Nat