Checked parse_shape

parse_shape matches one pattern position to each physical tensor dimension and returns the lengths of named positions in source order. An underscore or an ellipsis-expanded position is skipped. Unit and positive anonymous axes are accepted only when their literal length agrees with the corresponding physical dimension.

The checker returns the existing ordered SupplementaryLengths type. No separate plan structure is needed because this operation neither transforms tensor values nor carries data into a later lowering stage.

def TorchLean.Tensor.Internal.Check.ParseShape.expandAxes (expression : Syntax.Expression) (inputRank : ℕ) : List (Option Syntax.CompositeAxis)

Expand the unique ellipsis to one skipped position per unmatched physical dimension. A none entry records a physical dimension hidden by the ellipsis; every other top-level pattern position is retained verbatim.

The concrete checker establishes the structural and rank preconditions under which this list has exactly inputRank entries.

def TorchLean.Tensor.Internal.Check.ParseShape.binding? (patternAxis : Option Syntax.CompositeAxis) (dimension : ℕ) : Option (String × ℕ)

Extract the named length contributed by one expanded pattern position. Underscores, literals, units, and ellipsis-expanded positions contribute no binding.

theorem TorchLean.Tensor.Internal.Check.ParseShape.binding?_eq_some_length {patternAxis : Option Syntax.CompositeAxis} {dimension : ℕ} {name : String} {length : ℕ} (h : binding? patternAxis dimension = some (name, length)) : dimension = length

A returned binding always carries its paired physical dimension.

def TorchLean.Tensor.Internal.Check.ParseShape.AxisMatches (patternAxis : Option Syntax.CompositeAxis) (dimension : ℕ) : Prop

The declarative dimension condition for one expanded parse-shape position. Named axes and wildcards accept any dimension; units and numeric axes must match their literal lengths.

def TorchLean.Tensor.Internal.Check.ParseShape.Impl.validateAxis (patternAxis : Option Syntax.CompositeAxis) (dimension : ℕ) : Result Unit

Check one expanded parse-shape axis against its physical dimension.

def TorchLean.Tensor.Internal.Check.ParseShape.Impl.validateAxes : List (Option Syntax.CompositeAxis) → Shape → Result Unit

Validate expanded parse-shape axes and physical dimensions in lockstep.

def TorchLean.Tensor.Internal.Check.checkParseShape (expression : Syntax.Expression) (inputShape : Shape) : Result SupplementaryLengths

Check a parsed parse_shape expression against a concrete tensor shape.

The result contains exactly the named, non-underscore axes in pattern order. The checker rejects genuine composite axes, malformed ellipses, rank mismatches, literal-length mismatches, and duplicate returned names.

theorem TorchLean.Tensor.Internal.Check.checkParseShape_ordered_bindings {expression : Syntax.Expression} {inputShape : Shape} {bindings : SupplementaryLengths} (h : checkParseShape expression inputShape = Except.ok bindings) : bindings = List.filterMap (fun (item : Option Syntax.CompositeAxis × ℕ) => ParseShape.binding? item.1 item.2) ((ParseShape.expandAxes expression (List.length inputShape)).zip inputShape)

A successful result is the left-to-right filterMap of the expanded pattern zipped with physical dimensions. This states both the returned order and the fact that ellipsis and wildcard positions are skipped rather than reordered.

theorem TorchLean.Tensor.Internal.Check.checkParseShape_names_nodup {expression : Syntax.Expression} {inputShape : Shape} {bindings : SupplementaryLengths} (h : checkParseShape expression inputShape = Except.ok bindings) : bindings.names.Nodup

Successful parse-shape results never contain a duplicate axis name.

theorem TorchLean.Tensor.Internal.Check.checkParseShape_axes_match {expression : Syntax.Expression} {inputShape : Shape} {bindings : SupplementaryLengths} (h : checkParseShape expression inputShape = Except.ok bindings) : List.Forall₂ ParseShape.AxisMatches (ParseShape.expandAxes expression (List.length inputShape)) inputShape

Every successful pattern position satisfies its declarative dimension condition. In particular, unit and anonymous numeric axes agree with the physical shape, including dimensions of length zero where allowed.

theorem TorchLean.Tensor.Internal.Check.checkParseShape_dimension_agreement {expression : Syntax.Expression} {inputShape : Shape} {bindings : SupplementaryLengths} (h : checkParseShape expression inputShape = Except.ok bindings) {name : String} {length : ℕ} (hBinding : (name, length) ∈ bindings) : ∃ (patternAxis : Option Syntax.CompositeAxis), (patternAxis, length) ∈ (ParseShape.expandAxes expression (List.length inputShape)).zip inputShape ∧ ParseShape.binding? patternAxis length = some (name, length)

Each returned (name, length) is obtained from a named expanded pattern position paired with that exact physical tensor dimension.