tricu

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

common.tri (12510B)

      1 !import "prelude" !Local
      2 !import "binary"  !Local
      3 
      4 
      5 arboricxMagic = [(65) (82) (66) (79) (82) (73) (67) (88)]
      6 arboricxMajorVersion = [(0) (1)]
      7 arboricxMinorVersion = [(0) (0)]
      8 arboricxManifestSectionId = [(0) (0) (0) (1)]
      9 arboricxNodesSectionId = [(0) (0) (0) (2)]
     10 
     11 -- Manifest magic and version constants
     12 arboricxManifestMagic = [(65) (82) (66) (77) (78) (70) (83) (84)]
     13 arboricxManifestMajorVersion = [(0) (1)]
     14 arboricxManifestMinorVersion = [(0) (0)]
     15 
     16 errMissingSection = 4
     17 errUnsupportedVersion = 5
     18 errDuplicateSection = 6
     19 errDuplicateNode = 7
     20 errInvalidNodePayload = 8
     21 errMissingNode = 9
     22 errInvalidManifestMagic = 10
     23 errUnsupportedManifestVersion = 11
     24 errTrailingManifestBytes = 12
     25 errManifestValidationFailed = 13
     26 
     27 nodePayloadLeafTag = 0
     28 nodePayloadStemTag = 1
     29 nodePayloadForkTag = 2
     30 
     31 readArboricxMagic = (bs : expectBytes arboricxMagic bs)
     32 
     33 readArboricxHeader = (bs :
     34   bindResult (readArboricxMagic bs)
     35     (_ afterMagic :
     36       bindResult (readBytes 2 afterMagic)
     37         (majorVersion afterMajor :
     38           bindResult (readBytes 2 afterMajor)
     39             (minorVersion afterMinor :
     40               bindResult (readBytes 4 afterMinor)
     41                 (sectionCount afterSectionCount :
     42                   bindResult (readBytes 8 afterSectionCount)
     43                     (flags afterFlags :
     44                       bindResult (readBytes 8 afterFlags)
     45                         (dirOffset afterDirOffset :
     46                           ok
     47                             (pair majorVersion
     48                               (pair minorVersion
     49                                 (pair sectionCount
     50                                   (pair flags dirOffset))))
     51                             afterDirOffset)))))))
     52 
     53 readSectionRecord = (bs :
     54   bindResult (readBytes 4 bs)
     55     (sectionId afterSectionId :
     56       bindResult (readBytes 2 afterSectionId)
     57         (sectionVersion afterSectionVersion :
     58           bindResult (readBytes 2 afterSectionVersion)
     59             (sectionFlags afterSectionFlags :
     60               bindResult (readBytes 2 afterSectionFlags)
     61                 (compression afterCompression :
     62                   bindResult (readBytes 2 afterCompression)
     63                     (reserved1 afterReserved1 :
     64                       bindResult (readBytes 8 afterReserved1)
     65                         (offset afterOffset :
     66                           bindResult (readBytes 8 afterOffset)
     67                             (length afterLength :
     68                               bindResult (readBytes 4 afterLength)
     69                                 (reserved2 afterReserved2 :
     70                                   ok
     71                                     (pair sectionId
     72                                       (pair sectionVersion
     73                                         (pair sectionFlags
     74                                           (pair compression
     75                                             (pair reserved1
     76                                               (pair offset
     77                                                 (pair length reserved2)))))))
     78                                     afterReserved2)))))))))
     79 
     80 readSectionDirectory_ = y (self bs sectionCount i acc :
     81   matchBool
     82     (ok (reverse acc) bs)
     83     (bindResult (readSectionRecord bs)
     84       (sectionRecord afterSectionRecord :
     85         self afterSectionRecord sectionCount (succ i) (pair sectionRecord acc)))
     86     (equal? i sectionCount))
     87 
     88 readSectionDirectory = (sectionCount bs : readSectionDirectory_ bs sectionCount 0 t)
     89 
     90 sectionRecordId = (sectionRecord :
     91   matchPair
     92     (sectionId _ : sectionId)
     93     sectionRecord)
     94 
     95 sectionRecordVersion = (sectionRecord :
     96   matchPair
     97     (_ payload :
     98       matchPair
     99         (sectionVersion _ : sectionVersion)
    100         payload)
    101     sectionRecord)
    102 
    103 sectionRecordFlags = (sectionRecord :
    104   matchPair
    105     (_ payload :
    106       matchPair
    107         (_ payload2 :
    108           matchPair
    109             (sectionFlags _ : sectionFlags)
    110             payload2)
    111         payload)
    112     sectionRecord)
    113 
    114 sectionRecordCompression = (sectionRecord :
    115   matchPair
    116     (_ payload :
    117       matchPair
    118         (_ payload2 :
    119           matchPair
    120             (_ payload3 :
    121               matchPair
    122                 (compression _ : compression)
    123                 payload3)
    124             payload2)
    125         payload)
    126     sectionRecord)
    127 
    128 sectionRecordReserved1 = (sectionRecord :
    129   matchPair
    130     (_ payload :
    131       matchPair
    132         (_ payload2 :
    133           matchPair
    134             (_ payload3 :
    135               matchPair
    136                 (_ payload4 :
    137                   matchPair
    138                     (reserved1 _ : reserved1)
    139                     payload4)
    140                 payload3)
    141             payload2)
    142         payload)
    143     sectionRecord)
    144 
    145 sectionRecordOffset = (sectionRecord :
    146   matchPair
    147     (_ payload :
    148       matchPair
    149         (_ payload2 :
    150           matchPair
    151             (_ payload3 :
    152               matchPair
    153                 (_ payload4 :
    154                   matchPair
    155                     (_ payload5 :
    156                       matchPair
    157                         (offset _ : offset)
    158                         payload5)
    159                     payload4)
    160                 payload3)
    161             payload2)
    162         payload)
    163     sectionRecord)
    164 
    165 sectionRecordLength = (sectionRecord :
    166   matchPair
    167     (_ payload :
    168       matchPair
    169         (_ payload2 :
    170           matchPair
    171             (_ payload3 :
    172               matchPair
    173                 (_ payload4 :
    174                   matchPair
    175                     (_ payload5 :
    176                       matchPair
    177                         (_ payload6 :
    178                           matchPair
    179                             (length _ : length)
    180                             payload6)
    181                         payload5)
    182                     payload4)
    183                 payload3)
    184             payload2)
    185         payload)
    186     sectionRecord)
    187 
    188 sectionRecordReserved2 = (sectionRecord :
    189   matchPair
    190     (_ payload :
    191       matchPair
    192         (_ payload2 :
    193           matchPair
    194             (_ payload3 :
    195               matchPair
    196                 (_ payload4 :
    197                   matchPair
    198                     (_ payload5 :
    199                       matchPair
    200                         (_ payload6 :
    201                           matchPair
    202                             (_ reserved2 : reserved2)
    203                             payload6)
    204                         payload5)
    205                     payload4)
    206                 payload3)
    207             payload2)
    208         payload)
    209     sectionRecord)
    210 
    211 lookupSectionRecord_ = y (self directory sectionId :
    212   matchList
    213     nothing
    214     (sectionRecord rest :
    215       matchBool
    216         (just sectionRecord)
    217         (self rest sectionId)
    218         (bytesEq? sectionId (sectionRecordId sectionRecord)))
    219     directory)
    220 
    221 lookupSectionRecord = (sectionId directory : lookupSectionRecord_ directory sectionId)
    222 
    223 sectionDirectoryHasId?_ = y (self directory sectionId :
    224   matchList
    225     false
    226     (sectionRecord rest :
    227       or?
    228         (bytesEq? sectionId (sectionRecordId sectionRecord))
    229         (self rest sectionId))
    230     directory)
    231 
    232 sectionDirectoryHasId? = (sectionId directory : sectionDirectoryHasId?_ directory sectionId)
    233 
    234 sectionDirectoryHasDuplicateIds? = y (self directory :
    235   matchList
    236     false
    237     (sectionRecord rest :
    238       or?
    239         (sectionDirectoryHasId?_ rest (sectionRecordId sectionRecord))
    240         (self rest))
    241     directory)
    242 
    243 validateSectionDirectory = (directory rest :
    244   matchBool
    245     (err errDuplicateSection rest)
    246     (ok directory rest)
    247     (sectionDirectoryHasDuplicateIds? directory))
    248 
    249 byteSlice = (offset length bytes : bytesTake length (bytesDrop offset bytes))
    250 
    251 natMake = (bit rest :
    252   matchBool
    253     0
    254     (pair bit rest)
    255     (and? (equal? bit 0) (equal? rest 0)))
    256 
    257 natAdd = y (self a b :
    258   triage
    259     b
    260     (_ : b)
    261     (aBit aRest :
    262       triage
    263         a
    264         (_ : a)
    265         (bBit bRest :
    266           matchBool
    267             (natMake 0 (succ (self aRest bRest)))
    268             (natMake (matchBool (matchBool 0 1 bBit) (matchBool 1 0 bBit) aBit)
    269               (self aRest bRest))
    270             (and? (equal? aBit 1) (equal? bBit 1)))
    271         b)
    272     a)
    273 
    274 natDouble = (n : matchBool 0 (pair 0 n) (equal? n 0))
    275 
    276 natTimes256 = (n :
    277   natDouble
    278     (natDouble
    279       (natDouble
    280         (natDouble
    281           (natDouble
    282             (natDouble
    283               (natDouble
    284                 (natDouble n))))))))
    285 
    286 byteNatShiftAppend_ = y (self byte acc i :
    287   matchBool
    288     acc
    289     (triage
    290       (natMake 0 (self 0 acc (succ i)))
    291       (_ : acc)
    292       (bit rest : natMake bit (self rest acc (succ i)))
    293       byte)
    294     (equal? i 8))
    295 
    296 byteNatShiftAppend = (byte acc : byteNatShiftAppend_ byte acc 0)
    297 
    298 beBytesToNat = (bytes :
    299   foldl
    300     (acc byte : byteNatShiftAppend byte acc)
    301     0
    302     bytes)
    303 
    304 u32BEBytesToNat = beBytesToNat
    305 u64BEBytesToNat = beBytesToNat
    306 
    307 arboricxHeaderMajorVersion = (header :
    308   matchPair
    309     (majorVersion _ : majorVersion)
    310     header)
    311 
    312 arboricxHeaderMinorVersion = (header :
    313   matchPair
    314     (_ payload :
    315       matchPair
    316         (minorVersion _ : minorVersion)
    317         payload)
    318     header)
    319 
    320 arboricxHeaderSectionCount = (header :
    321   matchPair
    322     (_ payload :
    323       matchPair
    324         (_ payload2 :
    325           matchPair
    326             (sectionCount _ : sectionCount)
    327             payload2)
    328         payload)
    329     header)
    330 
    331 arboricxHeaderFlags = (header :
    332   matchPair
    333     (_ payload :
    334       matchPair
    335         (_ payload2 :
    336           matchPair
    337             (_ payload3 :
    338               matchPair
    339                 (flags _ : flags)
    340                 payload3)
    341             payload2)
    342         payload)
    343     header)
    344 
    345 arboricxHeaderDirOffset = (header :
    346   matchPair
    347     (_ payload :
    348       matchPair
    349         (_ payload2 :
    350           matchPair
    351             (_ payload3 :
    352               matchPair
    353                 (_ dirOffset : dirOffset)
    354                 payload3)
    355             payload2)
    356         payload)
    357     header)
    358 
    359 validateArboricxHeader = (header rest :
    360   matchBool
    361     (ok header rest)
    362     (err errUnsupportedVersion rest)
    363     (and?
    364       (bytesEq? arboricxMajorVersion (arboricxHeaderMajorVersion header))
    365       (bytesEq? arboricxMinorVersion (arboricxHeaderMinorVersion header))))
    366 
    367 readArboricxContainer = (bs :
    368   bindResult (readArboricxHeader bs)
    369     (header afterHeader :
    370       bindResult (validateArboricxHeader header afterHeader)
    371         (validHeader afterValidHeader :
    372           bindResult (readSectionDirectory
    373             (u32BEBytesToNat (arboricxHeaderSectionCount validHeader))
    374             (bytesDrop (u64BEBytesToNat (arboricxHeaderDirOffset validHeader)) bs))
    375             (directory afterDirectory :
    376               bindResult (validateSectionDirectory directory afterDirectory)
    377                 (validDirectory afterValidDirectory :
    378                   ok (pair validHeader validDirectory) afterValidDirectory)))))
    379 
    380 sectionRecordOffsetNat = (sectionRecord :
    381   u64BEBytesToNat (sectionRecordOffset sectionRecord))
    382 
    383 sectionRecordLengthNat = (sectionRecord :
    384   u64BEBytesToNat (sectionRecordLength sectionRecord))
    385 
    386 extractSectionBytes = (sectionRecord containerBytes :
    387   byteSlice
    388     (sectionRecordOffsetNat sectionRecord)
    389     (sectionRecordLengthNat sectionRecord)
    390     containerBytes)
    391 
    392 extractSectionBytesResult = (sectionRecord containerBytes rest :
    393   (sectionBytes :
    394     matchBool
    395       (ok sectionBytes rest)
    396       (err errUnexpectedEof rest)
    397       (equal? (bytesLength sectionBytes) (sectionRecordLengthNat sectionRecord)))
    398     (extractSectionBytes sectionRecord containerBytes))
    399 
    400 lookupSectionBytes = (sectionId directory containerBytes :
    401   triage
    402     nothing
    403     (sectionRecord : just (extractSectionBytes sectionRecord containerBytes))
    404     (_ _ : nothing)
    405     (lookupSectionRecord sectionId directory))
    406 
    407 sectionBytesOrErr = (sectionId directory containerBytes rest :
    408   triage
    409     (err errMissingSection rest)
    410     (sectionRecord : extractSectionBytesResult sectionRecord containerBytes rest)
    411     (_ _ : err errMissingSection rest)
    412     (lookupSectionRecord sectionId directory))
    413 
    414 readArboricxSectionBytes = (sectionId bs :
    415   bindResult (readArboricxContainer bs)
    416     (container afterContainer :
    417       matchPair
    418         (_ directory : sectionBytesOrErr sectionId directory bs afterContainer)
    419         container))
    420 
    421 readArboricxRequiredSections = (bs :
    422   bindResult (readArboricxContainer bs)
    423     (container afterContainer :
    424       matchPair
    425         (_ directory :
    426           bindResult (sectionBytesOrErr arboricxManifestSectionId directory bs afterContainer)
    427             (manifestBytes _ :
    428               bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer)
    429                 (nodesBytes _ :
    430                   ok (pair manifestBytes nodesBytes) afterContainer)))
    431         container))