tricu

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

b27f1eac18cbe8ad80cdd91f9f546b2d2a782b6cc5c5676232491b95751abe5a.tri (15572B)

      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 -- Stable abstraction keeps applications residual beneath the argument binders.
    122 -- Only the factored outer split uses this direct selector. Nested tests and
    123 -- sequential failures retain spCase/spIf and their continuation protocol.
    124 -- Leaf has no extra binder here, so do NOT shift its body as spCase does.
    125 spDirectCase leaf stem fork value = (spApp4 (spLit triage)
    126   leaf (spLam stem) (spLam (spLam fork)) value)
    127 spIf yes no condition = (spApp3 (spLit lazyBool)
    128   (spLam (spShift yes)) (spLam (spShift no)) condition)
    129 
    130 -- hit receives the updated context and shifted miss expression. A left
    131 -- child's handlers may add binders before its saved right sibling is visited.
    132 spPattern pattern value ctx hit miss = (let payload = sourcePatternPayload pattern in
    133   case sourcePatternTag pattern of
    134     0 = hit ctx miss
    135     1 = spCase (hit ctx miss) (spShift miss) (spShift2 miss) value
    136     2 = (spCase miss
    137       (spPattern payload (spVar 0) (spShiftContext ctx) hit (spShift miss))
    138       (spShift2 miss) value)
    139     3 = (spCase miss (spShift miss)
    140       (spPattern (fst payload) (spVar 1)
    141         (spSave (spShiftContext (spShiftContext ctx)) (spVar 0))
    142         (next nextMiss : spPattern (snd payload) (fst (spPending next))
    143           (spPop next) hit nextMiss)
    144         (spShift2 miss)) value)
    145     4 = hit (spBind ctx payload value) miss
    146     5 = spIf (hit ctx miss) miss (spApp2 (spLit equal?) value (spLit payload))
    147     6 = spPattern (snd payload) value (spBind ctx (fst payload) value) hit miss
    148     -- Validation admits only tags 0..7; the remaining tag is a resolved pin.
    149     _ = (spIf (hit ctx miss) miss
    150       (spApp2 (spLit equal?) value (spRaise payload (spFuel ctx)))))
    151 
    152 spArguments patterns = (lazyList (_ : t)
    153   (_ rest : pair (spVar (length rest)) (spArguments rest)) patterns)
    154 spMatchArguments patterns ctx body miss = (lazyList
    155   (_ : spBody body ctx)
    156   (pattern rest : spPattern pattern (fst (spPending ctx)) (spPop ctx)
    157     (next nextMiss : spMatchArguments rest next body nextMiss) miss) patterns)
    158 
    159 -- Sequential fallback for arbitrary ordered patterns. A final irrefutable row
    160 -- cannot miss, so it needs neither a failure binder nor a delayed empty suffix.
    161 spSequentialEquations equations ctx = (lazyList (_ : spLit t)
    162   (equation rest : lazyBool
    163     (_ : spMatchArguments (fst equation) ctx (snd equation) (spLit t))
    164     (_ : spApp
    165       (spLam (spMatchArguments (fst equation)
    166         (spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
    167       (spLam (spShift (spSequentialEquations rest ctx))))
    168     (emptyList? rest)) equations)
    169 
    170 -- Only factor a constructor test that the FIRST row must reach. All preceding
    171 -- columns must be plain captures/wildcards in EVERY row. Pins, literals and
    172 -- whole patterns at the split column conservatively retain sequential lowering.
    173 -- This is not permission to reorder tests of different arguments or children.
    174 spPlainIrrefutable pattern = (let tag = sourcePatternTag pattern in
    175   or? (equal? tag 0) (equal? tag 4))
    176 spRootPattern pattern = (let tag = sourcePatternTag pattern in
    177   or? (spPlainIrrefutable pattern)
    178     (or? (equal? tag 1) (or? (equal? tag 2) (equal? tag 3))))
    179 spFindSplit equations patterns column = (lazyList (_ : nothing)
    180   (pattern rest : lazyBool
    181     (_ : lazyBool
    182       (_ : spFindSplit equations rest (succ column))
    183       (_ : nothing)
    184       (all? (equation : spPlainIrrefutable (nth column (fst equation))) equations))
    185     (_ : lazyBool
    186       (_ : just column)
    187       (_ : nothing)
    188       (and? (spRootPattern pattern)
    189         (all? (equation : spRootPattern (nth column (fst equation))) equations)))
    190     (spPlainIrrefutable pattern)) patterns)
    191 spRootAccepts kind pattern =
    192   or? (spPlainIrrefutable pattern) (equal? kind (sourcePatternTag pattern))
    193 
    194 -- The selected constructor and its child expressions are already available.
    195 -- Child coordinates travel explicitly because a failure binder shifts them.
    196 -- Nested patterns still use ordinary left-to-right matching and saved siblings.
    197 spKnownPattern pattern children value ctx hit miss = (case sourcePatternTag pattern of
    198   1 = hit ctx miss
    199   2 = spPattern (sourcePatternPayload pattern) (fst children) ctx hit miss
    200   3 = (spPattern (fst (sourcePatternPayload pattern)) (fst children)
    201     (spSave ctx (fst (snd children)))
    202     (next nextMiss : spPattern (snd (sourcePatternPayload pattern))
    203       (fst (spPending next)) (spPop next) hit nextMiss) miss)
    204   _ = spPattern pattern value ctx hit miss)
    205 spKnownArguments patterns column children ctx body miss = (lazyList
    206   (_ : spBody body ctx)
    207   (pattern rest : lazyBool
    208     (_ : spKnownPattern pattern children (fst (spPending ctx)) (spPop ctx)
    209       (next nextMiss : spMatchArguments rest next body nextMiss) miss)
    210     (_ : spPattern pattern (fst (spPending ctx)) (spPop ctx)
    211       (next nextMiss : spKnownArguments rest (pred_ column) children next body nextMiss) miss)
    212     (isZero_? column)) patterns)
    213 spKnownIrrefutable pattern = (case sourcePatternTag pattern of
    214   1 = true
    215   2 = spIrrefutable (sourcePatternPayload pattern)
    216   3 = and? (spIrrefutable (fst (sourcePatternPayload pattern)))
    217            (spIrrefutable (snd (sourcePatternPayload pattern)))
    218   _ = spIrrefutable pattern)
    219 spKnownRowIrrefutable patterns column = (lazyList (_ : true)
    220   (pattern rest : lazyBool
    221     (_ : and? (spKnownIrrefutable pattern) (spAllIrrefutable rest))
    222     (_ : and? (spIrrefutable pattern) (spKnownRowIrrefutable rest (pred_ column)))
    223     (isZero_? column)) patterns)
    224 spKnownEquations equations column children ctx = (lazyList (_ : spLit t)
    225   (equation rest : lazyBool
    226     (_ : spKnownArguments (fst equation) column children ctx (snd equation) (spLit t))
    227     (_ : spApp
    228       (spLam (spKnownArguments (fst equation) column (map spShift children)
    229         (spShiftContext ctx) (snd equation) (spApp (spVar 0) (spLit t))))
    230       (spLam (spShift (spKnownEquations rest column children ctx))))
    231     (spKnownRowIrrefutable (fst equation) column)) equations)
    232 spSplitEquationsWith select equations column ctx = (let
    233   rows kind = filter (equation : spRootAccepts kind (nth column (fst equation))) equations
    234   stemCtx = spShiftContext ctx
    235   forkCtx = spShiftContext stemCtx
    236   in select
    237     (spKnownEquations (rows 1) column [] ctx)
    238     (spKnownEquations (rows 2) column [(spVar 0)] stemCtx)
    239     (spKnownEquations (rows 3) column [(spVar 1) (spVar 0)] forkCtx)
    240     (nth column (spPending ctx)))
    241 spEquationsWith select equations ctx = (lazyMaybe
    242   (_ : spSequentialEquations equations ctx)
    243   (column : spSplitEquationsWith select equations column ctx)
    244   (spFindSplit equations (fst (fst equations)) 0))
    245 spWrap patterns body = (lazyList (_ : body)
    246   (_ rest : spLam (spWrap rest body)) patterns)
    247 
    248 spDiagnostic expected found location = parserDiagnostic 48 expected found location t
    249 spError expected pattern = (err
    250   (spDiagnostic expected (sourcePatternTag pattern) (sourcePatternLocation pattern)) t)
    251 spHasName names name = (lazyList (_ : false)
    252   (head rest : lazyBool (_ : true) (_ : spHasName rest name) (equal? head name)) names)
    253 spIntroduce names name pattern = (lazyBool
    254   (_ : err (spDiagnostic "unique capture" name (sourcePatternLocation pattern)) t)
    255   (_ : ok (pair name names) t) (spHasName names name))
    256 spValidatePattern pattern names = (let payload = sourcePatternPayload pattern in
    257   case sourcePatternTag pattern of
    258     0 = ok names t
    259     1 = ok names t
    260     2 = spValidatePattern payload names
    261     3 = (bindResult (spValidatePattern (fst payload) names)
    262       (next _ : spValidatePattern (snd payload) next))
    263     4 = spIntroduce names payload pattern
    264     5 = ok names t
    265     6 = (bindResult (spIntroduce names (fst payload) pattern)
    266       (next _ : spValidatePattern (snd payload) next))
    267     7 = ok names t
    268     _ = spError "pattern tag" pattern)
    269 spValidateArguments patterns = (let rec
    270   validate remaining names = (lazyList (_ : ok names t)
    271     (pattern rest : bindResult (spValidatePattern pattern names)
    272       (next _ : validate rest next)) remaining)
    273   in validate patterns t)
    274 spIrrefutable pattern = case sourcePatternTag pattern of
    275   0 = true
    276   4 = true
    277   6 = spIrrefutable (snd (sourcePatternPayload pattern))
    278   _ = false
    279 spAllIrrefutable patterns = (lazyList (_ : true)
    280   (pattern rest : lazyBool (_ : spAllIrrefutable rest) (_ : false) (spIrrefutable pattern)) patterns)
    281 spValidateEquations equations arity = (lazyList
    282   (_ : err (spDiagnostic "nonempty equations" t t) t)
    283   (equation rest : lazyBool
    284     (_ : lazyResult (problem tail : err problem tail)
    285       (names tail : lazyList
    286         (_ : lazyBool (_ : ok t t)
    287           (_ : err (spDiagnostic "final irrefutable equation" t
    288             (sourceCoreStart (snd equation))) t)
    289           (spAllIrrefutable (fst equation)))
    290         (_ tail : spValidateEquations rest arity) rest)
    291       (spValidateArguments (fst equation)))
    292     (_ : err (spDiagnostic "consistent arity" (length (fst equation))
    293       (sourceCoreStart (snd equation))) t)
    294     (equal? (length (fst equation)) arity)) equations)
    295 
    296 sourceLowerEquationsWith select equations = (lazyList
    297   (_ : err (spDiagnostic "nonempty equations" t t) t)
    298   (first rest : let patterns = fst first in
    299     let arity = length patterns in
    300     lazyBool
    301       (_ : err (spDiagnostic "positive equation arity" 0
    302         (sourceCoreStart (snd first))) t)
    303       (_ : lazyResult (problem tail : err problem tail)
    304         (_ tail : ok (spWrap patterns
    305           (spEquationsWith select equations (spContext patterns t (spArguments patterns)))) t)
    306         (spValidateEquations equations arity))
    307       (isZero_? arity)) equations)
    308 
    309 
    310 -- Selection is explicit; the optimized backend retains delayed construction.
    311 sourceLowerEquations = sourceLowerEquationsWith spCase
    312 sourceLowerStableEquations = sourceLowerEquationsWith spDirectCase