Supported backend primitive types, and their relation to Idris primitives. The module contains a number of interfaces (`Primitive.Num`, `Primitive.Eq` etc.). These indicate what operations can be performed on primitive data in the backend. They are entirely distinct from the Idris interfaces `Prelude.Num` etc. but carry largely the same meaning. For example, primitive types satsifying `Primitive.Ord` have a notion of ordering.
import public Compiler.Xla.XlaData
interface Num : Type -> Type
interface Neg : Type -> Type
interface Abs : Type -> Type
interface Integral : Type -> Type
interface Fractional : Type -> Type
interface Eq : Type -> Type
interface Ord : Type -> Type
interface PrimitiveRW : Type -> Type -> Type
A `PrimitiveRW dtype idr` means that values of type `idr` can be used to construct backend
data with data type `dtype`.
PrimitiveRW PRED Bool
PrimitiveRW S32 Int32
PrimitiveRW U32 Nat
PrimitiveRW U64 Nat
PrimitiveRW F64 Double