Expression token state

This module owns duplicate detection, group state, token decoding, and the canonicalization invariants preserved by each state transition.

inductive TorchLean.Tensor.Internal.Syntax.Parser.Impl.AxisKey : Type

Duplicate-detection identity for a named axis or the single ellipsis marker.

• named (name : String) : AxisKey

  Duplicate-detection key for a user-named axis.

• ellipsis : AxisKey

  Duplicate-detection key shared by all ellipsis occurrences.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Syntax.Parser.Impl.instDecidableEqAxisKey : DecidableEq AxisKey

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.instDecidableEqAxisKey.decEq (x✝ x✝¹ : AxisKey) : Decidable (x✝ = x✝¹)

structure TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState : Type

Accumulated grouping and duplicate-detection state for one expression.

• seen : List AxisKey

  Axis identities already accepted in this expression.

• group : Option (Span × List (Located Axis))

  The currently open parenthesized group, if any.

• axesRev : List CompositeAxis

  Completed physical axes in reverse source order.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.canonicalTokenKind (policy : IdentifierPolicy) : TokenKind → TokenKind

Normalize decimal words to their canonical natural-number spelling while leaving structural tokens unchanged.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.canonicalTokenKind_beq_arrow (policy : IdentifierPolicy) (token : TokenKind) : (canonicalTokenKind policy token == TokenKind.arrow) = (token == TokenKind.arrow)

Canonicalizing decimal words does not change whether a token is an arrow.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.canonicalTokenKind_eq_comma (policy : IdentifierPolicy) (token : TokenKind) : canonicalTokenKind policy token = TokenKind.comma ↔ token = TokenKind.comma

Canonicalizing decimal words preserves and reflects comma tokens.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.findArrow_eq_none_of_canonical (policy : IdentifierPolicy) (sourceTokens targetTokens : List Token) (hTokens : List.map Located.value targetTokens = List.map (fun (token : Token) => canonicalTokenKind policy token.value) sourceTokens) (hFind : List.find? (fun (token : Token) => token.value == TokenKind.arrow) sourceTokens = none) : List.find? (fun (token : Token) => token.value == TokenKind.arrow) targetTokens = none

Canonical token replacement cannot introduce an arrow into an arrow-free stream.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.duplicateDiagnostic (span : Span) : Diagnostic

Construct a source-located duplicate-axis diagnostic.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.registerKey (config : ExpressionConfig) (key : AxisKey) (span : Span) (seen : List AxisKey) : Result (List AxisKey)

Record one named axis or ellipsis while enforcing the expression's duplicate policy.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.registerKey_eq_ok_at_span (config : ExpressionConfig) (key : AxisKey) (sourceSpan targetSpan : Span) (seen nextSeen : List AxisKey) (hRegister : registerKey config key sourceSpan seen = Except.ok nextSeen) : registerKey config key targetSpan seen = Except.ok nextSeen

Successful duplicate registration is independent of the diagnostic source span.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.hasForbiddenUnderscore (config : ExpressionConfig) (name : String) : Bool

Enforce einops underscore placement while permitting the wildcard _.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.decodeWord (policy : IdentifierPolicy) (config : ExpressionConfig) (token : Token) (state : ExpressionState) : Result (Located Axis × ExpressionState)

Interpret one word token as a named, anonymous, or unit axis and update duplicate tracking.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.decodeEllipsis (config : ExpressionConfig) (token : Token) (state : ExpressionState) : Result (Located Axis × ExpressionState)

Decode and register a bare ellipsis token.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.pushAxis (axis : Located Axis) (state : ExpressionState) : ExpressionState

Append an axis to the open group or as a new top-level physical axis.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.tokenKinds (state : ExpressionState) : List TokenKind

Render the parser state's completed axes and any currently open group.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.tokenKinds_pushAxis (axis : Located Axis) (state : ExpressionState) : (pushAxis axis state).tokenKinds = state.tokenKinds ++ [axis.value.tokenKind]

Appending an axis to parser state appends its token kind to the rendered state.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.CanonicalEq (left right : ExpressionState) : Prop

Relate parser states that differ only in source spans and canonical decimal spelling.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.canonicalEq_pushAxis (leftAxis rightAxis : Located Axis) (leftState rightState : ExpressionState) (hState : leftState.CanonicalEq rightState) (hAxis : leftAxis.value.tokenKind = rightAxis.value.tokenKind) : (pushAxis leftAxis leftState).CanonicalEq (pushAxis rightAxis rightState)

