tricu

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

a3a1a150ea25365df69c4c19c61d1390eaae87107a3217f386b9bca6d20cbe46.tri (6286B)

      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 = sourceCoreFixI
     93 stableSelf = sourceCoreFixSelf
     94 stableWait = sourceCoreFixWait
     95 stableWaitSelf = sourceCoreFixWaitSelf
     96 stableFix = sourceCoreFix
     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 = sourceAstFunction_ self node
    108 sourceRecursiveFunction = sourceAstFunction?
    109 sourceRecursiveBody definition = sourceAstLambda (fst definition) (sourceDefinitionBody definition)
    110 
    111 -- Wrap self only for ordering; compile the original definitions below. This
    112 -- retains existing missing-name, duplicate, equation and mutual-cycle checks.
    113 sourceStablePrepare_ self definitions = (lazyList (_ : ok [] t)
    114   (definition rest : stableBind
    115     (lazyBool
    116       (_ : lazyBool
    117         (_ : ok (pair (fst definition) (sourceRecursiveBody definition)) t)
    118         (_ : err (parserDiagnostic 48 "recursive function requires parameters"
    119           (sourceDefinitionName definition) (sourceDefinitionPosition definition) t) definition)
    120         (sourceRecursiveFunction (sourceDefinitionBody definition)))
    121       (_ : ok definition t) (sourceDefinitionSelfRecursive definition))
    122     (prepared : stableBind (self rest) (remaining : ok (pair prepared remaining) t)))
    123   definitions)
    124 sourceStablePrepare definitions = y sourceStablePrepare_ definitions
    125 orderStableProgram environment program = (stableBind
    126   (sourceStablePrepare (sourceProgramDefinitions program))
    127   (definitions : orderGateProgram environment (pair definitions (sourceProgramFinal program))))
    128 
    129 sourceCompileStableDefinition environment definition = (let recursive = sourceDefinitionSelfRecursive definition in
    130   stableBind (resolveGateAst environment (lazyBool
    131     (_ : sourceRecursiveBody definition) (_ : sourceDefinitionBody definition) recursive))
    132     (core : stableBind (stableCompileCore core)
    133       (tree : ok (lazyBool (_ : stableFix tree) (_ : tree) recursive) t)))
    134