From fdf875915103e2f29140d26e48c20a5286b4019d Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 11:19:42 -0800
Subject: [PATCH 1/7] Rename file

---
 egglog_src/{lakeroad.egg => churchroad.egg}       | 0
 src/lib.rs                                        | 2 +-
 tests/egglog_tests/agilex_alm.egg                 | 2 +-
 tests/egglog_tests/construct_sequential_cycle.egg | 2 +-
 tests/egglog_tests/half_adder.egg                 | 2 +-
 tests/egglog_tests/typing.egg                     | 2 +-
 6 files changed, 5 insertions(+), 5 deletions(-)
 rename egglog_src/{lakeroad.egg => churchroad.egg} (100%)

diff --git a/egglog_src/lakeroad.egg b/egglog_src/churchroad.egg
similarity index 100%
rename from egglog_src/lakeroad.egg
rename to egglog_src/churchroad.egg
diff --git a/src/lib.rs b/src/lib.rs
index 3c92251..e03224e 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -222,7 +222,7 @@ pub fn import_churchroad(egraph: &mut EGraph) {
     egraph
         .parse_and_run_program(
             r#"
-(include "egglog_src/lakeroad.egg")
+(include "egglog_src/churchroad.egg")
     "#,
         )
         .unwrap();
diff --git a/tests/egglog_tests/agilex_alm.egg b/tests/egglog_tests/agilex_alm.egg
index 065ebe1..b2c20f4 100644
--- a/tests/egglog_tests/agilex_alm.egg
+++ b/tests/egglog_tests/agilex_alm.egg
@@ -1,5 +1,5 @@
 ; Handled by calling churchroad::import_churchroad(&mut egraph) in the macro.
-; (include "egglog_src/lakeroad.egg")
+; (include "egglog_src/churchroad.egg")
 
 ; wire declarations
 ; a
diff --git a/tests/egglog_tests/construct_sequential_cycle.egg b/tests/egglog_tests/construct_sequential_cycle.egg
index ae5e56b..c9b0350 100644
--- a/tests/egglog_tests/construct_sequential_cycle.egg
+++ b/tests/egglog_tests/construct_sequential_cycle.egg
@@ -1,5 +1,5 @@
 ; Handled by calling churchroad::import_churchroad(&mut egraph) in the macro.
-; (include "egglog_src/lakeroad.egg")
+; (include "egglog_src/churchroad.egg")
 
 ; CONSTRUCTING GRAPHS
 ;
diff --git a/tests/egglog_tests/half_adder.egg b/tests/egglog_tests/half_adder.egg
index ce5a7d7..d9bb430 100644
--- a/tests/egglog_tests/half_adder.egg
+++ b/tests/egglog_tests/half_adder.egg
@@ -1,5 +1,5 @@
 ; Handled by calling churchroad::import_churchroad(&mut egraph) in the macro.
-; (include "egglog_src/lakeroad.egg")
+; (include "egglog_src/churchroad.egg")
 
 ; wire declarations
 ; $and$half-adder.v:17$2_Y
diff --git a/tests/egglog_tests/typing.egg b/tests/egglog_tests/typing.egg
index c45506a..01f2981 100644
--- a/tests/egglog_tests/typing.egg
+++ b/tests/egglog_tests/typing.egg
@@ -1,5 +1,5 @@
 ; Handled by calling churchroad::import_churchroad(&mut egraph) in the macro.
-; (include "egglog_src/lakeroad.egg")
+; (include "egglog_src/churchroad.egg")
 
 (let clk (Var "clk" 1))
 (let a (Var "a" 8))

From 16dda2104dbe265b4067590c98e925c77373a659 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 11:38:56 -0800
Subject: [PATCH 2/7] Move module enumeration rewrites to a file

---
 egglog_src/module_enumeration_rewrites.egg | 78 +++++++++++++++++++
 src/lib.rs                                 | 90 ++++++++++++++++++++++
 2 files changed, 168 insertions(+)
 create mode 100644 egglog_src/module_enumeration_rewrites.egg

diff --git a/egglog_src/module_enumeration_rewrites.egg b/egglog_src/module_enumeration_rewrites.egg
new file mode 100644
index 0000000..29e9b1b
--- /dev/null
+++ b/egglog_src/module_enumeration_rewrites.egg
@@ -0,0 +1,78 @@
+
+(ruleset enumerate-modules)
+(rewrite (Var name bw) (apply (MakeModule (Hole) (vec-of 0)) (vec-of (Var_ name bw))) :ruleset enumerate-modules)
+(rewrite
+  (Op0 op )
+  (apply (MakeModule (Op0_ op ) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) ))) (vec-append (vec-pop (vec-of (Var "unused" 0))) ))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op1 op expr0)
+  (apply (MakeModule (Op1_ op (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op1 op (apply (MakeModule graph0 _) args0))
+  (apply (MakeModule (Op1_ op graph0) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op2 op expr0 expr1)
+  (apply (MakeModule (Op2_ op (Hole) (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) (vec-of expr1)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) (vec-of expr1)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op2 op expr0 (apply (MakeModule graph1 _) args1))
+  (apply (MakeModule (Op2_ op (Hole) graph1) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) args1))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) args1))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op2 op (apply (MakeModule graph0 _) args0) expr1)
+  (apply (MakeModule (Op2_ op graph0 (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 (vec-of expr1)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 (vec-of expr1)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op2 op (apply (MakeModule graph0 _) args0) (apply (MakeModule graph1 _) args1))
+  (apply (MakeModule (Op2_ op graph0 graph1) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 args1))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 args1))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op expr0 expr1 expr2)
+  (apply (MakeModule (Op3_ op (Hole) (Hole) (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) (vec-of expr1) (vec-of expr2)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) (vec-of expr1) (vec-of expr2)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op expr0 expr1 (apply (MakeModule graph2 _) args2))
+  (apply (MakeModule (Op3_ op (Hole) (Hole) graph2) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) (vec-of expr1) args2))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) (vec-of expr1) args2))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op expr0 (apply (MakeModule graph1 _) args1) expr2)
+  (apply (MakeModule (Op3_ op (Hole) graph1 (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) args1 (vec-of expr2)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) args1 (vec-of expr2)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op expr0 (apply (MakeModule graph1 _) args1) (apply (MakeModule graph2 _) args2))
+  (apply (MakeModule (Op3_ op (Hole) graph1 graph2) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) args1 args2))) (vec-append (vec-pop (vec-of (Var "unused" 0))) (vec-of expr0) args1 args2))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op (apply (MakeModule graph0 _) args0) expr1 expr2)
+  (apply (MakeModule (Op3_ op graph0 (Hole) (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 (vec-of expr1) (vec-of expr2)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 (vec-of expr1) (vec-of expr2)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op (apply (MakeModule graph0 _) args0) expr1 (apply (MakeModule graph2 _) args2))
+  (apply (MakeModule (Op3_ op graph0 (Hole) graph2) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 (vec-of expr1) args2))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 (vec-of expr1) args2))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op (apply (MakeModule graph0 _) args0) (apply (MakeModule graph1 _) args1) expr2)
+  (apply (MakeModule (Op3_ op graph0 graph1 (Hole)) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 args1 (vec-of expr2)))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 args1 (vec-of expr2)))
+:ruleset enumerate-modules
+)
+(rewrite
+  (Op3 op (apply (MakeModule graph0 _) args0) (apply (MakeModule graph1 _) args1) (apply (MakeModule graph2 _) args2))
+  (apply (MakeModule (Op3_ op graph0 graph1 graph2) (debruijnify (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 args1 args2))) (vec-append (vec-pop (vec-of (Var "unused" 0))) args0 args1 args2))
+:ruleset enumerate-modules
+)
\ No newline at end of file
diff --git a/src/lib.rs b/src/lib.rs
index e03224e..70acadf 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -347,6 +347,76 @@ pub fn import_churchroad(egraph: &mut EGraph) {
         .unwrap();
 }
 
