1993cce4a57c4225bf46d355be9436b48ceeffbcaddffd2f5e8184550f0fe7b4.tri (6185B)
1 !import prelude * 2 !import source_core * 3 !import source_pattern * 4 !export * 5 -- Opt-in compiler-IR experiment. Not imported by the canonical compiler. 6 7 -- Two authored private kinds plus compiler-only protected thunk kind 98; 8 -- all are eliminated before sourceCompileCore sees them. 9 -- Branch contains (condition, (yes body, no body)); Recur contains next state. 10 -- Step bodies address state at index 0, head at 1, outer binders from 2. 11 -- Trusted compiler-built IR only: Recur requires a list step and always 12 -- consumes its original tail. This prototype is not a public validation API. 13 stageBranch condition yes no = sourceCoreNode 96 (pair condition (pair yes no)) t t 14 stageRecur state = sourceCoreNode 97 state t t 15 16 -- A plain unused lambda binder does NOT delay a closed redex: K (loop [1]) 17 -- still computes loop [1] while constructing the tree. Make each application 18 -- depend on the force token. triage f t t token yields f on the Leaf token 19 -- supplied by lazyBool, but its function shape is unknown before that token. 20 -- This is compiler-generated dependency, not a runtime primitive/interpreter. 21 -- Shift through protected thunks as binders without exposing their bodies to 22 -- an outer guard pass. Ordinary span metadata is never used as a marker. 23 stageShift_ self node cutoff = (let kind = sourceCoreKind node in 24 let payload = sourceCorePayload node in 25 lazyBool 26 (_ : sourceCoreBound (lazyBool (_ : payload) (_ : succ payload) 27 (lt_? payload cutoff)) (sourceCoreStart node) (sourceCoreEnd node)) 28 (_ : lazyBool 29 (_ : spApp (self (fst payload) cutoff) (self (snd payload) cutoff)) 30 (_ : lazyBool 31 (_ : sourceCoreNode kind (self payload (succ cutoff)) 32 (sourceCoreStart node) (sourceCoreEnd node)) 33 (_ : lazyBool 34 (_ : sourceCoreList (map (child : self child cutoff) payload) 35 (sourceCoreStart node) (sourceCoreEnd node)) 36 (_ : node) (equal? kind sourceCoreListKind)) 37 (or? (equal? kind sourceCoreLambdaKind) (equal? kind 98))) 38 (equal? kind sourceCoreApplyKind)) 39 (equal? kind sourceCoreBoundKind)) 40 stageShift node = y stageShift_ node 0 41 stageFinish_ self node = (let kind = sourceCoreKind node in 42 let payload = sourceCorePayload node in 43 lazyBool 44 (_ : spLam (self payload)) 45 (_ : lazyBool 46 (_ : spApp (self (fst payload)) (self (snd payload))) 47 (_ : lazyBool 48 (_ : spLam (self payload)) 49 (_ : lazyBool 50 (_ : sourceCoreList (map self payload) (sourceCoreStart node) (sourceCoreEnd node)) 51 (_ : node) (equal? kind sourceCoreListKind)) 52 (equal? kind sourceCoreLambdaKind)) 53 (equal? kind sourceCoreApplyKind)) 54 (equal? kind 98)) 55 stageFinish node = y stageFinish_ node 56 stageGuard_ self node depth = (let kind = sourceCoreKind node in 57 let payload = sourceCorePayload node in 58 lazyBool 59 (_ : spApp (spApp4 (spLit triage) (self (fst payload) depth) 60 (spLit t) (spLit t) (spVar depth)) (self (snd payload) depth)) 61 (_ : lazyBool (_ : spLam (self payload (succ depth))) 62 (_ : lazyBool 63 (_ : sourceCoreList (map (child : self child depth) payload) 64 (sourceCoreStart node) (sourceCoreEnd node)) 65 (_ : node) (equal? kind sourceCoreListKind)) 66 (equal? kind sourceCoreLambdaKind)) 67 (equal? kind sourceCoreApplyKind)) 68 stageGuard node = y stageGuard_ node 0 69 -- Kind 98 is opaque to stageGuard, but stageShift traverses it as a binder. 70 -- Re-guarding inner thunks with an outer token grows nested branches badly. 71 stageThunk body = sourceCoreNode 98 (stageGuard (stageShift body)) t t 72 stageDelayBranch condition yes no = (spApp3 (spLit lazyBool) 73 (stageThunk yes) (stageThunk no) condition) 74 75 -- Syntax-driven traversal. depth counts only binders inside the supplied body. 76 -- In step mode, insert hidden tail/self captures into the user binder layout. 77 stageBody_ self node step depth = (let kind = sourceCoreKind node in 78 let payload = sourceCorePayload node in 79 lazyBool 80 (_ : stageDelayBranch (self (fst payload) step depth) 81 (self (fst (snd payload)) step depth) (self (snd (snd payload)) step depth)) 82 (_ : lazyBool 83 (_ : spApp2 (spVar (add depth 3)) (spVar (succ depth)) 84 (self payload step depth)) 85 (_ : lazyBool 86 (_ : let index = payload in spVar (lazyBool 87 (_ : index) 88 (_ : lazyBool (_ : index) 89 (_ : lazyBool (_ : succ index) (_ : add index 2) 90 (equal? index (succ depth))) (equal? index depth)) 91 (or? (not? step) (lt_? index depth)))) 92 (_ : lazyBool 93 (_ : spApp (self (fst payload) step depth) (self (snd payload) step depth)) 94 (_ : lazyBool 95 (_ : spLam (self payload step (succ depth))) 96 (_ : lazyBool 97 (_ : sourceCoreList (map (child : self child step depth) payload) 98 (sourceCoreStart node) (sourceCoreEnd node)) 99 (_ : node) (equal? kind sourceCoreListKind)) 100 (equal? kind sourceCoreLambdaKind)) 101 (equal? kind sourceCoreApplyKind)) 102 (equal? kind sourceCoreBoundKind)) 103 (equal? kind 97)) 104 (equal? kind 96)) 105 stageBody node = stageFinish (y stageBody_ node false 0) 106 stageStep node = stageFinish (y stageBody_ node true 0) 107 108 -- Explicit list gate: no inference of the consumed argument. done may read 109 -- state at index 0 but has no outer free binders. Malformed non-cons input 110 -- follows done, as in tfSlice. 111 -- The author supplies head/state code, not self, tail, y, thunks or a worker. 112 stageList done body = (lazyResult (problem rest : err problem rest) 113 (worker rest : ok (spLam (spLam (spApp2 114 (spApp (spLit y) (spShift2 worker)) (spVar 1) (spVar 0)))) t) 115 (sourceLowerEquations [ 116 (sourceEquation [(sourcePatternCapture "self" t) (sourcePatternLeaf t) 117 (sourcePatternCapture "state" t)] (stageBody done)) 118 (sourceEquation [(sourcePatternCapture "self" t) 119 (sourcePatternFork (sourcePatternCapture "head" t) (sourcePatternCapture "tail" t) t) 120 (sourcePatternCapture "state" t)] (stageStep body)) 121 (sourceEquation [(sourcePatternCapture "self" t) (sourcePatternAny t) 122 (sourcePatternCapture "state" t)] (stageBody done)) 123 ]))