|
67 | 67 | [egraph-pointer (egraph_copy (egraph-data-egraph-pointer eg-data))])) |
68 | 68 |
|
69 | 69 | ; Adds expressions returning the root ids |
70 | | -(define (egraph-add-exprs egg-data batch roots ctx) |
| 70 | +(define (egraph-add-exprs egg-data batch ctx) |
71 | 71 | (match-define (egraph-data ptr id->spec) egg-data) |
72 | 72 |
|
73 | 73 | ; normalizes an approx spec |
|
108 | 108 | [(list op ids ...) (egraph_add_node ptr (~s op) (list->u32vec ids))] |
109 | 109 | [(? (disjoin symbol? number?) x) (egraph_add_node ptr (~s x) 0-vec)])) |
110 | 110 |
|
111 | | - (define insert-batch (batch-remove-zombie batch roots)) |
112 | | - (define mappings (build-vector (batch-length insert-batch) values)) |
| 111 | + (define mappings (build-vector (batch-length batch) values)) |
113 | 112 | (define (remap x) |
114 | 113 | (vector-ref mappings x)) |
115 | 114 |
|
116 | 115 | ; Inserting nodes bottom-up |
117 | | - (for ([node (in-vector (batch-nodes insert-batch))] |
| 116 | + (for ([node (in-vector (batch-nodes batch))] |
118 | 117 | [n (in-naturals)]) |
119 | 118 | (define idx |
120 | 119 | (match node |
|
125 | 124 | [(approx spec impl) (insert-node! (list '$approx (remap spec) (remap impl)))] |
126 | 125 | [(list op (app remap args) ...) (insert-node! (cons op args))])) |
127 | 126 | (vector-set! mappings n idx)) |
128 | | - (for ([root (in-vector (batch-roots insert-batch))]) |
| 127 | + (for ([root (in-vector (batch-roots batch))]) |
129 | 128 | (egraph_add_root ptr (remap root))) |
130 | 129 |
|
131 | | - (for ([node (in-vector (batch-nodes insert-batch))] |
| 130 | + (for ([node (in-vector (batch-nodes batch))] |
132 | 131 | #:when (approx? node)) |
133 | 132 | (match-define (approx spec impl) node) |
134 | 133 | (hash-ref! id->spec |
135 | 134 | (remap spec) |
136 | 135 | (lambda () |
137 | | - (define spec* (normalize-spec (batch-ref insert-batch spec))) |
138 | | - (define type (representation-type (repr-of-node insert-batch impl ctx))) |
| 136 | + (define spec* (normalize-spec (batch-ref batch spec))) |
| 137 | + (define type (representation-type (repr-of-node batch impl ctx))) |
139 | 138 | (cons spec* type)))) |
140 | 139 |
|
141 | | - (for/list ([root (in-vector (batch-roots insert-batch))]) |
| 140 | + (for/list ([root (in-vector (batch-roots batch))]) |
142 | 141 | (remap root))) |
143 | 142 |
|
144 | 143 | ;; runs rules on an egraph (optional iteration limit) |
|
202 | 201 |
|
203 | 202 | (define (egraph-expr-equal? egraph-data expr goal ctx) |
204 | 203 | (define batch (progs->batch (list expr goal))) |
205 | | - (match-define (list id1 id2) (egraph-add-exprs egraph-data batch (batch-roots batch) ctx)) |
| 204 | + (match-define (list id1 id2) (egraph-add-exprs egraph-data batch ctx)) |
206 | 205 | (= id1 id2)) |
207 | 206 |
|
208 | 207 | ;; returns a flattened list of terms or #f if it failed to expand the proof due to budget |
|
1222 | 1221 | (loop (sub1 num-iters)))] |
1223 | 1222 | [else (values egg-graph iteration-data)]))) |
1224 | 1223 |
|
1225 | | -(define (egraph-run-schedule batch roots schedule ctx) |
| 1224 | +(define (egraph-run-schedule batch schedule ctx) |
1226 | 1225 | ; allocate the e-graph |
1227 | 1226 | (define egg-graph (make-egraph-data)) |
1228 | 1227 |
|
1229 | 1228 | ; insert expressions into the e-graph |
1230 | | - (define root-ids (egraph-add-exprs egg-graph batch roots ctx)) |
| 1229 | + (define root-ids (egraph-add-exprs egg-graph batch ctx)) |
1231 | 1230 |
|
1232 | 1231 | ; run the schedule |
1233 | 1232 | (define egg-graph* |
|
1266 | 1265 |
|
1267 | 1266 | ;; Herbie's version of an egg runner. |
1268 | 1267 | ;; Defines parameters for running rewrite rules with egg |
1269 | | -(struct egg-runner (batch roots reprs schedule ctx new-roots egg-graph) |
| 1268 | +(struct egg-runner (batch reprs schedule ctx new-roots egg-graph) |
1270 | 1269 | #:transparent ; for equality |
1271 | 1270 | #:methods gen:custom-write ; for abbreviated printing |
1272 | 1271 | [(define (write-proc alt port mode) |
|
1282 | 1281 | ;; - scheduler: `(scheduler . <name>)` [default: backoff] |
1283 | 1282 | ;; - `simple`: run all rules without banning |
1284 | 1283 | ;; - `backoff`: ban rules if the fire too much |
1285 | | -(define (make-egraph batch roots reprs schedule ctx) |
| 1284 | +(define (make-egraph batch reprs schedule ctx) |
1286 | 1285 | (define (oops! fmt . args) |
1287 | 1286 | (apply error 'verify-schedule! fmt args)) |
1288 | 1287 | ; verify the schedule |
|
1306 | 1305 | [_ (oops! "in instruction `~a`, unknown parameter `~a`" instr param)]))] |
1307 | 1306 | [_ (oops! "expected `(<rules> . <params>)`, got `~a`" instr)])) |
1308 | 1307 |
|
1309 | | - (define-values (root-ids egg-graph) (egraph-run-schedule batch roots schedule ctx)) |
| 1308 | + (define-values (root-ids egg-graph) (egraph-run-schedule batch schedule ctx)) |
1310 | 1309 |
|
1311 | 1310 | ; make the runner |
1312 | | - (egg-runner batch roots reprs schedule ctx root-ids egg-graph)) |
| 1311 | + (egg-runner batch reprs schedule ctx root-ids egg-graph)) |
1313 | 1312 |
|
1314 | 1313 | (define (regraph-dump regraph root-ids reprs) |
1315 | 1314 | (define dump-dir "dump-egg") |
|
0 commit comments