Shared elaboration infrastructure

This module contains the common metaprogramming machinery used by every operation family. Literal term grammar lives in TorchLean.Tensor.Internal.Elab.Syntax. These internal utilities inspect dependent tensor types, preserve symbolic natural-number dimensions, construct heterogeneous tensor families, and emit proof-bearing checker certificates.

The helpers live in TorchLean.Tensor.Internal.Elab.Impl because they are implementation infrastructure rather than user API. Operation modules share them directly; there is no alternate tensor representation or compatibility elaborator.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprSpan : Lean.ToExpr Syntax.Span

def TorchLean.Tensor.Internal.Elab.instToExprSpan.toExpr : Syntax.Span → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprLocated {α✝ : Type u} [Lean.ToExpr α✝] [Lean.ToLevel] : Lean.ToExpr (Syntax.Located α✝)

def TorchLean.Tensor.Internal.Elab.instToExprLocated.toExpr {α✝ : Type u} [Lean.ToExpr α✝] : Lean.ToLevel → Syntax.Located α✝ → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprAxis : Lean.ToExpr Syntax.Axis

def TorchLean.Tensor.Internal.Elab.instToExprAxis.toExpr : Syntax.Axis → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprCompositeAxis : Lean.ToExpr Syntax.CompositeAxis

def TorchLean.Tensor.Internal.Elab.instToExprCompositeAxis.toExpr : Syntax.CompositeAxis → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprExpression : Lean.ToExpr Syntax.Expression

def TorchLean.Tensor.Internal.Elab.instToExprExpression.toExpr : Syntax.Expression → Lean.Expr

def TorchLean.Tensor.Internal.Elab.instToExprTransformPattern.toExpr : Syntax.TransformPattern → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprTransformPattern : Lean.ToExpr Syntax.TransformPattern

def TorchLean.Tensor.Internal.Elab.instToExprEinsumPattern.toExpr : Syntax.EinsumPattern → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprEinsumPattern : Lean.ToExpr Syntax.EinsumPattern

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprPackPattern : Lean.ToExpr Syntax.PackPattern

def TorchLean.Tensor.Internal.Elab.instToExprPackPattern.toExpr : Syntax.PackPattern → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprTransformKind : Lean.ToExpr Check.TransformKind

def TorchLean.Tensor.Internal.Elab.instToExprTransformKind.toExpr : Check.TransformKind → Lean.Expr

def TorchLean.Tensor.Internal.Elab.instToExprAxisId.toExpr : Check.AxisId → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprAxisId : Lean.ToExpr Check.AxisId

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprEinsumAxis : Lean.ToExpr Check.EinsumAxis

def TorchLean.Tensor.Internal.Elab.instToExprEinsumAxis.toExpr : Check.EinsumAxis → Lean.Expr

def TorchLean.Tensor.Internal.Elab.instToExprNormalizedTransform.toExpr : Check.NormalizedTransform → Lean.Expr

@[instance_reducible]

instance TorchLean.Tensor.Internal.Elab.instToExprNormalizedTransform : Lean.ToExpr Check.NormalizedTransform

def TorchLean.Tensor.Internal.Elab.Impl.pluralColumns (length : ℕ) : String

Render a singular or plural label for a diagnostic source range.

def TorchLean.Tensor.Internal.Elab.Impl.patternMarker (span : Syntax.Span) : String

Draw a caret marker beneath the source range selected by a diagnostic.

def TorchLean.Tensor.Internal.Elab.Impl.throwPatternDiagnostic {α : Type} (operation phase source message : String) (span : Syntax.Span) : Lean.Elab.TermElabM α

Raise an elaboration error containing the pattern and its precise source range.

partial def TorchLean.Tensor.Internal.Elab.Impl.staticListElements? (value : Lean.Expr) : Lean.MetaM (Option (List Lean.Expr))

Expose the elements of a statically known list while retaining symbolic element expressions.

def TorchLean.Tensor.Internal.Elab.Impl.concreteNatExpressions? (dimensions : List Lean.Expr) : Lean.MetaM (Option Shape)

Read natural-number expressions only when every dimension is concrete.

def TorchLean.Tensor.Internal.Elab.Impl.concreteShapes? (shapes : List (List Lean.Expr)) : Lean.MetaM (Option (List Shape))

Read shape-expression spines as ordinary shapes only when every dimension reduces to a natural-number literal.

partial def TorchLean.Tensor.Internal.Elab.Impl.concreteListLength? (value : Lean.Expr) : Lean.MetaM (Option ℕ)

Compute the length of a statically known list without inspecting its elements.

def TorchLean.Tensor.Internal.Elab.Impl.concreteIntExpression? (value : Lean.Expr) : Lean.MetaM (Option ℤ)

Evaluate an integer expression when kernel reduction exposes a literal.

partial def TorchLean.Tensor.Internal.Elab.Impl.concreteIntList? (value : Lean.Expr) : Lean.MetaM (Option (List ℤ))

Read a statically written list whose integer elements all reduce to literals.

partial def TorchLean.Tensor.Internal.Elab.Impl.concreteRequestedShapes? (value : Lean.Expr) : Lean.MetaM (Option Check.RequestedShapes)

