Proofs refactors

Cargo.toml

@@ -7,6 +7,7 @@ members = [
   "egglog-bridge",
   "numeric-id",
   "union-find",
+  "tests/proof_api",
   "src/sort/add_primitive",
   "wasm-example"
 ]

Makefile

@@ -8,9 +8,9 @@ WWW=${PWD}/target/www
 all: test nits docs
 
 test:
-	cargo nextest run --release
+	cargo nextest run --workspace --all-features --release
 	# nextest doesn't run doctests, so do it here
-	cargo test --doc --release
+	cargo test --workspace --all-features --doc --release
 
 nits:
 	@rustup component add clippy

core-relations/src/action/mod.rs

@@ -112,7 +112,8 @@ pub(crate) struct Bindings {
 impl std::ops::Index<Variable> for Bindings {
     type Output = [Value];
     fn index(&self, var: Variable) -> &[Value] {
-        self.get(var).unwrap()
+        self.get(var)
+            .unwrap_or_else(|| panic!("Bindings missing value for variable {:?}", var))
     }
 }
 
@@ -632,7 +633,8 @@ impl ExecutionState<'_> {
                                                 bindings[*v][offset]
                                             }
                                             WriteVal::IncCounter(ctr) => {
-                                                Value::from_usize(ctrs.inc(*ctr))
+                                                let res = ctrs.inc(*ctr);
+                                                Value::from_usize(res)
                                             }
                                             WriteVal::CurrentVal(ix) => row[*ix],
                                         };
@@ -743,6 +745,37 @@ impl ExecutionState<'_> {
                     }
                 }
             },
