tricu

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

e57eb8ac508bd8fc249eca91d496c58132fcbfe8607385dc743161a1a481d06d.tri (10830B)

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