Type-safe WGSL expressions using GADTs (Generalized Algebraic Data Types). The type parameter ensures that operations are only valid for compatible types.

inductive Hesper.WGSL.Exp : WGSLType → Type

Type-safe WGSL expressions. The type parameter t : WGSLType ensures compile-time type safety.

• litF32 : Float → Exp (WGSLType.scalar ScalarType.f32)
• litF16 : Float → Exp (WGSLType.scalar ScalarType.f16)
• litI32 : Int → Exp (WGSLType.scalar ScalarType.i32)
• litU32 : Nat → Exp (WGSLType.scalar ScalarType.u32)
• litBool : Bool → Exp (WGSLType.scalar ScalarType.bool)
• var {t : WGSLType} : String → Exp t
• add {t : WGSLType} : Exp t → Exp t → Exp t
• sub {t : WGSLType} : Exp t → Exp t → Exp t
• mul {t : WGSLType} : Exp t → Exp t → Exp t
• div {t : WGSLType} : Exp t → Exp t → Exp t
• mod {t : WGSLType} : Exp t → Exp t → Exp t
• neg {t : WGSLType} : Exp t → Exp t
• eq {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.bool)
• ne {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.bool)
• lt {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.bool)
• le {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.bool)
• gt {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.bool)
• ge {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.bool)
• and : Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool)
• or : Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool)
• not : Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool)
• shiftLeft : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• shiftRight : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• bitAnd : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• bitOr : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• bitXor : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• mulhiU32 : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)

  High 32 bits of a×b (u32 × u32 → u64, take hi). Core primitive for fastdiv (see llama.cpp's init_fastdiv_values / fastdiv in common.cuh). Lowered to PTX mul.hi.u32; WGSL path computes via u32(u64(a) * u64(b) >> 32).

• toF32 {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.f32)
• toF32U {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.f32)
• toF16 {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.f16)
• toI32 {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.i32)
• toU32 {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32)
• index {elemTy : WGSLType} {n : Nat} : Exp (elemTy.array n) → Exp (WGSLType.scalar ScalarType.u32) → Exp elemTy
• loadByteFromU32Buf {n : Nat} (bufName : String) (byteIdx : Exp (WGSLType.scalar ScalarType.u32)) : Exp (WGSLType.scalar ScalarType.u32)

  Byte-granularity load from a buffer declared as array<u32, n>. The buffer is addressed by byte index. On CUDA this lowers to one ld.global.u8 instruction (zero-extended into a u32 dest); on WGSL (where storage buffers lack byte granularity) it emulates the load via (buf[byteIdx >> 2] >> ((byteIdx & 3) * 8)) & 0xFF.

  Used by Q6_K matmul to avoid issuing one u32 load per scale byte.

• loadU16FromU32Buf {n : Nat} (bufName : String) (byteIdx : Exp (WGSLType.scalar ScalarType.u32)) : Exp (WGSLType.scalar ScalarType.u32)

  Halfword (16-bit) load from a buffer declared as array<u32, n>. Lowers to one ld.global.u16 on CUDA; emulated on WGSL via the same shift+mask pattern as loadByteFromU32Buf. Used to read fp16 block scales from Q6_K blocks in a single load.

• indexBuf {elemTy : WGSLType} {n : Nat} : Exp (elemTy.bufferArray n) → (bufIdx elemIdx : Exp (WGSLType.scalar ScalarType.u32)) → Exp elemTy

  Two-level indexing into a bufferArray elemTy n: pick the bufIdx-th buffer, then read element elemIdx from it. On CUDA this lowers to pointer-table load + ld.global. On WGSL to arr[bufIdx][elemIdx].

• vecX {st : ScalarType} : Exp (WGSLType.vec2 st) → Exp (WGSLType.scalar st)
• vecY {st : ScalarType} : Exp (WGSLType.vec2 st) → Exp (WGSLType.scalar st)
• vec3X {st : ScalarType} : Exp (WGSLType.vec3 st) → Exp (WGSLType.scalar st)
• vec3Y {st : ScalarType} : Exp (WGSLType.vec3 st) → Exp (WGSLType.scalar st)
• vec3Z {st : ScalarType} : Exp (WGSLType.vec3 st) → Exp (WGSLType.scalar st)
• vecZ {st : ScalarType} : Exp (WGSLType.vec3 st) → Exp (WGSLType.scalar st)
• vecW {st : ScalarType} : Exp (WGSLType.vec4 st) → Exp (WGSLType.scalar st)
• vec4X {st : ScalarType} : Exp (WGSLType.vec4 st) → Exp (WGSLType.scalar st)
• vec4Y {st : ScalarType} : Exp (WGSLType.vec4 st) → Exp (WGSLType.scalar st)
• vec4Z {st : ScalarType} : Exp (WGSLType.vec4 st) → Exp (WGSLType.scalar st)
• vec2 {st : ScalarType} : Exp (WGSLType.scalar st) → Exp (WGSLType.scalar st) → Exp (WGSLType.vec2 st)
• vec3 {st : ScalarType} : Exp (WGSLType.scalar st) → Exp (WGSLType.scalar st) → Exp (WGSLType.scalar st) → Exp (WGSLType.vec3 st)
• vec4 {st : ScalarType} : Exp (WGSLType.scalar st) → Exp (WGSLType.scalar st) → Exp (WGSLType.scalar st) → Exp (WGSLType.scalar st) → Exp (WGSLType.vec4 st)
• sqrt {t : WGSLType} : Exp t → Exp t
• abs {t : WGSLType} : Exp t → Exp t
• min {t : WGSLType} : Exp t → Exp t → Exp t
• max {t : WGSLType} : Exp t → Exp t → Exp t
• clamp {t : WGSLType} : Exp t → Exp t → Exp t → Exp t
• exp {t : WGSLType} : Exp t → Exp t
• exp2 {t : WGSLType} : Exp t → Exp t
• log {t : WGSLType} : Exp t → Exp t
• log2 {t : WGSLType} : Exp t → Exp t
• inverseSqrt {t : WGSLType} : Exp t → Exp t
• sin {t : WGSLType} : Exp t → Exp t
• cos {t : WGSLType} : Exp t → Exp t
• tan {t : WGSLType} : Exp t → Exp t
• asin {t : WGSLType} : Exp t → Exp t
• acos {t : WGSLType} : Exp t → Exp t
• atan {t : WGSLType} : Exp t → Exp t
• atan2 {t : WGSLType} : Exp t → Exp t → Exp t
• sinh {t : WGSLType} : Exp t → Exp t
• cosh {t : WGSLType} : Exp t → Exp t
• tanh {t : WGSLType} : Exp t → Exp t
• asinh {t : WGSLType} : Exp t → Exp t
• acosh {t : WGSLType} : Exp t → Exp t
• atanh {t : WGSLType} : Exp t → Exp t
• floor {t : WGSLType} : Exp t → Exp t
• ceil {t : WGSLType} : Exp t → Exp t
• round {t : WGSLType} : Exp t → Exp t
• trunc {t : WGSLType} : Exp t → Exp t
• fract {t : WGSLType} : Exp t → Exp t
• sign {t : WGSLType} : Exp t → Exp t
• saturate {t : WGSLType} : Exp t → Exp t
• pow {t : WGSLType} : Exp t → Exp t → Exp t
• step {t : WGSLType} : Exp t → Exp t → Exp t
• mix {t : WGSLType} : Exp t → Exp t → Exp t → Exp t
• smoothstep {t : WGSLType} : Exp t → Exp t → Exp t → Exp t
• fma {t : WGSLType} : Exp t → Exp t → Exp t → Exp t
• dot {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.f32)
• cross {st : ScalarType} : Exp (WGSLType.vec3 st) → Exp (WGSLType.vec3 st) → Exp (WGSLType.vec3 st)
• length {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.f32)
• distance {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.f32)
• normalize {t : WGSLType} : Exp t → Exp t
• faceForward {t : WGSLType} : Exp t → Exp t → Exp t → Exp t
• reflect {t : WGSLType} : Exp t → Exp t → Exp t
• refract {t : WGSLType} : Exp t → Exp t → Exp (WGSLType.scalar ScalarType.f32) → Exp t
• determinant {st : ScalarType} : Exp (WGSLType.mat2x2 st) → Exp (WGSLType.scalar st)
• determinant3 {st : ScalarType} : Exp (WGSLType.mat3x3 st) → Exp (WGSLType.scalar st)
• determinant4 {st : ScalarType} : Exp (WGSLType.mat4x4 st) → Exp (WGSLType.scalar st)
• transpose {st : ScalarType} : Exp (WGSLType.mat2x2 st) → Exp (WGSLType.mat2x2 st)
• transpose3 {st : ScalarType} : Exp (WGSLType.mat3x3 st) → Exp (WGSLType.mat3x3 st)
• transpose4 {st : ScalarType} : Exp (WGSLType.mat4x4 st) → Exp (WGSLType.mat4x4 st)
• all {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.bool)
• any {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.bool)
• select {t : WGSLType} : Exp (WGSLType.scalar ScalarType.bool) → Exp t → Exp t → Exp t
• arrayLength {t : WGSLType} : String → Exp (WGSLType.scalar ScalarType.u32)
• bitcast {fromTy toTy : WGSLType} : Exp fromTy → Exp toTy
• countLeadingZeros : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• countOneBits : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• countTrailingZeros : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• firstLeadingBit : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• firstLeadingBitSigned : Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• firstTrailingBit : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• reverseBits : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• extractBits : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• extractBitsSigned : Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.i32)
• insertBits : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• dpdx {t : WGSLType} : Exp t → Exp t
• dpdxCoarse {t : WGSLType} : Exp t → Exp t
• dpdxFine {t : WGSLType} : Exp t → Exp t
• dpdy {t : WGSLType} : Exp t → Exp t
• dpdyCoarse {t : WGSLType} : Exp t → Exp t
• dpdyFine {t : WGSLType} : Exp t → Exp t
• fwidth {t : WGSLType} : Exp t → Exp t
• fwidthCoarse {t : WGSLType} : Exp t → Exp t
• fwidthFine {t : WGSLType} : Exp t → Exp t
• call {t : WGSLType} : String → List ((t : WGSLType) × Exp t) → Exp t
• subgroupMatrixLoad {st : ScalarType} {m k : Nat} : String → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.subgroupMatrixLeft st m k)
• subgroupMatrixLoadRight {st : ScalarType} {k n : Nat} : String → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.subgroupMatrixRight st k n)
• subgroupMatrixMultiplyAccumulate {st : ScalarType} {m k n : Nat} : Exp (WGSLType.subgroupMatrixLeft st m k) → Exp (WGSLType.subgroupMatrixRight st k n) → Exp (WGSLType.subgroupMatrixResult st m n) → Exp (WGSLType.subgroupMatrixResult st m n)
• subgroupMatrixMultiplyAccumulateMixed {inSt outSt : ScalarType} {m k n : Nat} : Exp (WGSLType.subgroupMatrixLeft inSt m k) → Exp (WGSLType.subgroupMatrixRight inSt k n) → Exp (WGSLType.subgroupMatrixResult outSt m n) → Exp (WGSLType.subgroupMatrixResult outSt m n)

  Mixed-precision multiply-accumulate: A and B are inSt, C/D are outSt. Real NVIDIA cooperativeMatrix configs typically use (f16, f16) → f32 rather than the single-type variant above. WGSL + Dawn accept this form too, so we expose a separate constructor.

