Native tensor literals

Lean's ordinary bracket syntax remains list syntax unless its expected type is Spec.Shape or TorchLean.Tensor α shape. Shape brackets elaborate through Shape.ofList. For a tensor expected type, ordinary nested brackets construct a tensor and verify every dimension during elaboration.

List patterns retain their usual meaning, including empty and nested patterns. The tensor elaborator delegates to the packed implementation, so there is one storage invariant and no separate representation for literals.

def TorchLean.Tensor.Internal.Elab.tensorOrListLiteralStx : Lean.ParserDescr

Brackets whose interpretation can be directed by an expected tensor type.

def TorchLean.Tensor.Internal.Elab.tensorLiteralExpectedTypeStx : Lean.ParserDescr

Internal marker carrying the expected type through bracket expansion.

def TorchLean.Tensor.Internal.Elab.expandTensorLiteral : Lean.Macro

Keep the contents as Lean's builtin list syntax and mark the surrounding type ascription for the tensor elaborator. Lean expands macros before collecting pattern variables: a custom term node at that point would make even [x] an invalid list pattern. A type ascription lets that collector see the ordinary list constructors while leaving the expected-type decision to elaboration.

The inner node uses the original list parser directly. Its expansion therefore keeps Lean's own handling of long lists and cannot call this macro again.

def TorchLean.Tensor.Internal.Elab.elabTensorLiteral : Lean.Elab.Term.TermElab

Interpret marked brackets using their expected type. Ordinary lists, including the constructor expressions produced while elaborating patterns, go straight to Lean's list elaboration.

For tensors, elaborate the list with the scalar or subtensor type required by the trailing dimensions, then use the usual packed constructors. This also works when a caller has already expanded the list macro before elaboration.