+/// Generate all module enumeration rewrites used by Churchroad.
+///
+/// This function is used to generate the contents of the the
+/// `egglog_src/module_enumeration_rewrites.egg` file. A test in this file
+/// ensures that the generated file matches what this function produces.
+pub fn generate_module_enumeration_rewrites(enumeration_ruleset_name: &str) -> String {
+    format!(
+            "
+(ruleset {enumeration_ruleset_name})
+{rewrites}",
+            enumeration_ruleset_name = enumeration_ruleset_name,
+            rewrites = vec![
+                // Var
+                // Note that this puts a loop in the graph, because a Var
+                // becomes a hole applied to itself. We just need to be careful
+                // about that during extraction.
+                format!("(rewrite (Var name bw) (apply (MakeModule (Hole) (vec-of 0)) (vec-of (Var_ name bw))) :ruleset {})", enumeration_ruleset_name),
+
+                // 0-ary
+                generate_module_enumeration_rewrite(&[], Some(enumeration_ruleset_name)),
+                // 1-ary
+                generate_module_enumeration_rewrite(&[true], Some(enumeration_ruleset_name)),
+                generate_module_enumeration_rewrite(&[false], Some(enumeration_ruleset_name)),
+                // 2-ary
+                generate_module_enumeration_rewrite(&[true, true], Some(enumeration_ruleset_name)),
+                generate_module_enumeration_rewrite(&[true, false], Some(enumeration_ruleset_name)),
+                generate_module_enumeration_rewrite(&[false, true], Some(enumeration_ruleset_name)),
+                generate_module_enumeration_rewrite(
+                    &[false, false],
+                    Some(enumeration_ruleset_name)
+                ),
+                // 3-ary
+                generate_module_enumeration_rewrite(
+                    &[true, true, true],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[true, true, false],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[true, false, true],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[true, false, false],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[false, true, true],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[false, true, false],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[false, false, true],
+                    Some(enumeration_ruleset_name)
+                ),
+                generate_module_enumeration_rewrite(
+                    &[false, false, false],
+                    Some(enumeration_ruleset_name)
+                ),
+                // clang-format on
+            ]
+            .join("\n"),
+        )
+}
+
 /// Generate module enumeration rewrite.
 ///
 /// - hole_indicator: a list of booleans indicating whether the Op's
