Faster proof encoding: congruence via :merge + single self-referential UF (~1.8x)

egglog-experimental/src/fresh_macro.rs

@@ -89,6 +89,7 @@ fn desugar_fresh_rule(
         schema: Schema {
             input: schema,
             output: output_sort,
+            extra_outputs: vec![],
         },
         cost: first_opts.cost,
         unextractable: first_opts.unextractable,

egglog-experimental/src/primitive.rs

@@ -263,6 +263,8 @@ fn required_context(egraph: &mut EGraph, expr: &ResolvedExpr) -> Context {
                     }
                 }
                 ResolvedCall::Primitive(_) => Context::Pure,
+                // `values` builds/destructures a tuple value; it reads or writes no tables.
+                ResolvedCall::Values(_) => Context::Pure,
                 ResolvedCall::Func(func) => match func.subtype {
                     FunctionSubtype::Constructor => Context::Write,
                     FunctionSubtype::Custom => Context::Read,

egglog/CHANGELOG.md

@@ -2,6 +2,27 @@
 
 ## [Unreleased] - ReleaseDate
 
+- **Single self-referential union-find (proof mode).** The proof term encoding now
+  represents each sort's union-find as one native-tuple function `@UF : (S) -> (S, Proof)`
+  (parent + a proof `key = parent`) with a self-referential `:merge`, replacing the former
+  two-table `@UF_S (S S) -> Proof` relation plus `@UF_Sf` index. Constructor-view congruence
+  and the UF self-merge both keep the smaller e-class and stage an oriented displaced edge,
+  so the `single_parent`/`uf_function_index` rules and per-term self-loop seeds are gone. This
+  mirrors the term (non-proof) encoding's single-table `@UF : (S) -> S`.
+- **Tuple-output functions.** A function may declare more than one output sort, e.g.
+  `(function interval (Math) (i64 i64) :merge (values (max old0 new0) (min old1 new1)))`. Such a
+  function stores its outputs as separate value columns; the functional dependency is
+  `keys -> (value0, value1, ...)`. Outputs are destructured in queries with
+  `(= (values lo hi) (interval x))`, written with `(set (interval x) (values 0 100))`, and merged
+  with a `(values ...)` clause whose `i`-th element merges column `i` using the bound variables
+  `old0`, `new0`, `old1`, `new1`, .... Tuple outputs are only allowed for plain functions (not
+  constructors, relations, or view tables) and are not supported by the term/proof encoding.
+- Built-in keywords (most command, action, and schedule heads such as `function`, `set`, `union`,
+  `rule`, `run`, ..., plus the tuple constructor `values`) are now reserved and may no longer be
+  used as user identifiers (function/sort/constructor/relation/variant names or variables). Names
+  starting with `:` are likewise reserved, since that prefix marks option keywords (`:merge`,
+  `:cost`, ...). The common-word commands `input` and `output` are only partially reserved: they
+  remain usable as variables, but not as definition names or as the head of a call expression.
 - Add typed `EGraph` extension state that clones with `EGraph` and is restored by `push`/`pop`.
 - Report full source file paths in egglog span and error messages.
 - Fix seminaive matching after nested containers rebuild in place by propagating dirty container ids through parent containers.

egglog/core-relations/src/free_join/mod.rs

@@ -607,7 +607,16 @@ impl Database {
         while !to_merge.is_empty() {
             for table_id in to_merge.iter().copied() {
                 let mut info = self.tables.unwrap_val(table_id);
-                let mut es = ExecutionState::new(self.read_only_view(), Default::default());
+                // Pre-seed the table's OWN buffer so a self-referential merge — one that stages a
+                // write back into its own table (e.g. the term encoder's `@UF` recursive
+                // parent-union) — can stage it. The table has been `unwrap_val`'d out of
+                // `self.tables`, so the lazy `new_buffer()` path (which indexes `self.tables`) would
+                // fail for the self id. Staged rows land in `pending_state` and are picked up on the
+                // next fixpoint iteration of this loop. Non-self-referential merges get an empty,
+                // never-touched buffer. (The strata path in `merge_all` handles this via write-deps.)
+                let mut bufs = DenseIdMap::default();
+                bufs.insert(table_id, info.table.new_buffer());
+                let mut es = ExecutionState::new(self.read_only_view(), bufs);
                 changed |= info.table.merge(&mut es).added || es.changed;
                 self.tables.insert(table_id, info);
             }