From 0329e6dc4dd8cdddfd879a7016f524052afcbb7c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 9 Apr 2026 20:48:18 +0000 Subject: [PATCH 1/3] Initial plan From dab7b2dbc756c41a67dbda044b5838591486672d Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 9 Apr 2026 20:54:11 +0000 Subject: [PATCH 2/3] Improve check error message and add documentation for constructor term behavior Agent-Logs-Url: https://github.com/egraphs-good/egglog/sessions/7ca6f621-bd4b-4430-89c1-ef6dc4f7e6a7 Co-authored-by: saulshanabrook <1186124+saulshanabrook@users.noreply.github.com> --- src/ast/mod.rs | 19 ++++++++++++++++++- src/lib.rs | 2 +- tests/check-constructor-not-in-egraph.egg | 18 ++++++++++++++++++ ...pshot_check_constructor_not_in_egraph.snap | 6 ++++++ 4 files changed, 43 insertions(+), 2 deletions(-) create mode 100644 tests/check-constructor-not-in-egraph.egg create mode 100644 tests/snapshots/files__shared_snapshot_check_constructor_not_in_egraph.snap diff --git a/src/ast/mod.rs b/src/ast/mod.rs index beb4ef3c0..7e7ac81ba 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -849,7 +849,14 @@ where PrintOverallStatistics(Span, Option), /// The `check` command checks that the given facts /// match at least once in the current database. - /// The list of facts is matched in the same way a [`Command::Rule`] is matched. + /// The list of facts is matched in the same way a [`Command::Rule`] is matched, + /// i.e., it runs a query against the current e-graph state. + /// + /// Note: For `eqsort` terms (e.g., constructor applications like `(Num 6)`), + /// the terms must already be present in the e-graph for the check to succeed. + /// Unlike primitive types (e.g., `i64`), constructor terms are not automatically + /// materialized by `check`. This mirrors the behavior of rules, which also only + /// match against existing e-graph state. /// /// Example: /// @@ -867,6 +874,16 @@ where /// [ERROR] Check failed /// [INFO ] Command failed as expected. /// ``` + /// + /// Example using constructor terms (terms must be in the e-graph first): + /// + /// ```text + /// (datatype Math) + /// (constructor Num (i64) Math) + /// (let x (Num 6)) + /// (check (= x (Num 6))) ;; succeeds: (Num 6) is now in the e-graph + /// (fail (check (= (Num 7) (Num 7)))) ;; fails: (Num 7) is not in the e-graph + /// ``` Check(Span, Vec>), Prove(Span, Vec>), ProveExists(Span, Head), diff --git a/src/lib.rs b/src/lib.rs index 1686afdbc..ab7261cdc 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -2104,7 +2104,7 @@ pub enum Error { TypeError(#[from] TypeError), #[error("Errors:\n{}", ListDisplay(.0, "\n"))] TypeErrors(Vec), - #[error("{}\nCheck failed: \n{}", .1, ListDisplay(.0, "\n"))] + #[error("{}\nCheck failed (are the relevant terms present in the e-graph?): \n{}", .1, ListDisplay(.0, "\n"))] CheckError(Vec, Span), #[error("{1}\nNo such ruleset: {0}")] NoSuchRuleset(String, Span), diff --git a/tests/check-constructor-not-in-egraph.egg b/tests/check-constructor-not-in-egraph.egg new file mode 100644 index 000000000..30b89bd9b --- /dev/null +++ b/tests/check-constructor-not-in-egraph.egg @@ -0,0 +1,18 @@ +;; This test verifies that check fails when constructor terms are not in the e-graph. +;; The `check` command runs a query against existing e-graph state, so constructor +;; terms (eqsort terms) must already be present for a check to succeed. + +(datatype Math) +(constructor Num (i64) Math) + +;; This check fails because (Num 6) is not in the e-graph yet +(fail (check (= (Num 6) (Num 6)))) + +;; Introduce (Num 6) into the e-graph using let +(let x (Num 6)) + +;; Now this succeeds because (Num 6) is in the e-graph +(check (= x (Num 6))) + +;; This still fails because (Num 7) is not in the e-graph +(fail (check (= (Num 7) (Num 7)))) diff --git a/tests/snapshots/files__shared_snapshot_check_constructor_not_in_egraph.snap b/tests/snapshots/files__shared_snapshot_check_constructor_not_in_egraph.snap new file mode 100644 index 000000000..903ce70cc --- /dev/null +++ b/tests/snapshots/files__shared_snapshot_check_constructor_not_in_egraph.snap @@ -0,0 +1,6 @@ +--- +source: tests/files.rs +assertion_line: 94 +expression: snapshot_content_across_treatments +--- +((Num 1)) From aa8ebf202855d7c9f8b787b23d37191ae8787a97 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 9 Apr 2026 20:58:15 +0000 Subject: [PATCH 3/3] Add equality check test for two variable references to same constructor term Agent-Logs-Url: https://github.com/egraphs-good/egglog/sessions/7ca6f621-bd4b-4430-89c1-ef6dc4f7e6a7 Co-authored-by: saulshanabrook <1186124+saulshanabrook@users.noreply.github.com> --- tests/check-constructor-not-in-egraph.egg | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/check-constructor-not-in-egraph.egg b/tests/check-constructor-not-in-egraph.egg index 30b89bd9b..bcf1c75d7 100644 --- a/tests/check-constructor-not-in-egraph.egg +++ b/tests/check-constructor-not-in-egraph.egg @@ -14,5 +14,9 @@ ;; Now this succeeds because (Num 6) is in the e-graph (check (= x (Num 6))) +;; Two variable references to the same constructor term are also equal +(let y (Num 6)) +(check (= x y)) + ;; This still fails because (Num 7) is not in the e-graph (fail (check (= (Num 7) (Num 7))))