tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

6c0e9998875942bb19c1f783ebffe61b23aa1eb578a46a874034444c4a9a3c49.tri (5681B)

      1 !import prelude *
      2 !import binary *
      3 !import arboricx_common *
      4 !import native_math as N
      5 !export readNodeRecord
      6 !export nodePayloadKind
      7 !export nodePayloadHasTag?
      8 !export nodePayloadLeaf?
      9 !export nodePayloadStem?
     10 !export nodePayloadFork?
     11 !export nodePayloadValid?
     12 !export nodePayloadChildIndices
     13 !export nodeRecordsHaveInvalidPayload?
     14 !export validateNodeRecords
     15 !export readNodeRecords
     16 !export readNodesSection
     17 !export readNodesSectionComplete
     18 !export nodesSectionCount
     19 !export nodesSectionRecords
     20 !export readArboricxNodesSection
     21 !export nodeIndexToTree
     22 !export readArboricxTreeFromIndex
     23 !export readArboricxExecutableFromIndex
     24 
     25 -- Indexed records contain canonical octets and strictly backward u32 indices.
     26 readNodeRecord = (do bindParser
     27   payloadLength <- readBytes 4
     28   payload <- readBytes (u32BEBytesToNat payloadLength)
     29   pureParser payload)
     30 
     31 nodePayloadKind = bytesHead
     32 nodePayloadHasTag? tag payload = case payload of
     33   [actual | _] = equal? actual tag
     34   _ = false
     35 nodePayloadLeaf? payload = equal? payload [0]
     36 nodePayloadStem? payload = case payload of
     37   [1 a b c d] = binaryBytes? [a b c d]
     38   _ = false
     39 nodePayloadFork? payload = case payload of
     40   [2 a b c d e f g h] = binaryBytes? [a b c d e f g h]
     41   _ = false
     42 nodePayloadValid? payload = or? (nodePayloadLeaf? payload) (or? (nodePayloadStem? payload) (nodePayloadFork? payload))
     43 nodePayloadChildIndices payload = case payload of
     44   [1 a b c d] = [(u32BEBytesToNat [a b c d])]
     45   [2 a b c d e f g h] = [(u32BEBytesToNat [a b c d]) (u32BEBytesToNat [e f g h])]
     46   _ = []
     47 nodeRecordsHaveInvalidPayload? records = case records of
     48   [] = false
     49   [payload | rest] = or? (not? (nodePayloadValid? payload)) (nodeRecordsHaveInvalidPayload? rest)
     50   _ = true
     51 
     52 -- Persistent bit trie: slot Maybe value, then (zero branch, one branch).
     53 -- Canonical natural keys; no linear search through the built prefix per edge.
     54 nodeTableGet index table = case table of
     55   (slot, (left, right)) = (case index of
     56     0 = matchMaybe (err errMissingNode t) (value : ok value t) slot
     57     (t bit rest) = lazyBool (_ : nodeTableGet rest right) (_ : nodeTableGet rest left) bit
     58     _ = err errMissingNode t)
     59   _ = err errMissingNode t
     60 
     61 nodeTablePut index value table = (let
     62   update slot left right = (case index of
     63     0 = pair (just value) (pair left right)
     64     (t bit rest) = (lazyBool
     65       (_ : pair slot (pair left (nodeTablePut rest value right)))
     66       (_ : pair slot (pair (nodeTablePut rest value left) right))
     67       bit)
     68     _ = table)
     69   in case table of
     70     (slot, (left, right)) = update slot left right
     71     _ = update nothing t t)
     72 
     73 -- Preserve payload-error precedence across the whole section, then reject
     74 -- forward/missing edges and duplicate canonical payloads. Payload keys cannot
     75 -- collide: leaf=0, stems start with 1 over five bytes, forks with 2 over nine.
     76 validateNodeRecords records rest = (lazyBool
     77   (_ : err errInvalidNodePayload rest)
     78   (_ : let rec
     79     walk remaining index seen = (case remaining of
     80       [] = ok records rest
     81       [payload | tail] = (lazyBool
     82         (_ : let key = beBytesToNat payload in lazyBool
     83           (_ : err errDuplicateNode rest)
     84           (_ : walk tail (N.successor index) (nodeTablePut key t seen))
     85           (fst (nodeTableGet key seen)))
     86         (_ : err errMissingNode rest)
     87         (all? (child : N.lt child index) (nodePayloadChildIndices payload)))
     88       _ = err errInvalidNodePayload rest)
     89     in walk records 0 t)
     90   (nodeRecordsHaveInvalidPayload? records))
     91 
     92 readNodeRecords count = repeatParser count readNodeRecord
     93 readNodesSection = (do bindParser
     94   count <- readBytes 8
     95   records <- readNodeRecords (u64BEBytesToNat count)
     96   valid <- validateNodeRecords records
     97   pureParser (pair count valid))
     98 readNodesSectionComplete bytes = (bindResult (readNodesSection bytes)
     99   (value rest : case rest of
    100     [] = ok value rest
    101     _ = err errUnexpectedBytes rest))
    102 nodesSectionCount = fst
    103 nodesSectionRecords = snd
    104 
    105 readArboricxNodesSection bytes = (bindResult (readArboricxContainer bytes)
    106   (container rest : bindResult (sectionBytesOrErr arboricxNodesSectionId (snd container) bytes rest)
    107     (payload _ : bindResult (readNodesSectionComplete payload)
    108       (nodes _ : ok nodes rest))))
    109 
    110 -- Reconstruction validates each consumed record. The full bundle boundary
    111 -- validates *all* records before selecting a root. Output expansion/resource
    112 -- bounds are not guaranteed merely because the input DAG is small.
    113 nodePayloadToTreeFromBuilt table payload = (lazyBool
    114   (_ : case payload of
    115     [0] = ok t t
    116     [1 a b c d] = (bindResult (nodeTableGet (u32BEBytesToNat [a b c d]) table)
    117       (child _ : ok (t child) t))
    118     [2 a b c d e f g h] = (bindResult (nodeTableGet (u32BEBytesToNat [a b c d]) table)
    119       (left _ : bindResult (nodeTableGet (u32BEBytesToNat [e f g h]) table)
    120         (right _ : ok (pair left right) t)))
    121     _ = err errInvalidNodePayload t)
    122   (_ : err errInvalidNodePayload t)
    123   (nodePayloadValid? payload))
    124 
    125 nodeIndexToTree records target = (lazyBool
    126   (_ : let rec
    127     walk remaining index table = (case remaining of
    128       [] = err errMissingNode t
    129       [payload | tail] = (bindResult (nodePayloadToTreeFromBuilt table payload)
    130         (tree _ : lazyBool
    131           (_ : ok tree t)
    132           (_ : walk tail (N.successor index) (nodeTablePut index tree table))
    133           (N.equal index target)))
    134       _ = err errInvalidNodePayload t)
    135     in walk records 0 t)
    136   (_ : err errMissingNode t)
    137   (isNat? target))
    138 
    139 readArboricxTreeFromIndex index bytes = (bindResult (readArboricxNodesSection bytes)
    140   (section rest : bindResult (nodeIndexToTree (snd section) (u32BEBytesToNat index))
    141     (tree _ : ok tree rest)))
    142 readArboricxExecutableFromIndex = readArboricxTreeFromIndex