tricu

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

880ca4eefe955ed2ac38ca0a6ce8f04e41e44aeaf32c82b1bd4d8fb7342d9dba.tri (10024B)

      1 !import prelude *
      2 !import binary *
      3 !import arboricx_common *
      4 !export *
      5 
      6 readManifestMagic bytes = (matchResult
      7   (code rest : err (lazyBool (_ : errInvalidManifestMagic) (_ : code) (equal? code errUnexpectedBytes)) rest)
      8   ok
      9   (expectBytes arboricxManifestMagic bytes))
     10 
     11 -- Read a u32 BE length, then that many raw bytes.
     12 -- Returns the payload bytes and remaining input.
     13 readLengthPrefixedString = (do bindParser
     14   lengthBytes <- readBytes 4
     15   payload <- readBytes (u32BEBytesToNat lengthBytes)
     16   pureParser payload)
     17 
     18 readUtf8String bytes = (bindResult (readLengthPrefixedString bytes)
     19   (text rest : lazyBool (_ : ok text rest) (_ : err errManifestValidationFailed rest) (binaryUtf8? text)))
     20 
     21 -- Helper: read a single capability string (length-prefixed string)
     22 readCapability = (bs :
     23   readUtf8String bs)
     24 
     25 -- Counted capability strings.
     26 readCapabilities count = repeatParser count readCapability
     27 
     28 -- Helper: read a single root entry (4-byte u32 BE index + length-prefixed role)
     29 readRootEntry = (do bindParser
     30   indexRaw <- readBytes 4
     31   role <- readUtf8String
     32   pureParser (pair indexRaw role))
     33 
     34 -- Counted root entries.
     35 readRoots count = repeatParser count readRootEntry
     36 
     37 -- Helper: read a single export entry
     38 readExportEntry = (do bindParser
     39   name <- readUtf8String
     40   rootIndexRaw <- readBytes 4
     41   kind <- readUtf8String
     42   abi <- readUtf8String
     43   pureParser (pair name (pair rootIndexRaw (pair kind abi))))
     44 
     45 -- Counted export entries.
     46 readExports count = repeatParser count readExportEntry
     47 
     48 validateManifestVersion major minor bytes = (lazyBool
     49   (_ : ok unit bytes)
     50   (_ : err errUnsupportedManifestVersion bytes)
     51   (and? (equal? major arboricxManifestMajorVersion) (equal? minor arboricxManifestMinorVersion)))
     52 
     53 -- Main core manifest parser.
     54 -- Reads: magic, version, core strings, capabilities, closure, roots, exports.
     55 readManifestCore = (do bindParser
     56   readManifestMagic
     57   major <- readBytes 2
     58   minor <- readBytes 2
     59   validateManifestVersion major minor
     60   schema <- readUtf8String
     61   bundleType <- readUtf8String
     62   treeCalculus <- readUtf8String
     63   treeHashAlgorithm <- readUtf8String
     64   treeHashDomain <- readUtf8String
     65   treeNodePayload <- readUtf8String
     66   runtimeSemantics <- readUtf8String
     67   runtimeEvaluation <- readUtf8String
     68   runtimeAbi <- readUtf8String
     69   capCountRaw <- readBytes 4
     70   capabilities <- readCapabilities (u32BEBytesToNat capCountRaw)
     71   closureByte <- readBytes 1
     72   rootCountRaw <- readBytes 4
     73   roots <- readRoots (u32BEBytesToNat rootCountRaw)
     74   exportCountRaw <- readBytes 4
     75   exports <- readExports (u32BEBytesToNat exportCountRaw)
     76   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)))))))))))))
     77 
     78 -- Metadata tag constants (u16 values)
     79 tagPackage    = [(0) (1)]
     80 tagVersion    = [(0) (2)]
     81 tagDescription = [(0) (3)]
     82 tagLicense    = [(0) (4)]
     83 tagCreatedBy  = [(0) (5)]
     84 
     85 -- Read a single TLV entry: u16 tag + u32 length + value bytes.
     86 -- Returns the pair (tag, value) and remaining input.
     87 readTLV = (do bindParser
     88   tag <- readBytes 2
     89   tlvLenRaw <- readBytes 4
     90   tlvValue <- readBytes (u32BEBytesToNat tlvLenRaw)
     91   pureParser (pair tag tlvValue))
     92 
     93 -- Counted TLV entries.
     94 readTLVList count = repeatParser count readTLV
     95 
     96 -- Prefix parser: retain both opaque TLV lists and the actual remaining suffix.
     97 readManifest = (do bindParser
     98   core <- readManifestCore
     99   metaCount <- readBytes 4
    100   metadata <- readTLVList (u32BEBytesToNat metaCount)
    101   extCount <- readBytes 4
    102   extensions <- readTLVList (u32BEBytesToNat extCount)
    103   pureParser (pair core (pair metadata extensions)))
    104 
    105 readManifestComplete bytes = (bindResult (readManifest bytes)
    106   (value rest : case rest of
    107     [] = ok value rest
    108     _ = err errTrailingManifestBytes rest))
    109 
    110 -- Lookup a metadata value by tag from a TLV list.
    111 -- Returns nothing if not found, just value if found.
    112 lookupMetadata tlvs tag = (maybeMap snd (find (entry : equal? (fst entry) tag) tlvs))
    113 exportName entry = fst entry
    114 exportRoot entry = fst (snd entry)
    115 exportNameEq? name entry = equal? name (exportName entry)
    116 findExportByName exports name = find (exportNameEq? name) exports
    117 getExportNames exports = map exportName exports
    118 
    119 mainExportName = "main"
    120 
    121 maybeExportToResult = (maybeExport :
    122   triage
    123     (err errMissingSection t)
    124     (export : ok export t)
    125     (_ _ : err errMissingSection t)
    126     maybeExport)
    127 
    128 selectSingleExport = (exports :
    129   matchList
    130     (err errMissingSection t)
    131     (export rest :
    132       matchBool
    133         (ok export t)
    134         (err errMissingSection t)
    135         (emptyList? rest))
    136     exports)
    137 
    138 selectDefaultExport = (exports :
    139   triage
    140     (selectSingleExport exports)
    141     (export : ok export t)
    142     (_ _ : err errMissingSection t)
    143     (findExportByName exports mainExportName))
    144 
    145 -- Select an export: explicit name if provided, otherwise "main", otherwise
    146 -- the sole export if the bundle has exactly one export.
    147 selectExport = (exports nameBytes :
    148   matchBool
    149     (selectDefaultExport exports)
    150     (maybeExportToResult (findExportByName exports nameBytes))
    151     (emptyList? nameBytes))
    152 
    153 -- Expected core string values (raw UTF-8 bytes, not decoded to Unicode characters).
    154 expectedSchema = "arboricx.bundle.manifest.v1"
    155 expectedBundleType = "tree-calculus-executable-object"
    156 expectedTreeCalculus = "tree-calculus.v1"
    157 expectedTreeHashAlgorithm = "indexed"
    158 expectedTreeHashDomain = "arboricx.indexed.node.v1"
    159 expectedTreeNodePayload = "arboricx.indexed.payload.v1"
    160 expectedRuntimeSemantics = "tree-calculus.v1"
    161 expectedRuntimeEvaluation = "normal-order"
    162 expectedRuntimeAbi = "arboricx.abi.tree.v1"
    163 
    164 -- Manifest core field accessors.
    165 -- readManifestCore returns: (pair schema (pair bundleType (... (pair closureByte (pair roots exports)))))
    166 manifestSchema record = case record of
    167   (value, _) = value
    168   _ = t
    169 
    170 manifestBundleType record = case record of
    171   (_, (value, _)) = value
    172   _ = t
    173 
    174 manifestTreeCalculus record = case record of
    175   (_, (_, (value, _))) = value
    176   _ = t
    177 
    178 manifestTreeHashAlgorithm record = case record of
    179   (_, (_, (_, (value, _)))) = value
    180   _ = t
    181 
    182 manifestTreeHashDomain record = case record of
    183   (_, (_, (_, (_, (value, _))))) = value
    184   _ = t
    185 
    186 manifestTreeNodePayload record = case record of
    187   (_, (_, (_, (_, (_, (value, _)))))) = value
    188   _ = t
    189 
    190 manifestRuntimeSemantics record = case record of
    191   (_, (_, (_, (_, (_, (_, (value, _))))))) = value
    192   _ = t
    193 
    194 manifestRuntimeEvaluation record = case record of
    195   (_, (_, (_, (_, (_, (_, (_, (value, _)))))))) = value
    196   _ = t
    197 
    198 manifestRuntimeAbi record = case record of
    199   (_, (_, (_, (_, (_, (_, (_, (_, (value, _))))))))) = value
    200   _ = t
    201 
    202 manifestCapabilities record = case record of
    203   (_, (_, (_, (_, (_, (_, (_, (_, (_, (value, _)))))))))) = value
    204   _ = t
    205 
    206 manifestClosureByte record = case record of
    207   (_, (_, (_, (_, (_, (_, (_, (_, (_, (_, (value, _))))))))))) = value
    208   _ = t
    209 
    210 manifestRoots record = case record of
    211   (_, (_, (_, (_, (_, (_, (_, (_, (_, (_, (_, (value, _)))))))))))) = value
    212   _ = t
    213 
    214 manifestExports record = case record of
    215   (_, (_, (_, (_, (_, (_, (_, (_, (_, (_, (_, (_, value)))))))))))) = value
    216   _ = t
    217 
    218 -- Helper: compare a manifest field against an expected byte string.
    219 manifestFieldMatch? = (actual expected : bytesEq? actual expected)
    220 
    221 -- Validate core manifest fields against expected values.
    222 validateManifestCore = (core rest :
    223   matchBool
    224     (ok core rest)
    225     (err errManifestValidationFailed rest)
    226     (and?
    227       (manifestFieldMatch? (manifestSchema core) expectedSchema)
    228       (and?
    229         (manifestFieldMatch? (manifestBundleType core) expectedBundleType)
    230         (and?
    231           (manifestFieldMatch? (manifestTreeCalculus core) expectedTreeCalculus)
    232           (and?
    233             (manifestFieldMatch? (manifestTreeHashAlgorithm core) expectedTreeHashAlgorithm)
    234             (and?
    235               (manifestFieldMatch? (manifestTreeHashDomain core) expectedTreeHashDomain)
    236               (and?
    237                 (manifestFieldMatch? (manifestTreeNodePayload core) expectedTreeNodePayload)
    238                 (and?
    239                   (manifestFieldMatch? (manifestRuntimeSemantics core) expectedRuntimeSemantics)
    240                   (and?
    241                     (manifestFieldMatch? (manifestRuntimeEvaluation core) expectedRuntimeEvaluation)
    242                     (and?
    243                       (manifestFieldMatch? (manifestRuntimeAbi core) expectedRuntimeAbi)
    244                       (and?
    245                         (bytesEq? (manifestClosureByte core) [(0)])
    246                         (and?
    247                           (not? (emptyList? (manifestRoots core)))
    248                           (and? (not? (emptyList? (manifestExports core)))
    249                             (and? (equal? (manifestCapabilities core) [])
    250                               (and? (manifestRootsValid? (manifestRoots core)) (manifestExportsValid? (manifestExports core)))))))))))))))))
    251 
    252 
    253 -- Export names are UTF-8 byte strings, never filesystem paths.
    254 -- Validate every export before selection; never silently replace kind or ABI.
    255 manifestExportsValid? exports = case exports of
    256   [] = true
    257   [(name, (root, (kind, abi))) | rest] = (and? (not? (equal? name []))
    258     (and? (binaryBytes? name)
    259       (and? (and? (binaryBytes? root) (equal? (length root) 4))
    260         (and? (equal? kind "term")
    261           (and? (equal? abi expectedRuntimeAbi)
    262             (and? (not? (any? (exportNameEq? name) rest)) (manifestExportsValid? rest)))))))
    263   _ = false
    264 
    265 manifestRootsValid? roots = case roots of
    266   [] = true
    267   [(index, role) | rest] = (and? (binaryBytes? index)
    268     (and? (equal? (length index) 4) (and? (binaryBytes? role) (manifestRootsValid? rest))))
    269   _ = false
    270 
    271 
    272 -- Unknown metadata and extensions remain opaque. Known metadata tags are text.
    273 validateManifestMetadata fields rest = (lazyBool
    274   (_ : ok fields rest)
    275   (_ : err errManifestValidationFailed rest)
    276   (all? (entry : let tag = beBytesToNat (fst entry) in
    277     or? (not? (and? (gte_? tag 1) (lte_? tag 5))) (binaryUtf8? (snd entry))) fields))