!import "arboricx-common.tri" !Local

readNodeRecord = (bs :
  bindResult (readBytes 32 bs)
    (nodeHash afterNodeHash :
      bindResult (readBytes 4 afterNodeHash)
        (payloadLength afterPayloadLength :
          bindResult (readBytes (u32BEBytesToNat payloadLength) afterPayloadLength)
            (payload afterPayload :
              ok
                (pair nodeHash
                  (pair payloadLength payload))
                afterPayload))))

nodeRecordHash = (nodeRecord :
  matchPair
    (nodeHash _ : nodeHash)
    nodeRecord)

nodeRecordPayloadLength = (nodeRecord :
  matchPair
    (_ payload :
      matchPair
        (payloadLength _ : payloadLength)
        payload)
    nodeRecord)

nodeRecordPayload = (nodeRecord :
  matchPair
    (_ payload :
      matchPair
        (_ nodePayload : nodePayload)
        payload)
    nodeRecord)

nodePayloadKind = (nodePayload : bytesHead nodePayload)

nodePayloadHasTag? = (tag nodePayload :
  triage
    false
    (actualTag : byteEq? actualTag tag)
    (_ _ : false)
    (nodePayloadKind nodePayload))

nodePayloadLeaf? = (nodePayload : bytesEq? [(0)] nodePayload)

nodePayloadStem? = (nodePayload :
  and?
    (nodePayloadHasTag? nodePayloadStemTag nodePayload)
    (equal? (bytesLength nodePayload) 33))

nodePayloadFork? = (nodePayload :
  and?
    (nodePayloadHasTag? nodePayloadForkTag nodePayload)
    (equal? (bytesLength nodePayload) 65))

nodePayloadValid? = (nodePayload :
  or?
    (nodePayloadLeaf? nodePayload)
    (or?
      (nodePayloadStem? nodePayload)
      (nodePayloadFork? nodePayload)))

nodePayloadStemChildHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload))
nodePayloadForkLeftHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload))
nodePayloadForkRightHash = (nodePayload : bytesTake 32 (bytesDrop 33 nodePayload))

nodeRecordPayloadValid? = (nodeRecord : nodePayloadValid? (nodeRecordPayload nodeRecord))

nodeRecordsHaveInvalidPayload? = y (self nodeRecords :
  matchList
    false
    (nodeRecord rest :
      or?
        (not? (nodeRecordPayloadValid? nodeRecord))
        (self rest))
    nodeRecords)

nodeRecordsHaveHash? = y (self nodeRecords nodeHash :
  matchList
    false
    (nodeRecord rest :
      or?
        (bytesEq? nodeHash (nodeRecordHash nodeRecord))
        (self rest nodeHash))
    nodeRecords)

nodeRecordsHaveDuplicateHashes? = y (self nodeRecords :
  matchList
    false
    (nodeRecord rest :
      or?
        (nodeRecordsHaveHash? rest (nodeRecordHash nodeRecord))
        (self rest))
    nodeRecords)

lookupNodeRecord_ = y (self nodeRecords nodeHash :
  matchList
    nothing
    (nodeRecord rest :
      matchBool
        (just nodeRecord)
        (self rest nodeHash)
        (bytesEq? nodeHash (nodeRecordHash nodeRecord)))
    nodeRecords)

lookupNodeRecord = (nodeHash nodeRecords : lookupNodeRecord_ nodeRecords nodeHash)

nodeRecordChildHashes = (nodeRecord :
  (nodePayload :
    matchBool
      t
      (matchBool
        (pair (nodePayloadStemChildHash nodePayload) t)
        (pair (nodePayloadForkLeftHash nodePayload)
          (pair (nodePayloadForkRightHash nodePayload) t))
        (nodePayloadStem? nodePayload))
      (nodePayloadLeaf? nodePayload))
    (nodeRecordPayload nodeRecord))

nodeHashPresent? = (nodeHash nodeRecords : nodeRecordsHaveHash? nodeRecords nodeHash)

