tricu

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

381ba6e37050972ee435d151216ae7015fb09a7333c1d43752a76f29294193f8.tri (12504B)

      1 !import prelude *
      2 !import parser *
      3 !import source_core *
      4 !export *
      5 
      6 -- Equation lowering prototype, independent of the surface parser and SCP ABI.
      7 -- Pattern = (tag, (payload, location)); literal payloads are opaque trees.
      8 -- Equation = (argument patterns, core body). Body indices address captures in
      9 -- reverse introduction order, then surrounding lexical binders. Pin core is
     10 -- resolved in that surrounding scope, never against this equation's captures.
     11 -- Inputs are compiler-built patterns and well-formed source.core syntax.
     12 
     13 sourcePatternNode tag payload location = pair tag (pair payload location)
     14 sourcePatternTag pattern = fst pattern
     15 sourcePatternPayload pattern = fst (snd pattern)
     16 sourcePatternLocation pattern = snd (snd pattern)
     17 sourcePatternAny location = sourcePatternNode 0 t location
     18 sourcePatternLeaf location = sourcePatternNode 1 t location
     19 sourcePatternStem child location = sourcePatternNode 2 child location
     20 sourcePatternFork left right location = sourcePatternNode 3 (pair left right) location
     21 sourcePatternCapture name location = sourcePatternNode 4 name location
     22 sourcePatternLiteral tree location = sourcePatternNode 5 tree location
     23 sourcePatternWhole name child location = sourcePatternNode 6 (pair name child) location
     24 sourcePatternPin core location = sourcePatternNode 7 core location
     25 sourceEquation patterns body = pair patterns body
     26 
     27 spLit tree = sourceCoreExternal tree t t
     28 spVar index = sourceCoreBound index t t
     29 spApp function argument = sourceCoreApply function argument t t
     30 spLam body = sourceCoreLambda body t t
     31 spApp2 f a b = spApp (spApp f a) b
     32 spApp3 f a b c = spApp (spApp2 f a b) c
     33 spApp4 f a b c d = spApp (spApp3 f a b c) d
     34 
     35 -- All three branches are continuations, including Leaf. Work is performed
     36 -- only after structural selection, not passed as an ordinary triage result.
     37 spSelect leafK stemK forkK value = ((chosen : chosen t)
     38   (triage leafK (child : _ : stemK child)
     39     (left right : _ : forkK left right) value))
     40 
     41 -- Syntax-driven shifting; never inspect an External's arbitrary tree payload.
     42 spShift_ self node cutoff = (let kind = sourceCoreKind node in
     43   lazyBool
     44     (_ : lazyBool
     45       (_ : sourceCoreBound (succ (sourceCorePayload node))
     46         (sourceCoreStart node) (sourceCoreEnd node))
     47       (_ : node) (lte_? cutoff (sourceCorePayload node)))
     48     (_ : lazyBool
     49       (_ : sourceCoreApply
     50         (self (fst (sourceCorePayload node)) cutoff)
     51         (self (snd (sourceCorePayload node)) cutoff)
     52         (sourceCoreStart node) (sourceCoreEnd node))
     53       (_ : lazyBool
     54         (_ : sourceCoreLambda (self (sourceCorePayload node) (succ cutoff))
     55           (sourceCoreStart node) (sourceCoreEnd node))
     56         (_ : lazyBool
     57           (_ : sourceCoreList (map (child : self child cutoff)
     58             (sourceCorePayload node)) (sourceCoreStart node) (sourceCoreEnd node))
     59           (_ : node) (equal? kind sourceCoreListKind))
     60         (equal? kind sourceCoreLambdaKind))
     61       (equal? kind sourceCoreApplyKind))
     62     (equal? kind sourceCoreBoundKind))
     63 spShift node = y spShift_ node 0
     64 spShift2 node = spShift (spShift node)
     65 -- Consume a syntax-derived binder list, not a numeric depth difference.
     66 spRaise_ self fuel node = (lazyList (_ : node)
     67   (_ rest : self rest (spShift node)) fuel)
     68 spRaise node fuel = y spRaise_ fuel node
     69 
     70 -- Context = (binder fuel, (reverse captures, pending argument/sibling syntax)).
     71 -- Capture aliases and pending expressions are shifted together under every
     72 -- generated binder. No counter-driven sibling raising or runtime table exists.
     73 spContext fuel captures pending = pair fuel (pair captures pending)
     74 spFuel ctx = fst ctx
     75 spDepth ctx = length (spFuel ctx)
     76 spCaptures ctx = fst (snd ctx)
     77 spPending ctx = snd (snd ctx)
     78 spShiftContext ctx = (spContext (pair t (spFuel ctx))
     79   (map (entry : pair (fst entry) (spShift (snd entry))) (spCaptures ctx))
     80   (map spShift (spPending ctx)))
     81 spBind ctx name value = (spContext (spFuel ctx)
     82   (pair (pair name value) (spCaptures ctx)) (spPending ctx))
     83 spSave ctx value = spContext (spFuel ctx) (spCaptures ctx) (pair value (spPending ctx))
     84 spPop ctx = spContext (spFuel ctx) (spCaptures ctx) (snd (spPending ctx))
     85 
     86 spCaptureAt_ self captures index = (lazyList (_ : nothing)
     87   (entry rest : lazyBool (_ : just (snd entry))
     88     (_ : self rest (pred_ index)) (isZero_? index)) captures)
     89 spCaptureAt captures index = y spCaptureAt_ captures index
     90 
     91 -- Substitute resolved capture indices, preserving lambdas in the body and
     92 -- shifting outer lexical references past generated matcher binders.
     93 spBodyBound node ctx fuel = (let index = sourceCorePayload node in
     94   let cutoff = length fuel in
     95   lazyBool (_ : node)
     96     (_ : lazyMaybe
     97       (_ : sourceCoreBound
     98         (add cutoff (add (spDepth ctx)
     99           (sub (sub index cutoff) (length (spCaptures ctx)))))
    100         (sourceCoreStart node) (sourceCoreEnd node))
    101       (value : sourceCoreWithSpan (spRaise value fuel)
    102         (sourceCoreStart node) (sourceCoreEnd node))
    103       (spCaptureAt (spCaptures ctx) (sub index cutoff)))
    104     (lt_? index cutoff))
    105 spBody_ self node ctx fuel = (let kind = sourceCoreKind node in
    106   lazyBool (_ : spBodyBound node ctx fuel)
    107     (_ : lazyBool
    108       (_ : sourceCoreApply
    109         (self (fst (sourceCorePayload node)) ctx fuel)
    110         (self (snd (sourceCorePayload node)) ctx fuel)
    111         (sourceCoreStart node) (sourceCoreEnd node))
    112       (_ : lazyBool
    113         (_ : sourceCoreLambda (self (sourceCorePayload node) ctx (pair t fuel))
    114           (sourceCoreStart node) (sourceCoreEnd node))
    115         (_ : lazyBool
    116           (_ : sourceCoreList (map (child : self child ctx fuel)
    117             (sourceCorePayload node)) (sourceCoreStart node) (sourceCoreEnd node))
    118           (_ : node) (equal? kind sourceCoreListKind))
    119         (equal? kind sourceCoreLambdaKind))
    120       (equal? kind sourceCoreApplyKind))
    121     (equal? kind sourceCoreBoundKind))
    122 spBody node ctx = y spBody_ node ctx t
    123 
    124 spCase leaf stem fork value = (spApp4 (spLit spSelect)
    125   (spLam (spShift leaf)) (spLam stem) (spLam (spLam fork)) value)
    126 spIf yes no condition = (spApp3 (spLit lazyBool)
    127   (spLam (spShift yes)) (spLam (spShift no)) condition)
    128 
    129 -- hit receives the updated context and shifted miss expression. A left
    130 -- child's handlers may add binders before its saved right sibling is visited.
    131 spPattern_ self pattern value ctx hit miss = (let payload = sourcePatternPayload pattern in
    132   let tag = sourcePatternTag pattern in
    133   lazyBool (_ : hit ctx miss)
    134     (_ : lazyBool
    135       (_ : spCase (hit ctx miss) (spShift miss) (spShift2 miss) value)
    136       (_ : lazyBool
    137         (_ : spCase miss
    138           (self payload (spVar 0) (spShiftContext ctx) hit (spShift miss))
    139           (spShift2 miss) value)
    140         (_ : lazyBool
    141           (_ : spCase miss (spShift miss)
    142             (self (fst payload) (spVar 1)
    143               (spSave (spShiftContext (spShiftContext ctx)) (spVar 0))
    144               (next nextMiss : self (snd payload) (fst (spPending next))
    145                 (spPop next) hit nextMiss)
    146               (spShift2 miss)) value)
    147           (_ : lazyBool
    148             (_ : hit (spBind ctx payload value) miss)
    149             (_ : lazyBool
    150               (_ : spIf (hit ctx miss) miss
    151                 (spApp2 (spLit equal?) value (spLit payload)))
    152               (_ : lazyBool
    153                 (_ : self (snd payload) value (spBind ctx (fst payload) value) hit miss)
    154                 (_ : spIf (hit ctx miss) miss
    155                   (spApp2 (spLit equal?) value (spRaise payload (spFuel ctx))))
    156                 (equal? tag 6))
    157               (equal? tag 5))
    158             (equal? tag 4))
    159           (equal? tag 3))
    160         (equal? tag 2))
    161       (equal? tag 1))
    162     (equal? tag 0))
    163 spPattern pattern value ctx hit miss = y spPattern_ pattern value ctx hit miss
    164 
    165 spArguments_ self patterns = (lazyList (_ : t)
    166   (_ rest : pair (spVar (length rest)) (self rest)) patterns)
    167 spArguments patterns = y spArguments_ patterns
    168 spMatchArguments_ self patterns ctx body miss = (lazyList
    169   (_ : spBody body ctx)
    170   (pattern rest : spPattern pattern (fst (spPending ctx)) (spPop ctx)
    171     (next nextMiss : self rest next body nextMiss) miss) patterns)
    172 spMatchArguments patterns ctx body miss = y spMatchArguments_ patterns ctx body miss
    173 
    174 -- The final equation is irrefutable, so the empty suffix is unreachable.
    175 -- One native lazy continuation shares all misses to the remaining equations.
    176 spEquations_ self equations ctx = (lazyList (_ : spLit t)
    177   (equation rest : spApp
    178     (spLam (spMatchArguments (fst equation)
    179       (spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
    180     (spLam (spShift (self rest ctx)))) equations)
    181 spEquations equations ctx = y spEquations_ equations ctx
    182 spWrap_ self patterns body = (lazyList (_ : body)
    183   (_ rest : spLam (self rest body)) patterns)
    184 spWrap patterns body = y spWrap_ patterns body
    185 
    186 spDiagnostic expected found location = parserDiagnostic 48 expected found location t
    187 spError expected pattern = (err
    188   (spDiagnostic expected (sourcePatternTag pattern) (sourcePatternLocation pattern)) t)
    189 spHasName_ self names name = (lazyList (_ : false)
    190   (head rest : lazyBool (_ : true) (_ : self rest name) (equal? head name)) names)
    191 spHasName names name = y spHasName_ names name
    192 spIntroduce names name pattern = (lazyBool
    193   (_ : err (spDiagnostic "unique capture" name (sourcePatternLocation pattern)) t)
    194   (_ : ok (pair name names) t) (spHasName names name))
    195 spValidatePattern_ self pattern names = (let tag = sourcePatternTag pattern in
    196   let payload = sourcePatternPayload pattern in
    197   lazyBool (_ : ok names t)
    198     (_ : lazyBool (_ : ok names t)
    199       (_ : lazyBool (_ : self payload names)
    200         (_ : lazyBool
    201           (_ : lazyResult (problem rest : err problem rest)
    202             (next rest : self (snd payload) next) (self (fst payload) names))
    203           (_ : lazyBool (_ : spIntroduce names payload pattern)
    204             (_ : lazyBool (_ : ok names t)
    205               (_ : lazyBool
    206                 (_ : lazyResult (problem rest : err problem rest)
    207                   (next rest : self (snd payload) next)
    208                   (spIntroduce names (fst payload) pattern))
    209                 (_ : lazyBool (_ : ok names t) (_ : spError "pattern tag" pattern)
    210                   (equal? tag 7))
    211                 (equal? tag 6))
    212               (equal? tag 5))
    213             (equal? tag 4))
    214           (equal? tag 3))
    215         (equal? tag 2))
    216       (equal? tag 1))
    217     (equal? tag 0))
    218 spValidatePattern pattern names = y spValidatePattern_ pattern names
    219 spValidateArguments_ self patterns names = (lazyList (_ : ok names t)
    220   (pattern rest : lazyResult (problem tail : err problem tail)
    221     (next tail : self rest next) (spValidatePattern pattern names)) patterns)
    222 spValidateArguments patterns = y spValidateArguments_ patterns t
    223 spIrrefutable_ self pattern = (let tag = sourcePatternTag pattern in
    224   lazyBool (_ : true)
    225     (_ : lazyBool (_ : true)
    226       (_ : lazyBool (_ : self (snd (sourcePatternPayload pattern))) (_ : false)
    227         (equal? tag 6)) (equal? tag 4)) (equal? tag 0))
    228 spIrrefutable pattern = y spIrrefutable_ pattern
    229 spAllIrrefutable_ self patterns = (lazyList (_ : true)
    230   (pattern rest : lazyBool (_ : self rest) (_ : false) (spIrrefutable pattern)) patterns)
    231 spAllIrrefutable patterns = y spAllIrrefutable_ patterns
    232 spValidateEquations_ self equations arity = (lazyList
    233   (_ : err (spDiagnostic "nonempty equations" t t) t)
    234   (equation rest : lazyBool
    235     (_ : lazyResult (problem tail : err problem tail)
    236       (names tail : lazyList
    237         (_ : lazyBool (_ : ok t t)
    238           (_ : err (spDiagnostic "final irrefutable equation" t
    239             (sourceCoreStart (snd equation))) t)
    240           (spAllIrrefutable (fst equation)))
    241         (_ tail : self rest arity) rest)
    242       (spValidateArguments (fst equation)))
    243     (_ : err (spDiagnostic "consistent arity" (length (fst equation))
    244       (sourceCoreStart (snd equation))) t)
    245     (equal? (length (fst equation)) arity)) equations)
    246 spValidateEquations equations arity = y spValidateEquations_ equations arity
    247 
    248 sourceLowerEquations equations = (lazyList
    249   (_ : err (spDiagnostic "nonempty equations" t t) t)
    250   (first rest : let patterns = fst first in
    251     let arity = length patterns in
    252     lazyBool
    253       (_ : err (spDiagnostic "positive equation arity" 0
    254         (sourceCoreStart (snd first))) t)
    255       (_ : lazyResult (problem tail : err problem tail)
    256         (_ tail : ok (spWrap patterns
    257           (spEquations equations (spContext patterns t (spArguments patterns)))) t)
    258         (spValidateEquations equations arity))
    259       (isZero_? arity)) equations)
    260