• subgroupMatrixStore {st : ScalarType} {m n : Nat} : String → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.subgroupMatrixResult st m n) → Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• subgroupMatrixZeroLeft {st : ScalarType} {m k : Nat} : Exp (WGSLType.subgroupMatrixLeft st m k)
• subgroupMatrixZeroRight {st : ScalarType} {k n : Nat} : Exp (WGSLType.subgroupMatrixRight st k n)
• subgroupMatrixZeroResult {st : ScalarType} {m n : Nat} : Exp (WGSLType.subgroupMatrixResult st m n)
• subgroupBroadcast {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32) → Exp t
• subgroupBroadcastFirst {t : WGSLType} : Exp t → Exp t
• subgroupShuffle {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32) → Exp t
• subgroupShuffleDown {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32) → Exp t
• subgroupShuffleUp {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32) → Exp t
• subgroupShuffleXor {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32) → Exp t
• subgroupAdd {t : WGSLType} : Exp t → Exp t
• subgroupExclusiveAdd {t : WGSLType} : Exp t → Exp t
• subgroupInclusiveAdd {t : WGSLType} : Exp t → Exp t
• subgroupMul {t : WGSLType} : Exp t → Exp t
• subgroupExclusiveMul {t : WGSLType} : Exp t → Exp t
• subgroupInclusiveMul {t : WGSLType} : Exp t → Exp t
• subgroupMin {t : WGSLType} : Exp t → Exp t
• subgroupMax {t : WGSLType} : Exp t → Exp t
• subgroupAnd {t : WGSLType} : Exp t → Exp t
• subgroupOr {t : WGSLType} : Exp t → Exp t
• subgroupXor {t : WGSLType} : Exp t → Exp t
• subgroupAll : Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool)
• subgroupAny : Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.scalar ScalarType.bool)
• subgroupBallot : Exp (WGSLType.scalar ScalarType.bool) → Exp (WGSLType.vec4 ScalarType.u32)
• subgroupElect : Exp (WGSLType.scalar ScalarType.bool)
• quadBroadcast {t : WGSLType} : Exp t → Exp (WGSLType.scalar ScalarType.u32) → Exp t
• quadSwapX {t : WGSLType} : Exp t → Exp t
• quadSwapY {t : WGSLType} : Exp t → Exp t
• quadSwapDiagonal {t : WGSLType} : Exp t → Exp t
• atomicAdd {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicAddU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicSub {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicSubU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicMin {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicMinU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicMax {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicMaxU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicExchange {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicExchangeU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicCompareExchangeWeak {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicCompareExchangeWeakU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicLoad {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32)
• atomicLoadU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32)
• atomicStore {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicStoreU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicAnd {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicAndU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicOr {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicOrU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• atomicXor {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicI32)) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32)
• atomicXorU {space : MemorySpace} : Exp (WGSLType.ptr space (WGSLType.scalar ScalarType.atomicU32)) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• storageBarrier : Exp (WGSLType.scalar ScalarType.u32)
• textureBarrier : Exp (WGSLType.scalar ScalarType.u32)
• workgroupUniformLoad {space : MemorySpace} {t : WGSLType} : Exp (WGSLType.ptr space t) → Exp t
• fieldAccess {x✝ : String} {ty : WGSLType} : Exp (WGSLType.struct x✝) → String → Exp ty
• structConstruct {x✝ : String} : String → List (String × (t : WGSLType) × Exp t) → Exp (WGSLType.struct x✝)
• textureSample {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.vec4 ScalarType.f32)
• textureLoad {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp (WGSLType.vec2 ScalarType.i32) → Exp (WGSLType.scalar ScalarType.i32) → Exp (WGSLType.vec4 ScalarType.f32)
• textureStore {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp (WGSLType.vec2 ScalarType.i32) → Exp (WGSLType.vec4 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• textureDimensions {x✝ : String} {t : WGSLType} : Exp (WGSLType.texture2D x✝) → Exp (WGSLType.vec2 ScalarType.u32)
• textureNumLayers {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp (WGSLType.scalar ScalarType.u32)
• textureNumLevels {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp (WGSLType.scalar ScalarType.u32)
• textureNumSamples {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp (WGSLType.scalar ScalarType.u32)
• textureSampleLevel {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.f32) → Exp (WGSLType.vec4 ScalarType.f32)
• textureSampleBias {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.f32) → Exp (WGSLType.vec4 ScalarType.f32)
• textureSampleGrad {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.vec4 ScalarType.f32)
• textureSampleCompare {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.f32) → Exp (WGSLType.scalar ScalarType.f32)
• textureGather {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.vec4 ScalarType.f32)
• textureSampleBaseClampToEdge {x✝ : String} : Exp (WGSLType.texture2D x✝) → Exp WGSLType.sampler → Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.vec4 ScalarType.f32)
• pack4x8snorm : Exp (WGSLType.vec4 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• pack4x8unorm : Exp (WGSLType.vec4 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• pack4xI8 : Exp (WGSLType.vec4 ScalarType.i32) → Exp (WGSLType.scalar ScalarType.u32)
• pack4xU8 : Exp (WGSLType.vec4 ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• pack4xI8Clamp : Exp (WGSLType.vec4 ScalarType.i32) → Exp (WGSLType.scalar ScalarType.u32)
• pack4xU8Clamp : Exp (WGSLType.vec4 ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• pack2x16snorm : Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• pack2x16unorm : Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• pack2x16float : Exp (WGSLType.vec2 ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• fmaF16x2 : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)

  Packed half2 fused multiply-add: dst = a*b + c, where each operand holds two f16 values packed into one u32 (low half = lane 0, high = 1). CUDA backend lowers to a single fma.rn.f16x2 PTX instruction. WGSL backend uses native vec2<f16> fma (requires enable f16;).

• unpack4x8snorm : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec4 ScalarType.f32)
• unpack4x8unorm : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec4 ScalarType.f32)
• unpack4xI8 : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec4 ScalarType.i32)
• unpack4xU8 : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec4 ScalarType.u32)
• unpack2x16snorm : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec2 ScalarType.f32)
• unpack2x16unorm : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec2 ScalarType.f32)
• unpack2x16float : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.vec2 ScalarType.f32)
• roundToI32 : Exp (WGSLType.scalar ScalarType.f32) → Exp (WGSLType.scalar ScalarType.u32)
• dot4I8Packed : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.i32)
• dot4U8Packed : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)
• subSatS8x4 : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)

  Packed signed-saturating subtract per byte (CUDA __vsubss4). Each lane interprets the u32 as 4 int8 values and computes clamp(a_byte - b_byte, -128, 127) per byte. PTX lowers to a single sub.sat.s8x4 instruction (sm_70+). On WGSL there is no native equivalent — it falls back to a per-byte sequence in the WGSL emitter (acceptable since WGSL is not the perf path for Q6_K). Used by Q6_K vec_dot to compute (vil | vih) - 32 per byte without cross-byte borrow.

• workgroupBarrier : Exp (WGSLType.scalar ScalarType.u32)
• warpBarrier : Exp (WGSLType.scalar ScalarType.u32)

  Warp-level barrier (CUDA __syncwarp()). On PTX backends lowers to bar.warp.sync 0xFFFFFFFF (much cheaper than block barrier). On WGSL backends falls back to workgroupBarrier() since WGSL lacks a dedicated warp-sync primitive — slightly over-syncs but preserves correctness.

• bufferAddr (bufName : String) (elemSize : Nat) : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u64)

  Raw u64 pointer to element idx of a global buffer, without dereferencing. CUDA-only. Used as the global-address operand for cpAsyncCgSharedGlobal. elemSize is the byte size of one element (typically 4 for u32/f32 buffers). WGSL backend has no notion of raw pointer Exps — only used in the CUDA path.

• sharedSymAddr (smemName : String) (elemSize : Nat) : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u32)

  Raw u32 byte-address of element idx in a shared-memory array. Lowers to mov.u32 + add.u32 on CUDA. Used as the smem-address operand for cpAsyncCgSharedGlobal. elemSize is byte size of one element (typically 4 for u32 smem arrays).

• cpAsyncCgSharedGlobal : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u64) → Nat → Exp (WGSLType.scalar ScalarType.u32)

  ── cp.async (sm_80+) ── async global→shared copy. .cg only supports bytes = 16. Use cpAsyncCaSharedGlobal for 4- or 8-byte transfers.

• cpAsyncCaSharedGlobal : Exp (WGSLType.scalar ScalarType.u32) → Exp (WGSLType.scalar ScalarType.u64) → Nat → Exp (WGSLType.scalar ScalarType.u32)

  cp.async.ca cache-all variant. Supports bytes ∈ {4, 8, 16}.

• cpAsyncCommitGroup : Exp (WGSLType.scalar ScalarType.u32)

  cp.async.commit_group — mark all preceding cp.async issues by this thread as one group.

• cpAsyncWaitGroup : Nat → Exp (WGSLType.scalar ScalarType.u32)

  cp.async.wait_group N — block until all but the most recent N committed groups have completed. N=0 waits for all.

def Hesper.WGSL.floatToWGSL (f : Float) : String

Convert Float to WGSL literal string with full precision. Uses scientific notation (e.g. 1.0e-7) when needed to preserve significant digits. FP32 has ~7 significant decimal digits.

Equations

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

partial def Hesper.WGSL.Exp.toWGSL {t : WGSLType} : Exp t → String

Code generation: convert expression to WGSL string

Operator overloading for ergonomic Exp construction

These instances let kernel code use +, -, *, /, %, <, ==, &&& (bit-and), ||| (bit-or), <<< (shift-left), >>> (shift-right) on Exp ty values directly, instead of Exp.add, Exp.mul, etc. Closes one of the major cognitive gaps when porting kernels from CUDA C++: q + k * scale reads the same in CUDA and ShaderM.

Exp.add q k style still works — the operator is sugar, not a replacement.

instance Hesper.WGSL.instHAddExp {t : WGSLType} : HAdd (Exp t) (Exp t) (Exp t)

Equations

• Hesper.WGSL.instHAddExp = { hAdd := Hesper.WGSL.Exp.add }

instance Hesper.WGSL.instHSubExp {t : WGSLType} : HSub (Exp t) (Exp t) (Exp t)

Equations

• Hesper.WGSL.instHSubExp = { hSub := Hesper.WGSL.Exp.sub }

instance Hesper.WGSL.instHMulExp {t : WGSLType} : HMul (Exp t) (Exp t) (Exp t)

Equations

• Hesper.WGSL.instHMulExp = { hMul := Hesper.WGSL.Exp.mul }

instance Hesper.WGSL.instHDivExp {t : WGSLType} : HDiv (Exp t) (Exp t) (Exp t)

Equations

• Hesper.WGSL.instHDivExp = { hDiv := Hesper.WGSL.Exp.div }

instance Hesper.WGSL.instHModExp {t : WGSLType} : HMod (Exp t) (Exp t) (Exp t)

Equations

• Hesper.WGSL.instHModExp = { hMod := Hesper.WGSL.Exp.mod }

instance Hesper.WGSL.instOfNatExpScalarU32 {n : Nat} : OfNat (Exp (WGSLType.scalar ScalarType.u32)) n

Numeric literals in Exp context: (0 : Exp (.scalar .u32)) becomes Exp.litU32 0, (0 : Exp (.scalar .i32)) becomes Exp.litI32 0. For f32 / f16 literals use Exp.litF32 0.0 directly (Lean's OfScientific interaction with Float-typed Exp is fragile; explicit wrapper avoids surprises).

Equations

• Hesper.WGSL.instOfNatExpScalarU32 = { ofNat := Hesper.WGSL.Exp.litU32 n }

instance Hesper.WGSL.instOfNatExpScalarI32 {n : Nat} : OfNat (Exp (WGSLType.scalar ScalarType.i32)) n

Equations

• Hesper.WGSL.instOfNatExpScalarI32 = { ofNat := Hesper.WGSL.Exp.litI32 (Int.ofNat n) }

instance Hesper.WGSL.instAndOpExpScalarU32 : AndOp (Exp (WGSLType.scalar ScalarType.u32))

Bit ops: &&& = bitwise AND, ||| = bitwise OR. Names match Lean's standard &&& / ||| for u32/i32.

Equations

• Hesper.WGSL.instAndOpExpScalarU32 = { and := Hesper.WGSL.Exp.bitAnd }

instance Hesper.WGSL.instOrOpExpScalarU32 : OrOp (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instOrOpExpScalarU32 = { or := Hesper.WGSL.Exp.bitOr }

instance Hesper.WGSL.instHShiftLeftExpScalarU32 : HShiftLeft (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32))

Shift operators using Lean's HShiftLeft/HShiftRight so x <<< n and x >>> n work uniformly with u32 expressions.

Equations

• Hesper.WGSL.instHShiftLeftExpScalarU32 = { hShiftLeft := Hesper.WGSL.Exp.shiftLeft }

instance Hesper.WGSL.instHShiftRightExpScalarU32 : HShiftRight (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHShiftRightExpScalarU32 = { hShiftRight := Hesper.WGSL.Exp.shiftRight }

instance Hesper.WGSL.instHAddExpScalarU32Nat : HAdd (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Mixed-arity arithmetic with Lean literals. Allows pos + 1 instead of Exp.add pos (Exp.litU32 1), 2 * dPair instead of Exp.mul (Exp.litU32 2) dPair, x * 0.5 (f32) instead of Exp.mul x (Exp.litF32 0.5), etc. Available for u32 + Nat (both directions) and f32 + Float (both directions). Matches the Hesper convention that kernel arithmetic keeps the typed Exp _ wrapper visible at every site so PTX lowering can pick the right instruction.

Equations

• Hesper.WGSL.instHAddExpScalarU32Nat = { hAdd := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) (n : Nat) => x.add (Hesper.WGSL.Exp.litU32 n) }

instance Hesper.WGSL.instHAddNatExpScalarU32 : HAdd Nat (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHAddNatExpScalarU32 = { hAdd := fun (n : Nat) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) => (Hesper.WGSL.Exp.litU32 n).add x }

instance Hesper.WGSL.instHSubExpScalarU32Nat : HSub (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHSubExpScalarU32Nat = { hSub := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) (n : Nat) => x.sub (Hesper.WGSL.Exp.litU32 n) }

instance Hesper.WGSL.instHSubNatExpScalarU32 : HSub Nat (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHSubNatExpScalarU32 = { hSub := fun (n : Nat) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) => (Hesper.WGSL.Exp.litU32 n).sub x }

instance Hesper.WGSL.instHMulExpScalarU32Nat : HMul (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHMulExpScalarU32Nat = { hMul := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) (n : Nat) => x.mul (Hesper.WGSL.Exp.litU32 n) }

instance Hesper.WGSL.instHMulNatExpScalarU32 : HMul Nat (Exp (WGSLType.scalar ScalarType.u32)) (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHMulNatExpScalarU32 = { hMul := fun (n : Nat) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) => (Hesper.WGSL.Exp.litU32 n).mul x }

instance Hesper.WGSL.instHDivExpScalarU32Nat : HDiv (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHDivExpScalarU32Nat = { hDiv := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) (n : Nat) => x.div (Hesper.WGSL.Exp.litU32 n) }

instance Hesper.WGSL.instHModExpScalarU32Nat : HMod (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Equations

• Hesper.WGSL.instHModExpScalarU32Nat = { hMod := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.u32)) (n : Nat) => x.mod (Hesper.WGSL.Exp.litU32 n) }

instance Hesper.WGSL.instHAddExpScalarF32Float : HAdd (Exp (WGSLType.scalar ScalarType.f32)) Float (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHAddExpScalarF32Float = { hAdd := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) (f : Float) => x.add (Hesper.WGSL.Exp.litF32 f) }

instance Hesper.WGSL.instHAddFloatExpScalarF32 : HAdd Float (Exp (WGSLType.scalar ScalarType.f32)) (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHAddFloatExpScalarF32 = { hAdd := fun (f : Float) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) => (Hesper.WGSL.Exp.litF32 f).add x }

instance Hesper.WGSL.instHSubExpScalarF32Float : HSub (Exp (WGSLType.scalar ScalarType.f32)) Float (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHSubExpScalarF32Float = { hSub := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) (f : Float) => x.sub (Hesper.WGSL.Exp.litF32 f) }

instance Hesper.WGSL.instHSubFloatExpScalarF32 : HSub Float (Exp (WGSLType.scalar ScalarType.f32)) (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHSubFloatExpScalarF32 = { hSub := fun (f : Float) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) => (Hesper.WGSL.Exp.litF32 f).sub x }

instance Hesper.WGSL.instHMulExpScalarF32Float : HMul (Exp (WGSLType.scalar ScalarType.f32)) Float (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHMulExpScalarF32Float = { hMul := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) (f : Float) => x.mul (Hesper.WGSL.Exp.litF32 f) }

instance Hesper.WGSL.instHMulFloatExpScalarF32 : HMul Float (Exp (WGSLType.scalar ScalarType.f32)) (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHMulFloatExpScalarF32 = { hMul := fun (f : Float) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) => (Hesper.WGSL.Exp.litF32 f).mul x }

instance Hesper.WGSL.instHDivExpScalarF32Float : HDiv (Exp (WGSLType.scalar ScalarType.f32)) Float (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHDivExpScalarF32Float = { hDiv := fun (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) (f : Float) => x.div (Hesper.WGSL.Exp.litF32 f) }

instance Hesper.WGSL.instHDivFloatExpScalarF32 : HDiv Float (Exp (WGSLType.scalar ScalarType.f32)) (Exp (WGSLType.scalar ScalarType.f32))

Equations

• Hesper.WGSL.instHDivFloatExpScalarF32 = { hDiv := fun (f : Float) (x : Hesper.WGSL.Exp (Hesper.WGSL.WGSLType.scalar Hesper.WGSL.ScalarType.f32)) => (Hesper.WGSL.Exp.litF32 f).div x }

instance Hesper.WGSL.instHShiftLeftExpScalarU32Nat : HShiftLeft (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Allow shifting by a Lean Nat literal: x >>> 3 instead of x >>> Exp.litU32 3. Same for <<<.

Equations

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

instance Hesper.WGSL.instHShiftRightExpScalarU32Nat : HShiftRight (Exp (WGSLType.scalar ScalarType.u32)) Nat (Exp (WGSLType.scalar ScalarType.u32))

Equations

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

Sentinel constants (Step 9f)

Common literals that appear repeatedly in attention / softmax kernels. Centralising them makes intent explicit and prevents typos like -1.0e30 vs -3.4e38 differing across files.

Two negInf flavours are exposed:

• negInf30 = -1.0e30. The hesper convention; matches existing V2-V11 call sites. Drop-in replacement for the existing literal.
• negInfHalf = -FLT_MAX / 2.0f ≈ -1.7e38. llama.cpp's convention. The "/2" leaves head-room so expf(x - max) doesn't overflow when max == -FLT_MAX. Use when porting from llama.cpp to keep arithmetic bit-identical.

def Hesper.WGSL.Exp.f32Zero : Exp (WGSLType.scalar ScalarType.f32)

Equations

• Hesper.WGSL.Exp.f32Zero = Hesper.WGSL.Exp.litF32 0.0

def Hesper.WGSL.Exp.f32One : Exp (WGSLType.scalar ScalarType.f32)

Equations

• Hesper.WGSL.Exp.f32One = Hesper.WGSL.Exp.litF32 1.0

def Hesper.WGSL.Exp.negInf30 : Exp (WGSLType.scalar ScalarType.f32)

Equations

• Hesper.WGSL.Exp.negInf30 = Hesper.WGSL.Exp.litF32 (-10e29)

def Hesper.WGSL.Exp.negInfHalf : Exp (WGSLType.scalar ScalarType.f32)

Equations

• Hesper.WGSL.Exp.negInfHalf = Hesper.WGSL.Exp.litF32 (-17014117e31)

def Hesper.WGSL.Exp.u32Zero : Exp (WGSLType.scalar ScalarType.u32)

u32 literal helpers — for slot-index and lane-mask constants that show up at every call site.

Equations

• Hesper.WGSL.Exp.u32Zero = Hesper.WGSL.Exp.litU32 0

def Hesper.WGSL.Exp.u32One : Exp (WGSLType.scalar ScalarType.u32)

Equations

• Hesper.WGSL.Exp.u32One = Hesper.WGSL.Exp.litU32 1

def Hesper.WGSL.«term_<ᵉ_» : Lean.TrailingParserDescr

Comparison operators on Exp. Cannot reuse Lean's < / == because those resolve to Bool, not Exp (.scalar .bool). Unicode suffix ᵉ ("e" for Exp) keeps the operator visually similar to CUDA C++ while signalling that the result is an Exp Bool, not a Lean Bool.

Usage: kPos <ᵉ splitEnd instead of Exp.lt kPos splitEnd.

Equations

• Hesper.WGSL.«term_<ᵉ_» = Lean.ParserDescr.trailingNode `Hesper.WGSL.«term_<ᵉ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᵉ ") (Lean.ParserDescr.cat `term 51))

def Hesper.WGSL.«term_≤ᵉ_» : Lean.TrailingParserDescr

Equations

• Hesper.WGSL.«term_≤ᵉ_» = Lean.ParserDescr.trailingNode `Hesper.WGSL.«term_≤ᵉ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ᵉ ") (Lean.ParserDescr.cat `term 51))

def Hesper.WGSL.«term_>ᵉ_» : Lean.TrailingParserDescr

Equations

• Hesper.WGSL.«term_>ᵉ_» = Lean.ParserDescr.trailingNode `Hesper.WGSL.«term_>ᵉ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >ᵉ ") (Lean.ParserDescr.cat `term 51))

def Hesper.WGSL.«term_≥ᵉ_» : Lean.TrailingParserDescr

Equations

• Hesper.WGSL.«term_≥ᵉ_» = Lean.ParserDescr.trailingNode `Hesper.WGSL.«term_≥ᵉ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ᵉ ") (Lean.ParserDescr.cat `term 51))

def Hesper.WGSL.«term_==ᵉ_» : Lean.TrailingParserDescr

Equations

• Hesper.WGSL.«term_==ᵉ_» = Lean.ParserDescr.trailingNode `Hesper.WGSL.«term_==ᵉ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ==ᵉ ") (Lean.ParserDescr.cat `term 51))

def Hesper.WGSL.«term_!=ᵉ_» : Lean.TrailingParserDescr

Equations

• Hesper.WGSL.«term_!=ᵉ_» = Lean.ParserDescr.trailingNode `Hesper.WGSL.«term_!=ᵉ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " !=ᵉ ") (Lean.ParserDescr.cat `term 51))