tricu

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

1dd3ea5f1be1963fff6d51062940f5313cda1ac0f2885f036106d7aad1575577.tri (5827B)

      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 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 (stableBracket (fst (sourceTermPayload term)))
     52           (stableBracket (snd (sourceTermPayload term))) (sourceTermLocation term))
     53         (_ : term)
     54         (equal? (sourceTermKind term) 3))
     55       (equal? (sourceTermKind term) 2))
     56     (equal? (sourceTermKind term) 1)
     57 
     58 
     59 -- Inspect only the kind before selecting payload access. Literal externals
     60 -- remain opaque trees; lists retain residual constructor applications.
     61 stableEliminate node = (case sourceCoreKind node of
     62   ^sourceCoreLeafKind = sourceTermLiteral t (sourceCoreStart node)
     63   ^sourceCoreBoundKind = sourceTermVariable (sourceCorePayload node) (sourceCoreStart node)
     64   ^sourceCoreApplyKind = stableTermApply
     65     (stableEliminate (fst (sourceCorePayload node)))
     66     (stableEliminate (snd (sourceCorePayload node))) (sourceCoreStart node)
     67   ^sourceCoreLambdaKind = stableBracket (stableEliminate (sourceCorePayload node))
     68   ^sourceCoreExternalKind = sourceTermLiteral (sourceCorePayload node) (sourceCoreStart node)
     69   ^sourceCoreNumberKind = sourceTermLiteral (sourceCorePayload node) (sourceCoreStart node)
     70   ^sourceCoreStringKind = sourceTermLiteral (sourceCorePayload node) (sourceCoreStart node)
     71   ^sourceCoreListKind = sourceEliminateList (sourceCorePayload node) stableEliminate (sourceCoreStart node)
     72   _ = sourceTermInvalid node (sourceCoreStart node))
     73 
     74 -- Native wait and Z, with self-first workers: Z f x = f (Z f) x.
     75 -- All applications below construct trees out of already-normal arguments.
     76 stableI = sourceCoreFixI
     77 stableSelf = sourceCoreFixSelf
     78 stableWait = sourceCoreFixWait
     79 stableWaitSelf = sourceCoreFixWaitSelf
     80 stableFix = sourceCoreFix
     81 
     82 stableBind result next = lazyResult (problem rest : err problem rest) (value unused : next value) result
     83 stableCompileCore core = sourceRunTerm (stableEliminate core)
     84 
     85 -- Determine self-reference with the ordinary lexical free-name traversal. A
     86 -- parameter/local/pattern capture of the same spelling is not recursion.
     87 sourceDefinitionSelfRecursive definition = (lazyMaybe (_ : false) (_ : true)
     88   (sourceFindBinder (map sourceAstPayload (sourceFreeNames (sourceDefinitionBody definition)))
     89     (sourceDefinitionName definition)))
     90 
     91 sourceRecursiveFunction = sourceAstFunction?
     92 sourceRecursiveBody definition = sourceAstLambda (fst definition) (sourceDefinitionBody definition)
     93 
     94 -- Wrap self only for ordering; compile the original definitions below. This
     95 -- retains existing missing-name, duplicate, equation and mutual-cycle checks.
     96 sourceStablePrepare definitions = (lazyList (_ : ok [] t)
     97   (definition rest : stableBind
     98     (lazyBool
     99       (_ : lazyBool
    100         (_ : ok (pair (fst definition) (sourceRecursiveBody definition)) t)
    101         (_ : err (parserDiagnostic 48 "recursive function requires parameters"
    102           (sourceDefinitionName definition) (sourceDefinitionPosition definition) t) definition)
    103         (sourceRecursiveFunction (sourceDefinitionBody definition)))
    104       (_ : ok definition t) (sourceDefinitionSelfRecursive definition))
    105     (prepared : stableBind (sourceStablePrepare rest) (remaining : ok (pair prepared remaining) t)))
    106   definitions)
    107 orderStableProgram environment program = (stableBind
    108   (sourceStablePrepare (sourceProgramDefinitions program))
    109   (definitions : orderGateProgram environment (pair definitions (sourceProgramFinal program))))
    110 
    111 sourceCompileStableDefinition environment definition = (let recursive = sourceDefinitionSelfRecursive definition in
    112   stableBind (resolveStableGateAst environment (lazyBool
    113     (_ : sourceRecursiveBody definition) (_ : sourceDefinitionBody definition) recursive))
    114     (core : stableBind (stableCompileCore core)
    115       (tree : ok (lazyBool (_ : stableFix tree) (_ : tree) recursive) t)))
    116