tricu

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

6a758421025aa98114ee63a87e92ac9a6094a69aeb0a18373f2fe6211ff7349e.tri (10993B)

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