-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* handwritten examples~ * fixed root * something is wrong with the dump of choice.egg * Update dummy data from egglog --------- Co-authored-by: Max Willsey <[email protected]>
- Loading branch information
1 parent
84d67bf
commit c04b7fc
Showing
7 changed files
with
1,530 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
# make the .json data from the .egg files in this directory | ||
# run make from this directory | ||
# FIXME this doesn't quite work yet, egglog | ||
# doesn't export roots properly | ||
|
||
egg_files = $(wildcard *.egg) | ||
json_files = $(egg_files:.egg=.json) | ||
|
||
all: $(json_files) | ||
|
||
egglog_manifest = ../../../egglog/Cargo.toml | ||
|
||
%.json: %.egg | ||
cargo run --manifest-path $(egglog_manifest) -- $< --to-json | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
(datatype Math (Add Math Math) (A) (B)) | ||
|
||
(birewrite (Add a (Add b c)) (Add (Add a b) c)) | ||
(rewrite (Add a b) (Add b a)) | ||
|
||
; Tree extraction does not care about associativity or ordering | ||
; DAG extraction notices that balanced trees are much cheaper | ||
; Optimal tree is (let t1 (a + b) in let t2 = (t1 + t1) in (t2 + t2) | ||
; Which is cost 5 and proportional to the logarithm of the number of nodes | ||
(let A2 (Add (A) (A))) | ||
(let A4 (Add A2 A2)) | ||
(let B2 (Add (B) (B))) | ||
(let B4 (Add B2 B2)) | ||
(let t (Add A4 B4)) | ||
|
||
(run 10) |
Oops, something went wrong.