tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

47ebe7c143d9a639e3d4c9a8cc346411ac9607eeb9c6962050c9289c1a8cbbdf.tri (10932B)

      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 stableTermApply
     10 !export stableApplication
     11 !export stableBracket
     12 !export stableEliminate
     13 !export stableI
     14 !export stableSelf
     15 !export stableWait
     16 !export stableWaitSelf
     17 !export stableFix
     18 !export stableBind
     19 !export stableCompileCore
     20 !export sourceDefinitionSelfRecursive
     21 !export sourceRecursiveFunction
     22 !export sourceRecursiveBody
     23 !export sourceStablePrepare
     24 !export orderStableProgram
     25 !export sourceCompileStableDefinition
     26 !export sourceCompileStableDefinitionWith
     27 !export orderStableProgramWith
     28 
     29 -- Stable native abstraction backend. Selected explicitly by the unit/build API.
     30 -- Barry Jay, Reflective Programs in Tree Calculus, sections 4.2, 4.4-4.5.
     31 
     32 -- Fold only constructor applications whose operands are literal trees. Leaf
     33 -- and Stem functions construct Stem/Fork without reducing a redex. Never fold
     34 -- a Fork function here: that would reintroduce the closed-body hazard. Packing
     35 -- these generated trees avoids re-abstracting their syntax at every binder.
     36 stableTermApply function argument location = (lazyBool
     37   (_ : triage
     38     (sourceTermLiteral (t (sourceTermPayload argument)) location)
     39     (child : sourceTermLiteral (t child (sourceTermPayload argument)) location)
     40     (_ _ : sourceTermApply function argument location)
     41     (sourceTermPayload function))
     42   (_ : sourceTermApply function argument location)
     43   (and? (equal? (sourceTermKind function) 1) (equal? (sourceTermKind argument) 1)))
     44 
     45 -- tricu's stem rule is t (t a) b c = a c (b c), unlike the book's
     46 -- reversed b c (a c). Thus [x](u v) = t (t ([x]u)) ([x]v).
     47 -- The annotated path below may prune independent constructor-only subtrees.
     48 -- Literal payloads are represented trees.
     49 stableApplication left right location = (stableTermApply
     50   (stableTermApply (sourceTermLiteral t location)
     51     (stableTermApply (sourceTermLiteral t location) left location) location)
     52   right location)
     53 
     54 -- Internal annotated residual: ((shape, minimum-free-index+1), ordinary node).
     55 -- Its application children carry the same annotations. Metadata is maintained
     56 -- incrementally as nodes are built. A zero minimum denotes a closed subtree;
     57 -- one means the binder being eliminated occurs. Any larger minimum shifts down by one when
     58 -- removing an unused binder. Literal payloads are already represented trees.
     59 -- Shape certificates permit only Leaf/Stem construction with certified
     60 -- arguments. A variable has an opaque shape.
     61 -- Fork applications, unknown calls and constructors containing computations
     62 -- remain residual; neither binder independence alone nor eta is sufficient.
     63 -- The ordinary residual API is restored at the public boundary. Keep both
     64 -- shape and dependency summaries out of executable trees and diagnostics.
     65 -- Zero bound means closed. Shapes: 0 computation, 1 Leaf, 2 Stem,
     66 -- 3 Fork, 4 opaque variable. Application children carry annotations too.
     67 stableCachedNode kind payload location shape bound =
     68   pair (pair shape bound) (sourceTermNode kind payload location)
     69 stableCachedShape node = fst (fst node)
     70 stableCachedBound node = snd (fst node)
     71 stableCachedKind node = sourceTermKind (snd node)
     72 stableCachedPayload node = sourceTermPayload (snd node)
     73 stableCachedLocation node = sourceTermLocation (snd node)
     74 stableCachedLiteral tree location = stableCachedNode 1 tree location (triage 1 (_ : 2) (_ _ : 3) tree) 0
     75 stableCachedVariable index location = stableCachedNode 2 index location 4 (succ index)
     76 stableCachedMin left right = lazyBool (_ : right)
     77   (_ : lazyBool (_ : left)
     78     (_ : lazyBool (_ : left) (_ : right) (lte_? left right))
     79     (isZero_? right)) (isZero_? left)
     80 stableCachedRawApply function argument location = (let shape = stableCachedShape function in
     81   stableCachedNode 3 (pair function argument) location
     82     (lazyBool
     83       (_ : lazyBool (_ : 0) (_ : succ shape) (isZero_? (stableCachedShape argument)))
     84       (_ : 0) (or? (equal? shape 1) (equal? shape 2)))
     85     (stableCachedMin (stableCachedBound function) (stableCachedBound argument)))
     86 stableCachedApply function argument location = lazyBool
     87   (_ : triage
     88     (stableCachedLiteral (t (stableCachedPayload argument)) location)
     89     (child : stableCachedLiteral (t child (stableCachedPayload argument)) location)
     90     (_ _ : stableCachedRawApply function argument location)
     91     (stableCachedPayload function))
     92   (_ : stableCachedRawApply function argument location)
     93   (and? (equal? (stableCachedKind function) 1) (equal? (stableCachedKind argument) 1))
     94 stableCachedApplication left right location = stableCachedApply
     95   (stableCachedApply (stableCachedLiteral t location) (stableCachedApply (stableCachedLiteral t location) left location) location)
     96   right location
     97 -- Precondition: the current binder is absent (minimum is not one).
     98 -- Closed subtrees need neither shifting nor copying. Remaining metadata can
     99 -- be shifted directly: no shape or dependency traversal is needed here.
    100 stableCachedLower term = lazyBool
    101   (_ : term)
    102   (_ : case stableCachedKind term of
    103     2 = stableCachedVariable (pred_ (stableCachedPayload term)) (stableCachedLocation term)
    104     3 = stableCachedNode 3 (pair (stableCachedLower (fst (stableCachedPayload term))) (stableCachedLower (snd (stableCachedPayload term))))
    105       (stableCachedLocation term) (stableCachedShape term) (pred_ (stableCachedBound term))
    106     _ = term)
    107   (isZero_? (stableCachedBound term))
    108 stableCachedBracket term = case stableCachedKind term of
    109   1 = stableCachedApply (stableCachedLiteral sourceCombK (stableCachedLocation term)) term (stableCachedLocation term)
    110   2 = lazyBool
    111     (_ : stableCachedLiteral sourceCombI (stableCachedLocation term))
    112     (_ : stableCachedApply (stableCachedLiteral sourceCombK (stableCachedLocation term))
    113       (stableCachedVariable (pred_ (stableCachedPayload term)) (stableCachedLocation term)) (stableCachedLocation term))
    114     (isZero_? (stableCachedPayload term))
    115   3 = lazyBool
    116     (_ : stableCachedApply (stableCachedLiteral sourceCombK (stableCachedLocation term)) (stableCachedLower term) (stableCachedLocation term))
    117     (_ : stableCachedApplication (stableCachedBracket (fst (stableCachedPayload term)))
    118       (stableCachedBracket (snd (stableCachedPayload term))) (stableCachedLocation term))
    119     (and? (not? (equal? (stableCachedBound term) 1)) (not? (isZero_? (stableCachedShape term))))
    120   _ = term
    121 stableCachedFromPlain term = case sourceTermKind term of
    122   1 = stableCachedLiteral (sourceTermPayload term) (sourceTermLocation term)
    123   2 = stableCachedVariable (sourceTermPayload term) (sourceTermLocation term)
    124   3 = stableCachedRawApply (stableCachedFromPlain (fst (sourceTermPayload term)))
    125     (stableCachedFromPlain (snd (sourceTermPayload term))) (sourceTermLocation term)
    126   _ = stableCachedNode (sourceTermKind term) (sourceTermPayload term) (sourceTermLocation term) 0 0
    127 stableCachedToPlain term = case stableCachedKind term of
    128   3 = sourceTermApply (stableCachedToPlain (fst (stableCachedPayload term)))
    129     (stableCachedToPlain (snd (stableCachedPayload term))) (stableCachedLocation term)
    130   _ = snd term
    131 stableCachedEliminate node = case sourceCoreKind node of
    132   1 = stableCachedLiteral t (sourceCoreStart node)
    133   2 = stableCachedVariable (sourceCorePayload node) (sourceCoreStart node)
    134   3 = stableCachedApply (stableCachedEliminate (fst (sourceCorePayload node)))
    135     (stableCachedEliminate (snd (sourceCorePayload node))) (sourceCoreStart node)
    136   4 = stableCachedBracket (stableCachedEliminate (sourceCorePayload node))
    137   5 = stableCachedLiteral (sourceCorePayload node) (sourceCoreStart node)
    138   6 = stableCachedLiteral (sourceCorePayload node) (sourceCoreStart node)
    139   7 = stableCachedLiteral (sourceCorePayload node) (sourceCoreStart node)
    140   8 = (let rec elements pending = (lazyList
    141     (_ : stableCachedLiteral t (sourceCoreStart node))
    142     (head rest : stableCachedRawApply
    143       (stableCachedRawApply (stableCachedLiteral t (sourceCoreStart node)) (stableCachedEliminate head) (sourceCoreStart node))
    144       (elements rest) (sourceCoreStart node)) pending)
    145     in elements (sourceCorePayload node))
    146   _ = stableCachedNode 4 node (sourceCoreStart node) 0 0
    147 stableBracket   term = stableCachedToPlain (stableCachedBracket (stableCachedFromPlain term))
    148 stableEliminate node = stableCachedToPlain (stableCachedEliminate node)
    149 
    150 -- Native wait and Z, with self-first workers: Z f x = f (Z f) x.
    151 -- All applications below construct trees out of already-normal arguments.
    152 stableI        = sourceCoreFixI
    153 stableSelf     = sourceCoreFixSelf
    154 stableWait     = sourceCoreFixWait
    155 stableWaitSelf = sourceCoreFixWaitSelf
    156 stableFix      = sourceCoreFix
    157 
    158 stableBind        result next = lazyResult (problem rest : err problem rest) (value unused : next value) result
    159 stableCompileCore core        = sourceRunTerm (stableEliminate core)
    160 
    161 -- Determine self-reference with the ordinary lexical free-name traversal. A
    162 -- parameter/local/pattern capture of the same spelling is not recursion.
    163 sourceDefinitionSelfRecursive definition = (lazyMaybe (_ : false) (_ : true)
    164   (sourceFindBinder (map sourceAstPayload (sourceFreeNames (sourceDefinitionBody definition)))
    165     (sourceDefinitionName definition)))
    166 
    167 sourceRecursiveFunction        = sourceAstFunction?
    168 sourceRecursiveBody definition = sourceAstLambda (fst definition) (sourceDefinitionBody definition)
    169 
    170 -- Wrap self only for ordering; compile the original definitions below. This
    171 -- retains existing missing-name, duplicate, equation and mutual-cycle checks.
    172 sourceStablePrepare definitions = (lazyList (_ : ok [] t)
    173   (definition rest : stableBind
    174     (lazyBool
    175       (_ : lazyBool
    176         (_ : ok (pair (fst definition) (sourceRecursiveBody definition)) t)
    177         (_ : err (parserDiagnostic 48 "recursive function requires parameters"
    178           (sourceDefinitionName definition) (sourceDefinitionPosition definition) t) definition)
    179         (sourceRecursiveFunction (sourceDefinitionBody definition)))
    180       (_ : ok definition t) (sourceDefinitionSelfRecursive definition))
    181     (prepared : stableBind (sourceStablePrepare rest) (remaining : ok (pair prepared remaining) t)))
    182   definitions)
    183 orderStableProgramWith orderProgram environment program = (stableBind
    184   (sourceStablePrepare (sourceProgramDefinitions program))
    185   (definitions : orderProgram environment (pair definitions (sourceProgramFinal program))))
    186 
    187 sourceCompileStableDefinitionWith resolve environment definition = (let recursive = sourceDefinitionSelfRecursive definition in
    188   stableBind (resolve environment (lazyBool
    189     (_ : sourceRecursiveBody definition) (_ : sourceDefinitionBody definition) recursive))
    190     (core : stableBind (stableCompileCore core)
    191       (tree : ok (lazyBool (_ : stableFix tree) (_ : tree) recursive) t)))
    192 
    193 orderStableProgram = orderStableProgramWith orderGateProgram
    194 sourceCompileStableDefinition = sourceCompileStableDefinitionWith resolveStableGateAst