nodeChildHashesPresent? = y (self childHashes nodeRecords :
  matchList
    true
    (childHash rest :
      and?
        (nodeHashPresent? childHash nodeRecords)
        (self rest nodeRecords))
    childHashes)

nodeRecordChildrenPresent? = (nodeRecord nodeRecords :
  nodeChildHashesPresent? (nodeRecordChildHashes nodeRecord) nodeRecords)

nodeRecordsClosed? = y (self nodeRecords allNodeRecords :
  matchList
    true
    (nodeRecord rest :
      and?
        (nodeRecordChildrenPresent? nodeRecord allNodeRecords)
        (self rest allNodeRecords))
    nodeRecords)

validateNodeRecords = (nodeRecords rest :
  matchBool
    (err errInvalidNodePayload rest)
    (matchBool
      (err errDuplicateNode rest)
      (matchBool
        (ok nodeRecords rest)
        (err errMissingNode rest)
        (nodeRecordsClosed? nodeRecords nodeRecords))
      (nodeRecordsHaveDuplicateHashes? nodeRecords))
    (nodeRecordsHaveInvalidPayload? nodeRecords))

readNodeRecords_ = y (self bs nodeCount i acc :
  matchBool
    (ok (reverse acc) bs)
    (bindResult (readNodeRecord bs)
      (nodeRecord afterNodeRecord :
        self afterNodeRecord nodeCount (succ i) (pair nodeRecord acc)))
    (equal? i nodeCount))

readNodeRecords = (nodeCount bs : readNodeRecords_ bs nodeCount 0 t)

readNodesSection = (bs :
  bindResult (readBytes 8 bs)
    (nodeCount afterNodeCount :
      bindResult (readNodeRecords (u64BEBytesToNat nodeCount) afterNodeCount)
        (nodeRecords afterNodeRecords :
          bindResult (validateNodeRecords nodeRecords afterNodeRecords)
            (validNodeRecords afterValidNodeRecords :
              ok (pair nodeCount validNodeRecords) afterValidNodeRecords))))

readNodesSectionComplete = (bs :
  bindResult (readNodesSection bs)
    (nodesSection afterNodesSection :
      matchBool
        (ok nodesSection afterNodesSection)
        (err errUnexpectedBytes afterNodesSection)
        (bytesNil? afterNodesSection)))

readArboricxNodesSection = (bs :
  bindResult (readArboricxContainer bs)
    (container afterContainer :
      matchPair
        (_ directory :
          bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer)
            (nodesBytes _ :
              bindResult (readNodesSectionComplete nodesBytes)
                (nodesSection _ : ok nodesSection afterContainer)))
        container))

nodesSectionCount = (nodesSection :
  matchPair
    (nodeCount _ : nodeCount)
    nodesSection)

nodesSectionRecords = (nodesSection :
  matchPair
    (_ nodeRecords : nodeRecords)
    nodesSection)

nodeRecordToTreeWith = (self nodeRecords nodeRecord :
  (nodePayload :
    matchBool
      (ok t t)
      (matchBool
        (bindResult (self (nodePayloadStemChildHash nodePayload) nodeRecords)
          (child _ : ok (t child) t))
        (bindResult (self (nodePayloadForkLeftHash nodePayload) nodeRecords)
          (left _ :
            bindResult (self (nodePayloadForkRightHash nodePayload) nodeRecords)
              (right _ : ok (pair left right) t)))
        (nodePayloadStem? nodePayload))
      (nodePayloadLeaf? nodePayload))
    (nodeRecordPayload nodeRecord))

nodeHashToTree = y (self nodeHash nodeRecords :
  triage
    (err errMissingNode t)
    (nodeRecord : nodeRecordToTreeWith self nodeRecords nodeRecord)
    (_ _ : err errMissingNode t)
    (lookupNodeRecord nodeHash nodeRecords))

readArboricxTreeFromHash = (rootHash bs :
  bindResult (readArboricxNodesSection bs)
    (nodesSection afterContainer :
      bindResult (nodeHashToTree rootHash (nodesSectionRecords nodesSection))
        (tree _ : ok tree afterContainer)))

readArboricxExecutableFromHash = readArboricxTreeFromHash