Proof encoding in egglog itself

.github/workflows/build.yml

@@ -15,6 +15,8 @@ jobs:
       - uses: taiki-e/install-action@v2
         with:
           tool: nextest
+      - uses: taiki-e/install-action@v2
+        with:
           tool: cargo-insta
       - uses: Swatinem/rust-cache@v2
       - run: make test

CHANGELOG.md

@@ -2,7 +2,9 @@
 
 ## [Unreleased] - ReleaseDate
 
+- Refactored API to use [`TermId`] more consistently instead of `Term` where possible, simplifying egglog code.
 - Require globals to use the `$` prefix; missing prefixes now log a warning by default and can be upgraded to errors with `--strict-mode` or `EGraph::set_strict_mode`.
+- Desugar `relation`s to `constructor`s to simplify the language and implementation. Relations no longer return unit `()` values.
 - Export let bindings in the serialized format so they are visualized (#701)
   - Breaking change: renames `ignore_viz` to `let_binding` in `GenericFunctionDecl`.
 

Makefile

@@ -8,7 +8,7 @@ WWW=${PWD}/target/www
 all: test nits docs
 
 test:
-	cargo insta test --test-runner nextest --release --workspace
+	cargo insta test --release --workspace --test-runner nextest --unreferenced reject
 	# nextest doesn't run doctests, so do it here
 	cargo test --doc --release --workspace
 

egglog-ast/src/generic_ast_helpers.rs

@@ -1,4 +1,3 @@
-use std::borrow::Cow;
 use std::fmt::{Display, Formatter};
 use std::hash::Hash;
 
@@ -31,16 +30,6 @@ macro_rules! impl_from {
 
 pub const INTERNAL_SYMBOL_PREFIX: &str = "@";
 
-/// Gets rid of internal symbol prefixes for printing.
-/// This allows us to test parsing of desugared programs.
-pub fn sanitize_internal_name(name: &str) -> Cow<'_, str> {
-    if let Some(stripped) = name.strip_prefix(INTERNAL_SYMBOL_PREFIX) {
-        Cow::Owned(format!("_{}", stripped))
-    } else {
-        Cow::Borrowed(name)
-    }
-}
-
 impl<Head: Display, Leaf: Display> Display for GenericRule<Head, Leaf>
 where
     Head: Clone + Display,
@@ -72,12 +61,12 @@ where
             }
         }
         let ruleset = if !self.ruleset.is_empty() {
-            format!(":ruleset {}", sanitize_internal_name(&self.ruleset))
+            format!(":ruleset {}", &self.ruleset)
         } else {
             "".into()
         };
         let name = if !self.name.is_empty() {
-            format!(":name \"{}\"", sanitize_internal_name(&self.name))
+            format!(":name \"{}\"", &self.name)
         } else {
             "".into()
         };

src/ast/check_shadowing.rs

@@ -80,6 +80,7 @@ impl Names {
             ResolvedNCommand::Extract(..) => Ok(()),
             ResolvedNCommand::RunSchedule(..) => Ok(()),
             ResolvedNCommand::PrintOverallStatistics(..) => Ok(()),
+            ResolvedNCommand::ProveExists(..) => Ok(()),
             ResolvedNCommand::PrintFunction(..) => Ok(()),
             ResolvedNCommand::PrintSize(..) => Ok(()),
             ResolvedNCommand::Input { .. } => Ok(()),

src/ast/desugar.rs

@@ -7,6 +7,7 @@ use egglog_ast::span::Span;
 pub(crate) fn desugar_command(
     command: Command,
     parser: &mut Parser,
+    proof_testing: bool,
 ) -> Result<Vec<NCommand>, Error> {
     let rule_name = rule_name(&command);
     let res = match command {
@@ -30,10 +31,9 @@ pub(crate) fn desugar_command(
             schema,
             cost,
             unextractable,
+            true,
         ))],
-        Command::Relation { span, name, inputs } => vec![NCommand::Function(
-            FunctionDecl::relation(span, name, inputs),
-        )],
+        Command::Relation { span, name, inputs } => desugar_relation(parser, span, name, inputs),
         Command::Datatype {
             span,
             name,
@@ -77,6 +77,7 @@ pub(crate) fn desugar_command(
                         },
                         variant.cost,
                         false,
+                        true,
                     )));
                 }
             }
@@ -112,7 +113,13 @@ pub(crate) fn desugar_command(
             vec![NCommand::PrintOverallStatistics(span, file.clone())]
         }
         Command::Extract(span, expr, variants) => vec![NCommand::Extract(span, expr, variants)],
-        Command::Check(span, facts) => vec![NCommand::Check(span, facts)],
+        Command::Check(span, facts) => {
+            if proof_testing {
+                desugar_prove(parser, span.clone(), facts.clone())
+            } else {
+                vec![NCommand::Check(span, facts)]
+            }
+        }
         Command::PrintFunction(span, symbol, size, file, mode) => {
             vec![NCommand::PrintFunction(span, symbol, size, file, mode)]
         }
