!import "base.tri" !Local
!import "list.tri" !Local
!import "bytes.tri" !Local
!import "binary.tri" !Local

arboricxMagic = [(65) (82) (66) (79) (82) (73) (67) (88)]
arboricxMajorVersion = [(0) (1)]
arboricxMinorVersion = [(0) (0)]
arboricxManifestSectionId = [(0) (0) (0) (1)]
arboricxNodesSectionId = [(0) (0) (0) (2)]

-- Manifest magic and version constants
arboricxManifestMagic = [(65) (82) (66) (77) (78) (70) (83) (84)]
arboricxManifestMajorVersion = [(0) (1)]
arboricxManifestMinorVersion = [(0) (0)]

errMissingSection = 4
errUnsupportedVersion = 5
errDuplicateSection = 6
errDuplicateNode = 7
errInvalidNodePayload = 8
errMissingNode = 9
errInvalidManifestMagic = 10
errUnsupportedManifestVersion = 11
errTrailingManifestBytes = 12
errManifestValidationFailed = 13

nodePayloadLeafTag = 0
nodePayloadStemTag = 1
nodePayloadForkTag = 2

readArboricxMagic = (bs : expectBytes arboricxMagic bs)

readArboricxHeader = (bs :
  bindResult (readArboricxMagic bs)
    (_ afterMagic :
      bindResult (readBytes 2 afterMagic)
        (majorVersion afterMajor :
          bindResult (readBytes 2 afterMajor)
            (minorVersion afterMinor :
              bindResult (readBytes 4 afterMinor)
                (sectionCount afterSectionCount :
                  bindResult (readBytes 8 afterSectionCount)
                    (flags afterFlags :
                      bindResult (readBytes 8 afterFlags)
                        (dirOffset afterDirOffset :
                          ok
                            (pair majorVersion
                              (pair minorVersion
                                (pair sectionCount
                                  (pair flags dirOffset))))
                            afterDirOffset)))))))

readSectionRecord = (bs :
  bindResult (readBytes 4 bs)
    (sectionId afterSectionId :
      bindResult (readBytes 2 afterSectionId)
        (sectionVersion afterSectionVersion :
          bindResult (readBytes 2 afterSectionVersion)
            (sectionFlags afterSectionFlags :
              bindResult (readBytes 2 afterSectionFlags)
                (compression afterCompression :
                  bindResult (readBytes 2 afterCompression)
                    (digestAlgorithm afterDigestAlgorithm :
                      bindResult (readBytes 8 afterDigestAlgorithm)
                        (offset afterOffset :
                          bindResult (readBytes 8 afterOffset)
                            (length afterLength :
                              bindResult (readBytes 32 afterLength)
                                (digest afterDigest :
                                  ok
                                    (pair sectionId
                                      (pair sectionVersion
                                        (pair sectionFlags
                                          (pair compression
                                            (pair digestAlgorithm
                                              (pair offset
                                                (pair length digest)))))))
                                    afterDigest)))))))))

readSectionDirectory_ = y (self bs sectionCount i acc :
  matchBool
    (ok (reverse acc) bs)
    (bindResult (readSectionRecord bs)
      (sectionRecord afterSectionRecord :
        self afterSectionRecord sectionCount (succ i) (pair sectionRecord acc)))
    (equal? i sectionCount))

readSectionDirectory = (sectionCount bs : readSectionDirectory_ bs sectionCount 0 t)

sectionRecordId = (sectionRecord :
  matchPair
    (sectionId _ : sectionId)
    sectionRecord)

sectionRecordVersion = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (sectionVersion _ : sectionVersion)
        payload)
    sectionRecord)

sectionRecordFlags = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (sectionFlags _ : sectionFlags)
            payload2)
        payload)
    sectionRecord)

sectionRecordCompression = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (compression _ : compression)
                payload3)
            payload2)
        payload)
    sectionRecord)

sectionRecordDigestAlgorithm = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (_ payload4 :
                  matchPair
                    (digestAlgorithm _ : digestAlgorithm)
                    payload4)
                payload3)
            payload2)
        payload)
    sectionRecord)

sectionRecordOffset = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (_ payload4 :
                  matchPair
                    (_ payload5 :
                      matchPair
                        (offset _ : offset)
                        payload5)
                    payload4)
                payload3)
            payload2)
        payload)
    sectionRecord)

sectionRecordLength = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (_ payload4 :
                  matchPair
                    (_ payload5 :
                      matchPair
                        (_ payload6 :
                          matchPair
                            (length _ : length)
                            payload6)
                        payload5)
                    payload4)
                payload3)
            payload2)
        payload)
    sectionRecord)

sectionRecordDigest = (sectionRecord :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (_ payload4 :
                  matchPair
                    (_ payload5 :
                      matchPair
                        (_ payload6 :
                          matchPair
                            (_ digest : digest)
                            payload6)
                        payload5)
                    payload4)
                payload3)
            payload2)
        payload)
    sectionRecord)

lookupSectionRecord_ = y (self directory sectionId :
  matchList
    nothing
    (sectionRecord rest :
      matchBool
        (just sectionRecord)
        (self rest sectionId)
        (bytesEq? sectionId (sectionRecordId sectionRecord)))
    directory)

lookupSectionRecord = (sectionId directory : lookupSectionRecord_ directory sectionId)

sectionDirectoryHasId?_ = y (self directory sectionId :
  matchList
    false
    (sectionRecord rest :
      or?
        (bytesEq? sectionId (sectionRecordId sectionRecord))
        (self rest sectionId))
    directory)

sectionDirectoryHasId? = (sectionId directory : sectionDirectoryHasId?_ directory sectionId)