+            Instr::InsertIfNe { table, l, r, vals } => match (l, r) {
+                (QueryEntry::Var(v1), QueryEntry::Var(v2)) => {
+                    for_each_binding_with_mask!(mask, vals.as_slice(), bindings, |iter| {
+                        iter.zip(&bindings[*v1])
+                            .zip(&bindings[*v2])
+                            .for_each(|((vals, v1), v2)| {
+                                if v1 != v2 {
+                                    self.stage_insert(*table, &vals);
+                                }
+                            })
+                    })
+                }
+                (QueryEntry::Var(v), QueryEntry::Const(c))
+                | (QueryEntry::Const(c), QueryEntry::Var(v)) => {
+                    for_each_binding_with_mask!(mask, vals.as_slice(), bindings, |iter| {
+                        iter.zip(&bindings[*v]).for_each(|(vals, cond)| {
+                            if cond != c {
+                                self.stage_insert(*table, &vals);
+                            }
+                        })
+                    })
+                }
+                (QueryEntry::Const(c1), QueryEntry::Const(c2)) => {
+                    if c1 != c2 {
+                        for_each_binding_with_mask!(mask, vals.as_slice(), bindings, |iter| iter
+                            .for_each(|vals| {
+                                self.stage_insert(*table, &vals);
+                            }))
+                    }
+                }
+            },
             Instr::Remove { table, args } => {
                 for_each_binding_with_mask!(mask, args.as_slice(), bindings, |iter| {
                     iter.for_each(|args| {
@@ -866,6 +899,14 @@ pub(crate) enum Instr {
         vals: Vec<QueryEntry>,
     },
 
+    /// Insert `vals` into `table` if `l` and `r` are not equal.
+    InsertIfNe {
+        table: TableId,
+        l: QueryEntry,
+        r: QueryEntry,
+        vals: Vec<QueryEntry>,
+    },
+
     /// Remove the entry corresponding to `args` in `func`.
     Remove {
         table: TableId,

core-relations/src/base_values/mod.rs

@@ -79,6 +79,17 @@ impl BaseValues {
         id
     }
 
+    /// Get the underlying `P` represented by the [`Value`] `v`, assuming it's type `ty` matches
+    /// the [`BaseValueId`] for `P`.
+    ///
+    /// This method does not panic if `P` was never registered as a type in this [`BaseValues`]
+    /// instance.
+    pub fn try_get_as<P: BaseValue>(&self, v: Value, ty: BaseValueId) -> Option<P> {
+        self.type_ids
+            .get(&TypeId::of::<P>())
+            .and_then(|&id| (id == ty).then_some(self.unwrap::<P>(v)))
+    }
+
     /// Get the [`BaseValueId`] for the given base value type `P`.
     pub fn get_ty<P: BaseValue>(&self) -> BaseValueId {
         self.type_ids[&TypeId::of::<P>()]

core-relations/src/base_values/tests.rs

@@ -268,7 +268,7 @@ fn roundtrip_medium_integers_interned() {
     // Test large isize values (need interning on 64-bit systems)
     bases.register_type::<isize>();
     if std::mem::size_of::<isize>() == 8 {
-        for val in [-2147483649isize, isize::MIN, isize::MAX] {
+        for val in [isize::MIN, isize::MAX] {
             let boxed = bases.get(val);
             let unboxed = bases.unwrap::<isize>(boxed);
             assert_eq!(val, unboxed);

core-relations/src/common.rs

@@ -103,8 +103,8 @@ impl<K: NumericId, V> Clear for DenseIdMap<K, V> {
 define_id!(pub Value, u32, "A generic identifier representing an egglog value");
 
 impl Value {
-    pub(crate) fn stale() -> Self {
-        Value::new(u32::MAX)
+    pub(crate) const fn stale() -> Self {
+        Value::new_const(u32::MAX)
     }
     /// Values have a special "Stale" value that is used to indicate that the
     /// value isn't intended to be read.

core-relations/src/free_join/mod.rs

@@ -435,7 +435,14 @@ impl Database {
     ///
     /// These counters can be used to generate unique ids as part of an action.
     pub fn add_counter(&mut self) -> CounterId {
-        self.counters.0.push(AtomicUsize::new(0))
+        self.add_counter_with_initial_val(0)
+    }
+
+    /// Create a new counter for this database starting at the given `val`.
+    ///
+    /// These counters can be used to generate unique ids as part of an action.
+    pub fn add_counter_with_initial_val(&mut self, val: usize) -> CounterId {
+        self.counters.0.push(AtomicUsize::new(val))
     }
 
     /// Increment the given counter and return its previous value.

core-relations/src/query.rs

@@ -455,14 +455,14 @@ impl RuleBuilder<'_, '_> {
                 None
             }
         }));
+        let desc: String = desc.into();
         let action_id = self.qb.rsb.rule_set.actions.push(ActionInfo {
             instrs: Arc::new(self.qb.instrs),
             used_vars,
         });
         self.qb.query.action = action_id;
         // Plan the query
         let plan = self.qb.rsb.db.plan_query(self.qb.query);
-        let desc: String = desc.into();
         // Add it to the ruleset.
         self.qb
             .rsb
@@ -601,6 +601,28 @@ impl RuleBuilder<'_, '_> {
         Ok(())
     }
 
+    /// Insert the specified values into the given table if `l` and `r` are not
+    /// equal.
+    pub fn insert_if_ne(
+        &mut self,
+        table: TableId,
+        l: QueryEntry,
+        r: QueryEntry,
+        vals: &[QueryEntry],
+    ) -> Result<(), QueryError> {
+        let table_info = self.table_info(table);
+        self.validate_row(table, table_info, vals)?;
+        self.qb.instrs.push(Instr::InsertIfNe {
+            table,
+            l,
+            r,
+            vals: vals.to_vec(),
+        });
+        self.qb
+            .mark_used(vals.iter().chain(once(&l)).chain(once(&r)));
+        Ok(())
+    }
+
     /// Remove the specified entry from the given table, if it is there.
     pub fn remove(&mut self, table: TableId, args: &[QueryEntry]) -> Result<(), QueryError> {
         let table_info = self.table_info(table);

core-relations/src/table_spec.rs

@@ -135,6 +135,7 @@ pub trait Rebuilder: Send + Sync {
 }
 
 /// A row in a table.
+#[derive(Debug)]
 pub struct Row {
     /// The id associated with the row.
     pub id: RowId,

core-relations/src/tests.rs

@@ -1082,3 +1082,135 @@ fn call_external_with_fallback() {
     h_contents.sort();
     assert_eq!(h_contents, vec![vec![v(2), v(0)], vec![v(4), v(0)],]);
 }
+
+#[test]
+fn insert_if_ne_with_vars() {
+    fn make_two_col_table() -> SortedWritesTable {
+        SortedWritesTable::new(
+            2,
+            2,
+            None,
+            vec![],
+            Box::new(move |_, a, b, _| {
+                if a != b {
+                    panic!("merge not supported")
+                } else {
+                    false
+                }
+            }),
+        )
+    }
+    let mut db = Database::default();
+    let pairs = db.add_table(make_two_col_table(), iter::empty(), iter::empty());
+    let output = db.add_table(make_two_col_table(), iter::empty(), iter::empty());
+
+    {
+        let mut buf = db.get_table(pairs).new_buffer();
+        buf.stage_insert(&[v(1), v(1)]);
+        buf.stage_insert(&[v(1), v(2)]);
+        buf.stage_insert(&[v(2), v(3)]);
+        buf.stage_insert(&[v(4), v(4)]);
+    }
+    db.merge_all();
+
+    let mut rsb = RuleSetBuilder::new(&mut db);
+    let mut query = rsb.new_rule();
+    let x = query.new_var_named("x");
+    let y = query.new_var_named("y");
+    query.add_atom(pairs, &[x.into(), y.into()], &[]).unwrap();
+    let mut rb = query.build();
+    rb.insert_if_ne(output, x.into(), y.into(), &[x.into(), y.into()])
+        .unwrap();
+    rb.build();
+    let rs = rsb.build();
+    assert!(db.run_rule_set(&rs, ReportLevel::TimeOnly).changed);
+
+    let out = db.get_table(output);
+    let all = out.all();
+    let mut contents = out
+        .scan(all.as_ref())
+        .iter()
+        .map(|(_, row)| row.to_vec())
+        .collect::<Vec<_>>();
+    contents.sort();
+    assert_eq!(contents, vec![vec![v(1), v(2)], vec![v(2), v(3)]]);
+}
+
+#[test]
+fn insert_if_ne_consts_and_vars() {
+    fn make_one_col_table() -> SortedWritesTable {
+        SortedWritesTable::new(
+            1,
+            1,
+            None,
+            vec![],
+            Box::new(move |_, a, b, _| {
+                if a != b {
+                    panic!("merge not supported")
+                } else {
+                    false
+                }
+            }),
+        )
+    }
+    fn make_two_col_table() -> SortedWritesTable {
+        SortedWritesTable::new(
+            2,
+            2,
+            None,
+            vec![],
+            Box::new(move |_, a, b, _| {
+                if a != b {
+                    panic!("merge not supported")
+                } else {
+                    false
+                }
+            }),
+        )
+    }
+
+    let mut db = Database::default();
+    let source = db.add_table(make_one_col_table(), iter::empty(), iter::empty());
+    let output = db.add_table(make_two_col_table(), iter::empty(), iter::empty());
+    {
+        let mut buf = db.get_table(source).new_buffer();
+        buf.stage_insert(&[v(0)]);
+        buf.stage_insert(&[v(1)]);
+    }
+    db.merge_all();
+
+    let mut rsb = RuleSetBuilder::new(&mut db);
+    let mut query = rsb.new_rule();
+    let x = query.new_var_named("x");
+    query.add_atom(source, &[x.into()], &[]).unwrap();
+    let mut rb = query.build();
+    rb.insert_if_ne(output, x.into(), v(1).into(), &[x.into(), v(10).into()])
+        .unwrap();
+    rb.insert_if_ne(
+        output,
+        v(2).into(),
+        v(2).into(),
+        &[v(2).into(), v(2).into()],
+    )
+    .unwrap();
+    rb.insert_if_ne(
+        output,
+        v(3).into(),
+        v(4).into(),
+        &[v(3).into(), v(4).into()],
+    )
+    .unwrap();
+    rb.build();
+    let rs = rsb.build();
+    assert!(db.run_rule_set(&rs, ReportLevel::TimeOnly).changed);
+
+    let output = db.get_table(output);
+    let all = output.all();
+    let mut contents = output
+        .scan(all.as_ref())
+        .iter()
+        .map(|(_, row)| row.to_vec())
+        .collect::<Vec<_>>();
+    contents.sort();
+    assert_eq!(contents, vec![vec![v(0), v(10)], vec![v(3), v(4)]]);
+}

egglog-ast/src/generic_ast.rs

@@ -21,6 +21,8 @@ pub enum GenericExpr<Head, Leaf> {
     Lit(Span, Literal),
 }
 
+pub type Expr = GenericExpr<String, String>;
+
 /// Facts are the left-hand side of a [`Command::Rule`].
 /// They represent a part of a database query.
 /// Facts can be expressions or equality constraints between expressions.

egglog-ast/src/generic_ast_helpers.rs

@@ -157,7 +157,11 @@ where
             GenericExpr::Lit(_ann, lit) => write!(f, "{lit}"),
             GenericExpr::Var(_ann, var) => write!(f, "{var}"),
             GenericExpr::Call(_ann, op, children) => {
-                write!(f, "({} {})", op, ListDisplay(children, " "))
+                if children.is_empty() {
+                    write!(f, "({})", op)
+                } else {
+                    write!(f, "({} {})", op, ListDisplay(children, " "))
+                }
             }
         }
     }

egglog-bridge/Cargo.toml

@@ -13,6 +13,7 @@ egglog-core-relations = { workspace = true }
 egglog-numeric-id = { workspace = true }
 egglog-union-find = { workspace = true }
 egglog-reports = { workspace = true }
+egglog-ast = { workspace = true }
 hashbrown = { workspace = true }
 smallvec = { workspace = true }
 thiserror = { workspace = true }