@@ -127,7 +134,7 @@ pub(crate) fn desugar_command(
             vec![NCommand::Pop(span, num)]
         }
         Command::Fail(span, cmd) => {
-            let mut desugared = desugar_command(*cmd, parser)?;
+            let mut desugared = desugar_command(*cmd, parser, proof_testing)?;
 
             let last = desugared.pop().unwrap();
             desugared.push(NCommand::Fail(span, Box::new(last)));
@@ -139,11 +146,75 @@ pub(crate) fn desugar_command(
         Command::UserDefined(span, name, args) => {
             vec![NCommand::UserDefined(span, name, args)]
         }
+        Command::Prove(span, query) => desugar_prove(parser, span, query),
+        Command::ProveExists(span, constructor) => {
+            vec![NCommand::ProveExists(span, constructor)]
+        }
     };
 
     Ok(res)
 }
 
+/// Desugars a `prove` command into egglog commands.
+/// For example, `(prove (= a b))` becomes:
+/// ```text
+/// (sort ExistsSort)
+/// (function ExistsConstructor () ExistsSort)
+/// (ruleset exists)
+/// (rule ((= a b))
+///       ((ExistsConstructor))
+///       :ruleset exists
+///       :name "prove_exists_rule")
+/// (run exists)
+/// (prove-exists ExistsConstructor)
+/// ```
+/// This creates a fresh constructor that can only be created if the query holds.
+/// Then `prove-exists` extracts a proof that the constructor exists.
+fn desugar_prove(parser: &mut Parser, span: Span, query: Vec<Fact>) -> Vec<NCommand> {
+    let fresh_sort = parser.symbol_gen.fresh("ExistsSort");
+    let constructor_name = parser.symbol_gen.fresh("ExistsConstructor");
+    let ruleset = parser.symbol_gen.fresh("exists");
+    let name = parser.symbol_gen.fresh("prove_exists_rule");
+    vec![
+        NCommand::Sort(span.clone(), fresh_sort.clone(), None),
+        NCommand::Function(FunctionDecl::constructor(
+            span.clone(),
+            constructor_name.clone(),
+            Schema {
+                input: vec![],
+                output: fresh_sort.clone(),
+            },
+            None,
+            false,
+            false,
+        )),
+        NCommand::AddRuleset(span.clone(), ruleset.clone()),
+        // rule that constructs the new constructor
+        NCommand::NormRule {
+            rule: Rule {
+                span: span.clone(),
+                body: query,
+                head: Actions::singleton(Action::Expr(
+                    span.clone(),
+                    Expr::Call(span.clone(), constructor_name.clone(), vec![]),
+                )),
+                ruleset: ruleset.clone(),
+                name,
+            },
+        },
+        // run the rule
+        NCommand::RunSchedule(GenericSchedule::Run(
+            span.clone(),
+            GenericRunConfig {
+                ruleset,
+                until: None,
+            },
+        )),
+        // get a proof for the constructor
+        NCommand::ProveExists(span, constructor_name),
+    ]
+}
+
 fn desugar_datatype(span: Span, name: String, variants: Vec<Variant>) -> Vec<NCommand> {
     vec![NCommand::Sort(span.clone(), name.clone(), None)]
         .into_iter()
@@ -157,6 +228,7 @@ fn desugar_datatype(span: Span, name: String, variants: Vec<Variant>) -> Vec<NCo
                 },
                 variant.cost,
                 variant.unextractable,
+                true,
             ))
         }))
         .collect()
@@ -237,6 +309,31 @@ fn desugar_birewrite(
         .collect()
 }
 
+/// Desugar relation by making a new sort and a constructor for it.
+fn desugar_relation(
+    parser: &mut Parser,
+    span: Span,
+    name: String,
+    inputs: Vec<String>,
+) -> Vec<NCommand> {
+    let dashes_removed = name.replace('-', "");
+    let fresh_sort = parser.symbol_gen.fresh(&format!("{dashes_removed}Sort"));
+    vec![
+        NCommand::Sort(span.clone(), fresh_sort.clone(), None),
+        NCommand::Function(FunctionDecl::constructor(
+            span,
+            name,
+            Schema {
+                input: inputs,
+                output: fresh_sort,
+            },
+            None,
+            false,
+            false,
+        )),
+    ]
+}
+
 pub fn rule_name<Head, Leaf>(command: &GenericCommand<Head, Leaf>) -> String
 where
     Head: Clone + Display,

src/ast/expr.rs

@@ -38,8 +38,7 @@ impl Hash for ResolvedVar {
 
 impl Display for ResolvedVar {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
-        let display_name = crate::util::sanitize_internal_name(&self.name);
-        write!(f, "{}", display_name)
+        write!(f, "{}", self.name)
     }
 }