TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Elab.Transform.View

Certified input views for transform fusion #

This module recovers one source tensor and one certified flat-index program from a visible chain of shape-only tensor operations. Rearrange, repeat, einsum, and reduction elaborators share this recognizer so every consumer uses the same coordinate semantics and dependent shape transport.

The metaprogramming result is an ordinary tuple rather than a new public plan type. Its coordinate map is the independent semantics, its flat map is the native executable representation, one proof connects those maps, and another identifies the visible tensor term with the flat pullback from its source.

source
def TorchLean.Tensor.Internal.Elab.Impl.checkedTransformShapes (checked : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)

Recover the physical input and output shapes stored in a checked transform.

Instances For
    source
    def TorchLean.Tensor.Internal.Elab.Impl.rearrangeAxesProof (checked hKind : Lean.Expr) :
    Lean.MetaM Lean.Expr

    Recover the input-axis subset proof certified by a rearrangement plan.

    Instances For
      source
      def TorchLean.Tensor.Internal.Elab.Impl.repeatAxesProof (checked hKind : Lean.Expr) :
      Lean.MetaM Lean.Expr

      Recover the input-axis subset proof certified by a repeat plan.

      Instances For
        source
        def TorchLean.Tensor.Internal.Elab.Impl.checkedProjection (checked hAxes : Lean.Expr) :
        Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr)

        Build the checked coordinate projection, its compact flat representation, and the theorem connecting them.

        Instances For
          source
          def TorchLean.Tensor.Internal.Elab.Impl.directFlatProjection (inputShape coordinateMap : Lean.Expr) :
          Lean.MetaM (Lean.Expr × Lean.Expr)

          Represent an arbitrary coordinate map by direct row-major linearization.

          Checked transformations use checkedProjection instead. This fallback keeps fusion general for user-defined Rep.pull and Rep.reindex inputs.

          Instances For
            source
            def TorchLean.Tensor.Internal.Elab.Impl.composeCertifiedProjections (outerMap outerFlatMap hOuterMap innerMap innerFlatMap hInnerMap : Lean.Expr) :
            Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr)

            Compose coordinate maps, flat maps, and their correctness certificates.

            Instances For
              source
              def TorchLean.Tensor.Internal.Elab.Impl.fusedTransformInput? (inputShape tensor : Lean.Expr) :
              Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

              Recover one composed output-to-source map from a leading shape-only pipeline.

              The recognized source may be an ordinary or already fused rearrangement or repeat, or a direct Rep.reindex or Rep.pull. Generated lets are preserved without duplicating their checked plans. The result includes equalities for both the visible tensor and the compact logical reference used by downstream denotational semantics.

              Instances For