module Compiler.QuotedLiteral import Compiler.IntegerLiteral import Std.Natural import Data.UTF8 import Model.Config import Model.Word32 import Std.Byte import Std.Foundation family QuotedLiteralFailure : Type 0 constructor QuotedInvalidPrefix constructor QuotedUnknownEscape constructor QuotedIncompleteEscape constructor QuotedBadHex constructor QuotedNonASCII constructor QuotedNewline constructor QuotedUnterminated constructor QuotedTrailingInput constructor QuotedUnicodeSyntax constructor QuotedInvalidScalar constructor QuotedInvalidUTF8 end-family family QuotedLiteralResult : Type 0 constructor QuotedLiteralDecoded field unrestricted quotedDecodedBytes : Bytes constructor QuotedLiteralFailed field unrestricted quotedFailure : (family QuotedLiteralFailure) field unrestricted quotedFailureByte : Nat field unrestricted quotedFailureEndByte : Nat end-family family QuotedByteState : Type 0 constructor QuotedNormal constructor QuotedEscape field unrestricted escapeStart : Nat constructor QuotedHexHigh field unrestricted hexStart : Nat constructor QuotedHexLow field unrestricted lowHexStart : Nat field unrestricted highHexDigit : Nat constructor QuotedFailureTail field unrestricted failureTailKind : (family QuotedLiteralFailure) field unrestricted failureTailStart : Nat field unrestricted failureTailRemaining : Nat constructor QuotedClosed end-family family QuotedTextState : Type 0 constructor QuotedTextNormal constructor QuotedTextEscape field unrestricted textEscapeStart : Nat constructor QuotedTextUnicodeOpen field unrestricted unicodeOpenStart : Nat constructor QuotedTextUnicodeDigits field unrestricted unicodeDigitsStart : Nat field unrestricted unicodeDigitCount : Nat field unrestricted unicodeAccumulator : (family ModelWord32) constructor QuotedTextClosed end-family -- Continuations are forced only for the selected transition. def quotedChoose = (lambda unrestricted condition : Nat . (lambda unrestricted yes : (pi unrestricted force : Nat . (family QuotedLiteralResult)) . (lambda unrestricted no : (pi unrestricted force : Nat . (family QuotedLiteralResult)) . (app (nat-eliminate (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . (family QuotedLiteralResult))) no (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . (family QuotedLiteralResult)) . yes)) condition) zero)))) def quotedPrepend = (lambda unrestricted head : Byte . (lambda unrestricted result : (family QuotedLiteralResult) . (eliminate QuotedLiteralResult (lambda unrestricted value : (family QuotedLiteralResult) . (family QuotedLiteralResult)) result (branch QuotedLiteralDecoded bytes . (constructor QuotedLiteralResult QuotedLiteralDecoded (bytes-cons head bytes))) (branch QuotedLiteralFailed failure offset endOffset . (constructor QuotedLiteralResult QuotedLiteralFailed failure offset endOffset))))) -- A quoted recovery fragment stops before a delimiter or physical newline. def quotedRecoveryBoundary = (lambda unrestricted value : Byte . (Std.Natural/naturalOr (byte-equal value (byte 34)) (Std.Natural/naturalOr (byte-equal value (byte 10)) (byte-equal value (byte 13))))) def quotedByteStep = (lambda unrestricted head : Byte . (lambda unrestricted state : (family QuotedByteState) . (lambda unrestricted offset : Nat . (lambda unrestricted continue : (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) . (eliminate QuotedByteState (lambda unrestricted current : (family QuotedByteState) . (family QuotedLiteralResult)) state (branch QuotedNormal . (quotedChoose (byte-equal head (byte 13)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedNewline) offset (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 10)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedNewline) offset (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 34)) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedClosed) (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 92)) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedEscape offset) (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-less-than head (byte 128)) (lambda unrestricted force : Nat . (quotedPrepend head (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedFailureTail (constructor QuotedLiteralFailure QuotedNonASCII) offset zero) (succ offset))))))))))))) (branch QuotedEscape start . (quotedChoose (byte-equal head (byte 13)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedNewline) offset (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 10)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedNewline) offset (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 92)) (lambda unrestricted force : Nat . (quotedPrepend (byte 92) (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 34)) (lambda unrestricted force : Nat . (quotedPrepend (byte 34) (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 114)) (lambda unrestricted force : Nat . (quotedPrepend (byte 13) (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 116)) (lambda unrestricted force : Nat . (quotedPrepend (byte 9) (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 110)) (lambda unrestricted force : Nat . (quotedPrepend (byte 10) (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 120)) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedHexHigh start) (succ offset))) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedFailureTail (constructor QuotedLiteralFailure QuotedUnknownEscape) start zero) (succ offset))))))))))))))))))) (branch QuotedHexHigh start . (eliminate IntegerLiteralDigitResult (lambda unrestricted decoded : (family IntegerLiteralDigitResult) . (family QuotedLiteralResult)) (Compiler.IntegerLiteral/integerLiteralDecodeHex head) (branch IntegerLiteralDigitValue digit . (continue (constructor QuotedByteState QuotedHexLow start digit) (succ offset))) (branch IntegerLiteralDigitFailed failure . (quotedChoose (quotedRecoveryBoundary head) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedBadHex) start offset)) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedFailureTail (constructor QuotedLiteralFailure QuotedBadHex) start (succ zero)) (succ offset))))))) (branch QuotedHexLow start high . (eliminate IntegerLiteralDigitResult (lambda unrestricted decoded : (family IntegerLiteralDigitResult) . (family QuotedLiteralResult)) (Compiler.IntegerLiteral/integerLiteralDecodeHex head) (branch IntegerLiteralDigitValue digit . (quotedPrepend (nat-to-byte (Std.Natural/naturalAdd (Std.Natural/naturalMultiply high (byte-to-nat (byte 16))) digit)) (continue (constructor QuotedByteState QuotedNormal) (succ offset)))) (branch IntegerLiteralDigitFailed failure . (quotedChoose (quotedRecoveryBoundary head) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedBadHex) start offset)) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedFailureTail (constructor QuotedLiteralFailure QuotedBadHex) start zero) (succ offset))))))) (branch QuotedFailureTail failure start remaining . (quotedChoose (Data.UTF8/utf8ContinuationValid head) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedFailureTail failure start remaining) (succ offset))) (lambda unrestricted force : Nat . (quotedChoose remaining (lambda unrestricted force : Nat . (quotedChoose (quotedRecoveryBoundary head) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset)) (lambda unrestricted force : Nat . (continue (constructor QuotedByteState QuotedFailureTail failure start zero) (succ offset))))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset)))))) (branch QuotedClosed . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedTrailingInput) offset (succ offset)))))))) def quotedByteFinish = (lambda unrestricted state : (family QuotedByteState) . (lambda unrestricted offset : Nat . (eliminate QuotedByteState (lambda unrestricted current : (family QuotedByteState) . (family QuotedLiteralResult)) state (branch QuotedNormal . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnterminated) zero offset)) (branch QuotedEscape start . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedIncompleteEscape) start offset)) (branch QuotedHexHigh start . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedBadHex) start offset)) (branch QuotedHexLow start high . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedBadHex) start offset)) (branch QuotedFailureTail failure start remaining . (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset)) (branch QuotedClosed . (constructor QuotedLiteralResult QuotedLiteralDecoded b""))))) -- Input includes its closing quote; the full-spelling byte offset starts at2. def decodeByteLiteralBody = (lambda unrestricted body : Bytes . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult)))) quotedByteFinish (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) . (lambda unrestricted state : (family QuotedByteState) . (lambda unrestricted offset : Nat . (quotedByteStep head state offset continue)))))) body) (constructor QuotedByteState QuotedNormal) (succ (succ zero)))) def quotedDecodeByteLiteral = (lambda unrestricted spelling : Bytes . (quotedChoose (byte-equal (bytes-head spelling) (byte 98)) (lambda unrestricted force : Nat . (quotedChoose (byte-equal (bytes-head (bytes-tail spelling)) (byte 34)) (lambda unrestricted force : Nat . (decodeByteLiteralBody (bytes-tail (bytes-tail spelling)))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedInvalidPrefix) zero zero)))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedInvalidPrefix) zero zero)))) -- Stable parser failure tags; the result above retains the exact byte offset. def quotedLiteralFailureCode = (lambda unrestricted failure : (family QuotedLiteralFailure) . (eliminate QuotedLiteralFailure (lambda unrestricted current : (family QuotedLiteralFailure) . Nat) failure (branch QuotedInvalidPrefix . (byte-to-nat (byte 91))) (branch QuotedUnknownEscape . (byte-to-nat (byte 92))) (branch QuotedIncompleteEscape . (byte-to-nat (byte 93))) (branch QuotedBadHex . (byte-to-nat (byte 94))) (branch QuotedNonASCII . (byte-to-nat (byte 95))) (branch QuotedNewline . (byte-to-nat (byte 96))) (branch QuotedUnterminated . (byte-to-nat (byte 97))) (branch QuotedTrailingInput . (byte-to-nat (byte 98))) (branch QuotedUnicodeSyntax . (byte-to-nat (byte 99))) (branch QuotedInvalidScalar . (byte-to-nat (byte 100))) (branch QuotedInvalidUTF8 . (byte-to-nat (byte 101))))) -- Prepend an encoded scalar without changing the following failure location. def quotedPrependBytes = (lambda unrestricted prefix : Bytes . (lambda unrestricted result : (family QuotedLiteralResult) . (eliminate QuotedLiteralResult (lambda unrestricted current : (family QuotedLiteralResult) . (family QuotedLiteralResult)) result (branch QuotedLiteralDecoded suffix . (constructor QuotedLiteralResult QuotedLiteralDecoded (bytes-append prefix suffix))) (branch QuotedLiteralFailed failure offset endOffset . (constructor QuotedLiteralResult QuotedLiteralFailed failure offset endOffset))))) -- Each hex digit shifts four bits once; six digits fit in the 24 low bits. def quotedAppendHexDigit = (lambda unrestricted word : (family ModelWord32) . (lambda unrestricted digit : Nat . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32)) word (branch ModelWord32Value b0 b1 b2 b3 . (constructor ModelWord32 ModelWord32Value (nat-to-byte (Std.Natural/naturalAdd (byte-to-nat (Std.Byte/byteShiftLeftTruncated b0 (byte-to-nat (byte 4)))) digit)) (Std.Byte/byteOr (Std.Byte/byteShiftLeftTruncated b1 (byte-to-nat (byte 4))) (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 4)))) (Std.Byte/byteOr (Std.Byte/byteShiftLeftTruncated b2 (byte-to-nat (byte 4))) (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4)))) (Std.Byte/byteOr (Std.Byte/byteShiftLeftTruncated b3 (byte-to-nat (byte 4))) (Std.Byte/byteShiftRight b2 (byte-to-nat (byte 4))))))))) -- Keep scalar arithmetic bounded while consuming the complete malformed escape. def quotedAppendBoundedHexDigit = (lambda unrestricted count : Nat . (lambda unrestricted accumulator : (family ModelWord32) . (lambda unrestricted digit : Nat . (nat-eliminate (lambda unrestricted condition : Nat . (family ModelWord32)) accumulator (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ModelWord32) . (quotedAppendHexDigit accumulator digit))) (nat-less-than count (byte-to-nat (byte 6))))))) -- This helper is used only after decodeUTF8 validates the full Text spelling. def quotedValidatedScalarEnd = (lambda unrestricted head : Byte . (lambda unrestricted offset : Nat . (Std.Natural/naturalAdd offset (Std.Natural/naturalSelect (Data.UTF8/utf8LeadFourValid head) (byte-to-nat (byte 4)) (Std.Natural/naturalSelect (Data.UTF8/utf8LeadThreeValid head) (byte-to-nat (byte 3)) (Std.Natural/naturalSelect (Data.UTF8/utf8LeadTwoValid head) (byte-to-nat (byte 2)) (succ zero))))))) def quotedTextStep = (lambda unrestricted head : Byte . (lambda unrestricted state : (family QuotedTextState) . (lambda unrestricted offset : Nat . (lambda unrestricted continue : (pi unrestricted state : (family QuotedTextState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) . (quotedChoose (byte-equal head (byte 13)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedNewline) offset (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 10)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedNewline) offset (succ offset))) (lambda unrestricted force : Nat . (eliminate QuotedTextState (lambda unrestricted current : (family QuotedTextState) . (family QuotedLiteralResult)) state (branch QuotedTextNormal . (quotedChoose (byte-equal head (byte 34)) (lambda unrestricted force : Nat . (continue (constructor QuotedTextState QuotedTextClosed) (succ offset))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 92)) (lambda unrestricted force : Nat . (continue (constructor QuotedTextState QuotedTextEscape offset) (succ offset))) (lambda unrestricted force : Nat . (quotedPrepend head (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))))))) (branch QuotedTextEscape start . (quotedChoose (byte-equal head (byte 92)) (lambda unrestricted force : Nat . (quotedPrepend (byte 92) (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 34)) (lambda unrestricted force : Nat . (quotedPrepend (byte 34) (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 114)) (lambda unrestricted force : Nat . (quotedPrepend (byte 13) (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 116)) (lambda unrestricted force : Nat . (quotedPrepend (byte 9) (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 110)) (lambda unrestricted force : Nat . (quotedPrepend (byte 10) (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))) (lambda unrestricted force : Nat . (quotedChoose (byte-equal head (byte 117)) (lambda unrestricted force : Nat . (continue (constructor QuotedTextState QuotedTextUnicodeOpen start) (succ offset))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnknownEscape) start (quotedValidatedScalarEnd head offset))))))))))))))) (branch QuotedTextUnicodeOpen start . (quotedChoose (byte-equal head (byte 123)) (lambda unrestricted force : Nat . (continue (constructor QuotedTextState QuotedTextUnicodeDigits start zero Model.Word32/modelWord32Zero) (succ offset))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnicodeSyntax) start offset)))) (branch QuotedTextUnicodeDigits start count accumulator . (quotedChoose (byte-equal head (byte 125)) (lambda unrestricted force : Nat . (quotedChoose (Std.Natural/naturalAnd count (nat-less-than count (byte-to-nat (byte 7)))) (lambda unrestricted force : Nat . (eliminate UTF8CodepointEncodeResult (lambda unrestricted encoded : (family UTF8CodepointEncodeResult) . (family QuotedLiteralResult)) (Data.UTF8/utf8EncodeCodepoint (constructor UTF8Codepoint UTF8CodepointValue accumulator)) (branch UTF8CodepointEncoded bytes . (quotedPrependBytes bytes (continue (constructor QuotedTextState QuotedTextNormal) (succ offset)))) (branch UTF8CodepointRejected failure . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedInvalidScalar) start (succ offset))))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnicodeSyntax) start (succ offset))))) (lambda unrestricted force : Nat . (eliminate IntegerLiteralDigitResult (lambda unrestricted decoded : (family IntegerLiteralDigitResult) . (family QuotedLiteralResult)) (Compiler.IntegerLiteral/integerLiteralDecodeHex head) (branch IntegerLiteralDigitValue digit . (continue (constructor QuotedTextState QuotedTextUnicodeDigits start (succ count) (quotedAppendBoundedHexDigit count accumulator digit)) (succ offset))) (branch IntegerLiteralDigitFailed failure . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnicodeSyntax) start offset)))))) (branch QuotedTextClosed . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedTrailingInput) offset (succ offset)))))))))))) def quotedTextFinish = (lambda unrestricted state : (family QuotedTextState) . (lambda unrestricted offset : Nat . (eliminate QuotedTextState (lambda unrestricted current : (family QuotedTextState) . (family QuotedLiteralResult)) state (branch QuotedTextNormal . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnterminated) zero offset)) (branch QuotedTextEscape start . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedIncompleteEscape) start offset)) (branch QuotedTextUnicodeOpen start . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnicodeSyntax) start offset)) (branch QuotedTextUnicodeDigits start count accumulator . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedUnicodeSyntax) start offset)) (branch QuotedTextClosed . (constructor QuotedLiteralResult QuotedLiteralDecoded b""))))) def quotedDecodeTextBody = (lambda unrestricted body : Bytes . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted state : (family QuotedTextState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult)))) quotedTextFinish (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted state : (family QuotedTextState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) . (lambda unrestricted state : (family QuotedTextState) . (lambda unrestricted offset : Nat . (quotedTextStep head state offset continue)))))) body) (constructor QuotedTextState QuotedTextNormal) (succ zero))) def quotedDecodeTextLiteral = (lambda unrestricted spelling : Bytes . (eliminate UTF8DecodeResult (lambda unrestricted decoded : (family UTF8DecodeResult) . (family QuotedLiteralResult)) (Data.UTF8/decodeUTF8 spelling) (branch UTF8DecodeSucceeded points . (quotedChoose (byte-equal (bytes-head spelling) (byte 34)) (lambda unrestricted force : Nat . (quotedDecodeTextBody (bytes-tail spelling))) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedInvalidPrefix) zero zero)))) (branch UTF8DecodeFailed failure offset . (constructor QuotedLiteralResult QuotedLiteralFailed (constructor QuotedLiteralFailure QuotedInvalidUTF8) (Model.Word32/modelWord32ToNatural offset) (succ (Model.Word32/modelWord32ToNatural offset)))))) -- Stable diagnostics for the closed literal failure vocabulary; other parser -- failures retain their caller-owned code. def quotedLiteralDiagnosticCode = (lambda unrestricted code : Nat . (lambda unrestricted fallback : Bytes . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes)) (lambda unrestricted force : Nat . fallback) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-SOURCE-INVALID-UTF8"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedInvalidUTF8)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-SCALAR"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedInvalidScalar)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-UNICODE-ESCAPE"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedUnicodeSyntax)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-UNTERMINATED"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedUnterminated)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-NEWLINE"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedNewline)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-BYTES-NON-ASCII"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedNonASCII)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-BYTE-ESCAPE"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedBadHex)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-INCOMPLETE-ESCAPE"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedIncompleteEscape)))) zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) . (lambda unrestricted force : Nat . b"ALPHA-LITERAL-UNKNOWN-ESCAPE"))) (Std.Natural/naturalEqual code (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedUnknownEscape)))) zero))) -- Structural lexing validates only quoted atoms; unquoted spelling is unchanged. def quotedValidateSourceAtom = (lambda unrestricted spelling : Bytes . (quotedChoose (byte-equal (bytes-head spelling) (byte 34)) (lambda unrestricted force : Nat . (quotedDecodeTextLiteral spelling)) (lambda unrestricted force : Nat . (quotedChoose (Std.Natural/naturalAnd (byte-equal (bytes-head spelling) (byte 98)) (byte-equal (bytes-head (bytes-tail spelling)) (byte 34))) (lambda unrestricted force : Nat . (quotedDecodeByteLiteral spelling)) (lambda unrestricted force : Nat . (constructor QuotedLiteralResult QuotedLiteralDecoded spelling))))))