Lossless einops syntax trees

The AST preserves grouping, unit axes, anonymous-axis occurrences, and source locations. This is more informative than the reference implementation's internal ParsedExpression, which erases unit axes while parsing.

inductive TorchLean.Tensor.Internal.Syntax.Axis : Type

An elementary axis in a transformation expression.

Anonymous axes carry an occurrence number because two textual occurrences of the same numeral denote distinct axes in einops.

• named (name : String) : Axis

  A logical axis identified by the user's name.

• anonymous (value occurrence : Nat) : Axis

  A numeric axis, distinguished by its occurrence in the source pattern.

• unit : Axis

  A length-one axis written as 1.

• ellipsis : Axis

  The ... axis that stands for zero or more physical dimensions.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprAxis : Repr Axis

def TorchLean.Tensor.Internal.Syntax.instReprAxis.repr : Axis → Nat → Std.Format

def TorchLean.Tensor.Internal.Syntax.instDecidableEqAxis.decEq (x✝ x✝¹ : Axis) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqAxis : DecidableEq Axis

structure TorchLean.Tensor.Internal.Syntax.CompositeAxis : Type

One top-level axis or parenthesized composition.

• axes : List (Located Axis)

  Elementary axes written in this top-level component.

• parenthesized : Bool

  Whether the component was explicitly enclosed in parentheses.

• span : Span

  Source range covering the complete component.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprCompositeAxis : Repr CompositeAxis

def TorchLean.Tensor.Internal.Syntax.instReprCompositeAxis.repr : CompositeAxis → Nat → Std.Format

def TorchLean.Tensor.Internal.Syntax.instDecidableEqCompositeAxis.decEq (x✝ x✝¹ : CompositeAxis) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqCompositeAxis : DecidableEq CompositeAxis

def TorchLean.Tensor.Internal.Syntax.CompositeAxis.semanticAxes (axis : CompositeAxis) : List (Located Axis)

Unit axes disappear from the elementary-axis sequence.

def TorchLean.Tensor.Internal.Syntax.CompositeAxis.hasEllipsis (axis : CompositeAxis) : Bool

Whether this composition contains an ellipsis.

structure TorchLean.Tensor.Internal.Syntax.Expression : Type

One side of a transformation or einsum pattern.

• axes : List CompositeAxis

  Top-level physical axes in source order.

• span : Span

  Source range covering the complete expression.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprExpression : Repr Expression

def TorchLean.Tensor.Internal.Syntax.instReprExpression.repr : Expression → Nat → Std.Format

def TorchLean.Tensor.Internal.Syntax.instDecidableEqExpression.decEq (x✝ x✝¹ : Expression) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqExpression : DecidableEq Expression

def TorchLean.Tensor.Internal.Syntax.Expression.flatAxes (expression : Expression) : List (Located Axis)

Elementary axes after removing syntactic unit axes.

def TorchLean.Tensor.Internal.Syntax.Expression.namedAxes (expression : Expression) : List (Located String)

Named axes in source order, including repeated occurrences when allowed.

def TorchLean.Tensor.Internal.Syntax.Expression.ellipsisCount (expression : Expression) : Nat

The number of ellipses in an expression.

def TorchLean.Tensor.Internal.Syntax.Expression.hasParenthesizedEllipsis (expression : Expression) : Bool

Whether an ellipsis occurs inside parentheses.

def TorchLean.Tensor.Internal.Syntax.Expression.hasCompositeAxes (expression : Expression) : Bool

Whether an expression contains a genuine composite axis.

structure TorchLean.Tensor.Internal.Syntax.TransformPattern : Type

The shared syntax of rearrange, repeat, and reduce.

• left : Expression

  Input-side expression.

• arrow : Span

  Source range of the -> token.

• right : Expression

  Output-side expression.

• span : Span

  Source range covering the complete transformation pattern.

def TorchLean.Tensor.Internal.Syntax.instReprTransformPattern.repr : TransformPattern → Nat → Std.Format

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprTransformPattern : Repr TransformPattern

def TorchLean.Tensor.Internal.Syntax.instDecidableEqTransformPattern.decEq (x✝ x✝¹ : TransformPattern) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqTransformPattern : DecidableEq TransformPattern

structure TorchLean.Tensor.Internal.Syntax.PackPattern : Type

The separate grammar used by pack and unpack.

• before : List (Located String)

  Fixed named axes before the packed * region.

• packed : Span

  Source range of the unique * token.

• after : List (Located String)

  Fixed named axes after the packed * region.

• span : Span

  Source range covering the complete packing pattern.

def TorchLean.Tensor.Internal.Syntax.instReprPackPattern.repr : PackPattern → Nat → Std.Format

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprPackPattern : Repr PackPattern

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqPackPattern : DecidableEq PackPattern

def TorchLean.Tensor.Internal.Syntax.instDecidableEqPackPattern.decEq (x✝ x✝¹ : PackPattern) : Decidable (x✝ = x✝¹)

structure TorchLean.Tensor.Internal.Syntax.EinsumPattern : Type

The multi-input grammar used by einsum.

• inputs : List Expression

  Comma-separated operand expressions in source order.

• arrow : Span

  Source range of the -> token.

• output : Expression

  Output expression following the arrow.

• span : Span

  Source range covering the complete einsum pattern.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprEinsumPattern : Repr EinsumPattern

def TorchLean.Tensor.Internal.Syntax.instReprEinsumPattern.repr : EinsumPattern → Nat → Std.Format

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqEinsumPattern : DecidableEq EinsumPattern

def TorchLean.Tensor.Internal.Syntax.instDecidableEqEinsumPattern.decEq (x✝ x✝¹ : EinsumPattern) : Decidable (x✝ = x✝¹)