tricu

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

nodes.tri (10943B)

      1 !import "prelude"         !Local
      2 !import "binary"          !Local
      3 !import "arboricx.common" !Local
      4 
      5 -- Indexed Arboricx node section reader.
      6 --
      7 -- Node records in the indexed format are just length-prefixed payloads:
      8 --   u32 payloadLength || payload
      9 -- A payload is one of:
     10 --   0x00
     11 --   0x01 || childIndex:u32be
     12 --   0x02 || leftIndex:u32be || rightIndex:u32be
     13 -- Child indices must point strictly backward in the node array.
     14 
     15 readNodeRecord = (bs :
     16   bindResult (readBytes 4 bs)
     17     (payloadLength afterPayloadLength :
     18       bindResult (readBytes (u32BEBytesToNat payloadLength) afterPayloadLength)
     19         (payload afterPayload :
     20           ok payload afterPayload)))
     21 
     22 nodePayloadKind = (nodePayload : bytesHead nodePayload)
     23 
     24 nodePayloadHasTag? = (tag nodePayload :
     25   triage
     26     false
     27     (actualTag : equal? actualTag tag)
     28     (_ _ : false)
     29     (nodePayloadKind nodePayload))
     30 
     31 nodePayloadLeaf? = (nodePayload :
     32   bytesEq? [(0)] nodePayload)
     33 
     34 nodePayloadStem? = (nodePayload :
     35   and?
     36     (nodePayloadHasTag? nodePayloadStemTag nodePayload)
     37     (equal? (bytesLength nodePayload) 5))
     38 
     39 nodePayloadFork? = (nodePayload :
     40   and?
     41     (nodePayloadHasTag? nodePayloadForkTag nodePayload)
     42     (equal? (bytesLength nodePayload) 9))
     43 
     44 nodePayloadValid? = (nodePayload :
     45   or?
     46     (nodePayloadLeaf? nodePayload)
     47     (or?
     48       (nodePayloadStem? nodePayload)
     49       (nodePayloadFork? nodePayload)))
     50 
     51 nodeU32FromBytes4 = (b0 b1 b2 b3 :
     52   u32BEBytesToNat
     53     (pair b0
     54       (pair b1
     55         (pair b2
     56           (pair b3 t)))))
     57 
     58 withNodePayloadStemIndex = (nodePayload shortK indexK :
     59   matchList
     60     (shortK t)
     61     (tag r0 :
     62       matchList
     63         (shortK t)
     64         (b0 r1 :
     65           matchList
     66             (shortK t)
     67             (b1 r2 :
     68               matchList
     69                 (shortK t)
     70                 (b2 r3 :
     71                   matchList
     72                     (shortK t)
     73                     (b3 _ :
     74                       indexK (nodeU32FromBytes4 b0 b1 b2 b3))
     75                     r3) r2) r1) r0) nodePayload)
     76 
     77 withNodePayloadForkIndices = (nodePayload shortK indicesK :
     78   matchList
     79     (shortK t)
     80     (tag r0 :
     81       matchList
     82         (shortK t)
     83         (l0 r1 :
     84           matchList
     85             (shortK t)
     86             (l1 r2 :
     87               matchList
     88                 (shortK t)
     89                 (l2 r3 :
     90                   matchList
     91                     (shortK t)
     92                     (l3 r4 :
     93                       matchList
     94                         (shortK t)
     95                         (r0b r5 :
     96                           matchList
     97                             (shortK t)
     98                             (r1b r6 :
     99                               matchList
    100                                 (shortK t)
    101                                 (r2b r7 :
    102                                   matchList
    103                                     (shortK t)
    104                                     (r3b _ :
    105                                       indicesK
    106                                         (nodeU32FromBytes4 l0 l1 l2 l3)
    107                                         (nodeU32FromBytes4 r0b r1b r2b r3b)) r7) r6) r5) r4) r3) r2) r1) r0) nodePayload)
    108 
    109 nodePayloadStemChildIndex = (nodePayload :
    110   withNodePayloadStemIndex nodePayload (_ : 0) (index : index))
    111 
    112 nodePayloadForkLeftIndex = (nodePayload :
    113   withNodePayloadForkIndices nodePayload (_ : 0) (left right : left))
    114 
    115 nodePayloadForkRightIndex = (nodePayload :
    116   withNodePayloadForkIndices nodePayload (_ : 0) (left right : right))
    117 
    118 nodeRecordsHaveInvalidPayload? = y (self nodeRecords :
    119   matchList
    120     false
    121     (nodePayload rest :
    122       or?
    123         (not? (nodePayloadValid? nodePayload))
    124         (self rest))
    125     nodeRecords)
    126 
    127 nodePayloadChildIndices = (nodePayload :
    128   matchList
    129     t
    130     (tag rest :
    131       lazyBool
    132         (_ :
    133           withNodePayloadStemIndex
    134             nodePayload
    135             (_ : t)
    136             (childIndex : pair childIndex t))
    137         (_ :
    138           lazyBool
    139             (_ :
    140               withNodePayloadForkIndices
    141                 nodePayload
    142                 (_ : t)
    143                 (leftIndex rightIndex :
    144                   pair leftIndex (pair rightIndex t)))
    145             (_ : t)
    146             (equal? tag nodePayloadForkTag))
    147         (equal? tag nodePayloadStemTag))
    148     nodePayload)
    149 
    150 -- True iff index n names an element before limit in records.
    151 -- For topologically sorted indexed bundles, every child of record i must
    152 -- satisfy childIndex < i, so searching only the prefix [0, i) validates both
    153 -- bounds and acyclicity.
    154 nodeIndexInPrefix? = y (self records n i limit :
    155   matchList
    156     false
    157     (_ rest :
    158       matchBool
    159         false
    160         (matchBool
    161           true
    162           (self rest n (succ i) limit)
    163           (equal? i n))
    164         (equal? i limit))
    165     records)
    166 
    167 nodeChildIndicesInPrefix? = y (self childIndices records limit :
    168   matchList
    169     true
    170     (childIndex rest :
    171       matchBool
    172         (self rest records limit)
    173         false
    174         (nodeIndexInPrefix? records childIndex 0 limit))
    175     childIndices)
    176 
    177 nodePayloadIndicesValid? = (nodePayload i records :
    178   nodeChildIndicesInPrefix?
    179     (nodePayloadChildIndices nodePayload)
    180     records
    181     i)
    182 
    183 nodeRecordsValidIndicesFrom? = y (self allRecords remainingRecords i :
    184   matchList
    185     true
    186     (nodePayload rest :
    187       matchBool
    188         (self allRecords rest (succ i))
    189         false
    190         (nodePayloadIndicesValid? nodePayload i allRecords))
    191     remainingRecords)
    192 
    193 nodeRecordsValidIndices? = (nodeRecords i :
    194   nodeRecordsValidIndicesFrom? nodeRecords nodeRecords i)
    195 
    196 validateNodeRecords = (nodeRecords rest :
    197   matchBool
    198     (err errInvalidNodePayload rest)
    199     (matchBool
    200       (ok nodeRecords rest)
    201       (err errMissingNode rest)
    202       (nodeRecordsValidIndices? nodeRecords 0))
    203     (nodeRecordsHaveInvalidPayload? nodeRecords))
    204 
    205 readNodeRecords_ = y (self bs nodeCount i acc :
    206   matchBool
    207     (ok (reverse acc) bs)
    208     (bindResult (readNodeRecord bs)
    209       (nodeRecord afterNodeRecord :
    210         self afterNodeRecord nodeCount (succ i) (pair nodeRecord acc)))
    211     (equal? i nodeCount))
    212 
    213 readNodeRecords = (nodeCount bs :
    214   readNodeRecords_ bs nodeCount 0 t)
    215 
    216 readNodesSection = (bs :
    217   bindResult (readBytes 8 bs)
    218     (nodeCount afterNodeCount :
    219       bindResult (readNodeRecords (u64BEBytesToNat nodeCount) afterNodeCount)
    220         (nodeRecords afterNodeRecords :
    221           bindResult (validateNodeRecords nodeRecords afterNodeRecords)
    222             (validNodeRecords afterValidNodeRecords :
    223               ok (pair nodeCount validNodeRecords) afterValidNodeRecords))))
    224 
    225 readNodesSectionComplete = (bs :
    226   bindResult (readNodesSection bs)
    227     (nodesSection afterNodesSection :
    228       matchBool
    229         (ok nodesSection afterNodesSection)
    230         (err errUnexpectedBytes afterNodesSection)
    231         (bytesNil? afterNodesSection)))
    232 
    233 readArboricxNodesSection = (bs :
    234   bindResult (readArboricxContainer bs)
    235     (container afterContainer :
    236       matchPair
    237         (_ directory :
    238           bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer)
    239             (nodesBytes _ :
    240               bindResult (readNodesSectionComplete nodesBytes)
    241                 (nodesSection _ : ok nodesSection afterContainer)))
    242         container))
    243 
    244 nodesSectionCount = (nodesSection :
    245   matchPair
    246     (nodeCount _ : nodeCount)
    247     nodesSection)
    248 
    249 nodesSectionRecords = (nodesSection :
    250   matchPair
    251     (_ nodeRecords : nodeRecords)
    252     nodesSection)
    253 
    254 nodeBuiltTreeIndex = (entry :
    255   matchPair
    256     (index _ : index)
    257     entry)
    258 
    259 nodeBuiltTreeValue = (entry :
    260   matchPair
    261     (_ tree : tree)
    262     entry)
    263 
    264 nodeTreeByIndex_ = (self builtTrees targetIndex :
    265   lazyList
    266     (_ : err errMissingNode t)
    267     (entry rest :
    268       lazyBool
    269         (_ : ok (nodeBuiltTreeValue entry) t)
    270         (_ : self rest targetIndex)
    271         (equal? (nodeBuiltTreeIndex entry) targetIndex))
    272     builtTrees)
    273 
    274 nodeTreeByIndex = (builtTrees targetIndex :
    275   y nodeTreeByIndex_ builtTrees targetIndex)
    276 
    277 nodePayloadToTreeFromBuilt = (builtTrees nodePayload :
    278   matchList
    279     (err errInvalidNodePayload t)
    280     (tag rest :
    281       lazyBool
    282         (_ : ok t t)
    283         (_ :
    284           lazyBool
    285             (_ :
    286               withNodePayloadStemIndex
    287                 nodePayload
    288                 (_ : err errInvalidNodePayload t)
    289                 (childIndex :
    290                   lazyResult
    291                     (code after : err code after)
    292                     (child _ : ok (t child) t)
    293                     (nodeTreeByIndex builtTrees childIndex)))
    294             (_ :
    295               lazyBool
    296                 (_ :
    297                   withNodePayloadForkIndices
    298                     nodePayload
    299                     (_ : err errInvalidNodePayload t)
    300                     (leftIndex rightIndex :
    301                       lazyResult
    302                         (code after : err code after)
    303                         (left _ :
    304                           lazyResult
    305                             (code after : err code after)
    306                             (right _ : ok (pair left right) t)
    307                             (nodeTreeByIndex builtTrees rightIndex))
    308                         (nodeTreeByIndex builtTrees leftIndex)))
    309                 (_ : err errInvalidNodePayload t)
    310                 (equal? tag nodePayloadForkTag))
    311             (equal? tag nodePayloadStemTag))
    312         (equal? tag 0))
    313     nodePayload)
    314 
    315 nodeBuildState = (targetIndex i builtTrees :
    316   pair targetIndex (pair i builtTrees))
    317 
    318 nodeBuildStateTargetIndex = (state :
    319   matchPair
    320     (targetIndex _ : targetIndex)
    321     state)
    322 
    323 nodeBuildStateI = (state :
    324   matchPair
    325     (_ rest :
    326       matchPair
    327         (i _ : i)
    328         rest)
    329     state)
    330 
    331 nodeBuildStateBuiltTrees = (state :
    332   matchPair
    333     (_ rest :
    334       matchPair
    335         (_ builtTrees : builtTrees)
    336         rest)
    337     state)
    338 
    339 nodeIndexToTree_ = (self remainingRecords state :
    340   ((nodeIndex :
    341     ((i :
    342       ((builtTrees :
    343         lazyList
    344           (_ : err errMissingNode t)
    345           (nodePayload rest :
    346             lazyResult
    347               (code after : err code after)
    348               (tree _ :
    349                 lazyBool
    350                   (_ : ok tree t)
    351                   (_ :
    352                     self
    353                       rest
    354                       (nodeBuildState
    355                         nodeIndex
    356                         (succ i)
    357                         (pair (pair i tree) builtTrees)))
    358                   (equal? i nodeIndex))
    359               (nodePayloadToTreeFromBuilt builtTrees nodePayload))
    360           remainingRecords)
    361        (nodeBuildStateBuiltTrees state)))
    362      (nodeBuildStateI state)))
    363    (nodeBuildStateTargetIndex state)))
    364 
    365 nodeIndexToTree = (nodeRecords nodeIndex :
    366   y nodeIndexToTree_ nodeRecords (nodeBuildState nodeIndex 0 t))
    367 
    368 readArboricxTreeFromIndex = (rootIndexBytes bs :
    369   bindResult (readArboricxNodesSection bs)
    370     (nodesSection afterContainer :
    371       bindResult (nodeIndexToTree (nodesSectionRecords nodesSection) (u32BEBytesToNat rootIndexBytes))
    372         (tree _ : ok tree afterContainer)))
    373 
    374 readArboricxExecutableFromIndex = readArboricxTreeFromIndex