module Data.JSONAccess

import Data.Bytes
import Data.JSON
import Data.UTF8
import Model.Parameter
import Model.Word64
import Std.Natural

family JSONMemberLookupResult : Type 0
constructor JSONMemberMissing
constructor JSONMemberFound
field unrestricted jsonMemberFoundValue : (family JSON)
constructor JSONMemberDuplicated
constructor JSONMemberTreeMalformed

end-family

family JSONValueAccessResult : Type 0
constructor JSONValueAccessSucceeded
field unrestricted jsonAccessedValue : (family JSON)
constructor JSONValueAccessFailed
field unrestricted jsonValueAccessError : (family JSONErrorCode)

end-family

family JSONBytesAccessResult : Type 0
constructor JSONBytesAccessSucceeded
field unrestricted jsonAccessedBytes : Bytes
constructor JSONBytesAccessFailed
field unrestricted jsonBytesAccessError : (family JSONErrorCode)

end-family

family JSONArrayAccessResult : Type 0
constructor JSONArrayAccessSucceeded
field unrestricted jsonAccessedArrayValues : (family JSON)
constructor JSONArrayAccessFailed
field unrestricted jsonArrayAccessError : (family JSONErrorCode)

end-family

family JSONObjectAccessResult : Type 0
constructor JSONObjectAccessSucceeded
field unrestricted jsonAccessedObjectMembers : (family JSON)
constructor JSONObjectAccessFailed
field unrestricted jsonObjectAccessError : (family JSONErrorCode)

end-family

family JSONBooleanAccessResult : Type 0
constructor JSONBooleanAccessSucceeded
field unrestricted jsonAccessedBoolean : Nat
constructor JSONBooleanAccessFailed
field unrestricted jsonBooleanAccessError : (family JSONErrorCode)

end-family

family JSONNullAccessResult : Type 0
constructor JSONNullAccessSucceeded
constructor JSONNullAccessFailed
field unrestricted jsonNullAccessError : (family JSONErrorCode)

end-family

family JSONInteger : Type 0
constructor JSONIntegerValue
field unrestricted jsonIntegerNegative : Nat
field unrestricted jsonIntegerMagnitude : Nat

end-family

family JSONIntegerFoldResult : Type 0
constructor JSONIntegerFoldSucceeded
field unrestricted jsonIntegerFoldMagnitude : Nat
field unrestricted jsonIntegerFoldDigits : Nat
constructor JSONIntegerFoldFailed

end-family

family JSONIntegerAccessResult : Type 0
constructor JSONIntegerAccessSucceeded
field unrestricted jsonAccessedInteger : (family JSONInteger)
constructor JSONIntegerAccessFailed
field unrestricted jsonIntegerAccessError : (family JSONErrorCode)

end-family

family JSONWord64AccessResult : Type 0
constructor JSONWord64AccessSucceeded
field unrestricted jsonAccessedWord64 : (family ModelWord64)
constructor JSONWord64AccessFailed
field unrestricted jsonWord64AccessError : (family JSONErrorCode)
end-family

