Shared report decoding

This module provides the reflection, formatting, and axis-analysis utilities used by the operation-specific einops? reports.

instantiateOuterLets is not defined here. It is Tensor.Internal.instantiateOuterLets from NN/Tactic/Einops/Proof.lean, which this module already imports, and which had the identical four-line body. Report.Impl sits inside Tensor.Internal, so the uses below find it by walking outward.

def TorchLean.Tensor.Internal.Report.Impl.reportWhnf (expression : Lean.Expr) : Lean.MetaM Lean.Expr

Normalize reflected report data after instantiating pending metavariables.

def TorchLean.Tensor.Internal.Report.Impl.constructorFields? (expression : Lean.Expr) (constructorName : Lean.Name) (fieldCount : ℕ) : Option (Array Lean.Expr)

Expose the fields of an expected reflected constructor after removing generated outer lets and metadata.

def TorchLean.Tensor.Internal.Report.Impl.decodeStringLiteral (expression : Lean.Expr) : Lean.MetaM (Option String)

Decode a reflected string only when kernel normalization exposes a literal.

def TorchLean.Tensor.Internal.Report.Impl.decodeNatLiteral (expression : Lean.Expr) : Lean.MetaM (Option ℕ)

Decode a reflected natural number only when it reduces to a literal.

partial def TorchLean.Tensor.Internal.Report.Impl.decodeExprList {α : Type} (expression : Lean.Expr) (decodeItem : Lean.Expr → Lean.MetaM (Option α)) : Lean.MetaM (Option (List α))

Decode a reflected list with an element decoder, failing atomically.

def TorchLean.Tensor.Internal.Report.Impl.decodeNatList (expression : Lean.Expr) : Lean.MetaM (Option (List ℕ))

Decode a fully concrete reflected shape or list of natural numbers.

def TorchLean.Tensor.Internal.Report.Impl.decodeTransformAxis (expression : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × String))

Decode a transformation axis together with its user-facing description.

def TorchLean.Tensor.Internal.Report.Impl.decodeEinsumAxis (expression : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × String))

Decode an einsum axis together with its user-facing description.

def TorchLean.Tensor.Internal.Report.Impl.decodeEinsumAxisValue (expression : Lean.Expr) : Lean.MetaM (Option Check.EinsumAxis)

Decode a reflected einsum axis to its concrete checker value.

def TorchLean.Tensor.Internal.Report.Impl.formatShape (shape : List ℕ) : String

Render one concrete shape in tensor notation.

def TorchLean.Tensor.Internal.Report.Impl.formatShapes (shapes : List (List ℕ)) : String

Render a heterogeneous family of concrete shapes.

def TorchLean.Tensor.Internal.Report.Impl.shapeSize : List ℕ → ℕ

Compute the number of scalar entries described by a concrete shape.

def TorchLean.Tensor.Internal.Report.Impl.formatType (typeExpression : Lean.Expr) : Lean.MetaM String

Pretty-print an elaborated type using the current local context.

def TorchLean.Tensor.Internal.Report.Impl.inferredType (expression : Lean.Expr) : Lean.MetaM String

Infer and pretty-print the type of an elaborated expression.

def TorchLean.Tensor.Internal.Report.Impl.containsConstant (expression : Lean.Expr) (name : Lean.Name) : Bool

Test whether a reflected term contains an application of a named constant.

def TorchLean.Tensor.Internal.Report.Impl.concreteTensorType (scalarType : Lean.Expr) (shape : List ℕ) : Lean.MetaM String

Pretty-print one concrete tensor type without evaluating a tensor value.

def TorchLean.Tensor.Internal.Report.Impl.reportSection (title : String) (lines : List String) : List String

Format one uniformly indented report section.

def TorchLean.Tensor.Internal.Report.Impl.typeCheckSection (entries : List (String × String)) : List String

Format checked input and output types.

def TorchLean.Tensor.Internal.Report.Impl.performanceFooter : List String

Explain how static estimates relate to actual runtime measurements.

def TorchLean.Tensor.Internal.Report.Impl.formatAxes (axes : List (Lean.Expr × String)) : String

Render a flat logical-axis list.

def TorchLean.Tensor.Internal.Report.Impl.formatAxisGroup (group : List (Lean.Expr × String)) : String

Render one elementary-axis group using einops parentheses.

def TorchLean.Tensor.Internal.Report.Impl.formatAxisGroups (groups : List (List (Lean.Expr × String))) : String

Render a physical shape's complete sequence of logical-axis groups.

def TorchLean.Tensor.Internal.Report.Impl.uniqueAxes (axes : List (Lean.Expr × String)) : List (Lean.Expr × String)

Preserve the first occurrence of each reflected axis expression.

def TorchLean.Tensor.Internal.Report.Impl.axesNotIn (axes others : List (Lean.Expr × String)) : List (Lean.Expr × String)

Select axes absent from another reflected axis list.

def TorchLean.Tensor.Internal.Report.Impl.repeatedAxes (axes : List (Lean.Expr × String)) : List (Lean.Expr × String)

Select the axes repeated within one operand.

def TorchLean.Tensor.Internal.Report.Impl.axisLength? (lengths : List (Lean.Expr × ℕ)) (axis : Lean.Expr) : Option ℕ

Look up the concrete length associated with a reflected axis expression.

def TorchLean.Tensor.Internal.Report.Impl.axisShape? (axes : List (Lean.Expr × String)) (lengths : List (Lean.Expr × ℕ)) : Option (List ℕ)

Resolve an ordered axis list to a concrete shape when every length is known.

def TorchLean.Tensor.Internal.Report.Impl.broadcastDescriptions (shape : List ℕ) (axes : List (Lean.Expr × String)) (lengths : List (Lean.Expr × ℕ)) : List String

Describe singleton dimensions that expand to non-singleton logical axes.

def TorchLean.Tensor.Internal.Report.Impl.numberedStageLines : ℕ → List String → List String

Number human-readable lowering stages from the supplied starting index.