First-order exponent tail. The three `bytes-eliminate` reads (the exponent
marker over the whole remaining input, and the optional sign over its tail)
forced their ignored tail-inductions -- a re-walk of the remaining per call,
on a path taken for EVERY number. Each is now an O(1) `bytes-head` /
`bytes-tail` peek guarded by emptiness. The emitted number bytes are unchanged.
941def jsonParseNumberExponent =
942 (lambda unrestricted prefix : BytesBuilder .
943 (lambda unrestricted input : Bytes .
944 (nat-eliminate
945 (lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
946 (app
947 (lambda unrestricted marker : Byte .
948 (app
949 (lambda unrestricted tail : Bytes .
950 (nat-eliminate
951 (lambda unrestricted exponent : Nat . (family JSONNumberParseResult))
952 (constructor
953 JSONNumberParseResult
954 JSONNumberParsed
955 (bytes-builder-build prefix)
956 (bytes-cons marker tail))
957 (lambda unrestricted exponentPredecessor : Nat .
958 (lambda unrestricted exponentInduction : (family JSONNumberParseResult) .
959 (app
960 (lambda unrestricted signedPrefix : BytesBuilder .
961 (app
962 (lambda unrestricted afterSign : Bytes .
963 (eliminate
964 JSONDigitSplit
965 (lambda unrestricted current : (family JSONDigitSplit) .
966 (family JSONNumberParseResult))
967 (jsonTakeDigits afterSign)
968 (branch
969 JSONDigitSplitValue
970 digits
971 remaining
972 count
973 .
974 (nat-eliminate
975 (lambda unrestricted nonempty : Nat .
976 (family JSONNumberParseResult))
977 (jsonNumberFailure
978 (constructor JSONErrorCode JSONNumberExponentDigitsMissing)
979 afterSign)
980 (lambda unrestricted predecessor : Nat .
981 (lambda unrestricted induction : (family JSONNumberParseResult) .
982 (constructor
983 JSONNumberParseResult
984 JSONNumberParsed
985 (bytes-builder-build
986 (bytes-builder-append signedPrefix digits))
987 remaining)))
988 count))))
989 (nat-eliminate
990 (lambda unrestricted signNonEmpty : Nat . Bytes)
991 (app
992 (lambda unrestricted sign : Byte .
993 (app
994 (lambda unrestricted signTail : Bytes .
995 (nat-eliminate
996 (lambda unrestricted signed : Nat . Bytes)
997 tail
998 (lambda unrestricted predecessor : Nat .
999 (lambda unrestricted induction : Bytes . signTail))
1000 (jsonFlagOr
1001 (byte-equal sign (byte 43))
1002 (byte-equal sign (byte 45)))))
1003 (bytes-tail tail)))
1004 (bytes-head tail))
1005 (lambda unrestricted signEmptyPredecessor : Nat .
1006 (lambda unrestricted signEmptyInduction : Bytes . tail))
1007 (naturalIsZero (bytes-length tail)))))
1008 (bytes-builder-append
1009 prefix
1010 (bytes-builder-chunk
1011 (nat-eliminate
1012 (lambda unrestricted signNonEmpty : Nat . Bytes)
1013 (app
1014 (lambda unrestricted sign : Byte .
1015 (app
1016 (lambda unrestricted signTail : Bytes .
1017 (nat-eliminate
1018 (lambda unrestricted signed : Nat . Bytes)
1019 (bytes-cons marker b"")
1020 (lambda unrestricted predecessor : Nat .
1021 (lambda unrestricted induction : Bytes .
1022 (bytes-cons marker (bytes-cons sign b""))))
1023 (jsonFlagOr
1024 (byte-equal sign (byte 43))
1025 (byte-equal sign (byte 45)))))
1026 (bytes-tail tail)))
1027 (bytes-head tail))
1028 (lambda unrestricted signEmptyPredecessor : Nat .
1029 (lambda unrestricted signEmptyInduction : Bytes .
1030 (bytes-cons marker b"")))
1031 (naturalIsZero (bytes-length tail))))))))
1032 (jsonFlagOr (byte-equal marker (byte 101)) (byte-equal marker (byte 69)))))
1033 (bytes-tail input)))
1034 (bytes-head input))
1035 (lambda unrestricted emptyPredecessor : Nat .
1036 (lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
1037 (constructor
1038 JSONNumberParseResult
1039 JSONNumberParsed
1040 (bytes-builder-build prefix)
1041 b"")))
1042 (naturalIsZero (bytes-length input)))))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.