tricu

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

stable.tri (11004B)

      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, not deferred applications.
     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 are annotated, not ordinary sourceTerm values.
     56 -- Metadata is maintained as nodes are built, never by scanning a subtree at
     57 -- each bracket visit. A zero minimum denotes a closed subtree; one means the
     58 -- 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 is an opaque value, never a known callable 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 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