Shape-checking diagnostics #

Shape checking is separate from parsing, but uses the same source spans.

source

inductive TorchLean.Tensor.Internal.Check.DiagnosticCode :

Type

Stable categories for concrete shape-checking failures.

rankMismatch : DiagnosticCode
The number of physical dimensions disagreed with the pattern rank.
invalidEllipsis : DiagnosticCode
An ellipsis was placed or expanded in a way forbidden by the operation.
anonymousAxisInRearrange : DiagnosticCode
A rearrangement used a numeric axis, which cannot identify input data.
axisMismatch : DiagnosticCode
The input and output patterns referred to different logical axes.
duplicateAxisLength : DiagnosticCode
The caller supplied more than one length for the same named axis.
unusedAxisLength : DiagnosticCode
The caller supplied a named length that the pattern does not use.
cannotInferAxis : DiagnosticCode
A composite input dimension did not determine one of its axis lengths.
dimensionMismatch : DiagnosticCode
A known axis length disagreed with the corresponding tensor dimension.
missingAxisLength : DiagnosticCode
An output-only axis had no length supplied by the caller.
einsumOperandCountMismatch : DiagnosticCode
The number of einsum tensors disagreed with the number of input expressions.
unsupportedEinsumAxis : DiagnosticCode
An einsum expression used grouping or an axis form outside its surface grammar.
unknownEinsumOutputAxis : DiagnosticCode
An einsum output named an axis absent from every input.
duplicateEinsumOutputAxis : DiagnosticCode
An einsum output named the same logical axis more than once.
tooManyEinsumAxes : DiagnosticCode
The reference-compatible einsum front end exceeded its 52-label limit.
repeatedEinsumDimensionMismatch : DiagnosticCode
Repeated occurrences of an einsum label in one operand had unequal lengths.
incompatibleEinsumBroadcast : DiagnosticCode
Non-singleton occurrences of an einsum axis had incompatible lengths.
compositeParseShapeAxis : DiagnosticCode
A parse_shape expression used a grouped physical axis.
duplicateParseShapeAxis : DiagnosticCode
A parse_shape expression bound the same name more than once.
emptyPackInput : DiagnosticCode
pack was asked to combine no tensors.
packRankMismatch : DiagnosticCode
A tensor rank was too small for the fixed axes of a pack pattern.
packDimensionMismatch : DiagnosticCode
Corresponding fixed axes of packed tensors had different lengths.
unpackRankMismatch : DiagnosticCode
A packed tensor rank disagreed with the rank implied by its metadata.
invalidPackedShape : DiagnosticCode
Unpack metadata did not describe a valid concrete packed shape.
multipleInferredDimensions : DiagnosticCode
An unpack shape requested inference for more than one dimension.
cannotInferPackedDimension : DiagnosticCode
The packed extent did not uniquely determine an inferred dimension.
packedAxisMismatch : DiagnosticCode
Unpack metadata did not multiply to the packed tensor dimension.
internalInvariant : DiagnosticCode
An implementation invariant failed after earlier checks had established it.

Instances For

source

def TorchLean.Tensor.Internal.Check.instReprDiagnosticCode.repr :

DiagnosticCode → Nat → Std.Format

Instances For

source

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.instReprDiagnosticCode :

Repr DiagnosticCode

source

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.instDecidableEqDiagnosticCode :

DecidableEq DiagnosticCode

source

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.instBEqDiagnosticCode :

BEq DiagnosticCode

source

def TorchLean.Tensor.Internal.Check.instBEqDiagnosticCode.beq :

DiagnosticCode → DiagnosticCode → Bool

Instances For

source

structure TorchLean.Tensor.Internal.Check.Diagnostic :

Type

A structured concrete-checking error.

code : DiagnosticCode
Stable machine-readable category of the checking failure.
message : String
Human-readable explanation of the failed shape obligation.
span : Syntax.Span
Smallest useful range of the pattern responsible for the failure.

Instances For

source

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.instReprDiagnostic :

Repr Diagnostic

source

def TorchLean.Tensor.Internal.Check.instReprDiagnostic.repr :

Diagnostic → Nat → Std.Format

Instances For

source