tricu

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

1d43992c04f9881c1ebd0e0ef7f6bdc735780f646a52f95b5a7fb46e14fd4f83.tri (14902B)

      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 -- Sequential fallback for arbitrary ordered patterns. A final irrefutable row
    154 -- cannot miss, so it needs neither a failure binder nor a delayed empty suffix.
    155 spSequentialEquations equations ctx = (lazyList (_ : spLit t)
    156   (equation rest : lazyBool
    157     (_ : spMatchArguments (fst equation) ctx (snd equation) (spLit t))
    158     (_ : spApp
    159       (spLam (spMatchArguments (fst equation)
    160         (spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
    161       (spLam (spShift (spSequentialEquations rest ctx))))
    162     (emptyList? rest)) equations)
    163 
    164 -- Only factor a constructor test that the FIRST row must reach. All preceding
    165 -- columns must be plain captures/wildcards in EVERY row. Pins, literals and
    166 -- whole patterns at the split column conservatively retain sequential lowering.
    167 -- This is not permission to reorder tests of different arguments or children.
    168 spPlainIrrefutable pattern = (let tag = sourcePatternTag pattern in
    169   or? (equal? tag 0) (equal? tag 4))
    170 spRootPattern pattern = (let tag = sourcePatternTag pattern in
    171   or? (spPlainIrrefutable pattern)
    172     (or? (equal? tag 1) (or? (equal? tag 2) (equal? tag 3))))
    173 spFindSplit equations patterns column = (lazyList (_ : nothing)
    174   (pattern rest : lazyBool
    175     (_ : lazyBool
    176       (_ : spFindSplit equations rest (succ column))
    177       (_ : nothing)
    178       (all? (equation : spPlainIrrefutable (nth column (fst equation))) equations))
    179     (_ : lazyBool
    180       (_ : just column)
    181       (_ : nothing)
    182       (and? (spRootPattern pattern)
    183         (all? (equation : spRootPattern (nth column (fst equation))) equations)))
    184     (spPlainIrrefutable pattern)) patterns)
    185 spRootAccepts kind pattern =
    186   or? (spPlainIrrefutable pattern) (equal? kind (sourcePatternTag pattern))
    187 
    188 -- The selected constructor and its child expressions are already available.
    189 -- Child coordinates travel explicitly because a failure binder shifts them.
    190 -- Nested patterns still use ordinary left-to-right matching and saved siblings.
    191 spKnownPattern pattern children value ctx hit miss = (case sourcePatternTag pattern of
    192   1 = hit ctx miss
    193   2 = spPattern (sourcePatternPayload pattern) (fst children) ctx hit miss
    194   3 = (spPattern (fst (sourcePatternPayload pattern)) (fst children)
    195     (spSave ctx (fst (snd children)))
    196     (next nextMiss : spPattern (snd (sourcePatternPayload pattern))
    197       (fst (spPending next)) (spPop next) hit nextMiss) miss)
    198   _ = spPattern pattern value ctx hit miss)
    199 spKnownArguments patterns column children ctx body miss = (lazyList
    200   (_ : spBody body ctx)
    201   (pattern rest : lazyBool
    202     (_ : spKnownPattern pattern children (fst (spPending ctx)) (spPop ctx)
    203       (next nextMiss : spMatchArguments rest next body nextMiss) miss)
    204     (_ : spPattern pattern (fst (spPending ctx)) (spPop ctx)
    205       (next nextMiss : spKnownArguments rest (pred_ column) children next body nextMiss) miss)
    206     (isZero_? column)) patterns)
    207 spKnownIrrefutable pattern = (case sourcePatternTag pattern of
    208   1 = true
    209   2 = spIrrefutable (sourcePatternPayload pattern)
    210   3 = and? (spIrrefutable (fst (sourcePatternPayload pattern)))
    211            (spIrrefutable (snd (sourcePatternPayload pattern)))
    212   _ = spIrrefutable pattern)
    213 spKnownRowIrrefutable patterns column = (lazyList (_ : true)
    214   (pattern rest : lazyBool
    215     (_ : and? (spKnownIrrefutable pattern) (spAllIrrefutable rest))
    216     (_ : and? (spIrrefutable pattern) (spKnownRowIrrefutable rest (pred_ column)))
    217     (isZero_? column)) patterns)
    218 spKnownEquations equations column children ctx = (lazyList (_ : spLit t)
    219   (equation rest : lazyBool
    220     (_ : spKnownArguments (fst equation) column children ctx (snd equation) (spLit t))
    221     (_ : spApp
    222       (spLam (spKnownArguments (fst equation) column (map spShift children)
    223         (spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
    224       (spLam (spShift (spKnownEquations rest column children ctx))))
    225     (spKnownRowIrrefutable (fst equation) column)) equations)
    226 spSplitEquations equations column ctx = (let
    227   rows kind = filter (equation : spRootAccepts kind (nth column (fst equation))) equations
    228   stemCtx = spShiftContext ctx
    229   forkCtx = spShiftContext stemCtx
    230   in spCase
    231     (spKnownEquations (rows 1) column [] ctx)
    232     (spKnownEquations (rows 2) column [(spVar 0)] stemCtx)
    233     (spKnownEquations (rows 3) column [(spVar 1) (spVar 0)] forkCtx)
    234     (nth column (spPending ctx)))
    235 spEquations equations ctx = (lazyMaybe
    236   (_ : spSequentialEquations equations ctx)
    237   (column : spSplitEquations equations column ctx)
    238   (spFindSplit equations (fst (fst equations)) 0))
    239 spWrap patterns body = (lazyList (_ : body)
    240   (_ rest : spLam (spWrap rest body)) patterns)
    241 
    242 spDiagnostic expected found location = parserDiagnostic 48 expected found location t
    243 spError expected pattern = (err
    244   (spDiagnostic expected (sourcePatternTag pattern) (sourcePatternLocation pattern)) t)
    245 spHasName names name = (lazyList (_ : false)
    246   (head rest : lazyBool (_ : true) (_ : spHasName rest name) (equal? head name)) names)
    247 spIntroduce names name pattern = (lazyBool
    248   (_ : err (spDiagnostic "unique capture" name (sourcePatternLocation pattern)) t)
    249   (_ : ok (pair name names) t) (spHasName names name))
    250 spValidatePattern pattern names = (let payload = sourcePatternPayload pattern in
    251   case sourcePatternTag pattern of
    252     0 = ok names t
    253     1 = ok names t
    254     2 = spValidatePattern payload names
    255     3 = (bindResult (spValidatePattern (fst payload) names)
    256       (next _ : spValidatePattern (snd payload) next))
    257     4 = spIntroduce names payload pattern
    258     5 = ok names t
    259     6 = (bindResult (spIntroduce names (fst payload) pattern)
    260       (next _ : spValidatePattern (snd payload) next))
    261     7 = ok names t
    262     _ = spError "pattern tag" pattern)
    263 spValidateArguments patterns = (let rec
    264   validate remaining names = (lazyList (_ : ok names t)
    265     (pattern rest : bindResult (spValidatePattern pattern names)
    266       (next _ : validate rest next)) remaining)
    267   in validate patterns t)
    268 spIrrefutable pattern = case sourcePatternTag pattern of
    269   0 = true
    270   4 = true
    271   6 = spIrrefutable (snd (sourcePatternPayload pattern))
    272   _ = false
    273 spAllIrrefutable patterns = (lazyList (_ : true)
    274   (pattern rest : lazyBool (_ : spAllIrrefutable rest) (_ : false) (spIrrefutable pattern)) patterns)
    275 spValidateEquations equations arity = (lazyList
    276   (_ : err (spDiagnostic "nonempty equations" t t) t)
    277   (equation rest : lazyBool
    278     (_ : lazyResult (problem tail : err problem tail)
    279       (names tail : lazyList
    280         (_ : lazyBool (_ : ok t t)
    281           (_ : err (spDiagnostic "final irrefutable equation" t
    282             (sourceCoreStart (snd equation))) t)
    283           (spAllIrrefutable (fst equation)))
    284         (_ tail : spValidateEquations rest arity) rest)
    285       (spValidateArguments (fst equation)))
    286     (_ : err (spDiagnostic "consistent arity" (length (fst equation))
    287       (sourceCoreStart (snd equation))) t)
    288     (equal? (length (fst equation)) arity)) equations)
    289 
    290 sourceLowerEquations equations = (lazyList
    291   (_ : err (spDiagnostic "nonempty equations" t t) t)
    292   (first rest : let patterns = fst first in
    293     let arity = length patterns in
    294     lazyBool
    295       (_ : err (spDiagnostic "positive equation arity" 0
    296         (sourceCoreStart (snd first))) t)
    297       (_ : lazyResult (problem tail : err problem tail)
    298         (_ tail : ok (spWrap patterns
    299           (spEquations equations (spContext patterns t (spArguments patterns)))) t)
    300         (spValidateEquations equations arity))
    301       (isZero_? arity)) equations)
    302