reductions-engine.rkt (21452B)
1 #lang racket/base 2 (require (for-syntax racket/base 3 syntax/parse 4 syntax/parse/experimental/contract) 5 racket/contract/base 6 syntax/stx 7 "deriv-util.rkt" 8 "stx-util.rkt" 9 "context.rkt" 10 "steps.rkt" 11 "reductions-config.rkt") 12 (provide (all-from-out "steps.rkt") 13 (all-from-out "reductions-config.rkt") 14 DEBUG 15 R 16 !) 17 18 (define-syntax ! (syntax-rules ())) 19 20 (define-syntax-rule (with-syntax1 ([pattern rhs]) . body) 21 (syntax-case rhs () 22 [pattern (let () . body)] 23 [x (raise-syntax-error 'with-syntax1 24 (format "failed pattern match against ~s" 25 'pattern) 26 #'x)])) 27 28 (define-syntax-rule (DEBUG form ...) 29 (when #f 30 form ... (void))) 31 32 (define-syntax-rule (STRICT-CHECKS form ...) 33 (when #f 34 form ... (void))) 35 36 (define RST/c (syntaxish? syntaxish? state/c list? . -> . RS/c)) 37 38 ;; (R R-clause ...) : RST 39 40 ;; An R-clause is one of 41 ;; [! expr] 42 ;; [#:set-syntax expr] 43 ;; [#:expect-syntax expr] 44 ;; [#:pattern pattern] 45 ;; [#:do expr ...] 46 ;; [#:let var expr] 47 ;; [#:left-foot] 48 ;; [#:walk term2 description] 49 ;; [#:rename pattern rename [description]] 50 ;; [#:rename/no-step pattern stx stx] 51 ;; [#:reductions expr] 52 ;; [#:learn ids] 53 ;; [#:if test R-clause ...] 54 ;; [#:when test R-clause ...] 55 ;; [#:hide-check ids] 56 ;; [#:seek-check] 57 ;; [generator hole fill] 58 59 (define-syntax R 60 (syntax-parser 61 [(R . clauses) 62 #'(lambda (f v s ws) 63 (R** f v _ s ws . clauses))])) 64 65 (define-syntax RP 66 (syntax-parser 67 [(RP p . clauses) 68 #'(lambda (f v s ws) 69 (R** f v p s ws . clauses))])) 70 71 ;; (R** form virtual-form pattern . clauses) 72 (define-syntax R** 73 (syntax-parser #:literals (! =>) 74 75 ;; (R** f v p s ws . clauses) 76 ;; f is the "real" form 77 ;; v is the "virtual" form (used for steps) 78 ;; - vis=#t: starts as f 79 ;; - vis=#f: starts as last visible term 80 ;; s is the last marked state 81 ;; ws is the list of steps, reversed 82 83 ;; Base: done 84 [(R** f v p s ws) 85 #'(RSunit ws f v s)] 86 87 [(R** f v p s ws => k . more) 88 #:declare k (expr/c #'RST/c) 89 #'(RSbind (k f v s ws) 90 (RP p . more))] 91 92 ;; Error-point case 93 [(R** f v p s ws [! maybe-exn] . more) 94 #:declare maybe-exn (expr/c #'(or/c exn? false/c)) 95 #'(let ([x maybe-exn]) 96 (if x 97 ;; FIXME 98 (RSfail (cons (stumble v x) ws) x) 99 (R** f v p s ws . more)))] 100 101 ;; Change patterns 102 [(R** f v p s ws [#:pattern p2] . more) 103 #'(R** f v p2 s ws . more)] 104 105 ;; Execute expressions for effect 106 [(R** f v p s ws [#:do expr ...] . more) 107 #'(begin 108 (with-syntax1 ([p f]) 109 expr ... (void)) 110 (R** f v p s ws . more))] 111 112 [(R** f v p s ws [#:let var expr] . more) 113 #'(let ([var (with-syntax1 ([p f]) expr)]) 114 (R** f v p s ws . more))] 115 116 [(R** f v p s ws [#:parameterize ((param expr) ...) . clauses] . more) 117 #:declare param (expr/c #'parameter?) 118 #'(RSbind (parameterize ((param expr) ...) 119 (R** f v p s ws . clauses)) 120 (RP p . more))] 121 122 ;; Change syntax 123 [(R** f v p s ws [#:set-syntax form] . more) 124 #:declare form (expr/c #'syntaxish?) 125 #'(let ([f2 (with-syntax1 ([p f]) form)]) 126 ;; FIXME: should (current-pass-hides?) be relevant? 127 (let ([v2 (if (visibility) f2 v)]) 128 (R** f2 v2 p s ws . more)))] 129 130 [(R** f v p s ws [#:expect-syntax expr ds] . more) 131 #:declare expr (expr/c #'syntax?) 132 #'(let ([expected (with-syntax1 ([p f]) expr)]) 133 (STRICT-CHECKS 134 (check-same-stx 'expect-syntax f expected ds)) 135 (R** f v p s ws . more))] 136 137 [(R** f v p s ws [#:left-foot] . more) 138 #'(R** f v p s ws [#:step #f v] . more)] 139 [(R** f v p s ws [#:left-foot fs] . more) 140 #'(R** f v p s ws [#:step #f fs] . more)] 141 142 [(R** f v p s ws [#:step type] . more) 143 #'(R** f v p s ws [#:step type v] . more)] 144 145 [(R** f v p s ws [#:step type fs] . more) 146 #:declare fs (expr/c #'syntaxish?) 147 #:declare type (expr/c #'(or/c step-type? false/c)) 148 #'(let ([s2 (and (visibility) 149 (current-state-with v (with-syntax1 ([p f]) fs)))] 150 [type-var type]) 151 (DEBUG 152 (printf "visibility = ~s\n" (if (visibility) 'VISIBLE 'HIDDEN)) 153 (printf "step: s1 = ~s\n" s) 154 (printf "step: s2 = ~s\n\n" s2)) 155 (let ([ws2 156 (if (and (visibility) type-var) 157 (cons (make step type-var s s2) ws) 158 ws)]) 159 (R** f v p s2 ws2 . more)))] 160 161 [(R** f v p s ws [#:walk form2 description] . more) 162 #:declare form2 (expr/c #'syntaxish?) 163 #'(let ([wfv (with-syntax1 ([p f]) form2)]) 164 (R** f v p s ws 165 [#:left-foot] 166 [#:set-syntax wfv] 167 [#:step description] 168 . more))] 169 170 [(R** f v p s ws [#:reductions rs] . more) 171 #:declare rs (expr/c #'(listof step?)) 172 #'(let ([ws2 173 (if (visibility) 174 (revappend (with-syntax1 ([p f]) rs) ws) 175 ws)]) 176 (R** f v p s ws2 . more))] 177 178 [(R** f v p s ws [#:in-hole hole . clauses] . more) 179 #'(let ([k (RP p . more)] 180 [reducer 181 (lambda (_) 182 (R . clauses))]) 183 (Run reducer f v p s ws hole #f k))] 184 185 ;; Rename 186 [(R** f v p s ws [#:rename pattern renames] . more) 187 #'(R** f v p s ws [#:rename pattern renames #f] . more)] 188 [(R** f v p s ws [#:rename pattern renames description] . more) 189 #'(R** f v p s ws [#:rename* pattern renames description #f]. more)] 190 191 [(R** f v p s ws [#:rename* pattern renames description mark-flag] . more) 192 #'(let-values ([(renames-var description-var) 193 (with-syntax1 ([p f]) 194 (values renames description))]) 195 (let* ([pre-renames-var 196 (with-syntax1 ([p f]) (syntax pattern))] 197 [f2 198 ((CC pattern f p) renames)] 199 [whole-form-rename? (eq? f pre-renames-var)] 200 [renames-mapping 201 (make-renames-mapping pre-renames-var renames-var)] 202 [v2 203 (cond [(or (visibility) (eq? mark-flag #f)) 204 (apply-renames-mapping renames-mapping v)] 205 [(eq? mark-flag 'mark) 206 v] 207 [(eq? mark-flag 'unmark) 208 (apply-renames-mapping 209 (compose-renames-mappings 210 (table->renames-mapping (marking-table)) 211 renames-mapping) 212 v)])] 213 [ws2 214 (if (and description-var (visibility)) 215 (cons (walk v v2 description-var 216 #:foci1 pre-renames-var 217 #:foci2 renames-var) 218 ws) 219 ws)]) 220 (parameterize ((subterms-table 221 (table-apply-renames-mapping 222 (subterms-table) 223 renames-mapping 224 whole-form-rename?))) 225 (R** f2 v2 p s ws2 . more))))] 226 227 [(R** f v p s ws [#:rename/mark pvar from to] . more) 228 #:declare from (expr/c #'syntaxish?) 229 #:declare to (expr/c #'syntaxish?) 230 #'(let ([real-from (with-syntax1 ([p f]) #'pvar)]) 231 (STRICT-CHECKS 232 (check-same-stx 'rename/mark real-from from)) 233 (when (marking-table) 234 (add-to-renames-table (marking-table) from to)) 235 (R** f v p s ws [#:rename* pvar to #f 'mark] . more))] 236 237 [(R** f v p s ws [#:rename/unmark pvar from to] . more) 238 #:declare from (expr/c #'syntaxish?) 239 #:declare to (expr/c #'syntaxish?) 240 #'(let ([real-from (with-syntax1 ([p f]) #'pvar)]) 241 (STRICT-CHECKS 242 (check-same-stx 'rename/mark real-from from)) 243 (R** f v p s ws [#:rename* pvar to #f 'unmark] . more))] 244 245 ;; Change syntax with rename (but no step) 246 [(R** f v p s ws [#:rename/no-step pvar from to] . more) 247 #:declare from (expr/c #'syntaxish?) 248 #:declare to (expr/c #'syntaxish?) 249 #'(let ([real-from (with-syntax1 ([p f]) #'pvar)]) 250 (STRICT-CHECKS 251 (check-same-stx 'rename/no-step real-from from)) 252 (R** f v p s ws [#:rename pvar to] . more))] 253 254 ;; Add to definite binders 255 [(R** f v p s ws [#:binders ids] . more) 256 #:declare ids (expr/c #'(listof identifier)) 257 #'(begin (learn-binders (flatten-identifiers (with-syntax1 ([p f]) ids))) 258 (R** f v p s ws . more))] 259 260 ;; Add to definite uses 261 [(R** f v p s ws [#:learn ids] . more) 262 #:declare ids (expr/c #'(listof identifier?)) 263 #'(begin (learn-definites (with-syntax1 ([p f]) ids)) 264 (R** f v p s ws . more))] 265 266 ;; Conditional (pattern changes lost afterwards ...) 267 [(R** f v p s ws [#:if test [consequent ...] [alternate ...]] . more) 268 #'(let ([continue (RP p . more)]) 269 (if (with-syntax1 ([p f]) test) 270 (R** f v p s ws consequent ... => continue) 271 (R** f v p s ws alternate ... => continue)))] 272 273 ;; Conditional (pattern changes lost afterwards ...) 274 [(R** f v p s ws [#:when test consequent ...] . more) 275 #'(let ([continue (RP p . more)]) 276 (if (with-syntax1 ([p f]) test) 277 (R** f v p s ws consequent ... => continue) 278 (continue f v s ws)))] 279 280 ;; HIDING DIRECTIVES 281 [(R** f v p s ws [#:hide-check ids] . more) 282 #:declare ids (expr/c #'(listof identifier?)) 283 #'(visibility-off (andmap (macro-policy) ids) 284 v 285 (lambda () (R** f v p s ws . more)))] 286 287 [(R** f v p s ws [#:seek-check] . more) 288 #'(seek-point f v (lambda (v2) (R** f v2 p s ws . more)))] 289 290 [(R** f v p s ws [#:print-state msg] . more) 291 #'(begin (printf "** ~s\n" msg) 292 (printf "f = ~.s\n" (stx->datum f)) 293 (printf "v = ~.s\n" (stx->datum v)) 294 (printf "s = ~.s\n" (stx->datum s)) 295 (R** f v p s ws . more))] 296 297 ;; ** Multi-pass reductions ** 298 299 ;; Pass1 does expansion. 300 ;; If something should happen regardless of whether hiding occurred 301 ;; in pass1 (eg, lifting), put it before the Pass2 marker. 302 303 ;; Use #:unsafe-bind-visible to access 'v' 304 ;; Warning: don't do anything that relies on real 'f' before pass2 305 306 ;; If something should be hidden if any hiding occurred in pass1, 307 ;; put it after the Pass2 marker (eg, splice, block->letrec). 308 309 [(R** f v p s ws [#:pass1] . more) 310 #'(parameterize ((hides-flags 311 (cons (box (not (visibility))) (hides-flags)))) 312 (DEBUG (printf "** pass1\n")) 313 (R** f v p s ws . more))] 314 315 [(R** f v p s ws [#:pass2 clause ...] . more) 316 #'(let* ([previous-pass-hides? (current-pass-hides?)] 317 [k (lambda (f2 v2 s2 ws2) 318 (parameterize ((hides-flags (cdr (hides-flags)))) 319 (when previous-pass-hides? (current-pass-hides? #t)) 320 (R** f2 v2 p s2 ws2 . more)))]) 321 (DEBUG (printf "** pass2\n")) 322 ;; FIXME: maybe refresh subterms table from v? 323 (visibility-off (not previous-pass-hides?) 324 v 325 (lambda () 326 (when #f (print-viable-subterms v)) 327 (R** f v p s ws clause ... => k)) 328 #t))] 329 330 [(R** f v p s ws [#:with-visible-form clause ...] . more) 331 #'(let ([k (RP p #| [#:set-syntax f] |# . more)]) 332 (if (visibility) 333 (R** v v p s ws clause ... => k) 334 (k f v s ws)))] 335 336 [(R** f v p s ws [#:new-local-context clause ...] . more) 337 ;; If vis = #t, then (clause ...) do not affect local config 338 ;; If vis = #f, then proceed normally 339 ;; *except* must save & restore real term 340 #'(let* ([vis (visibility)] 341 [process-clauses (lambda () (R** #f (if vis #f v) _ #f ws clause ...))]) 342 (RSbind (if vis 343 (with-new-local-context v (process-clauses)) 344 (process-clauses)) 345 (lambda (f2 v2 s2 ws2) 346 (let ([v2 (if vis v v2)] 347 [s2 (if vis s s2)]) 348 (R** f v2 p s2 ws2 . more)))))] 349 350 ;; Subterm handling 351 [(R** f v p s ws [reducer hole fill] . more) 352 #:declare reducer (expr/c #'(any/c . -> . RST/c)) 353 #'(let ([k (RP p . more)] 354 [reducer-var reducer]) 355 (Run reducer-var f v p s ws hole fill k))])) 356 357 (define-syntax (Run stx) 358 (syntax-case stx () 359 ;; Implementation of subterm handling for (hole ...) sequences 360 [(Run reducer f v p s ws (hole :::) fills-e k) 361 (and (identifier? #':::) 362 (free-identifier=? #'::: (quote-syntax ...))) 363 #'(let* ([fctx (CC (hole :::) f p)] 364 [init-e1s (with-syntax1 ([p f]) (syntax->list #'(hole :::)))] 365 [fills fills-e]) 366 (DEBUG 367 (printf "Run (multi, vis=~s)\n" (visibility)) 368 (printf " f: ~.s\n" (stx->datum f)) 369 (printf " v: ~.s\n" (stx->datum v)) 370 (printf " p: ~.s\n" 'p) 371 (printf " hole: ~.s\n" '(hole :::)) 372 (print-viable-subterms v)) 373 (if (visibility) 374 (let ([vctx (CC (hole :::) v p)] 375 [vsubs (with-syntax1 ([p v]) (syntax->list #'(hole :::)))]) 376 (run-multiple/visible reducer init-e1s fctx vsubs vctx fills s ws k)) 377 (run-multiple/nonvisible reducer init-e1s fctx v fills s ws k)))] 378 ;; Implementation of subterm handling 379 [(Run reducer f v p s ws hole fill k) 380 #'(let* ([init-e (with-syntax1 ([p f]) #'hole)] 381 [fctx (CC hole f p)]) 382 (DEBUG 383 (printf "Run (single, vis=~s)\n" (visibility)) 384 (printf " f: ~.s\n" (stx->datum f)) 385 (printf " v: ~.s\n" (stx->datum v)) 386 (printf " p: ~.s\n" 'p) 387 (printf " hole: ~.s\n" 'hole) 388 (print-viable-subterms v)) 389 (if (visibility) 390 (let ([vctx (CC hole v p)] 391 [vsub (with-syntax1 ([p v]) #'hole)]) 392 (run-one reducer init-e fctx vsub vctx fill s ws k)) 393 (run-one reducer init-e fctx v values fill s ws k)))])) 394 395 ;; run-one 396 (define (run-one reducer init-e fctx vsub vctx fill s ws k) 397 (DEBUG 398 (printf "run-one\n") 399 (printf " fctx: ~.s\n" (stx->datum (fctx #'HOLE))) 400 (printf " vctx: ~.s\n" (stx->datum (vctx #'HOLE)))) 401 (RSbind (with-context vctx 402 ((reducer fill) init-e vsub s ws)) 403 (lambda (f2 v2 s2 ws2) (k (fctx f2) (vctx v2) s2 ws2)))) 404 405 ;; run-multiple/visible 406 (define (run-multiple/visible reducer init-e1s fctx vsubs vctx fills s ws k) 407 (DEBUG 408 (printf "run-multiple/visible\n") 409 (printf " fctx: ~.s\n" (stx->datum (fctx (for/list ([dummy init-e1s]) #'HOLE)))) 410 (printf " vctx: ~.s\n" (stx->datum (vctx (for/list ([dummy init-e1s]) #'HOLE)))) 411 (unless (= (length fills) (length init-e1s)) 412 (printf " fills(~s): ~.s\n" (length fills) fills) 413 (printf " init-e1s: ~.s\n" (stx->datum init-e1s)) 414 (printf " vsubs: ~.s\n" (stx->datum vsubs)))) 415 (let loop ([fills fills] [prefix null] [vprefix null] [suffix init-e1s] [vsuffix vsubs] [s s] [ws ws]) 416 (cond 417 [(pair? fills) 418 (RSbind (with-context (lambda (x) (vctx (revappend vprefix (cons x (cdr vsuffix))))) 419 ((reducer (car fills)) (car suffix) (car vsuffix) s ws)) 420 (lambda (f2 v2 s2 ws2) 421 (loop (cdr fills) 422 (cons f2 prefix) 423 (cons v2 vprefix) 424 (cdr suffix) 425 (cdr vsuffix) 426 s2 427 ws2)))] 428 [(null? fills) 429 (k (fctx (reverse prefix)) (vctx (reverse vprefix)) s ws)]))) 430 431 ;; run-multiple/nonvisible 432 (define (run-multiple/nonvisible reducer init-e1s fctx v fills s ws k) 433 (DEBUG 434 (printf "run-multiple/nonvisible\n") 435 (printf " fctx: ~.s\n" (stx->datum (fctx (for/list ([dummy init-e1s]) #'HOLE))))) 436 (let loop ([fills fills] [prefix null] [suffix init-e1s] [v v] [s s] [ws ws]) 437 (DEBUG 438 (printf " v: ~.s\n" (stx->datum (datum->syntax #f v)))) 439 (cond 440 [(pair? fills) 441 (RSbind ((reducer (car fills)) (car suffix) v s ws) 442 (lambda (f2 v2 s2 ws2) 443 (loop (cdr fills) 444 (cons f2 prefix) 445 (cdr suffix) 446 v2 447 s2 448 ws2)))] 449 [(null? fills) 450 (k (fctx (reverse prefix)) v s ws)]))) 451 452 ;; ------------------------------------ 453 454 ;; CC 455 ;; the context constructor 456 (define-syntax (CC stx) 457 (syntax-case stx () 458 [(CC HOLE expr pattern) 459 #'(syntax-copier HOLE expr pattern)])) 460 461 (define (revappend a b) 462 (cond [(pair? a) (revappend (cdr a) (cons (car a) b))] 463 [(null? a) b])) 464 465 466 ;; visibility-off : boolean stx stx (-> a) -> a 467 (define (visibility-off new-visible? stx k [reset-subterms? #f]) 468 (cond [(and (not new-visible?) (or (visibility) reset-subterms?)) 469 (begin 470 (DEBUG 471 (printf "hide => seek: ~.s\n" (stx->datum stx))) 472 (current-pass-hides? #t) 473 (let* ([subterms (gather-proper-subterms stx)] 474 [marking (marking-table)] 475 [subterms 476 (if marking 477 (table-apply-renames-mapping 478 subterms 479 (table->renames-mapping marking) 480 #f) 481 subterms)]) 482 (parameterize ((visibility #f) 483 (subterms-table subterms) 484 (marking-table (or marking (make-hasheq)))) 485 (k))))] 486 [else (k)])) 487 488 ;; Seek 489 490 (provide/contract 491 [seek-point (syntaxish? syntaxish? (syntaxish? . -> . RS/c) . -> . RS/c)]) 492 493 ;; seek-point : stx (-> RS/c) -> RS/c 494 (define (seek-point stx vstx k) 495 (if (visibility) 496 (k vstx) 497 (begin 498 (DEBUG (printf "Seek point\n") 499 (print-viable-subterms stx)) 500 (let ([paths (table-get (subterms-table) stx)]) 501 (cond [(null? paths) 502 (DEBUG (printf "seek-point: failed on ~.s\n" (stx->datum stx))) 503 (k vstx)] 504 [(null? (cdr paths)) 505 (let ([path (car paths)]) 506 (DEBUG (printf "seek => hide: ~.s\n" (stx->datum stx))) 507 (let ([ctx (lambda (x) (path-replace vstx path x))]) 508 (RScase (parameterize ((visibility #t) 509 (subterms-table #f) 510 (marking-table #f)) 511 ;; Found stx within vstx 512 (with-context ctx (k stx))) 513 (lambda (ws2 stx2 vstx2 s2) 514 (let ([vstx2 (ctx vstx2)]) 515 (RSunit ws2 stx2 vstx2 s2))) 516 (lambda (ws exn) 517 (RSfail ws exn)))))] 518 [else 519 (raise (make nonlinearity stx paths))]))))) 520 521 (provide print-viable-subterms) 522 (define (print-viable-subterms stx) 523 (DEBUG 524 (let ([t (subterms-table)]) 525 (when t 526 (printf "viable subterms:\n") 527 (let loop ([stx stx]) 528 (cond [(syntax? stx) 529 (let ([paths (table-get t stx)]) 530 (if (pair? paths) 531 (printf " ~s\n" (stx->datum stx)) 532 (loop (syntax-e stx))))] 533 [(pair? stx) 534 (loop (car stx)) 535 (loop (cdr stx))])))))) 536 537 (define (check-same-stx function actual expected [derivs null]) 538 (unless (eq? actual expected) 539 (let* ([actual-datum (stx->datum actual)] 540 [expected-datum (stx->datum expected)] 541 [same-form? (equal? actual-datum expected-datum)]) 542 (if same-form? 543 (eprintf "same form but wrong wrappings:\n~.s\nwrongness:\n~.s\n" 544 actual-datum 545 (wrongness actual expected)) 546 (eprintf "got:\n~.s\n\nexpected:\n~.s\n" 547 actual-datum 548 expected-datum)) 549 (for ([d derivs]) (eprintf "\n~.s\n" d)) 550 (error function 551 (if same-form? 552 "wrong starting point (wraps)!" 553 "wrong starting point (form)!"))))) 554 555 (define (wrongness a b) 556 (cond [(eq? a b) 557 '---] 558 [(stx-list? a) 559 (map wrongness (stx->list a) (stx->list b))] 560 [(stx-pair? a) 561 (cons (wrongness (stx-car a) (stx-car b)) 562 (wrongness (stx-cdr a) (stx-cdr b)))] 563 [else (stx->datum a)])) 564 565 566 ;; flatten-identifiers : syntaxlike -> (list-of identifier) 567 (define (flatten-identifiers stx) 568 (syntax-case stx () 569 [id (identifier? #'id) (list #'id)] 570 [() null] 571 [(x . y) (append (flatten-identifiers #'x) (flatten-identifiers #'y))] 572 [else (error 'flatten-identifiers "neither syntax list nor identifier: ~s" 573 (if (syntax? stx) 574 (syntax->datum stx) 575 stx))]))