Transformation arrow splitting

Arrow splitting rejects missing or duplicate arrows and preserves canonical left and right token sequences.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.splitArrow (eof : Span) : List Token → List Token → Result (List Token × Token × List Token)

Split a transformation token stream at its unique arrow.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.splitArrow_canonical (sourceEof targetEof : Span) (sourceTokens targetTokens sourceLeftRev targetLeftRev sourceLeft sourceRight : List Token) (sourceArrow : Token) (hTokens : List.map Located.value targetTokens = List.map (fun (token : Token) => canonicalTokenKind IdentifierPolicy.pythonUnicode token.value) sourceTokens) (hLeftRev : List.map Located.value targetLeftRev = List.map (fun (token : Token) => canonicalTokenKind IdentifierPolicy.pythonUnicode token.value) sourceLeftRev) (hSplit : splitArrow sourceEof sourceTokens sourceLeftRev = Except.ok (sourceLeft, sourceArrow, sourceRight)) : ∃ (targetLeft : List Token), ∃ (targetArrow : Token), ∃ (targetRight : List Token), splitArrow targetEof targetTokens targetLeftRev = Except.ok (targetLeft, targetArrow, targetRight) ∧ List.map Located.value targetLeft = List.map (fun (token : Token) => canonicalTokenKind IdentifierPolicy.pythonUnicode token.value) sourceLeft ∧ List.map Located.value targetRight = List.map (fun (token : Token) => canonicalTokenKind IdentifierPolicy.pythonUnicode token.value) sourceRight

Splitting canonical tokens preserves the left and right token sequences.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.splitArrow_eq_ok_decomposition (eof : Span) (tokens leftRev left right : List Token) (arrow : Token) (hSplit : splitArrow eof tokens leftRev = Except.ok (left, arrow, right)) : leftRev.reverse ++ tokens = left ++ arrow :: right ∧ arrow.value = TokenKind.arrow

A successful arrow split reconstructs the original stream around an arrow token.