Merge remote-tracking branch 'origin/main' into om4

data/dummy_examples/Makefile

@@ -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
+

data/dummy_examples/ab_add.egg

@@ -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)