def jsonLookupMembers =
  (lambda unrestricted wanted : Bytes .
    (lambda unrestricted members : (family JSON) .
      (eliminate
        JSON
        (lambda unrestricted current : (family JSON) . (family JSONMemberLookupResult))
        members
        (branch
          JSONObject
          nested
          nestedInduction
          .
          (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch JSONObjectEnd . (constructor JSONMemberLookupResult JSONMemberMissing))
        (branch
          JSONObjectMember
          key
          value
          tail
          valueInduction
          tailInduction
          .
          (nat-eliminate
            (lambda unrestricted matches : Nat . (family JSONMemberLookupResult))
            tailInduction
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family JSONMemberLookupResult) .
                (eliminate
                  JSONMemberLookupResult
                  (lambda unrestricted current : (family JSONMemberLookupResult) .
                    (family JSONMemberLookupResult))
                  tailInduction
                  (branch
                    JSONMemberMissing
                    .
                    (constructor JSONMemberLookupResult JSONMemberFound value))
                  (branch
                    JSONMemberFound
                    duplicateValue
                    .
                    (constructor JSONMemberLookupResult JSONMemberDuplicated))
                  (branch
                    JSONMemberDuplicated
                    .
                    (constructor JSONMemberLookupResult JSONMemberDuplicated))
                  (branch
                    JSONMemberTreeMalformed
                    .
                    (constructor JSONMemberLookupResult JSONMemberTreeMalformed)))))
            (bytes-equal wanted key)))
        (branch
          JSONArray
          values
          valuesInduction
          .
          (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch JSONArrayEnd . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch
          JSONArrayNext
          head
          tail
          headInduction
          tailInduction
          .
          (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch JSONString text . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch JSONNumber number . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch JSONBoolean value . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
        (branch JSONNull . (constructor JSONMemberLookupResult JSONMemberTreeMalformed)))))

def objectLookup =
  (lambda unrestricted wanted : Bytes .
    (lambda unrestricted value : (family JSON) .
      (eliminate
        JSON
        (lambda unrestricted current : (family JSON) . (family JSONValueAccessResult))
        value
        (branch
          JSONObject
          members
          membersInduction
          .
          (eliminate
            JSONMemberLookupResult
            (lambda unrestricted current : (family JSONMemberLookupResult) .
              (family JSONValueAccessResult))
            (jsonLookupMembers wanted members)
            (branch
              JSONMemberMissing
              .
              (constructor
                JSONValueAccessResult
                JSONValueAccessFailed
                (constructor JSONErrorCode JSONMissingMember)))
            (branch
              JSONMemberFound
              member
              .
              (constructor JSONValueAccessResult JSONValueAccessSucceeded member))
            (branch
              JSONMemberDuplicated
              .
              (constructor
                JSONValueAccessResult
                JSONValueAccessFailed
                (constructor JSONErrorCode JSONDuplicateMember)))
            (branch
              JSONMemberTreeMalformed
              .
              (constructor
                JSONValueAccessResult
                JSONValueAccessFailed
                (constructor JSONErrorCode JSONMalformedTree)))))
        (branch
          JSONObjectEnd
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONObjectMember
          key
          member
          tail
          memberInduction
          tailInduction
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONArray
          values
          valuesInduction
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONArrayEnd
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONArrayNext
          head
          tail
          headInduction
          tailInduction
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONString
          text
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONNumber
          number
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONBoolean
          boolean
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject)))
        (branch
          JSONNull
          .
          (constructor
            JSONValueAccessResult
            JSONValueAccessFailed
            (constructor JSONErrorCode JSONExpectedObject))))))

def jsonObject =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONObjectAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (eliminate
          JSONTreeAuditResult
          (lambda unrestricted current : (family JSONTreeAuditResult) .
            (family JSONObjectAccessResult))
          (jsonAuditTreeWithTokenLimits
            (constructor JSONBound JSONBoundBelowTwoPower jsonNaturalTwenty)
            (constructor JSONBound JSONBoundAtMost jsonNaturalOneThousandTwentyFour)
            (constructor JSONBound JSONBoundAtMost jsonNaturalSixtyFiveThousandFiveHundredThirtySix)
            value)
          (branch
            JSONTreeAuditSucceeded
            kind
            counts
            depth
            sequenceCount
            .
            (constructor JSONObjectAccessResult JSONObjectAccessSucceeded members))
          (branch
            JSONTreeAuditFailed
            code
            .
            (constructor JSONObjectAccessResult JSONObjectAccessFailed code))))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONString
        text
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONNumber
        number
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))
      (branch
        JSONNull
        .
        (constructor
          JSONObjectAccessResult
          JSONObjectAccessFailed
          (constructor JSONErrorCode JSONExpectedObject)))))

def jsonString =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONBytesAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONString
        text
        .
        (eliminate
          UTF8DecodeResult
          (lambda unrestricted current : (family UTF8DecodeResult) . (family JSONBytesAccessResult))
          (decodeUTF8 text)
          (branch
            UTF8DecodeSucceeded
            codepoints
            .
            (constructor JSONBytesAccessResult JSONBytesAccessSucceeded text))
          (branch
            UTF8DecodeFailed
            code
            offset
            .
            (constructor
              JSONBytesAccessResult
              JSONBytesAccessFailed
              (constructor JSONErrorCode JSONInvalidUTF8)))))
      (branch
        JSONNumber
        number
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))
      (branch
        JSONNull
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedString)))))

def jsonArray =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONArrayAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor JSONArrayAccessResult JSONArrayAccessSucceeded values))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONString
        text
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONNumber
        number
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))
      (branch
        JSONNull
        .
        (constructor
          JSONArrayAccessResult
          JSONArrayAccessFailed
          (constructor JSONErrorCode JSONExpectedArray)))))

