module Data.JSONRender

import Data.Bytes
import Data.JSON
import Data.UTF8
import Std.Natural

family JSONRenderKind : Type 0
constructor JSONRenderValueKind
constructor JSONRenderObjectMembersKind
constructor JSONRenderArrayValuesKind

end-family

family JSONRenderFragment : Type 0
constructor JSONRenderFragmentSucceeded
field unrestricted jsonRenderFragmentKind : (family JSONRenderKind)
field unrestricted jsonRenderFragmentBuilder : BytesBuilder
field unrestricted jsonRenderFragmentCount : Nat
constructor JSONRenderFragmentFailed
field unrestricted jsonRenderFragmentError : (family JSONErrorCode)

end-family

family JSONRenderResult : Type 0
constructor JSONRendered
field unrestricted jsonRenderedBytes : Bytes
constructor JSONRenderFailed
field unrestricted jsonRenderError : (family JSONErrorCode)

end-family

family JSONRenderTelemetry : Type 0
constructor JSONRenderTelemetryValue
field unrestricted jsonRenderTelemetryCounts : (family JSONCounts)
field unrestricted jsonRenderTelemetryMaximumDepth : Nat
field unrestricted jsonRenderTelemetryOutputBytes : Nat

end-family

family JSONObservedRenderResult : Type 0
constructor JSONObservedRendered
field unrestricted jsonObservedRenderedBytes : Bytes
field unrestricted jsonObservedRenderTelemetry : (family JSONRenderTelemetry)
constructor JSONObservedRenderFailed
field unrestricted jsonObservedRenderError : (family JSONErrorCode)
field unrestricted jsonObservedRenderFailureTelemetry : (family JSONRenderTelemetry)

end-family

def jsonRenderFailure =
  (constructor
    JSONRenderFragment
    JSONRenderFragmentFailed
    (constructor JSONErrorCode JSONMalformedTree))

def jsonRenderKindIsValue =
  (lambda unrestricted kind : (family JSONRenderKind) .
    (eliminate
      JSONRenderKind
      (lambda unrestricted current : (family JSONRenderKind) . Nat)
      kind
      (branch JSONRenderValueKind . (succ zero))
      (branch JSONRenderObjectMembersKind . zero)
      (branch JSONRenderArrayValuesKind . zero)))

def jsonRenderKindIsObjectMembers =
  (lambda unrestricted kind : (family JSONRenderKind) .
    (eliminate
      JSONRenderKind
      (lambda unrestricted current : (family JSONRenderKind) . Nat)
      kind
      (branch JSONRenderValueKind . zero)
      (branch JSONRenderObjectMembersKind . (succ zero))
      (branch JSONRenderArrayValuesKind . zero)))

def jsonRenderKindIsArrayValues =
  (lambda unrestricted kind : (family JSONRenderKind) .
    (eliminate
      JSONRenderKind
      (lambda unrestricted current : (family JSONRenderKind) . Nat)
      kind
      (branch JSONRenderValueKind . zero)
      (branch JSONRenderObjectMembersKind . zero)
      (branch JSONRenderArrayValuesKind . (succ zero))))

def jsonRenderEscapedControl =
  (lambda unrestricted value : Byte .
    (bytes-builder-chunk
      (bytes-cons
        (byte 92)
        (bytes-cons
          (byte 117)
          (bytes-cons
            (byte 48)
            (bytes-cons
              (byte 48)
              (bytes-cons
                (dataBytesHexDigit
                  (naturalDivideUnchecked (byte-to-nat value) (byte-to-nat (byte 16))))
                (bytes-cons
                  (dataBytesHexDigit
                    (naturalModuloUnchecked (byte-to-nat value) (byte-to-nat (byte 16))))
                  b""))))))))

