IR element types

An IR value has a tensor shape and an element type. These descriptors identify the element representation without choosing a device, storage buffer, or kernel. Binary and decimal descriptors reuse FloatLib's validated formats. A configured binary128 or custom binary format is not a separate IR constructor.

context preserves scalar-polymorphic Lean graphs: the caller chooses their element type through the existing Storage and Context instances. Captured mixed-dtype programs use explicit descriptors instead.

Named types provide an extension point for a frontend or backend with another representation. Describing a type does not supply its arithmetic implementation; an interpreter must register the corresponding semantics or reject execution.

inductive NN.IR.DType : Type

Device-independent element representation of a tensor value.

• context : DType

  Scalar type supplied by a homogeneous Lean graph's caller.

• bool : DType

  Boolean values, distinct from numeric zero/one tensors.

• integer (signed : Bool) (width : Option ℕ := none) : DType

  Signed or unsigned integers; none means unbounded, and a width must be positive.

• binary (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) : DType

  A validated FloatLib binary format, including its bias and exceptional-value encoding.

• decimal (format : FloatLib.Floats.Formats.DecimalInterchange.Format) : DType

  A validated FloatLib decimal interchange format.

• posit (bits : ℕ) : DType

  A Posit Standard encoding of at least two bits.

• rational : DType

  Exact rational values.

• real : DType

  Mathematical real values, for specification interpreters.

• complex (component : DType) : DType

  Real and imaginary components have the same explicitly described element type.

• named (name : Lean.Name) (parameters : Array ℕ := #[]) : DType

  An extension identified by a qualified name and static natural-number parameters.

@[instance_reducible]

instance NN.IR.instDecidableEqDType : DecidableEq DType

def NN.IR.instDecidableEqDType.decEq (x✝ x✝¹ : DType) : Decidable (x✝ = x✝¹)

def NN.IR.instReprDType.repr : DType → ℕ → Std.Format

@[instance_reducible]

instance NN.IR.instReprDType : Repr DType

@[instance_reducible]

instance NN.IR.instInhabitedDType : Inhabited DType

def NN.IR.DType.float16 : DType

IEEE binary16.

def NN.IR.DType.bfloat16 : DType

Brain floating point with eight exponent bits and seven fraction bits.

def NN.IR.DType.float32 : DType

IEEE binary32.

def NN.IR.DType.float64 : DType

IEEE binary64.

def NN.IR.DType.valid : DType → Bool

Whether parameters not already validated by FloatLib form a usable descriptor.

def NN.IR.DType.check (dtype : DType) : Except String Unit

Check descriptor parameters before accepting a graph or registering an implementation.

def NN.IR.DType.describe : DType → String

Compact type spelling for errors and graph displays, including custom format parameters.

@[instance_reducible]

instance NN.IR.DType.instToString : ToString DType

def NN.IR.DType.Internal.nameJson (name : Lean.Name) : Lean.Json

Preserve numeric and escaped name components, rather than parsing a display spelling.

def NN.IR.DType.Internal.name (value : Lean.Json) : Except String Lean.Name

Component arrays are lossless; qualified strings are also accepted from frontend producers.

def NN.IR.DType.Internal.name.parse : ℕ → List Char → Lean.Name → Option Lean.Name

@[irreducible]

def NN.IR.DType.Internal.depth : Lean.Json → ℕ

JSON nesting depth, computed without the partial printer or proof-only SizeOf code.

@[irreducible]

def NN.IR.DType.Internal.listDepth : List Lean.Json → ℕ

Maximum nesting among an array's entries.

@[irreducible]

def NN.IR.DType.Internal.treeDepth : (Std.DTreeMap.Internal.Impl String fun (x : String) => Lean.Json) → ℕ

Maximum nesting among an object's values; keys do not add a component level.

def NN.IR.DType.Internal.read : ℕ → Lean.Json → Except String DType

Decode nested components with a budget derived from the JSON structure, not a fixed depth.

def NN.IR.DType.toJson : DType → Lean.Json

Encode the complete element representation, including format bias and name components.

def NN.IR.DType.fromJson (value : Lean.Json) : Except String DType

Decode and validate a descriptor without selecting a numerical implementation.

theorem NN.IR.DType.fromJson_valid {value : Lean.Json} {dtype : DType} (h : fromJson value = Except.ok dtype) : dtype.valid = true

Successful decoding cannot introduce invalid element-type parameters.

@[instance_reducible]

instance NN.IR.DType.instToJson : Lean.ToJson DType

@[instance_reducible]

instance NN.IR.DType.instFromJson : Lean.FromJson DType