cd10e622fe9175a69148056134e5106bb7ce1527ed021b2d74b79e6cf7c89466.tri (8330B)
1 !import base as B 2 !import io as HostIO 3 !export pure 4 !export bind 5 !export request 6 !export checkedRequest 7 !export checkWith 8 !export checkRequest 9 !export handle 10 !export forward 11 !export label 12 !export fail 13 !export liftIO 14 !export runPure 15 !export runIO 16 !export collect 17 !export view 18 !export diagnostic 19 !export scope 20 !export spawn 21 22 -- Request/response effects. Handler callbacks return computations yielding one 23 -- reply. liftIO bridges host actions into this protocol. 24 pure value = B.pair 100 value 25 bind action next = B.pair 101 (B.pair action next) 26 request service operation argument = B.pair 102 (B.pair [service operation argument] pure) 27 handle service handler action = B.pair 104 (B.pair [service handler] action) 28 label name action = B.pair 105 (B.pair [name] action) 29 fail kind service operation detail = B.pair 103 [kind service operation detail] 30 31 -- Handlers execute outside their own installation scope, so forwarding is an 32 -- ordinary request there. At other call sites it uses the current environment. 33 -- Service names select routes; host operations use OS process authority. 34 forward = request 35 liftIO action = request "host.io" "run" action 36 37 -- Boundary constructors snapshot the actual lexical environment during 38 -- normalization, including when invoked inside a handler callback. 39 -- Child frames start empty; immutable routing and label values are inherited. 40 scope body = B.pair 107 body 41 spawn supervised keep handles body = B.pair 108 [supervised keep handles body] 42 43 -- Diagnostics are data: kind, service, operation, detail, outer-to-inner labels. 44 diagnostic kind service operation detail labels = [kind service operation detail labels] 45 46 -- Check once, then select one continuation. Success passes the checked value; 47 -- rejection passes its diagnostic; a malformed reply passes the original value. 48 -- Each continuation owns its outcome policy and only the selected one runs. 49 checkWith contract value rejected malformed next = case B.checkContract contract value of 50 ((t t), (checked, t)) = next checked 51 (t, (message, _)) = rejected message 52 _ = malformed value 53 54 -- Request-boundary policy carries routing details into handler diagnostics. 55 checkRequest service operation contract argument = checkWith contract argument 56 (message : fail "invalid-request" service operation message) 57 (original : fail "invalid-request-contract" service operation original) 58 59 checkedRequest service operation inputC outputC argument = 60 checkRequest service operation inputC argument (checked : do bind 61 reply <- request service operation checked 62 checkWith outputC reply 63 (message : fail "invalid-response" service operation message) 64 (original : fail "invalid-response-contract" service operation original) 65 pure) 66 67 findHandler wanted [[service handler] | outer] = B.lazyBool 68 (_ : B.pair handler outer) 69 (_ : findHandler wanted outer) 70 (B.equal? wanted service) 71 findHandler _ _ = t 72 73 -- Normalized views: 100 value; 103 complete diagnostic; 106 ([service op arg], 74 -- outer-to-inner labels, reply continuation). View stops at the first request. 75 -- Frames retain caller environments and labels; handlers use the environment 76 -- suffix outside their installation, but keep the requesting execution's labels. 77 normalize action environment frames labels = let 78 broken = B.pair 103 (diagnostic "invalid-computation" t t t labels) 79 resume value [] = pure value 80 -- Force the popped stack tail's outer constructor before reusing it. A lazy 81 -- projection here can keep consumed frames (and their old chunks) reachable. 82 resume value [[saved savedLabels next] | rest] = case rest of 83 [] = normalize (next value) saved [] savedLabels 84 more{[_ | _]} = normalize (next value) saved more savedLabels 85 _ = broken 86 resume _ _ = broken 87 dispatch event{[service operation argument]} next = case findHandler service environment of 88 (handler, outer) = normalize (handler operation argument) outer 89 (B.pair [environment labels next] frames) labels 90 _ = B.pair 106 [event labels (reply : normalize (next reply) environment frames labels)] 91 dispatch _ _ = broken 92 in case action of 93 (100, value) = resume value frames 94 (101, (first, next)) = normalize first environment (B.pair [environment labels next] frames) labels 95 (102, (event, next)) = dispatch event next 96 (103, [kind service operation detail]) = B.pair 103 (diagnostic kind service operation detail labels) 97 (104, (entry{[service handler]}, body)) = normalize body (B.pair entry environment) 98 (B.pair [environment labels pure] frames) labels 99 (105, (extraLabels, body)) = normalize body environment 100 (B.pair [environment labels pure] frames) (B.append labels extraLabels) 101 (107, body) = B.pair 107 [labels 102 (owner : normalize (body owner) environment [] labels) 103 (reply : resume reply frames)] 104 (108, [supervised keep handles body]) = B.pair 108 [supervised keep handles labels 105 (fresh : normalize (body fresh) environment [] labels) 106 (reply : resume reply frames)] 107 _ = broken 108 109 view action = normalize action [] [] [] 110 111 -- Execution Result is distinct from an operation's ordinary Result value. 112 -- Pure interpretation rejects every unhandled request, including host IO. 113 runPure action = case view action of 114 (100, value) = B.ok value t 115 (103, problem) = B.err problem t 116 (106, [[service operation argument] labels next]) = B.err 117 (diagnostic "unhandled-request" service operation argument labels) t 118 _ = B.err (diagnostic "invalid-view" t t t []) t 119 120 -- Handler failures become terminal outcomes. Ordinary service Results remain 121 -- values. Labels/continuations stay lazy; only the label list spine is checked. 122 runHost current = case current of 123 (100, value) = HostIO.pure value 124 (103, problem) = HostIO.fail problem 125 (106, [["host.io" "run" action] labels next]) = case B.checkContract (B.listOf B.anyC) labels of 126 ((t t), _) = HostIO.bind action (reply : runHost (next reply)) 127 _ = HostIO.fail (diagnostic "invalid-view" t t t []) 128 (106, [[service operation argument] labels next]) = HostIO.fail 129 (diagnostic "unhandled-request" service operation argument labels) 130 (107, [labels body next]) = case B.checkContract (B.listOf B.anyC) labels of 131 ((t t), _) = HostIO.bind (HostIO.scope (owner : runHost (body owner))) 132 (reply : runHost (next reply)) 133 _ = HostIO.fail (diagnostic "invalid-view" t t t []) 134 (108, [supervised keep handles labels body next]) = case B.checkContract (B.listOf B.anyC) labels of 135 ((t t), _) = HostIO.bind (HostIO.spawn supervised keep handles (fresh : runHost (body fresh))) 136 (reply : runHost (next reply)) 137 _ = HostIO.fail (diagnostic "invalid-view" t t t []) 138 _ = HostIO.fail (diagnostic "invalid-view" t t t []) 139 runIO action = runHost (view action) 140 141 -- Collection threads its accumulator through a boundary transformer. 142 -- Inner handlers run first. Other residual requests are relayed to outer 143 -- handlers, with their labels scoped ONLY around the forwarded request. 144 -- It returns [value chronological-events]. Failures retain their labels. 145 collect service operation argumentC reply action = let rec 146 walk current reversed = case current of 147 (100, value) = pure [value (B.reverse reversed)] 148 (103, [kind failedService failedOperation detail labels]) = B.pair 105 149 (B.pair labels (fail kind failedService failedOperation detail)) 150 (106, [event{[wanted op argument]} labels next]) = B.lazyBool 151 (_ : case B.checkContract argumentC argument of 152 ((t t), (checked, t)) = walk (next reply) (B.pair checked reversed) 153 (t, (message, _)) = B.pair 105 (B.pair labels (fail "invalid-request" service operation message)) 154 _ = B.pair 105 (B.pair labels (fail "invalid-request-contract" service operation argument))) 155 (_ : bind (B.pair 105 (B.pair labels (request wanted op argument))) 156 (answer : walk (next answer) reversed)) 157 (B.and? (B.equal? wanted service) (B.equal? op operation)) 158 (107, [labels body next]) = B.pair 105 (B.pair labels 159 (fail "state-boundary" service operation "Install collection inside the scoped body")) 160 (108, [supervised keep handles labels body next]) = B.pair 105 (B.pair labels 161 (fail "state-boundary" service operation "Install child-local collection explicitly")) 162 _ = fail "invalid-view" t t t 163 in walk (view action) []