Statement-level DSL for complete WGSL shaders. Supports variable declarations, assignments, loops, conditionals, and shader structure.

inductive Hesper.WGSL.Stmt : Type

WGSL Statements

• varDecl (name : String) (ty : WGSLType) (init : Option ((t : WGSLType) × Exp t)) : Stmt
• assign (name : String) (ty : WGSLType) (value : Exp ty) : Stmt
• assignIndex (arrName : String) (index : Exp (WGSLType.scalar ScalarType.u32)) (ty : WGSLType) (value : Exp ty) : Stmt
• assignIndexBuf (arrName : String) (bufIdx elemIdx : Exp (WGSLType.scalar ScalarType.u32)) (ty : WGSLType) (value : Exp ty) : Stmt
• forLoop (varName : String) (init : Exp (WGSLType.scalar ScalarType.u32)) (cond : Exp (WGSLType.scalar ScalarType.bool)) (update : Exp (WGSLType.scalar ScalarType.u32)) (body : List Stmt) : Stmt
• ifStmt (cond : Exp (WGSLType.scalar ScalarType.bool)) (thenBody elseBody : List Stmt) : Stmt
• exprStmt {t : WGSLType} (e : Exp t) : Stmt
• block (stmts : List Stmt) : Stmt
• varDeclLdV4U32 (n0 n1 n2 n3 bufName : String) (u32Idx : Exp (WGSLType.scalar ScalarType.u32)) : Stmt
• varDeclLdV4F32Shared (n0 n1 n2 n3 sharedName : String) (f32Idx : Exp (WGSLType.scalar ScalarType.u32)) : Stmt

structure Hesper.WGSL.StorageBuffer : Type

Storage buffer binding

• group : Nat
• binding : Nat
• name : String
• elemType : WGSLType
• readWrite : Bool

structure Hesper.WGSL.WorkgroupSize : Type

Workgroup size specification

• x : Nat
• y : Nat
• z : Nat

inductive Hesper.WGSL.BuiltinBinding : Type

Built-in variable bindings in compute shader

• workgroupId : BuiltinBinding
• localInvocationId : BuiltinBinding
• globalInvocationId : BuiltinBinding

structure Hesper.WGSL.BuiltinParam : Type

• builtin : BuiltinBinding
• name : String

structure Hesper.WGSL.FunctionParam : Type

Shader function parameter

• name : String
• ty : WGSLType
• builtin : Option BuiltinBinding

structure Hesper.WGSL.WorkgroupVar : Type

Workgroup variable declaration (shared memory)

• name : String
• type : WGSLType

instance Hesper.WGSL.instReprWorkgroupVar : Repr WorkgroupVar

Equations

• Hesper.WGSL.instReprWorkgroupVar = { reprPrec := Hesper.WGSL.instReprWorkgroupVar.repr }

def Hesper.WGSL.instReprWorkgroupVar.repr : WorkgroupVar → Nat → Std.Format

Equations

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

def Hesper.WGSL.instBEqWorkgroupVar.beq : WorkgroupVar → WorkgroupVar → Bool

Equations

• Hesper.WGSL.instBEqWorkgroupVar.beq { name := a, type := a_1 } { name := b, type := b_1 } = (a == b && a_1 == b_1)
• Hesper.WGSL.instBEqWorkgroupVar.beq x✝¹ x✝ = false

instance Hesper.WGSL.instBEqWorkgroupVar : BEq WorkgroupVar

Equations

• Hesper.WGSL.instBEqWorkgroupVar = { beq := Hesper.WGSL.instBEqWorkgroupVar.beq }

structure Hesper.WGSL.ComputeShader : Type

Complete compute shader structure

• extensions : List String
• diagnostics : List (String × String)
• structs : List StructDef
• buffers : List StorageBuffer
• workgroupVars : List WorkgroupVar
• workgroupSize : WorkgroupSize
• builtins : List BuiltinParam
• body : List Stmt

def Hesper.WGSL.BuiltinBinding.toWGSL : BuiltinBinding → String

Convert builtin binding to WGSL string

Equations

• Hesper.WGSL.BuiltinBinding.workgroupId.toWGSL = "workgroup_id"
• Hesper.WGSL.BuiltinBinding.localInvocationId.toWGSL = "local_invocation_id"
• Hesper.WGSL.BuiltinBinding.globalInvocationId.toWGSL = "global_invocation_id"

partial def Hesper.WGSL.Stmt.toWGSL (indent : Nat := 0) : Stmt → String

Convert statement to WGSL string with indentation

def Hesper.WGSL.StructDef.toWGSL (structDef : StructDef) : String

Generate WGSL struct definition

Equations

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

def Hesper.WGSL.ComputeShader.toWGSL (shader : ComputeShader) : String

Generate complete WGSL shader code from ComputeShader

Equations

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

def Hesper.WGSL.declareVar (name : String) (ty : WGSLType) (init : Option ((t : WGSLType) × Exp t) := none) : Stmt