def jsonNumber =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONBytesAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONString
        text
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONNumber
        number
        .
        (nat-eliminate
          (lambda unrestricted bounded : Nat . (family JSONBytesAccessResult))
          (constructor
            JSONBytesAccessResult
            JSONBytesAccessFailed
            (constructor JSONErrorCode JSONNumberLimitExceeded))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family JSONBytesAccessResult) .
              (eliminate
                JSONNumberParseResult
                (lambda unrestricted current : (family JSONNumberParseResult) .
                  (family JSONBytesAccessResult))
                (jsonParseNumber number)
                (branch
                  JSONNumberParsed
                  parsed
                  remaining
                  .
                  (nat-eliminate
                    (lambda unrestricted complete : Nat . (family JSONBytesAccessResult))
                    (constructor
                      JSONBytesAccessResult
                      JSONBytesAccessFailed
                      (constructor JSONErrorCode JSONExpectedNumber))
                    (lambda unrestricted completePredecessor : Nat .
                      (lambda unrestricted completeInduction : (family JSONBytesAccessResult) .
                        (constructor JSONBytesAccessResult JSONBytesAccessSucceeded parsed)))
                    (naturalIsZero (bytes-length remaining))))
                (branch
                  JSONNumberParseFailed
                  code
                  remaining
                  .
                  (constructor JSONBytesAccessResult JSONBytesAccessFailed code)))))
          (jsonNaturalLessThanOrEqual (bytes-length number) jsonNaturalOneThousandTwentyFour)))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONNull
        .
        (constructor
          JSONBytesAccessResult
          JSONBytesAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))))

def jsonBoolean =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONBooleanAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONString
        text
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONNumber
        number
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))
      (branch
        JSONBoolean
        boolean
        .
        (nat-eliminate
          (lambda unrestricted valid : Nat . (family JSONBooleanAccessResult))
          (constructor
            JSONBooleanAccessResult
            JSONBooleanAccessFailed
            (constructor JSONErrorCode JSONMalformedTree))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family JSONBooleanAccessResult) .
              (constructor JSONBooleanAccessResult JSONBooleanAccessSucceeded boolean)))
          (nat-less-than boolean jsonNaturalTwo)))
      (branch
        JSONNull
        .
        (constructor
          JSONBooleanAccessResult
          JSONBooleanAccessFailed
          (constructor JSONErrorCode JSONExpectedBoolean)))))

def jsonNull =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONNullAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONString
        text
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONNumber
        number
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONNullAccessResult
          JSONNullAccessFailed
          (constructor JSONErrorCode JSONExpectedNull)))
      (branch JSONNull . (constructor JSONNullAccessResult JSONNullAccessSucceeded))))

def jsonIntegerFoldWithFuel =
  (lambda unrestricted fuel : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat .
        (pi unrestricted input : Bytes .
          (pi unrestricted magnitude : Nat .
            (pi unrestricted digits : Nat . (family JSONIntegerFoldResult)))))
      (lambda unrestricted input : Bytes .
        (lambda unrestricted magnitude : Nat .
          (lambda unrestricted digits : Nat .
            (bytes-eliminate
              (lambda unrestricted current : Bytes . (family JSONIntegerFoldResult))
              (constructor JSONIntegerFoldResult JSONIntegerFoldSucceeded magnitude digits)
              (lambda unrestricted head : Byte .
                (lambda unrestricted tail : Bytes .
                  (lambda unrestricted induction : (family JSONIntegerFoldResult) .
                    (constructor JSONIntegerFoldResult JSONIntegerFoldFailed))))
              input))))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (pi unrestricted input : Bytes . (pi unrestricted magnitude : Nat . (pi unrestricted digits : Nat . (family JSONIntegerFoldResult)))) .
          (lambda unrestricted input : Bytes .
            (lambda unrestricted magnitude : Nat .
              (lambda unrestricted digits : Nat .
                (bytes-eliminate
                  (lambda unrestricted current : Bytes . (family JSONIntegerFoldResult))
                  (constructor JSONIntegerFoldResult JSONIntegerFoldSucceeded magnitude digits)
                  (lambda unrestricted head : Byte .
                    (lambda unrestricted tail : Bytes .
                      (lambda unrestricted tailInduction : (family JSONIntegerFoldResult) .
                        (nat-eliminate
                          (lambda unrestricted digit : Nat . (family JSONIntegerFoldResult))
                          (constructor JSONIntegerFoldResult JSONIntegerFoldFailed)
                          (lambda unrestricted digitPredecessor : Nat .
                            (lambda unrestricted digitInduction : (family JSONIntegerFoldResult) .
                              (induction
                                tail
                                (naturalAdd
                                  -- ten times the magnitude, folded over the TEN: a fold over
                                  -- the magnitude walks its whole value (L21 finding)
                                  (naturalMultiply (byte-to-nat (byte 10)) magnitude)
                                  (naturalSaturatingSubtract
                                    (byte-to-nat head)
                                    (byte-to-nat (byte 48))))
                                (succ digits))))
                          (jsonByteIsDigit head)))))
                  input))))))
      fuel))