@@ -460,4 +530,24 @@ pub fn list_modules(egraph: &mut EGraph, num_variants: usize) {
 #[cfg(test)]
 mod tests {
     // use super::*;
+
+    use std::path::Path;
+
+    #[test]
+    fn test_module_enumeration_rewrites_up_to_date() {
+        // Read in egglog_src/module_enumeration_rewrites.egg and check that it
+        // matches the output of generate_module_enumeration_rewrites.
+        let actual = std::fs::read_to_string(
+            Path::new(env!("CARGO_MANIFEST_DIR"))
+                .join("egglog_src")
+                .join("module_enumeration_rewrites.egg"),
+        )
+        .unwrap();
+        let expected = super::generate_module_enumeration_rewrites("enumerate-modules");
+        assert_eq!(
+            expected, actual,
+            "Copy and paste this up-to-date source into module_enumeartion_rewrites.egg:\n{}",
+            expected
+        );
+    }
 }

From d167dc14f503c18cf4f64da2b01193c25dd223d9 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 11:42:00 -0800
Subject: [PATCH 3/7] Include rewrites from file

---
 src/lib.rs | 68 ++++--------------------------------------------------
 1 file changed, 5 insertions(+), 63 deletions(-)

diff --git a/src/lib.rs b/src/lib.rs
index 70acadf..b491fe6 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -280,70 +280,12 @@ pub fn import_churchroad(egraph: &mut EGraph) {
             .unwrap(),
     });
 
-    let enumeration_ruleset_name = "enumerate-modules";
     egraph
-        .parse_and_run_program(&format!(
-            "
-(ruleset {enumeration_ruleset_name})
-{rewrites}",
-            enumeration_ruleset_name = enumeration_ruleset_name,
-            rewrites = vec![
-                // Var
-                // Note that this puts a loop in the graph, because a Var
-                // becomes a hole applied to itself. We just need to be careful
-                // about that during extraction.
-                format!("(rewrite (Var name bw) (apply (MakeModule (Hole) (vec-of 0)) (vec-of (Var_ name bw))) :ruleset {})", enumeration_ruleset_name),
-
-                // 0-ary
-                generate_module_enumeration_rewrite(&[], Some(enumeration_ruleset_name)),
-                // 1-ary
-                generate_module_enumeration_rewrite(&[true], Some(enumeration_ruleset_name)),
-                generate_module_enumeration_rewrite(&[false], Some(enumeration_ruleset_name)),
-                // 2-ary
-                generate_module_enumeration_rewrite(&[true, true], Some(enumeration_ruleset_name)),
-                generate_module_enumeration_rewrite(&[true, false], Some(enumeration_ruleset_name)),
-                generate_module_enumeration_rewrite(&[false, true], Some(enumeration_ruleset_name)),
-                generate_module_enumeration_rewrite(
-                    &[false, false],
-                    Some(enumeration_ruleset_name)
-                ),
-                // 3-ary
-                generate_module_enumeration_rewrite(
-                    &[true, true, true],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[true, true, false],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[true, false, true],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[true, false, false],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[false, true, true],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[false, true, false],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[false, false, true],
-                    Some(enumeration_ruleset_name)
-                ),
-                generate_module_enumeration_rewrite(
-                    &[false, false, false],
-                    Some(enumeration_ruleset_name)
-                ),
-                // clang-format on
-            ]
-            .join("\n"),
-        ))
+        .parse_and_run_program(
+            r#"
+(include "egglog_src/module_enumeration_rewrites.egg")
+    "#,
+        )
         .unwrap();
 }
 

