Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

5,902 lines337 declarations199.2 KiBSHA-256 6d135c41813d

def · lines 421–515

flushStreamingAtom

Full file
421def flushStreamingAtom =
422  (lambda unrestricted state : (family StreamingStructuralState) .
423    (eliminate
424      StreamingStructuralState
425      (lambda unrestricted value : (family StreamingStructuralState) .
426        (family StreamingStructuralState))
427      state
428      (branch
429        StreamingStructuralActive
430        pendingAtom
431        streamingForest
432        streamingStack
433        origin
434        .
435        (nat-eliminate
436          (lambda unrestricted atomLength : Nat . (family StreamingStructuralState))
437          (constructor
438            StreamingStructuralState
439            StreamingStructuralActive
440            b""
441            streamingForest
442            streamingStack
443            (constructor SyntaxOrigin SyntaxOriginUnknown))
444          (lambda unrestricted predecessor : Nat .
445            (lambda unrestricted induction : (family StreamingStructuralState) .
446              (eliminate
447                QuotedLiteralResult
448                (lambda unrestricted checked : (family QuotedLiteralResult) .
449                  (family StreamingStructuralState))
450                (Compiler.QuotedLiteral/quotedValidateSourceAtom pendingAtom)
451                (branch
452                  QuotedLiteralDecoded
453                  payload
454                  .
455                  (constructor
456                    StreamingStructuralState
457                    StreamingStructuralActive
458                    b""
459                    (constructor
460                      Syntax
461                      SyntaxCons
462                      (constructor Syntax SyntaxAtom pendingAtom origin)
463                      streamingForest)
464                    streamingStack
465                    (constructor SyntaxOrigin SyntaxOriginUnknown)))
466                (branch
467                  QuotedLiteralFailed
468                  failure
469                  start
470                  end
471                  .
472                  (constructor
473                    StreamingStructuralState
474                    StreamingStructuralFailed
475                    (Compiler.QuotedLiteral/quotedLiteralFailureCode failure)
476                    (syntaxOriginRebaseRange origin start end)
477                    b""
478                    (constructor SyntaxOrigin SyntaxOriginUnknown))))))
479          (bytes-length pendingAtom)))
480      (branch
481        StreamingStructuralFailed
482        streamingFailureCode
483        structuralFailureOrigin
484        recoveryAtom
485        recoveryOrigin
486        .
487        (eliminate
488          QuotedLiteralResult
489          (lambda unrestricted checked : (family QuotedLiteralResult) .
490            (family StreamingStructuralState))
491          (Compiler.QuotedLiteral/quotedValidateSourceAtom recoveryAtom)
492          (branch
493            QuotedLiteralDecoded
494            payload
495            .
496            (constructor
497              StreamingStructuralState
498              StreamingStructuralFailed
499              streamingFailureCode
500              structuralFailureOrigin
501              b""
502              (constructor SyntaxOrigin SyntaxOriginUnknown)))
503          (branch
504            QuotedLiteralFailed
505            failure
506            start
507            end
508            .
509            (constructor
510              StreamingStructuralState
511              StreamingStructuralFailed
512              (Compiler.QuotedLiteral/quotedLiteralFailureCode failure)
513              (syntaxOriginRebaseRange recoveryOrigin start end)
514              b""
515              (constructor SyntaxOrigin SyntaxOriginUnknown)))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.