TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Instances

Capability instances for configured binary formats #

Representation-independent instances serve custom carriers. Higher-priority instances for Configured.Code expose byte tables after dependent elimination of the selected storage plan, and give the machine-word plans and the two-word wide formats a first-order entry point. When the structural candidate wins, a closed ExecFloat.Binary call can specialize that kernel to its descriptor.

The priorities encode capability preference, not numerical semantics: every candidate must supply the same refinement contract before it can be selected. Keeping this wiring in one module makes backend choice inspectable and prevents storage-specific instances from leaking through the rest of the configured API.

source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.addCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Add (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.subCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Sub (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.mulCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Mul (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.divCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Div (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.sqrtCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Sqrt (Family format code plan)
source
@[instance_reducible, instance 100]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.fmaCapability (format : FloatFormat) (plan : StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (Model format) code] [planning : ExecFloat.Backend.PolicyFor (Family format code plan)] :
ExecFloat.Fma (Family format code plan)

Higher-priority built-in-carrier instances match Code plan before inspecting the plan. This works for every statically computed precision, including a forKnownWidth expression that has not yet reduced to a storage constructor during typeclass indexing. The dependent candidate helpers then add direct byte tables exactly when the selected plan is .byte.

Families with a custom carrier continue to use the representation-independent instances above.

First-order entry points #

A machine-word or pair plan calls its structural kernel directly only when that candidate wins against the generic kernel under the policy in scope. Otherwise it executes the memoized selection. This includes tiny formats stored in a larger word: their FMA and square-root costs can favor the generic kernel. Byte tables and limb candidates always enter through selection.

The guard stays inside execute so closed callers can specialize the selected kernel. A match around the capability record would prevent the compiler from reducing the projection before kernel specialization. The proofs below unfold candidate selection, including the choice between word and fixed-limb square root and FMA; numerical equivalence alone does not justify a route.

source
@[instance_reducible, always_inline, instance 200]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticAddCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
ExecFloat.Add (Family format (Code plan) plan)
source
@[instance_reducible, always_inline, instance 200]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticSubCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
ExecFloat.Sub (Family format (Code plan) plan)
source
@[instance_reducible, always_inline, instance 200]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticMulCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
ExecFloat.Mul (Family format (Code plan) plan)
source
@[instance_reducible, always_inline, instance 200]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticDivCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
ExecFloat.Div (Family format (Code plan) plan)
source
@[instance_reducible, always_inline, instance 200]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticSqrtCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
ExecFloat.Sqrt (Family format (Code plan) plan)
source
@[instance_reducible, always_inline, instance 200]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.automaticFmaCapability (format : FloatFormat) (plan : StoragePlan format) [planning : ExecFloat.Backend.PolicyFor (Family format (Code plan) plan)] :
ExecFloat.Fma (Family format (Code plan) plan)

Closed limb plans expose their concrete carrier during typeclass indexing. These instances forward to the automatic portfolios so ExecFloat.BinaryLimbs retains the policy in scope, its certified candidates, and the generic fallback.

source
@[instance_reducible, instance 900]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbCodec (format : FloatFormat) (width_gt : 128 < format.bitWidth) :
ExecFloat.ModelCodec (StoragePlan.limbs width_gt) (Model format) (Model.WideLimb.Value format)

The canonical lossless codec for the concrete limb carrier.

Keep this below codecForPlan: ModelCodec.Code is an output parameter, so unresolved codec goals must try the generic plan before the concrete limb carrier. This preserves inference for conversions between definitionally equal descriptors such as Binary.format 8 23 and binary32.

source
@[instance_reducible, always_inline, instance 210]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbAddCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
ExecFloat.Add (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

Policy-selected addition for the concrete limb carrier.

source
@[instance_reducible, always_inline, instance 210]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbSubCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
ExecFloat.Sub (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

Policy-selected subtraction for the concrete limb carrier.

source
@[instance_reducible, always_inline, instance 210]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbMulCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
ExecFloat.Mul (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

Policy-selected multiplication for the concrete limb carrier.

source
@[instance_reducible, always_inline, instance 210]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbDivCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
ExecFloat.Div (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

Policy-selected division for the concrete limb carrier.

source
@[instance_reducible, always_inline, instance 210]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbSqrtCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
ExecFloat.Sqrt (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

Policy-selected square root for the concrete limb carrier.

source
@[instance_reducible, always_inline, instance 210]
instance FloatLib.Floats.Formats.BinaryInterchange.Configured.limbFmaCapability (format : FloatFormat) (width_gt : 128 < format.bitWidth) [planning : ExecFloat.Backend.PolicyFor (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))] :
ExecFloat.Fma (Family format (Model.WideLimb.Value format) (StoragePlan.limbs width_gt))

Policy-selected fused multiply-add for the concrete limb carrier.