lexical-worker.tri (20180B)
1 !import prelude * 2 !import source_core as C 3 !import source_compile as K 4 !import consumers_pattern_slots as Slots 5 !import consumers_validate as V 6 !import consumers_structural as S 7 !export * 8 -- Validated lexical SCP compiler. Source patterns/templates are consumed 9 -- only while building core syntax; the residual TC worker has neither a 10 -- capture list nor a matcher/template interpreter. Effects stay at the edge. 11 12 lLit value = C.sourceCoreExternal value t t 13 lVar index = C.sourceCoreBound index t t 14 lApp function argument = C.sourceCoreApply function argument t t 15 lLam body = C.sourceCoreLambda body t t 16 lApp2 f a b = lApp (lApp f a) b 17 lApp3 f a b c = lApp (lApp2 f a b) c 18 lApp4 f a b c d = lApp (lApp3 f a b c) d 19 lApp5 f a b c d e = lApp (lApp4 f a b c d) e 20 21 -- Executable worker v1: tagged (initial state, open CPS entry). 22 -- The entry is (input, state, success, failure). This is a calling 23 -- convention, not a proof that an arbitrary tree is executable code. Shape 24 -- checking rejects accidental nonworkers at invocation boundaries; it is not 25 -- an authenticity or callable-code check. Only prepared/linked descriptors 26 -- are trusted as executable workers; a forged tagged tree is outside the ABI. 27 lWorkerTag = "scp-worker.v1" 28 lWorker state entry = pair lWorkerTag (pair state entry) 29 lWorkerShape? worker = (lazyBool 30 (_ : lazyBool (_ : equal? (fst worker) lWorkerTag) 31 (_ : false) (lIsPair (snd worker))) 32 (_ : false) (lIsPair worker)) 33 lInvokeOpen worker input state success failure = (lazyBool 34 (_ : (snd (snd worker)) input state success failure) 35 (_ : failure "invalid SCP worker") (lWorkerShape? worker)) 36 -- A closed call checks the descriptor once. Delegating to lInvokeOpen here 37 -- would repeat the same tag/shape scan on every call. 38 lInvokeClosed worker input success failure = (lazyBool 39 (_ : (snd (snd worker)) input (fst (snd worker)) success failure) 40 (_ : failure "invalid SCP worker") (lWorkerShape? worker)) 41 42 -- Syntax shifting is driven by syntax, never by unknown runtime trees. 43 lShift_ self node cutoff = (lazyBool 44 (_ : lazyBool (_ : lVar (succ (C.sourceCorePayload node))) 45 (_ : node) (lte_? cutoff (C.sourceCorePayload node))) 46 (_ : lazyBool (_ : lApp (self (fst (C.sourceCorePayload node)) cutoff) 47 (self (snd (C.sourceCorePayload node)) cutoff)) 48 (_ : lazyBool (_ : lLam (self (C.sourceCorePayload node) (succ cutoff))) 49 (_ : node) (equal? (C.sourceCoreKind node) C.sourceCoreLambdaKind)) 50 (equal? (C.sourceCoreKind node) C.sourceCoreApplyKind)) 51 (equal? (C.sourceCoreKind node) C.sourceCoreBoundKind)) 52 lShift node = y lShift_ node 0 53 lShift2 node = lShift (lShift node) 54 lShift3 node = lShift (lShift2 node) 55 lShiftEntry entry = pair (fst entry) (lShift (snd entry)) 56 -- ctx = (lexical slots, (binder depth, (self, (input, (state, (success, failure)))))) 57 -- Depth is compile-time metadata only; no depth counter survives in the worker. 58 lContext slots depth self input state success failure = pair slots (pair depth (pair self (pair input (pair state (pair success failure))))) 59 lSlots ctx = fst ctx 60 lDepth ctx = fst (snd ctx) 61 lSelf ctx = fst (snd (snd ctx)) 62 lInput ctx = fst (snd (snd (snd ctx))) 63 lState ctx = fst (snd (snd (snd (snd ctx)))) 64 lSuccess ctx = fst (snd (snd (snd (snd (snd ctx))))) 65 lFailure ctx = snd (snd (snd (snd (snd (snd ctx))))) 66 lWithSuccess ctx success = (lContext (lSlots ctx) (lDepth ctx) 67 (lSelf ctx) (lInput ctx) (lState ctx) success (lFailure ctx)) 68 lShiftContext ctx = (lContext (map lShiftEntry (lSlots ctx)) (succ (lDepth ctx)) 69 (lShift (lSelf ctx)) (lShift (lInput ctx)) (lShift (lState ctx)) 70 (lShift (lSuccess ctx)) (lShift (lFailure ctx))) 71 lBind ctx name value = (lContext (pair (pair name value) (lSlots ctx)) (lDepth ctx) 72 (lSelf ctx) (lInput ctx) (lState ctx) (lSuccess ctx) (lFailure ctx)) 73 -- A nested left pattern can introduce binders before its sibling is visited. 74 -- Raise the saved sibling expression by that exact lexical depth difference. 75 lRaise_ self depth target value = (lazyBool (_ : value) 76 (_ : self (succ depth) target (lShift value)) (equal? depth target)) 77 lRaise depth target value = y lRaise_ depth target value 78 lFind_ self entries name = (lazyList (_ : lLit t) 79 (entry rest : lazyBool (_ : snd entry) (_ : self rest name) 80 (equal? (fst entry) name)) entries) 81 lFind entries name = y lFind_ entries name 82 83 -- A literal-Fork spine ending in Capture is ordinary structural IR. Compile 84 -- that shape to a shared scanner rather than duplicating a nested decision 85 -- tree for every byte. No prefix-specific source pattern or IR tag survives. 86 lPrefixShape_ self pattern reversed = (matchPair (tag payload : 87 lazyBool 88 (_ : lazyList (_ : nothing) 89 (_ _ : just (pair (reverse reversed) payload)) reversed) 90 (_ : lazyBool 91 (_ : matchPair (headPattern tailPattern : 92 matchPair (headTag headValue : 93 lazyBool (_ : self tailPattern (pair headValue reversed)) 94 (_ : nothing) (equal? headTag 5)) headPattern) payload) 95 (_ : nothing) (equal? tag 3)) 96 (equal? tag 4)) pattern) 97 lPrefixShape pattern = y lPrefixShape_ pattern t 98 -- The scanner consumes the runtime input before recursion. The prefix is a 99 -- known literal extracted from authored IR at compile time. 100 lPrefixRest_ self input prefix = (lazyList 101 (_ : lazyList (_ : just t) (_ _ : nothing) prefix) 102 (ih ir : lazyList (_ : just input) 103 (ph pr : lazyBool (_ : self ir pr) (_ : nothing) (equal? ih ph)) prefix) 104 input) 105 lPrefixRest prefix input = y lPrefixRest_ input prefix 106 107 -- Generic ordered structural match. The miss branch is the *next rule*. 108 lCase leafCase stemCase forkCase value = lApp4 (lLit triage) leafCase stemCase forkCase value 109 lIf yes no flag = (lApp3 (lLit lazyBool) (lLam (lShift yes)) 110 (lLam (lShift no)) flag) 111 lPrefix prefix slot value ctx hit miss = (lApp3 (lLit lazyMaybe) 112 (lLam (lShift miss)) 113 (lLam (hit (lBind (lShiftContext ctx) slot (lVar 0)) (lShift miss))) 114 (lApp2 (lLit lPrefixRest) (lLit prefix) value)) 115 lPattern_ self pattern value ctx hit miss = (lazyMaybe 116 (_ : matchPair (tag payload : 117 lazyBool (_ : hit ctx miss) 118 (_ : lazyBool (_ : lCase (hit ctx miss) (lLam (lShift miss)) 119 (lLam (lLam (lShift2 miss))) value) 120 (_ : lazyBool (_ : lCase miss 121 (lLam (self payload (lVar 0) (lShiftContext ctx) hit (lShift miss))) 122 (lLam (lLam (lShift2 miss))) value) 123 (_ : lazyBool (_ : matchPair (left right : lCase miss (lLam (lShift miss)) 124 (lLam (lLam (self left (lVar 1) (lShiftContext (lShiftContext ctx)) 125 (next nextMiss : self right 126 (lRaise (lDepth (lShiftContext (lShiftContext ctx))) 127 (lDepth next) (lVar 0)) next hit nextMiss) 128 (lShift2 miss)))) value) payload) 129 (_ : lazyBool (_ : hit (lBind ctx payload value) miss) 130 (_ : lazyBool (_ : lIf (hit ctx miss) miss 131 (lApp2 (lLit equal?) (lLit payload) value)) 132 (_ : lazyBool 133 (_ : matchPair (name child : self child value 134 (lBind ctx name value) hit miss) payload) 135 (_ : miss) 136 (equal? tag 6)) 137 (equal? tag 5)) (equal? tag 4)) (equal? tag 3)) 138 (equal? tag 2)) (equal? tag 1)) (equal? tag 0)) pattern) 139 (prefixSlot : lPrefix (fst prefixSlot) (snd prefixSlot) value ctx hit miss) 140 (lPrefixShape pattern)) 141 lPattern pattern value ctx hit miss = y lPattern_ pattern value ctx hit miss 142 143 -- Each output is CPS-translated at compile time. Every newly introduced 144 -- value is a native lambda binder, not an entry in a runtime capture list. 145 lBinary self left right ctx success operation = (self left ctx (lLam (self right (lShiftContext ctx) 146 (lLam (lApp (lShift2 success) (lApp2 (lLit operation) (lVar 1) (lVar 0))))))) 147 lEmitRecur self nextInput nextState ctx success = (self nextInput ctx (lLam (self nextState (lShiftContext ctx) 148 (lLam (lApp4 (lShift2 (lSelf ctx)) (lVar 1) (lVar 0) 149 (lShift2 success) (lShift2 (lFailure ctx))))))) 150 lEmitCall self worker argument slot receiver ctx success = (self worker ctx (lLam (self argument (lShiftContext ctx) 151 (lLam (lApp4 (lLit lInvokeClosed) (lVar 1) (lVar 0) 152 (lLam (self receiver 153 (lBind (lShiftContext (lShiftContext (lShiftContext ctx))) 154 slot (lVar 0)) (lShift (lShift2 success)))) 155 (lShift2 (lFailure ctx))))))) 156 -- Tail delegation does not install a return receiver or restore either 157 -- worker's initial state. The caller's continuations pass straight through. 158 lEmitBecome self worker argument nextState ctx success = (self worker ctx 159 (lLam (self argument (lShiftContext ctx) 160 (lLam (self nextState (lShiftContext (lShiftContext ctx)) 161 (lLam (lApp5 (lLit lInvokeOpen) (lVar 2) (lVar 1) (lVar 0) 162 (lShift3 success) (lShift3 (lFailure ctx))))))))) 163 -- Share one lazy next-arm continuation, just as rule matching does. 164 lMatchArms_ self output arms value ctx = (lazyList 165 (_ : lApp (lFailure ctx) (lLit "no matching output arm")) 166 (arm rest : matchPair (pattern body : 167 lApp (lLam (lPattern pattern (lShift value) (lShiftContext ctx) 168 (ready nextMiss : output body ready (lSuccess ready)) 169 (lApp (lVar 0) (lLit t)))) 170 (lLam (lShift (self output rest value ctx)))) arm) arms) 171 lMatchArms output arms value ctx = y lMatchArms_ output arms value ctx 172 -- Recognize only the exact two-arm Boolean match. Fixed-format inspection 173 -- happens during compilation, never on a runtime scrutinee or arm list. 174 lBooleanArms arms = (lazyList (_ : nothing) (first rest : 175 lazyList (_ : nothing) (second tail : 176 lazyList (_ : matchPair (noPattern no : matchPair (yesPattern yes : 177 lazyBool (_ : just (pair no yes)) (_ : nothing) 178 (and? (equal? noPattern S.patLeaf) 179 (equal? yesPattern (S.patStem S.patLeaf)))) second) first) 180 (_ _ : nothing) tail) rest) arms) 181 lNoMatch ctx = lApp (lFailure ctx) (lLit "no matching output arm") 182 -- This is a lowering of the generic match, not a second Boolean semantics. 183 -- A noncanonical stem or a fork reaches the same missing-arm failure. 184 lMatchBoolean output no yes value ctx = (lCase 185 (output no ctx (lSuccess ctx)) 186 (lLam (lCase 187 (output yes (lShiftContext ctx) (lSuccess (lShiftContext ctx))) 188 (lLam (lNoMatch (lShiftContext (lShiftContext ctx)))) 189 (lLam (lLam (lNoMatch (lShiftContext 190 (lShiftContext (lShiftContext ctx)))))) 191 (lVar 0))) 192 (lLam (lLam (lNoMatch (lShiftContext (lShiftContext ctx))))) 193 value) 194 -- Matching inside another output must resume that output's continuation, 195 -- not return directly from the enclosing worker. The context carries the 196 -- continuation through pattern binders and the shared next-arm thunk. 197 lEmitMatch self source arms ctx success = (self source ctx 198 (lLam (lazyMaybe 199 (_ : lMatchArms self arms (lVar 0) 200 (lWithSuccess (lShiftContext ctx) (lShift success))) 201 (branches : lMatchBoolean self (fst branches) (snd branches) 202 (lVar 0) (lWithSuccess (lShiftContext ctx) (lShift success))) 203 (lBooleanArms arms)))) 204 lOutput_ self output ctx success = (matchPair (tag payload : 205 lazyBool (_ : lApp success (lLit payload)) 206 (_ : lazyBool (_ : lApp success (lFind (lSlots ctx) payload)) 207 (_ : lazyBool (_ : matchPair (left right : lBinary self left right ctx success pair) payload) 208 (_ : lazyBool (_ : matchPair (nextInput nextState : 209 lEmitRecur self nextInput nextState ctx success) payload) 210 (_ : lazyBool (_ : matchPair (worker more : matchPair 211 (argument continuation : matchPair (slot receiver : 212 lEmitCall self worker argument slot receiver ctx success) 213 continuation) more) payload) 214 (_ : lazyBool (_ : self payload ctx 215 (lLam (lApp (lShift success) (lApp (lLit t) (lVar 0))))) 216 (_ : lazyBool (_ : matchPair (worker more : matchPair 217 (argument nextState : lEmitBecome self worker argument nextState 218 ctx success) more) payload) 219 (_ : lazyBool (_ : matchPair (left right : 220 lBinary self left right ctx success equal?) payload) 221 (_ : lazyBool 222 (_ : matchPair (source arms : 223 lEmitMatch self source arms ctx success) payload) 224 (_ : lLit t) (equal? tag 9)) 225 (equal? tag 8)) (equal? tag 6)) 226 (equal? tag 5)) (equal? tag 4)) (equal? tag 3)) 227 (equal? tag 2)) (equal? tag 1)) (equal? tag 0)) output) 228 lOutput output ctx success = y lOutput_ output ctx success 229 230 -- Backend capability checks stay separate from authored-IR validation. 231 -- Every reference pattern/output form currently has a direct lexical lowering. 232 lIsPair value = triage false (_ : false) (_ _ : true) value 233 lValidPatternPair self payload = (lazyBool 234 (_ : matchPair (a b : andLazy? (self a) (_ : self b)) payload) 235 (_ : false) (lIsPair payload)) 236 lValidPatternAs self payload = (lazyBool 237 (_ : matchPair (name child : self child) payload) 238 (_ : false) (lIsPair payload)) 239 lValidPattern_ self pattern = (lazyBool 240 (_ : matchPair (tag payload : 241 lazyBool (_ : true) (_ : lazyBool (_ : true) 242 (_ : lazyBool (_ : self payload) 243 (_ : lazyBool (_ : lValidPatternPair self payload) 244 (_ : lazyBool (_ : true) (_ : lazyBool (_ : true) 245 (_ : lazyBool (_ : lValidPatternAs self payload) 246 (_ : false) (equal? tag 6)) (equal? tag 5)) (equal? tag 4)) 247 (equal? tag 3)) (equal? tag 2)) (equal? tag 1)) (equal? tag 0)) pattern) 248 (_ : false) (lIsPair pattern)) 249 lValidPattern pattern = y lValidPattern_ pattern 250 lHasSlot_ self slots name = (lazyList (_ : false) 251 (slot rest : or? (equal? slot name) (self rest name)) slots) 252 lHasSlot slots name = y lHasSlot_ slots name 253 lValidOutputPair self payload slots = (lazyBool 254 (_ : matchPair (a b : andLazy? (self a slots) (_ : self b slots)) payload) 255 (_ : false) (lIsPair payload)) 256 lValidOutputCall self payload slots = (lazyBool 257 (_ : matchPair (worker more : lazyBool 258 (_ : matchPair (argument continuation : lazyBool 259 (_ : matchPair (name receiver : andLazy? (self worker slots) 260 (_ : andLazy? (self argument slots) 261 (_ : self receiver (pair name slots)))) continuation) 262 (_ : false) (lIsPair continuation)) more) 263 (_ : false) (lIsPair more)) payload) 264 (_ : false) (lIsPair payload)) 265 lValidOutputBecome self payload slots = (lazyBool 266 (_ : matchPair (worker more : lazyBool 267 (_ : matchPair (argument state : andLazy? (self worker slots) 268 (_ : andLazy? (self argument slots) (_ : self state slots))) more) 269 (_ : false) (lIsPair more)) payload) 270 (_ : false) (lIsPair payload)) 271 lValidMatchArms_ self arms slots output = (lazyList 272 (_ : true) 273 (arm rest : andLazy? 274 (matchPair (pattern body : andLazy? (lValidPattern pattern) 275 (_ : output body (Slots.patternSlots pattern slots))) arm) 276 (_ : self rest slots output)) arms) 277 lValidMatchArms arms slots output = y lValidMatchArms_ arms slots output 278 lValidOutputMatch self payload slots = (lazyBool 279 (_ : matchPair (source arms : andLazy? (self source slots) 280 (_ : lValidMatchArms arms slots self)) payload) 281 (_ : false) (lIsPair payload)) 282 lValidOutput_ self output slots = (lazyBool 283 (_ : matchPair (tag payload : 284 lazyBool (_ : true) (_ : lazyBool (_ : lHasSlot slots payload) 285 (_ : lazyBool (_ : lValidOutputPair self payload slots) 286 (_ : lazyBool (_ : lValidOutputPair self payload slots) 287 (_ : lazyBool (_ : lValidOutputCall self payload slots) 288 (_ : lazyBool (_ : self payload slots) 289 (_ : lazyBool (_ : lValidOutputBecome self payload slots) 290 (_ : lazyBool (_ : lValidOutputPair self payload slots) 291 (_ : lazyBool (_ : lValidOutputMatch self payload slots) 292 (_ : false) (equal? tag 9)) 293 (equal? tag 8)) (equal? tag 6)) 294 (equal? tag 5)) (equal? tag 4)) (equal? tag 3)) 295 (equal? tag 2)) (equal? tag 1)) (equal? tag 0)) output) 296 (_ : false) (lIsPair output)) 297 lValidOutput output slots = y lValidOutput_ output slots 298 -- Authored IR is already structurally validated before this check. A failed 299 -- rule here is a lexical-backend capability gap, not malformed source. 300 lUnsupported index path = err (V.vDiagnostic 301 "unsupported" index path "lexical worker capability") t 302 lCheckBackendRule rule index = matchPair (input more : matchPair 303 (state output : lazyBool 304 (_ : lazyBool 305 (_ : lazyBool (_ : ok t t) (_ : lUnsupported index ["output"]) 306 (lValidOutput output (Slots.patternSlots state (Slots.patternSlots input t)))) 307 (_ : lUnsupported index ["state pattern"]) (lValidPattern state)) 308 (_ : lUnsupported index ["input pattern"]) (lValidPattern input)) more) rule 309 lCheckBackend_ self rules index = (lazyList 310 (_ : ok t t) 311 (rule rest : bindResult (lCheckBackendRule rule index) 312 (_ _ : self rest (succ index))) rules) 313 lCheckBackend rules = y lCheckBackend_ rules 0 314 315 lRules_ self rules ctx = (lazyList (_ : lApp (lFailure ctx) (lLit "no matching consumer rule")) 316 (rule rest : matchPair (inputPattern more : matchPair 317 (statePattern output : 318 -- One lazy next-rule thunk is shared by all misses within this rule. 319 -- Do not copy the rest of the generated rule chain per pattern branch. 320 lApp (lLam (lPattern inputPattern (lInput (lShiftContext ctx)) 321 (lShiftContext ctx) 322 (bound nextRule : lPattern statePattern (lState bound) bound 323 (ready nextMiss : lOutput output ready (lSuccess ready)) nextRule) 324 (lApp (lVar 0) (lLit t)))) 325 (lLam (lShift (self rest ctx)))) more) rule) rules) 326 lRules rules ctx = y lRules_ rules ctx 327 328 -- The fixed point lives under compile, not in a top-level constant. 329 lLoop consumer = (lApp (lLit y) 330 (lLam (lLam (lLam (lLam (lLam (lRules (snd consumer) 331 (lContext t 0 (lVar 4) (lVar 3) (lVar 2) (lVar 1) (lVar 0))))))))) 332 lCompileWith backend consumer = bindResult (V.vValidate consumer) (accepted _ : 333 bindResult (lCheckBackend (snd accepted)) (_ _ : 334 bindResult (backend (lCoreOpen accepted)) (entry _ : 335 ok (lWorker (fst accepted) entry) t))) 336 lCompile consumer = lCompileWith K.sourceCompileCore consumer 337 lCompileKiselyov consumer = lCompileWith K.sourceCompileCoreKiselyov consumer 338 lRunChecked worker input = (lInvokeClosed worker input 339 (value : ok value t) (message : err message t)) 340 341 -- One open-state CPS entry is compiled for both pure calls and effect 342 -- receivers. Only the descriptor carries the default initial state; the 343 -- effect driver supplies explicit state for each resumption. 344 lCoreOpen consumer = lLam (lLam (lLam (lLam 345 (lApp4 (lLoop consumer) (lVar 3) (lVar 2) (lVar 1) (lVar 0))))) 346 -- Kept as a named entry point for existing effect clients. It now returns 347 -- the same descriptor as lCompile; the driver supplies explicit state. 348 lCompileOpenWith backend consumer = lCompileWith backend consumer 349 lCompileOpen consumer = lCompileOpenWith K.sourceCompileCore consumer 350 lCompileOpenKiselyov consumer = lCompileOpenWith K.sourceCompileCoreKiselyov consumer 351 lRunOpenChecked worker input state = (lInvokeOpen worker input state 352 (value : ok value t) (message : err message t)) 353 -- Generic adapter for E.run: its existing per-resumption environment is fst. 354 lEffectStep program input = lRunOpenChecked (snd program) input (fst program) 355 356 -- Preparation checks a proper receiver table and each executable descriptor. 357 -- Prepared invocation uses compiler-produced or trusted linked entries with 358 -- explicit state; success and worker failures retain the standard Result ABI. 359 lPrepareEffectReceivers_ self rows = (triage (ok t t) 360 (_ : err "improper prepared receiver table" t) 361 (row rest : lazyBool 362 (_ : lazyBool 363 (_ : lazyBool 364 (_ : bindResult (self rest) (prepared _ : ok (pair row prepared) t)) 365 (_ : err (pair "invalid prepared worker" (fst row)) t) 366 (lWorkerShape? (snd (snd row)))) 367 (_ : err "invalid prepared consumer" t) (lIsPair (snd row))) 368 (_ : err "invalid prepared receiver row" t) (lIsPair row)) rows) 369 lPrepareEffectReceivers rows = y lPrepareEffectReceivers_ rows 370 lPreparedEffectStep program input = ((snd (snd (snd program))) input (fst program) 371 (value : ok value t) (message : err message t))