Part of `jsonParseValueStep`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
1561def jsonParseValueStepPart1 =
1562 (lambda unrestricted parser : (family JSONParser) .
1563 (lambda unrestricted clean : Bytes .
1564 (lambda unrestricted head : Byte .
1565 (lambda unrestricted tail : Bytes .
1566 (nat-eliminate
1567 (lambda unrestricted array : Nat . (family JSONParseResult))
1568 (nat-eliminate
1569 (lambda unrestricted trueValue : Nat . (family JSONParseResult))
1570 (nat-eliminate
1571 (lambda unrestricted falseValue : Nat . (family JSONParseResult))
1572 (nat-eliminate
1573 (lambda unrestricted nullValue : Nat . (family JSONParseResult))
1574 (nat-eliminate
1575 (lambda unrestricted number : Nat . (family JSONParseResult))
1576 (jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) clean)
1577 (lambda unrestricted numberPredecessor : Nat .
1578 (lambda unrestricted numberInduction : (family JSONParseResult) .
1579 (eliminate
1580 JSONNumberParseResult
1581 (lambda unrestricted current : (family JSONNumberParseResult) .
1582 (family JSONParseResult))
1583 (jsonParseNumber clean)
1584 (branch
1585 JSONNumberParsed
1586 numberBytes
1587 remaining
1588 .
1589 (constructor
1590 JSONParseResult
1591 JSONParsed
1592 (constructor JSON JSONNumber numberBytes)
1593 remaining))
1594 (branch
1595 JSONNumberParseFailed
1596 code
1597 remaining
1598 .
1599 (jsonParseFailure code remaining)))))
1600 (jsonFlagOr (byte-equal head (byte 45)) (jsonByteIsDigit head)))
1601 (lambda unrestricted nullPredecessor : Nat .
1602 (lambda unrestricted nullInduction : (family JSONParseResult) .
1603 (eliminate
1604 JSONLiteralResult
1605 (lambda unrestricted current : (family JSONLiteralResult) .
1606 (family JSONParseResult))
1607 (jsonConsumeLiteral b"null" clean)
1608 (branch
1609 JSONLiteralConsumed
1610 remaining
1611 .
1612 (constructor
1613 JSONParseResult
1614 JSONParsed
1615 (constructor JSON JSONNull)
1616 remaining))
1617 (branch
1618 JSONLiteralFailed
1619 remaining
1620 .
1621 (jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) remaining)))))
1622 (byte-equal head (byte 110)))
1623 (lambda unrestricted falsePredecessor : Nat .
1624 (lambda unrestricted falseInduction : (family JSONParseResult) .
1625 (eliminate
1626 JSONLiteralResult
1627 (lambda unrestricted current : (family JSONLiteralResult) .
1628 (family JSONParseResult))
1629 (jsonConsumeLiteral b"false" clean)
1630 (branch
1631 JSONLiteralConsumed
1632 remaining
1633 .
1634 (constructor
1635 JSONParseResult
1636 JSONParsed
1637 (constructor JSON JSONBoolean zero)
1638 remaining))
1639 (branch
1640 JSONLiteralFailed
1641 remaining
1642 .
1643 (jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) remaining)))))
1644 (byte-equal head (byte 102)))
1645 (lambda unrestricted truePredecessor : Nat .
1646 (lambda unrestricted trueInduction : (family JSONParseResult) .
1647 (eliminate
1648 JSONLiteralResult
1649 (lambda unrestricted current : (family JSONLiteralResult) .
1650 (family JSONParseResult))
1651 (jsonConsumeLiteral b"true" clean)
1652 (branch
1653 JSONLiteralConsumed
1654 remaining
1655 .
1656 (constructor
1657 JSONParseResult
1658 JSONParsed
1659 (constructor JSON JSONBoolean (succ zero))
1660 remaining))
1661 (branch
1662 JSONLiteralFailed
1663 remaining
1664 .
1665 (jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) remaining)))))
1666 (byte-equal head (byte 116)))
1667 (lambda unrestricted arrayPredecessor : Nat .
1668 (lambda unrestricted arrayInduction : (family JSONParseResult) .
1669 (eliminate
1670 JSONParseResult
1671 (lambda unrestricted current : (family JSONParseResult) .
1672 (family JSONParseResult))
1673 (jsonParserArray parser tail)
1674 (branch
1675 JSONParsed
1676 values
1677 remaining
1678 .
1679 (constructor
1680 JSONParseResult
1681 JSONParsed
1682 (constructor JSON JSONArray values)
1683 remaining))
1684 (branch JSONParseFailed code remaining . (jsonParseFailure code remaining)))))
1685 (byte-equal head (byte 91)))))))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.