Transformation plans and executable checking

This module resolves elementary-axis lengths for rearrange, repeat, and reduce. A composite input dimension may contain at most one axis whose length is not supplied or fixed by an anonymous numeric axis. The remaining length is inferred by exact division.

TransformPlan stores only the mathematical data consumed by semantics and lowering: a normalized pattern, a total axis-length function, and the physical output shape. Supplementary user input and partial assignments belong to the concrete checking algorithm and deliberately do not survive in the plan. This separation also permits elaborators to construct plans from symbolic Nat expressions without imitating the concrete inference procedure.

When a known product is zero and the input dimension is also zero, the missing factor is not uniquely determined. The certified checker rejects that case rather than relying on the reference implementation's accidental integer division by zero.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Check.SupplementaryLengths : Type

User-supplied lengths for named axes.

def TorchLean.Tensor.Internal.Check.SupplementaryLengths.names (lengths : SupplementaryLengths) : List String

Names in a supplementary-length list, preserving user order.

def TorchLean.Tensor.Internal.Check.SupplementaryLengths.lookup? (lengths : SupplementaryLengths) (name : String) : Option ℕ

Look up the first supplied length with the given name.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Check.PartialAxisLengths : Type

A possibly incomplete assignment of elementary-axis lengths.

def TorchLean.Tensor.Internal.Check.PartialAxisLengths.seed (supplementary : SupplementaryLengths) : PartialAxisLengths

Seed an assignment from anonymous literals and named supplementary lengths.

def TorchLean.Tensor.Internal.Check.PartialAxisLengths.set (lengths : PartialAxisLengths) (axis : AxisId) (length : ℕ) : PartialAxisLengths

Update one elementary-axis length.

def TorchLean.Tensor.Internal.Check.resolvedProduct (lengths : PartialAxisLengths) : List AxisId → Option ℕ

Multiply the resolved lengths of a list of elementary axes.

structure TorchLean.Tensor.Internal.Check.TransformPlan : Type

The semantic data of a checked transformation.

Axis lengths are total because all resolution obligations are discharged before a plan is constructed. This avoids exposing the checker's temporary Option-valued assignment to semantics, lowerings, or symbolic elaboration.

• normalization : CheckedNormalization

  Parsed and ellipsis-expanded transformation with structural proofs.

• axisLength : AxisId → ℕ

  Total length assignment for every logical elementary axis.

• output : Shape

  Physical output induced by grouped output axes.

def TorchLean.Tensor.Internal.Check.TransformPlan.normalized (plan : TransformPlan) : NormalizedTransform

The normalized transformation underlying a checked plan.

def TorchLean.Tensor.Internal.Check.TransformPlan.allAxes (plan : TransformPlan) : List AxisId

Every elementary axis relevant to the plan, with harmless cross-side repetition.

def TorchLean.Tensor.Internal.Check.TransformPlan.groupLength (plan : TransformPlan) (group : List AxisId) : ℕ

The product represented by one composite axis.

def TorchLean.Tensor.Internal.Check.TransformPlan.inferredInput (plan : TransformPlan) : Shape

Input dimensions reconstructed from resolved elementary-axis lengths.

def TorchLean.Tensor.Internal.Check.TransformPlan.inferredOutput (plan : TransformPlan) : Shape

Output dimensions reconstructed from resolved elementary-axis lengths.

def TorchLean.Tensor.Internal.Check.TransformPlan.literalAxesAgree (plan : TransformPlan) : Bool

Anonymous numeric axes retain their literal lengths.

structure TorchLean.Tensor.Internal.Check.TransformPlan.Valid (plan : TransformPlan) : Prop

The semantic facts certified for every transformation plan.

• normalization : plan.normalized.Valid

  The underlying parsed transformation satisfies all structural checks.

• literal_axes : plan.literalAxesAgree = true

  Every anonymous numeric axis retains the length written in the pattern.

• input_shape : plan.inferredInput = plan.normalized.input

  Resolved logical-axis lengths reconstruct the physical input shape.

• output_shape : plan.output = plan.inferredOutput

  The stored output shape is exactly the shape induced by the output groups.

structure TorchLean.Tensor.Internal.Check.CheckedTransform : Type

A transformation bundled with every invariant required by semantics and lowering.

• value : TransformPlan

  Total semantic plan produced by shape checking.

• valid : self.value.Valid

  Proof that all lengths and physical shapes agree with the normalized pattern.

def TorchLean.Tensor.Internal.Check.checkTransform (kind : TransformKind) (pattern : Syntax.TransformPattern) (inputShape : Shape) (supplementary : SupplementaryLengths := []) : Result CheckedTransform

Check a normalized transformation against concrete dimensions and supplied named-axis lengths.