fix test suite

memoryleak47 · Oct 17, 2024 · ab05c4d · ab05c4d
1 parent 557f63b
commit ab05c4d
Show file tree

Hide file tree

Showing 16 changed files with 175 additions and 183 deletions.
diff --git a/src/explain/registry.rs b/src/explain/registry.rs
@@ -8,11 +8,11 @@ pub(crate) struct ProofRegistry(Rc<RefCell<HashMap<Equation, ProvenEq>>>);
 fn normalize_eq(eq: &Equation) -> Equation {
     let mut theta = SlotMap::new();
     for x in eq.l.slots() {
-        theta.insert(x, Slot::numeric(theta.len()));
+        theta.insert(x, Slot::numeric(theta.len() as _));
     }
     for x in eq.r.slots() {
         if !theta.contains_key(x) {
-            theta.insert(x, Slot::numeric(theta.len()));
+            theta.insert(x, Slot::numeric(theta.len() as _));
         }
     }
     eq.apply_slotmap(&theta)

diff --git a/tests/arith/rewrite.rs b/tests/arith/rewrite.rs
@@ -24,54 +24,54 @@ pub fn rewrite_arith(eg: &mut EGraph<Arith>) {
 }
 
 fn beta() -> Rewrite<Arith> {
-    let pat = "(app (lam s1 ?b) ?t)";
-    let outpat = "(let s1 ?t ?b)";
+    let pat = "(app (lam $1 ?b) ?t)";
+    let outpat = "(let $1 ?t ?b)";
 
     Rewrite::new("beta", pat, outpat)
 }
 
 fn eta() -> Rewrite<Arith> {
-    let pat = "(lam s1 (app ?b (var s1)))";
+    let pat = "(lam $1 (app ?b (var $1)))";
     let outpat = "?b";
 
     Rewrite::new_if("eta", pat, outpat, |subst| {
-        !subst["b"].slots().contains(&Slot::new(1))
+        !subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn eta_expansion() -> Rewrite<Arith> {
     let pat = "?b";
-    let outpat = "(lam s1 (app ?b (var s1)))";
+    let outpat = "(lam $1 (app ?b (var $1)))";
     Rewrite::new("eta-expansion", pat, outpat)
 }
 
 fn my_let_unused() -> Rewrite<Arith> {
-    let pat = "(let s1 ?t ?b)";
+    let pat = "(let $1 ?t ?b)";
     let outpat = "?b";
     Rewrite::new_if("my-let-unused", pat, outpat, |subst| {
-        !subst["b"].slots().contains(&Slot::new(1))
+        !subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn let_var_same() -> Rewrite<Arith> {
-    let pat = "(let s1 ?e (var s1))";
+    let pat = "(let $1 ?e (var $1))";
     let outpat = "?e";
     Rewrite::new("let-var-same", pat, outpat)
 }
 
 fn let_app() -> Rewrite<Arith> {
-    let pat = "(let s1 ?e (app ?a ?b))";
-    let outpat = "(app (let s1 ?e ?a) (let s1 ?e ?b))";
+    let pat = "(let $1 ?e (app ?a ?b))";
+    let outpat = "(app (let $1 ?e ?a) (let $1 ?e ?b))";
     Rewrite::new_if("let-app", pat, outpat, |subst| {
-        subst["a"].slots().contains(&Slot::new(1)) || subst["b"].slots().contains(&Slot::new(1))
+        subst["a"].slots().contains(&Slot::numeric(1)) || subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn let_lam_diff() -> Rewrite<Arith> {
-    let pat = "(let s1 ?e (lam s2 ?b))";
-    let outpat = "(lam s2 (let s1 ?e ?b))";
+    let pat = "(let $1 ?e (lam $2 ?b))";
+    let outpat = "(lam $2 (let $1 ?e ?b))";
     Rewrite::new_if("let-lam-diff", pat, outpat, |subst| {
-        subst["b"].slots().contains(&Slot::new(1))
+        subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 

diff --git a/tests/arith/tst.rs b/tests/arith/tst.rs
@@ -25,8 +25,8 @@ fn assert_reaches(start: &str, goal: &str, steps: usize) {
 
 #[test]
 fn t1() { // x+y = y+x
-    let x = "s0";
-    let y = "s1";
+    let x = "$0";
+    let y = "$1";
 
     let a = &format!("(add (var {x}) (var {y}))");
     let b = &format!("(add (var {y}) (var {x}))");
@@ -35,9 +35,9 @@ fn t1() { // x+y = y+x
 
 #[test]
 fn t2() { // (x+y) * (x+y) = (x+y) * (y+x)
-    let x = "s0";
-    let y = "s1";
-    let z = "s2";
+    let x = "$0";
+    let y = "$1";
+    let z = "$2";
 
     let a = &format!("(mul (add (var {x}) (var {y})) (add (var {x}) (var {y})))");
     let b = &format!("(mul (add (var {x}) (var {y})) (add (var {y}) (var {x})))");
@@ -47,9 +47,9 @@ fn t2() { // (x+y) * (x+y) = (x+y) * (y+x)
 
 #[test]
 fn t3() { // (x+y) * (y+z) = (z+y) * (y+x)
-    let x = "s0";
-    let y = "s1";
-    let z = "s2";
+    let x = "$0";
+    let y = "$1";
+    let z = "$2";
 
     let a = &format!("(mul (add (var {x}) (var {y})) (add (var {y}) (var {z})))");
     let b = &format!("(mul (add (var {z}) (var {y})) (add (var {y}) (var {x})))");
@@ -58,21 +58,17 @@ fn t3() { // (x+y) * (y+z) = (z+y) * (y+x)
 
 #[test]
 fn t4() { // (x+y)**2 = x**2 + x*y + x*y + y**2
-    let x = "s0";
-    let y = "s1";
-    let z = "s2";
-
-    let a = "(mul (add (var {x}) (var {y})) (add (var {x}) (var {y})))";
-    let b = "(add (mul (var {x}) (var {x}))
-             (add (mul (var {x}) (var {y}))
-             (add (mul (var {x}) (var {y}))
-                  (mul (var {y}) (var {y}))
+    let a = "(mul (add (var $x) (var $y)) (add (var $x) (var $y)))";
+    let b = "(add (mul (var $x) (var $x))
+             (add (mul (var $x) (var $y))
+             (add (mul (var $x) (var $y))
+                  (mul (var $y) (var $y))
              )))";
     assert_reaches(a, b, 10);
 }
 
 fn add_chain(it: impl Iterator<Item=usize>) -> String {
-    let mut it = it.map(|u| format!("(var s{u})"));
+    let mut it = it.map(|u| format!("(var ${u})"));
     let mut x = format!("{}", it.next().unwrap());
     for y in it {
         x = format!("(add {x} {y})");
@@ -94,9 +90,9 @@ fn t5() { // x0+...+xN = xN+...+x0
 
 #[test]
 fn t6() { // z*(x+y) = z*(y+x)
-    let x = "s0";
-    let y = "s1";
-    let z = "s2";
+    let x = "$0";
+    let y = "$1";
+    let z = "$2";
 
     let a = &format!("(mul (var {z}) (add (var {x}) (var {y})))");
     let b = &format!("(mul (var {z}) (add (var {y}) (var {x})))");

diff --git a/tests/array/rewrite.rs b/tests/array/rewrite.rs
@@ -44,61 +44,61 @@ fn rew(name: &str, s1: &str, s2: &str) -> Rewrite<Array> {
 //////////////////////
 
 fn beta() -> Rewrite<Array> {
-    let pat = "(app (lam s1 ?body) ?e)";
-    let outpat = "(let s1 ?e ?body)";
+    let pat = "(app (lam $1 ?body) ?e)";
+    let outpat = "(let $1 ?e ?body)";
 
     Rewrite::new("beta", pat, outpat)
 }
 
 fn eta() -> Rewrite<Array> {
-    let pat = "(lam s1 (app ?f (var s1)))";
+    let pat = "(lam $1 (app ?f (var $1)))";
     let outpat = "?f";
 
     Rewrite::new_if("eta", pat, outpat, |subst| {
-        !subst["f"].slots().contains(&Slot::new(1))
+        !subst["f"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn my_let_unused() -> Rewrite<Array> {
-    let pat = "(let s1 ?t ?b)";
+    let pat = "(let $1 ?t ?b)";
     let outpat = "?b";
     Rewrite::new_if("my-let-unused", pat, outpat, |subst| {
-        !subst["b"].slots().contains(&Slot::new(1))
+        !subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn let_var_same() -> Rewrite<Array> {
-    let pat = "(let s1 ?e (var s1))";
+    let pat = "(let $1 ?e (var $1))";
     let outpat = "?e";
     Rewrite::new("let-var-same", pat, outpat)
 }
 
 fn let_var_diff() -> Rewrite<Array> {
-    let pat = "(let s1 ?e (var s2))";
-    let outpat = "(var s2)";
+    let pat = "(let $1 ?e (var $2))";
+    let outpat = "(var $2)";
     Rewrite::new("let-var-diff", pat, outpat)
 }
 
 fn let_app() -> Rewrite<Array> {
-    let pat = "(let s1 ?e (app ?a ?b))";
-    let outpat = "(app (let s1 ?e ?a) (let s1 ?e ?b))";
+    let pat = "(let $1 ?e (app ?a ?b))";
+    let outpat = "(app (let $1 ?e ?a) (let $1 ?e ?b))";
     Rewrite::new_if("let-app", pat, outpat, |subst| {
-        subst["a"].slots().contains(&Slot::new(1)) || subst["b"].slots().contains(&Slot::new(1))
+        subst["a"].slots().contains(&Slot::numeric(1)) || subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn let_lam_diff() -> Rewrite<Array> {
-    let pat = "(let s1 ?e (lam s2 ?body))";
-    let outpat = "(lam s2 (let s1 ?e ?body))";
+    let pat = "(let $1 ?e (lam $2 ?body))";
+    let outpat = "(lam $2 (let $1 ?e ?body))";
     Rewrite::new_if("let-lam-diff", pat, outpat, |subst| {
-        subst["body"].slots().contains(&Slot::new(1))
+        subst["body"].slots().contains(&Slot::numeric(1))
     })
 }
 
 /////////////////////
 
 fn map_fusion() -> Rewrite<Array> {
-    let mfu = "s0";
+    let mfu = "$0";
     let pat = "(app (app (app m ?nn) ?f) (app (app (app m ?nn) ?g) ?arg))";
     let outpat = &format!("(app (app (app m ?nn) (lam {mfu} (app ?f (app ?g (var {mfu}))))) ?arg)");
     Rewrite::new("map-fusion", pat, outpat)
@@ -109,14 +109,14 @@ fn map_fission() -> Rewrite<Array> {
     let mfi = 1;
 
     let pat = &format!(
-        "(app (app m ?nn) (lam s{x} (app ?f ?gx)))"
+        "(app (app m ?nn) (lam ${x} (app ?f ?gx)))"
     );
 
     let outpat = &format!(
-        "(lam s{mfi} (app (app (app m ?nn) ?f) (app (app (app m ?nn) (lam s{x} ?gx)) (var s{mfi}))))"
+        "(lam ${mfi} (app (app (app m ?nn) ?f) (app (app (app m ?nn) (lam ${x} ?gx)) (var ${mfi}))))"
     );
 
     Rewrite::new_if("map-fission", pat, outpat, move |subst| {
-        !subst["f"].slots().contains(&Slot::new(x))
+        !subst["f"].slots().contains(&Slot::numeric(x))
     })
 }
diff --git a/tests/fgh/mod.rs b/tests/fgh/mod.rs
@@ -53,8 +53,8 @@ impl Language for Fgh {
 #[test]
 fn transitive_symmetry() {
     let eg: &mut EGraph<Fgh> = &mut EGraph::new();
-    equate("(f s1 s2)", "(g s2 s1)", eg);
-    equate("(g s1 s2)", "(h s1 s2)", eg);
+    equate("(f $1 $2)", "(g $2 $1)", eg);
+    equate("(g $1 $2)", "(h $1 $2)", eg);
     eg.dump();
-    explain("(f s1 s2)", "(h s2 s1)", eg);
+    explain("(f $1 $2)", "(h $2 $1)", eg);
 }
diff --git a/tests/lambda/big_step.rs b/tests/lambda/big_step.rs
@@ -26,7 +26,7 @@ pub fn rewrite_big_step(eg: &mut EGraph<Lambda>) {
 
         let Lambda::App(l, t) = cand.app.clone() else { panic!() };
         let Lambda::Lam(x, b) = cand.lam.clone() else { panic!() };
-        assert_eq!(x, Slot::new(0));
+        assert_eq!(x, Slot::numeric(0));
 
         // l.m :: slots(lam) -> slots(app)
         let mut m = l.m.clone();

diff --git a/tests/lambda/build.rs b/tests/lambda/build.rs
@@ -2,16 +2,16 @@ use crate::lambda::*;
 
 // The Y combinator.
 pub fn y() -> String {
-    let a = format!("(lam s0 (app (var s1) (app (var s0) (var s0))))");
+    let a = format!("(lam $0 (app (var $1) (app (var $0) (var $0))))");
 
-    format!("(lam s1 (app {a} {a}))") }
+    format!("(lam $1 (app {a} {a}))") }
 
 pub fn zero() -> String {
-    format!("(lam s0 (lam s1 (var s0)))")
+    format!("(lam $0 (lam $1 (var $0)))")
 }
 
 pub fn suc() -> String {
-    format!("(lam s0 (lam s1 (lam s2 (app (var s2) (var s0)))))")
+    format!("(lam $0 (lam $1 (lam $2 (app (var $2) (var $0)))))")
 }
 
 pub fn num(x: u32) -> String {
@@ -38,10 +38,10 @@ pub fn add() -> String {
 
 pub fn add_impl() -> String {
     let s = suc();
-    let add = "s0";
-    let x = "s1";
-    let y = "s2";
-    let z = "s3";
+    let add = "$0";
+    let x = "$1";
+    let y = "$2";
+    let z = "$3";
 
     format!("(lam {add} (lam {x} (lam {y}
         (app (app (var {x}) (var {y})) (lam {z} (app (app (var {add}) (var {z})) (app {s} (var {y})))))

diff --git a/tests/lambda/lambda_small_step.rs b/tests/lambda/lambda_small_step.rs
@@ -22,7 +22,7 @@ pub fn rewrite_small_step(eg: &mut EGraph<Lambda>) {
 
         let Lambda::App(l, t) = cand.app.clone() else { panic!() };
         let Lambda::Lam(x, b) = cand.lam.clone() else { panic!() };
-        assert_eq!(x, Slot::new(0));
+        assert_eq!(x, Slot::numeric(0));
 
         // b.m :: slots(b.id) -> L1
         // l.m :: slots(l.id) -> L0 (and thus L1 -> L0)

diff --git a/tests/lambda/let_small_step.rs b/tests/lambda/let_small_step.rs
@@ -22,37 +22,37 @@ pub fn rewrite_let(eg: &mut EGraph<Lambda>) {
 }
 
 fn beta() -> Rewrite<Lambda> {
-    let pat = "(app (lam s1 ?b) ?t)";
-    let outpat = "(let s1 ?t ?b)";
+    let pat = "(app (lam $1 ?b) ?t)";
+    let outpat = "(let $1 ?t ?b)";
     Rewrite::new("beta", pat, outpat)
 }
 
 fn my_let_unused() -> Rewrite<Lambda> {
-    let pat = "(let s1 ?t ?b)";
+    let pat = "(let $1 ?t ?b)";
     let outpat = "?b";
     Rewrite::new_if("my-let-unused", pat, outpat, |subst| {
-        !subst["b"].slots().contains(&Slot::new(1))
+        !subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn let_var_same() -> Rewrite<Lambda> {
-    let pat = "(let s1 ?e (var s1))";
+    let pat = "(let $1 ?e (var $1))";
     let outpat = "?e";
     Rewrite::new("let-var-same", pat, outpat)
 }
 
 fn let_app() -> Rewrite<Lambda> {
-    let pat = "(let s1 ?e (app ?a ?b))";
-    let outpat = "(app (let s1 ?e ?a) (let s1 ?e ?b))";
+    let pat = "(let $1 ?e (app ?a ?b))";
+    let outpat = "(app (let $1 ?e ?a) (let $1 ?e ?b))";
     Rewrite::new_if("let-app", pat, outpat, |subst| {
-        subst["a"].slots().contains(&Slot::new(1)) || subst["b"].slots().contains(&Slot::new(1))
+        subst["a"].slots().contains(&Slot::numeric(1)) || subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
 
 fn let_lam_diff() -> Rewrite<Lambda> {
-    let pat = "(let s1 ?e (lam s2 ?b))";
-    let outpat = "(lam s2 (let s1 ?e ?b))";
+    let pat = "(let $1 ?e (lam $2 ?b))";
+    let outpat = "(lam $2 (let $1 ?e ?b))";
     Rewrite::new_if("let-lam-diff", pat, outpat, |subst| {
-        subst["b"].slots().contains(&Slot::new(1))
+        subst["b"].slots().contains(&Slot::numeric(1))
     })
 }
diff --git a/tests/lambda/normalize.rs b/tests/lambda/normalize.rs
@@ -8,7 +8,7 @@ pub fn lam_normalize(re: &RecExpr<Lambda>) -> RecExpr<Lambda> {
 // map :: original name -> normalized name.
 fn lam_normalize_impl(re: &RecExpr<Lambda>, counter: &mut usize, map: HashMap<Slot, Slot>) -> RecExpr<Lambda> {
     let mut alloc_slot = || {
-        let out = Slot::new(*counter);
+        let out = Slot::numeric(*counter as _);
         *counter += 1;
         out
     };

diff --git a/tests/lambda/step.rs b/tests/lambda/step.rs
@@ -76,7 +76,7 @@ fn lam_subst(re: &RecExpr<Lambda>, x: Slot, t: &RecExpr<Lambda>) -> RecExpr<Lamb
                 let mut b: RecExpr<Lambda> = b.clone();
 
                 if f.contains(&y) {
-                    let y2 = (0..).map(|i| Slot::new(i))
+                    let y2 = (0..).map(|i| Slot::numeric(i))
                                   .filter(|i| !f.contains(i))
                                   .next()
                                   .unwrap();