|
133 | 133 | (define-values (all-bindings extract-bindings) |
134 | 134 | (egglog-add-exprs insert-batch insert-brfs (egglog-runner-ctx runner) subproc)) |
135 | 135 |
|
136 | | - (send-to-egglog (list `(ruleset run-extract-commands) |
137 | | - `(rule () (,@all-bindings) :ruleset run-extract-commands) |
138 | | - `(run-schedule (repeat 1 run-extract-commands))) |
139 | | - subproc) |
| 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)))) |
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 (send-to-egglog (list '(run-schedule (saturate lift))) subproc)] |
| 145 | + ['lift (egglog-send subproc (list '(run-schedule (saturate lift))))] |
146 | 146 |
|
147 | | - ['lower (send-to-egglog (list '(run-schedule (saturate lower))) subproc)] |
| 147 | + ['lower (egglog-send subproc (list '(run-schedule (saturate lower))))] |
148 | 148 |
|
149 | | - ['unsound (send-to-egglog (list '(run-schedule (saturate unsound))) subproc)] |
| 149 | + ['unsound (egglog-send subproc (list '(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)])) |
|
157 | 157 | `(extract (,constructor-name) ,(*egglog-variants-limit*)))) |
158 | 158 |
|
159 | 159 | (define stdout-content |
160 | | - (send-to-egglog extract-commands subproc #:num-extracts (length extract-commands))) |
| 160 | + (egglog-send subproc extract-commands #:num-extracts (length extract-commands))) |
161 | 161 |
|
162 | 162 | ;; (Listof (Listof exprs)) |
163 | 163 | (define herbie-exprss |
|
206 | 206 | (define (prelude subproc #:mixed-egraph? [mixed-egraph? #t]) |
207 | 207 | (define pform (*active-platform*)) |
208 | 208 |
|
209 | | - (send-to-egglog |
210 | | - (list |
211 | | - `(datatype M (Num BigRat :cost 4294967295) (Var String :cost 4294967295) ,@(platform-spec-nodes))) |
212 | | - subproc) |
213 | | - |
214 | | - (send-to-egglog (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)) |
241 | | - subproc) |
| 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))) |
242 | 243 |
|
243 | 244 | (void)) |
244 | 245 |
|
|
544 | 545 | (set! root-bindings (cons (vector-ref mappings n) root-bindings)))) |
545 | 546 |
|
546 | 547 | ; Var-lowering-rules |
547 | | - (send-to-egglog (for/list ([var (in-list (context-vars ctx))] |
548 | | - [repr (in-list (context-var-reprs ctx))]) |
549 | | - `(rule ((= e (Var ,(symbol->string var)))) |
550 | | - ((let ty ,(symbol->string (representation-name repr)) |
551 | | - ) |
552 | | - (let ety (,(typed-var-id (representation-name repr)) |
553 | | - ,(symbol->string var)) |
554 | | - ) |
555 | | - (union (do-lower e ty) ety)) |
556 | | - :ruleset |
557 | | - lower)) |
558 | | - subproc) |
| 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))) |
559 | 560 |
|
560 | 561 | ; Var-lifting-rules |
561 | | - (send-to-egglog (for/list ([var (in-list (context-vars ctx))] |
562 | | - [repr (in-list (context-var-reprs ctx))]) |
563 | | - `(rule ((= e (,(typed-var-id (representation-name repr)) ,(symbol->string var)))) |
564 | | - ((let se (Var |
565 | | - ,(symbol->string var)) |
566 | | - ) |
567 | | - (union (do-lift e) se)) |
568 | | - :ruleset |
569 | | - lift)) |
570 | | - subproc) |
| 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))) |
571 | 572 |
|
572 | 573 | (define all-bindings '()) |
573 | 574 | (define binding->constructor (make-hash)) ; map from binding name to constructor name |
|
585 | 586 | (define curr-var-spec-binding `(let ,binding-name (Var ,(symbol->string var)))) |
586 | 587 |
|
587 | 588 | ; Send the constructor definition |
588 | | - (send-to-egglog (list `(constructor ,constructor-name () M :unextractable)) subproc) |
| 589 | + (egglog-send subproc (list `(constructor ,constructor-name () M :unextractable))) |
589 | 590 |
|
590 | 591 | ; Add the binding and constructor set to all-bindings for the future rule |
591 | 592 | (set! all-bindings (cons curr-var-spec-binding all-bindings)) |
|
606 | 607 | `(let ,binding-name (,(typed-var-id (representation-name repr)) ,(symbol->string var)))) |
607 | 608 |
|
608 | 609 | ; Send the constructor definition |
609 | | - (send-to-egglog (list `(constructor ,constructor-name () MTy :unextractable)) subproc) |
| 610 | + (egglog-send subproc (list `(constructor ,constructor-name () MTy :unextractable))) |
610 | 611 |
|
611 | 612 | ; Add the binding and constructor set to all-bindings for the future rule |
612 | 613 | (set! all-bindings (cons curr-var-typed-binding all-bindings)) |
|
639 | 640 |
|
640 | 641 | (define curr-binding-exprs `(let ,binding-name ,actual-binding)) |
641 | 642 |
|
642 | | - (send-to-egglog (list `(constructor ,constructor-name () ,curr-datatype :unextractable)) subproc) |
| 643 | + (egglog-send subproc (list `(constructor ,constructor-name () ,curr-datatype :unextractable))) |
643 | 644 |
|
644 | 645 | (set! all-bindings (cons curr-binding-exprs all-bindings)) |
645 | 646 | (set! all-bindings (cons `(set (,constructor-name) ,binding-name) all-bindings)) |
|
728 | 729 | ;; e-graph while extracting. For now, popping provides a smaller e-graph and gives |
729 | 730 | ;; performance comparable to Egg-Herbie, thought it doesn't affect correctness too much |
730 | 731 | [math-node-limit? |
731 | | - (send-to-egglog (list '(pop)) subproc) |
| 732 | + (egglog-send subproc (list '(pop))) |
732 | 733 | (values (sub1 curr-iter) #t)] |
733 | 734 |
|
734 | 735 | ;; If Unsoundness detected or node-limit reached, then return the |
735 | 736 | ;; optimal iter limit (one less than current) and run (pop) |
736 | 737 | [math-unsound? |
737 | 738 | ;; Pop once at the end since the egraph isn't valid |
738 | | - (send-to-egglog (list '(pop)) subproc) |
| 739 | + (egglog-send subproc (list '(pop))) |
739 | 740 |
|
740 | 741 | ;; Return one less than current iteration and indicate that we need to run again because pop |
741 | 742 | (values (sub1 curr-iter) #t)] |
|
760 | 761 | ;; TODO: See the TODO from above |
761 | 762 | [(equal? const-total-nodes prev-number-nodes) (values curr-iter #f)] |
762 | 763 | [const-node-limit? |
763 | | - (send-to-egglog (list '(pop)) subproc) |
| 764 | + (egglog-send subproc (list '(pop))) |
764 | 765 | (values (sub1 curr-iter) #t)] |
765 | 766 |
|
766 | 767 | [const-unsound? |
767 | | - (send-to-egglog (list '(pop)) subproc) |
| 768 | + (egglog-send subproc (list '(pop))) |
768 | 769 | (values (sub1 curr-iter) #t)] |
769 | 770 |
|
770 | 771 | [else |
|
774 | 775 | (loop (add1 curr-iter))])])]))) |
775 | 776 |
|
776 | 777 | (define (get-egglog-output curr-schedule subproc node-limit) |
777 | | - (define-values (node-values unsound?) (send-to-egglog-unsound-detection curr-schedule subproc)) |
| 778 | + (define-values (node-values unsound?) (egglog-send-unsound-detection subproc curr-schedule)) |
778 | 779 |
|
779 | 780 | ; (when unsound? |
780 | 781 | ; (printf "ALERT : UNSOUNDNESS DETECTED when...\n")) |
|
0 commit comments