Runtime Scalar Selection

Runtime commands may choose Lean Float, executable IEEE binary32, complex binary32, or exact real-number semantics. DType records that choice. FromFloat supplies the one additional operation needed by commands that construct values from host Float literals.

Model definitions remain polymorphic over the existing Context α interface. The runtime dtype does not replace that mathematical interface; it selects a concrete scalar type that satisfies it.

class TorchLean.Runtime.FromFloat (α : Type) : Type

Conversion from host Float constants into a selected runtime scalar type.

• ofFloat : Float → α

  Convert a host Float literal into this runtime scalar backend.

def TorchLean.Runtime.ofFloat {α : Type} [FromFloat α] (x : Float) : α

Generic host-float injection for TorchLean scalar backends.

@[implicit_reducible]

instance TorchLean.Runtime.instFromFloatFloat : FromFloat Float

Float is already the host literal type, so injection is identity.

@[implicit_reducible]

instance TorchLean.Runtime.instFromFloatIEEE32Exec : FromFloat Floats.IEEE754.IEEE32Exec

Inject host Float literals into the executable IEEE-754 binary32 backend.

@[implicit_reducible]

instance TorchLean.Runtime.instFromFloatDualOfZero {α : Type} [FromFloat α] [Zero α] : FromFloat (Runtime.Autograd.TorchLean.Dual α)

Inject host literals into the dual-number backend used by the runtime autograd engine.

We interpret a literal as a primal value with zero tangent/adjoint component.

@[implicit_reducible]

instance TorchLean.Runtime.instFromFloatComplexOfZero {α : Type} [FromFloat α] [Zero α] : FromFloat (Complex α)

Inject host literals into TorchLean's parametric complex scalar (imaginary part defaults to 0).

@[implicit_reducible, defaultInstance 100]

instance TorchLean.Runtime.instOfScientificOfFromFloat {α : Type} [FromFloat α] : OfScientific α

Allow numeric literals like 0.1 to elaborate to any TorchLean runtime scalar backend.

structure TorchLean.Runtime.Float32Config : Type

Configuration for the float32 dtype option.

We support both:

• proof-only float32 semantics (mode = .fp32, noncomputable), and
• executable IEEE-754 float32 semantics (mode = .ieee754Exec).

• mode : Floats.Float32Mode

  Which float32 semantics backend to use.

def TorchLean.Runtime.instReprFloat32Config.repr : Float32Config → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Runtime.instReprFloat32Config : Repr Float32Config

@[implicit_reducible]

instance TorchLean.Runtime.instDecidableEqFloat32Config : DecidableEq Float32Config

def TorchLean.Runtime.instDecidableEqFloat32Config.decEq (x✝ x✝¹ : Float32Config) : Decidable (x✝ = x✝¹)

inductive TorchLean.Runtime.DType : Type

Scalar type choice for runnable executables.

This is a runtime selection mechanism used by example programs; the core library itself is parametric in the scalar type α.

PyTorch Mapping

This corresponds loosely to choosing dtype= in PyTorch, but with additional "proof-only" variants:

• .float uses Lean's builtin Float (executable, but its IEEE-754 behavior is trusted),
• .float32 uses TorchLean's float32 model (either proof-only or executable),
• .complex uses TorchLean's parametric complex scalar over a float32 backend,
• .real uses ℝ (proof-only; not executable).

• float : DType
• float32 (cfg : Float32Config := { }) : DType
• complex (cfg : Float32Config) : DType
• real : DType

@[implicit_reducible]

instance TorchLean.Runtime.instReprDType : Repr DType

def TorchLean.Runtime.instReprDType.repr : DType → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Runtime.instDecidableEqDType : DecidableEq DType

def TorchLean.Runtime.instDecidableEqDType.decEq (x✝ x✝¹ : DType) : Decidable (x✝ = x✝¹)

def TorchLean.Runtime.DType.isExecutable : DType → Bool

Whether this dtype can be used in an executable (IO/#eval) context.

def TorchLean.Runtime.DType.log : DType → IO Unit

Log a short description of the chosen dtype to stdout.

def TorchLean.Runtime.DType.Internal.parseFloat32Mode (v : String) : Except String Floats.Float32Mode

Parse a float32 mode selector string into a Float32Mode.

def TorchLean.Runtime.DType.Internal.parseDTypeValue (v : String) : Except String DType

Parse a dtype selector string into a DType.

def TorchLean.Runtime.DType.parseAndStripWithDefault (args : List String) (default : DType) : Except String (DType × List String)

Parse and remove dtype flags from CLI arguments, using default when no dtype flags are provided.

This is the same parsing logic as parseAndStrip, but it lets higher-level runners choose a different default dtype depending on context (e.g. CUDA eager requires Float).

def TorchLean.Runtime.DType.parseAndStrip (args : List String) : Except String (DType × List String)

Parse and remove dtype flags from CLI arguments.

Supported flags:

• --dtype <value> or --dtype=<value>
• --float32-mode <mode> or --float32-mode=<mode>

The two flags are mutually exclusive.

def TorchLean.Runtime.DType.withRuntime (dt : DType) (k : {α : Type} → [Context α] → [DecidableEq Spec.Shape] → [ToString α] → [FromFloat α] → IO Unit) : IO (Except String Unit)

Run k under the scalar type selected by dt.

If dt is proof-only, this returns an error rather than trying to execute noncomputable code.

def TorchLean.Runtime.DType.withExec (dt : DType) (k : {α : Type} → [Context α] → [DecidableEq Spec.Shape] → [ToString α] → (Float → α) → IO Unit) : IO (Except String Unit)

Run k under the scalar type selected by dt, passing an explicit cast function Float → α.

This is a convenient shape for executables that construct tensors from Float lists.