-- Does a run of decimal digits denote a magnitude at most 2^63 - 1? Decided
-- on the DIGITS, never on the natural: fewer than nineteen digits always fit,
-- more never do, and nineteen fit when they are not lexicographically above
-- 9223372036854775807. A runtime natural costs ~164 bytes per unit of
-- magnitude and the checker's division is unary, so neither 2^63 nor a
-- 63-step halving of a 2^63-scale value is computable on either side; the
-- string comparison costs nineteen byte comparisons at most.
def jsonInt64MaximumDigits : Bytes =
  b"9223372036854775807"

def jsonIntegerDigitsFitInt64 =
  (lambda unrestricted digits : Bytes .
    (nat-eliminate
      (lambda unrestricted current : Nat . Nat)
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        (eliminate
          DataBytesOrdering
          (lambda unrestricted current : (family DataBytesOrdering) . Nat)
          (dataBytesCompare digits jsonInt64MaximumDigits)
          (branch DataBytesLess . (succ zero))
          (branch DataBytesEqual . (succ zero))
          (branch DataBytesGreater . zero))
        (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
        (naturalSaturatingSubtract (bytes-length digits) (bytes-length jsonInt64MaximumDigits)))
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero)))
      (naturalSaturatingSubtract (bytes-length jsonInt64MaximumDigits) (bytes-length digits))))

def jsonIntegerFold =
  (lambda unrestricted input : Bytes .
    (jsonIntegerFoldWithFuel (bytes-length input) input zero zero))

def jsonIntegerFromBytes =
  (lambda unrestricted input : Bytes .
    (bytes-eliminate
      (lambda unrestricted current : Bytes . (family JSONIntegerAccessResult))
      (constructor
        JSONIntegerAccessResult
        JSONIntegerAccessFailed
        (constructor JSONErrorCode JSONExpectedInteger))
      (lambda unrestricted head : Byte .
        (lambda unrestricted tail : Bytes .
          (lambda unrestricted tailInduction : (family JSONIntegerAccessResult) .
            (app
              (lambda unrestricted negative : Nat .
                (app
                  (lambda unrestricted digits : Bytes .
                    (eliminate
                      JSONIntegerFoldResult
                      (lambda unrestricted current : (family JSONIntegerFoldResult) .
                        (family JSONIntegerAccessResult))
                      (jsonIntegerFold digits)
                      (branch
                        JSONIntegerFoldSucceeded
                        magnitude
                        count
                        .
                        (nat-eliminate
                          (lambda unrestricted supported : Nat . (family JSONIntegerAccessResult))
                          (constructor
                            JSONIntegerAccessResult
                            JSONIntegerAccessFailed
                            (constructor JSONErrorCode JSONNumericRangeUnsupported))
                          (lambda unrestricted supportedPredecessor : Nat .
                            (lambda unrestricted supportedInduction : (family JSONIntegerAccessResult) .
                              (nat-eliminate
                                (lambda unrestricted nonempty : Nat .
                                  (family JSONIntegerAccessResult))
                                (constructor
                                  JSONIntegerAccessResult
                                  JSONIntegerAccessFailed
                                  (constructor JSONErrorCode JSONExpectedInteger))
                                (lambda unrestricted predecessor : Nat .
                                  (lambda unrestricted induction : (family JSONIntegerAccessResult) .
                                    (constructor
                                      JSONIntegerAccessResult
                                      JSONIntegerAccessSucceeded
                                      (constructor
                                        JSONInteger
                                        JSONIntegerValue
                                        (nat-eliminate
                                        (lambda unrestricted zeroMagnitude : Nat . Nat)
                                        negative
                                        (lambda unrestricted magnitudePredecessor : Nat .
                                        (lambda unrestricted magnitudeInduction : Nat . zero))
                                        (naturalIsZero magnitude))
                                        magnitude))))
                                count)))
                          (jsonIntegerDigitsFitInt64 digits)))
                      (branch
                        JSONIntegerFoldFailed
                        .
                        (constructor
                          JSONIntegerAccessResult
                          JSONIntegerAccessFailed
                          (constructor JSONErrorCode JSONExpectedInteger)))))
                  (nat-eliminate
                    (lambda unrestricted signed : Nat . Bytes)
                    input
                    (lambda unrestricted predecessor : Nat .
                      (lambda unrestricted induction : Bytes . tail))
                    negative)))
              (byte-equal head (byte 45))))))
      input))

