tricu

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

86fe4cfaf4adb3f897d87265ff2ee6c6b21eabea1fb0724b161164c6c026aa66.tri (11441B)


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