compile.tri (18994B)
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 elements eliminate location = (let rec 186 walk remaining = (lazyList 187 (_ : sourceTermLiteral t location) 188 (head rest : sourceTermApply 189 (sourceTermApply (sourceTermLiteral t location) (eliminate head) location) 190 (walk rest) location) remaining) 191 in walk elements) 192 193 sourceEliminate_ self node = 194 lazyBool 195 (_ : sourceTermLiteral t (sourceCoreStart node)) 196 (_ : lazyBool 197 (_ : sourceTermVariable (sourceCorePayload node) (sourceCoreStart node)) 198 (_ : lazyBool 199 (_ : sourceTermApply 200 (self (fst (sourceCorePayload node))) 201 (self (snd (sourceCorePayload node))) 202 (sourceCoreStart node)) 203 (_ : lazyBool 204 (_ : sourceBracket (self (sourceCorePayload node))) 205 (_ : lazyBool 206 (_ : sourceTermLiteral (sourceCorePayload node) 207 (sourceCoreStart node)) 208 (_ : lazyBool 209 (_ : sourceEliminateList (sourceCorePayload node) 210 self (sourceCoreStart node)) 211 (_ : sourceTermInvalid node (sourceCoreStart node)) 212 (equal? (sourceCoreKind node) sourceCoreListKind)) 213 (or? (equal? (sourceCoreKind node) sourceCoreExternalKind) 214 (or? (equal? (sourceCoreKind node) sourceCoreNumberKind) 215 (equal? (sourceCoreKind node) sourceCoreStringKind)))) 216 (equal? (sourceCoreKind node) sourceCoreLambdaKind)) 217 (equal? (sourceCoreKind node) sourceCoreApplyKind)) 218 (equal? (sourceCoreKind node) sourceCoreBoundKind)) 219 (equal? (sourceCoreKind node) sourceCoreLeafKind) 220 221 sourceEliminate = (node : y sourceEliminate_ node) 222 223 sourceEliminateEta_ self node = 224 lazyBool 225 (_ : sourceTermLiteral t (sourceCoreStart node)) 226 (_ : lazyBool 227 (_ : sourceTermVariable (sourceCorePayload node) (sourceCoreStart node)) 228 (_ : lazyBool 229 (_ : sourceTermApply 230 (self (fst (sourceCorePayload node))) 231 (self (snd (sourceCorePayload node))) 232 (sourceCoreStart node)) 233 (_ : lazyBool 234 (_ : sourceBracketEta (self (sourceCorePayload node))) 235 (_ : lazyBool 236 (_ : sourceTermLiteral (sourceCorePayload node) 237 (sourceCoreStart node)) 238 (_ : lazyBool 239 (_ : sourceEliminateList (sourceCorePayload node) 240 self (sourceCoreStart node)) 241 (_ : sourceTermInvalid node (sourceCoreStart node)) 242 (equal? (sourceCoreKind node) sourceCoreListKind)) 243 (or? (equal? (sourceCoreKind node) sourceCoreExternalKind) 244 (or? (equal? (sourceCoreKind node) sourceCoreNumberKind) 245 (equal? (sourceCoreKind node) sourceCoreStringKind)))) 246 (equal? (sourceCoreKind node) sourceCoreLambdaKind)) 247 (equal? (sourceCoreKind node) sourceCoreApplyKind)) 248 (equal? (sourceCoreKind node) sourceCoreBoundKind)) 249 (equal? (sourceCoreKind node) sourceCoreLeafKind) 250 251 sourceEliminateEta = (node : y sourceEliminateEta_ node) 252 253 -- Bader's kiselyov_eta: convert an entire core term into a residual term and 254 -- a stack of binder-use bits in one syntax traversal. The bits are consumed 255 -- from the inside out. Applications use B/C/R/S or eta identities according 256 -- to those bits. Unlike the per-binder star pass, this also sees nested 257 -- abstraction use without walking each application repeatedly. 258 sourceKFlags_ self first second = 259 lazyList 260 (_ : second) 261 (a restA : lazyList 262 (_ : first) 263 (b restB : pair (or? a b) (self restA restB)) 264 second) 265 first 266 sourceKFlags = (first second : y sourceKFlags_ first second) 267 268 sourceKTermLiteral? term tree = 269 and? (equal? (sourceTermKind term) 1) 270 (equal? (sourceTermPayload term) tree) 271 272 -- S K anything is extensionally I. Recognize the application form before 273 -- sourceRunTerm reduces it, as in Bader's is_id; a literal S K t is also I. 274 sourceKTermIdentityLeft? left = 275 lazyBool 276 (_ : and? 277 (sourceKTermLiteral? (fst (sourceTermPayload left)) sourceCombS) 278 (sourceKTermLiteral? (snd (sourceTermPayload left)) sourceCombK)) 279 (_ : false) 280 (equal? (sourceTermKind left) 3) 281 282 sourceKTermIdentity? term = 283 lazyBool 284 (_ : equal? (sourceTermPayload term) sourceCombI) 285 (_ : lazyBool 286 (_ : sourceKTermIdentityLeft? (fst (sourceTermPayload term))) 287 (_ : false) 288 (equal? (sourceTermKind term) 3)) 289 (equal? (sourceTermKind term) 1) 290 291 sourceKIsIdentity bits term = 292 lazyList 293 (_ : false) 294 (bit rest : and? bit 295 (and? (emptyList? rest) (sourceKTermIdentity? term))) 296 bits 297 298 sourceKHash_ self leftBits left rightBits right location = 299 lazyList 300 (_ : lazyList 301 (_ : sourceTermApply left right location) 302 (rightBit rightRest : 303 lazyBool 304 (_ : lazyBool 305 (_ : left) 306 (_ : self t 307 (sourceTermApply 308 (sourceTermLiteral sourceCombB location) left location) 309 rightRest right location) 310 (sourceKIsIdentity rightBits right)) 311 (_ : self t left rightRest right location) 312 rightBit) 313 rightBits) 314 (leftBit leftRest : 315 lazyList 316 (_ : lazyBool 317 (_ : lazyBool 318 (_ : sourceTermApply 319 (sourceTermLiteral sourceCombT location) right location) 320 (_ : self t 321 (sourceTermApply 322 (sourceTermLiteral sourceCombR location) right location) 323 leftRest left location) 324 (sourceKIsIdentity leftBits left)) 325 (_ : self leftRest left t right location) 326 leftBit) 327 (rightBit rightRest : 328 lazyBool 329 (_ : lazyBool 330 (_ : self t 331 (sourceTermLiteral sourceCombT location) 332 rightRest right location) 333 (_ : lazyBool 334 (_ : self leftRest 335 (self t (sourceTermLiteral sourceCombS location) 336 leftRest left location) 337 rightRest right location) 338 (_ : self leftRest 339 (self t (sourceTermLiteral sourceCombC location) 340 leftRest left location) 341 rightRest right location) 342 rightBit) 343 (and? (not? rightBit) 344 (sourceKIsIdentity leftBits left))) 345 (_ : lazyBool 346 (_ : left) 347 (_ : lazyBool 348 (_ : self leftRest 349 (self t (sourceTermLiteral sourceCombB location) 350 leftRest left location) 351 rightRest right location) 352 (_ : self leftRest left rightRest right location) 353 rightBit) 354 (and? rightBit 355 (sourceKIsIdentity rightBits right))) 356 leftBit) 357 rightBits) 358 leftBits 359 360 sourceKHash = (leftBits left rightBits right location : 361 y sourceKHash_ leftBits left rightBits right location) 362 363 sourceKApply left right location = 364 pair (sourceKFlags (fst left) (fst right)) 365 (sourceKHash (fst left) (snd left) (fst right) (snd right) 366 location) 367 368 sourceKBoundUses_ self index = 369 lazyBool 370 (_ : pair true t) 371 (_ : pair false (self (pred_ index))) 372 (isZero_? index) 373 sourceKBoundUses = (index : y sourceKBoundUses_ index) 374 375 -- Empty-left specialization of Kiselyov's application operator. Inspect the 376 -- bits being consumed *before* a known-empty control list can unfold the 377 -- generic operator while a surrounding abstraction is still symbolic. 378 sourceKWeaken_ self bits left right location = 379 lazyList 380 (_ : sourceTermApply left right location) 381 (bit rest : lazyBool 382 (_ : lazyBool 383 (_ : left) 384 (_ : self rest 385 (sourceTermApply 386 (sourceTermLiteral sourceCombB location) left location) 387 right location) 388 (sourceKIsIdentity bits right)) 389 (_ : self rest left right location) 390 bit) 391 bits 392 sourceKWeaken = (bits left right location : 393 y sourceKWeaken_ bits left right location) 394 395 sourceKAbstract bits term location = 396 lazyList 397 (_ : pair t (sourceTermApply 398 (sourceTermLiteral sourceCombK location) term location)) 399 (bit rest : lazyBool 400 (_ : pair rest term) 401 (_ : pair rest 402 (sourceKWeaken rest (sourceTermLiteral sourceCombK location) 403 term location)) 404 bit) 405 bits 406 407 sourceKList_ self elements convert location = 408 lazyList 409 (_ : pair t (sourceTermLiteral t location)) 410 (element rest : sourceKApply 411 (sourceKApply (pair t (sourceTermLiteral t location)) 412 (convert element) location) 413 (self rest convert location) location) 414 elements 415 sourceKList = (elements convert location : 416 y sourceKList_ elements convert location) 417 418 sourceKConvertApp self node = 419 sourceKApply (self (fst (sourceCorePayload node))) 420 (self (snd (sourceCorePayload node))) 421 (sourceCoreStart node) 422 423 sourceKConvertLambdaPack packed location = 424 sourceKAbstract (fst packed) (snd packed) location 425 426 sourceKConvertLambda self node = 427 sourceKConvertLambdaPack (self (sourceCorePayload node)) 428 (sourceCoreStart node) 429 430 sourceKConvertList self node = 431 sourceKList (sourceCorePayload node) self (sourceCoreStart node) 432 433 sourceKConvert_ self node = 434 lazyBool 435 (_ : pair t (sourceTermLiteral t (sourceCoreStart node))) 436 (_ : lazyBool 437 (_ : pair (sourceKBoundUses (sourceCorePayload node)) 438 (sourceTermLiteral sourceCombI (sourceCoreStart node))) 439 (_ : lazyBool 440 (_ : sourceKConvertApp self node) 441 (_ : lazyBool 442 (_ : sourceKConvertLambda self node) 443 (_ : lazyBool 444 (_ : pair t (sourceTermLiteral 445 (sourceCorePayload node) (sourceCoreStart node))) 446 (_ : lazyBool 447 (_ : sourceKConvertList self node) 448 (_ : pair t (sourceTermInvalid node 449 (sourceCoreStart node))) 450 (equal? (sourceCoreKind node) sourceCoreListKind)) 451 (or? (equal? (sourceCoreKind node) sourceCoreExternalKind) 452 (or? (equal? (sourceCoreKind node) sourceCoreNumberKind) 453 (equal? (sourceCoreKind node) sourceCoreStringKind)))) 454 (equal? (sourceCoreKind node) sourceCoreLambdaKind)) 455 (equal? (sourceCoreKind node) sourceCoreApplyKind)) 456 (equal? (sourceCoreKind node) sourceCoreBoundKind)) 457 (equal? (sourceCoreKind node) sourceCoreLeafKind) 458 sourceKConvert = (node : y sourceKConvert_ node) 459 460 sourceRunTerm term = 461 lazyBool 462 (_ : ok (sourceTermPayload term) t) 463 (_ : lazyBool 464 (_ : err (parserDiagnostic 22 t (sourceTermPayload term) 465 (sourceTermLocation term) t) term) 466 (_ : lazyBool 467 (_ : lazyResult 468 (diagnostic rest : err diagnostic rest) 469 (function unused : 470 lazyResult 471 (diagnostic rest : err diagnostic rest) 472 (argument unused : ok (function argument) t) 473 (sourceRunTerm (snd (sourceTermPayload term)))) 474 (sourceRunTerm (fst (sourceTermPayload term)))) 475 (_ : err (parserDiagnostic 23 t (sourceTermKind term) 476 (sourceTermLocation term) t) term) 477 (equal? (sourceTermKind term) 3)) 478 (equal? (sourceTermKind term) 2)) 479 (equal? (sourceTermKind term) 1) 480 481 sourceCompileCoreReference = (node : sourceRunTerm (sourceEliminate node)) 482 sourceCompileCoreKiselyov = (node : sourceRunTerm (snd (sourceKConvert node))) 483 sourceCompileCore = (node : sourceRunTerm (sourceEliminateEta node)) 484 485 compileGateSource = (environment characters : 486 lazyResult 487 (diagnostic rest : err diagnostic rest) 488 (core unused : sourceCompileCore core) 489 (resolveGateSource environment characters)) 490