def jsonInteger =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONIntegerAccessResult))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONString
        text
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch JSONNumber number . (jsonIntegerFromBytes number))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))
      (branch
        JSONNull
        .
        (constructor
          JSONIntegerAccessResult
          JSONIntegerAccessFailed
          (constructor JSONErrorCode JSONExpectedNumber)))))

-- Tensor-file offsets can exceed both 2^32 and the practical runtime range
-- of Nat. Parse their decimal spelling straight into eight bytes. The bound
-- is checked on the spelling BEFORE the wrapping word arithmetic: every
-- nonnegative decimal prefix is at most the final value, so neither 10*a nor
-- 10*a+digit can overflow once the complete digit string fits u64.
-- This accepts integer JSON syntax only; 1.0, 1e3, -0 and quoted numbers are
-- not offsets. jsonNumber owns JSON syntax/leading-zero validation.
def jsonWord64MaximumDigits : Bytes = b"18446744073709551615"

def jsonWord64DigitsFit =
  (lambda unrestricted digits : Bytes .
    (naturalOr (naturalLess (bytes-length digits) 20)
      (naturalAnd (naturalEqual (bytes-length digits) 20)
        (eliminate DataBytesOrdering
          (lambda unrestricted current : (family DataBytesOrdering) . Nat)
          (dataBytesCompare digits jsonWord64MaximumDigits)
          (branch DataBytesLess . 1)
          (branch DataBytesEqual . 1)
          (branch DataBytesGreater . 0)))))

def jsonWord64DigitStep =
  (lambda unrestricted accumulator : (family ModelWord64) .
    (lambda unrestricted digit : Byte .
      (let unrestricted twice = (modelWord64ShiftLeftOne accumulator) in
        (let unrestricted eight = (modelWord64ShiftLeftOne (modelWord64ShiftLeftOne twice)) in
          (modelWord64Add (modelWord64Add eight twice)
            (modelWord64FromNaturalTruncated
              (naturalSaturatingSubtract (byte-to-nat digit) 48)))))))

def jsonWord64Digits =
  (lambda unrestricted digits : Bytes .
    (app
      (bytes-eliminate
        (lambda unrestricted current : Bytes .
          (pi unrestricted accumulator : (family ModelWord64) . (family JSONWord64AccessResult)))
        (lambda unrestricted accumulator : (family ModelWord64) .
          (constructor JSONWord64AccessResult JSONWord64AccessSucceeded accumulator))
        (lambda unrestricted head : Byte .
          (lambda unrestricted tail : Bytes .
            (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord64) . (family JSONWord64AccessResult)) .
              (lambda unrestricted accumulator : (family ModelWord64) .
                (nat-eliminate
                  (lambda unrestricted valid : Nat . (family JSONWord64AccessResult))
                  (constructor JSONWord64AccessResult JSONWord64AccessFailed
                    (constructor JSONErrorCode JSONExpectedInteger))
                  (lambda unrestricted p : Nat .
                    (lambda unrestricted unused : (family JSONWord64AccessResult) .
                      (induction (jsonWord64DigitStep accumulator head))))
                  (jsonByteIsDigit head))))))
        digits)
      modelWord64Zero))

def jsonWord64 =
  (lambda unrestricted value : (family JSON) .
    (eliminate JSONBytesAccessResult
      (lambda unrestricted current : (family JSONBytesAccessResult) . (family JSONWord64AccessResult))
      (jsonNumber value)
      (branch JSONBytesAccessSucceeded digits .
        (nat-eliminate
          (lambda unrestricted fits : Nat . (family JSONWord64AccessResult))
          (constructor JSONWord64AccessResult JSONWord64AccessFailed
            (constructor JSONErrorCode JSONNumericRangeUnsupported))
          (lambda unrestricted p : Nat .
            (lambda unrestricted unused : (family JSONWord64AccessResult) . (jsonWord64Digits digits)))
          (jsonWord64DigitsFit digits)))
      (branch JSONBytesAccessFailed code .
        (constructor JSONWord64AccessResult JSONWord64AccessFailed code))))