Einops lexer

The lexer separates punctuation from axis words while preserving Unicode scalar offsets. Its default identifier policy reproduces the CPython 3.12 Unicode predicates used by einops v0.8.2. An explicit ASCII policy remains available for applications that deliberately restrict their pattern format.

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

Identifier operations required by the lexer and parser.

• isWordChar : Char → Bool

  Whether a character may continue the current axis word.

• isIdentifier : String → Bool

  Whether a complete word is a valid named axis.

• isDecimal : String → Bool

  Whether a complete word denotes a nonnegative decimal integer.

• toNat? : String → Option Nat

  Convert a validated decimal word to its natural-number value.

def TorchLean.Tensor.Internal.Syntax.IdentifierPolicy.ascii : IdentifierPolicy

Restrict axis names and anonymous dimensions to ASCII characters.

def TorchLean.Tensor.Internal.Syntax.IdentifierPolicy.pythonUnicode : IdentifierPolicy

Match the word, identifier, and decimal predicates used by einops v0.8.2 on CPython 3.12.13 with Unicode 15.0.0.

Word characters follow str.isalnum() plus underscore. Complete words then follow str.isidentifier(), while anonymous dimensions follow str.isdecimal() and Python's arbitrary-precision decimal conversion.

theorem TorchLean.Tensor.Internal.Syntax.IdentifierPolicy.pythonUnicode_isWordChar_of_isDigit (character : Char) (hDigit : character.isDigit = true) : pythonUnicode.isWordChar character = true

Every ASCII decimal digit is a word character under the Python policy.

theorem TorchLean.Tensor.Internal.Syntax.IdentifierPolicy.pythonUnicode_isDecimal_toString (value : Nat) : pythonUnicode.isDecimal (toString value) = true

Canonical decimal notation is recognized by the Python policy.

theorem TorchLean.Tensor.Internal.Syntax.IdentifierPolicy.pythonUnicode_word_toString (value : Nat) : (toString value).toList ≠ [] ∧ ∀ (character : Char), character ∈ (toString value).toList → pythonUnicode.isWordChar character = true

Canonical natural-number notation is a nonempty lexer word under the Python identifier policy.

theorem TorchLean.Tensor.Internal.Syntax.IdentifierPolicy.pythonUnicode_toNat?_toString (value : Nat) : pythonUnicode.toNat? (toString value) = some value

Canonical decimal notation decodes to the natural number it renders.

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

Tokens shared by the three pattern grammars.

• word (text : String) : TokenKind

  An identifier or decimal axis literal.

• leftParen : TokenKind

  The opening delimiter of a composite axis.

• rightParen : TokenKind

  The closing delimiter of a composite axis.

• ellipsis : TokenKind

  The ... token.

• arrow : TokenKind

  The -> token separating input and output expressions.

• comma : TokenKind

  The comma separating einsum operands.

• star : TokenKind

  The packed-axis marker used by pack and unpack.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instReprTokenKind : Repr TokenKind

def TorchLean.Tensor.Internal.Syntax.instReprTokenKind.repr : TokenKind → Nat → Std.Format

def TorchLean.Tensor.Internal.Syntax.instDecidableEqTokenKind.decEq (x✝ x✝¹ : TokenKind) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.instDecidableEqTokenKind : DecidableEq TokenKind

def TorchLean.Tensor.Internal.Syntax.TokenKind.render : TokenKind → String

Canonical source text for one lexer token.

def TorchLean.Tensor.Internal.Syntax.TokenKind.renderSequence : List TokenKind → String

Render a token sequence with conventional einops spacing.

Parentheses remain tight, commas have no preceding space, and every other token boundary receives one space. Empty operands are represented by consecutive commas or by a comma adjacent to the arrow.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Syntax.Token : Type

A token with its source location.

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

Which source characters count as inter-token whitespace.

• isWhitespace : Char → Bool

  Decide whether a source character separates adjacent tokens.

def TorchLean.Tensor.Internal.Syntax.LexicalWhitespace.transformation : LexicalWhitespace

Transformation parsing in einops v0.8.2 treats only spaces as whitespace.

def TorchLean.Tensor.Internal.Syntax.LexicalWhitespace.general : LexicalWhitespace

Packing uses Python's whitespace splitting behavior.

def TorchLean.Tensor.Internal.Syntax.lex (source : String) (policy : IdentifierPolicy := IdentifierPolicy.pythonUnicode) (whitespace : LexicalWhitespace := LexicalWhitespace.transformation) : Result (List Token)

Tokenize an einops pattern using the selected identifier and whitespace policies.

theorem TorchLean.Tensor.Internal.Syntax.word_valid_of_lex_eq_ok (source : String) (policy : IdentifierPolicy) (whitespace : LexicalWhitespace) {tokens : List Token} (hLex : lex source policy whitespace = Except.ok tokens) {token : Token} (hToken : token ∈ tokens) {text : String} (hWord : token.value = TokenKind.word text) : text.toList ≠ [] ∧ ∀ (character : Char), character ∈ text.toList → policy.isWordChar character = true

Every word emitted by a successful lexer run is nonempty and consists entirely of characters accepted by that run's identifier policy.

theorem TorchLean.Tensor.Internal.Syntax.lex_word (policy : IdentifierPolicy) (whitespace : LexicalWhitespace) (text : String) (hNonempty : text.toList ≠ []) (hCharacters : ∀ (character : Char), character ∈ text.toList → policy.isWordChar character = true) : lex text policy whitespace = Except.ok [{ value := TokenKind.word text, span := { offset := 0, length := text.toList.length } }]

A nonempty string consisting entirely of word characters lexes as one word.

This is the compositional lexer fact used by canonical pattern rendering; identifier and decimal validation remain the parser's responsibility.

theorem TorchLean.Tensor.Internal.Syntax.TokenKind.lex_renderSequence_transformation (tokens : List TokenKind) (hWords : ∀ (text : String), word text ∈ tokens → text.toList ≠ [] ∧ ∀ (character : Char), character ∈ text.toList → IdentifierPolicy.pythonUnicode.isWordChar character = true) : Except.map (List.map Located.value) (lex (renderSequence tokens)) = Except.ok tokens

Canonical token rendering is a right inverse of the transformation lexer once source spans are erased.

The word hypothesis is necessary because TokenKind.word is also available to clients constructing token lists directly, whereas words produced by lex always satisfy it.

theorem TorchLean.Tensor.Internal.Syntax.TokenKind.lex_renderSequence_general (tokens : List TokenKind) (hWords : ∀ (text : String), word text ∈ tokens → text.toList ≠ [] ∧ ∀ (character : Char), character ∈ text.toList → IdentifierPolicy.pythonUnicode.isWordChar character = true) : Except.map (List.map Located.value) (lex (renderSequence tokens) IdentifierPolicy.pythonUnicode LexicalWhitespace.general) = Except.ok tokens

Canonical token rendering is also a right inverse of the general-whitespace lexer used by pack and unpack.