From 619f801fdc6d9a8402c7fc86b66ba5d09344520d Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Thu, 2 Jul 2026 18:32:32 +0000 Subject: [PATCH 1/4] Port tuple-output functions from egglog#938 Ports egraphs-good/egglog#938 ("Add tuple-output functions") into the vendored egglog/ subtree. A function may declare more than one output sort, stored as separate value columns (no boxing); outputs are destructured in queries, written in actions, and merged per column with a (values ...) clause. Restricted to plain functions and unsupported by the term/proof encoding. The upstream diff applied cleanly except for one context conflict in src/proofs/proof_encoding_helpers.rs (this fork carries an extra NaiveEqSortPrimitiveFact reason); the TupleOutputFunction variant and guard were reapplied by hand. Co-Authored-By: Claude Opus 4.8 --- egglog/CHANGELOG.md | 14 ++ egglog/egglog-bridge/src/lib.rs | 193 +++++++++++++----- egglog/egglog-bridge/src/rule.rs | 21 +- egglog/src/ast/desugar.rs | 4 + egglog/src/ast/mod.rs | 184 +++++++++++++++-- egglog/src/ast/parse.rs | 151 ++++++++++++-- egglog/src/ast/proof_global_remover.rs | 3 + egglog/src/ast/remove_globals.rs | 3 + egglog/src/constraint.rs | 54 +++-- egglog/src/core.rs | 135 +++++++++++-- egglog/src/exec_state.rs | 3 + egglog/src/extract.rs | 23 ++- egglog/src/lib.rs | 103 ++++++++-- egglog/src/prelude.rs | 1 + egglog/src/proofs/proof_checker.rs | 2 + egglog/src/proofs/proof_encoding.rs | 6 + egglog/src/proofs/proof_encoding_helpers.rs | 10 + egglog/src/proofs/proof_extraction.rs | 3 + egglog/src/typechecking.rs | 197 +++++++++++++++---- egglog/src/util.rs | 1 + egglog/tests/tuple_outputs.rs | 207 ++++++++++++++++++++ 21 files changed, 1128 insertions(+), 190 deletions(-) create mode 100644 egglog/tests/tuple_outputs.rs diff --git a/egglog/CHANGELOG.md b/egglog/CHANGELOG.md index 5bf6fe5..bebcfb0 100644 --- a/egglog/CHANGELOG.md +++ b/egglog/CHANGELOG.md @@ -2,6 +2,20 @@ ## [Unreleased] - ReleaseDate +- **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 (no boxing); 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. diff --git a/egglog/egglog-bridge/src/lib.rs b/egglog/egglog-bridge/src/lib.rs index ed42721..69fe57e 100644 --- a/egglog/egglog-bridge/src/lib.rs +++ b/egglog/egglog-bridge/src/lib.rs @@ -332,10 +332,7 @@ impl EGraph { let mut bufs = DenseIdMap::default(); for (func, row) in values.into_iter() { let table_info = &self.funcs[func]; - let schema_math = SchemaMath { - subsume: table_info.can_subsume, - func_cols: table_info.schema.len(), - }; + let schema_math = table_info.schema_math(); let table_id = table_info.table; extended_row.extend_from_slice(&row); schema_math.write_table_row( @@ -362,10 +359,7 @@ impl EGraph { /// This method panics if the values do not match the arity of the function. pub fn add_term(&mut self, func: FunctionId, inputs: &[Value]) -> Value { let info = &self.funcs[func]; - let schema_math = SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - }; + let schema_math = info.schema_math(); let mut extended_row = Vec::new(); extended_row.extend_from_slice(inputs); let res = self.fresh_id(); @@ -388,10 +382,7 @@ impl EGraph { /// (`key`). pub fn lookup_id(&self, func: FunctionId, key: &[Value]) -> Option { let info = &self.funcs[func]; - let schema_math = SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - }; + let schema_math = info.schema_math(); let table_id = info.table; let table = self.db.get_table(table_id); let row = table.get_row(key)?; @@ -438,10 +429,7 @@ impl EGraph { pub fn for_each_while(&self, table: FunctionId, mut f: impl FnMut(ScanEntry<'_>) -> bool) { let info = &self.funcs[table]; let table = self.funcs[table].table; - let schema_math = SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - }; + let schema_math = info.schema_math(); let imp = self.db.get_table(table); let all = imp.all(); let mut cur = Offset::new(0); @@ -522,8 +510,21 @@ impl EGraph { .filter(|(_, ty)| matches!(ty, ColumnTy::Id)) .map(|(i, _)| ColumnId::from_usize(i)) .collect(); + // The number of value (return) columns is determined by the merge: a `Columns` merge has + // one entry per value column, every other merge applies to a single value column. + let n_vals = match &merge { + MergeFn::Columns(cols) => cols.len(), + _ => 1, + }; + assert!( + schema.len() >= n_vals, + "function {name} has fewer columns ({}) than value columns ({n_vals})", + schema.len() + ); + let n_keys = schema.len() - n_vals; let schema_math = SchemaMath { subsume: can_subsume, + n_keys, func_cols: schema.len(), }; let n_args = schema_math.num_keys(); @@ -551,6 +552,7 @@ impl EGraph { let res = self.funcs.push(FunctionInfo { table: table_id, schema: schema.clone(), + n_keys, incremental_rebuild_rules: Default::default(), nonincremental_rebuild_rule: RuleId::new(!0), default_val: default, @@ -995,6 +997,9 @@ struct CachedPlanInfo { struct FunctionInfo { table: TableId, schema: Vec, + /// The number of key (input) columns. The remaining columns of `schema` are value/return + /// columns (one for most functions, more for tuple-output functions). + n_keys: usize, incremental_rebuild_rules: Vec, nonincremental_rebuild_rule: RuleId, default_val: DefaultVal, @@ -1002,6 +1007,16 @@ struct FunctionInfo { name: Arc, } +impl FunctionInfo { + fn schema_math(&self) -> SchemaMath { + SchemaMath { + subsume: self.can_subsume, + n_keys: self.n_keys, + func_cols: self.schema.len(), + } + } +} + impl FunctionInfo { fn ret_ty(&self) -> ColumnTy { self.schema.last().copied().unwrap() @@ -1031,14 +1046,24 @@ pub enum MergeFn { /// The output of a merge is determined by looking up the value for the given function and the /// given arguments in the egraph. Function(FunctionId, Vec), - /// Always return the old value for the given function. + /// Always return the old value for the given function (this column's old value). Old, - /// Always return the new value for the given function. + /// Always return the new value for the given function (this column's new value). New, + /// The old value of the `i`th value column. Used by tuple-output merges, where a column's + /// merge may reference any output column of the old row. + OldCol(usize), + /// The new value of the `i`th value column. + NewCol(usize), /// Always overwrite the new value for the given function with a constant. This is more useful /// as a "base case" in a more complicated merge function (e.g. one that clamps a value between /// 1 and 100) than it is as a standalone merge function. Const(Value), + /// A merge for a tuple-output function: one [`MergeFn`] per value column. Each inner + /// `MergeFn` produces that column's merged value and may reference any column via + /// [`MergeFn::OldCol`] / [`MergeFn::NewCol`]. The length determines the number of value + /// columns of the function. + Columns(Vec), } impl MergeFn { @@ -1064,7 +1089,11 @@ impl MergeFn { UnionId => { write_deps.insert(egraph.uf_table); } - AssertEq | Old | New | Const(..) => {} + Columns(cols) => { + cols.iter() + .for_each(|col| col.fill_deps(egraph, read_deps, write_deps)); + } + AssertEq | Old | New | OldCol(..) | NewCol(..) | Const(..) => {} } } @@ -1074,20 +1103,26 @@ impl MergeFn { function_name: &str, egraph: &mut EGraph, ) -> Box { - let resolved = self.resolve(function_name, egraph); + let resolved = self.resolve_columns(function_name, egraph); + assert_eq!( + resolved.len(), + schema_math.n_vals(), + "merge for {function_name} must have one entry per value column" + ); Box::new(move |state, cur, new, out| { let timestamp = new[schema_math.ts_col()]; let mut changed = false; - let ret_val = { - let cur = cur[schema_math.ret_val_col()]; - let new = new[schema_math.ret_val_col()]; - let out = resolved.run(state, cur, new, timestamp); - changed |= cur != out; - out - }; + // Compute each merged value column. `cur` and `new` are full rows, so a tuple-output + // column's merge may reference any output column via `OldCol`/`NewCol`. + let mut merged_vals = SmallVec::<[Value; 4]>::new(); + for (i, col_merge) in resolved.iter().enumerate() { + let out_val = col_merge.run(state, cur, new, schema_math.n_keys, i, timestamp); + changed |= cur[schema_math.val_col(i)] != out_val; + merged_vals.push(out_val); + } let subsume = schema_math.subsume.then(|| { let cur = cur[schema_math.subsume_col()]; @@ -1098,12 +1133,15 @@ impl MergeFn { }); if changed { out.extend_from_slice(new); + for (i, val) in merged_vals.iter().enumerate() { + out[schema_math.val_col(i)] = *val; + } schema_math.write_table_row( out, RowVals { timestamp, subsume, - ret_val: Some(ret_val), + ret_val: None, }, ); } @@ -1112,11 +1150,29 @@ impl MergeFn { }) } + /// Resolve this merge into one [`ResolvedMergeFn`] per value column. Single-value merges + /// (the common case) resolve to a one-element vector; [`MergeFn::Columns`] resolves to one + /// entry per column. + fn resolve_columns(&self, function_name: &str, egraph: &mut EGraph) -> Vec { + match self { + MergeFn::Columns(cols) => cols + .iter() + .map(|col| col.resolve(function_name, egraph)) + .collect(), + other => vec![other.resolve(function_name, egraph)], + } + } + fn resolve(&self, function_name: &str, egraph: &mut EGraph) -> ResolvedMergeFn { match self { MergeFn::Const(v) => ResolvedMergeFn::Const(*v), MergeFn::Old => ResolvedMergeFn::Old, MergeFn::New => ResolvedMergeFn::New, + MergeFn::OldCol(i) => ResolvedMergeFn::OldCol(*i), + MergeFn::NewCol(i) => ResolvedMergeFn::NewCol(*i), + MergeFn::Columns(_) => { + panic!("nested Columns merge is not supported (Columns must be top-level)") + } MergeFn::AssertEq => ResolvedMergeFn::AssertEq { panic: egraph.new_panic(format!( "Illegal merge attempted for function {function_name}" @@ -1171,6 +1227,8 @@ enum ResolvedMergeFn { Const(Value), Old, New, + OldCol(usize), + NewCol(usize), AssertEq { panic: ExternalFunctionId, }, @@ -1190,12 +1248,29 @@ enum ResolvedMergeFn { } impl ResolvedMergeFn { - fn run(&self, state: &mut ExecutionState, cur: Value, new: Value, ts: Value) -> Value { + /// Compute the merged value for value column `self_col`. + /// + /// `cur` and `new` are the full conflicting rows. `n_keys` is the number of key columns, so + /// value column `i` lives at `cur[n_keys + i]`. `Old`/`New` refer to `self_col`'s value, while + /// `OldCol`/`NewCol` reference an explicit column — this lets a tuple-output column's merge + /// read any other output column. + fn run( + &self, + state: &mut ExecutionState, + cur: &[Value], + new: &[Value], + n_keys: usize, + self_col: usize, + ts: Value, + ) -> Value { match self { ResolvedMergeFn::Const(v) => *v, - ResolvedMergeFn::Old => cur, - ResolvedMergeFn::New => new, + ResolvedMergeFn::Old => cur[n_keys + self_col], + ResolvedMergeFn::New => new[n_keys + self_col], + ResolvedMergeFn::OldCol(i) => cur[n_keys + i], + ResolvedMergeFn::NewCol(i) => new[n_keys + i], ResolvedMergeFn::AssertEq { panic } => { + let (cur, new) = (cur[n_keys + self_col], new[n_keys + self_col]); if cur != new { let res = state.call_external_func(*panic, &[]); assert_eq!(res, None); @@ -1203,6 +1278,7 @@ impl ResolvedMergeFn { cur } ResolvedMergeFn::UnionId { uf_table } => { + let (cur, new) = (cur[n_keys + self_col], new[n_keys + self_col]); if cur != new { state.stage_insert(*uf_table, &[cur, new, ts]); // We pick the minimum when unioning. This matches the original egglog @@ -1219,7 +1295,7 @@ impl ResolvedMergeFn { ResolvedMergeFn::Primitive { prim, args, panic } => { let args = args .iter() - .map(|arg| arg.run(state, cur, new, ts)) + .map(|arg| arg.run(state, cur, new, n_keys, self_col, ts)) .collect::>(); match state.call_external_func(*prim, &args) { @@ -1227,19 +1303,19 @@ impl ResolvedMergeFn { None => { let res = state.call_external_func(*panic, &[]); assert_eq!(res, None); - cur + cur[n_keys + self_col] } } } ResolvedMergeFn::Function { func, args, panic } => { // see github.com/egraphs-good/egglog/pull/287 - if cur == new { - return cur; + if cur[n_keys + self_col] == new[n_keys + self_col] { + return cur[n_keys + self_col]; } let args = args .iter() - .map(|arg| arg.run(state, cur, new, ts)) + .map(|arg| arg.run(state, cur, new, n_keys, self_col, ts)) .collect::>(); // Merge functions dispatch to another function that may be @@ -1250,7 +1326,7 @@ impl ResolvedMergeFn { func.lookup_or_insert(state, &args).unwrap_or_else(|| { let res = state.call_external_func(*panic, &[]); assert_eq!(res, None); - cur + cur[n_keys + self_col] }) } } @@ -1290,10 +1366,7 @@ impl TableAction { }; TableAction { table: func_info.table, - table_math: SchemaMath { - func_cols: func_info.schema.len(), - subsume: func_info.can_subsume, - }, + table_math: func_info.schema_math(), default: match &func_info.default_val { DefaultVal::FreshId => Some(MergeVal::Counter(egraph.id_counter)), DefaultVal::Fail => None, @@ -1310,10 +1383,9 @@ impl TableAction { self.kind } - /// Number of input columns (schema minus the trailing output - /// column). + /// Number of input (key) columns. pub fn input_arity(&self) -> usize { - self.table_math.func_cols - 1 + self.table_math.num_keys() } /// Look up a row and return its return-value column, or `None` if the @@ -1388,7 +1460,10 @@ impl TableAction { let timestamp = MergeVal::Constant(Value::from_usize(state.read_counter(self.timestamp))); let mut merge_vals = SmallVec::<[MergeVal; 3]>::new(); + // Build just the non-key portion (single value + ts + subsume) of the row. + // `lookup_or_insert` is only used for single-value functions/constructors. SchemaMath { + n_keys: 0, func_cols: 1, ..self.table_math } @@ -1617,15 +1692,21 @@ fn combine_subsumed(v1: Value, v2: Value) -> Value { /// Functions can have multiple "output columns" in the underlying core-relations layer depending /// on whether different features are enabled. Roughly, tables are laid out as: /// -/// > `[key0, ..., keyn, return value, timestamp, subsume?]` +/// > `[key0, ..., keyn, value0, ..., valuem, timestamp, subsume?]` +/// +/// Where there are `n+1` key columns, `m+1` value (return) columns, and columns marked with a +/// question mark are optional, depending on the egraph and table-level configuration. /// -/// Where there are `n+1` key columns and columns marked with a question mark are optional, -/// depending on the egraph and table-level configuration. +/// Most functions have a single value column (`m == 0`); tuple-output functions (declared with a +/// parenthesized list of output sorts) have more than one. The functional dependency is always +/// from the key columns to the value columns. #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] struct SchemaMath { /// Whether or not the table is enabled for subsumption. subsume: bool, - /// The number of columns in the function (including the return value). + /// The number of key (input) columns. + n_keys: usize, + /// The number of columns in the function (keys plus all value/return columns). func_cols: usize, } @@ -1682,15 +1763,27 @@ impl SchemaMath { } fn num_keys(&self) -> usize { - self.func_cols - 1 + self.n_keys + } + + /// The number of value (return) columns. + fn n_vals(&self) -> usize { + self.func_cols - self.n_keys } fn table_columns(&self) -> usize { self.func_cols + 1 /* timestamp */ + if self.subsume { 1 } else { 0 } } + /// The column index of the `i`th value (return) column. + fn val_col(&self, i: usize) -> usize { + self.n_keys + i + } + + /// The first value column. For single-output functions this is *the* return value; + /// for tuple-output functions it is value column 0. fn ret_val_col(&self) -> usize { - self.func_cols - 1 + self.n_keys } fn ts_col(&self) -> usize { diff --git a/egglog/egglog-bridge/src/rule.rs b/egglog/egglog-bridge/src/rule.rs index 8a4a7da..141b44f 100644 --- a/egglog/egglog-bridge/src/rule.rs +++ b/egglog/egglog-bridge/src/rule.rs @@ -357,13 +357,11 @@ impl RuleBuilder<'_> { let schema_math = if let Some(func) = func { let info = &self.egraph.funcs[func]; assert_eq!(info.schema.len(), entries.len()); - SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - } + info.schema_math() } else { SchemaMath { subsume: subsume_entry.is_some(), + n_keys: entries.len().saturating_sub(1), func_cols: entries.len(), } }; @@ -484,10 +482,7 @@ impl RuleBuilder<'_> { || "subsumed a nonextestent row!".to_string(), ); let info = &self.egraph.funcs[func]; - let schema_math = SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - }; + let schema_math = info.schema_math(); assert!(info.can_subsume); assert_eq!(entries.len() + 1, info.schema.len()); let entries = entries.to_vec(); @@ -540,10 +535,7 @@ impl RuleBuilder<'_> { .to_var(); let table = info.table; let id_counter = self.query.id_counter; - let schema_math = SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - }; + let schema_math = info.schema_math(); let cb: BuildRuleCallback = match info.default_val { DefaultVal::Const(_) | DefaultVal::FreshId => { let wv: WriteVal = match &info.default_val { @@ -673,10 +665,7 @@ impl RuleBuilder<'_> { let info = &self.egraph.funcs[func]; let table = info.table; let entries = entries.to_vec(); - let schema_math = SchemaMath { - subsume: info.can_subsume, - func_cols: info.schema.len(), - }; + let schema_math = info.schema_math(); self.query.add_rule.push(Box::new(move |inner, rb| { let mut dst_vars = inner.convert_all(&entries); schema_math.write_table_row( diff --git a/egglog/src/ast/desugar.rs b/egglog/src/ast/desugar.rs index 11614aa..1dcf2fb 100644 --- a/egglog/src/ast/desugar.rs +++ b/egglog/src/ast/desugar.rs @@ -107,6 +107,7 @@ pub(crate) fn desugar_command( Schema { input: variant.types, output: datatype.clone(), + extra_outputs: vec![], }, variant.cost, false, @@ -242,6 +243,7 @@ fn desugar_prove(parser: &mut Parser, span: Span, query: Vec) -> Vec) -> Vec @@ -666,6 +667,13 @@ where ///``` /// A function can have a `cost` for extraction. /// + /// The output of a function is usually a single sort, but may be a parenthesized list of + /// sorts, e.g. `(function f (Math) (i64 i64) ...)`, declaring a *tuple-output* function whose + /// functional dependency maps the inputs to a tuple of value columns. Tuple outputs are + /// destructured in queries with `(= (values a b) (f x))`, written with + /// `(set (f x) (values a b))`, and merged with a `(values e0 e1 ...)` clause where `ei` merges + /// column `i` using the bound variables `old0`, `new0`, `old1`, `new1`, .... + /// /// Finally, it can have a `merge` and `on_merge`, which are triggered when /// the function dependency is violated. /// In this case, the merge expression determines which of the two outputs @@ -1289,18 +1297,66 @@ impl Display for Variant { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct Schema { pub input: Vec, + /// The first (primary) output sort. Most functions have exactly this one output. pub output: String, + /// Additional output sorts for tuple-output functions (declared with a parenthesized list of + /// output sorts, e.g. `(function f (Math) (i64 i64) ...)`). Empty for ordinary functions. + /// Together with [`Schema::output`], `output` followed by `extra_outputs` gives all of a + /// function's value columns (see [`Schema::outputs`]). + pub extra_outputs: Vec, } impl Display for Schema { fn fmt(&self, f: &mut Formatter) -> std::fmt::Result { - write!(f, "({}) {}", ListDisplay(&self.input, " "), self.output) + if self.extra_outputs.is_empty() { + write!(f, "({}) {}", ListDisplay(&self.input, " "), self.output) + } else { + write!( + f, + "({}) ({} {})", + ListDisplay(&self.input, " "), + self.output, + ListDisplay(&self.extra_outputs, " ") + ) + } } } impl Schema { pub fn new(input: Vec, output: String) -> Self { - Self { input, output } + Self { + input, + output, + extra_outputs: vec![], + } + } + + /// Construct a schema with one or more output sorts. `outputs` must be non-empty. + pub fn new_tuple(input: Vec, outputs: Vec) -> Self { + let mut outputs = outputs.into_iter(); + let output = outputs + .next() + .expect("schema must have at least one output"); + Self { + input, + output, + extra_outputs: outputs.collect(), + } + } + + /// Iterate over all output (value-column) sorts: the primary output followed by any extras. + pub fn outputs(&self) -> impl Iterator { + std::iter::once(&self.output).chain(self.extra_outputs.iter()) + } + + /// The number of output (value) columns. + pub fn num_outputs(&self) -> usize { + 1 + self.extra_outputs.len() + } + + /// Whether this function has more than one output column. + pub fn is_tuple_output(&self) -> bool { + !self.extra_outputs.is_empty() } } @@ -1385,7 +1441,7 @@ pub struct Facts(pub Vec>); impl Facts where - Head: Clone + Display, + Head: Clone + Display + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash, { /// Flattens a list of facts into a Query. @@ -1406,21 +1462,66 @@ where for fact in self.0.iter() { match fact { GenericFact::Eq(span, e1, e2) => { - let mut to_equate = vec![]; - let mut process = |expr: &GenericExpr| { - let (child_atoms, expr) = expr.to_query(typeinfo, fresh_gen); - atoms.extend(child_atoms); - to_equate.push(expr.get_corresponding_var_or_lit(typeinfo)); - expr - }; - let e1 = process(e1); - let e2 = process(e2); - atoms.push(GenericAtom { - span: span.clone(), - head: HeadOrEq::Eq, - args: to_equate, - }); - new_body.push(GenericFact::Eq(span.clone(), e1, e2)); + // Tuple destructure: `(= (values v...) (f a...))` (in either order), where `f` + // is a tuple-output function. This lowers directly to the function atom + // `f(a..., v...)` — the `values` targets become the function's output columns. + if let Some(td) = match_tuple_destructure(e1, e2, typeinfo) { + let mut atom_args = vec![]; + let mut mapped_inputs = vec![]; + for arg in td.func_args { + let (child_atoms, mexpr) = arg.to_query(typeinfo, fresh_gen); + atoms.extend(child_atoms); + atom_args.push(mexpr.get_corresponding_var_or_lit(typeinfo)); + mapped_inputs.push(mexpr); + } + let mut mapped_values = vec![]; + for v in td.values_args { + let (child_atoms, mexpr) = v.to_query(typeinfo, fresh_gen); + atoms.extend(child_atoms); + atom_args.push(mexpr.get_corresponding_var_or_lit(typeinfo)); + mapped_values.push(mexpr); + } + atoms.push(GenericAtom { + span: td.func_span.clone(), + head: HeadOrEq::Head(td.func_head.clone()), + args: atom_args, + }); + // Reconstruct a mapped `Eq` fact so type annotation can produce the + // resolved form (which is re-lowered the same way during canonicalization). + let values_mapped = GenericExpr::Call( + td.values_span.clone(), + CorrespondingVar::new( + td.values_head.clone(), + fresh_gen.fresh(td.func_head), + ), + mapped_values, + ); + let func_mapped = GenericExpr::Call( + td.func_span.clone(), + CorrespondingVar::new( + td.func_head.clone(), + fresh_gen.fresh(td.func_head), + ), + mapped_inputs, + ); + new_body.push(GenericFact::Eq(span.clone(), values_mapped, func_mapped)); + } else { + let mut to_equate = vec![]; + let mut process = |expr: &GenericExpr| { + let (child_atoms, expr) = expr.to_query(typeinfo, fresh_gen); + atoms.extend(child_atoms); + to_equate.push(expr.get_corresponding_var_or_lit(typeinfo)); + expr + }; + let e1 = process(e1); + let e2 = process(e2); + atoms.push(GenericAtom { + span: span.clone(), + head: HeadOrEq::Eq, + args: to_equate, + }); + new_body.push(GenericFact::Eq(span.clone(), e1, e2)); + } } GenericFact::Fact(expr) => { let (child_atoms, expr) = expr.to_query(typeinfo, fresh_gen); @@ -1433,6 +1534,47 @@ where } } +/// The pieces of a recognized `(= (values v...) (f a...))` tuple destructure. +struct TupleDestructure<'a, Head, Leaf> { + values_head: &'a Head, + values_span: &'a Span, + values_args: &'a [GenericExpr], + func_head: &'a Head, + func_span: &'a Span, + func_args: &'a [GenericExpr], +} + +/// Recognize `(= (values v...) (f a...))` in either argument order, where `f` is a tuple-output +/// function. The arity (number of `values` targets vs. output columns) is validated later by the +/// usual type-checking arity constraints. +fn match_tuple_destructure<'a, Head, Leaf>( + e1: &'a GenericExpr, + e2: &'a GenericExpr, + typeinfo: &TypeInfo, +) -> Option> +where + Head: Clone + Display + HeadOps, + Leaf: Clone + PartialEq + Eq + Display + Hash, +{ + for (a, b) in [(e1, e2), (e2, e1)] { + if let GenericExpr::Call(values_span, values_head, values_args) = a + && values_head.is_values() + && let GenericExpr::Call(func_span, func_head, func_args) = b + && func_head.tuple_output_arity(typeinfo).is_some() + { + return Some(TupleDestructure { + values_head, + values_span, + values_args, + func_head, + func_span, + func_args, + }); + } + } + None +} + #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct CorrespondingVar where @@ -1675,6 +1817,7 @@ where schema: Schema { input: schema.input.into_iter().map(&mut *fun).collect(), output: fun(schema.output), + extra_outputs: schema.extra_outputs.into_iter().map(&mut *fun).collect(), }, cost, unextractable, @@ -1702,6 +1845,7 @@ where schema: Schema { input: schema.input.into_iter().map(&mut *fun).collect(), output: fun(schema.output), + extra_outputs: schema.extra_outputs.into_iter().map(&mut *fun).collect(), }, merge, hidden, diff --git a/egglog/src/ast/parse.rs b/egglog/src/ast/parse.rs index 4d0aebb..85957e8 100644 --- a/egglog/src/ast/parse.rs +++ b/egglog/src/ast/parse.rs @@ -38,6 +38,60 @@ macro_rules! error { }; } +/// Names that may not be used as user identifiers (function/sort/constructor/relation/variant +/// names or variables) because they are built-in keywords of the surface syntax: most command, +/// action, and schedule heads, plus `values` (the tuple constructor for tuple-output functions). +/// Keeping these out of the identifier namespace avoids confusing programs where, say, a function +/// named `set` reads like the `set` action. A few common-word commands (`input`, `output`) are +/// only partially reserved — see [`COMMAND_ONLY_KEYWORDS`]. Names starting with `:` are reserved +/// separately (the `:` prefix marks option keywords), see [`Parser::ensure_symbol_not_reserved`]. +const RESERVED_KEYWORDS: &[&str] = &[ + // commands + "sort", + "datatype", + "datatype*", + "function", + "constructor", + "relation", + "ruleset", + "unstable-combined-ruleset", + "rule", + "rewrite", + "birewrite", + "run", + "run-schedule", + "check", + "extract", + "push", + "pop", + "print-function", + "print-size", + "print-stats", + "include", + "fail", + "prove", + "prove-exists", + // actions + "let", + "set", + "union", + "delete", + "subsume", + "panic", + // schedules + "repeat", + "saturate", + "seq", + // tuple-output destructuring/construction + "values", +]; + +/// Commands whose names are common enough to want as ordinary identifiers, so they are only +/// *partially* reserved: usable as variables, but not as the head of a call s-expr (so `(input +/// ...)` always means the command, never a table lookup) nor as a definition (table/sort/etc.) +/// name. +const COMMAND_ONLY_KEYWORDS: &[&str] = &["input", "output"]; + pub enum Sexp { // Will never contain `Literal::Unit`, as this // will be parsed as an empty `Sexp::List`. @@ -168,7 +222,26 @@ impl Default for Parser { impl Parser { fn ensure_symbol_not_reserved(&self, symbol: &str, span: &Span) -> Result<(), ParseError> { - if self.symbol_gen.is_reserved(symbol) && self.ensure_no_reserved_symbols { + // Disabled when re-parsing egglog's own generated programs (e.g. proof/term encoding), + // which may legitimately use internal-prefixed names. + if !self.ensure_no_reserved_symbols { + return Ok(()); + } + if RESERVED_KEYWORDS.contains(&symbol) { + return error!( + span.clone(), + "`{symbol}` is a reserved keyword and cannot be used as a name" + ); + } + // The leading `:` marks option keywords (`:merge`, `:cost`, `:ruleset`, ...); the parser + // uses it to delimit options, so it cannot be the start of a user identifier. + if symbol.starts_with(':') { + return error!( + span.clone(), + "`{symbol}` cannot be used as a name: the `:` prefix is reserved for option keywords" + ); + } + if self.symbol_gen.is_reserved(symbol) { return error!( span.clone(), "symbols starting with '{}' are reserved for egglog internals", @@ -178,6 +251,28 @@ impl Parser { Ok(()) } + /// Check that a name introducing a definition (function/sort/constructor/relation/datatype/ + /// variant) is allowed: neither a reserved keyword nor a command-only keyword like + /// `input`/`output` (which would otherwise create an uncallable table). + fn ensure_definition_name(&self, name: &str, span: &Span) -> Result<(), ParseError> { + self.ensure_symbol_not_reserved(name, span)?; + if self.ensure_no_reserved_symbols && COMMAND_ONLY_KEYWORDS.contains(&name) { + return error!( + span.clone(), + "`{name}` is a command and cannot be used as a definition name" + ); + } + Ok(()) + } + + /// Parse an atom that introduces a new name (e.g. a function, sort, constructor, or relation), + /// rejecting reserved keywords such as `values` and command names like `input`/`output`. + fn parse_name(&self, sexp: &Sexp, what: &'static str) -> Result { + let name = sexp.expect_atom(what)?; + self.ensure_definition_name(&name, &sexp.span())?; + Ok(name) + } + pub fn get_program_from_string( &mut self, filename: Option, @@ -263,7 +358,7 @@ impl Parser { match tail { [name] => vec![Command::Sort { span, - name: name.expect_atom("sort name")?, + name: self.parse_name(name, "sort name")?, presort_and_args: None, uf: None, proof_func: None, @@ -273,7 +368,7 @@ impl Parser { let (func, args, _) = call.expect_call("container sort declaration")?; vec![Command::Sort { span, - name: name.expect_atom("sort name")?, + name: self.parse_name(name, "sort name")?, presort_and_args: Some(( func, map_fallible(args, self, Self::parse_expr)?, @@ -306,7 +401,7 @@ impl Parser { } vec![Command::Sort { span, - name: name.expect_atom("sort name")?, + name: self.parse_name(name, "sort name")?, presort_and_args: None, uf, proof_func, @@ -324,7 +419,7 @@ impl Parser { "datatype" => match tail { [name, variants @ ..] => vec![Command::Datatype { span, - name: name.expect_atom("sort name")?, + name: self.parse_name(name, "sort name")?, variants: map_fallible(variants, self, Self::variant)?, }], _ => return error!(span, "usage: (datatype *)"), @@ -379,7 +474,7 @@ impl Parser { } }; vec![Command::Function { - name: name.expect_atom("function name")?, + name: self.parse_name(name, "function name")?, schema: self.parse_schema(inputs, output)?, merge, hidden, @@ -419,7 +514,7 @@ impl Parser { vec![Command::Constructor { span, - name: name.expect_atom("constructor name")?, + name: self.parse_name(name, "constructor name")?, schema: self.parse_schema(inputs, output)?, cost, unextractable, @@ -439,7 +534,7 @@ impl Parser { "relation" => match tail { [name, inputs] => vec![Command::Relation { span, - name: name.expect_atom("relation name")?, + name: self.parse_name(name, "relation name")?, inputs: map_fallible(inputs.expect_list("input sorts")?, self, |_, sexp| { sexp.expect_atom("input sort") })?, @@ -931,6 +1026,17 @@ impl Parser { return func.parse(tail, span, self); } + // `input`/`output` are commands, not callable tables, so they may not head an + // expression even though they are allowed as ordinary variable names. + if self.ensure_no_reserved_symbols + && COMMAND_ONLY_KEYWORDS.contains(&head.as_str()) + { + return error!( + span, + "`{head}` is a command and cannot be used as the head of an expression" + ); + } + Expr::Call( span.clone(), head, @@ -950,7 +1056,7 @@ impl Parser { Ok(match head.as_str() { "sort" => match tail { [name, call] => { - let name = name.expect_atom("sort name")?; + let name = self.parse_name(name, "sort name")?; let (func, args, _) = call.expect_call("container sort declaration")?; let args = map_fallible(args, self, Self::parse_expr)?; (span, name, Subdatatypes::NewSort(func, args)) @@ -963,6 +1069,7 @@ impl Parser { } }, _ => { + self.ensure_definition_name(&head, &span)?; let variants = map_fallible(tail, self, Self::variant)?; (span, head, Subdatatypes::Variants(variants)) } @@ -971,6 +1078,7 @@ impl Parser { pub fn variant(&mut self, sexp: &Sexp) -> Result { let (name, tail, span) = sexp.expect_call("datatype variant")?; + self.ensure_definition_name(&name, &span)?; let (types, cost, unextractable) = match tail { [types @ .., Sexp::Atom(o, _)] if *o == ":unextractable" => (types, None, true), @@ -1023,14 +1131,27 @@ impl Parser { } pub fn parse_schema(&self, input: &Sexp, output: &Sexp) -> Result { - Ok(Schema { - input: input - .expect_list("input sorts")? + let input = input + .expect_list("input sorts")? + .iter() + .map(|sexp| sexp.expect_atom("input sort")) + .collect::>()?; + // The output is either a single sort, or a parenthesized list of sorts for a + // tuple-output function (e.g. `(function f (Math) (i64 i64) ...)`). + let outputs: Vec = match output { + Sexp::List(list, _) => list .iter() - .map(|sexp| sexp.expect_atom("input sort")) + .map(|sexp| sexp.expect_atom("output sort")) .collect::>()?, - output: output.expect_atom("output sort")?, - }) + _ => vec![output.expect_atom("output sort")?], + }; + if outputs.is_empty() { + return error!( + output.span(), + "a function must have at least one output sort" + ); + } + Ok(Schema::new_tuple(input, outputs)) } } diff --git a/egglog/src/ast/proof_global_remover.rs b/egglog/src/ast/proof_global_remover.rs index 2cbbb4b..7f6f841 100644 --- a/egglog/src/ast/proof_global_remover.rs +++ b/egglog/src/ast/proof_global_remover.rs @@ -42,6 +42,7 @@ fn resolved_var_to_call(var: &ResolvedVar) -> ResolvedCall { subtype: FunctionSubtype::Constructor, input: vec![], output: var.sort.clone(), + extra_outputs: vec![], }) } @@ -80,6 +81,7 @@ fn remove_globals_cmd(cmd: ResolvedNCommand) -> Vec { subtype: FunctionSubtype::Constructor, input: vec![], output: ty.clone(), + extra_outputs: vec![], }); let func_decl = ResolvedFunctionDecl { name: name.name, @@ -87,6 +89,7 @@ fn remove_globals_cmd(cmd: ResolvedNCommand) -> Vec { schema: Schema { input: vec![], output: ty.name().to_owned(), + extra_outputs: vec![], }, resolved_schema: resolved_call.clone(), merge: None, diff --git a/egglog/src/ast/remove_globals.rs b/egglog/src/ast/remove_globals.rs index c37f908..3f2cdbd 100644 --- a/egglog/src/ast/remove_globals.rs +++ b/egglog/src/ast/remove_globals.rs @@ -62,6 +62,7 @@ fn resolved_var_to_call(var: &ResolvedVar) -> ResolvedCall { subtype: FunctionSubtype::Custom, input: vec![], output: var.sort.clone(), + extra_outputs: vec![], }) } @@ -98,6 +99,7 @@ impl GlobalRemover<'_> { subtype: FunctionSubtype::Custom, input: vec![], output: ty.clone(), + extra_outputs: vec![], }); let func_decl = ResolvedFunctionDecl { name: name.name, @@ -105,6 +107,7 @@ impl GlobalRemover<'_> { schema: Schema { input: vec![], output: ty.name().to_owned(), + extra_outputs: vec![], }, resolved_schema: resolved_call.clone(), merge: None, diff --git a/egglog/src/constraint.rs b/egglog/src/constraint.rs index 3267a58..f3a1385 100644 --- a/egglog/src/constraint.rs +++ b/egglog/src/constraint.rs @@ -542,6 +542,21 @@ impl Assignment { .iter() .map(|arg| self.annotate_expr(arg, typeinfo, ctx)) .collect(); + // The `values` tuple constructor resolves to `ResolvedCall::Values` carrying its + // element sorts. A tuple-output function call carries only its input columns here + // (its outputs live on the `values` side of the destructure/set), so it resolves + // from input types alone. + if head.as_str() == "values" { + let sorts = args.iter().map(|arg| arg.output_type()).collect(); + return GenericExpr::Call(span.clone(), ResolvedCall::Values(sorts), args); + } + if let Some(ty) = typeinfo.get_func_type(head).filter(|t| t.is_tuple_output()) { + let input_types: Vec<_> = args.iter().map(|arg| arg.output_type()).collect(); + let resolved_call = + ResolvedCall::from_resolution_func_types(head, &input_types, typeinfo) + .unwrap_or_else(|| ResolvedCall::Func(ty.clone())); + return GenericExpr::Call(span.clone(), resolved_call, args); + } let types: Vec<_> = args .iter() .map(|arg| arg.output_type()) @@ -621,12 +636,23 @@ impl Assignment { .map(|child| self.annotate_expr(child, typeinfo, ctx)) .collect(); let rhs = self.annotate_expr(rhs, typeinfo, ctx); - let types: Vec<_> = children - .iter() - .map(|child| child.output_type()) - .chain(once(rhs.output_type())) - .collect(); - let resolved_call = ResolvedCall::from_resolution(head, &types, typeinfo, ctx); + // For a tuple-output function the `rhs` is a `(values ...)` form, so the function + // is resolved from its input columns alone. + let resolved_call = if let Some(ty) = + typeinfo.get_func_type(head).filter(|t| t.is_tuple_output()) + { + let input_types: Vec<_> = + children.iter().map(|child| child.output_type()).collect(); + ResolvedCall::from_resolution_func_types(head, &input_types, typeinfo) + .unwrap_or_else(|| ResolvedCall::Func(ty.clone())) + } else { + let types: Vec<_> = children + .iter() + .map(|child| child.output_type()) + .chain(once(rhs.output_type())) + .collect(); + ResolvedCall::from_resolution(head, &types, typeinfo, ctx) + }; if !matches!(resolved_call, ResolvedCall::Func(_)) { return Err(TypeError::UnboundFunction(head.clone(), span.clone())); } @@ -835,7 +861,7 @@ impl CoreAction { } let mut args = args.clone(); - args.push(rhs.clone()); + args.extend(rhs.iter().cloned()); Ok(get_literal_and_global_constraints(&args, typeinfo) .chain(get_atom_application_constraints( @@ -917,11 +943,13 @@ fn get_atom_application_constraints( // `constraint::xor` means one and only one of the instantiation can hold. let mut xor_constraints: Vec>>> = vec![]; - // function atom constraints + // function atom constraints. A function atom carries all input columns followed by all output + // columns (more than one for a tuple-output function). if let Some(typ) = type_info.get_func_type(head) { let mut constraints = vec![]; + let expected = typ.input.len() + typ.num_outputs(); // arity mismatch - if typ.input.len() + 1 != args.len() { + if expected != args.len() { constraints.push(constraint::impossible( ImpossibleConstraint::ArityMismatch { atom: Atom { @@ -929,15 +957,15 @@ fn get_atom_application_constraints( head: head.to_owned(), args: args.to_vec(), }, - expected: typ.input.len() + 1, + expected, }, )); } else { for (arg_typ, arg) in typ .input .iter() + .chain(typ.outputs()) .cloned() - .chain(once(typ.output.clone())) .zip(args.iter().cloned()) { constraints.push(constraint::assign(arg, arg_typ)); @@ -1181,7 +1209,9 @@ pub(crate) fn grounded_check( for atom in body.atoms.iter() { let mut add_global_and_literal = false; match &atom.head { - HeadOrEq::Head(ResolvedCall::Func(_)) => { + // `Values` never appears as a query atom head (tuple destructures are lowered to the + // underlying function atom), but it is grounded like a function if it ever did. + HeadOrEq::Head(ResolvedCall::Func(_) | ResolvedCall::Values(_)) => { for arg in atom.args.iter() { problem.constraints.push(assign(arg.clone(), ())); } diff --git a/egglog/src/core.rs b/egglog/src/core.rs index d0dd46d..d1ef64f 100644 --- a/egglog/src/core.rs +++ b/egglog/src/core.rs @@ -111,10 +111,41 @@ impl Hash for SpecializedPrimitive { } } -#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone)] pub enum ResolvedCall { Func(FuncType), Primitive(SpecializedPrimitive), + /// The `values` tuple constructor, used to destructure a tuple-output function's outputs in a + /// query (`(= (values a b) (f x))`) or to construct them in a `set` action + /// (`(set (f x) (values a b))`). Carries the output sorts. It never reaches the backend on its + /// own: it is always paired with a tuple-output function call when lowering to core. + Values(Vec), +} + +impl PartialEq for ResolvedCall { + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (ResolvedCall::Func(a), ResolvedCall::Func(b)) => a == b, + (ResolvedCall::Primitive(a), ResolvedCall::Primitive(b)) => a == b, + (ResolvedCall::Values(a), ResolvedCall::Values(b)) => { + a.len() == b.len() && a.iter().zip(b).all(|(x, y)| x.name() == y.name()) + } + _ => false, + } + } +} + +impl Eq for ResolvedCall {} + +impl Hash for ResolvedCall { + fn hash(&self, state: &mut H) { + std::mem::discriminant(self).hash(state); + match self { + ResolvedCall::Func(f) => f.hash(state), + ResolvedCall::Primitive(p) => p.hash(state), + ResolvedCall::Values(sorts) => sorts.iter().for_each(|s| s.name().hash(state)), + } + } } impl ResolvedCall { @@ -122,6 +153,7 @@ impl ResolvedCall { match self { ResolvedCall::Func(func) => &func.name, ResolvedCall::Primitive(prim) => prim.name(), + ResolvedCall::Values(_) => "values", } } @@ -129,6 +161,10 @@ impl ResolvedCall { match self { ResolvedCall::Func(func) => &func.output, ResolvedCall::Primitive(prim) => prim.output(), + // `values` has no single output; its first column is returned only so that callers + // that incidentally ask for "a" sort do not panic. Tuple-output uses are routed + // specially before this is consulted. + ResolvedCall::Values(sorts) => &sorts[0], } } @@ -138,10 +174,11 @@ impl ResolvedCall { match self { ResolvedCall::Func(func) => { let mut types = func.input.clone(); - types.push(func.output.clone()); + types.extend(func.outputs().cloned()); types } ResolvedCall::Primitive(prim) => prim.input().to_vec(), + ResolvedCall::Values(sorts) => sorts.clone(), } } @@ -171,7 +208,7 @@ impl ResolvedCall { ctx: crate::Context, ) -> ResolvedCall { if let Some(ty) = typeinfo.get_func_type(head) { - let expected = ty.input.iter().chain(once(&ty.output)).map(|s| s.name()); + let expected = ty.input.iter().chain(ty.outputs()).map(|s| s.name()); let actual = types.iter().map(|s| s.name()); if expected.eq(actual) { return ResolvedCall::Func(ty.clone()); @@ -206,6 +243,7 @@ impl Display for ResolvedCall { match self { ResolvedCall::Func(func) => write!(f, "{}", func.name), ResolvedCall::Primitive(prim) => write!(f, "{}", prim.name()), + ResolvedCall::Values(_) => write!(f, "values"), } } } @@ -224,6 +262,7 @@ impl IsFunc for ResolvedCall { match self { ResolvedCall::Func(func) => type_info.is_constructor(&func.name), ResolvedCall::Primitive(_) => false, + ResolvedCall::Values(_) => false, } } } @@ -234,6 +273,41 @@ impl IsFunc for String { } } +/// Operations on a call head needed to lower the `values` tuple sugar. Implemented for both the +/// unresolved (`String`) and resolved ([`ResolvedCall`]) head representations so that the same +/// lowering code runs in both the type-checking and canonicalization passes. +pub trait HeadOps { + /// Whether this head is the `values` tuple constructor. + fn is_values(&self) -> bool; + /// If this head is a tuple-output function (more than one output column), the number of output + /// columns; otherwise `None`. + fn tuple_output_arity(&self, type_info: &TypeInfo) -> Option; +} + +impl HeadOps for String { + fn is_values(&self) -> bool { + self == "values" + } + fn tuple_output_arity(&self, type_info: &TypeInfo) -> Option { + type_info + .get_func_type(self) + .map(|t| t.num_outputs()) + .filter(|n| *n > 1) + } +} + +impl HeadOps for ResolvedCall { + fn is_values(&self) -> bool { + matches!(self, ResolvedCall::Values(_)) + } + fn tuple_output_arity(&self, _type_info: &TypeInfo) -> Option { + match self { + ResolvedCall::Func(f) if f.is_tuple_output() => Some(f.num_outputs()), + _ => None, + } + } +} + #[derive(Debug, Clone)] pub enum GenericAtomTerm { Var(Span, Leaf), @@ -462,6 +536,7 @@ impl Query { head: head.clone(), args: atom.args.clone(), }), + ResolvedCall::Values(_) => None, }) } @@ -473,6 +548,7 @@ impl Query { args: atom.args.clone(), }), ResolvedCall::Primitive(_) => None, + ResolvedCall::Values(_) => None, }) } } @@ -481,11 +557,13 @@ impl Query { pub enum GenericCoreAction { Let(Span, Leaf, Head, Vec>), LetAtomTerm(Span, Leaf, GenericAtomTerm), + /// `(set (f keys...) value...)`. The last field holds the function's output (value) columns: + /// one for an ordinary function, more for a tuple-output function. Set( Span, Head, Vec>, - GenericAtomTerm, + Vec>, ), Change(Span, Change, Head, Vec>), Union(Span, GenericAtomTerm, GenericAtomTerm), @@ -554,9 +632,9 @@ where add_from_atom(&mut free_vars, at); free_vars.remove(v); } - GenericCoreAction::Set(_span, _, ats, at) => { + GenericCoreAction::Set(_span, _, ats, vals) => { add_from_atoms(&mut free_vars, ats); - add_from_atom(&mut free_vars, at); + add_from_atoms(&mut free_vars, vals); } GenericCoreAction::Change(_span, _change, _, ats) => { add_from_atoms(&mut free_vars, ats); @@ -610,14 +688,14 @@ pub(crate) trait GenericActionsExt { ctx: &mut CoreActionContext<'_, Head, Leaf, FG>, ) -> Result<(GenericCoreActions, MappedActions), TypeError> where - Head: Clone + Display + IsFunc, + Head: Clone + Display + IsFunc + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash, FG: FreshGen; } impl GenericActionsExt for GenericActions where - Head: Clone + Display + IsFunc, + Head: Clone + Display + IsFunc + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash, { #[allow(clippy::type_complexity)] @@ -626,7 +704,7 @@ where ctx: &mut CoreActionContext<'_, Head, Leaf, FG>, ) -> Result<(GenericCoreActions, MappedActions), TypeError> where - Head: Clone + Display + IsFunc, + Head: Clone + Display + IsFunc + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash, FG: FreshGen, { @@ -663,7 +741,31 @@ where let mapped_arg = arg.to_core_actions(ctx, &mut norm_actions)?; mapped_args.push(mapped_arg); } - let mapped_expr = expr.to_core_actions(ctx, &mut norm_actions)?; + // The value may be a `(values v...)` tuple (for a tuple-output function), which + // contributes one output column per element; otherwise it is a single value. + let (mapped_value, value_terms) = match expr { + GenericExpr::Call(vspan, vhead, vargs) if vhead.is_values() => { + let mut mapped = vec![]; + let mut terms = vec![]; + for v in vargs { + let m = v.to_core_actions(ctx, &mut norm_actions)?; + terms.push(m.get_corresponding_var_or_lit(typeinfo)); + mapped.push(m); + } + let dummy = ctx.fresh_gen.fresh(vhead); + let mapped_call = GenericExpr::Call( + vspan.clone(), + CorrespondingVar::new(vhead.clone(), dummy), + mapped, + ); + (mapped_call, terms) + } + _ => { + let m = expr.to_core_actions(ctx, &mut norm_actions)?; + let term = m.get_corresponding_var_or_lit(typeinfo); + (m, vec![term]) + } + }; norm_actions.push(GenericCoreAction::Set( span.clone(), head.clone(), @@ -671,14 +773,14 @@ where .iter() .map(|e| e.get_corresponding_var_or_lit(typeinfo)) .collect(), - mapped_expr.get_corresponding_var_or_lit(typeinfo), + value_terms, )); let v = ctx.fresh_gen.fresh(head); mapped_actions.0.push(GenericAction::Set( span.clone(), CorrespondingVar::new(head.clone(), v), mapped_args, - mapped_expr, + mapped_value, )); } GenericAction::Change(span, change, head, args) => { @@ -730,7 +832,8 @@ where .iter() .map(|e| e.get_corresponding_var_or_lit(typeinfo)) .collect(), - mapped_expr.get_corresponding_var_or_lit(typeinfo), + // Constructors are single-output, so a single value column. + vec![mapped_expr.get_corresponding_var_or_lit(typeinfo)], )); let v = ctx.fresh_gen.fresh(head); mapped_actions.0.push(GenericAction::Set( @@ -1089,13 +1192,13 @@ pub(crate) trait GenericRuleExt { union_to_set_optimization: bool, ) -> Result, Head, Leaf>, TypeError> where - Head: Clone + Display + IsFunc, + Head: Clone + Display + IsFunc + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash + Debug; } impl GenericRuleExt for GenericRule where - Head: Clone + Display + IsFunc, + Head: Clone + Display + IsFunc + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash + Debug, { fn to_core_rule( @@ -1105,7 +1208,7 @@ where union_to_set_optimization: bool, ) -> Result, Head, Leaf>, TypeError> where - Head: Clone + Display + IsFunc, + Head: Clone + Display + IsFunc + HeadOps, Leaf: Clone + PartialEq + Eq + Display + Hash + Debug, { let (body, _correspondence) = Facts(self.body.clone()).to_query(typeinfo, fresh_gen); diff --git a/egglog/src/exec_state.rs b/egglog/src/exec_state.rs index ebac11e..10ea82a 100644 --- a/egglog/src/exec_state.rs +++ b/egglog/src/exec_state.rs @@ -290,6 +290,9 @@ pub trait Core<'a, 'db: 'a>: Internal<'a, 'db> { match resolved_call { ResolvedCall::Primitive(primitive) => self.apply_primitive(primitive, &values), ResolvedCall::Func(func) => self.apply_resolved_function(func, &values), + ResolvedCall::Values(_) => { + panic!("`values` cannot be evaluated as a single-valued expression") + } } } } diff --git a/egglog/src/extract.rs b/egglog/src/extract.rs index 3c7aa40..1ddb71a 100644 --- a/egglog/src/extract.rs +++ b/egglog/src/extract.rs @@ -812,7 +812,7 @@ impl EGraph { .ok_or(TypeError::UnboundFunction(sym.to_owned(), span!()))?; let mut rootsorts = func.schema.input.clone(); if include_output { - rootsorts.push(func.schema.output.clone()); + rootsorts.extend(func.schema.outputs().cloned()); } let extractor = Extractor::compute_costs_from_rootsorts( Some(rootsorts), @@ -840,11 +840,22 @@ impl EGraph { } inputs.push(termdag.app(sym.to_owned(), children)); if include_output { - let value = row.vals[func.schema.input.len()]; - let sort = &func.schema.output; - let (_, term) = extractor - .extract_best_with_sort(self, &mut termdag, value, sort.clone()) - .unwrap_or_else(|| (0, termdag.var("Unextractable".into()))); + // Extract every output (value) column. A tuple-output function has more than + // one; we display them wrapped in a `(values ...)` term to mirror the surface + // syntax. + let mut out_terms = Vec::new(); + for (i, sort) in func.schema.outputs().enumerate() { + let value = row.vals[func.schema.input.len() + i]; + let (_, term) = extractor + .extract_best_with_sort(self, &mut termdag, value, sort.clone()) + .unwrap_or_else(|| (0, termdag.var("Unextractable".into()))); + out_terms.push(term); + } + let term = if out_terms.len() == 1 { + out_terms.pop().unwrap() + } else { + termdag.app("values".to_owned(), out_terms) + }; output.as_mut().unwrap().push(term); } true diff --git a/egglog/src/lib.rs b/egglog/src/lib.rs index b9d7e20..5303c69 100644 --- a/egglog/src/lib.rs +++ b/egglog/src/lib.rs @@ -375,16 +375,30 @@ impl Function { #[derive(Clone, Debug)] pub struct ResolvedSchema { pub input: Vec, + /// The first (primary) output sort. See [`ResolvedSchema::outputs`]. pub output: ArcSort, + /// Additional output sorts for tuple-output functions. Empty for ordinary functions. + pub extra_outputs: Vec, } impl ResolvedSchema { - /// Get the type at position `index`, counting the `output` sort as at position `input.len()`. + /// All output (value-column) sorts: the primary output followed by any extras. + pub fn outputs(&self) -> impl Iterator { + std::iter::once(&self.output).chain(self.extra_outputs.iter()) + } + + /// Get the type at position `index`, counting the output columns as positions + /// `input.len()`, `input.len() + 1`, ... pub fn get_by_pos(&self, index: usize) -> Option<&ArcSort> { - if self.input.len() == index { - Some(&self.output) - } else { + if index < self.input.len() { self.input.get(index) + } else { + let out_idx = index - self.input.len(); + if out_idx == 0 { + Some(&self.output) + } else { + self.extra_outputs.get(out_idx - 1) + } } } } @@ -754,12 +768,23 @@ impl EGraph { let val = literal_to_value(&self.backend, literal); Ok(egglog_bridge::MergeFn::Const(val)) } - GenericExpr::Var(span, resolved_var) => match resolved_var.name.as_str() { - "old" => Ok(egglog_bridge::MergeFn::Old), - "new" => Ok(egglog_bridge::MergeFn::New), - // NB: type-checking should already catch unbound variables here. - _ => Err(TypeError::Unbound(resolved_var.name.clone(), span.clone()).into()), - }, + GenericExpr::Var(span, resolved_var) => { + let name = resolved_var.name.as_str(); + // Single-output merges use `old`/`new`; tuple-output merges use `old0`, `new0`, + // `old1`, ... to refer to the old/new value of a specific output column. + if name == "old" { + Ok(egglog_bridge::MergeFn::Old) + } else if name == "new" { + Ok(egglog_bridge::MergeFn::New) + } else if let Some(i) = name.strip_prefix("old").and_then(|s| s.parse().ok()) { + Ok(egglog_bridge::MergeFn::OldCol(i)) + } else if let Some(i) = name.strip_prefix("new").and_then(|s| s.parse().ok()) { + Ok(egglog_bridge::MergeFn::NewCol(i)) + } else { + // NB: type-checking should already catch unbound variables here. + Err(TypeError::Unbound(resolved_var.name.clone(), span.clone()).into()) + } + } GenericExpr::Call(_, ResolvedCall::Func(f), args) => { let translated_args = args .iter() @@ -801,6 +826,12 @@ impl EGraph { translated_args, )) } + // A top-level `(values ...)` tuple merge is decomposed per column in + // `declare_function`; reaching here means a `values` was nested inside another merge + // expression, which is not supported. + GenericExpr::Call(span, ResolvedCall::Values(_), _) => Err(Error::TypeError( + TypeError::TupleMergeNotValues("".to_owned(), span.clone()), + )), } } @@ -820,6 +851,13 @@ impl EGraph { .map(get_sort) .collect::, _>>()?; let output = get_sort(&decl.schema.output)?; + let extra_outputs = decl + .schema + .extra_outputs + .iter() + .map(get_sort) + .collect::, _>>()?; + let num_outputs = 1 + extra_outputs.len(); let can_subsume = match decl.subtype { FunctionSubtype::Constructor => true, @@ -828,30 +866,47 @@ impl EGraph { }; use egglog_bridge::{DefaultVal, MergeFn}; + let merge = match decl.subtype { + FunctionSubtype::Constructor => MergeFn::UnionId, + FunctionSubtype::Custom => match &decl.merge { + // A tuple-output merge is a `(values e0 e1 ...)` form: each `ei` becomes the merge + // for output column `i`. + Some(GenericExpr::Call(_, ResolvedCall::Values(_), cols)) => MergeFn::Columns( + cols.iter() + .map(|e| self.translate_expr_to_mergefn(e)) + .collect::, _>>()?, + ), + Some(expr) => self.translate_expr_to_mergefn(expr)?, + // No merge clause: assert equality per output column. + None if num_outputs > 1 => { + MergeFn::Columns((0..num_outputs).map(|_| MergeFn::AssertEq).collect()) + } + None => MergeFn::AssertEq, + }, + }; let backend_id = self.backend.add_table(egglog_bridge::FunctionConfig { schema: input .iter() .chain([&output]) + .chain(extra_outputs.iter()) .map(|sort| sort.column_ty(&self.backend)) .collect(), default: match decl.subtype { FunctionSubtype::Constructor => DefaultVal::FreshId, FunctionSubtype::Custom => DefaultVal::Fail, }, - merge: match decl.subtype { - FunctionSubtype::Constructor => MergeFn::UnionId, - FunctionSubtype::Custom => match &decl.merge { - None => MergeFn::AssertEq, - Some(expr) => self.translate_expr_to_mergefn(expr)?, - }, - }, + merge, name: decl.name.to_string(), can_subsume, }); let function = Function { decl: decl.clone(), - schema: ResolvedSchema { input, output }, + schema: ResolvedSchema { + input, + output, + extra_outputs, + }, can_subsume, backend_id, }; @@ -2689,6 +2744,9 @@ impl<'a> BackendRule<'a> { let (p, args, ty) = self.prim(p, &atom.args, ctx); self.rb.query_prim(p, &args, ty).unwrap() } + ResolvedCall::Values(_) => { + unreachable!("`values` is lowered to the underlying function atom before query") + } } } } @@ -2717,6 +2775,9 @@ impl<'a> BackendRule<'a> { format!("{span}: call of primitive {name} failed") }) } + ResolvedCall::Values(_) => { + panic!("`values` cannot be bound as a single value") + } }; self.entries.insert(v, y.into()); } @@ -2725,16 +2786,18 @@ impl<'a> BackendRule<'a> { let x = self.entry(x); self.entries.insert(v, x); } - core::GenericCoreAction::Set(_, f, xs, y) => match f { + core::GenericCoreAction::Set(_, f, xs, ys) => match f { ResolvedCall::Primitive(..) => panic!("runtime primitive set!"), + ResolvedCall::Values(..) => panic!("`values` is not a settable function"), ResolvedCall::Func(f) => { let f = self.func(f); - let args = self.args(xs.iter().chain([y])); + let args = self.args(xs.iter().chain(ys.iter())); self.rb.set(f, &args) } }, core::GenericCoreAction::Change(span, change, f, args) => match f { ResolvedCall::Primitive(..) => panic!("runtime primitive change!"), + ResolvedCall::Values(..) => panic!("`values` is not a changeable function"), ResolvedCall::Func(f) => { let name = f.name.clone(); let can_subsume = self.functions[&f.name].can_subsume; diff --git a/egglog/src/prelude.rs b/egglog/src/prelude.rs index 3e8b6c5..d32e5eb 100644 --- a/egglog/src/prelude.rs +++ b/egglog/src/prelude.rs @@ -825,6 +825,7 @@ macro_rules! datatype { Schema { input: vec![$(stringify!($args).to_owned()),*], output: stringify!($sort).to_owned(), + extra_outputs: vec![], }, [$($cost)*].first().copied(), false, diff --git a/egglog/src/proofs/proof_checker.rs b/egglog/src/proofs/proof_checker.rs index 8938026..835952a 100644 --- a/egglog/src/proofs/proof_checker.rs +++ b/egglog/src/proofs/proof_checker.rs @@ -189,6 +189,7 @@ fn eval_expr_with_subst( }) })? } + ResolvedCall::Values(_) => panic!("`values` is not supported in proofs"), }, }; @@ -1031,6 +1032,7 @@ impl ProofStore { } } } + ResolvedCall::Values(_) => panic!("`values` is not supported in proofs"), } } } diff --git a/egglog/src/proofs/proof_encoding.rs b/egglog/src/proofs/proof_encoding.rs index a51701e..ecc97e0 100644 --- a/egglog/src/proofs/proof_encoding.rs +++ b/egglog/src/proofs/proof_encoding.rs @@ -938,6 +938,9 @@ impl<'a> ProofInstrumentor<'a> { (fv.clone(), proof) } + ResolvedCall::Values(_) => { + panic!("tuple-output (`values`) functions are not supported in proofs") + } } } } @@ -1184,6 +1187,9 @@ impl<'a> ProofInstrumentor<'a> { )); fv } + ResolvedCall::Values(_) => { + panic!("tuple-output (`values`) functions are not supported in proofs") + } } } } diff --git a/egglog/src/proofs/proof_encoding_helpers.rs b/egglog/src/proofs/proof_encoding_helpers.rs index 778476c..ed02ef8 100644 --- a/egglog/src/proofs/proof_encoding_helpers.rs +++ b/egglog/src/proofs/proof_encoding_helpers.rs @@ -465,6 +465,8 @@ pub enum ProofEncodingUnsupportedReason { "rule uses `:naive` with an eq-sort primitive in the body. Proof encoding can only look up proofs for primitive eq-sort fact results under seminaive-safe query evaluation." )] NaiveEqSortPrimitiveFact, + #[error("tuple-output functions are not supported by the term/proof encoding.")] + TupleOutputFunction, } /// Checks whether a desugared program supports proof encoding. @@ -542,6 +544,14 @@ pub(crate) fn command_supports_proof_encoding( return Err(ProofEncodingUnsupportedReason::NaiveEqSortPrimitiveFact); } + // Tuple-output functions store multiple value columns, which the term/proof encoding (built + // around single-output constructor views) does not model. + if let crate::ast::GenericCommand::Function { schema, .. } = command + && schema.is_tuple_output() + { + return Err(ProofEncodingUnsupportedReason::TupleOutputFunction); + } + // Check all expressions for primitives without validators let mut all_primitives_have_validators = true; command.clone().visit_exprs(&mut |expr| { diff --git a/egglog/src/proofs/proof_extraction.rs b/egglog/src/proofs/proof_extraction.rs index c05c9c2..b40d105 100644 --- a/egglog/src/proofs/proof_extraction.rs +++ b/egglog/src/proofs/proof_extraction.rs @@ -30,6 +30,9 @@ impl ProofInstrumentor<'_> { ResolvedCall::Primitive(_) => { return Err(ProveExistsError::PrimitivesUnsupported); } + ResolvedCall::Values(_) => { + return Err(ProveExistsError::RequiresConstructor); + } }; let function = self diff --git a/egglog/src/typechecking.rs b/egglog/src/typechecking.rs index 53cf2b4..9d097ef 100644 --- a/egglog/src/typechecking.rs +++ b/egglog/src/typechecking.rs @@ -115,14 +115,38 @@ pub struct FuncType { pub name: String, pub subtype: FunctionSubtype, pub input: Vec, + /// The first (primary) output sort. See [`FuncType::outputs`]. pub output: ArcSort, + /// Additional output sorts for tuple-output functions. Empty for ordinary functions. + pub extra_outputs: Vec, +} + +impl FuncType { + /// All output (value-column) sorts: the primary output followed by any extras. + pub fn outputs(&self) -> impl Iterator { + std::iter::once(&self.output).chain(self.extra_outputs.iter()) + } + + /// The number of output (value) columns. + pub fn num_outputs(&self) -> usize { + 1 + self.extra_outputs.len() + } + + /// Whether this function has more than one output column. + pub fn is_tuple_output(&self) -> bool { + !self.extra_outputs.is_empty() + } } impl PartialEq for FuncType { fn eq(&self, other: &Self) -> bool { if self.name == other.name && self.subtype == other.subtype - && self.output.name() == other.output.name() + && self.num_outputs() == other.num_outputs() + && self + .outputs() + .zip(other.outputs()) + .all(|(a, b)| a.name() == b.name()) { if self.input.len() != other.input.len() { return false; @@ -145,7 +169,9 @@ impl Hash for FuncType { fn hash(&self, state: &mut H) { self.name.hash(state); self.subtype.hash(state); - self.output.name().hash(state); + for out in self.outputs() { + out.name().hash(state); + } for inp in &self.input { inp.name().hash(state); } @@ -688,32 +714,32 @@ impl TypeInfo { } fn function_to_functype(&self, func: &FunctionDecl) -> Result { + let resolve = |name: &String| -> Result { + self.sorts + .get(name) + .cloned() + .ok_or_else(|| TypeError::UndefinedSort(name.clone(), func.span.clone())) + }; let input = func .schema .input .iter() - .map(|name| { - if let Some(sort) = self.sorts.get(name) { - Ok(sort.clone()) - } else { - Err(TypeError::UndefinedSort(name.clone(), func.span.clone())) - } - }) + .map(&resolve) + .collect::, _>>()?; + let output = resolve(&func.schema.output)?; + let extra_outputs = func + .schema + .extra_outputs + .iter() + .map(&resolve) .collect::, _>>()?; - let output = if let Some(sort) = self.sorts.get(&func.schema.output) { - Ok(sort.clone()) - } else { - Err(TypeError::UndefinedSort( - func.schema.output.clone(), - func.span.clone(), - )) - }?; Ok(FuncType { name: func.name.clone(), subtype: func.subtype, input, - output: output.clone(), + output, + extra_outputs, }) } @@ -748,34 +774,69 @@ impl TypeInfo { fdecl.span.clone(), )); } - let mut bound_vars = IndexMap::default(); - let output_type = self.sorts.get(&fdecl.schema.output).unwrap(); - if fdecl.subtype == FunctionSubtype::Constructor && !output_type.is_eq_sort() { + let outputs: Vec = fdecl + .schema + .outputs() + .map(|name| self.sorts.get(name).unwrap().clone()) + .collect(); + let is_tuple = fdecl.schema.is_tuple_output(); + + // Tuple outputs are only meaningful for custom functions (which carry a functional + // dependency from keys to a tuple of values). Constructors and view tables mint/track a + // single e-class id. + if is_tuple + && (fdecl.subtype == FunctionSubtype::Constructor || fdecl.term_constructor.is_some()) + { + return Err(TypeError::TupleOutputNotAllowed( + fdecl.name.clone(), + fdecl.span.clone(), + )); + } + if fdecl.subtype == FunctionSubtype::Constructor && !outputs[0].is_eq_sort() { return Err(TypeError::ConstructorOutputNotSort( fdecl.name.clone(), fdecl.span.clone(), )); } - bound_vars.insert("old", (fdecl.span.clone(), output_type.clone())); - bound_vars.insert("new", (fdecl.span.clone(), output_type.clone())); + + // For single-output functions the merge expression refers to `old`/`new`. For + // tuple-output functions it refers to `old0`, `new0`, `old1`, `new1`, ... (one pair per + // output column), and the whole merge is a `(values ...)` form. + let mut bound_vars = IndexMap::default(); + let tuple_var_names: Vec<(String, String)> = (0..outputs.len()) + .map(|i| (format!("old{i}"), format!("new{i}"))) + .collect(); + if is_tuple { + for (i, (old_name, new_name)) in tuple_var_names.iter().enumerate() { + bound_vars.insert(old_name.as_str(), (fdecl.span.clone(), outputs[i].clone())); + bound_vars.insert(new_name.as_str(), (fdecl.span.clone(), outputs[i].clone())); + } + } else { + bound_vars.insert("old", (fdecl.span.clone(), outputs[0].clone())); + bound_vars.insert("new", (fdecl.span.clone(), outputs[0].clone())); + } + + let merge = match &fdecl.merge { + // Merge expressions run as part of action-side table updates: writes are allowed, but + // live DB reads would be untracked by seminaive rule execution. + Some(merge) if is_tuple => { + Some(self.typecheck_tuple_merge(symbol_gen, fdecl, merge, &outputs, &bound_vars)?) + } + Some(merge) => Some(self.typecheck_standalone_expr( + symbol_gen, + merge, + &bound_vars, + Context::Write, + )?), + None => None, + }; Ok(ResolvedFunctionDecl { name: fdecl.name.clone(), subtype: fdecl.subtype, schema: fdecl.schema.clone(), resolved_schema: ResolvedCall::Func(self.func_types.get(&fdecl.name).unwrap().clone()), - merge: match &fdecl.merge { - // Merge expressions run as part of action-side table updates: - // writes are allowed, but live DB reads would be untracked by - // seminaive rule execution. - Some(merge) => Some(self.typecheck_standalone_expr( - symbol_gen, - merge, - &bound_vars, - Context::Write, - )?), - None => None, - }, + merge, cost: fdecl.cost, unextractable: fdecl.unextractable, internal_hidden: fdecl.internal_hidden, @@ -785,6 +846,55 @@ impl TypeInfo { }) } + /// Typecheck the `(values e0 e1 ...)` merge of a tuple-output function. Each `ei` is checked + /// with `old0`/`new0`/... bound to the corresponding output columns, and must have the type of + /// output column `i`. The result is a resolved `values` call carrying the output sorts. + fn typecheck_tuple_merge( + &self, + symbol_gen: &mut SymbolGen, + fdecl: &FunctionDecl, + merge: &Expr, + outputs: &[ArcSort], + bound_vars: &IndexMap<&str, (Span, ArcSort)>, + ) -> Result { + let args = match merge { + GenericExpr::Call(_, head, args) if head.as_str() == "values" => args, + _ => { + return Err(TypeError::TupleMergeNotValues( + fdecl.name.clone(), + fdecl.span.clone(), + )); + } + }; + if args.len() != outputs.len() { + return Err(TypeError::TupleMergeArity { + name: fdecl.name.clone(), + expected: outputs.len(), + actual: args.len(), + span: fdecl.span.clone(), + }); + } + let mut resolved_args = Vec::with_capacity(args.len()); + for (arg, expected) in args.iter().zip(outputs) { + let resolved = + self.typecheck_standalone_expr(symbol_gen, arg, bound_vars, Context::Write)?; + let actual = resolved.output_type(); + if actual.name() != expected.name() { + return Err(TypeError::Mismatch { + expr: arg.clone(), + expected: expected.clone(), + actual, + }); + } + resolved_args.push(resolved); + } + Ok(GenericExpr::Call( + merge.span(), + ResolvedCall::Values(outputs.to_vec()), + resolved_args, + )) + } + fn typecheck_schedule( &self, symbol_gen: &mut SymbolGen, @@ -1197,6 +1307,23 @@ pub enum TypeError { crate::GLOBAL_NAME_PREFIX )] GlobalMissingPrefix { name: String, span: Span }, + #[error( + "{1}\nFunction {0} has a tuple output, which is only allowed for plain functions (not constructors, relations, or view tables)." + )] + TupleOutputNotAllowed(String, Span), + #[error( + "{1}\nThe :merge of tuple-output function {0} must be a `(values ...)` form with one expression per output column." + )] + TupleMergeNotValues(String, Span), + #[error( + "{span}\nThe :merge of tuple-output function {name} has {actual} columns but the function has {expected} output columns." + )] + TupleMergeArity { + name: String, + expected: usize, + actual: usize, + span: Span, + }, } #[cfg(test)] diff --git a/egglog/src/util.rs b/egglog/src/util.rs index 8c54a70..ca64402 100644 --- a/egglog/src/util.rs +++ b/egglog/src/util.rs @@ -102,6 +102,7 @@ impl FreshGen for SymbolGen { let sort = match name_hint { ResolvedCall::Func(f) => f.output.clone(), ResolvedCall::Primitive(prim) => prim.output().clone(), + ResolvedCall::Values(sorts) => sorts[0].clone(), }; ResolvedVar { name, diff --git a/egglog/tests/tuple_outputs.rs b/egglog/tests/tuple_outputs.rs new file mode 100644 index 0000000..0200c8b --- /dev/null +++ b/egglog/tests/tuple_outputs.rs @@ -0,0 +1,207 @@ +//! Integration tests for tuple-output functions: functions declared with more than one output +//! sort, e.g. `(function f (Math) (i64 i64) :merge (values ...))`. Their value columns are +//! destructured with `(= (values a b) (f x))` and written with `(set (f x) (values a b))`. + +use egglog::{EGraph, Error, TypeError}; + +fn run(prog: &str) -> Result<(), Error> { + EGraph::default() + .parse_and_run_program(None, prog) + .map(|_| ()) +} + +#[test] +fn tuple_merge_interval_analysis() { + // The motivating example: an interval analysis whose lower bound merges with `max` and whose + // upper bound merges with `min`, expressed as a single two-output function. + run(r#" + (datatype Math (Num i64) (Add Math Math)) + (function interval (Math) (i64 i64) + :merge (values (max old0 new0) (min old1 new1))) + + (rule ((= e (Num n))) + ((set (interval e) (values n n)))) + (rule ((= e (Add a b)) + (= (values alo ahi) (interval a)) + (= (values blo bhi) (interval b))) + ((set (interval e) (values (+ alo blo) (+ ahi bhi))))) + + (let expr (Add (Num 1) (Num 2))) + (run 10) + (check (= (values 3 3) (interval expr))) + "#) + .unwrap(); +} + +#[test] +fn tuple_merge_combines_columns_independently() { + // Two `set`s on the same key are resolved column-by-column: lo with max, hi with min. + run(r#" + (datatype M (V i64)) + (function iv (M) (i64 i64) :merge (values (max old0 new0) (min old1 new1))) + (set (iv (V 0)) (values 1 10)) + (set (iv (V 0)) (values 3 7)) + (check (= (values 3 7) (iv (V 0)))) + "#) + .unwrap(); +} + +#[test] +fn tuple_check_distinguishes_columns() { + // A `(values ...)` check must match every column, not just the first. + let bad = run(r#" + (datatype M (V i64)) + (function iv (M) (i64 i64) :merge (values (max old0 new0) (min old1 new1))) + (set (iv (V 0)) (values 3 7)) + (check (= (values 3 99) (iv (V 0)))) + "#); + assert!(bad.is_err(), "check on a wrong second column should fail"); +} + +#[test] +fn tuple_destructure_binds_each_column_in_rule() { + run(r#" + (datatype M (V i64)) + (function iv (M) (i64 i64) :merge (values (max old0 new0) (min old1 new1))) + (relation lo-is (M i64)) + (relation hi-is (M i64)) + (set (iv (V 0)) (values 3 7)) + (rule ((= (values l h) (iv x))) ((lo-is x l) (hi-is x h))) + (run 1) + (check (lo-is (V 0) 3)) + (check (hi-is (V 0) 7)) + (fail (check (lo-is (V 0) 7))) + "#) + .unwrap(); +} + +#[test] +fn tuple_output_eq_sorts() { + // Output columns may be e-classes, and are kept canonical across unions like any other column. + run(r#" + (datatype N (Nn i64)) + (function two (i64) (N N) :merge (values new0 new1)) + (set (two 0) (values (Nn 1) (Nn 2))) + (relation got (N N)) + (rule ((= (values a b) (two k))) ((got a b))) + (run 1) + (check (got (Nn 1) (Nn 2))) + + ; unioning an output e-class is reflected after rebuilding + (union (Nn 1) (Nn 5)) + (run 1) + (check (= (values (Nn 5) (Nn 2)) (two 0))) + "#) + .unwrap(); +} + +#[test] +fn tuple_no_merge_asserts_equality() { + // With no `:merge`, each output column asserts equality; a conflicting write is an error. + run(r#" + (datatype M (V i64)) + (function iv (M) (i64 i64)) + (set (iv (V 0)) (values 1 2)) + (set (iv (V 0)) (values 1 3)) + "#) + .expect_err("conflicting write under default (assert-eq) merge should fail"); +} + +#[test] +fn constructor_tuple_output_rejected() { + let err = EGraph::default() + .parse_and_run_program(None, "(constructor c (i64) (i64 i64))") + .unwrap_err(); + assert!( + matches!(err, Error::TypeError(TypeError::TupleOutputNotAllowed(..))), + "expected TupleOutputNotAllowed, got {err:?}" + ); +} + +#[test] +fn tuple_merge_arity_mismatch_rejected() { + let err = EGraph::default() + .parse_and_run_program( + None, + "(function f (i64) (i64 i64) :merge (values (max old0 new0)))", + ) + .unwrap_err(); + assert!( + matches!(err, Error::TypeError(TypeError::TupleMergeArity { .. })), + "expected TupleMergeArity, got {err:?}" + ); +} + +#[test] +fn builtin_keywords_are_reserved() { + // Built-in keywords (command/action/schedule heads, plus the tuple constructor `values`) may + // not be used as function/constructor/relation/variant names or as variables. + for prog in [ + // `values` (the tuple constructor) in each identifier position + "(function values (i64) i64 :merge new)", + "(sort S) (constructor values (i64) S)", + "(relation values (i64))", + "(datatype D (values i64))", + "(relation r (i64)) (rule ((r values)) ())", + // a sampling of command/action/schedule keywords + "(function set (i64) i64 :merge new)", + "(relation union (i64))", + "(sort run)", + "(datatype D (function i64))", + "(relation r (i64)) (rule ((r let)) ())", + ] { + let err = run(prog).expect_err(&format!("keyword should be rejected in: {prog}")); + assert!( + err.to_string().contains("reserved keyword"), + "expected a reserved-keyword error for {prog:?}, got: {err}" + ); + } + + // The `:` prefix is reserved for option keywords, so it cannot start an identifier. + let err = run("(relation :merge (i64))").unwrap_err(); + assert!( + err.to_string().contains("`:` prefix is reserved"), + "expected a colon-prefix error, got: {err}" + ); +} + +#[test] +fn input_output_are_only_partially_reserved() { + // `input`/`output` are usable as ordinary variables... + run("(relation r (i64)) (r 0) (rule ((r input)) ((r (+ input 1)))) (run 1) (check (r 1))") + .unwrap(); + + // ...but not as definition names... + for prog in [ + "(function input (i64) i64 :merge new)", + "(relation output (i64))", + "(sort input)", + "(datatype D (output i64))", + ] { + let err = run(prog).expect_err(&format!("`input`/`output` should be rejected in: {prog}")); + assert!( + err.to_string() + .contains("cannot be used as a definition name"), + "expected a definition-name error for {prog:?}, got: {err}" + ); + } + + // ...and not as the head of a call expression. + let err = run("(relation r (i64)) (rule ((r x)) ((r (input x))))").unwrap_err(); + assert!( + err.to_string() + .contains("cannot be used as the head of an expression"), + "expected a call-head error, got: {err}" + ); +} + +#[test] +fn tuple_merge_must_be_values_form() { + let err = EGraph::default() + .parse_and_run_program(None, "(function f (i64) (i64 i64) :merge old0)") + .unwrap_err(); + assert!( + matches!(err, Error::TypeError(TypeError::TupleMergeNotValues(..))), + "expected TupleMergeNotValues, got {err:?}" + ); +} From ed920b5f3878147e911aeaad531d0b7ecb2f4ce1 Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Tue, 7 Jul 2026 20:31:53 +0000 Subject: [PATCH 2/4] egglog-experimental: adapt to tuple-output Schema/ResolvedCall The workspace root now builds egglog-experimental alongside egglog, so it must handle the tuple-output additions from the #938 port: add `extra_outputs: vec![]` to the fresh! constructor Schema, and a `ResolvedCall::Values(_) => Context::Pure` arm (tuple construct/destructure reads/writes no tables). Co-Authored-By: Claude Opus 4.8 --- egglog-experimental/src/fresh_macro.rs | 1 + egglog-experimental/src/primitive.rs | 2 ++ egglog/src/ast/parse.rs | 8 +++++++- 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/egglog-experimental/src/fresh_macro.rs b/egglog-experimental/src/fresh_macro.rs index 50ce721..2ba3e73 100644 --- a/egglog-experimental/src/fresh_macro.rs +++ b/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, diff --git a/egglog-experimental/src/primitive.rs b/egglog-experimental/src/primitive.rs index d92704a..93d8cbe 100644 --- a/egglog-experimental/src/primitive.rs +++ b/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, diff --git a/egglog/src/ast/parse.rs b/egglog/src/ast/parse.rs index 85957e8..44f00e6 100644 --- a/egglog/src/ast/parse.rs +++ b/egglog/src/ast/parse.rs @@ -1013,7 +1013,13 @@ impl Parser { if *symbol == "_" { self.symbol_gen.fresh(symbol) } else { - self.ensure_symbol_not_reserved(symbol, span)?; + // `:`-prefixed atoms are option-keyword markers (e.g. `:until` in a custom + // run-schedule) that command macros consume as `Expr::Var`s; allow them here. + // User variables never start with `:`, so this doesn't weaken the reserved-name + // guarantee for identifiers. + if !symbol.starts_with(':') { + self.ensure_symbol_not_reserved(symbol, span)?; + } symbol.clone() }, ), From 25724adcdc5122da3fe23c419da753364aa926ff Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Tue, 7 Jul 2026 21:14:36 +0000 Subject: [PATCH 3/4] Tidy tuple-output doc comments Fix a doubled word and grammar in the `function` command doc, drop the redundant sentence on `Schema::extra_outputs` (already covered by `Schema::outputs`), and trim the memory-representation aside from the CHANGELOG entry. Co-Authored-By: Claude Opus 4.8 --- egglog/CHANGELOG.md | 2 +- egglog/src/ast/mod.rs | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/egglog/CHANGELOG.md b/egglog/CHANGELOG.md index bebcfb0..8b8abb9 100644 --- a/egglog/CHANGELOG.md +++ b/egglog/CHANGELOG.md @@ -4,7 +4,7 @@ - **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 (no boxing); the functional dependency is + 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 diff --git a/egglog/src/ast/mod.rs b/egglog/src/ast/mod.rs index a66768d..26b3169 100644 --- a/egglog/src/ast/mod.rs +++ b/egglog/src/ast/mod.rs @@ -657,8 +657,8 @@ where inputs: Vec, }, - /// The `function` command declare an egglog custom function, which is a database table with a - /// a functional dependency (also called a primary key) on its inputs to its output(s). + /// The `function` command declares an egglog custom function, which is a database table with a + /// functional dependency (also called a primary key) on its inputs to its output(s). /// /// ```text /// (function @@ -1301,8 +1301,6 @@ pub struct Schema { pub output: String, /// Additional output sorts for tuple-output functions (declared with a parenthesized list of /// output sorts, e.g. `(function f (Math) (i64 i64) ...)`). Empty for ordinary functions. - /// Together with [`Schema::output`], `output` followed by `extra_outputs` gives all of a - /// function's value columns (see [`Schema::outputs`]). pub extra_outputs: Vec, } From e688d4cb1f4186c025be9e3311d50efb1d759ce5 Mon Sep 17 00:00:00 2001 From: Oliver Flatt Date: Tue, 7 Jul 2026 21:47:39 +0000 Subject: [PATCH 4/4] Load all output columns in the input command for tuple-output functions `input_file` built rows and validated types using only `schema.output`, so loading a tuple-output custom function from a TSV rejected valid rows (too many fields) and would have inserted too few columns. Use `schema.outputs()` for both the type check and the row schema. Adds a regression test. Co-Authored-By: Claude Opus 4.8 --- egglog/src/lib.rs | 10 ++++++---- egglog/tests/tuple_outputs.rs | 24 ++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 4 deletions(-) diff --git a/egglog/src/lib.rs b/egglog/src/lib.rs index 5303c69..8dff7a4 100644 --- a/egglog/src/lib.rs +++ b/egglog/src/lib.rs @@ -1900,9 +1900,11 @@ impl EGraph { } if function_type.subtype != FunctionSubtype::Constructor { - match func.schema.output.name() { - "i64" | "String" | "Unit" => {} - s => panic!("Unsupported type {s} for input"), + for sort in func.schema.outputs() { + match sort.name() { + "i64" | "String" | "Unit" => {} + s => panic!("Unsupported type {s} for input"), + } } } @@ -1916,7 +1918,7 @@ impl EGraph { let mut row_schema = func.schema.input.clone(); if function_type.subtype == FunctionSubtype::Custom { - row_schema.push(func.schema.output.clone()); + row_schema.extend(func.schema.outputs().cloned()); } log::debug!("{row_schema:?}"); diff --git a/egglog/tests/tuple_outputs.rs b/egglog/tests/tuple_outputs.rs index 0200c8b..df8bf74 100644 --- a/egglog/tests/tuple_outputs.rs +++ b/egglog/tests/tuple_outputs.rs @@ -205,3 +205,27 @@ fn tuple_merge_must_be_values_form() { "expected TupleMergeNotValues, got {err:?}" ); } + +#[test] +fn tuple_output_input_command_loads_all_columns() { + // `(input f file)` for a tuple-output function must load every output column, not just + // the first, so a TSV row has `input + all outputs` fields. + let dir = std::env::temp_dir().join("egglog_tuple_output_input_test"); + std::fs::create_dir_all(&dir).unwrap(); + std::fs::write(dir.join("iv.tsv"), "1\t10\t20\n2\t30\t40\n").unwrap(); + + let mut egraph = EGraph::default(); + egraph.fact_directory = Some(dir.clone()); + let result = egraph.parse_and_run_program( + None, + r#" + (function iv (i64) (i64 i64) :merge (values old0 old1)) + (input iv "iv.tsv") + (check (= (values 10 20) (iv 1))) + (check (= (values 30 40) (iv 2))) + "#, + ); + + std::fs::remove_dir_all(&dir).ok(); + result.unwrap(); +}