1module Data.JSONAccess
2
3import Data.Bytes
4import Data.JSON
5import Data.UTF8
6import Model.Parameter
7import Model.Word64
8import Std.Natural
9
10family JSONMemberLookupResult : Type 0
11constructor JSONMemberMissing
12constructor JSONMemberFound
13field unrestricted jsonMemberFoundValue : (family JSON)
14constructor JSONMemberDuplicated
15constructor JSONMemberTreeMalformed
16
17end-family
18
19family JSONValueAccessResult : Type 0
20constructor JSONValueAccessSucceeded
21field unrestricted jsonAccessedValue : (family JSON)
22constructor JSONValueAccessFailed
23field unrestricted jsonValueAccessError : (family JSONErrorCode)
24
25end-family
26
27family JSONBytesAccessResult : Type 0
28constructor JSONBytesAccessSucceeded
29field unrestricted jsonAccessedBytes : Bytes
30constructor JSONBytesAccessFailed
31field unrestricted jsonBytesAccessError : (family JSONErrorCode)
32
33end-family
34
35family JSONArrayAccessResult : Type 0
36constructor JSONArrayAccessSucceeded
37field unrestricted jsonAccessedArrayValues : (family JSON)
38constructor JSONArrayAccessFailed
39field unrestricted jsonArrayAccessError : (family JSONErrorCode)
40
41end-family
42
43family JSONObjectAccessResult : Type 0
44constructor JSONObjectAccessSucceeded
45field unrestricted jsonAccessedObjectMembers : (family JSON)
46constructor JSONObjectAccessFailed
47field unrestricted jsonObjectAccessError : (family JSONErrorCode)
48
49end-family
50
51family JSONBooleanAccessResult : Type 0
52constructor JSONBooleanAccessSucceeded
53field unrestricted jsonAccessedBoolean : Nat
54constructor JSONBooleanAccessFailed
55field unrestricted jsonBooleanAccessError : (family JSONErrorCode)
56
57end-family
58
59family JSONNullAccessResult : Type 0
60constructor JSONNullAccessSucceeded
61constructor JSONNullAccessFailed
62field unrestricted jsonNullAccessError : (family JSONErrorCode)
63
64end-family
65
66family JSONInteger : Type 0
67constructor JSONIntegerValue
68field unrestricted jsonIntegerNegative : Nat
69field unrestricted jsonIntegerMagnitude : Nat
70
71end-family
72
73family JSONIntegerFoldResult : Type 0
74constructor JSONIntegerFoldSucceeded
75field unrestricted jsonIntegerFoldMagnitude : Nat
76field unrestricted jsonIntegerFoldDigits : Nat
77constructor JSONIntegerFoldFailed
78
79end-family
80
81family JSONIntegerAccessResult : Type 0
82constructor JSONIntegerAccessSucceeded
83field unrestricted jsonAccessedInteger : (family JSONInteger)
84constructor JSONIntegerAccessFailed
85field unrestricted jsonIntegerAccessError : (family JSONErrorCode)
86
87end-family
88
89family JSONWord64AccessResult : Type 0
90constructor JSONWord64AccessSucceeded
91field unrestricted jsonAccessedWord64 : (family ModelWord64)
92constructor JSONWord64AccessFailed
93field unrestricted jsonWord64AccessError : (family JSONErrorCode)
94end-family
95
96def jsonLookupMembers =
97 (lambda unrestricted wanted : Bytes .
98 (lambda unrestricted members : (family JSON) .
99 (eliminate
100 JSON
101 (lambda unrestricted current : (family JSON) . (family JSONMemberLookupResult))
102 members
103 (branch
104 JSONObject
105 nested
106 nestedInduction
107 .
108 (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
109 (branch JSONObjectEnd . (constructor JSONMemberLookupResult JSONMemberMissing))
110 (branch
111 JSONObjectMember
112 key
113 value
114 tail
115 valueInduction
116 tailInduction
117 .
118 (nat-eliminate
119 (lambda unrestricted matches : Nat . (family JSONMemberLookupResult))
120 tailInduction
121 (lambda unrestricted predecessor : Nat .
122 (lambda unrestricted induction : (family JSONMemberLookupResult) .
123 (eliminate
124 JSONMemberLookupResult
125 (lambda unrestricted current : (family JSONMemberLookupResult) .
126 (family JSONMemberLookupResult))
127 tailInduction
128 (branch
129 JSONMemberMissing
130 .
131 (constructor JSONMemberLookupResult JSONMemberFound value))
132 (branch
133 JSONMemberFound
134 duplicateValue
135 .
136 (constructor JSONMemberLookupResult JSONMemberDuplicated))
137 (branch
138 JSONMemberDuplicated
139 .
140 (constructor JSONMemberLookupResult JSONMemberDuplicated))
141 (branch
142 JSONMemberTreeMalformed
143 .
144 (constructor JSONMemberLookupResult JSONMemberTreeMalformed)))))
145 (bytes-equal wanted key)))
146 (branch
147 JSONArray
148 values
149 valuesInduction
150 .
151 (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
152 (branch JSONArrayEnd . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
153 (branch
154 JSONArrayNext
155 head
156 tail
157 headInduction
158 tailInduction
159 .
160 (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
161 (branch JSONString text . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
162 (branch JSONNumber number . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
163 (branch JSONBoolean value . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
164 (branch JSONNull . (constructor JSONMemberLookupResult JSONMemberTreeMalformed)))))
165
166def objectLookup =
167 (lambda unrestricted wanted : Bytes .
168 (lambda unrestricted value : (family JSON) .
169 (eliminate
170 JSON
171 (lambda unrestricted current : (family JSON) . (family JSONValueAccessResult))
172 value
173 (branch
174 JSONObject
175 members
176 membersInduction
177 .
178 (eliminate
179 JSONMemberLookupResult
180 (lambda unrestricted current : (family JSONMemberLookupResult) .
181 (family JSONValueAccessResult))
182 (jsonLookupMembers wanted members)
183 (branch
184 JSONMemberMissing
185 .
186 (constructor
187 JSONValueAccessResult
188 JSONValueAccessFailed
189 (constructor JSONErrorCode JSONMissingMember)))
190 (branch
191 JSONMemberFound
192 member
193 .
194 (constructor JSONValueAccessResult JSONValueAccessSucceeded member))
195 (branch
196 JSONMemberDuplicated
197 .
198 (constructor
199 JSONValueAccessResult
200 JSONValueAccessFailed
201 (constructor JSONErrorCode JSONDuplicateMember)))
202 (branch
203 JSONMemberTreeMalformed
204 .
205 (constructor
206 JSONValueAccessResult
207 JSONValueAccessFailed
208 (constructor JSONErrorCode JSONMalformedTree)))))
209 (branch
210 JSONObjectEnd
211 .
212 (constructor
213 JSONValueAccessResult
214 JSONValueAccessFailed
215 (constructor JSONErrorCode JSONExpectedObject)))
216 (branch
217 JSONObjectMember
218 key
219 member
220 tail
221 memberInduction
222 tailInduction
223 .
224 (constructor
225 JSONValueAccessResult
226 JSONValueAccessFailed
227 (constructor JSONErrorCode JSONExpectedObject)))
228 (branch
229 JSONArray
230 values
231 valuesInduction
232 .
233 (constructor
234 JSONValueAccessResult
235 JSONValueAccessFailed
236 (constructor JSONErrorCode JSONExpectedObject)))
237 (branch
238 JSONArrayEnd
239 .
240 (constructor
241 JSONValueAccessResult
242 JSONValueAccessFailed
243 (constructor JSONErrorCode JSONExpectedObject)))
244 (branch
245 JSONArrayNext
246 head
247 tail
248 headInduction
249 tailInduction
250 .
251 (constructor
252 JSONValueAccessResult
253 JSONValueAccessFailed
254 (constructor JSONErrorCode JSONExpectedObject)))
255 (branch
256 JSONString
257 text
258 .
259 (constructor
260 JSONValueAccessResult
261 JSONValueAccessFailed
262 (constructor JSONErrorCode JSONExpectedObject)))
263 (branch
264 JSONNumber
265 number
266 .
267 (constructor
268 JSONValueAccessResult
269 JSONValueAccessFailed
270 (constructor JSONErrorCode JSONExpectedObject)))
271 (branch
272 JSONBoolean
273 boolean
274 .
275 (constructor
276 JSONValueAccessResult
277 JSONValueAccessFailed
278 (constructor JSONErrorCode JSONExpectedObject)))
279 (branch
280 JSONNull
281 .
282 (constructor
283 JSONValueAccessResult
284 JSONValueAccessFailed
285 (constructor JSONErrorCode JSONExpectedObject))))))
286
287def jsonObject =
288 (lambda unrestricted value : (family JSON) .
289 (eliminate
290 JSON
291 (lambda unrestricted current : (family JSON) . (family JSONObjectAccessResult))
292 value
293 (branch
294 JSONObject
295 members
296 membersInduction
297 .
298 (eliminate
299 JSONTreeAuditResult
300 (lambda unrestricted current : (family JSONTreeAuditResult) .
301 (family JSONObjectAccessResult))
302 (jsonAuditTreeWithTokenLimits
303 (constructor JSONBound JSONBoundBelowTwoPower jsonNaturalTwenty)
304 (constructor JSONBound JSONBoundAtMost jsonNaturalOneThousandTwentyFour)
305 (constructor JSONBound JSONBoundAtMost jsonNaturalSixtyFiveThousandFiveHundredThirtySix)
306 value)
307 (branch
308 JSONTreeAuditSucceeded
309 kind
310 counts
311 depth
312 sequenceCount
313 .
314 (constructor JSONObjectAccessResult JSONObjectAccessSucceeded members))
315 (branch
316 JSONTreeAuditFailed
317 code
318 .
319 (constructor JSONObjectAccessResult JSONObjectAccessFailed code))))
320 (branch
321 JSONObjectEnd
322 .
323 (constructor
324 JSONObjectAccessResult
325 JSONObjectAccessFailed
326 (constructor JSONErrorCode JSONExpectedObject)))
327 (branch
328 JSONObjectMember
329 key
330 member
331 tail
332 memberInduction
333 tailInduction
334 .
335 (constructor
336 JSONObjectAccessResult
337 JSONObjectAccessFailed
338 (constructor JSONErrorCode JSONExpectedObject)))
339 (branch
340 JSONArray
341 values
342 valuesInduction
343 .
344 (constructor
345 JSONObjectAccessResult
346 JSONObjectAccessFailed
347 (constructor JSONErrorCode JSONExpectedObject)))
348 (branch
349 JSONArrayEnd
350 .
351 (constructor
352 JSONObjectAccessResult
353 JSONObjectAccessFailed
354 (constructor JSONErrorCode JSONExpectedObject)))
355 (branch
356 JSONArrayNext
357 head
358 tail
359 headInduction
360 tailInduction
361 .
362 (constructor
363 JSONObjectAccessResult
364 JSONObjectAccessFailed
365 (constructor JSONErrorCode JSONExpectedObject)))
366 (branch
367 JSONString
368 text
369 .
370 (constructor
371 JSONObjectAccessResult
372 JSONObjectAccessFailed
373 (constructor JSONErrorCode JSONExpectedObject)))
374 (branch
375 JSONNumber
376 number
377 .
378 (constructor
379 JSONObjectAccessResult
380 JSONObjectAccessFailed
381 (constructor JSONErrorCode JSONExpectedObject)))
382 (branch
383 JSONBoolean
384 boolean
385 .
386 (constructor
387 JSONObjectAccessResult
388 JSONObjectAccessFailed
389 (constructor JSONErrorCode JSONExpectedObject)))
390 (branch
391 JSONNull
392 .
393 (constructor
394 JSONObjectAccessResult
395 JSONObjectAccessFailed
396 (constructor JSONErrorCode JSONExpectedObject)))))
397
398def jsonString =
399 (lambda unrestricted value : (family JSON) .
400 (eliminate
401 JSON
402 (lambda unrestricted current : (family JSON) . (family JSONBytesAccessResult))
403 value
404 (branch
405 JSONObject
406 members
407 membersInduction
408 .
409 (constructor
410 JSONBytesAccessResult
411 JSONBytesAccessFailed
412 (constructor JSONErrorCode JSONExpectedString)))
413 (branch
414 JSONObjectEnd
415 .
416 (constructor
417 JSONBytesAccessResult
418 JSONBytesAccessFailed
419 (constructor JSONErrorCode JSONExpectedString)))
420 (branch
421 JSONObjectMember
422 key
423 member
424 tail
425 memberInduction
426 tailInduction
427 .
428 (constructor
429 JSONBytesAccessResult
430 JSONBytesAccessFailed
431 (constructor JSONErrorCode JSONExpectedString)))
432 (branch
433 JSONArray
434 values
435 valuesInduction
436 .
437 (constructor
438 JSONBytesAccessResult
439 JSONBytesAccessFailed
440 (constructor JSONErrorCode JSONExpectedString)))
441 (branch
442 JSONArrayEnd
443 .
444 (constructor
445 JSONBytesAccessResult
446 JSONBytesAccessFailed
447 (constructor JSONErrorCode JSONExpectedString)))
448 (branch
449 JSONArrayNext
450 head
451 tail
452 headInduction
453 tailInduction
454 .
455 (constructor
456 JSONBytesAccessResult
457 JSONBytesAccessFailed
458 (constructor JSONErrorCode JSONExpectedString)))
459 (branch
460 JSONString
461 text
462 .
463 (eliminate
464 UTF8DecodeResult
465 (lambda unrestricted current : (family UTF8DecodeResult) . (family JSONBytesAccessResult))
466 (decodeUTF8 text)
467 (branch
468 UTF8DecodeSucceeded
469 codepoints
470 .
471 (constructor JSONBytesAccessResult JSONBytesAccessSucceeded text))
472 (branch
473 UTF8DecodeFailed
474 code
475 offset
476 .
477 (constructor
478 JSONBytesAccessResult
479 JSONBytesAccessFailed
480 (constructor JSONErrorCode JSONInvalidUTF8)))))
481 (branch
482 JSONNumber
483 number
484 .
485 (constructor
486 JSONBytesAccessResult
487 JSONBytesAccessFailed
488 (constructor JSONErrorCode JSONExpectedString)))
489 (branch
490 JSONBoolean
491 boolean
492 .
493 (constructor
494 JSONBytesAccessResult
495 JSONBytesAccessFailed
496 (constructor JSONErrorCode JSONExpectedString)))
497 (branch
498 JSONNull
499 .
500 (constructor
501 JSONBytesAccessResult
502 JSONBytesAccessFailed
503 (constructor JSONErrorCode JSONExpectedString)))))
504
505def jsonArray =
506 (lambda unrestricted value : (family JSON) .
507 (eliminate
508 JSON
509 (lambda unrestricted current : (family JSON) . (family JSONArrayAccessResult))
510 value
511 (branch
512 JSONObject
513 members
514 membersInduction
515 .
516 (constructor
517 JSONArrayAccessResult
518 JSONArrayAccessFailed
519 (constructor JSONErrorCode JSONExpectedArray)))
520 (branch
521 JSONObjectEnd
522 .
523 (constructor
524 JSONArrayAccessResult
525 JSONArrayAccessFailed
526 (constructor JSONErrorCode JSONExpectedArray)))
527 (branch
528 JSONObjectMember
529 key
530 member
531 tail
532 memberInduction
533 tailInduction
534 .
535 (constructor
536 JSONArrayAccessResult
537 JSONArrayAccessFailed
538 (constructor JSONErrorCode JSONExpectedArray)))
539 (branch
540 JSONArray
541 values
542 valuesInduction
543 .
544 (constructor JSONArrayAccessResult JSONArrayAccessSucceeded values))
545 (branch
546 JSONArrayEnd
547 .
548 (constructor
549 JSONArrayAccessResult
550 JSONArrayAccessFailed
551 (constructor JSONErrorCode JSONExpectedArray)))
552 (branch
553 JSONArrayNext
554 head
555 tail
556 headInduction
557 tailInduction
558 .
559 (constructor
560 JSONArrayAccessResult
561 JSONArrayAccessFailed
562 (constructor JSONErrorCode JSONExpectedArray)))
563 (branch
564 JSONString
565 text
566 .
567 (constructor
568 JSONArrayAccessResult
569 JSONArrayAccessFailed
570 (constructor JSONErrorCode JSONExpectedArray)))
571 (branch
572 JSONNumber
573 number
574 .
575 (constructor
576 JSONArrayAccessResult
577 JSONArrayAccessFailed
578 (constructor JSONErrorCode JSONExpectedArray)))
579 (branch
580 JSONBoolean
581 boolean
582 .
583 (constructor
584 JSONArrayAccessResult
585 JSONArrayAccessFailed
586 (constructor JSONErrorCode JSONExpectedArray)))
587 (branch
588 JSONNull
589 .
590 (constructor
591 JSONArrayAccessResult
592 JSONArrayAccessFailed
593 (constructor JSONErrorCode JSONExpectedArray)))))
594
595def jsonNumber =
596 (lambda unrestricted value : (family JSON) .
597 (eliminate
598 JSON
599 (lambda unrestricted current : (family JSON) . (family JSONBytesAccessResult))
600 value
601 (branch
602 JSONObject
603 members
604 membersInduction
605 .
606 (constructor
607 JSONBytesAccessResult
608 JSONBytesAccessFailed
609 (constructor JSONErrorCode JSONExpectedNumber)))
610 (branch
611 JSONObjectEnd
612 .
613 (constructor
614 JSONBytesAccessResult
615 JSONBytesAccessFailed
616 (constructor JSONErrorCode JSONExpectedNumber)))
617 (branch
618 JSONObjectMember
619 key
620 member
621 tail
622 memberInduction
623 tailInduction
624 .
625 (constructor
626 JSONBytesAccessResult
627 JSONBytesAccessFailed
628 (constructor JSONErrorCode JSONExpectedNumber)))
629 (branch
630 JSONArray
631 values
632 valuesInduction
633 .
634 (constructor
635 JSONBytesAccessResult
636 JSONBytesAccessFailed
637 (constructor JSONErrorCode JSONExpectedNumber)))
638 (branch
639 JSONArrayEnd
640 .
641 (constructor
642 JSONBytesAccessResult
643 JSONBytesAccessFailed
644 (constructor JSONErrorCode JSONExpectedNumber)))
645 (branch
646 JSONArrayNext
647 head
648 tail
649 headInduction
650 tailInduction
651 .
652 (constructor
653 JSONBytesAccessResult
654 JSONBytesAccessFailed
655 (constructor JSONErrorCode JSONExpectedNumber)))
656 (branch
657 JSONString
658 text
659 .
660 (constructor
661 JSONBytesAccessResult
662 JSONBytesAccessFailed
663 (constructor JSONErrorCode JSONExpectedNumber)))
664 (branch
665 JSONNumber
666 number
667 .
668 (nat-eliminate
669 (lambda unrestricted bounded : Nat . (family JSONBytesAccessResult))
670 (constructor
671 JSONBytesAccessResult
672 JSONBytesAccessFailed
673 (constructor JSONErrorCode JSONNumberLimitExceeded))
674 (lambda unrestricted predecessor : Nat .
675 (lambda unrestricted induction : (family JSONBytesAccessResult) .
676 (eliminate
677 JSONNumberParseResult
678 (lambda unrestricted current : (family JSONNumberParseResult) .
679 (family JSONBytesAccessResult))
680 (jsonParseNumber number)
681 (branch
682 JSONNumberParsed
683 parsed
684 remaining
685 .
686 (nat-eliminate
687 (lambda unrestricted complete : Nat . (family JSONBytesAccessResult))
688 (constructor
689 JSONBytesAccessResult
690 JSONBytesAccessFailed
691 (constructor JSONErrorCode JSONExpectedNumber))
692 (lambda unrestricted completePredecessor : Nat .
693 (lambda unrestricted completeInduction : (family JSONBytesAccessResult) .
694 (constructor JSONBytesAccessResult JSONBytesAccessSucceeded parsed)))
695 (naturalIsZero (bytes-length remaining))))
696 (branch
697 JSONNumberParseFailed
698 code
699 remaining
700 .
701 (constructor JSONBytesAccessResult JSONBytesAccessFailed code)))))
702 (jsonNaturalLessThanOrEqual (bytes-length number) jsonNaturalOneThousandTwentyFour)))
703 (branch
704 JSONBoolean
705 boolean
706 .
707 (constructor
708 JSONBytesAccessResult
709 JSONBytesAccessFailed
710 (constructor JSONErrorCode JSONExpectedNumber)))
711 (branch
712 JSONNull
713 .
714 (constructor
715 JSONBytesAccessResult
716 JSONBytesAccessFailed
717 (constructor JSONErrorCode JSONExpectedNumber)))))
718
719def jsonBoolean =
720 (lambda unrestricted value : (family JSON) .
721 (eliminate
722 JSON
723 (lambda unrestricted current : (family JSON) . (family JSONBooleanAccessResult))
724 value
725 (branch
726 JSONObject
727 members
728 membersInduction
729 .
730 (constructor
731 JSONBooleanAccessResult
732 JSONBooleanAccessFailed
733 (constructor JSONErrorCode JSONExpectedBoolean)))
734 (branch
735 JSONObjectEnd
736 .
737 (constructor
738 JSONBooleanAccessResult
739 JSONBooleanAccessFailed
740 (constructor JSONErrorCode JSONExpectedBoolean)))
741 (branch
742 JSONObjectMember
743 key
744 member
745 tail
746 memberInduction
747 tailInduction
748 .
749 (constructor
750 JSONBooleanAccessResult
751 JSONBooleanAccessFailed
752 (constructor JSONErrorCode JSONExpectedBoolean)))
753 (branch
754 JSONArray
755 values
756 valuesInduction
757 .
758 (constructor
759 JSONBooleanAccessResult
760 JSONBooleanAccessFailed
761 (constructor JSONErrorCode JSONExpectedBoolean)))
762 (branch
763 JSONArrayEnd
764 .
765 (constructor
766 JSONBooleanAccessResult
767 JSONBooleanAccessFailed
768 (constructor JSONErrorCode JSONExpectedBoolean)))
769 (branch
770 JSONArrayNext
771 head
772 tail
773 headInduction
774 tailInduction
775 .
776 (constructor
777 JSONBooleanAccessResult
778 JSONBooleanAccessFailed
779 (constructor JSONErrorCode JSONExpectedBoolean)))
780 (branch
781 JSONString
782 text
783 .
784 (constructor
785 JSONBooleanAccessResult
786 JSONBooleanAccessFailed
787 (constructor JSONErrorCode JSONExpectedBoolean)))
788 (branch
789 JSONNumber
790 number
791 .
792 (constructor
793 JSONBooleanAccessResult
794 JSONBooleanAccessFailed
795 (constructor JSONErrorCode JSONExpectedBoolean)))
796 (branch
797 JSONBoolean
798 boolean
799 .
800 (nat-eliminate
801 (lambda unrestricted valid : Nat . (family JSONBooleanAccessResult))
802 (constructor
803 JSONBooleanAccessResult
804 JSONBooleanAccessFailed
805 (constructor JSONErrorCode JSONMalformedTree))
806 (lambda unrestricted predecessor : Nat .
807 (lambda unrestricted induction : (family JSONBooleanAccessResult) .
808 (constructor JSONBooleanAccessResult JSONBooleanAccessSucceeded boolean)))
809 (nat-less-than boolean jsonNaturalTwo)))
810 (branch
811 JSONNull
812 .
813 (constructor
814 JSONBooleanAccessResult
815 JSONBooleanAccessFailed
816 (constructor JSONErrorCode JSONExpectedBoolean)))))
817
818def jsonNull =
819 (lambda unrestricted value : (family JSON) .
820 (eliminate
821 JSON
822 (lambda unrestricted current : (family JSON) . (family JSONNullAccessResult))
823 value
824 (branch
825 JSONObject
826 members
827 membersInduction
828 .
829 (constructor
830 JSONNullAccessResult
831 JSONNullAccessFailed
832 (constructor JSONErrorCode JSONExpectedNull)))
833 (branch
834 JSONObjectEnd
835 .
836 (constructor
837 JSONNullAccessResult
838 JSONNullAccessFailed
839 (constructor JSONErrorCode JSONExpectedNull)))
840 (branch
841 JSONObjectMember
842 key
843 member
844 tail
845 memberInduction
846 tailInduction
847 .
848 (constructor
849 JSONNullAccessResult
850 JSONNullAccessFailed
851 (constructor JSONErrorCode JSONExpectedNull)))
852 (branch
853 JSONArray
854 values
855 valuesInduction
856 .
857 (constructor
858 JSONNullAccessResult
859 JSONNullAccessFailed
860 (constructor JSONErrorCode JSONExpectedNull)))
861 (branch
862 JSONArrayEnd
863 .
864 (constructor
865 JSONNullAccessResult
866 JSONNullAccessFailed
867 (constructor JSONErrorCode JSONExpectedNull)))
868 (branch
869 JSONArrayNext
870 head
871 tail
872 headInduction
873 tailInduction
874 .
875 (constructor
876 JSONNullAccessResult
877 JSONNullAccessFailed
878 (constructor JSONErrorCode JSONExpectedNull)))
879 (branch
880 JSONString
881 text
882 .
883 (constructor
884 JSONNullAccessResult
885 JSONNullAccessFailed
886 (constructor JSONErrorCode JSONExpectedNull)))
887 (branch
888 JSONNumber
889 number
890 .
891 (constructor
892 JSONNullAccessResult
893 JSONNullAccessFailed
894 (constructor JSONErrorCode JSONExpectedNull)))
895 (branch
896 JSONBoolean
897 boolean
898 .
899 (constructor
900 JSONNullAccessResult
901 JSONNullAccessFailed
902 (constructor JSONErrorCode JSONExpectedNull)))
903 (branch JSONNull . (constructor JSONNullAccessResult JSONNullAccessSucceeded))))
904
905def jsonIntegerFoldWithFuel =
906 (lambda unrestricted fuel : Nat .
907 (nat-eliminate
908 (lambda unrestricted current : Nat .
909 (pi unrestricted input : Bytes .
910 (pi unrestricted magnitude : Nat .
911 (pi unrestricted digits : Nat . (family JSONIntegerFoldResult)))))
912 (lambda unrestricted input : Bytes .
913 (lambda unrestricted magnitude : Nat .
914 (lambda unrestricted digits : Nat .
915 (bytes-eliminate
916 (lambda unrestricted current : Bytes . (family JSONIntegerFoldResult))
917 (constructor JSONIntegerFoldResult JSONIntegerFoldSucceeded magnitude digits)
918 (lambda unrestricted head : Byte .
919 (lambda unrestricted tail : Bytes .
920 (lambda unrestricted induction : (family JSONIntegerFoldResult) .
921 (constructor JSONIntegerFoldResult JSONIntegerFoldFailed))))
922 input))))
923 (lambda unrestricted predecessor : Nat .
924 (lambda unrestricted induction : (pi unrestricted input : Bytes . (pi unrestricted magnitude : Nat . (pi unrestricted digits : Nat . (family JSONIntegerFoldResult)))) .
925 (lambda unrestricted input : Bytes .
926 (lambda unrestricted magnitude : Nat .
927 (lambda unrestricted digits : Nat .
928 (bytes-eliminate
929 (lambda unrestricted current : Bytes . (family JSONIntegerFoldResult))
930 (constructor JSONIntegerFoldResult JSONIntegerFoldSucceeded magnitude digits)
931 (lambda unrestricted head : Byte .
932 (lambda unrestricted tail : Bytes .
933 (lambda unrestricted tailInduction : (family JSONIntegerFoldResult) .
934 (nat-eliminate
935 (lambda unrestricted digit : Nat . (family JSONIntegerFoldResult))
936 (constructor JSONIntegerFoldResult JSONIntegerFoldFailed)
937 (lambda unrestricted digitPredecessor : Nat .
938 (lambda unrestricted digitInduction : (family JSONIntegerFoldResult) .
939 (induction
940 tail
941 (naturalAdd
942 -- ten times the magnitude, folded over the TEN: a fold over
943 -- the magnitude walks its whole value (L21 finding)
944 (naturalMultiply (byte-to-nat (byte 10)) magnitude)
945 (naturalSaturatingSubtract
946 (byte-to-nat head)
947 (byte-to-nat (byte 48))))
948 (succ digits))))
949 (jsonByteIsDigit head)))))
950 input))))))
951 fuel))
952
953-- Does a run of decimal digits denote a magnitude at most 2^63 - 1? Decided
954-- on the DIGITS, never on the natural: fewer than nineteen digits always fit,
955-- more never do, and nineteen fit when they are not lexicographically above
956-- 9223372036854775807. A runtime natural costs ~164 bytes per unit of
957-- magnitude and the checker's division is unary, so neither 2^63 nor a
958-- 63-step halving of a 2^63-scale value is computable on either side; the
959-- string comparison costs nineteen byte comparisons at most.
960def jsonInt64MaximumDigits : Bytes =
961 b"9223372036854775807"
962
963def jsonIntegerDigitsFitInt64 =
964 (lambda unrestricted digits : Bytes .
965 (nat-eliminate
966 (lambda unrestricted current : Nat . Nat)
967 (nat-eliminate
968 (lambda unrestricted current : Nat . Nat)
969 (eliminate
970 DataBytesOrdering
971 (lambda unrestricted current : (family DataBytesOrdering) . Nat)
972 (dataBytesCompare digits jsonInt64MaximumDigits)
973 (branch DataBytesLess . (succ zero))
974 (branch DataBytesEqual . (succ zero))
975 (branch DataBytesGreater . zero))
976 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
977 (naturalSaturatingSubtract (bytes-length digits) (bytes-length jsonInt64MaximumDigits)))
978 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero)))
979 (naturalSaturatingSubtract (bytes-length jsonInt64MaximumDigits) (bytes-length digits))))
980
981def jsonIntegerFold =
982 (lambda unrestricted input : Bytes .
983 (jsonIntegerFoldWithFuel (bytes-length input) input zero zero))
984
985def jsonIntegerFromBytes =
986 (lambda unrestricted input : Bytes .
987 (bytes-eliminate
988 (lambda unrestricted current : Bytes . (family JSONIntegerAccessResult))
989 (constructor
990 JSONIntegerAccessResult
991 JSONIntegerAccessFailed
992 (constructor JSONErrorCode JSONExpectedInteger))
993 (lambda unrestricted head : Byte .
994 (lambda unrestricted tail : Bytes .
995 (lambda unrestricted tailInduction : (family JSONIntegerAccessResult) .
996 (app
997 (lambda unrestricted negative : Nat .
998 (app
999 (lambda unrestricted digits : Bytes .
1000 (eliminate
1001 JSONIntegerFoldResult
1002 (lambda unrestricted current : (family JSONIntegerFoldResult) .
1003 (family JSONIntegerAccessResult))
1004 (jsonIntegerFold digits)
1005 (branch
1006 JSONIntegerFoldSucceeded
1007 magnitude
1008 count
1009 .
1010 (nat-eliminate
1011 (lambda unrestricted supported : Nat . (family JSONIntegerAccessResult))
1012 (constructor
1013 JSONIntegerAccessResult
1014 JSONIntegerAccessFailed
1015 (constructor JSONErrorCode JSONNumericRangeUnsupported))
1016 (lambda unrestricted supportedPredecessor : Nat .
1017 (lambda unrestricted supportedInduction : (family JSONIntegerAccessResult) .
1018 (nat-eliminate
1019 (lambda unrestricted nonempty : Nat .
1020 (family JSONIntegerAccessResult))
1021 (constructor
1022 JSONIntegerAccessResult
1023 JSONIntegerAccessFailed
1024 (constructor JSONErrorCode JSONExpectedInteger))
1025 (lambda unrestricted predecessor : Nat .
1026 (lambda unrestricted induction : (family JSONIntegerAccessResult) .
1027 (constructor
1028 JSONIntegerAccessResult
1029 JSONIntegerAccessSucceeded
1030 (constructor
1031 JSONInteger
1032 JSONIntegerValue
1033 (nat-eliminate
1034 (lambda unrestricted zeroMagnitude : Nat . Nat)
1035 negative
1036 (lambda unrestricted magnitudePredecessor : Nat .
1037 (lambda unrestricted magnitudeInduction : Nat . zero))
1038 (naturalIsZero magnitude))
1039 magnitude))))
1040 count)))
1041 (jsonIntegerDigitsFitInt64 digits)))
1042 (branch
1043 JSONIntegerFoldFailed
1044 .
1045 (constructor
1046 JSONIntegerAccessResult
1047 JSONIntegerAccessFailed
1048 (constructor JSONErrorCode JSONExpectedInteger)))))
1049 (nat-eliminate
1050 (lambda unrestricted signed : Nat . Bytes)
1051 input
1052 (lambda unrestricted predecessor : Nat .
1053 (lambda unrestricted induction : Bytes . tail))
1054 negative)))
1055 (byte-equal head (byte 45))))))
1056 input))
1057
1058def jsonInteger =
1059 (lambda unrestricted value : (family JSON) .
1060 (eliminate
1061 JSON
1062 (lambda unrestricted current : (family JSON) . (family JSONIntegerAccessResult))
1063 value
1064 (branch
1065 JSONObject
1066 members
1067 membersInduction
1068 .
1069 (constructor
1070 JSONIntegerAccessResult
1071 JSONIntegerAccessFailed
1072 (constructor JSONErrorCode JSONExpectedNumber)))
1073 (branch
1074 JSONObjectEnd
1075 .
1076 (constructor
1077 JSONIntegerAccessResult
1078 JSONIntegerAccessFailed
1079 (constructor JSONErrorCode JSONExpectedNumber)))
1080 (branch
1081 JSONObjectMember
1082 key
1083 member
1084 tail
1085 memberInduction
1086 tailInduction
1087 .
1088 (constructor
1089 JSONIntegerAccessResult
1090 JSONIntegerAccessFailed
1091 (constructor JSONErrorCode JSONExpectedNumber)))
1092 (branch
1093 JSONArray
1094 values
1095 valuesInduction
1096 .
1097 (constructor
1098 JSONIntegerAccessResult
1099 JSONIntegerAccessFailed
1100 (constructor JSONErrorCode JSONExpectedNumber)))
1101 (branch
1102 JSONArrayEnd
1103 .
1104 (constructor
1105 JSONIntegerAccessResult
1106 JSONIntegerAccessFailed
1107 (constructor JSONErrorCode JSONExpectedNumber)))
1108 (branch
1109 JSONArrayNext
1110 head
1111 tail
1112 headInduction
1113 tailInduction
1114 .
1115 (constructor
1116 JSONIntegerAccessResult
1117 JSONIntegerAccessFailed
1118 (constructor JSONErrorCode JSONExpectedNumber)))
1119 (branch
1120 JSONString
1121 text
1122 .
1123 (constructor
1124 JSONIntegerAccessResult
1125 JSONIntegerAccessFailed
1126 (constructor JSONErrorCode JSONExpectedNumber)))
1127 (branch JSONNumber number . (jsonIntegerFromBytes number))
1128 (branch
1129 JSONBoolean
1130 boolean
1131 .
1132 (constructor
1133 JSONIntegerAccessResult
1134 JSONIntegerAccessFailed
1135 (constructor JSONErrorCode JSONExpectedNumber)))
1136 (branch
1137 JSONNull
1138 .
1139 (constructor
1140 JSONIntegerAccessResult
1141 JSONIntegerAccessFailed
1142 (constructor JSONErrorCode JSONExpectedNumber)))))
1143
1144-- Tensor-file offsets can exceed both 2^32 and the practical runtime range
1145-- of Nat. Parse their decimal spelling straight into eight bytes. The bound
1146-- is checked on the spelling BEFORE the wrapping word arithmetic: every
1147-- nonnegative decimal prefix is at most the final value, so neither 10*a nor
1148-- 10*a+digit can overflow once the complete digit string fits u64.
1149-- This accepts integer JSON syntax only; 1.0, 1e3, -0 and quoted numbers are
1150-- not offsets. jsonNumber owns JSON syntax/leading-zero validation.
1151def jsonWord64MaximumDigits : Bytes = b"18446744073709551615"
1152
1153def jsonWord64DigitsFit =
1154 (lambda unrestricted digits : Bytes .
1155 (naturalOr (naturalLess (bytes-length digits) 20)
1156 (naturalAnd (naturalEqual (bytes-length digits) 20)
1157 (eliminate DataBytesOrdering
1158 (lambda unrestricted current : (family DataBytesOrdering) . Nat)
1159 (dataBytesCompare digits jsonWord64MaximumDigits)
1160 (branch DataBytesLess . 1)
1161 (branch DataBytesEqual . 1)
1162 (branch DataBytesGreater . 0)))))
1163
1164def jsonWord64DigitStep =
1165 (lambda unrestricted accumulator : (family ModelWord64) .
1166 (lambda unrestricted digit : Byte .
1167 (let unrestricted twice = (modelWord64ShiftLeftOne accumulator) in
1168 (let unrestricted eight = (modelWord64ShiftLeftOne (modelWord64ShiftLeftOne twice)) in
1169 (modelWord64Add (modelWord64Add eight twice)
1170 (modelWord64FromNaturalTruncated
1171 (naturalSaturatingSubtract (byte-to-nat digit) 48)))))))
1172
1173def jsonWord64Digits =
1174 (lambda unrestricted digits : Bytes .
1175 (app
1176 (bytes-eliminate
1177 (lambda unrestricted current : Bytes .
1178 (pi unrestricted accumulator : (family ModelWord64) . (family JSONWord64AccessResult)))
1179 (lambda unrestricted accumulator : (family ModelWord64) .
1180 (constructor JSONWord64AccessResult JSONWord64AccessSucceeded accumulator))
1181 (lambda unrestricted head : Byte .
1182 (lambda unrestricted tail : Bytes .
1183 (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord64) . (family JSONWord64AccessResult)) .
1184 (lambda unrestricted accumulator : (family ModelWord64) .
1185 (nat-eliminate
1186 (lambda unrestricted valid : Nat . (family JSONWord64AccessResult))
1187 (constructor JSONWord64AccessResult JSONWord64AccessFailed
1188 (constructor JSONErrorCode JSONExpectedInteger))
1189 (lambda unrestricted p : Nat .
1190 (lambda unrestricted unused : (family JSONWord64AccessResult) .
1191 (induction (jsonWord64DigitStep accumulator head))))
1192 (jsonByteIsDigit head))))))
1193 digits)
1194 modelWord64Zero))
1195
1196def jsonWord64 =
1197 (lambda unrestricted value : (family JSON) .
1198 (eliminate JSONBytesAccessResult
1199 (lambda unrestricted current : (family JSONBytesAccessResult) . (family JSONWord64AccessResult))
1200 (jsonNumber value)
1201 (branch JSONBytesAccessSucceeded digits .
1202 (nat-eliminate
1203 (lambda unrestricted fits : Nat . (family JSONWord64AccessResult))
1204 (constructor JSONWord64AccessResult JSONWord64AccessFailed
1205 (constructor JSONErrorCode JSONNumericRangeUnsupported))
1206 (lambda unrestricted p : Nat .
1207 (lambda unrestricted unused : (family JSONWord64AccessResult) . (jsonWord64Digits digits)))
1208 (jsonWord64DigitsFit digits)))
1209 (branch JSONBytesAccessFailed code .
1210 (constructor JSONWord64AccessResult JSONWord64AccessFailed code))))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.