tricu

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

e241dbc6ad44737d47e20cbd6ca22604a105e98f9201bf31f5ef91e304762330.tri (10782B)

      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 -- This hot visitor deliberately retains cheap tag dispatch. Patterned case
     43 -- dispatch measured ~29% more allocation on nested binder/application syntax.
     44 spShift node = (let rec
     45   shift node cutoff = (let kind = sourceCoreKind node in
     46     lazyBool
     47       (_ : lazyBool
     48         (_ : sourceCoreBound (succ (sourceCorePayload node))
     49           (sourceCoreStart node) (sourceCoreEnd node))
     50         (_ : node) (lte_? cutoff (sourceCorePayload node)))
     51       (_ : lazyBool
     52         (_ : sourceCoreApply
     53           (shift (fst (sourceCorePayload node)) cutoff)
     54           (shift (snd (sourceCorePayload node)) cutoff)
     55           (sourceCoreStart node) (sourceCoreEnd node))
     56         (_ : lazyBool
     57           (_ : sourceCoreLambda (shift (sourceCorePayload node) (succ cutoff))
     58             (sourceCoreStart node) (sourceCoreEnd node))
     59           (_ : lazyBool
     60             (_ : sourceCoreList (map (child : shift child cutoff)
     61               (sourceCorePayload node)) (sourceCoreStart node) (sourceCoreEnd node))
     62             (_ : node) (equal? kind sourceCoreListKind))
     63           (equal? kind sourceCoreLambdaKind))
     64         (equal? kind sourceCoreApplyKind))
     65       (equal? kind sourceCoreBoundKind))
     66   in shift node 0)
     67 spShift2 node = spShift (spShift node)
     68 -- Consume a syntax-derived binder list, not a numeric depth difference.
     69 spRaise node fuel = (lazyList (_ : node)
     70   (_ rest : spRaise (spShift node) rest) fuel)
     71 
     72 -- Context = (binder fuel, (reverse captures, pending argument/sibling syntax)).
     73 -- Capture aliases and pending expressions are shifted together under every
     74 -- generated binder. No counter-driven sibling raising or runtime table exists.
     75 spContext fuel captures pending = pair fuel (pair captures pending)
     76 spFuel ctx = fst ctx
     77 spDepth ctx = length (spFuel ctx)
     78 spCaptures ctx = fst (snd ctx)
     79 spPending ctx = snd (snd ctx)
     80 spShiftContext ctx = (spContext (pair t (spFuel ctx))
     81   (map (entry : pair (fst entry) (spShift (snd entry))) (spCaptures ctx))
     82   (map spShift (spPending ctx)))
     83 spBind ctx name value = (spContext (spFuel ctx)
     84   (pair (pair name value) (spCaptures ctx)) (spPending ctx))
     85 spSave ctx value = spContext (spFuel ctx) (spCaptures ctx) (pair value (spPending ctx))
     86 spPop ctx = spContext (spFuel ctx) (spCaptures ctx) (snd (spPending ctx))
     87 
     88 spCaptureAt captures index = (lazyList (_ : nothing)
     89   (entry rest : lazyBool (_ : just (snd entry))
     90     (_ : spCaptureAt rest (pred_ index)) (isZero_? index)) captures)
     91 
     92 -- Substitute resolved capture indices, preserving lambdas in the body and
     93 -- shifting outer lexical references past generated matcher binders.
     94 spBodyBound node ctx fuel = (let index = sourceCorePayload node in
     95   let cutoff = length fuel in
     96   lazyBool (_ : node)
     97     (_ : lazyMaybe
     98       (_ : sourceCoreBound
     99         (add cutoff (add (spDepth ctx)
    100           (sub (sub index cutoff) (length (spCaptures ctx)))))
    101         (sourceCoreStart node) (sourceCoreEnd node))
    102       (value : sourceCoreWithSpan (spRaise value fuel)
    103         (sourceCoreStart node) (sourceCoreEnd node))
    104       (spCaptureAt (spCaptures ctx) (sub index cutoff)))
    105     (lt_? index cutoff))
    106 spBody node ctx = (let rec
    107   substitute node fuel = (let payload = sourceCorePayload node in
    108     let start = sourceCoreStart node in
    109     let end = sourceCoreEnd node in
    110     case sourceCoreKind node of
    111       ^sourceCoreBoundKind = spBodyBound node ctx fuel
    112       ^sourceCoreApplyKind = (sourceCoreApply
    113         (substitute (fst payload) fuel) (substitute (snd payload) fuel) start end)
    114       ^sourceCoreLambdaKind = sourceCoreLambda (substitute payload (pair t fuel)) start end
    115       ^sourceCoreListKind = sourceCoreList (map (child : substitute child fuel) payload) start end
    116       _ = node)
    117   in substitute node t)
    118 
    119 spCase leaf stem fork value = (spApp4 (spLit spSelect)
    120   (spLam (spShift leaf)) (spLam stem) (spLam (spLam fork)) value)
    121 spIf yes no condition = (spApp3 (spLit lazyBool)
    122   (spLam (spShift yes)) (spLam (spShift no)) condition)
    123 
    124 -- hit receives the updated context and shifted miss expression. A left
    125 -- child's handlers may add binders before its saved right sibling is visited.
    126 spPattern pattern value ctx hit miss = (let payload = sourcePatternPayload pattern in
    127   case sourcePatternTag pattern of
    128     0 = hit ctx miss
    129     1 = spCase (hit ctx miss) (spShift miss) (spShift2 miss) value
    130     2 = (spCase miss
    131       (spPattern payload (spVar 0) (spShiftContext ctx) hit (spShift miss))
    132       (spShift2 miss) value)
    133     3 = (spCase miss (spShift miss)
    134       (spPattern (fst payload) (spVar 1)
    135         (spSave (spShiftContext (spShiftContext ctx)) (spVar 0))
    136         (next nextMiss : spPattern (snd payload) (fst (spPending next))
    137           (spPop next) hit nextMiss)
    138         (spShift2 miss)) value)
    139     4 = hit (spBind ctx payload value) miss
    140     5 = spIf (hit ctx miss) miss (spApp2 (spLit equal?) value (spLit payload))
    141     6 = spPattern (snd payload) value (spBind ctx (fst payload) value) hit miss
    142     -- Validation admits only tags 0..7; the remaining tag is a resolved pin.
    143     _ = (spIf (hit ctx miss) miss
    144       (spApp2 (spLit equal?) value (spRaise payload (spFuel ctx)))))
    145 
    146 spArguments patterns = (lazyList (_ : t)
    147   (_ rest : pair (spVar (length rest)) (spArguments rest)) patterns)
    148 spMatchArguments patterns ctx body miss = (lazyList
    149   (_ : spBody body ctx)
    150   (pattern rest : spPattern pattern (fst (spPending ctx)) (spPop ctx)
    151     (next nextMiss : spMatchArguments rest next body nextMiss) miss) patterns)
    152 
    153 -- The final equation is irrefutable, so the empty suffix is unreachable.
    154 -- One native lazy continuation shares all misses to the remaining equations.
    155 spEquations equations ctx = (lazyList (_ : spLit t)
    156   (equation rest : spApp
    157     (spLam (spMatchArguments (fst equation)
    158       (spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
    159     (spLam (spShift (spEquations rest ctx)))) equations)
    160 spWrap patterns body = (lazyList (_ : body)
    161   (_ rest : spLam (spWrap rest body)) patterns)
    162 
    163 spDiagnostic expected found location = parserDiagnostic 48 expected found location t
    164 spError expected pattern = (err
    165   (spDiagnostic expected (sourcePatternTag pattern) (sourcePatternLocation pattern)) t)
    166 spHasName names name = (lazyList (_ : false)
    167   (head rest : lazyBool (_ : true) (_ : spHasName rest name) (equal? head name)) names)
    168 spIntroduce names name pattern = (lazyBool
    169   (_ : err (spDiagnostic "unique capture" name (sourcePatternLocation pattern)) t)
    170   (_ : ok (pair name names) t) (spHasName names name))
    171 spValidatePattern pattern names = (let payload = sourcePatternPayload pattern in
    172   case sourcePatternTag pattern of
    173     0 = ok names t
    174     1 = ok names t
    175     2 = spValidatePattern payload names
    176     3 = (bindResult (spValidatePattern (fst payload) names)
    177       (next _ : spValidatePattern (snd payload) next))
    178     4 = spIntroduce names payload pattern
    179     5 = ok names t
    180     6 = (bindResult (spIntroduce names (fst payload) pattern)
    181       (next _ : spValidatePattern (snd payload) next))
    182     7 = ok names t
    183     _ = spError "pattern tag" pattern)
    184 spValidateArguments patterns = (let rec
    185   validate remaining names = (lazyList (_ : ok names t)
    186     (pattern rest : bindResult (spValidatePattern pattern names)
    187       (next _ : validate rest next)) remaining)
    188   in validate patterns t)
    189 spIrrefutable pattern = case sourcePatternTag pattern of
    190   0 = true
    191   4 = true
    192   6 = spIrrefutable (snd (sourcePatternPayload pattern))
    193   _ = false
    194 spAllIrrefutable patterns = (lazyList (_ : true)
    195   (pattern rest : lazyBool (_ : spAllIrrefutable rest) (_ : false) (spIrrefutable pattern)) patterns)
    196 spValidateEquations equations arity = (lazyList
    197   (_ : err (spDiagnostic "nonempty equations" t t) t)
    198   (equation rest : lazyBool
    199     (_ : lazyResult (problem tail : err problem tail)
    200       (names tail : lazyList
    201         (_ : lazyBool (_ : ok t t)
    202           (_ : err (spDiagnostic "final irrefutable equation" t
    203             (sourceCoreStart (snd equation))) t)
    204           (spAllIrrefutable (fst equation)))
    205         (_ tail : spValidateEquations rest arity) rest)
    206       (spValidateArguments (fst equation)))
    207     (_ : err (spDiagnostic "consistent arity" (length (fst equation))
    208       (sourceCoreStart (snd equation))) t)
    209     (equal? (length (fst equation)) arity)) equations)
    210 
    211 sourceLowerEquations equations = (lazyList
    212   (_ : err (spDiagnostic "nonempty equations" t t) t)
    213   (first rest : let patterns = fst first in
    214     let arity = length patterns in
    215     lazyBool
    216       (_ : err (spDiagnostic "positive equation arity" 0
    217         (sourceCoreStart (snd first))) t)
    218       (_ : lazyResult (problem tail : err problem tail)
    219         (_ tail : ok (spWrap patterns
    220           (spEquations equations (spContext patterns t (spArguments patterns)))) t)
    221         (spValidateEquations equations arity))
    222       (isZero_? arity)) equations)
    223