tricu

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

arboricx.tri (5222B)

      1 !import prelude *
      2 !import binary as Binary
      3 !import native_math as N
      4 !import arboricx_common *
      5 !import arboricx_manifest *
      6 !import arboricx_nodes *
      7 !export *
      8 
      9 -- Parse each section once, validate the complete graph and every advertised
     10 -- root/export, then select. An invalid unselected export is still invalid.
     11 readArboricxDecoded bytes = (bindResult (readArboricxRequiredSections bytes)
     12   (sections rest : bindResult (readManifestComplete (fst sections))
     13     (manifest _ : bindResult (validateManifestCore (fst manifest) t)
     14       (core _ : bindResult (validateManifestMetadata (fst (snd manifest)) t)
     15         (_ _ : bindResult (readNodesSectionComplete (snd sections))
     16           (nodes _ : let
     17             count = u64BEBytesToNat (nodesSectionCount nodes)
     18             rootValid entry = N.lt (u32BEBytesToNat (fst entry)) count
     19             exportValid entry = N.lt (u32BEBytesToNat (exportRoot entry)) count
     20             in lazyBool
     21               (_ : ok (pair manifest nodes) rest)
     22               (_ : err errMissingNode rest)
     23               (and? (all? rootValid (manifestRoots core)) (all? exportValid (manifestExports core)))))))))
     24 
     25 readArboricxBundle bytes = bindResult (readArboricxDecoded bytes) (decoded rest : ok (fst decoded) rest)
     26 readArboricxExecutableByName name bytes = (bindResult (readArboricxDecoded bytes)
     27   (decoded rest : bindResult (selectExport (manifestExports (fst (fst decoded))) name)
     28     (selected _ : bindResult (nodeIndexToTree (nodesSectionRecords (snd decoded)) (u32BEBytesToNat (exportRoot selected)))
     29       (tree _ : ok tree rest))))
     30 
     31 readArboricxExecutable = (bs :
     32   readArboricxExecutableByName [] bs)
     33 
     34 applyArgs = (f args :
     35   foldl
     36     (acc arg : acc arg)
     37     f
     38     args)
     39 
     40 runArboricxByName = (nameBytes bs arg :
     41   bindResult (readArboricxExecutableByName nameBytes bs)
     42     (executable rest : ok (executable arg) rest))
     43 
     44 runArboricx = (bs arg :
     45   runArboricxByName [] bs arg)
     46 
     47 runArboricxArgsByName nameBytes bytes args = (lazyBool
     48   (_ : bindResult (readArboricxExecutableByName nameBytes bytes)
     49     (executable rest : ok (applyArgs executable args) rest))
     50   (_ : err errHostCodecFailed t)
     51   (hostList? args))
     52 
     53 runArboricxArgs = (bs args :
     54   runArboricxArgsByName [] bs args)
     55 
     56 errHostCodecFailed = 14
     57 
     58 hostTreeTag = 0
     59 hostStringTag = 1
     60 hostNumberTag = 2
     61 hostBoolTag = 3
     62 hostListTag = 4
     63 hostBytesTag = 5
     64 
     65 hostTree = (value : pair hostTreeTag value)
     66 hostString = (characters : pair hostStringTag characters)
     67 hostNumber = (n : pair hostNumberTag n)
     68 hostBool = (b : pair hostBoolTag b)
     69 hostList = (xs : pair hostListTag xs)
     70 hostBytes = (bytes : pair hostBytesTag bytes)
     71 
     72 hostValueTag = (hostValue : fst hostValue)
     73 hostValuePayload = (hostValue : snd hostValue)
     74 
     75 hostBool? = (value : or? (equal? value false) (equal? value true))
     76 
     77 hostNumber? = isNat?
     78 hostList? value = case value of
     79   [] = true
     80   [_ | rest] = hostList? rest
     81   _ = false
     82 
     83 -- Source strings are Unicode scalar lists; bytes are octets, not synonyms.
     84 hostScalar? value = (and? (isNat? value)
     85   (and? (N.lte value 1114111) (not? (N.inRange value 55296 57343))))
     86 hostString? value = case value of
     87   [] = true
     88   [character | rest] = and? (hostScalar? character) (hostString? rest)
     89   _ = false
     90 hostBytes? = Binary.binaryBytes?
     91 
     92 wrapHostValue = (validator wrapper resultValue rest :
     93   matchBool
     94     (ok (wrapper resultValue) rest)
     95     (err errHostCodecFailed rest)
     96     (validator resultValue))
     97 
     98 wrapHostValueByTag tag value rest = case tag of
     99   0 = ok (hostTree value) rest
    100   1 = wrapHostValue hostString? hostString value rest
    101   2 = wrapHostValue hostNumber? hostNumber value rest
    102   3 = wrapHostValue hostBool? hostBool value rest
    103   4 = wrapHostValue hostList? hostList value rest
    104   5 = wrapHostValue hostBytes? hostBytes value rest
    105   _ = err errHostCodecFailed rest
    106 
    107 -- Reject invalid dispatch requests before parsing or applying untrusted code.
    108 runArboricxByNameToTyped tag nameBytes bytes args = (lazyBool
    109   (_ : bindResult (runArboricxArgsByName nameBytes bytes args)
    110     (value rest : wrapHostValueByTag tag value rest))
    111   (_ : err errHostCodecFailed t)
    112   (and? (isNat? tag) (N.lte tag 5)))
    113 
    114 runArboricxByNameToTree = (nameBytes bs args :
    115   runArboricxByNameToTyped hostTreeTag nameBytes bs args)
    116 
    117 runArboricxByNameToString = (nameBytes bs args :
    118   runArboricxByNameToTyped hostStringTag nameBytes bs args)
    119 
    120 runArboricxByNameToNumber = (nameBytes bs args :
    121   runArboricxByNameToTyped hostNumberTag nameBytes bs args)
    122 
    123 runArboricxByNameToBool = (nameBytes bs args :
    124   runArboricxByNameToTyped hostBoolTag nameBytes bs args)
    125 
    126 runArboricxByNameToList = (nameBytes bs args :
    127   runArboricxByNameToTyped hostListTag nameBytes bs args)
    128 
    129 runArboricxByNameToBytes = (nameBytes bs args :
    130   runArboricxByNameToTyped hostBytesTag nameBytes bs args)
    131 
    132 runArboricxToTree = (bs args : runArboricxByNameToTyped hostTreeTag [] bs args)
    133 runArboricxToString = (bs args : runArboricxByNameToTyped hostStringTag [] bs args)
    134 runArboricxToNumber = (bs args : runArboricxByNameToTyped hostNumberTag [] bs args)
    135 runArboricxToBool = (bs args : runArboricxByNameToTyped hostBoolTag [] bs args)
    136 runArboricxToList = (bs args : runArboricxByNameToTyped hostListTag [] bs args)
    137 runArboricxToBytes = (bs args : runArboricxByNameToTyped hostBytesTag [] bs args)