def jsonRenderEscapedByte =
  (lambda unrestricted value : Byte .
    (nat-eliminate
      (lambda unrestricted quote : Nat . BytesBuilder)
      (nat-eliminate
        (lambda unrestricted slash : Nat . BytesBuilder)
        (nat-eliminate
          (lambda unrestricted backspace : Nat . BytesBuilder)
          (nat-eliminate
            (lambda unrestricted formFeed : Nat . BytesBuilder)
            (nat-eliminate
              (lambda unrestricted newline : Nat . BytesBuilder)
              (nat-eliminate
                (lambda unrestricted carriage : Nat . BytesBuilder)
                (nat-eliminate
                  (lambda unrestricted tab : Nat . BytesBuilder)
                  (nat-eliminate
                    (lambda unrestricted control : Nat . BytesBuilder)
                    (bytes-builder-chunk (bytes-cons value b""))
                    (lambda unrestricted predecessor : Nat .
                      (lambda unrestricted induction : BytesBuilder .
                        (jsonRenderEscapedControl value)))
                    (byte-less-than value (byte 32)))
                  (lambda unrestricted predecessor : Nat .
                    (lambda unrestricted induction : BytesBuilder .
                      (bytes-builder-chunk b"\\t")))
                  (byte-equal value (byte 9)))
                (lambda unrestricted predecessor : Nat .
                  (lambda unrestricted induction : BytesBuilder .
                    (bytes-builder-chunk b"\\r")))
                (byte-equal value (byte 13)))
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : BytesBuilder .
                  (bytes-builder-chunk b"\\n")))
              (byte-equal value (byte 10)))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\f")))
            (byte-equal value (byte 12)))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\b")))
          (byte-equal value (byte 8)))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\\\")))
        (byte-equal value (byte 92)))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\\"")))
      (byte-equal value (byte 34))))

def jsonRenderEscapedBuilder =
  (lambda unrestricted input : Bytes .
    (bytes-eliminate
      (lambda unrestricted current : Bytes . BytesBuilder)
      (bytes-builder-empty)
      (lambda unrestricted head : Byte .
        (lambda unrestricted tail : Bytes .
          (lambda unrestricted induction : BytesBuilder .
            (bytes-builder-append (jsonRenderEscapedByte head) induction))))
      input))

def jsonRenderStringFragment =
  (lambda unrestricted input : Bytes .
    (eliminate
      UTF8DecodeResult
      (lambda unrestricted current : (family UTF8DecodeResult) . (family JSONRenderFragment))
      (decodeUTF8 input)
      (branch
        UTF8DecodeSucceeded
        codepoints
        .
        (constructor
          JSONRenderFragment
          JSONRenderFragmentSucceeded
          (constructor JSONRenderKind JSONRenderValueKind)
          (bytes-builder-append
            (bytes-builder-chunk b"\"")
            (bytes-builder-append (jsonRenderEscapedBuilder input) (bytes-builder-chunk b"\"")))
          (succ zero)))
      (branch
        UTF8DecodeFailed
        code
        offset
        .
        (constructor
          JSONRenderFragment
          JSONRenderFragmentFailed
          (constructor JSONErrorCode JSONInvalidUTF8)))))

def jsonRenderCommaBefore =
  (lambda unrestricted count : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat . BytesBuilder)
      (bytes-builder-empty)
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b",")))
      count))

