Greg ShuflinandClaude Fable 5.1
8104955c71
Lean runs main on a helper thread, which Cocoa rejects for video init; export LEAN_MAIN_USE_THREAD=0 from the justfile on macOS. Wait for the camera permission event before reading the camera format, since SDL grants access asynchronously. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
310 lines
10 KiB
Lean4
310 lines
10 KiB
Lean4
namespace SDL
|
||
|
||
-- All SDL errors are represented as strings, so we can just wrap them in a structure
|
||
structure SDLError where
|
||
toString : String
|
||
deriving Nonempty
|
||
|
||
instance : ToString SDLError := ⟨SDLError.toString⟩
|
||
|
||
abbrev SDLIO := EIO SDLError
|
||
|
||
@[inline, always_inline]
|
||
def SDLIO.toIO (x : SDLIO α) : IO α :=
|
||
x.adapt fun e => IO.userError s!"SDL Error: {e}"
|
||
|
||
instance : MonadLift SDLIO IO := ⟨SDLIO.toIO⟩
|
||
|
||
-- see https://wiki.libsdl.org/SDL3/SDL_InitFlags
|
||
def SDL_INIT_VIDEO : UInt32 := 0x00000020
|
||
def SDL_INIT_CAMERA: UInt32 := 0x00010000
|
||
def SDL_WINDOW_SHOWN : UInt32 := 0x00000004
|
||
def SDL_RENDERER_ACCELERATED : UInt32 := 0x00000002
|
||
def SDL_QUIT : UInt32 := 0x100
|
||
def SDL_EVENT_CAMERA_DEVICE_APPROVED : UInt32 := 0x1402
|
||
def SDL_EVENT_CAMERA_DEVICE_DENIED : UInt32 := 0x1403
|
||
|
||
def SDL_SCANCODE_W : UInt32 := 26
|
||
def SDL_SCANCODE_A : UInt32 := 4
|
||
def SDL_SCANCODE_S : UInt32 := 22
|
||
def SDL_SCANCODE_D : UInt32 := 7
|
||
def SDL_SCANCODE_LEFT : UInt32 := 80
|
||
def SDL_SCANCODE_RIGHT : UInt32 := 79
|
||
def SDL_SCANCODE_SPACE : UInt32 := 44
|
||
def SDL_SCANCODE_ESCAPE : UInt32 := 41
|
||
|
||
def SDL_MOUSEBUTTONDOWN : UInt32 := 0x401
|
||
def SDL_MOUSEBUTTONUP : UInt32 := 0x402
|
||
def SDL_MOUSEMOTION : UInt32 := 0x400
|
||
def SDL_BUTTON_LEFT : UInt32 := 1
|
||
def SDL_BUTTON_MIDDLE : UInt32 := 2
|
||
def SDL_BUTTON_RIGHT : UInt32 := 4
|
||
|
||
|
||
-- see SDL_Render.h, SDL_TextureAccess
|
||
def SDL_TEXTUREACCESS_STATIC : UInt32 := 0x0
|
||
def SDL_TEXTUREACCESS_STREAMING : UInt32 := 0x1
|
||
def SDL_TEXTUREACCESS_TARGET :UInt32 := 0x2
|
||
|
||
|
||
def SDL_ALPHA_OPAQUE_FLOAT: Float := 1.0
|
||
|
||
structure SDLRect where
|
||
x : Int32
|
||
y : Int32
|
||
w : Int32
|
||
h : Int32
|
||
deriving Repr
|
||
|
||
structure SDLFRect where
|
||
x : Float
|
||
y : Float
|
||
w : Float
|
||
h : Float
|
||
deriving Repr
|
||
|
||
@[extern "sdl_init"]
|
||
opaque init : UInt32 → IO UInt32
|
||
|
||
@[extern "sdl_ttf_init"]
|
||
opaque ttfInit : IO Bool
|
||
|
||
@[extern "sdl_mixer_init"]
|
||
opaque mixerInit : IO Bool
|
||
|
||
@[extern "sdl_quit"]
|
||
opaque quit : IO Unit
|
||
|
||
private opaque SDLWindow.nonemptyType : NonemptyType
|
||
def SDLWindow : Type := SDLWindow.nonemptyType.type
|
||
instance SDLWindow.instNonempty : Nonempty SDLWindow := SDLWindow.nonemptyType.property
|
||
|
||
@[extern "sdl_create_window"]
|
||
opaque createWindow : @& String → Int32 → Int32 → UInt32 → SDLIO SDLWindow
|
||
|
||
private opaque SDLRenderer.nonemptyType : NonemptyType
|
||
def SDLRenderer : Type := SDLRenderer.nonemptyType.type
|
||
instance SDLRenderer.instNonempty : Nonempty SDLRenderer := SDLRenderer.nonemptyType.property
|
||
|
||
@[extern "sdl_create_renderer"]
|
||
opaque createRenderer : @& SDLWindow → SDLIO SDLRenderer
|
||
|
||
@[extern "sdl_create_window_and_renderer"]
|
||
opaque createWindowAndRenderer : @& String -> Int32 -> Int32 -> UInt32 -> SDLIO (SDLWindow × SDLRenderer)
|
||
|
||
@[extern "sdl_set_render_draw_color"]
|
||
opaque setRenderDrawColor : @& SDLRenderer → UInt8 → UInt8 → UInt8 → UInt8 → SDLIO Int32
|
||
|
||
@[extern "sdl_set_render_draw_color_float"]
|
||
opaque setRenderDrawColorFloat : @& SDLRenderer → Float → Float → Float → Float → SDLIO Bool
|
||
|
||
@[extern "sdl_render_clear"]
|
||
opaque renderClear : @& SDLRenderer → SDLIO Int32
|
||
|
||
@[extern "sdl_render_present"]
|
||
opaque renderPresent : @& SDLRenderer → IO Unit
|
||
|
||
@[extern "sdl_render_fill_rect"]
|
||
opaque renderFillRect : @& SDLRenderer → @& SDLRect → SDLIO Int32
|
||
|
||
@[extern "sdl_delay"]
|
||
opaque delay : UInt32 → IO Unit
|
||
|
||
@[extern "sdl_poll_event"]
|
||
opaque pollEvent : IO UInt32
|
||
|
||
@[extern "sdl_get_ticks"]
|
||
opaque getTicks : IO UInt64
|
||
|
||
@[extern "sdl_get_key_state"]
|
||
opaque getKeyState : UInt32 → IO Bool
|
||
|
||
private opaque PixelFormat.nonemptyType : NonemptyType
|
||
def PixelFormat : Type := PixelFormat.nonemptyType.type
|
||
instance PixelFormat.instNonempty : Nonempty PixelFormat := PixelFormat.nonemptyType.property
|
||
|
||
-- make SDLTexture an opaque type, and make sure to tell Lean that it is nonempty
|
||
private opaque SDLTexture.nonemptyType : NonemptyType
|
||
def SDLTexture : Type := SDLTexture.nonemptyType.type
|
||
instance SDLTexture.instNonempty : Nonempty SDLTexture := SDLTexture.nonemptyType.property
|
||
|
||
private opaque SDLSurface.nonemptyType : NonemptyType
|
||
def SDLSurface : Type := SDLSurface.nonemptyType.type
|
||
instance SDLSurface.instNonempty : Nonempty SDLSurface := SDLSurface.nonemptyType.property
|
||
|
||
namespace SDLSurface
|
||
|
||
@[extern "sdl_Surface_get_format"]
|
||
opaque format : @& SDLSurface -> UInt32
|
||
|
||
@[extern "sdl_Surface_get_w"]
|
||
opaque w : @& SDLSurface -> Int32
|
||
|
||
@[extern "sdl_Surface_get_h"]
|
||
opaque h : @& SDLSurface -> Int32
|
||
|
||
@[extern "sdl_Surface_get_pitch"]
|
||
opaque pitch : @& SDLSurface -> Int32
|
||
|
||
end SDLSurface
|
||
|
||
@[extern "sdl_image_load"]
|
||
-- @& means "by reference"
|
||
opaque loadImage : (path : @& System.FilePath) → SDLIO SDLSurface
|
||
|
||
@[extern "sdl_create_texture"]
|
||
opaque createTexture (renderer: @& SDLRenderer) (pixelFormat: UInt32) (textureAccess: UInt32) (w: UInt32) (h: UInt32): SDLIO SDLTexture
|
||
|
||
@[extern "sdl_create_texture_from_surface"]
|
||
opaque createTextureFromSurface
|
||
(renderer : @& SDLRenderer) (surface : @& SDLSurface) : SDLIO SDLTexture
|
||
|
||
|
||
-- TODO handle SDLRect argument
|
||
@[extern "sdl_update_texture"]
|
||
opaque updateTexture (texture: @& SDLTexture) (pixels: @& ByteArray) (pitch: Int32): SDLIO Bool
|
||
|
||
-- Zero-copy optimization: updates a texture directly from an SDL_Surface's
|
||
-- pixel buffer, avoiding the intermediate ByteArray copy required by
|
||
-- updateTexture. This is not strictly faithful to the SDL_UpdateTexture C API
|
||
-- (which takes a generic void* for pixels), but is safe because the surface
|
||
-- is borrowed (@&) for the duration of the call, preventing the GC from
|
||
-- collecting the surface (and its pixel data) while the update is in progress.
|
||
@[extern "sdl_update_texture_from_surface"]
|
||
opaque updateTextureFromSurface (texture: @& SDLTexture) (surface: @& SDLSurface): SDLIO Bool
|
||
|
||
|
||
def loadImageTexture
|
||
(renderer : SDLRenderer) (path : System.FilePath)
|
||
: SDLIO SDLTexture := do
|
||
let surface <- SDL.loadImage path
|
||
createTextureFromSurface renderer surface
|
||
|
||
private opaque SDLFont.nonemptyType : NonemptyType
|
||
def SDLFont : Type := SDLFont.nonemptyType.type
|
||
instance SDLFont.instNonempty : Nonempty SDLFont := SDLFont.nonemptyType.property
|
||
|
||
@[extern "sdl_load_font"]
|
||
opaque loadFont : System.FilePath → UInt32 → SDLIO SDLFont
|
||
|
||
@[extern "sdl_render_entire_texture"]
|
||
opaque renderEntireTexture (renderer : @& SDLRenderer) (texture : @& SDLTexture) (x : Int64) (y : Int64) (w : Int64) (h : Int64) : SDLIO Int32
|
||
|
||
-- TODO renderTexture should work in terms of rects, replace this with renderTextureRect
|
||
@[extern "sdl_render_texture"]
|
||
opaque renderTexture (renderer : @& SDLRenderer) (texture : @& SDLTexture) (srcX : Int64) (srcY : Int64) (srcW : Int64) (srcH : Int64) (dstX : Int64) (dstY : Int64) (dstW : Int64) (dstH : Int64) : SDLIO Int32
|
||
|
||
@[extern "sdl_render_texture_rect"]
|
||
opaque renderTextureRect (renderer : @& SDLRenderer) (texture : @& SDLTexture) (sourceRect : @& SDLFRect) (destRect : @& SDLFRect): SDLIO Bool
|
||
|
||
@[extern "sdl_render_texture_fullscreen"]
|
||
opaque renderTextureFullscreen (renderer : @& SDLRenderer) (texture : @& SDLTexture) : SDLIO Bool
|
||
|
||
@[extern "sdl_get_texture_width"]
|
||
opaque getTextureWidth (texture : @& SDLTexture) : SDLIO Int64
|
||
|
||
@[extern "sdl_get_texture_height"]
|
||
opaque getTextureHeight (texture : @& SDLTexture) : SDLIO Int64
|
||
|
||
@[extern "sdl_text_to_surface"]
|
||
opaque textToSurface (renderer : @& SDLRenderer) (font : @& SDLFont) (message : @& String) (x : Int32) (y : Int32) (red : UInt8) (green : UInt8) (blue : UInt8) (alpha : UInt8) : SDLIO SDLSurface
|
||
|
||
-- Mouse support
|
||
@[extern "sdl_get_mouse_state"]
|
||
opaque getMouseStateRaw : SDLIO UInt64
|
||
|
||
@[extern "sdl_set_relative_mouse_mode"]
|
||
opaque setRelativeMouseMode (window : @& SDLWindow) (enabled : Bool) : SDLIO UInt32
|
||
|
||
def getMousePos : SDLIO (Int32 × Int32) := do
|
||
let packed ← getMouseStateRaw
|
||
let x := (packed >>> 32).toUInt32.toInt32
|
||
let y := ((packed >>> 16) &&& 0xFFFF).toUInt32.toInt32
|
||
return (x, y)
|
||
|
||
def isMousePressed (button : UInt32) : SDLIO Bool := do
|
||
let packed ← getMouseStateRaw
|
||
let buttons := (packed &&& 0xFFFF).toUInt32
|
||
return (buttons &&& button) != 0
|
||
|
||
def isLeftMousePressed : SDLIO Bool := isMousePressed SDL_BUTTON_LEFT
|
||
def isRightMousePressed : SDLIO Bool := isMousePressed SDL_BUTTON_RIGHT
|
||
def isMiddleMousePressed : SDLIO Bool := isMousePressed SDL_BUTTON_MIDDLE
|
||
|
||
|
||
-- SDL_mixer support
|
||
|
||
private opaque SDLMixer.nonemptyType : NonemptyType
|
||
def SDLMixer : Type := SDLMixer.nonemptyType.type
|
||
instance SDLMixer.instNonempty : Nonempty SDLMixer := SDLMixer.nonemptyType.property
|
||
@[extern "sdl_create_mixer"]
|
||
opaque createMixer : Unit → SDLIO SDLMixer
|
||
|
||
private opaque SDLTrack.nonemptyType : NonemptyType
|
||
def SDLTrack : Type := SDLTrack.nonemptyType.type
|
||
instance SDLTrack.instNonempty : Nonempty SDLTrack := SDLTrack.nonemptyType.property
|
||
@[extern "sdl_create_track"]
|
||
opaque createTrack : @& SDLMixer → SDLIO SDLTrack
|
||
|
||
private opaque SDLAudio.nonemptyType : NonemptyType
|
||
def SDLAudio : Type := SDLAudio.nonemptyType.type
|
||
instance SDLAudio.instNonempty : Nonempty SDLAudio := SDLAudio.nonemptyType.property
|
||
@[extern "sdl_load_audio"]
|
||
opaque loadAudio : @& SDLMixer → System.FilePath → SDLIO SDLAudio
|
||
|
||
@[extern "sdl_set_track_audio"]
|
||
opaque setTrackAudio : @& SDLTrack → @& SDLAudio → SDLIO Bool
|
||
|
||
@[extern "sdl_play_track"]
|
||
opaque playTrack : @& SDLTrack → SDLIO Bool
|
||
|
||
-- Webcam
|
||
|
||
@[extern "sdl_get_cameras"]
|
||
opaque getCameras : SDLIO (List UInt32)
|
||
|
||
private opaque SDLCamera.nonemptyType : NonemptyType
|
||
def SDLCamera : Type := SDLCamera.nonemptyType.type
|
||
instance SDLCamera.instNonempty : Nonempty SDLCamera := SDLCamera.nonemptyType.property
|
||
@[extern "sdl_open_camera"]
|
||
opaque openCamera : UInt32 -> SDLIO SDLCamera
|
||
|
||
-- cameraspec stuff
|
||
|
||
private opaque Colorspace.nonemptyType : NonemptyType
|
||
def Colorspace : Type := Colorspace.nonemptyType.type
|
||
instance Colorspace.instNonempty : Nonempty Colorspace := Colorspace.nonemptyType.property
|
||
|
||
opaque CameraSpec.nonemptyType : NonemptyType
|
||
def CameraSpec : Type := CameraSpec.nonemptyType.type
|
||
instance CameraSpec.instNonempty : Nonempty CameraSpec := CameraSpec.nonemptyType.property
|
||
|
||
namespace CameraSpec
|
||
|
||
@[extern "sdl_CameraSpec_get_width"]
|
||
opaque width : @& CameraSpec -> UInt32
|
||
|
||
@[extern "sdl_CameraSpec_get_height"]
|
||
opaque height : @& CameraSpec -> UInt32
|
||
|
||
@[extern "sdl_CameraSpec_get_framerate_numerator"]
|
||
opaque framerateNumerator : @& CameraSpec -> UInt32
|
||
|
||
@[extern "sdl_CameraSpec_get_framerate_denominator"]
|
||
opaque framerateDenominator : @& CameraSpec -> UInt32
|
||
|
||
end CameraSpec
|
||
|
||
|
||
@[extern "sdl_get_camera_format"]
|
||
opaque getCameraFormat : @& SDLCamera -> SDLIO CameraSpec
|
||
|
||
@[extern "sdl_acquire_camera_frame"]
|
||
opaque acquireCameraFrame : (camera : @& SDLCamera) → IO (Option SDLSurface)
|
||
-- TODO: support returning the timestampNS too
|
||
|
||
@[extern "sdl_release_camera_frame"]
|
||
opaque releaseCameraFrame (camera : @& SDLCamera) (frame: SDLSurface): IO Unit
|
||
|
||
end SDL
|