tricu

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

ca105b189c1e70919efe86232915ba0c3bc43a385efa48a3c3269c5a17309e48.tri (10771B)

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