From 50423fc6645973668f91187c9ef1cfe59417b24b Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 11:51:14 -0800
Subject: [PATCH 4/7] Move debruijnify into its own function

---
 src/lib.rs | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/lib.rs b/src/lib.rs
index b491fe6..069ee4b 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -219,14 +219,25 @@ pub fn to_verilog(term_dag: &TermDag, id: usize) -> String {
 /// That's not currently possible because of the Rust-defined primitive
 /// `debruijnify` in Churchroad.
 pub fn import_churchroad(egraph: &mut EGraph) {
+    // STEP 1: import primary language definitions.
     egraph
-        .parse_and_run_program(
-            r#"
-(include "egglog_src/churchroad.egg")
-    "#,
-        )
+        .parse_and_run_program(r#"(include "egglog_src/churchroad.egg")"#)
+        .unwrap();
+
+    // STEP 2: add the `debruijnify` primitive to the egraph. This depends on
+    // the above language definitions, but it's not possible to do it in egglog,
+    // hence it's a Rust function.
+    add_debruijnify(egraph);
+
+    // STEP 3: import module enumeration rewrites. These depend on the
+    // `debruijnify` primitive.
+    egraph
+        .parse_and_run_program(r#"(include "egglog_src/module_enumeration_rewrites.egg")"#)
         .unwrap();
+}
 
+/// Add the `debruijnify` primitive to an [`EGraph`].
+fn add_debruijnify(egraph: &mut EGraph) {
     struct DeBruijnify {
         in_sort: Arc<VecSort>,
         out_sort: Arc<VecSort>,
@@ -279,14 +290,6 @@ pub fn import_churchroad(egraph: &mut EGraph) {
             .get_sort_by(|s: &Arc<VecSort>| s.name() == "IVec".into())
             .unwrap(),
     });
-
-    egraph
-        .parse_and_run_program(
-            r#"
-(include "egglog_src/module_enumeration_rewrites.egg")
-    "#,
-        )
-        .unwrap();
 }
 
 /// Generate all module enumeration rewrites used by Churchroad.

From 845670b8d9d9cdf5d571a248fbf4af97a81b4c16 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 12:47:20 -0800
Subject: [PATCH 5/7] Add `Add` op

---
 egglog_src/churchroad.egg | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/egglog_src/churchroad.egg b/egglog_src/churchroad.egg
index dc7304e..cbf3d9b 100644
--- a/egglog_src/churchroad.egg
+++ b/egglog_src/churchroad.egg
@@ -9,6 +9,7 @@
 ; Ops
 (datatype Op
   (And)
+  (Add)
   (Or)
   (Xor)
   (Shr)
@@ -102,6 +103,7 @@
 ;;; op.
 (relation AllBitwidthsMatch (Op))
 (AllBitwidthsMatch (And))
+(AllBitwidthsMatch (Add))
 (AllBitwidthsMatch (Or))
 (AllBitwidthsMatch (Xor))
 (AllBitwidthsMatch (Shr))

From 9f8c03bc3593af44cffc099ea62bac0e25a16ad6 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 12:47:34 -0800
Subject: [PATCH 6/7] Add demo for Monday

---
 src/lib.rs | 148 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 147 insertions(+), 1 deletion(-)

diff --git a/src/lib.rs b/src/lib.rs
index 069ee4b..8046f5a 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -474,10 +474,12 @@ pub fn list_modules(egraph: &mut EGraph, num_variants: usize) {
 
 #[cfg(test)]
 mod tests {
-    // use super::*;
+    use super::*;
 
     use std::path::Path;
 
+    use egglog::EGraph;
+
     #[test]
     fn test_module_enumeration_rewrites_up_to_date() {
         // Read in egglog_src/module_enumeration_rewrites.egg and check that it
@@ -495,4 +497,148 @@ mod tests {
             expected
         );
     }
+
+    #[test]
+    fn demo_2024_02_06() {
+        // Set the environment variable DEMO_2024_02_06_WRITE_SVGS to anything
+        // to produce SVGs.
+        fn write_svg(egraph: &EGraph, path: &str) {
+            if std::env::var("DEMO_2024_02_06_WRITE_SVGS").is_err() {
+                return;
+            }
+            let serialized = egraph.serialize_for_graphviz(true);
+            let svg_path = Path::new(path).with_extension("svg");
+            serialized.to_svg_file(svg_path).unwrap();
+        }
+
+        ///////////////////////////// BEGIN DEMO ///////////////////////////////
+
+        // We currently need to import Churchroad via Rust (rather than using an
+        // egglog `include`) because it depends on a custom primitive.
+        let mut egraph = EGraph::default();
+        import_churchroad(&mut egraph);
+
+        // Churchroad programs can be very simple circuits, e.g. this one-bit and:
+        egraph
+            .parse_and_run_program(
+                r#"
+
+                (let one-bit-and (Op2 (And) (Var "a" 1) (Var "b" 1)))
+
+            "#,
+            )
+            .unwrap();
+        write_svg(&egraph, "1.svg");
+
+        // Clean up the last example...
+        let mut egraph = EGraph::default();
+        import_churchroad(&mut egraph);
+
+        // The first interesting feature of Churchroad is that it can represent
+        // cyclic circuits using the native features of the egraph. For example,
+        // a simple counter circuit looks like this:
+        //
+        //        ┌────┐
+        //      ┌─▼─┐ ┌┴─┐
+        //      │reg│ │+1│
+        //      └─┬─┘ └▲─┘
+        //        └────┘
+        //
+        // In Churchroad, we can capture this easily using the following
+        // commands:
+        egraph
+            .parse_and_run_program(
+                r#"
+
+                ; Instantiate a placeholder wire, which will be connected later.
+                (let placeholder (Wire "placeholder" 8))
+
+                ; Generate the +1 box, but feed it with a temporary placeholder.
+                (let plusone  (Op2 (Add) placeholder (Op0 (BV 1 8))))
+
+                ; Generate the register, whose input is the output of +1.
+                (let reg (Op1 (Reg 0) plusone))
+
+                ; Finally, connect the placeholder to the output of the register
+                ; and delete the placeholder.
+                (union placeholder reg)
+                (delete (Wire "placeholder" 8))
+
+            "#,
+            )
+            .unwrap();
+        write_svg(&egraph, "2.svg");
+
+        // Clean up the last example...
+        let mut egraph = EGraph::default();
+        import_churchroad(&mut egraph);
+
+        // The next interesting feature of Churchroad is that the representation
+        // and its rewrites allow it to find repeated patterns across the
+        // egraph.
+        //
+        // First, let's discuss the underlying representation that allows this.
+        // As we saw in the first example, Churchroad can represent circuits
+        // directly. However, Churchroad can also represent circuits as
+        // applications of abstract modules to concrete inputs:
+        egraph
+            .parse_and_run_program(
+                r#"
+
+                ; An abstract `and` module.
+                (let and-module (MakeModule (Op2_ (And) (Hole) (Hole)) (vec-of 0 1)))
+
+                ; We can represent a concrete `and` by applying the abstract
+                ; module to concrete inputs.
+                (let and (apply and-module (vec-of (Var "a" 1) (Var "b" 1))))
+
+            "#,
+            )
+            .unwrap();
+        write_svg(&egraph, "3.svg");
+
+        // Clean up the last example...
+        let mut egraph = EGraph::default();
+        import_churchroad(&mut egraph);
+
+        // Translating from the first form to the second (`apply`-based) form is
+        // achieved simply with rewrites!
+        egraph
+            .parse_and_run_program(
+                r#"
+
+                ; First, "direct" form.
+                (let and (Op2 (And) (Var "a" 1) (Var "b" 1)))
+
+                ; Run module enumeration rewrites to convert to "apply" form.
+                (run-schedule (repeat 1 enumerate-modules))
+    
+            "#,
+            )
+            .unwrap();
+        write_svg(&egraph, "4.svg");
+
+        // Clean up the last example...
+        let mut egraph = EGraph::default();
+        import_churchroad(&mut egraph);
+
+        // So why do this? Well the `apply`-based form allows us to find
+        // repeated patterns in the egraph. As a simple example, imagine we have
+        // a series of two `and` gates in a row. This form will allow us to
+        // discover that the two `and` gates are the same:
+        egraph
+            .parse_and_run_program(
+                r#"
+
+                ; First, "direct" form.
+                (let and (Op2 (And) (Var "a" 1) (Op2 (And) (Var "b" 1) (Var "c" 1))))
+
+                ; Run module enumeration rewrites to convert to "apply" form.
+                (run-schedule (saturate enumerate-modules))
+    
+            "#,
+            )
+            .unwrap();
+        write_svg(&egraph, "5.svg");
+    }
 }

From b01fe96411e6cbc3ea7884250bb9dafa1b158380 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Sun, 25 Feb 2024 13:09:44 -0800
Subject: [PATCH 7/7] Update cargo.lock

---
 Cargo.lock | 88 +++++++++++++++++++++++++++---------------------------
 1 file changed, 44 insertions(+), 44 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index f35be33..59bbfaa 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -15,9 +15,9 @@ dependencies = [
 
 [[package]]
 name = "ahash"
-version = "0.8.8"
+version = "0.8.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "42cd52102d3df161c77a887b608d7a4897d7cc112886a9537b738a887a03aaff"
+checksum = "d713b3834d76b85304d4d525563c1276e2e30dc97cc67bfb4585a4a29fc2c89f"
 dependencies = [
  "cfg-if",
  "once_cell",
@@ -184,7 +184,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.49",
+ "syn 2.0.50",
 ]
 
 [[package]]
@@ -431,7 +431,7 @@ version = "0.14.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"
 dependencies = [
- "ahash 0.8.8",
+ "ahash 0.8.9",
  "allocator-api2",
 ]
 
@@ -443,9 +443,9 @@ checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
 
 [[package]]
 name = "hermit-abi"
-version = "0.3.6"
+version = "0.3.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bd5256b483761cd23699d0da46cc6fd2ee3be420bbe6d020ae4a091e70b7e9fd"
+checksum = "379dada1584ad501b383485dd706b8afb7a70fcbc7f4da7d780638a5a6124a60"
 
 [[package]]
 name = "humantime"
@@ -722,7 +722,7 @@ dependencies = [
  "pest_meta",
  "proc-macro2",
  "quote",
- "syn 2.0.49",
+ "syn 2.0.50",
 ]
 
 [[package]]
@@ -905,9 +905,9 @@ checksum = "7ffc183a10b4478d04cbbbfc96d0873219d962dd5accaff2ffbd4ceb7df837f4"
 
 [[package]]
 name = "ryu"
-version = "1.0.16"
+version = "1.0.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f98d2aa92eebf49b69786be48e4477826b256916e84a57ff2a4f21923b48eb4c"
+checksum = "e86697c916019a8588c99b5fac3cead74ec0b4b819707a682fd4d23fa0ce1ba1"
 
 [[package]]
 name = "scopeguard"
@@ -917,29 +917,29 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
 [[package]]
 name = "serde"
-version = "1.0.196"
+version = "1.0.197"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "870026e60fa08c69f064aa766c10f10b1d62db9ccd4d0abb206472bee0ce3b32"
+checksum = "3fb1c873e1b9b056a4dc4c0c198b24c3ffa059243875552b2bd0933b1aee4ce2"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.196"
+version = "1.0.197"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "33c85360c95e7d137454dc81d9a4ed2b8efd8fbe19cee57357b32b9771fccb67"
+checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.49",
+ "syn 2.0.50",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.113"
+version = "1.0.114"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "69801b70b1c3dac963ecb03a364ba0ceda9cf60c71cfe475e99864759c8b8a79"
+checksum = "c5f09b1bd632ef549eaa9f60a1f8de742bdbc698e6cee2095fc84dde5f549ae0"
 dependencies = [
  "indexmap",
  "itoa",
@@ -1012,9 +1012,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.49"
+version = "2.0.50"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "915aea9e586f80826ee59f8453c1101f9d1c4b3964cd2460185ee8e299ada496"
+checksum = "74f1bdc9872430ce9b75da68329d1c1746faf50ffac5f19e02b71e37ff881ffb"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1070,7 +1070,7 @@ checksum = "a953cb265bef375dae3de6663da4d3804eee9682ea80d8e2542529b73c531c81"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.49",
+ "syn 2.0.50",
 ]
 
 [[package]]
@@ -1161,7 +1161,7 @@ version = "0.52.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
 dependencies = [
- "windows-targets 0.52.0",
+ "windows-targets 0.52.3",
 ]
 
 [[package]]
@@ -1181,17 +1181,17 @@ dependencies = [
 
 [[package]]
 name = "windows-targets"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8a18201040b24831fbb9e4eb208f8892e1f50a37feb53cc7ff887feb8f50e7cd"
+checksum = "d380ba1dc7187569a8a9e91ed34b8ccfc33123bbacb8c0aed2d1ad7f3ef2dc5f"
 dependencies = [
- "windows_aarch64_gnullvm 0.52.0",
- "windows_aarch64_msvc 0.52.0",
- "windows_i686_gnu 0.52.0",
- "windows_i686_msvc 0.52.0",
- "windows_x86_64_gnu 0.52.0",
- "windows_x86_64_gnullvm 0.52.0",
- "windows_x86_64_msvc 0.52.0",
+ "windows_aarch64_gnullvm 0.52.3",
+ "windows_aarch64_msvc 0.52.3",
+ "windows_i686_gnu 0.52.3",
+ "windows_i686_msvc 0.52.3",
+ "windows_x86_64_gnu 0.52.3",
+ "windows_x86_64_gnullvm 0.52.3",
+ "windows_x86_64_msvc 0.52.3",
 ]
 
 [[package]]
@@ -1202,9 +1202,9 @@ checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
 
 [[package]]
 name = "windows_aarch64_gnullvm"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea"
+checksum = "68e5dcfb9413f53afd9c8f86e56a7b4d86d9a2fa26090ea2dc9e40fba56c6ec6"
 
 [[package]]
 name = "windows_aarch64_msvc"
@@ -1214,9 +1214,9 @@ checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
 
 [[package]]
 name = "windows_aarch64_msvc"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef"
+checksum = "8dab469ebbc45798319e69eebf92308e541ce46760b49b18c6b3fe5e8965b30f"
 
 [[package]]
 name = "windows_i686_gnu"
@@ -1226,9 +1226,9 @@ checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
 
 [[package]]
 name = "windows_i686_gnu"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313"
+checksum = "2a4e9b6a7cac734a8b4138a4e1044eac3404d8326b6c0f939276560687a033fb"
 
 [[package]]
 name = "windows_i686_msvc"
@@ -1238,9 +1238,9 @@ checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
 
 [[package]]
 name = "windows_i686_msvc"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a"
+checksum = "28b0ec9c422ca95ff34a78755cfa6ad4a51371da2a5ace67500cf7ca5f232c58"
 
 [[package]]
 name = "windows_x86_64_gnu"
@@ -1250,9 +1250,9 @@ checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
 
 [[package]]
 name = "windows_x86_64_gnu"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd"
+checksum = "704131571ba93e89d7cd43482277d6632589b18ecf4468f591fbae0a8b101614"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
@@ -1262,9 +1262,9 @@ checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e"
+checksum = "42079295511643151e98d61c38c0acc444e52dd42ab456f7ccfd5152e8ecf21c"
 
 [[package]]
 name = "windows_x86_64_msvc"
@@ -1274,9 +1274,9 @@ checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
 
 [[package]]
 name = "windows_x86_64_msvc"
-version = "0.52.0"
+version = "0.52.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
+checksum = "0770833d60a970638e989b3fa9fd2bb1aaadcf88963d1659fd7d9990196ed2d6"
 
 [[package]]
 name = "zerocopy"
@@ -1295,5 +1295,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.49",
+ "syn 2.0.50",
 ]