Declare a variable with optional initial value

Equations

• Hesper.WGSL.declareVar name ty init = Hesper.WGSL.Stmt.varDecl name ty init

def Hesper.WGSL.assign {ty : WGSLType} (name : String) (value : Exp ty) : Stmt

Assign to a variable

Equations

• Hesper.WGSL.assign name value = Hesper.WGSL.Stmt.assign name ty value

def Hesper.WGSL.assignAt {ty : WGSLType} (arrName : String) (index : Exp (WGSLType.scalar ScalarType.u32)) (value : Exp ty) : Stmt

Assign to array element

Equations

• Hesper.WGSL.assignAt arrName index value = Hesper.WGSL.Stmt.assignIndex arrName index ty value

def Hesper.WGSL.forLoop (varName : String) (init : Exp (WGSLType.scalar ScalarType.u32)) (cond : Exp (WGSLType.scalar ScalarType.bool)) (update : Exp (WGSLType.scalar ScalarType.u32)) (body : List Stmt) : Stmt

For loop statement

Equations

• Hesper.WGSL.forLoop varName init cond update body = Hesper.WGSL.Stmt.forLoop varName init cond update body

def Hesper.WGSL.expr {t : WGSLType} (e : Exp t) : Stmt

Expression statement (e.g., function calls)

Equations

• Hesper.WGSL.expr e = Hesper.WGSL.Stmt.exprStmt e

def Hesper.WGSL.initArray {ty : WGSLType} (arrName : String) (count : Nat) (gen : Nat → Exp ty) : List Stmt

Initialize array elements with a generator function

Equations

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

def Hesper.WGSL.nestedMap2D {α : Type} (rows cols : Nat) (f : Nat → Nat → α) : List α

Nested loops for 2D iteration

Equations

• Hesper.WGSL.nestedMap2D rows cols f = List.foldl (fun (acc : List α) (i : Nat) => acc ++ List.map (fun (j : Nat) => f i j) (List.range cols)) [] (List.range rows)

def Hesper.WGSL.loop (varName : String) (start end_ step : Exp (WGSLType.scalar ScalarType.u32)) (body : Exp (WGSLType.scalar ScalarType.u32) → List Stmt) : Stmt

HOAS-style loop construct. Instead of requiring a string variable name, takes a function that receives the loop variable as an Exp and returns the loop body.

Example: loop "i" 0 n 1 (fun i => [...statements using i...])

Equations

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

def Hesper.WGSL.staticFor {α : Type} (items : List α) (f : α → List Stmt) : List Stmt

Compile-time iteration over a list, generating statements for each element. Similar to Haskell's staticFor - unrolls the loop at DSL compile time.

Example: staticFor [0, 1, 2, 3] (fun i => assignAt "arr" i someValue)

Equations

• Hesper.WGSL.staticFor items f = List.foldl (fun (acc : List Hesper.WGSL.Stmt) (item : α) => acc ++ f item) [] items

def Hesper.WGSL.staticForRange (start end_ : Nat) (f : Nat → List Stmt) : List Stmt

Helper to iterate over a range with a body function

Equations

• Hesper.WGSL.staticForRange start end_ f = Hesper.WGSL.staticFor (List.map (fun (x : Nat) => x + start) (List.range (end_ - start))) f

def Hesper.WGSL.staticForIndexed {α : Type} (items : List α) (f : Nat → α → List Stmt) : List Stmt

Helper to iterate with index and value from a list

Equations

• Hesper.WGSL.staticForIndexed items f = Hesper.WGSL.staticFor ((List.range items.length).zip items) fun (x : Nat × α) => match x with | (i, item) => f i item

def Hesper.WGSL.loadMatricesLeft {st : ScalarType} {m k : Nat} (arrName : String) (count : Nat) (bufferRef : String) (getOffset : Nat → Exp (WGSLType.scalar ScalarType.u32)) (stride : Exp (WGSLType.scalar ScalarType.u32)) : List Stmt

Load multiple matrices into an array variable

Equations

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

def Hesper.WGSL.loadMatricesRight {st : ScalarType} {k n : Nat} (arrName : String) (count : Nat) (bufferRef : String) (getOffset : Nat → Exp (WGSLType.scalar ScalarType.u32)) (stride : Exp (WGSLType.scalar ScalarType.u32)) : List Stmt

Load multiple matrices (right operand) into an array variable

Equations

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

def Hesper.WGSL.matrixMulAccGrid {st : ScalarType} {m k n tm tn : Nat} (axArrName bxArrName accArrName : String) : List Stmt

Perform multiply-accumulate on 2D grid of matrices

Equations

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

def Hesper.WGSL.storeMatricesResult {st : ScalarType} {m n tm tn : Nat} (arrName bufferRef : String) (getOffset : Nat → Nat → Exp (WGSLType.scalar ScalarType.u32)) (stride : Exp (WGSLType.scalar ScalarType.u32)) : List Stmt

Store multiple result matrices from array to buffer

Equations

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