-- Part of `jsonRenderTree`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonRenderTreePart1 =
  (lambda unrestricted key : Bytes .
    (lambda unrestricted memberInduction : (family JSONRenderFragment) .
      (lambda unrestricted tailInduction : (family JSONRenderFragment) .
        (eliminate
          JSONRenderFragment
          (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
          (jsonRenderStringFragment key)
          (branch
            JSONRenderFragmentSucceeded
            keyKind
            keyBuilder
            keyCount
            .
            (eliminate
              JSONRenderFragment
              (lambda unrestricted current : (family JSONRenderFragment) .
                (family JSONRenderFragment))
              memberInduction
              (branch
                JSONRenderFragmentSucceeded
                memberKind
                memberBuilder
                memberCount
                .
                (eliminate
                  JSONRenderFragment
                  (lambda unrestricted current : (family JSONRenderFragment) .
                    (family JSONRenderFragment))
                  tailInduction
                  (branch
                    JSONRenderFragmentSucceeded
                    tailKind
                    tailBuilder
                    tailCount
                    .
                    (nat-eliminate
                      (lambda unrestricted validKey : Nat . (family JSONRenderFragment))
                      jsonRenderFailure
                      (lambda unrestricted keyPredecessor : Nat .
                        (lambda unrestricted keyInduction : (family JSONRenderFragment) .
                          (nat-eliminate
                            (lambda unrestricted validMember : Nat . (family JSONRenderFragment))
                            jsonRenderFailure
                            (lambda unrestricted memberPredecessor : Nat .
                              (lambda unrestricted memberRoleInduction : (family JSONRenderFragment) .
                                (nat-eliminate
                                  (lambda unrestricted validTail : Nat .
                                    (family JSONRenderFragment))
                                  jsonRenderFailure
                                  (lambda unrestricted tailPredecessor : Nat .
                                    (lambda unrestricted tailRoleInduction : (family JSONRenderFragment) .
                                      (constructor
                                        JSONRenderFragment
                                        JSONRenderFragmentSucceeded
                                        (constructor JSONRenderKind JSONRenderObjectMembersKind)
                                        (bytes-builder-append
                                        keyBuilder
                                        (bytes-builder-append
                                        (bytes-builder-chunk b":")
                                        (bytes-builder-append
                                        memberBuilder
                                        (bytes-builder-append
                                        (jsonRenderCommaBefore tailCount)
                                        tailBuilder))))
                                        (succ tailCount))))
                                  (jsonRenderKindIsObjectMembers tailKind))))
                            (jsonRenderKindIsValue memberKind))))
                      (jsonRenderKindIsValue keyKind)))
                  (branch
                    JSONRenderFragmentFailed
                    code
                    .
                    (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
              (branch
                JSONRenderFragmentFailed
                code
                .
                (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
          (branch
            JSONRenderFragmentFailed
            code
            .
            (constructor JSONRenderFragment JSONRenderFragmentFailed code))))))

-- Part of `jsonRenderTree`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonRenderTreePart2 =
  (lambda unrestricted tailInduction : (family JSONRenderFragment) .
    (lambda unrestricted headKind : (family JSONRenderKind) .
      (lambda unrestricted headBuilder : BytesBuilder .
        (eliminate
          JSONRenderFragment
          (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
          tailInduction
          (branch
            JSONRenderFragmentSucceeded
            tailKind
            tailBuilder
            tailCount
            .
            (nat-eliminate
              (lambda unrestricted validHead : Nat . (family JSONRenderFragment))
              jsonRenderFailure
              (lambda unrestricted headPredecessor : Nat .
                (lambda unrestricted headRoleInduction : (family JSONRenderFragment) .
                  (nat-eliminate
                    (lambda unrestricted validTail : Nat . (family JSONRenderFragment))
                    jsonRenderFailure
                    (lambda unrestricted tailPredecessor : Nat .
                      (lambda unrestricted tailRoleInduction : (family JSONRenderFragment) .
                        (constructor
                          JSONRenderFragment
                          JSONRenderFragmentSucceeded
                          (constructor JSONRenderKind JSONRenderArrayValuesKind)
                          (bytes-builder-append
                            headBuilder
                            (bytes-builder-append (jsonRenderCommaBefore tailCount) tailBuilder))
                          (succ tailCount))))
                    (jsonRenderKindIsArrayValues tailKind))))
              (jsonRenderKindIsValue headKind)))
          (branch
            JSONRenderFragmentFailed
            code
            .
            (constructor JSONRenderFragment JSONRenderFragmentFailed code))))))

def jsonRenderTree =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSON
      (lambda unrestricted current : (family JSON) . (family JSONRenderFragment))
      value
      (branch
        JSONObject
        members
        membersInduction
        .
        (eliminate
          JSONRenderFragment
          (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
          membersInduction
          (branch
            JSONRenderFragmentSucceeded
            kind
            builder
            count
            .
            (nat-eliminate
              (lambda unrestricted valid : Nat . (family JSONRenderFragment))
              jsonRenderFailure
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family JSONRenderFragment) .
                  (constructor
                    JSONRenderFragment
                    JSONRenderFragmentSucceeded
                    (constructor JSONRenderKind JSONRenderValueKind)
                    (bytes-builder-append
                      (bytes-builder-chunk b"{")
                      (bytes-builder-append builder (bytes-builder-chunk b"}")))
                    (succ zero))))
              (jsonRenderKindIsObjectMembers kind)))
          (branch
            JSONRenderFragmentFailed
            code
            .
            (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
      (branch
        JSONObjectEnd
        .
        (constructor
          JSONRenderFragment
          JSONRenderFragmentSucceeded
          (constructor JSONRenderKind JSONRenderObjectMembersKind)
          (bytes-builder-empty)
          zero))
      (branch
        JSONObjectMember
        key
        member
        tail
        memberInduction
        tailInduction
        .
        (jsonRenderTreePart1 key memberInduction tailInduction))
      (branch
        JSONArray
        values
        valuesInduction
        .
        (eliminate
          JSONRenderFragment
          (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
          valuesInduction
          (branch
            JSONRenderFragmentSucceeded
            kind
            builder
            count
            .
            (nat-eliminate
              (lambda unrestricted valid : Nat . (family JSONRenderFragment))
              jsonRenderFailure
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family JSONRenderFragment) .
                  (constructor
                    JSONRenderFragment
                    JSONRenderFragmentSucceeded
                    (constructor JSONRenderKind JSONRenderValueKind)
                    (bytes-builder-append
                      (bytes-builder-chunk b"[")
                      (bytes-builder-append builder (bytes-builder-chunk b"]")))
                    (succ zero))))
              (jsonRenderKindIsArrayValues kind)))
          (branch
            JSONRenderFragmentFailed
            code
            .
            (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
      (branch
        JSONArrayEnd
        .
        (constructor
          JSONRenderFragment
          JSONRenderFragmentSucceeded
          (constructor JSONRenderKind JSONRenderArrayValuesKind)
          (bytes-builder-empty)
          zero))
      (branch
        JSONArrayNext
        head
        tail
        headInduction
        tailInduction
        .
        (eliminate
          JSONRenderFragment
          (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
          headInduction
          (branch
            JSONRenderFragmentSucceeded
            headKind
            headBuilder
            headCount
            .
            (jsonRenderTreePart2 tailInduction headKind headBuilder))
          (branch
            JSONRenderFragmentFailed
            code
            .
            (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
      (branch JSONString text . (jsonRenderStringFragment text))
      (branch
        JSONNumber
        number
        .
        (eliminate
          JSONNumberParseResult
          (lambda unrestricted current : (family JSONNumberParseResult) .
            (family JSONRenderFragment))
          (jsonParseNumber number)
          (branch
            JSONNumberParsed
            parsed
            remaining
            .
            (nat-eliminate
              (lambda unrestricted noTrailing : Nat . (family JSONRenderFragment))
              jsonRenderFailure
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family JSONRenderFragment) .
                  (constructor
                    JSONRenderFragment
                    JSONRenderFragmentSucceeded
                    (constructor JSONRenderKind JSONRenderValueKind)
                    (bytes-builder-chunk parsed)
                    (succ zero))))
              (naturalIsZero (bytes-length remaining))))
          (branch JSONNumberParseFailed code remaining . jsonRenderFailure)))
      (branch
        JSONBoolean
        boolean
        .
        (constructor
          JSONRenderFragment
          JSONRenderFragmentSucceeded
          (constructor JSONRenderKind JSONRenderValueKind)
          (nat-eliminate
            (lambda unrestricted current : Nat . BytesBuilder)
            (bytes-builder-chunk b"false")
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : BytesBuilder .
                (bytes-builder-chunk b"true")))
            boolean)
          (succ zero)))
      (branch
        JSONNull
        .
        (constructor
          JSONRenderFragment
          JSONRenderFragmentSucceeded
          (constructor JSONRenderKind JSONRenderValueKind)
          (bytes-builder-chunk b"null")
          (succ zero)))))

def jsonRenderUnchecked =
  (lambda unrestricted value : (family JSON) .
    (eliminate
      JSONRenderFragment
      (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderResult))
      (jsonRenderTree value)
      (branch
        JSONRenderFragmentSucceeded
        kind
        builder
        count
        .
        (nat-eliminate
          (lambda unrestricted valid : Nat . (family JSONRenderResult))
          (constructor
            JSONRenderResult
            JSONRenderFailed
            (constructor JSONErrorCode JSONMalformedTree))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family JSONRenderResult) .
              (constructor JSONRenderResult JSONRendered (bytes-builder-build builder))))
          (jsonRenderKindIsValue kind)))
      (branch JSONRenderFragmentFailed code . (constructor JSONRenderResult JSONRenderFailed code))))

def jsonEmptyRenderTelemetry =
  (constructor JSONRenderTelemetry JSONRenderTelemetryValue jsonCountsZero zero zero)

def renderJSONObservedWithLimits =
  (lambda unrestricted limits : (family JSONLimits) .
    (lambda unrestricted value : (family JSON) .
      (eliminate
        JSONLimits
        (lambda unrestricted current : (family JSONLimits) . (family JSONObservedRenderResult))
        limits
        (branch
          JSONLimitsValue
          maximumInputBytes
          maximumDepth
          maximumStringBytes
          maximumNumberBytes
          maximumContainerEntries
          maximumOutputBytes
          .
          (eliminate
            JSONTreeAuditResult
            (lambda unrestricted current : (family JSONTreeAuditResult) .
              (family JSONObservedRenderResult))
            (jsonAuditTreeWithTokenLimits
              maximumStringBytes
              maximumNumberBytes
              maximumContainerEntries
              value)
            (branch
              JSONTreeAuditSucceeded
              kind
              counts
              depth
              sequenceCount
              .
              (nat-eliminate
                (lambda unrestricted valueKind : Nat . (family JSONObservedRenderResult))
                (constructor
                  JSONObservedRenderResult
                  JSONObservedRenderFailed
                  (constructor JSONErrorCode JSONMalformedTree)
                  (constructor JSONRenderTelemetry JSONRenderTelemetryValue counts depth zero))
                (lambda unrestricted kindPredecessor : Nat .
                  (lambda unrestricted kindInduction : (family JSONObservedRenderResult) .
                    (nat-eliminate
                      (lambda unrestricted depthBounded : Nat . (family JSONObservedRenderResult))
                      (constructor
                        JSONObservedRenderResult
                        JSONObservedRenderFailed
                        (constructor JSONErrorCode JSONDepthLimitExceeded)
                        (constructor JSONRenderTelemetry JSONRenderTelemetryValue counts depth zero))
                      (lambda unrestricted depthPredecessor : Nat .
                        (lambda unrestricted depthInduction : (family JSONObservedRenderResult) .
                          (eliminate
                            JSONRenderResult
                            (lambda unrestricted current : (family JSONRenderResult) .
                              (family JSONObservedRenderResult))
                            (jsonRenderUnchecked value)
                            (branch
                              JSONRendered
                              output
                              .
                              (nat-eliminate
                                (lambda unrestricted outputBounded : Nat .
                                  (family JSONObservedRenderResult))
                                (constructor
                                  JSONObservedRenderResult
                                  JSONObservedRenderFailed
                                  (constructor JSONErrorCode JSONOutputLimitExceeded)
                                  (constructor
                                    JSONRenderTelemetry
                                    JSONRenderTelemetryValue
                                    counts
                                    depth
                                    (bytes-length output)))
                                (lambda unrestricted outputPredecessor : Nat .
                                  (lambda unrestricted outputInduction : (family JSONObservedRenderResult) .
                                    (constructor
                                      JSONObservedRenderResult
                                      JSONObservedRendered
                                      output
                                      (constructor
                                        JSONRenderTelemetry
                                        JSONRenderTelemetryValue
                                        counts
                                        depth
                                        (bytes-length output)))))
                                (jsonBoundAllows maximumOutputBytes (bytes-length output))))
                            (branch
                              JSONRenderFailed
                              code
                              .
                              (constructor
                                JSONObservedRenderResult
                                JSONObservedRenderFailed
                                code
                                (constructor
                                  JSONRenderTelemetry
                                  JSONRenderTelemetryValue
                                  counts
                                  depth
                                  zero))))))
                      (jsonBoundAllows maximumDepth depth))))
                (jsonTreeKindIsValue kind)))
            (branch
              JSONTreeAuditFailed
              code
              .
              (constructor
                JSONObservedRenderResult
                JSONObservedRenderFailed
                code
                jsonEmptyRenderTelemetry)))))))

def renderJSONWithLimits =
  (lambda unrestricted limits : (family JSONLimits) .
    (lambda unrestricted value : (family JSON) .
      (eliminate
        JSONObservedRenderResult
        (lambda unrestricted current : (family JSONObservedRenderResult) .
          (family JSONRenderResult))
        (renderJSONObservedWithLimits limits value)
        (branch
          JSONObservedRendered
          output
          telemetry
          .
          (constructor JSONRenderResult JSONRendered output))
        (branch
          JSONObservedRenderFailed
          code
          telemetry
          .
          (constructor JSONRenderResult JSONRenderFailed code)))))

def renderJSON =
  (lambda unrestricted value : (family JSON) . (renderJSONWithLimits jsonDefaultLimits value))