tricu

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

932049708c30961bba6c8820fec50edb08bb58e60ba2e811476436972b104e50.tri (15173B)

      1 !import prelude *
      2 !import binary *
      3 !import arboricx_common *
      4 !import arboricx_nodes *
      5 !export *
      6 
      7 readManifestMagic = (bs :
      8   expectBytes arboricxManifestMagic bs)
      9 
     10 -- Read a u32 BE length, then that many raw bytes.
     11 -- Returns the payload bytes and remaining input.
     12 readLengthPrefixedString = (bs :
     13   bindResult (readBytes 4 bs)
     14     (lengthBytes afterLengthBytes :
     15       bindResult (readBytes (u32BEBytesToNat lengthBytes) afterLengthBytes)
     16         (payload afterPayload :
     17           ok payload afterPayload)))
     18 
     19 -- Helper: read a single capability string (length-prefixed string)
     20 readCapability = (bs :
     21   readLengthPrefixedString bs)
     22 
     23 -- Helper worker: read N capability strings (counts up from 0)
     24 readCapabilities_ = y (self bs count i acc :
     25   matchBool
     26     (ok (reverse acc) bs)
     27     (bindResult (readCapability bs)
     28       (cap afterCap :
     29         self afterCap count (succ i) (pair cap acc)))
     30     (equal? i count))
     31 
     32 -- Helper: read N capabilities
     33 readCapabilities = (count bs :
     34   readCapabilities_ bs count 0 t)
     35 
     36 -- Helper: read a single root entry (4-byte u32 BE index + length-prefixed role)
     37 readRootEntry = (bs :
     38   bindResult (readBytes 4 bs)
     39     (indexRaw afterIndex :
     40       bindResult (readLengthPrefixedString afterIndex)
     41         (role afterRole :
     42           ok (pair indexRaw role) afterRole)))
     43 
     44 -- Helper worker: read N root entries (counts up from 0)
     45 readRoots_ = y (self bs count i acc :
     46   matchBool
     47     (ok (reverse acc) bs)
     48     (bindResult (readRootEntry bs)
     49       (root afterRoot :
     50         self afterRoot count (succ i) (pair root acc)))
     51     (equal? i count))
     52 
     53 -- Helper: read N roots
     54 readRoots = (count bs :
     55   readRoots_ bs count 0 t)
     56 
     57 -- Helper: read a single export entry
     58 readExportEntry = (bs :
     59   bindResult (readLengthPrefixedString bs)
     60     (name afterName :
     61       bindResult (readBytes 4 afterName)
     62         (rootIndexRaw afterRootIndex :
     63           bindResult (readLengthPrefixedString afterRootIndex)
     64             (kind afterKind :
     65               bindResult (readLengthPrefixedString afterKind)
     66                 (abi afterAbi :
     67                   ok (pair name (pair rootIndexRaw (pair kind abi))) afterAbi)))))
     68 
     69 -- Helper worker: read N export entries (counts up from 0)
     70 readExports_ = y (self bs count i acc :
     71   matchBool
     72     (ok (reverse acc) bs)
     73     (bindResult (readExportEntry bs)
     74       (exp afterExp :
     75         self afterExp count (succ i) (pair exp acc)))
     76     (equal? i count))
     77 
     78 -- Helper: read N exports
     79 readExports = (count bs :
     80   readExports_ bs count 0 t)
     81 
     82 -- Main core manifest parser.
     83 -- Reads: magic, version, core strings, capabilities, closure, roots, exports.
     84 readManifestCore = (bs :
     85   bindResult (readManifestMagic bs)
     86     (_ afterMagic :
     87       bindResult (readBytes 2 afterMagic)
     88         (majorVersion afterMajor :
     89           bindResult (readBytes 2 afterMajor)
     90             (minorVersion afterMinor :
     91               bindResult (readLengthPrefixedString afterMinor)
     92                 (schema afterSchema :
     93                   bindResult (readLengthPrefixedString afterSchema)
     94                     (bundleType afterBundleType :
     95                       bindResult (readLengthPrefixedString afterBundleType)
     96                         (treeCalculus afterTreeCalculus :
     97                           bindResult (readLengthPrefixedString afterTreeCalculus)
     98                             (treeHashAlgorithm afterTreeHashAlgorithm :
     99                               bindResult (readLengthPrefixedString afterTreeHashAlgorithm)
    100                                 (treeHashDomain afterTreeHashDomain :
    101                                   bindResult (readLengthPrefixedString afterTreeHashDomain)
    102                                     (treeNodePayload afterTreeNodePayload :
    103                                       bindResult (readLengthPrefixedString afterTreeNodePayload)
    104                                         (runtimeSemantics afterRuntimeSemantics :
    105                                           bindResult (readLengthPrefixedString afterRuntimeSemantics)
    106                                             (runtimeEvaluation afterRuntimeEvaluation :
    107                                               bindResult (readLengthPrefixedString afterRuntimeEvaluation)
    108                                                 (runtimeAbi afterRuntimeAbi :
    109                                                   bindResult (readBytes 4 afterRuntimeAbi)
    110                                                     (capCountRaw afterCapCountRaw :
    111                                                       bindResult (readCapabilities (u32BEBytesToNat capCountRaw) afterCapCountRaw)
    112                                                         (capabilities afterCapabilities :
    113                                                           bindResult (readBytes 1 afterCapabilities)
    114                                                             (closureByte afterClosureByte :
    115                                                               bindResult (readBytes 4 afterClosureByte)
    116                                                                 (rootCountRaw afterRootCountRaw :
    117                                                                   bindResult (readRoots (u32BEBytesToNat rootCountRaw) afterRootCountRaw)
    118                                                                     (roots afterRoots :
    119                                                                       bindResult (readBytes 4 afterRoots)
    120                                                                         (exportCountRaw afterExportCountRaw :
    121                                                                           bindResult (readExports (u32BEBytesToNat exportCountRaw) afterExportCountRaw)
    122                                                                             (exports afterExports :
    123                                                                               ok
    124                                                                                 (pair schema
    125                                                                                   (pair bundleType
    126                                                                                     (pair treeCalculus
    127                                                                                       (pair treeHashAlgorithm
    128                                                                                         (pair treeHashDomain
    129                                                                                           (pair treeNodePayload
    130                                                                                             (pair runtimeSemantics
    131                                                                                               (pair runtimeEvaluation
    132                                                                                                 (pair runtimeAbi
    133                                                                                                   (pair capabilities
    134                                                                     (pair closureByte (pair roots exports)))))))))))) afterExports))))))))))))))))))))
    135 
    136 -- Metadata tag constants (u16 values)
    137 tagPackage    = [(0) (1)]
    138 tagVersion    = [(0) (2)]
    139 tagDescription = [(0) (3)]
    140 tagLicense    = [(0) (4)]
    141 tagCreatedBy  = [(0) (5)]
    142 
    143 -- Read a single TLV entry: u16 tag + u32 length + value bytes.
    144 -- Returns the pair (tag, value) and remaining input.
    145 readTLV = (bs :
    146   bindResult (readBytes 2 bs)
    147     (tag afterTag :
    148       bindResult (readBytes 4 afterTag)
    149         (tlvLenRaw afterTlvLenRaw :
    150           bindResult (readBytes (u32BEBytesToNat tlvLenRaw) afterTlvLenRaw)
    151             (tlvValue afterTlvValue :
    152               ok (pair tag tlvValue) afterTlvValue))))
    153 
    154 -- Worker: read N TLV entries (counts up from 0)
    155 readTLVs_ = y (self bs count i acc :
    156   matchBool
    157     (ok (reverse acc) bs)
    158     (bindResult (readTLV bs)
    159       (tlv afterTlv :
    160         self afterTlv count (succ i) (pair tlv acc)))
    161     (equal? i count))
    162 
    163 -- Read a count followed by that many TLV entries.
    164 readTLVList = (count bs :
    165   readTLVs_ bs count 0 t)
    166 
    167 -- Skip N extension TLV entries (counts up from 0)
    168 skipTLVs_ = y (self bs count i :
    169   matchBool
    170     (ok unit bs)
    171     (bindResult (readTLV bs)
    172       (_ afterTlv :
    173         self afterTlv count (succ i)))
    174     (equal? i count))
    175 
    176 -- Full manifest parser: core fields + metadata TLV list + extension TLV list.
    177 readManifest = (bs :
    178   bindResult (readManifestCore bs)
    179     (coreManifest afterCore :
    180       bindResult (readBytes 4 afterCore)
    181         (metaCountRaw afterMetaCountRaw :
    182           bindResult (readTLVList (u32BEBytesToNat metaCountRaw) afterMetaCountRaw)
    183             (metadataFields afterMetadataFields :
    184               bindResult (readBytes 4 afterMetadataFields)
    185                 (extCountRaw afterExtCountRaw :
    186                   bindResult (skipTLVs_ afterExtCountRaw (u32BEBytesToNat extCountRaw) 0)
    187                     (afterExtensions _ :
    188                       ok
    189                         (pair coreManifest (pair metadataFields afterExtensions))
    190                         afterExtensions))))))
    191 
    192 -- Lookup a metadata value by tag from a TLV list.
    193 -- Returns nothing if not found, just value if found.
    194 lookupMetadata_ = y (self tlvs tag :
    195   matchList
    196     nothing
    197     (tlv rest :
    198       matchBool
    199         (just (matchPair (_ value : value) tlv))
    200         (self rest tag)
    201         (bytesEq? (matchPair (tlvTag _ : tlvTag) tlv) tag))
    202     tlvs)
    203 
    204 lookupMetadata = (tlvs tag :
    205   lookupMetadata_ tlvs tag)
    206 
    207 -- Get export name from an export entry (pair name (pair rootIndex (pair kind abi)))
    208 exportName = (exp :
    209   matchPair
    210     (name _ : name)
    211     exp)
    212 
    213 exportRoot = (exp :
    214   matchPair
    215     (_ payload :
    216       matchPair
    217         (root _ : root)
    218         payload)
    219     exp)
    220 
    221 -- Check if an export name matches a given byte string.
    222 exportNameEq? = (nameBytes exp :
    223   bytesEq? nameBytes (exportName exp))
    224 
    225 -- Find first export matching a name, or nothing.
    226 findExportByName_ = y (self exports name :
    227   matchList
    228     nothing
    229     (exp rest :
    230       matchBool
    231         (just exp)
    232         (self rest name)
    233         (exportNameEq? name exp))
    234     exports)
    235 
    236 findExportByName = (exports name :
    237   findExportByName_ exports name)
    238 
    239 -- Get list of all export names from a list of exports.
    240 getExportNames_ = y (self acc exports :
    241   matchList
    242     (reverse acc)
    243     (exp rest :
    244       self (pair (exportName exp) acc) rest)
    245     exports)
    246 
    247 getExportNames = (exports :
    248   getExportNames_ t exports)
    249 
    250 mainExportName = "main"
    251 
    252 maybeExportToResult = (maybeExport :
    253   triage
    254     (err errMissingSection t)
    255     (export : ok export t)
    256     (_ _ : err errMissingSection t)
    257     maybeExport)
    258 
    259 selectSingleExport = (exports :
    260   matchList
    261     (err errMissingSection t)
    262     (export rest :
    263       matchBool
    264         (ok export t)
    265         (err errMissingSection t)
    266         (emptyList? rest))
    267     exports)
    268 
    269 selectDefaultExport = (exports :
    270   triage
    271     (selectSingleExport exports)
    272     (export : ok export t)
    273     (_ _ : err errMissingSection t)
    274     (findExportByName exports mainExportName))
    275 
    276 -- Select an export: explicit name if provided, otherwise "main", otherwise
    277 -- the sole export if the bundle has exactly one export.
    278 selectExport = (exports nameBytes :
    279   matchBool
    280     (selectDefaultExport exports)
    281     (maybeExportToResult (findExportByName exports nameBytes))
    282     (emptyList? nameBytes))
    283 
    284 selectExportOpt = (exports optNameBytes :
    285   selectExport exports optNameBytes)
    286 
    287 -- Expected core string values (raw UTF-8 bytes, not decoded to Unicode characters).
    288 expectedSchema = "arboricx.bundle.manifest.v1"
    289 expectedBundleType = "tree-calculus-executable-object"
    290 expectedTreeCalculus = "tree-calculus.v1"
    291 expectedTreeHashAlgorithm = "indexed"
    292 expectedTreeHashDomain = "arboricx.indexed.node.v1"
    293 expectedTreeNodePayload = "arboricx.indexed.payload.v1"
    294 expectedRuntimeSemantics = "tree-calculus.v1"
    295 expectedRuntimeEvaluation = "normal-order"
    296 expectedRuntimeAbi = "arboricx.abi.tree.v1"
    297 
    298 -- Manifest core field accessors.
    299 -- readManifestCore returns: (pair schema (pair bundleType (... (pair closureByte (pair roots exports)))))
    300 pairFirst = (p : matchPair (a _ : a) p)
    301 pairSecond = (p : matchPair (_ b : b) p)
    302 
    303 manifestSchema = (core : pairFirst core)
    304 manifestBundleType = (core : pairFirst (pairSecond core))
    305 manifestTreeCalculus = (core : pairFirst (pairSecond (pairSecond core)))
    306 manifestTreeHashAlgorithm = (core : pairFirst (pairSecond (pairSecond (pairSecond core))))
    307 manifestTreeHashDomain = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond core)))))
    308 manifestTreeNodePayload = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))
    309 manifestRuntimeSemantics = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))
    310 manifestRuntimeEvaluation = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))
    311 manifestRuntimeAbi = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))
    312 manifestCapabilities = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))))
    313 manifestClosureByte = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))))
    314 manifestRoots = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))))))
    315 manifestExports = (core : pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))))))
    316 
    317 -- Helper: compare a manifest field against an expected byte string.
    318 manifestFieldMatch? = (actual expected : bytesEq? actual expected)
    319 
    320 -- Validate core manifest fields against expected values.
    321 validateManifestCore = (core rest :
    322   matchBool
    323     (ok core rest)
    324     (err errManifestValidationFailed rest)
    325     (and?
    326       (manifestFieldMatch? (manifestSchema core) expectedSchema)
    327       (and?
    328         (manifestFieldMatch? (manifestBundleType core) expectedBundleType)
    329         (and?
    330           (manifestFieldMatch? (manifestTreeCalculus core) expectedTreeCalculus)
    331           (and?
    332             (manifestFieldMatch? (manifestTreeHashAlgorithm core) expectedTreeHashAlgorithm)
    333             (and?
    334               (manifestFieldMatch? (manifestTreeHashDomain core) expectedTreeHashDomain)
    335               (and?
    336                 (manifestFieldMatch? (manifestTreeNodePayload core) expectedTreeNodePayload)
    337                 (and?
    338                   (manifestFieldMatch? (manifestRuntimeSemantics core) expectedRuntimeSemantics)
    339                   (and?
    340                     (manifestFieldMatch? (manifestRuntimeEvaluation core) expectedRuntimeEvaluation)
    341                     (and?
    342                       (manifestFieldMatch? (manifestRuntimeAbi core) expectedRuntimeAbi)
    343                       (and?
    344                         (bytesEq? (manifestClosureByte core) [(0)])
    345                         (and?
    346                           (not? (emptyList? (manifestRoots core)))
    347                           (not? (emptyList? (manifestExports core)))))))))))))))