Expression token parsing

The recursive parser validates grouping and axis names in a lexer-produced token stream. Its canonical-token theorem records the syntax consumed on success; tensor dimensions and operation-specific constraints are checked separately.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.parseExpressionTokens (policy : IdentifierPolicy) (config : ExpressionConfig) (expressionSpan : Span) : List Token → ExpressionState → Result Expression

Parse one indexing expression while maintaining grouping and duplicate-axis state.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.tokenKinds_eq_of_parseExpressionTokens_eq_ok (policy : IdentifierPolicy) (config : ExpressionConfig) (expressionSpan : Span) (tokens : List Token) (state : ExpressionState) (expression : Expression) (hParse : parseExpressionTokens policy config expressionSpan tokens state = Except.ok expression) : expression.tokenKinds = state.tokenKinds ++ List.map (fun (token : Token) => canonicalTokenKind policy token.value) tokens

A successful expression parse records the canonical token sequence it consumed.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.parseExpressionTokens_canonical (config : ExpressionConfig) (sourceExpressionSpan targetExpressionSpan : Span) (sourceTokens targetTokens : List Token) (sourceState targetState : ExpressionState) (sourceExpression : Expression) (hTokens : List.map Located.value targetTokens = List.map (fun (token : Token) => canonicalTokenKind IdentifierPolicy.pythonUnicode token.value) sourceTokens) (hState : sourceState.CanonicalEq targetState) (hParse : parseExpressionTokens IdentifierPolicy.pythonUnicode config sourceExpressionSpan sourceTokens sourceState = Except.ok sourceExpression) : ∃ (targetExpression : Expression), parseExpressionTokens IdentifierPolicy.pythonUnicode config targetExpressionSpan targetTokens targetState = Except.ok targetExpression ∧ targetExpression.tokenKinds = sourceExpression.tokenKinds

Canonically equivalent token streams parse to expressions with equal token structure.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.canonical_words_valid_of_lex_eq_ok (source : String) (whitespace : LexicalWhitespace) (tokens : List Token) (hLex : lex source IdentifierPolicy.pythonUnicode whitespace = Except.ok tokens) (text : String) : TokenKind.word text ∈ List.map (fun (token : Token) => canonicalTokenKind IdentifierPolicy.pythonUnicode token.value) tokens → text.toList ≠ [] ∧ ∀ (character : Char), character ∈ text.toList → IdentifierPolicy.pythonUnicode.isWordChar character = true

Canonicalized words from a successful Python-policy lex remain valid lexer words.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.sourceSpan (source : String) : Span

The span covering an entire source string.