|
134 | 134 | (egglog-add-exprs insert-batch insert-brfs (egglog-runner-ctx runner) subproc)) |
135 | 135 |
|
136 | 136 | (egglog-send subproc |
137 | | - (list `(ruleset run-extract-commands) |
138 | | - `(rule () (,@all-bindings) :ruleset run-extract-commands) |
139 | | - `(run-schedule (repeat 1 run-extract-commands)))) |
| 137 | + `(ruleset run-extract-commands) |
| 138 | + `(rule () (,@all-bindings) :ruleset run-extract-commands) |
| 139 | + `(run-schedule (repeat 1 run-extract-commands))) |
140 | 140 |
|
141 | 141 | ;; 4. Running the schedule : having code inside to emulate egraph-run-rules |
142 | 142 |
|
143 | 143 | (for ([step (in-list (egglog-runner-schedule runner))]) |
144 | 144 | (match step |
145 | | - ['lift (egglog-send subproc (list '(run-schedule (saturate lift))))] |
| 145 | + ['lift (egglog-send subproc '(run-schedule (saturate lift)))] |
146 | 146 |
|
147 | | - ['lower (egglog-send subproc (list '(run-schedule (saturate lower))))] |
| 147 | + ['lower (egglog-send subproc '(run-schedule (saturate lower)))] |
148 | 148 |
|
149 | | - ['unsound (egglog-send subproc (list '(run-schedule (saturate unsound))))] |
| 149 | + ['unsound (egglog-send subproc '(run-schedule (saturate unsound)))] |
150 | 150 |
|
151 | 151 | ;; Run the rewrite ruleset interleaved with const-fold until the best iteration |
152 | 152 | ['rewrite (egglog-unsound-detected-subprocess step subproc)])) |
|
156 | 156 | (for/list ([constructor-name extract-bindings]) |
157 | 157 | `(extract (,constructor-name) ,(*egglog-variants-limit*)))) |
158 | 158 |
|
159 | | - (define stdout-content |
160 | | - (egglog-send subproc extract-commands #:num-extracts (length extract-commands))) |
| 159 | + (define stdout-content (egglog-extract subproc extract-commands)) |
161 | 160 |
|
162 | 161 | ;; (Listof (Listof exprs)) |
163 | 162 | (define herbie-exprss |
|
206 | 205 | (define (prelude subproc #:mixed-egraph? [mixed-egraph? #t]) |
207 | 206 | (define pform (*active-platform*)) |
208 | 207 |
|
209 | | - (egglog-send subproc |
210 | | - (list `(datatype M |
211 | | - (Num BigRat :cost 4294967295) |
212 | | - (Var String :cost 4294967295) |
213 | | - ,@(platform-spec-nodes)))) |
214 | | - |
215 | | - (egglog-send subproc |
216 | | - (append (list `(datatype MTy |
217 | | - ,@(num-typed-nodes pform) |
218 | | - ,@(var-typed-nodes pform) |
219 | | - (Approx M MTy) |
220 | | - ,@(platform-impl-nodes pform)) |
221 | | - `(constructor do-lower (M String) MTy :unextractable) |
222 | | - `(constructor do-lift (MTy) M :unextractable) |
223 | | - `(ruleset const-fold) |
224 | | - `(ruleset lower) |
225 | | - `(ruleset lift) |
226 | | - `(ruleset unsound) |
227 | | - `(function bad-merge? () bool :merge (or old new)) |
228 | | - `(ruleset bad-merge-rule) |
229 | | - `(set (bad-merge?) false) |
230 | | - `(rule ((= (Num c1) (Num c2)) (!= c1 c2)) |
231 | | - ((set (bad-merge?) true)) |
232 | | - :ruleset |
233 | | - bad-merge-rule)) |
234 | | - const-fold |
235 | | - (impl-lowering-rules pform) |
236 | | - (impl-lifting-rules pform) |
237 | | - (num-lowering-rules) |
238 | | - (num-lifting-rules) |
239 | | - (list (approx-lifting-rule)) |
240 | | - (egglog-rewrite-rules (*sound-removal-rules*) 'unsound) |
241 | | - (list `(ruleset rewrite)) |
242 | | - (egglog-rewrite-rules (*rules*) 'rewrite))) |
| 208 | + (egglog-send |
| 209 | + subproc |
| 210 | + `(datatype M (Num BigRat :cost 4294967295) (Var String :cost 4294967295) ,@(platform-spec-nodes))) |
| 211 | + |
| 212 | + (apply egglog-send |
| 213 | + subproc |
| 214 | + (append (list `(datatype MTy |
| 215 | + ,@(num-typed-nodes pform) |
| 216 | + ,@(var-typed-nodes pform) |
| 217 | + (Approx M MTy) |
| 218 | + ,@(platform-impl-nodes pform)) |
| 219 | + `(constructor do-lower (M String) MTy :unextractable) |
| 220 | + `(constructor do-lift (MTy) M :unextractable) |
| 221 | + `(ruleset const-fold) |
| 222 | + `(ruleset lower) |
| 223 | + `(ruleset lift) |
| 224 | + `(ruleset unsound) |
| 225 | + `(function bad-merge? () bool :merge (or old new)) |
| 226 | + `(ruleset bad-merge-rule) |
| 227 | + `(set (bad-merge?) false) |
| 228 | + `(rule ((= (Num c1) (Num c2)) (!= c1 c2)) |
| 229 | + ((set (bad-merge?) true)) |
| 230 | + :ruleset |
| 231 | + bad-merge-rule)) |
| 232 | + const-fold |
| 233 | + (impl-lowering-rules pform) |
| 234 | + (impl-lifting-rules pform) |
| 235 | + (num-lowering-rules) |
| 236 | + (num-lifting-rules) |
| 237 | + (list (approx-lifting-rule)) |
| 238 | + (egglog-rewrite-rules (*sound-removal-rules*) 'unsound) |
| 239 | + (list `(ruleset rewrite)) |
| 240 | + (egglog-rewrite-rules (*rules*) 'rewrite))) |
243 | 241 |
|
244 | 242 | (void)) |
245 | 243 |
|
|
545 | 543 | (set! root-bindings (cons (vector-ref mappings n) root-bindings)))) |
546 | 544 |
|
547 | 545 | ; Var-lowering-rules |
548 | | - (egglog-send subproc |
549 | | - (for/list ([var (in-list (context-vars ctx))] |
550 | | - [repr (in-list (context-var-reprs ctx))]) |
551 | | - `(rule ((= e (Var ,(symbol->string var)))) |
552 | | - ((let ty ,(symbol->string (representation-name repr)) |
553 | | - ) |
554 | | - (let ety (,(typed-var-id (representation-name repr)) |
555 | | - ,(symbol->string var)) |
556 | | - ) |
557 | | - (union (do-lower e ty) ety)) |
558 | | - :ruleset |
559 | | - lower))) |
| 546 | + (apply egglog-send |
| 547 | + subproc |
| 548 | + (for/list ([var (in-list (context-vars ctx))] |
| 549 | + [repr (in-list (context-var-reprs ctx))]) |
| 550 | + `(rule ((= e (Var ,(symbol->string var)))) |
| 551 | + ((let ty ,(symbol->string (representation-name repr)) |
| 552 | + ) |
| 553 | + (let ety (,(typed-var-id (representation-name repr)) |
| 554 | + ,(symbol->string var)) |
| 555 | + ) |
| 556 | + (union (do-lower e ty) ety)) |
| 557 | + :ruleset |
| 558 | + lower))) |
560 | 559 |
|
561 | 560 | ; Var-lifting-rules |
562 | | - (egglog-send subproc |
563 | | - (for/list ([var (in-list (context-vars ctx))] |
564 | | - [repr (in-list (context-var-reprs ctx))]) |
565 | | - `(rule ((= e (,(typed-var-id (representation-name repr)) ,(symbol->string var)))) |
566 | | - ((let se (Var |
567 | | - ,(symbol->string var)) |
568 | | - ) |
569 | | - (union (do-lift e) se)) |
570 | | - :ruleset |
571 | | - lift))) |
| 561 | + (apply egglog-send |
| 562 | + subproc |
| 563 | + (for/list ([var (in-list (context-vars ctx))] |
| 564 | + [repr (in-list (context-var-reprs ctx))]) |
| 565 | + `(rule ((= e (,(typed-var-id (representation-name repr)) ,(symbol->string var)))) |
| 566 | + ((let se (Var |
| 567 | + ,(symbol->string var)) |
| 568 | + ) |
| 569 | + (union (do-lift e) se)) |
| 570 | + :ruleset |
| 571 | + lift))) |
572 | 572 |
|
573 | 573 | (define all-bindings '()) |
574 | 574 | (define binding->constructor (make-hash)) ; map from binding name to constructor name |
|
586 | 586 | (define curr-var-spec-binding `(let ,binding-name (Var ,(symbol->string var)))) |
587 | 587 |
|
588 | 588 | ; Send the constructor definition |
589 | | - (egglog-send subproc (list `(constructor ,constructor-name () M :unextractable))) |
| 589 | + (egglog-send subproc `(constructor ,constructor-name () M :unextractable)) |
590 | 590 |
|
591 | 591 | ; Add the binding and constructor set to all-bindings for the future rule |
592 | 592 | (set! all-bindings (cons curr-var-spec-binding all-bindings)) |
|
607 | 607 | `(let ,binding-name (,(typed-var-id (representation-name repr)) ,(symbol->string var)))) |
608 | 608 |
|
609 | 609 | ; Send the constructor definition |
610 | | - (egglog-send subproc (list `(constructor ,constructor-name () MTy :unextractable))) |
| 610 | + (egglog-send subproc `(constructor ,constructor-name () MTy :unextractable)) |
611 | 611 |
|
612 | 612 | ; Add the binding and constructor set to all-bindings for the future rule |
613 | 613 | (set! all-bindings (cons curr-var-typed-binding all-bindings)) |
|
640 | 640 |
|
641 | 641 | (define curr-binding-exprs `(let ,binding-name ,actual-binding)) |
642 | 642 |
|
643 | | - (egglog-send subproc (list `(constructor ,constructor-name () ,curr-datatype :unextractable))) |
| 643 | + (egglog-send subproc `(constructor ,constructor-name () ,curr-datatype :unextractable)) |
644 | 644 |
|
645 | 645 | (set! all-bindings (cons curr-binding-exprs all-bindings)) |
646 | 646 | (set! all-bindings (cons `(set (,constructor-name) ,binding-name) all-bindings)) |
|
729 | 729 | ;; e-graph while extracting. For now, popping provides a smaller e-graph and gives |
730 | 730 | ;; performance comparable to Egg-Herbie, thought it doesn't affect correctness too much |
731 | 731 | [math-node-limit? |
732 | | - (egglog-send subproc (list '(pop))) |
| 732 | + (egglog-send subproc '(pop)) |
733 | 733 | (values (sub1 curr-iter) #t)] |
734 | 734 |
|
735 | 735 | ;; If Unsoundness detected or node-limit reached, then return the |
736 | 736 | ;; optimal iter limit (one less than current) and run (pop) |
737 | 737 | [math-unsound? |
738 | 738 | ;; Pop once at the end since the egraph isn't valid |
739 | | - (egglog-send subproc (list '(pop))) |
| 739 | + (egglog-send subproc '(pop)) |
740 | 740 |
|
741 | 741 | ;; Return one less than current iteration and indicate that we need to run again because pop |
742 | 742 | (values (sub1 curr-iter) #t)] |
|
761 | 761 | ;; TODO: See the TODO from above |
762 | 762 | [(equal? const-total-nodes prev-number-nodes) (values curr-iter #f)] |
763 | 763 | [const-node-limit? |
764 | | - (egglog-send subproc (list '(pop))) |
| 764 | + (egglog-send subproc '(pop)) |
765 | 765 | (values (sub1 curr-iter) #t)] |
766 | 766 |
|
767 | 767 | [const-unsound? |
768 | | - (egglog-send subproc (list '(pop))) |
| 768 | + (egglog-send subproc '(pop)) |
769 | 769 | (values (sub1 curr-iter) #t)] |
770 | 770 |
|
771 | 771 | [else |
|
0 commit comments