Pushing canonically equal axes preserves canonical parser-state equivalence.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.canonicalEq_setSeen (leftState rightState : ExpressionState) (leftSeen rightSeen : List AxisKey) (hState : leftState.CanonicalEq rightState) (hSeen : leftSeen = rightSeen) : { seen := leftSeen, group := leftState.group, axesRev := leftState.axesRev }.CanonicalEq { seen := rightSeen, group := rightState.group, axesRev := rightState.axesRev }

Replacing equal duplicate-tracking lists preserves canonical state equivalence.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.canonicalEq_openGroup (leftState rightState : ExpressionState) (leftSpan rightSpan : Span) (hState : leftState.CanonicalEq rightState) (hLeftGroup : leftState.group = none) (hRightGroup : rightState.group = none) : { seen := leftState.seen, group := some (leftSpan, []), axesRev := leftState.axesRev }.CanonicalEq { seen := rightState.seen, group := some (rightSpan, []), axesRev := rightState.axesRev }

Opening corresponding empty groups preserves canonical state equivalence.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.ExpressionState.canonicalEq_closeGroup (leftState rightState : ExpressionState) (leftOpenSpan rightOpenSpan leftCloseSpan rightCloseSpan : Span) (leftAxesRev rightAxesRev : List (Located Axis)) (hState : leftState.CanonicalEq rightState) (hLeftGroup : leftState.group = some (leftOpenSpan, leftAxesRev)) (hRightGroup : rightState.group = some (rightOpenSpan, rightAxesRev)) : { seen := leftState.seen, axesRev := { axes := leftAxesRev.reverse, parenthesized := true, span := leftOpenSpan.join leftCloseSpan } :: leftState.axesRev }.CanonicalEq { seen := rightState.seen, axesRev := { axes := rightAxesRev.reverse, parenthesized := true, span := rightOpenSpan.join rightCloseSpan } :: rightState.axesRev }

Closing corresponding groups preserves canonical token structure despite span changes.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.tokenKinds_pushAxis_decodeWord (policy : IdentifierPolicy) (config : ExpressionConfig) (token : Token) (state : ExpressionState) (axis : Located Axis) (nextState : ExpressionState) (hDecode : decodeWord policy config token state = Except.ok (axis, nextState)) : (pushAxis axis nextState).tokenKinds = state.tokenKinds ++ [canonicalTokenKind policy token.value]

Successful word decoding appends the token's canonical kind to parser state.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.decodeWord_canonical (config : ExpressionConfig) (sourceToken targetToken : Token) (sourceState targetState : ExpressionState) (sourceAxis : Located Axis) (sourceNextState : ExpressionState) (hValue : targetToken.value = canonicalTokenKind IdentifierPolicy.pythonUnicode sourceToken.value) (hState : sourceState.CanonicalEq targetState) (hDecode : decodeWord IdentifierPolicy.pythonUnicode config sourceToken sourceState = Except.ok (sourceAxis, sourceNextState)) : ∃ (targetAxis : Located Axis), ∃ (targetNextState : ExpressionState), decodeWord IdentifierPolicy.pythonUnicode config targetToken targetState = Except.ok (targetAxis, targetNextState) ∧ (pushAxis sourceAxis sourceNextState).CanonicalEq (pushAxis targetAxis targetNextState)

Decoding a canonical word spelling succeeds with an equivalent next parser state.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.tokenKinds_pushAxis_decodeEllipsis (config : ExpressionConfig) (token : Token) (state : ExpressionState) (axis : Located Axis) (nextState : ExpressionState) (hDecode : decodeEllipsis config token state = Except.ok (axis, nextState)) : (pushAxis axis nextState).tokenKinds = state.tokenKinds ++ [TokenKind.ellipsis]

Successful ellipsis decoding appends exactly one ellipsis token kind.

theorem TorchLean.Tensor.Internal.Syntax.Parser.Impl.decodeEllipsis_canonical (config : ExpressionConfig) (sourceToken targetToken : Token) (sourceState targetState : ExpressionState) (sourceAxis : Located Axis) (sourceNextState : ExpressionState) (hState : sourceState.CanonicalEq targetState) (hDecode : decodeEllipsis config sourceToken sourceState = Except.ok (sourceAxis, sourceNextState)) : ∃ (targetAxis : Located Axis), ∃ (targetNextState : ExpressionState), decodeEllipsis config targetToken targetState = Except.ok (targetAxis, targetNextState) ∧ (pushAxis sourceAxis sourceNextState).CanonicalEq (pushAxis targetAxis targetNextState)

Re-decoding an ellipsis at a new span preserves canonical parser state.