GLFW Safe API

Safe GLFW bindings with automatic resource management using Lean.External.

This module provides a clean API for GLFW resources. All resources are automatically cleaned up by Lean's GC when they go out of scope.

Usage Example

import Hesper.GLFW
import Hesper.WebGPU.Device

def main : IO Unit := do
  -- Initialize GLFW
  withGLFW do
    -- Create window (automatically cleaned up when out of scope)
    let window ← createWindow 800 600 "Hesper Window"

    -- Get device
    let device ← getDevice

    -- Create surface (automatically cleaned up)
    let surface ← createSurface device window

    -- Get preferred format and configure
    let format ← getSurfacePreferredFormat surface
    configureSurface surface 800 600 format

    -- Create shader and pipeline (automatically cleaned up)
    let shader ← createShaderModule device shaderCode
    let pipeline ← createRenderPipeline device shader format

    -- Main render loop
    while !(← windowShouldClose window) do
      renderFrame device surface pipeline
      pollEvents

def Hesper.GLFW.withGLFW {α : Type} (action : IO α) : IO α

Initialize GLFW with automatic cleanup

Equations

• Hesper.GLFW.withGLFW action = do Hesper.GLFW.Internal.glfwInit tryFinally action Hesper.GLFW.Internal.glfwTerminate

def Hesper.GLFW.createWindow (width height : Nat) (title : String) : IO Window

Create a window. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.createWindow width height title = Hesper.GLFW.Internal.createWindow width.toUInt32 height.toUInt32 title

def Hesper.GLFW.windowShouldClose (window : Window) : IO Bool

Check if window should close

Equations

• Hesper.GLFW.windowShouldClose window = Hesper.GLFW.Internal.windowShouldClose window

def Hesper.GLFW.pollEvents : IO Unit

Poll for events

Equations

• Hesper.GLFW.pollEvents = Hesper.GLFW.Internal.pollEvents

def Hesper.GLFW.getKey (window : Window) (key : Key) : IO KeyAction

Get key state

Equations

• Hesper.GLFW.getKey window key = do let state ← Hesper.GLFW.Internal.windowGetKey window key.toNat.toUInt32 pure (Hesper.GLFW.KeyAction.fromNat state.toNat)

def Hesper.GLFW.createSurface (device : WebGPU.Device) (window : Window) : IO Surface

Create a surface. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.createSurface device window = Hesper.GLFW.Internal.createSurface device window

def Hesper.GLFW.configureSurface (surface : Surface) (width height format : Nat) : IO Unit

Configure surface dimensions and format

Equations

• Hesper.GLFW.configureSurface surface width height format = Hesper.GLFW.Internal.configureSurface surface width.toUInt32 height.toUInt32 format.toUInt32

def Hesper.GLFW.getSurfacePreferredFormat (surface : Surface) : IO Nat

Get preferred surface format

Equations

• Hesper.GLFW.getSurfacePreferredFormat surface = do let format ← Hesper.GLFW.Internal.getSurfacePreferredFormat surface pure format.toNat

def Hesper.GLFW.present (surface : Surface) : IO Unit

Present surface

Equations

• Hesper.GLFW.present surface = Hesper.GLFW.Internal.surfacePresent surface

def Hesper.GLFW.getCurrentTexture (surface : Surface) : IO Texture

Get current texture. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.getCurrentTexture surface = Hesper.GLFW.Internal.getCurrentTexture surface

def Hesper.GLFW.createTextureView (texture : Texture) : IO TextureView

Create texture view. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.createTextureView texture = Hesper.GLFW.Internal.createTextureView texture

def Hesper.GLFW.createCommandEncoder (device : WebGPU.Device) : IO CommandEncoder

Create command encoder. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.createCommandEncoder device = Hesper.GLFW.Internal.createCommandEncoder device

def Hesper.GLFW.beginRenderPass (encoder : CommandEncoder) (view : TextureView) : IO RenderPassEncoder

Begin render pass. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.beginRenderPass encoder view = Hesper.GLFW.Internal.beginRenderPass encoder view

def Hesper.GLFW.setPipeline (pass : RenderPassEncoder) (pipeline : RenderPipeline) : IO Unit

Set pipeline in render pass

Equations

• Hesper.GLFW.setPipeline pass pipeline = Hesper.GLFW.Internal.setRenderPipeline pass pipeline

def Hesper.GLFW.drawVertices (pass : RenderPassEncoder) (count : Nat) : IO Unit

Draw vertices in render pass

Equations

• Hesper.GLFW.drawVertices pass count = Hesper.GLFW.Internal.draw pass count.toUInt32

def Hesper.GLFW.endRenderPass (pass : RenderPassEncoder) : IO Unit

End render pass

Equations

• Hesper.GLFW.endRenderPass pass = Hesper.GLFW.Internal.endRenderPass pass

def Hesper.GLFW.finishEncoder (encoder : CommandEncoder) : IO CommandBuffer

Finish encoder and get command buffer. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.finishEncoder encoder = Hesper.GLFW.Internal.finishEncoder encoder

def Hesper.GLFW.submit (device : WebGPU.Device) (cmd : CommandBuffer) : IO Unit

Submit command buffer to GPU

Equations

• Hesper.GLFW.submit device cmd = Hesper.GLFW.Internal.submitCommand device cmd

def Hesper.GLFW.createShaderModule (device : WebGPU.Device) (code : String) : IO ShaderModule

Create shader module. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.createShaderModule device code = Hesper.GLFW.Internal.createShaderModule device code

def Hesper.GLFW.createRenderPipeline (device : WebGPU.Device) (shader : ShaderModule) (format : Nat) : IO RenderPipeline

Create render pipeline. Automatically cleaned up by GC.

Equations

• Hesper.GLFW.createRenderPipeline device shader format = Hesper.GLFW.Internal.createRenderPipeline device shader format.toUInt32

def Hesper.GLFW.renderFrame (device : WebGPU.Device) (surface : Surface) (pipeline : RenderPipeline) : IO Unit

Render a single frame

Equations

• One or more equations did not get rendered due to their size.