Module Sarek_real64

module Device = Spoc_core.Device
module Vector = Spoc_core.Vector
type real64 = float

A real64 value on the host is a binary64 float.

val of_float : float -> real64

Identity host conversions - the host always carries full binary64.

val to_float : real64 -> float

Host reference arithmetic

Plain binary64 operations on real64 values, for building references and doing host-side combination of results. These are NOT the device ops (those live in the two substrates); they are the "what a correct answer looks like" oracle.

val add : real64 -> real64 -> real64
val sub : real64 -> real64 -> real64
val mul : real64 -> real64 -> real64
val div : real64 -> real64 -> real64
val sqrt : real64 -> real64

Substrate selection

type substrate =
  1. | Native_f64
    (*

    native IEEE-754 binary64 (device has fp64)

    *)
  2. | Fallback_df64
    (*

    double-float emulation (device lacks fp64)

    *)

The two concrete lowerings real64 can take on a device.

val string_of_substrate : substrate -> string
val substrate_for : ?force:substrate -> Device.t -> substrate

Substrate a device would use by default: native f64 iff it reports fp64 support, df64 otherwise. Pass ~force to override (used by tests to run the df64 fallback even on fp64-capable hardware, so both lowering paths are exercised everywhere).

val select : substrate -> native:'a -> fallback:'a -> 'a

Pick one of two per-substrate values (typically the two lowered kernel IRs, but works for anything).

Single-source kernels (palier B)

A %kernel.real64 ... kernel is authored ONCE over an abstract real64 vector element type and expands to the pair (native, fallback) - the same two lowered %kernel values palier A authored by hand. Each element is a (closure, kirc) pair; kernel_ir picks the one matching a device's substrate, ready to hand to Sarek.Execute.run_vectors.

val ir_of_kernel : ('a * ('b, 'c, 'd) Sarek.Kirc_types.kirc_kernel) -> Sarek_ir_types.kernel

Extract the lowered IR from one lowered kernel value.

val kernel_ir : substrate -> (('a * ('b, 'c, 'd) Sarek.Kirc_types.kirc_kernel) * ('e * ('f, 'g, 'h) Sarek.Kirc_types.kirc_kernel)) -> Sarek_ir_types.kernel

Pick the IR variant matching substrate from the (native, fallback) pair produced by %kernel.real64.

type real64_vector = {
  1. arg : Sarek.Execute.vector_arg;
  2. set : int -> float -> unit;
  3. get : int -> float;
  4. length : int;
}

Uniform host vectors

A real64_vector hides whether the underlying storage is a float64 vector (native path) or a df64 struct vector (fallback). Callers always read/write plain doubles; encoding/decoding to the df64 pair is done here. arg is the ready-to-pass kernel argument (the same physical vector run_vectors transfers to/from the device).

val create_vector : substrate -> int -> real64_vector

Create an n-element real64 vector in the storage matching substrate.

val vset : real64_vector -> int -> float -> unit
val vget : real64_vector -> int -> float
val vlength : real64_vector -> int

Substrate re-exports for kernel authors

The fallback kernel body pulls df64 ops in with let%sarek_include _ = ".../Sarek_df64.ml" and let open Sarek_df64 in; the native body uses Float64. Re-exported here for discoverability.

module Df64 = Sarek_df64
module Float64 = Sarek_float64.Float64