f013ecf3a86f12c9cf5a2bd19d693242488cebf38650842de03c7d44dc573167.tri (19133B)
1 !import prelude * 2 !import parser * 3 !import source_resolve * 4 !import source_core * 5 !export * 6 7 -- Shared residual syntax for the retained bracket strategies and the 8 -- dependency-aware Kiselyov strategy. Applications are *syntax* here; 9 -- sourceRunTerm alone performs Tree Calculus application. 10 sourceTermNode kind payload location = pair kind (pair payload location) 11 sourceTermKind term = fst term 12 sourceTermPayload term = fst (snd term) 13 sourceTermLocation term = snd (snd term) 14 sourceTermLiteral tree location = sourceTermNode 1 tree location 15 sourceTermVariable index location = sourceTermNode 2 index location 16 sourceTermApply function argument location = 17 sourceTermNode 3 (pair function argument) location 18 sourceTermInvalid core location = sourceTermNode 4 core location 19 20 sourceCombS = t (t (t t t)) t 21 sourceCombK = t t 22 sourceCombI = t (t (t t)) t 23 -- Johannes Bader's star_skibc_op_eta selects B/C when only one application 24 -- child uses the binder, and contracts the direct eta case. These are the 25 -- same tree combinators used by the bootstrap frontend, not host intrinsics. 26 sourceCombB = t (t (t t (t (t (t t t)) t))) (t t) 27 sourceCombC = (t (t (t (t (t t (t (t (t t t)) t))) (t (t (t t (t t))) (t (t (t t t)) t)))) (t t (t t))) 28 sourceCombT = sourceCombC sourceCombI 29 -- R is derived from Bader's star_ski_eta bird definition (MIT license), 30 -- rather than the longer equivalent tree used by the bootstrap frontend. 31 sourceCombR = t (t (t (t) (t (t (t (t (t (t) (t))) (t)))))) (t (t (t (t) (t (t)))) (t (t))) 32 33 -- Bracket abstraction of one de Bruijn binder. Variables beyond index zero 34 -- become variables at index n-1, for the surrounding lambda to eliminate. 35 sourceBracket_ self term = 36 lazyBool 37 (_ : sourceTermApply 38 (sourceTermLiteral sourceCombK (sourceTermLocation term)) term 39 (sourceTermLocation term)) 40 (_ : lazyBool 41 (_ : lazyBool 42 (_ : sourceTermLiteral sourceCombI (sourceTermLocation term)) 43 (_ : sourceTermApply 44 (sourceTermLiteral sourceCombK (sourceTermLocation term)) 45 (sourceTermVariable (pred_ (sourceTermPayload term)) 46 (sourceTermLocation term)) 47 (sourceTermLocation term)) 48 (isZero_? (sourceTermPayload term))) 49 (_ : lazyBool 50 (_ : sourceTermApply 51 (sourceTermApply 52 (sourceTermLiteral sourceCombS (sourceTermLocation term)) 53 (self (fst (sourceTermPayload term))) 54 (sourceTermLocation term)) 55 (self (snd (sourceTermPayload term))) 56 (sourceTermLocation term)) 57 (_ : term) 58 (equal? (sourceTermKind term) 3)) 59 (equal? (sourceTermKind term) 2)) 60 (equal? (sourceTermKind term) 1) 61 62 sourceBracketReference = (term : y sourceBracket_ term) 63 64 -- A free-variable test lets the retained B/C bracket path apply K to an 65 -- independent subtree. Without this pruning, repeated binders duplicate 66 -- residual S/K/I expressions exponentially even for a tiny source string. 67 sourceContainsBinder_ self term = 68 lazyBool 69 (_ : isZero_? (sourceTermPayload term)) 70 (_ : lazyBool 71 (_ : lazyBool 72 (_ : true) 73 (_ : self (snd (sourceTermPayload term))) 74 (self (fst (sourceTermPayload term)))) 75 (_ : false) 76 (equal? (sourceTermKind term) 3)) 77 (equal? (sourceTermKind term) 2) 78 79 sourceContainsBinder = (term : y sourceContainsBinder_ term) 80 81 -- Removing a binder decrements every surviving outer de Bruijn index. 82 sourceLower_ self term = 83 lazyBool 84 (_ : sourceTermVariable (pred_ (sourceTermPayload term)) 85 (sourceTermLocation term)) 86 (_ : lazyBool 87 (_ : sourceTermApply 88 (self (fst (sourceTermPayload term))) 89 (self (snd (sourceTermPayload term))) 90 (sourceTermLocation term)) 91 (_ : term) 92 (equal? (sourceTermKind term) 3)) 93 (equal? (sourceTermKind term) 2) 94 95 sourceLower = (term : y sourceLower_ term) 96 97 sourceBracketRightConstant self term left right = 98 lazyBool 99 (_ : sourceTermApply 100 (sourceTermLiteral sourceCombT (sourceTermLocation term)) 101 (sourceLower right) (sourceTermLocation term)) 102 (_ : sourceTermApply 103 (sourceTermApply 104 (sourceTermLiteral sourceCombC (sourceTermLocation term)) 105 (self left) (sourceTermLocation term)) 106 (sourceLower right) (sourceTermLocation term)) 107 (and? (equal? (sourceTermKind left) 2) 108 (isZero_? (sourceTermPayload left))) 109 110 sourceBracketDependentApp self term left right = 111 lazyBool 112 (_ : sourceBracketRightConstant self term left right) 113 (_ : lazyBool 114 (_ : lazyBool 115 (_ : sourceLower left) 116 (_ : sourceTermApply 117 (sourceTermApply 118 (sourceTermLiteral sourceCombB (sourceTermLocation term)) 119 (sourceLower left) (sourceTermLocation term)) 120 (self right) (sourceTermLocation term)) 121 (and? (equal? (sourceTermKind right) 2) 122 (isZero_? (sourceTermPayload right)))) 123 (_ : sourceTermApply 124 (sourceTermApply 125 (sourceTermLiteral sourceCombS (sourceTermLocation term)) 126 (self left) (sourceTermLocation term)) 127 (self right) (sourceTermLocation term)) 128 (not? (sourceContainsBinder left))) 129 (not? (sourceContainsBinder right)) 130 131 sourceBracketOptimized_ self term = 132 lazyBool 133 (_ : lazyBool 134 (_ : sourceTermLiteral sourceCombI (sourceTermLocation term)) 135 (_ : lazyBool 136 (_ : sourceBracketDependentApp self term 137 (fst (sourceTermPayload term)) (snd (sourceTermPayload term))) 138 (_ : term) 139 (equal? (sourceTermKind term) 3)) 140 (equal? (sourceTermKind term) 2)) 141 (_ : sourceTermApply 142 (sourceTermLiteral sourceCombK (sourceTermLocation term)) 143 (sourceLower term) 144 (sourceTermLocation term)) 145 (sourceContainsBinder term) 146 147 sourceBracket = (term : y sourceBracketOptimized_ term) 148 149 -- Bader's star_ski_eta deliberately uses S on dependent applications even 150 -- when a B or C is available. A locally smaller eliminator need not yield 151 -- the smaller *resulting function tree* after surrounding terms are applied. 152 -- Retain both strategies: they have different winners on different programs. 153 sourceBracketEtaApp self term left right = 154 lazyBool 155 (_ : sourceLower left) 156 (_ : sourceTermApply 157 (sourceTermApply 158 (sourceTermLiteral sourceCombS (sourceTermLocation term)) 159 (self left) (sourceTermLocation term)) 160 (self right) (sourceTermLocation term)) 161 (and? (not? (sourceContainsBinder left)) 162 (and? (equal? (sourceTermKind right) 2) 163 (isZero_? (sourceTermPayload right)))) 164 165 sourceBracketEta_ self term = 166 lazyBool 167 (_ : lazyBool 168 (_ : sourceTermLiteral sourceCombI (sourceTermLocation term)) 169 (_ : lazyBool 170 (_ : sourceBracketEtaApp self term 171 (fst (sourceTermPayload term)) (snd (sourceTermPayload term))) 172 (_ : term) 173 (equal? (sourceTermKind term) 3)) 174 (equal? (sourceTermKind term) 2)) 175 (_ : sourceTermApply 176 (sourceTermLiteral sourceCombK (sourceTermLocation term)) 177 (sourceLower term) (sourceTermLocation term)) 178 (sourceContainsBinder term) 179 180 sourceBracketEta = (term : y sourceBracketEta_ term) 181 182 -- A tricu list is a chain of Fork cells, not a host list stored in a Tree. 183 -- Build application syntax first; sourceRunTerm performs Tree application 184 -- only after all surrounding lambdas have been eliminated. 185 sourceEliminateList_ self elements eliminate location = 186 lazyList 187 (_ : sourceTermLiteral t location) 188 (head rest : sourceTermApply 189 (sourceTermApply 190 (sourceTermLiteral t location) 191 (eliminate head) location) 192 (self rest eliminate location) location) 193 elements 194 195 sourceEliminateList = (elements eliminate location : 196 y sourceEliminateList_ elements eliminate location) 197 198 sourceEliminate_ self node = 199 lazyBool 200 (_ : sourceTermLiteral t (sourceCoreStart node)) 201 (_ : lazyBool 202 (_ : sourceTermVariable (sourceCorePayload node) (sourceCoreStart node)) 203 (_ : lazyBool 204 (_ : sourceTermApply 205 (self (fst (sourceCorePayload node))) 206 (self (snd (sourceCorePayload node))) 207 (sourceCoreStart node)) 208 (_ : lazyBool 209 (_ : sourceBracket (self (sourceCorePayload node))) 210 (_ : lazyBool 211 (_ : sourceTermLiteral (sourceCorePayload node) 212 (sourceCoreStart node)) 213 (_ : lazyBool 214 (_ : sourceEliminateList (sourceCorePayload node) 215 self (sourceCoreStart node)) 216 (_ : sourceTermInvalid node (sourceCoreStart node)) 217 (equal? (sourceCoreKind node) sourceCoreListKind)) 218 (or? (equal? (sourceCoreKind node) sourceCoreExternalKind) 219 (or? (equal? (sourceCoreKind node) sourceCoreNumberKind) 220 (equal? (sourceCoreKind node) sourceCoreStringKind)))) 221 (equal? (sourceCoreKind node) sourceCoreLambdaKind)) 222 (equal? (sourceCoreKind node) sourceCoreApplyKind)) 223 (equal? (sourceCoreKind node) sourceCoreBoundKind)) 224 (equal? (sourceCoreKind node) sourceCoreLeafKind) 225 226 sourceEliminate = (node : y sourceEliminate_ node) 227 228 sourceEliminateEta_ self node = 229 lazyBool 230 (_ : sourceTermLiteral t (sourceCoreStart node)) 231 (_ : lazyBool 232 (_ : sourceTermVariable (sourceCorePayload node) (sourceCoreStart node)) 233 (_ : lazyBool 234 (_ : sourceTermApply 235 (self (fst (sourceCorePayload node))) 236 (self (snd (sourceCorePayload node))) 237 (sourceCoreStart node)) 238 (_ : lazyBool 239 (_ : sourceBracketEta (self (sourceCorePayload node))) 240 (_ : lazyBool 241 (_ : sourceTermLiteral (sourceCorePayload node) 242 (sourceCoreStart node)) 243 (_ : lazyBool 244 (_ : sourceEliminateList (sourceCorePayload node) 245 self (sourceCoreStart node)) 246 (_ : sourceTermInvalid node (sourceCoreStart node)) 247 (equal? (sourceCoreKind node) sourceCoreListKind)) 248 (or? (equal? (sourceCoreKind node) sourceCoreExternalKind) 249 (or? (equal? (sourceCoreKind node) sourceCoreNumberKind) 250 (equal? (sourceCoreKind node) sourceCoreStringKind)))) 251 (equal? (sourceCoreKind node) sourceCoreLambdaKind)) 252 (equal? (sourceCoreKind node) sourceCoreApplyKind)) 253 (equal? (sourceCoreKind node) sourceCoreBoundKind)) 254 (equal? (sourceCoreKind node) sourceCoreLeafKind) 255 256 sourceEliminateEta = (node : y sourceEliminateEta_ node) 257 258 -- Bader's kiselyov_eta: convert an entire core term into a residual term and 259 -- a stack of binder-use bits in one syntax traversal. The bits are consumed 260 -- from the inside out. Applications use B/C/R/S or eta identities according 261 -- to those bits. Unlike the per-binder star pass, this also sees nested 262 -- abstraction use without walking each application repeatedly. 263 sourceKFlags_ self first second = 264 lazyList 265 (_ : second) 266 (a restA : lazyList 267 (_ : first) 268 (b restB : pair (or? a b) (self restA restB)) 269 second) 270 first 271 sourceKFlags = (first second : y sourceKFlags_ first second) 272 273 sourceKTermLiteral? term tree = 274 and? (equal? (sourceTermKind term) 1) 275 (equal? (sourceTermPayload term) tree) 276 277 -- S K anything is extensionally I. Recognize the application form before 278 -- sourceRunTerm reduces it, as in Bader's is_id; a literal S K t is also I. 279 sourceKTermIdentityLeft? left = 280 lazyBool 281 (_ : and? 282 (sourceKTermLiteral? (fst (sourceTermPayload left)) sourceCombS) 283 (sourceKTermLiteral? (snd (sourceTermPayload left)) sourceCombK)) 284 (_ : false) 285 (equal? (sourceTermKind left) 3) 286 287 sourceKTermIdentity? term = 288 lazyBool 289 (_ : equal? (sourceTermPayload term) sourceCombI) 290 (_ : lazyBool 291 (_ : sourceKTermIdentityLeft? (fst (sourceTermPayload term))) 292 (_ : false) 293 (equal? (sourceTermKind term) 3)) 294 (equal? (sourceTermKind term) 1) 295 296 sourceKIsIdentity bits term = 297 lazyList 298 (_ : false) 299 (bit rest : and? bit 300 (and? (emptyList? rest) (sourceKTermIdentity? term))) 301 bits 302 303 sourceKHash_ self leftBits left rightBits right location = 304 lazyList 305 (_ : lazyList 306 (_ : sourceTermApply left right location) 307 (rightBit rightRest : 308 lazyBool 309 (_ : lazyBool 310 (_ : left) 311 (_ : self t 312 (sourceTermApply 313 (sourceTermLiteral sourceCombB location) left location) 314 rightRest right location) 315 (sourceKIsIdentity rightBits right)) 316 (_ : self t left rightRest right location) 317 rightBit) 318 rightBits) 319 (leftBit leftRest : 320 lazyList 321 (_ : lazyBool 322 (_ : lazyBool 323 (_ : sourceTermApply 324 (sourceTermLiteral sourceCombT location) right location) 325 (_ : self t 326 (sourceTermApply 327 (sourceTermLiteral sourceCombR location) right location) 328 leftRest left location) 329 (sourceKIsIdentity leftBits left)) 330 (_ : self leftRest left t right location) 331 leftBit) 332 (rightBit rightRest : 333 lazyBool 334 (_ : lazyBool 335 (_ : self t 336 (sourceTermLiteral sourceCombT location) 337 rightRest right location) 338 (_ : lazyBool 339 (_ : self leftRest 340 (self t (sourceTermLiteral sourceCombS location) 341 leftRest left location) 342 rightRest right location) 343 (_ : self leftRest 344 (self t (sourceTermLiteral sourceCombC location) 345 leftRest left location) 346 rightRest right location) 347 rightBit) 348 (and? (not? rightBit) 349 (sourceKIsIdentity leftBits left))) 350 (_ : lazyBool 351 (_ : left) 352 (_ : lazyBool 353 (_ : self leftRest 354 (self t (sourceTermLiteral sourceCombB location) 355 leftRest left location) 356 rightRest right location) 357 (_ : self leftRest left rightRest right location) 358 rightBit) 359 (and? rightBit 360 (sourceKIsIdentity rightBits right))) 361 leftBit) 362 rightBits) 363 leftBits 364 365 sourceKHash = (leftBits left rightBits right location : 366 y sourceKHash_ leftBits left rightBits right location) 367 368 sourceKApply left right location = 369 pair (sourceKFlags (fst left) (fst right)) 370 (sourceKHash (fst left) (snd left) (fst right) (snd right) 371 location) 372 373 sourceKBoundUses_ self index = 374 lazyBool 375 (_ : pair true t) 376 (_ : pair false (self (pred_ index))) 377 (isZero_? index) 378 sourceKBoundUses = (index : y sourceKBoundUses_ index) 379 380 -- Empty-left specialization of Kiselyov's application operator. Inspect the 381 -- bits being consumed *before* a known-empty control list can unfold the 382 -- generic operator while a surrounding abstraction is still symbolic. 383 sourceKWeaken_ self bits left right location = 384 lazyList 385 (_ : sourceTermApply left right location) 386 (bit rest : lazyBool 387 (_ : lazyBool 388 (_ : left) 389 (_ : self rest 390 (sourceTermApply 391 (sourceTermLiteral sourceCombB location) left location) 392 right location) 393 (sourceKIsIdentity bits right)) 394 (_ : self rest left right location) 395 bit) 396 bits 397 sourceKWeaken = (bits left right location : 398 y sourceKWeaken_ bits left right location) 399 400 sourceKAbstract bits term location = 401 lazyList 402 (_ : pair t (sourceTermApply 403 (sourceTermLiteral sourceCombK location) term location)) 404 (bit rest : lazyBool 405 (_ : pair rest term) 406 (_ : pair rest 407 (sourceKWeaken rest (sourceTermLiteral sourceCombK location) 408 term location)) 409 bit) 410 bits 411 412 sourceKList_ self elements convert location = 413 lazyList 414 (_ : pair t (sourceTermLiteral t location)) 415 (element rest : sourceKApply 416 (sourceKApply (pair t (sourceTermLiteral t location)) 417 (convert element) location) 418 (self rest convert location) location) 419 elements 420 sourceKList = (elements convert location : 421 y sourceKList_ elements convert location) 422 423 sourceKConvertApp self node = 424 sourceKApply (self (fst (sourceCorePayload node))) 425 (self (snd (sourceCorePayload node))) 426 (sourceCoreStart node) 427 428 sourceKConvertLambdaPack packed location = 429 sourceKAbstract (fst packed) (snd packed) location 430 431 sourceKConvertLambda self node = 432 sourceKConvertLambdaPack (self (sourceCorePayload node)) 433 (sourceCoreStart node) 434 435 sourceKConvertList self node = 436 sourceKList (sourceCorePayload node) self (sourceCoreStart node) 437 438 sourceKConvert_ self node = 439 lazyBool 440 (_ : pair t (sourceTermLiteral t (sourceCoreStart node))) 441 (_ : lazyBool 442 (_ : pair (sourceKBoundUses (sourceCorePayload node)) 443 (sourceTermLiteral sourceCombI (sourceCoreStart node))) 444 (_ : lazyBool 445 (_ : sourceKConvertApp self node) 446 (_ : lazyBool 447 (_ : sourceKConvertLambda self node) 448 (_ : lazyBool 449 (_ : pair t (sourceTermLiteral 450 (sourceCorePayload node) (sourceCoreStart node))) 451 (_ : lazyBool 452 (_ : sourceKConvertList self node) 453 (_ : pair t (sourceTermInvalid node 454 (sourceCoreStart node))) 455 (equal? (sourceCoreKind node) sourceCoreListKind)) 456 (or? (equal? (sourceCoreKind node) sourceCoreExternalKind) 457 (or? (equal? (sourceCoreKind node) sourceCoreNumberKind) 458 (equal? (sourceCoreKind node) sourceCoreStringKind)))) 459 (equal? (sourceCoreKind node) sourceCoreLambdaKind)) 460 (equal? (sourceCoreKind node) sourceCoreApplyKind)) 461 (equal? (sourceCoreKind node) sourceCoreBoundKind)) 462 (equal? (sourceCoreKind node) sourceCoreLeafKind) 463 sourceKConvert = (node : y sourceKConvert_ node) 464 465 sourceRunTerm_ self term = 466 lazyBool 467 (_ : ok (sourceTermPayload term) t) 468 (_ : lazyBool 469 (_ : err (parserDiagnostic 22 t (sourceTermPayload term) 470 (sourceTermLocation term) t) term) 471 (_ : lazyBool 472 (_ : lazyResult 473 (diagnostic rest : err diagnostic rest) 474 (function unused : 475 lazyResult 476 (diagnostic rest : err diagnostic rest) 477 (argument unused : ok (function argument) t) 478 (self (snd (sourceTermPayload term)))) 479 (self (fst (sourceTermPayload term)))) 480 (_ : err (parserDiagnostic 23 t (sourceTermKind term) 481 (sourceTermLocation term) t) term) 482 (equal? (sourceTermKind term) 3)) 483 (equal? (sourceTermKind term) 2)) 484 (equal? (sourceTermKind term) 1) 485 486 sourceRunTerm = (term : y sourceRunTerm_ term) 487 sourceCompileCoreReference = (node : sourceRunTerm (sourceEliminate node)) 488 sourceCompileCoreKiselyov = (node : sourceRunTerm (snd (sourceKConvert node))) 489 sourceCompileCore = (node : sourceRunTerm (sourceEliminateEta node)) 490 491 compileGateSource = (environment characters : 492 lazyResult 493 (diagnostic rest : err diagnostic rest) 494 (core unused : sourceCompileCore core) 495 (resolveGateSource environment characters)) 496