1module Data.JSONRender
2
3import Data.Bytes
4import Data.JSON
5import Data.UTF8
6import Std.Natural
7
8family JSONRenderKind : Type 0
9constructor JSONRenderValueKind
10constructor JSONRenderObjectMembersKind
11constructor JSONRenderArrayValuesKind
12
13end-family
14
15family JSONRenderFragment : Type 0
16constructor JSONRenderFragmentSucceeded
17field unrestricted jsonRenderFragmentKind : (family JSONRenderKind)
18field unrestricted jsonRenderFragmentBuilder : BytesBuilder
19field unrestricted jsonRenderFragmentCount : Nat
20constructor JSONRenderFragmentFailed
21field unrestricted jsonRenderFragmentError : (family JSONErrorCode)
22
23end-family
24
25family JSONRenderResult : Type 0
26constructor JSONRendered
27field unrestricted jsonRenderedBytes : Bytes
28constructor JSONRenderFailed
29field unrestricted jsonRenderError : (family JSONErrorCode)
30
31end-family
32
33family JSONRenderTelemetry : Type 0
34constructor JSONRenderTelemetryValue
35field unrestricted jsonRenderTelemetryCounts : (family JSONCounts)
36field unrestricted jsonRenderTelemetryMaximumDepth : Nat
37field unrestricted jsonRenderTelemetryOutputBytes : Nat
38
39end-family
40
41family JSONObservedRenderResult : Type 0
42constructor JSONObservedRendered
43field unrestricted jsonObservedRenderedBytes : Bytes
44field unrestricted jsonObservedRenderTelemetry : (family JSONRenderTelemetry)
45constructor JSONObservedRenderFailed
46field unrestricted jsonObservedRenderError : (family JSONErrorCode)
47field unrestricted jsonObservedRenderFailureTelemetry : (family JSONRenderTelemetry)
48
49end-family
50
51def jsonRenderFailure =
52 (constructor
53 JSONRenderFragment
54 JSONRenderFragmentFailed
55 (constructor JSONErrorCode JSONMalformedTree))
56
57def jsonRenderKindIsValue =
58 (lambda unrestricted kind : (family JSONRenderKind) .
59 (eliminate
60 JSONRenderKind
61 (lambda unrestricted current : (family JSONRenderKind) . Nat)
62 kind
63 (branch JSONRenderValueKind . (succ zero))
64 (branch JSONRenderObjectMembersKind . zero)
65 (branch JSONRenderArrayValuesKind . zero)))
66
67def jsonRenderKindIsObjectMembers =
68 (lambda unrestricted kind : (family JSONRenderKind) .
69 (eliminate
70 JSONRenderKind
71 (lambda unrestricted current : (family JSONRenderKind) . Nat)
72 kind
73 (branch JSONRenderValueKind . zero)
74 (branch JSONRenderObjectMembersKind . (succ zero))
75 (branch JSONRenderArrayValuesKind . zero)))
76
77def jsonRenderKindIsArrayValues =
78 (lambda unrestricted kind : (family JSONRenderKind) .
79 (eliminate
80 JSONRenderKind
81 (lambda unrestricted current : (family JSONRenderKind) . Nat)
82 kind
83 (branch JSONRenderValueKind . zero)
84 (branch JSONRenderObjectMembersKind . zero)
85 (branch JSONRenderArrayValuesKind . (succ zero))))
86
87def jsonRenderEscapedControl =
88 (lambda unrestricted value : Byte .
89 (bytes-builder-chunk
90 (bytes-cons
91 (byte 92)
92 (bytes-cons
93 (byte 117)
94 (bytes-cons
95 (byte 48)
96 (bytes-cons
97 (byte 48)
98 (bytes-cons
99 (dataBytesHexDigit
100 (naturalDivideUnchecked (byte-to-nat value) (byte-to-nat (byte 16))))
101 (bytes-cons
102 (dataBytesHexDigit
103 (naturalModuloUnchecked (byte-to-nat value) (byte-to-nat (byte 16))))
104 b""))))))))
105
106def jsonRenderEscapedByte =
107 (lambda unrestricted value : Byte .
108 (nat-eliminate
109 (lambda unrestricted quote : Nat . BytesBuilder)
110 (nat-eliminate
111 (lambda unrestricted slash : Nat . BytesBuilder)
112 (nat-eliminate
113 (lambda unrestricted backspace : Nat . BytesBuilder)
114 (nat-eliminate
115 (lambda unrestricted formFeed : Nat . BytesBuilder)
116 (nat-eliminate
117 (lambda unrestricted newline : Nat . BytesBuilder)
118 (nat-eliminate
119 (lambda unrestricted carriage : Nat . BytesBuilder)
120 (nat-eliminate
121 (lambda unrestricted tab : Nat . BytesBuilder)
122 (nat-eliminate
123 (lambda unrestricted control : Nat . BytesBuilder)
124 (bytes-builder-chunk (bytes-cons value b""))
125 (lambda unrestricted predecessor : Nat .
126 (lambda unrestricted induction : BytesBuilder .
127 (jsonRenderEscapedControl value)))
128 (byte-less-than value (byte 32)))
129 (lambda unrestricted predecessor : Nat .
130 (lambda unrestricted induction : BytesBuilder .
131 (bytes-builder-chunk b"\\t")))
132 (byte-equal value (byte 9)))
133 (lambda unrestricted predecessor : Nat .
134 (lambda unrestricted induction : BytesBuilder .
135 (bytes-builder-chunk b"\\r")))
136 (byte-equal value (byte 13)))
137 (lambda unrestricted predecessor : Nat .
138 (lambda unrestricted induction : BytesBuilder .
139 (bytes-builder-chunk b"\\n")))
140 (byte-equal value (byte 10)))
141 (lambda unrestricted predecessor : Nat .
142 (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\f")))
143 (byte-equal value (byte 12)))
144 (lambda unrestricted predecessor : Nat .
145 (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\b")))
146 (byte-equal value (byte 8)))
147 (lambda unrestricted predecessor : Nat .
148 (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\\\")))
149 (byte-equal value (byte 92)))
150 (lambda unrestricted predecessor : Nat .
151 (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\\"")))
152 (byte-equal value (byte 34))))
153
154def jsonRenderEscapedBuilder =
155 (lambda unrestricted input : Bytes .
156 (bytes-eliminate
157 (lambda unrestricted current : Bytes . BytesBuilder)
158 (bytes-builder-empty)
159 (lambda unrestricted head : Byte .
160 (lambda unrestricted tail : Bytes .
161 (lambda unrestricted induction : BytesBuilder .
162 (bytes-builder-append (jsonRenderEscapedByte head) induction))))
163 input))
164
165def jsonRenderStringFragment =
166 (lambda unrestricted input : Bytes .
167 (eliminate
168 UTF8DecodeResult
169 (lambda unrestricted current : (family UTF8DecodeResult) . (family JSONRenderFragment))
170 (decodeUTF8 input)
171 (branch
172 UTF8DecodeSucceeded
173 codepoints
174 .
175 (constructor
176 JSONRenderFragment
177 JSONRenderFragmentSucceeded
178 (constructor JSONRenderKind JSONRenderValueKind)
179 (bytes-builder-append
180 (bytes-builder-chunk b"\"")
181 (bytes-builder-append (jsonRenderEscapedBuilder input) (bytes-builder-chunk b"\"")))
182 (succ zero)))
183 (branch
184 UTF8DecodeFailed
185 code
186 offset
187 .
188 (constructor
189 JSONRenderFragment
190 JSONRenderFragmentFailed
191 (constructor JSONErrorCode JSONInvalidUTF8)))))
192
193def jsonRenderCommaBefore =
194 (lambda unrestricted count : Nat .
195 (nat-eliminate
196 (lambda unrestricted current : Nat . BytesBuilder)
197 (bytes-builder-empty)
198 (lambda unrestricted predecessor : Nat .
199 (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b",")))
200 count))
201
202-- Part of `jsonRenderTree`, lifted out to keep it inside the §28.3 size and
203-- nesting limits; the parameters are the locals it still needs.
204def jsonRenderTreePart1 =
205 (lambda unrestricted key : Bytes .
206 (lambda unrestricted memberInduction : (family JSONRenderFragment) .
207 (lambda unrestricted tailInduction : (family JSONRenderFragment) .
208 (eliminate
209 JSONRenderFragment
210 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
211 (jsonRenderStringFragment key)
212 (branch
213 JSONRenderFragmentSucceeded
214 keyKind
215 keyBuilder
216 keyCount
217 .
218 (eliminate
219 JSONRenderFragment
220 (lambda unrestricted current : (family JSONRenderFragment) .
221 (family JSONRenderFragment))
222 memberInduction
223 (branch
224 JSONRenderFragmentSucceeded
225 memberKind
226 memberBuilder
227 memberCount
228 .
229 (eliminate
230 JSONRenderFragment
231 (lambda unrestricted current : (family JSONRenderFragment) .
232 (family JSONRenderFragment))
233 tailInduction
234 (branch
235 JSONRenderFragmentSucceeded
236 tailKind
237 tailBuilder
238 tailCount
239 .
240 (nat-eliminate
241 (lambda unrestricted validKey : Nat . (family JSONRenderFragment))
242 jsonRenderFailure
243 (lambda unrestricted keyPredecessor : Nat .
244 (lambda unrestricted keyInduction : (family JSONRenderFragment) .
245 (nat-eliminate
246 (lambda unrestricted validMember : Nat . (family JSONRenderFragment))
247 jsonRenderFailure
248 (lambda unrestricted memberPredecessor : Nat .
249 (lambda unrestricted memberRoleInduction : (family JSONRenderFragment) .
250 (nat-eliminate
251 (lambda unrestricted validTail : Nat .
252 (family JSONRenderFragment))
253 jsonRenderFailure
254 (lambda unrestricted tailPredecessor : Nat .
255 (lambda unrestricted tailRoleInduction : (family JSONRenderFragment) .
256 (constructor
257 JSONRenderFragment
258 JSONRenderFragmentSucceeded
259 (constructor JSONRenderKind JSONRenderObjectMembersKind)
260 (bytes-builder-append
261 keyBuilder
262 (bytes-builder-append
263 (bytes-builder-chunk b":")
264 (bytes-builder-append
265 memberBuilder
266 (bytes-builder-append
267 (jsonRenderCommaBefore tailCount)
268 tailBuilder))))
269 (succ tailCount))))
270 (jsonRenderKindIsObjectMembers tailKind))))
271 (jsonRenderKindIsValue memberKind))))
272 (jsonRenderKindIsValue keyKind)))
273 (branch
274 JSONRenderFragmentFailed
275 code
276 .
277 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
278 (branch
279 JSONRenderFragmentFailed
280 code
281 .
282 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
283 (branch
284 JSONRenderFragmentFailed
285 code
286 .
287 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))))
288
289-- Part of `jsonRenderTree`, lifted out to keep it inside the §28.3 size and
290-- nesting limits; the parameters are the locals it still needs.
291def jsonRenderTreePart2 =
292 (lambda unrestricted tailInduction : (family JSONRenderFragment) .
293 (lambda unrestricted headKind : (family JSONRenderKind) .
294 (lambda unrestricted headBuilder : BytesBuilder .
295 (eliminate
296 JSONRenderFragment
297 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
298 tailInduction
299 (branch
300 JSONRenderFragmentSucceeded
301 tailKind
302 tailBuilder
303 tailCount
304 .
305 (nat-eliminate
306 (lambda unrestricted validHead : Nat . (family JSONRenderFragment))
307 jsonRenderFailure
308 (lambda unrestricted headPredecessor : Nat .
309 (lambda unrestricted headRoleInduction : (family JSONRenderFragment) .
310 (nat-eliminate
311 (lambda unrestricted validTail : Nat . (family JSONRenderFragment))
312 jsonRenderFailure
313 (lambda unrestricted tailPredecessor : Nat .
314 (lambda unrestricted tailRoleInduction : (family JSONRenderFragment) .
315 (constructor
316 JSONRenderFragment
317 JSONRenderFragmentSucceeded
318 (constructor JSONRenderKind JSONRenderArrayValuesKind)
319 (bytes-builder-append
320 headBuilder
321 (bytes-builder-append (jsonRenderCommaBefore tailCount) tailBuilder))
322 (succ tailCount))))
323 (jsonRenderKindIsArrayValues tailKind))))
324 (jsonRenderKindIsValue headKind)))
325 (branch
326 JSONRenderFragmentFailed
327 code
328 .
329 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))))
330
331def jsonRenderTree =
332 (lambda unrestricted value : (family JSON) .
333 (eliminate
334 JSON
335 (lambda unrestricted current : (family JSON) . (family JSONRenderFragment))
336 value
337 (branch
338 JSONObject
339 members
340 membersInduction
341 .
342 (eliminate
343 JSONRenderFragment
344 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
345 membersInduction
346 (branch
347 JSONRenderFragmentSucceeded
348 kind
349 builder
350 count
351 .
352 (nat-eliminate
353 (lambda unrestricted valid : Nat . (family JSONRenderFragment))
354 jsonRenderFailure
355 (lambda unrestricted predecessor : Nat .
356 (lambda unrestricted induction : (family JSONRenderFragment) .
357 (constructor
358 JSONRenderFragment
359 JSONRenderFragmentSucceeded
360 (constructor JSONRenderKind JSONRenderValueKind)
361 (bytes-builder-append
362 (bytes-builder-chunk b"{")
363 (bytes-builder-append builder (bytes-builder-chunk b"}")))
364 (succ zero))))
365 (jsonRenderKindIsObjectMembers kind)))
366 (branch
367 JSONRenderFragmentFailed
368 code
369 .
370 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
371 (branch
372 JSONObjectEnd
373 .
374 (constructor
375 JSONRenderFragment
376 JSONRenderFragmentSucceeded
377 (constructor JSONRenderKind JSONRenderObjectMembersKind)
378 (bytes-builder-empty)
379 zero))
380 (branch
381 JSONObjectMember
382 key
383 member
384 tail
385 memberInduction
386 tailInduction
387 .
388 (jsonRenderTreePart1 key memberInduction tailInduction))
389 (branch
390 JSONArray
391 values
392 valuesInduction
393 .
394 (eliminate
395 JSONRenderFragment
396 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
397 valuesInduction
398 (branch
399 JSONRenderFragmentSucceeded
400 kind
401 builder
402 count
403 .
404 (nat-eliminate
405 (lambda unrestricted valid : Nat . (family JSONRenderFragment))
406 jsonRenderFailure
407 (lambda unrestricted predecessor : Nat .
408 (lambda unrestricted induction : (family JSONRenderFragment) .
409 (constructor
410 JSONRenderFragment
411 JSONRenderFragmentSucceeded
412 (constructor JSONRenderKind JSONRenderValueKind)
413 (bytes-builder-append
414 (bytes-builder-chunk b"[")
415 (bytes-builder-append builder (bytes-builder-chunk b"]")))
416 (succ zero))))
417 (jsonRenderKindIsArrayValues kind)))
418 (branch
419 JSONRenderFragmentFailed
420 code
421 .
422 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
423 (branch
424 JSONArrayEnd
425 .
426 (constructor
427 JSONRenderFragment
428 JSONRenderFragmentSucceeded
429 (constructor JSONRenderKind JSONRenderArrayValuesKind)
430 (bytes-builder-empty)
431 zero))
432 (branch
433 JSONArrayNext
434 head
435 tail
436 headInduction
437 tailInduction
438 .
439 (eliminate
440 JSONRenderFragment
441 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
442 headInduction
443 (branch
444 JSONRenderFragmentSucceeded
445 headKind
446 headBuilder
447 headCount
448 .
449 (jsonRenderTreePart2 tailInduction headKind headBuilder))
450 (branch
451 JSONRenderFragmentFailed
452 code
453 .
454 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
455 (branch JSONString text . (jsonRenderStringFragment text))
456 (branch
457 JSONNumber
458 number
459 .
460 (eliminate
461 JSONNumberParseResult
462 (lambda unrestricted current : (family JSONNumberParseResult) .
463 (family JSONRenderFragment))
464 (jsonParseNumber number)
465 (branch
466 JSONNumberParsed
467 parsed
468 remaining
469 .
470 (nat-eliminate
471 (lambda unrestricted noTrailing : Nat . (family JSONRenderFragment))
472 jsonRenderFailure
473 (lambda unrestricted predecessor : Nat .
474 (lambda unrestricted induction : (family JSONRenderFragment) .
475 (constructor
476 JSONRenderFragment
477 JSONRenderFragmentSucceeded
478 (constructor JSONRenderKind JSONRenderValueKind)
479 (bytes-builder-chunk parsed)
480 (succ zero))))
481 (naturalIsZero (bytes-length remaining))))
482 (branch JSONNumberParseFailed code remaining . jsonRenderFailure)))
483 (branch
484 JSONBoolean
485 boolean
486 .
487 (constructor
488 JSONRenderFragment
489 JSONRenderFragmentSucceeded
490 (constructor JSONRenderKind JSONRenderValueKind)
491 (nat-eliminate
492 (lambda unrestricted current : Nat . BytesBuilder)
493 (bytes-builder-chunk b"false")
494 (lambda unrestricted predecessor : Nat .
495 (lambda unrestricted induction : BytesBuilder .
496 (bytes-builder-chunk b"true")))
497 boolean)
498 (succ zero)))
499 (branch
500 JSONNull
501 .
502 (constructor
503 JSONRenderFragment
504 JSONRenderFragmentSucceeded
505 (constructor JSONRenderKind JSONRenderValueKind)
506 (bytes-builder-chunk b"null")
507 (succ zero)))))
508
509def jsonRenderUnchecked =
510 (lambda unrestricted value : (family JSON) .
511 (eliminate
512 JSONRenderFragment
513 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderResult))
514 (jsonRenderTree value)
515 (branch
516 JSONRenderFragmentSucceeded
517 kind
518 builder
519 count
520 .
521 (nat-eliminate
522 (lambda unrestricted valid : Nat . (family JSONRenderResult))
523 (constructor
524 JSONRenderResult
525 JSONRenderFailed
526 (constructor JSONErrorCode JSONMalformedTree))
527 (lambda unrestricted predecessor : Nat .
528 (lambda unrestricted induction : (family JSONRenderResult) .
529 (constructor JSONRenderResult JSONRendered (bytes-builder-build builder))))
530 (jsonRenderKindIsValue kind)))
531 (branch JSONRenderFragmentFailed code . (constructor JSONRenderResult JSONRenderFailed code))))
532
533def jsonEmptyRenderTelemetry =
534 (constructor JSONRenderTelemetry JSONRenderTelemetryValue jsonCountsZero zero zero)
535
536def renderJSONObservedWithLimits =
537 (lambda unrestricted limits : (family JSONLimits) .
538 (lambda unrestricted value : (family JSON) .
539 (eliminate
540 JSONLimits
541 (lambda unrestricted current : (family JSONLimits) . (family JSONObservedRenderResult))
542 limits
543 (branch
544 JSONLimitsValue
545 maximumInputBytes
546 maximumDepth
547 maximumStringBytes
548 maximumNumberBytes
549 maximumContainerEntries
550 maximumOutputBytes
551 .
552 (eliminate
553 JSONTreeAuditResult
554 (lambda unrestricted current : (family JSONTreeAuditResult) .
555 (family JSONObservedRenderResult))
556 (jsonAuditTreeWithTokenLimits
557 maximumStringBytes
558 maximumNumberBytes
559 maximumContainerEntries
560 value)
561 (branch
562 JSONTreeAuditSucceeded
563 kind
564 counts
565 depth
566 sequenceCount
567 .
568 (nat-eliminate
569 (lambda unrestricted valueKind : Nat . (family JSONObservedRenderResult))
570 (constructor
571 JSONObservedRenderResult
572 JSONObservedRenderFailed
573 (constructor JSONErrorCode JSONMalformedTree)
574 (constructor JSONRenderTelemetry JSONRenderTelemetryValue counts depth zero))
575 (lambda unrestricted kindPredecessor : Nat .
576 (lambda unrestricted kindInduction : (family JSONObservedRenderResult) .
577 (nat-eliminate
578 (lambda unrestricted depthBounded : Nat . (family JSONObservedRenderResult))
579 (constructor
580 JSONObservedRenderResult
581 JSONObservedRenderFailed
582 (constructor JSONErrorCode JSONDepthLimitExceeded)
583 (constructor JSONRenderTelemetry JSONRenderTelemetryValue counts depth zero))
584 (lambda unrestricted depthPredecessor : Nat .
585 (lambda unrestricted depthInduction : (family JSONObservedRenderResult) .
586 (eliminate
587 JSONRenderResult
588 (lambda unrestricted current : (family JSONRenderResult) .
589 (family JSONObservedRenderResult))
590 (jsonRenderUnchecked value)
591 (branch
592 JSONRendered
593 output
594 .
595 (nat-eliminate
596 (lambda unrestricted outputBounded : Nat .
597 (family JSONObservedRenderResult))
598 (constructor
599 JSONObservedRenderResult
600 JSONObservedRenderFailed
601 (constructor JSONErrorCode JSONOutputLimitExceeded)
602 (constructor
603 JSONRenderTelemetry
604 JSONRenderTelemetryValue
605 counts
606 depth
607 (bytes-length output)))
608 (lambda unrestricted outputPredecessor : Nat .
609 (lambda unrestricted outputInduction : (family JSONObservedRenderResult) .
610 (constructor
611 JSONObservedRenderResult
612 JSONObservedRendered
613 output
614 (constructor
615 JSONRenderTelemetry
616 JSONRenderTelemetryValue
617 counts
618 depth
619 (bytes-length output)))))
620 (jsonBoundAllows maximumOutputBytes (bytes-length output))))
621 (branch
622 JSONRenderFailed
623 code
624 .
625 (constructor
626 JSONObservedRenderResult
627 JSONObservedRenderFailed
628 code
629 (constructor
630 JSONRenderTelemetry
631 JSONRenderTelemetryValue
632 counts
633 depth
634 zero))))))
635 (jsonBoundAllows maximumDepth depth))))
636 (jsonTreeKindIsValue kind)))
637 (branch
638 JSONTreeAuditFailed
639 code
640 .
641 (constructor
642 JSONObservedRenderResult
643 JSONObservedRenderFailed
644 code
645 jsonEmptyRenderTelemetry)))))))
646
647def renderJSONWithLimits =
648 (lambda unrestricted limits : (family JSONLimits) .
649 (lambda unrestricted value : (family JSON) .
650 (eliminate
651 JSONObservedRenderResult
652 (lambda unrestricted current : (family JSONObservedRenderResult) .
653 (family JSONRenderResult))
654 (renderJSONObservedWithLimits limits value)
655 (branch
656 JSONObservedRendered
657 output
658 telemetry
659 .
660 (constructor JSONRenderResult JSONRendered output))
661 (branch
662 JSONObservedRenderFailed
663 code
664 telemetry
665 .
666 (constructor JSONRenderResult JSONRenderFailed code)))))
667
668def renderJSON =
669 (lambda unrestricted value : (family JSON) . (renderJSONWithLimits jsonDefaultLimits value))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.