sectionDirectoryHasDuplicateIds? = y (self directory :
  matchList
    false
    (sectionRecord rest :
      or?
        (sectionDirectoryHasId?_ rest (sectionRecordId sectionRecord))
        (self rest))
    directory)

validateSectionDirectory = (directory rest :
  matchBool
    (err errDuplicateSection rest)
    (ok directory rest)
    (sectionDirectoryHasDuplicateIds? directory))

byteSlice = (offset length bytes : bytesTake length (bytesDrop offset bytes))

natMake = (bit rest :
  matchBool
    0
    (pair bit rest)
    (and? (equal? bit 0) (equal? rest 0)))

natAdd = y (self a b :
  triage
    b
    (_ : b)
    (aBit aRest :
      triage
        a
        (_ : a)
        (bBit bRest :
          matchBool
            (natMake 0 (succ (self aRest bRest)))
            (natMake (matchBool (matchBool 0 1 bBit) (matchBool 1 0 bBit) aBit)
              (self aRest bRest))
            (and? (equal? aBit 1) (equal? bBit 1)))
        b)
    a)

natDouble = (n : matchBool 0 (pair 0 n) (equal? n 0))

natTimes256 = (n :
  natDouble
    (natDouble
      (natDouble
        (natDouble
          (natDouble
            (natDouble
              (natDouble
                (natDouble n))))))))

byteNatShiftAppend_ = y (self byte acc i :
  matchBool
    acc
    (triage
      (natMake 0 (self 0 acc (succ i)))
      (_ : acc)
      (bit rest : natMake bit (self rest acc (succ i)))
      byte)
    (equal? i 8))

byteNatShiftAppend = (byte acc : byteNatShiftAppend_ byte acc 0)

beBytesToNat = (bytes :
  foldl
    (acc byte : byteNatShiftAppend byte acc)
    0
    bytes)

u32BEBytesToNat = beBytesToNat
u64BEBytesToNat = beBytesToNat

arboricxHeaderMajorVersion = (header :
  matchPair
    (majorVersion _ : majorVersion)
    header)

arboricxHeaderMinorVersion = (header :
  matchPair
    (_ payload :
      matchPair
        (minorVersion _ : minorVersion)
        payload)
    header)

arboricxHeaderSectionCount = (header :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (sectionCount _ : sectionCount)
            payload2)
        payload)
    header)

arboricxHeaderFlags = (header :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (flags _ : flags)
                payload3)
            payload2)
        payload)
    header)

arboricxHeaderDirOffset = (header :
  matchPair
    (_ payload :
      matchPair
        (_ payload2 :
          matchPair
            (_ payload3 :
              matchPair
                (_ dirOffset : dirOffset)
                payload3)
            payload2)
        payload)
    header)

validateArboricxHeader = (header rest :
  matchBool
    (ok header rest)
    (err errUnsupportedVersion rest)
    (and?
      (bytesEq? arboricxMajorVersion (arboricxHeaderMajorVersion header))
      (bytesEq? arboricxMinorVersion (arboricxHeaderMinorVersion header))))

readArboricxContainer = (bs :
  bindResult (readArboricxHeader bs)
    (header afterHeader :
      bindResult (validateArboricxHeader header afterHeader)
        (validHeader afterValidHeader :
          bindResult (readSectionDirectory
            (u32BEBytesToNat (arboricxHeaderSectionCount validHeader))
            (bytesDrop (u64BEBytesToNat (arboricxHeaderDirOffset validHeader)) bs))
            (directory afterDirectory :
              bindResult (validateSectionDirectory directory afterDirectory)
                (validDirectory afterValidDirectory :
                  ok (pair validHeader validDirectory) afterValidDirectory)))))

sectionRecordOffsetNat = (sectionRecord :
  u64BEBytesToNat (sectionRecordOffset sectionRecord))

sectionRecordLengthNat = (sectionRecord :
  u64BEBytesToNat (sectionRecordLength sectionRecord))

extractSectionBytes = (sectionRecord containerBytes :
  byteSlice
    (sectionRecordOffsetNat sectionRecord)
    (sectionRecordLengthNat sectionRecord)
    containerBytes)

extractSectionBytesResult = (sectionRecord containerBytes rest :
  (sectionBytes :
    matchBool
      (ok sectionBytes rest)
      (err errUnexpectedEof rest)
      (equal? (bytesLength sectionBytes) (sectionRecordLengthNat sectionRecord)))
    (extractSectionBytes sectionRecord containerBytes))

lookupSectionBytes = (sectionId directory containerBytes :
  triage
    nothing
    (sectionRecord : just (extractSectionBytes sectionRecord containerBytes))
    (_ _ : nothing)
    (lookupSectionRecord sectionId directory))

sectionBytesOrErr = (sectionId directory containerBytes rest :
  triage
    (err errMissingSection rest)
    (sectionRecord : extractSectionBytesResult sectionRecord containerBytes rest)
    (_ _ : err errMissingSection rest)
    (lookupSectionRecord sectionId directory))

readArboricxSectionBytes = (sectionId bs :
  bindResult (readArboricxContainer bs)
    (container afterContainer :
      matchPair
        (_ directory : sectionBytesOrErr sectionId directory bs afterContainer)
        container))

readArboricxRequiredSections = (bs :
  bindResult (readArboricxContainer bs)
    (container afterContainer :
      matchPair
        (_ directory :
          bindResult (sectionBytesOrErr arboricxManifestSectionId directory bs afterContainer)
            (manifestBytes _ :
              bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer)
                (nodesBytes _ :
                  ok (pair manifestBytes nodesBytes) afterContainer)))
        container))