tricu

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

f67a4c8962535f306b6ab5383dc38223aab3c35e11d6053070b854af8adcdf00.tri (6731B)

      1 !import prelude *
      2 !import parser *
      3 !import source_core *
      4 !import source_ast *
      5 !import source_compile *
      6 !import source_resolve *
      7 !import source_program *
      8 !import source_order *
      9 !export *
     10 
     11 -- Stable native abstraction backend. Selected explicitly by the unit/build API.
     12 -- Barry Jay, Reflective Programs in Tree Calculus, sections 4.2, 4.4-4.5.
     13 
     14 -- Fold only constructor applications whose operands are literal trees. Leaf
     15 -- and Stem functions construct Stem/Fork without reducing a redex. Never fold
     16 -- a Fork function here: that would reintroduce the closed-body hazard. Packing
     17 -- these generated trees avoids re-abstracting their syntax at every binder.
     18 stableTermApply function argument location = (lazyBool
     19   (_ : triage
     20     (sourceTermLiteral (t (sourceTermPayload argument)) location)
     21     (child : sourceTermLiteral (t child (sourceTermPayload argument)) location)
     22     (_ _ : sourceTermApply function argument location)
     23     (sourceTermPayload function))
     24   (_ : sourceTermApply function argument location)
     25   (and? (equal? (sourceTermKind function) 1) (equal? (sourceTermKind argument) 1)))
     26 
     27 -- tricu's stem rule is t (t a) b c = a c (b c), unlike the book's
     28 -- reversed b c (a c). Thus [x](u v) = t (t ([x]u)) ([x]v).
     29 -- No independent-application K shortcut. Literal payloads are already
     30 -- represented trees, not deferred applications.
     31 stableApplication left right location = (stableTermApply
     32   (stableTermApply (sourceTermLiteral t location)
     33     (stableTermApply (sourceTermLiteral t location) left location) location)
     34   right location)
     35 
     36 stableBracket_ self term =
     37   lazyBool
     38     (_ : stableTermApply
     39       (sourceTermLiteral sourceCombK (sourceTermLocation term)) term
     40       (sourceTermLocation term))
     41     (_ : lazyBool
     42       (_ : lazyBool
     43         (_ : sourceTermLiteral sourceCombI (sourceTermLocation term))
     44         (_ : stableTermApply
     45           (sourceTermLiteral sourceCombK (sourceTermLocation term))
     46           (sourceTermVariable (pred_ (sourceTermPayload term))
     47             (sourceTermLocation term))
     48           (sourceTermLocation term))
     49         (isZero_? (sourceTermPayload term)))
     50       (_ : lazyBool
     51         (_ : stableApplication (self (fst (sourceTermPayload term)))
     52           (self (snd (sourceTermPayload term))) (sourceTermLocation term))
     53         (_ : term)
     54         (equal? (sourceTermKind term) 3))
     55       (equal? (sourceTermKind term) 2))
     56     (equal? (sourceTermKind term) 1)
     57 
     58 stableBracket = (term : y stableBracket_ term)
     59 
     60 stableEliminate_ self node =
     61   lazyBool
     62     (_ : sourceTermLiteral t (sourceCoreStart node))
     63     (_ : lazyBool
     64       (_ : sourceTermVariable (sourceCorePayload node) (sourceCoreStart node))
     65       (_ : lazyBool
     66         (_ : stableTermApply
     67           (self (fst (sourceCorePayload node)))
     68           (self (snd (sourceCorePayload node)))
     69           (sourceCoreStart node))
     70         (_ : lazyBool
     71           (_ : stableBracket (self (sourceCorePayload node)))
     72           (_ : lazyBool
     73             (_ : sourceTermLiteral (sourceCorePayload node)
     74                    (sourceCoreStart node))
     75             (_ : lazyBool
     76               (_ : sourceEliminateList (sourceCorePayload node)
     77                 self (sourceCoreStart node))
     78               (_ : sourceTermInvalid node (sourceCoreStart node))
     79               (equal? (sourceCoreKind node) sourceCoreListKind))
     80             (or? (equal? (sourceCoreKind node) sourceCoreExternalKind)
     81                  (or? (equal? (sourceCoreKind node) sourceCoreNumberKind)
     82                       (equal? (sourceCoreKind node) sourceCoreStringKind))))
     83           (equal? (sourceCoreKind node) sourceCoreLambdaKind))
     84         (equal? (sourceCoreKind node) sourceCoreApplyKind))
     85       (equal? (sourceCoreKind node) sourceCoreBoundKind))
     86     (equal? (sourceCoreKind node) sourceCoreLeafKind)
     87 
     88 stableEliminate = (node : y stableEliminate_ node)
     89 
     90 -- Native wait and Z, with self-first workers: Z f x = f (Z f) x.
     91 -- All applications below construct trees out of already-normal arguments.
     92 stableI = sourceCombI
     93 stableSelf = t (t stableI) stableI
     94 stableWait f x = t (t (t (t (t t f)) (t t x))) stableI
     95 stableWaitSelf x = stableWait stableSelf x
     96 stableFix f = stableWait stableSelf (t (t (t t f)) stableWaitSelf)
     97 
     98 stableBind result next = lazyResult (problem rest : err problem rest) (value unused : next value) result
     99 stableCompileCore core = sourceRunTerm (stableEliminate core)
    100 
    101 -- Determine self-reference with the ordinary lexical free-name traversal. A
    102 -- parameter/local/pattern capture of the same spelling is not recursion.
    103 sourceDefinitionSelfRecursive definition = (lazyMaybe (_ : false) (_ : true)
    104   (sourceFindBinder (map sourceAstPayload (sourceFreeNames (sourceDefinitionBody definition)))
    105     (sourceDefinitionName definition)))
    106 
    107 sourceRecursiveFunction_ self node = (let kind = sourceAstKind node in
    108   lazyBool (_ : true)
    109     (_ : lazyBool (_ : self (sourceAstPayload node))
    110       (_ : lazyBool
    111         (_ : lazyList (_ : false) (equation rest : not? (emptyList? (fst equation)))
    112           (sourceAstPayload node))
    113         (_ : false) (equal? kind sourceAstEquationsKind))
    114       (equal? kind sourceAstGroupKind))
    115     (equal? kind sourceAstLambdaKind))
    116 sourceRecursiveFunction node = y sourceRecursiveFunction_ node
    117 sourceRecursiveBody definition = sourceAstLambda (fst definition) (sourceDefinitionBody definition)
    118 
    119 -- Wrap self only for ordering; compile the original definitions below. This
    120 -- retains existing missing-name, duplicate, equation and mutual-cycle checks.
    121 sourceStablePrepare_ self definitions = (lazyList (_ : ok [] t)
    122   (definition rest : stableBind
    123     (lazyBool
    124       (_ : lazyBool
    125         (_ : ok (pair (fst definition) (sourceRecursiveBody definition)) t)
    126         (_ : err (parserDiagnostic 48 "recursive function requires parameters"
    127           (sourceDefinitionName definition) (sourceDefinitionPosition definition) t) definition)
    128         (sourceRecursiveFunction (sourceDefinitionBody definition)))
    129       (_ : ok definition t) (sourceDefinitionSelfRecursive definition))
    130     (prepared : stableBind (self rest) (remaining : ok (pair prepared remaining) t)))
    131   definitions)
    132 sourceStablePrepare definitions = y sourceStablePrepare_ definitions
    133 orderStableProgram environment program = (stableBind
    134   (sourceStablePrepare (sourceProgramDefinitions program))
    135   (definitions : orderGateProgram environment (pair definitions (sourceProgramFinal program))))
    136 
    137 sourceCompileStableDefinition environment definition = (let recursive = sourceDefinitionSelfRecursive definition in
    138   stableBind (resolveGateAst environment (lazyBool
    139     (_ : sourceRecursiveBody definition) (_ : sourceDefinitionBody definition) recursive))
    140     (core : stableBind (stableCompileCore core)
    141       (tree : ok (lazyBool (_ : stableFix tree) (_ : tree) recursive) t)))
    142