2467def parseJSONObservedWithLimits =
2468 (lambda unrestricted limits : (family JSONLimits) .
2469 (lambda unrestricted input : Bytes .
2470 (eliminate
2471 JSONLimits
2472 (lambda unrestricted current : (family JSONLimits) . (family JSONObservedDocumentResult))
2473 limits
2474 (branch
2475 JSONLimitsValue
2476 maximumInputBytes
2477 maximumDepth
2478 maximumStringBytes
2479 maximumNumberBytes
2480 maximumContainerEntries
2481 maximumOutputBytes
2482 .
2483 (nat-eliminate
2484 (lambda unrestricted inputBounded : Nat . (family JSONObservedDocumentResult))
2485 (constructor
2486 JSONObservedDocumentResult
2487 JSONObservedDocumentFailed
2488 (constructor JSONErrorCode JSONInputLimitExceeded)
2489 zero
2490 (jsonEmptyParseTelemetry (bytes-length input) zero))
2491 (lambda unrestricted inputPredecessor : Nat .
2492 (lambda unrestricted inputInduction : (family JSONObservedDocumentResult) .
2493 (eliminate
2494 JSONDocumentResult
2495 (lambda unrestricted current : (family JSONDocumentResult) .
2496 (family JSONObservedDocumentResult))
2497 (jsonParseDocumentUnchecked input)
2498 (branch
2499 JSONDocumentParsed
2500 parsed
2501 .
2502 (eliminate
2503 JSONTreeAuditResult
2504 (lambda unrestricted current : (family JSONTreeAuditResult) .
2505 (family JSONObservedDocumentResult))
2506 (jsonAuditTreeWithTokenLimits
2507 maximumStringBytes
2508 maximumNumberBytes
2509 maximumContainerEntries
2510 parsed)
2511 (branch
2512 JSONTreeAuditSucceeded
2513 kind
2514 counts
2515 depth
2516 sequenceCount
2517 .
2518 (nat-eliminate
2519 (lambda unrestricted valueKind : Nat .
2520 (family JSONObservedDocumentResult))
2521 (constructor
2522 JSONObservedDocumentResult
2523 JSONObservedDocumentFailed
2524 (constructor JSONErrorCode JSONMalformedTree)
2525 (bytes-length input)
2526 (constructor
2527 JSONParseTelemetry
2528 JSONParseTelemetryValue
2529 (bytes-length input)
2530 (bytes-length input)
2531 zero
2532 (bytes-length input)
2533 depth
2534 counts))
2535 (lambda unrestricted kindPredecessor : Nat .
2536 (lambda unrestricted kindInduction : (family JSONObservedDocumentResult) .
2537 (nat-eliminate
2538 (lambda unrestricted depthBounded : Nat .
2539 (family JSONObservedDocumentResult))
2540 (constructor
2541 JSONObservedDocumentResult
2542 JSONObservedDocumentFailed
2543 (constructor JSONErrorCode JSONDepthLimitExceeded)
2544 (bytes-length input)
2545 (constructor
2546 JSONParseTelemetry
2547 JSONParseTelemetryValue
2548 (bytes-length input)
2549 (bytes-length input)
2550 zero
2551 (bytes-length input)
2552 depth
2553 counts))
2554 (lambda unrestricted depthPredecessor : Nat .
2555 (lambda unrestricted depthInduction : (family JSONObservedDocumentResult) .
2556 (constructor
2557 JSONObservedDocumentResult
2558 JSONObservedDocumentParsed
2559 parsed
2560 (constructor
2561 JSONParseTelemetry
2562 JSONParseTelemetryValue
2563 (bytes-length input)
2564 (bytes-length input)
2565 zero
2566 (bytes-length input)
2567 depth
2568 counts))))
2569 (jsonBoundAllows maximumDepth depth))))
2570 (jsonTreeKindIsValue kind)))
2571 (branch
2572 JSONTreeAuditFailed
2573 code
2574 .
2575 (constructor
2576 JSONObservedDocumentResult
2577 JSONObservedDocumentFailed
2578 code
2579 (bytes-length input)
2580 (jsonEmptyParseTelemetry (bytes-length input) (bytes-length input))))))
2581 (branch
2582 JSONDocumentFailed
2583 code
2584 offset
2585 .
2586 (constructor
2587 JSONObservedDocumentResult
2588 JSONObservedDocumentFailed
2589 code
2590 offset
2591 (jsonEmptyParseTelemetry (bytes-length input) offset))))))
2592 (jsonBoundAllows maximumInputBytes (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.