Read concrete unpack metadata as a statically written list of integer lists.

def TorchLean.Tensor.Internal.Elab.Impl.tensorTypeInfo (tensorSyntax : Lean.Syntax) (tensorType : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Lean.Expr)

Recover the element type, static shape, and storage selected by TorchLean.Tensor.

The canonical public tensor abbreviation is unfolded before inspecting its packed representation. Arbitrary coordinate functions are not accepted as tensors.

def TorchLean.Tensor.Internal.Elab.Impl.elaborateTensor (tensorSyntax : Lean.Syntax) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.Expr)

Elaborate one tensor and expose its static list structure while preserving symbolic dimension expressions.

A nonempty list of equal-shaped tensors is accepted as a convenient stacked tensor and contributes its statically known list length as a leading axis.

def TorchLean.Tensor.Internal.Elab.Impl.supplementaryExpr (lengthSyntax : Array (Lean.TSyntax `einopsAxisLength)) : Lean.Elab.TermElabM (List (String × Lean.Expr))

Elaborate named supplementary axis lengths as natural-number expressions.

def TorchLean.Tensor.Internal.Elab.Impl.concreteSupplementary? (supplementary : List (String × Lean.Expr)) : Lean.MetaM (Option Check.SupplementaryLengths)

Reify supplementary axis lengths when every supplied expression is concrete.

def TorchLean.Tensor.Internal.Elab.Impl.applyConstructorArgument (constructor constructorType argument : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Apply one explicit structure-constructor argument after checking its dependent field type.

def TorchLean.Tensor.Internal.Elab.Impl.sealCertificate (proposition certificate : Lean.Expr) : Lean.MetaM Lean.Expr

Seal a generated certificate in a kernel-checked auxiliary theorem.

The module-qualified theorem kind prevents exported terms in independently compiled modules from producing the same _einops_N declaration names.

def TorchLean.Tensor.Internal.Elab.Impl.buildCertificate (constructorName : Lean.Name) (parameters fixedFields : Array Lean.Expr) (decidableFields : ℕ) : Lean.MetaM Lean.Expr

Build a proof-valued structure using explicit parameters, any fields that are already proved, and kernel-reduced decisions for the remaining fields.

def TorchLean.Tensor.Internal.Elab.Impl.certifyWithTactic (description : String) (proposition : Lean.Expr) (tactic : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Run a focused tactic on a generated proposition and seal the resulting kernel certificate in an auxiliary theorem.

Callers choose the smallest tactic vocabulary appropriate for their invariant. Failure is reported as a missing user hypothesis rather than hidden behind an unchecked cast or axiom.

def TorchLean.Tensor.Internal.Elab.Impl.certifyGeneratedInvariant (description : String) (proposition : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Discharge a general symbolic shape invariant using the arithmetic and finite-family vocabulary shared by transformations and packing.

def TorchLean.Tensor.Internal.Elab.Impl.axisDescription : Check.AxisId → String

Human-readable description of a logical transformation axis.

def TorchLean.Tensor.Internal.Elab.Impl.axisExpression? (assignments : List (Check.AxisId × Lean.Expr)) (axis : Check.AxisId) : Option Lean.Expr

Look up the symbolic length currently assigned to a logical axis.

def TorchLean.Tensor.Internal.Elab.Impl.appendAxisExpression (assignments : List (Check.AxisId × Lean.Expr)) (axis : Check.AxisId) (length : Lean.Expr) : List (Check.AxisId × Lean.Expr)

Append a symbolic axis assignment unless that axis was assigned earlier.

def TorchLean.Tensor.Internal.Elab.Impl.natProductExpr : List Lean.Expr → Lean.MetaM Lean.Expr

Construct a balanced-by-source-order natural-number product expression.

def TorchLean.Tensor.Internal.Elab.Impl.natSumExpr : List Lean.Expr → Lean.MetaM Lean.Expr

Construct a source-order natural-number sum expression.

def TorchLean.Tensor.Internal.Elab.Impl.axisExpressions (assignments : List (Check.AxisId × Lean.Expr)) (axes : List Check.AxisId) : Lean.MetaM (List Lean.Expr)

Resolve a list of logical axes to their symbolic length expressions.

def TorchLean.Tensor.Internal.Elab.Impl.axisProductExpr (assignments : List (Check.AxisId × Lean.Expr)) (axes : List Check.AxisId) : Lean.MetaM Lean.Expr

Multiply the symbolic lengths assigned to a group of elementary axes.

partial def TorchLean.Tensor.Internal.Elab.Impl.natMultiplicationFactors (value : Lean.Expr) : Lean.MetaM (List Lean.Expr)

Flatten multiplication syntax after reducible normalization, preserving each factor expression for definitional matching.

partial def TorchLean.Tensor.Internal.Elab.Impl.natAdditionSummands (value : Lean.Expr) : Lean.MetaM (List Lean.Expr)

Flatten addition syntax after reducible normalization, preserving each summand expression for definitional matching.

def TorchLean.Tensor.Internal.Elab.Impl.eraseDefinitionalFactor? (factor : Lean.Expr) : List Lean.Expr → Lean.MetaM (Option (List Lean.Expr))

Remove one definitionally equal factor from a candidate multiset.

def TorchLean.Tensor.Internal.Elab.Impl.eraseDefinitionalFactors? (factors : List Lean.Expr) : List Lean.Expr → Lean.MetaM (Option (List Lean.Expr))

Remove every requested factor by definitional equality, respecting multiplicity.

def TorchLean.Tensor.Internal.Elab.Impl.explicitMissingFactor? (dimension : Lean.Expr) (knownLengths : List Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Recover the missing factor when the tensor type already displays a product.

For example, if the physical dimension is syntactically height * width and height is known, the remaining expression width is a valid axis length even when height = 0. Falling back immediately to natural-number division would unnecessarily demand positivity and would lose information deliberately present in the dependent tensor type.

def TorchLean.Tensor.Internal.Elab.Impl.explicitResidual? (total : Lean.Expr) (known : List Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Recover the part of a packed length not occupied by known segments.

Addition is treated modulo association and order, but only definitionally equal summands are removed. This preserves expressions already present in the tensor type without asking the kernel to choose a subtraction normal form.

def TorchLean.Tensor.Internal.Elab.Impl.shapeExpr (dimensions : List Lean.Expr) : Lean.MetaM Lean.Expr

Construct the type-level shape list represented by symbolic dimensions.

def TorchLean.Tensor.Internal.Elab.Impl.shapesExpr (shapes : List Lean.Expr) : Lean.MetaM Lean.Expr

Construct a list of already elaborated type-level shape expressions.

def TorchLean.Tensor.Internal.Elab.Impl.castTensorToCompactShape (result targetShape : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Transport a generated tensor from a checker-indexed result shape to the compact dimension list computed by the surface operation.

The equality is definitional for generated plans, but the explicit transport prevents inferred declaration types from retaining the complete checker certificate.

def TorchLean.Tensor.Internal.Elab.Impl.publicTensorType (scalarType shape storage : Lean.Expr) : Lean.MetaM Lean.Expr

Construct the public tensor type corresponding to an internal list-shaped dimension expression.

Generated kernels use Rep directly, but inferred declaration types should retain the ordinary Tensor α [dims] spelling seen by users and editor tooling.

def TorchLean.Tensor.Internal.Elab.Impl.exposePublicTensorType (result shape : Lean.Expr) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Give an inferred tensor result its compact public type without changing its value or its checked implementation.

An explicit expected type remains authoritative. Otherwise the scalar and storage are recovered from the generated Rep, while shape is the compact shape expression computed by the public operation.

def TorchLean.Tensor.Internal.Elab.Impl.expectedTensorShape? (expectedType? : Option Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract a tensor shape from an informative, non-metavariable expected type.

def TorchLean.Tensor.Internal.Elab.Impl.extractSuccessfulResult (checkedResult : Lean.Expr) : Lean.MetaM Lean.Expr

Extract the value from a checker result already proved to be successful.

def TorchLean.Tensor.Internal.Elab.Impl.attachCheckerAgreement (checkedResult checked result : Lean.Expr) : Lean.MetaM Lean.Expr

Register evidence that a reflected certificate is exactly the ordinary checker's result.

The agreement is checked once as a named theorem. It is deliberately not embedded as a nondependent let in every generated value: doing so repeats a potentially large checker proposition during downstream type checking even though the proof has no computational or dependent use.

partial def TorchLean.Tensor.Internal.Elab.Impl.buildTensorFamilyCases (scalarType storage : Lean.Expr) (inputShapes inputTensors : List Lean.Expr) (tensorIndex : Lean.Expr) : Lean.MetaM Lean.Expr

Eliminate a finite tensor index into one branch per heterogeneous operand, retaining each branch's exact dependent shape.

def TorchLean.Tensor.Internal.Elab.Impl.buildTensorFamily (scalarType storage : Lean.Expr) (inputShapes inputTensors : List Lean.Expr) : Lean.MetaM Lean.Expr

Build the dependent Fin n-indexed family of heterogeneous input tensors.

def TorchLean.Tensor.Internal.Elab.Impl.elaborateCommonScalarFamily (operation member : String) (tensorSyntax : Array (Lean.TSyntax `term)) : Lean.Elab.TermElabM (List Lean.Expr × List (List Lean.Expr) × Lean.Expr × Lean.Expr × List Bool)

Elaborate a nonempty tensor family and convert mixed element types to one common type before operation-specific checking.

Promotion folds from left to right. Each input conversion is composed during that fold and materialized at most once after the final common type is known. Homogeneous families retain their original tensors and storage exactly.

def TorchLean.Tensor.Internal.Elab.Impl.withCommonScalarFamily (operation member : String) (tensorSyntax : Array (Lean.TSyntax `term)) (body : List Lean.Expr → List (List Lean.Expr) → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Elaborate a common-scalar tensor family and share every required conversion around the generated consumer.

The continuation sees local tensor variables rather than repeated conversion expressions. Each conversion is passed through nativeStage, whose no-inline boundary ensures native execution materializes it once before entering the consumer rather than sinking it into every downstream scalar read.