TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Automatic

Automatic portfolios for built-in configured carriers #

These dependent matches inspect the already selected StoragePlan and add direct candidates when their proofs apply: byte tables for the byte carrier and the wide-limb kernels for the limb carrier. Word and wide carriers reuse the representation-independent structural portfolios.

Byte-table eligibility depends only on encoded width. Every table is certified against the same configured specification used by the structural portfolio.

source
def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Internal.byteAdd (format : FloatFormat) (width_le : format.bitWidth ≤ 8) :
ExecFloat.Backend.Certified Spec.add

Certified addition table for any configured descriptor that fits in one byte.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Internal.byteSub (format : FloatFormat) (width_le : format.bitWidth ≤ 8) :
    ExecFloat.Backend.Certified Spec.sub

    Certified subtraction table for any configured descriptor that fits in one byte.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Internal.byteMul (format : FloatFormat) (width_le : format.bitWidth ≤ 8) :
      ExecFloat.Backend.Certified Spec.mul

      Certified multiplication table for any configured descriptor that fits in one byte.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Internal.byteDiv (format : FloatFormat) (width_le : format.bitWidth ≤ 8) :
        ExecFloat.Backend.Certified Spec.div

        Certified division table for any configured descriptor that fits in one byte.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Internal.byteSqrt (format : FloatFormat) (width_le : format.bitWidth ≤ 8) :
          ExecFloat.Backend.Certified Spec.sqrt

          Certified square-root table for any configured descriptor that fits in one byte.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.Internal.byteFma (format : FloatFormat) (width_le : format.bitWidth ≤ 8) :
            ExecFloat.Backend.Certified Spec.fma

            Certified fused-multiply-add table for any configured descriptor that fits in one byte.

            Instances For

              Complete portfolios for automatically selected built-in carriers #

              source
              def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.automaticAddCandidates (format : FloatFormat) (plan : StoragePlan format) :
              ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.add)

              Addition candidates for the carrier selected by Configured.Code.

              Matching Code plan before inspecting plan is important for parameterized public types. Typeclass discrimination does not unfold an arbitrary forKnownWidth expression far enough to discover an instance whose head mentions .byte directly. This dependent match makes the byte table available after the built-in carrier instance has already been selected.

              Instances For
                source
                def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.automaticSubCandidates (format : FloatFormat) (plan : StoragePlan format) :
                ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sub)

                Subtraction candidates for the automatically selected built-in carrier.

                Instances For
                  source
                  def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.automaticMulCandidates (format : FloatFormat) (plan : StoragePlan format) :
                  ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.mul)

                  Multiplication candidates for the automatically selected built-in carrier.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.automaticDivCandidates (format : FloatFormat) (plan : StoragePlan format) :
                    ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.div)

                    Division candidates for the automatically selected built-in carrier.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.automaticSqrtCandidates (format : FloatFormat) (plan : StoragePlan format) :
                      ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sqrt)

                      Square-root candidates for the automatically selected built-in carrier.

                      Instances For
                        source
                        def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.automaticFmaCandidates (format : FloatFormat) (plan : StoragePlan format) :
                        ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.fma)

                        Fused-multiply-add candidates for the automatically selected built-in carrier.

                        Instances For