Remove unused CheckProof commands

src/ast/desugar.rs

@@ -331,7 +331,6 @@ pub(crate) fn desugar_command(
             }
         }
         Command::Check(span, facts) => vec![NCommand::Check(span, facts)],
-        Command::CheckProof => vec![NCommand::CheckProof],
         Command::PrintFunction(span, symbol, size) => {
             vec![NCommand::PrintTable(span, symbol, size)]
         }

src/ast/mod.rs

@@ -204,7 +204,6 @@ where
     RunSchedule(GenericSchedule<Head, Leaf>),
     PrintOverallStatistics,
     Check(Span, Vec<GenericFact<Head, Leaf>>),
-    CheckProof,
     PrintTable(Span, Symbol, usize),
     PrintSize(Span, Option<Symbol>),
     Output {
@@ -256,7 +255,6 @@ where
             GenericNCommand::Check(span, facts) => {
                 GenericCommand::Check(span.clone(), facts.clone())
             }
-            GenericNCommand::CheckProof => GenericCommand::CheckProof,
             GenericNCommand::PrintTable(span, name, n) => {
                 GenericCommand::PrintFunction(span.clone(), *name, *n)
             }
@@ -316,7 +314,6 @@ where
                 span,
                 facts.into_iter().map(|fact| fact.visit_exprs(f)).collect(),
             ),
-            GenericNCommand::CheckProof => GenericNCommand::CheckProof,
             GenericNCommand::PrintTable(span, name, n) => {
                 GenericNCommand::PrintTable(span, name, n)
             }
@@ -766,8 +763,6 @@ where
     /// [INFO ] Command failed as expected.
     /// ```
     Check(Span, Vec<GenericFact<Head, Leaf>>),
-    /// Currently unused, this command will check proofs when they are implemented.
-    CheckProof,
     /// Print out rows a given function, extracting each of the elements of the function.
     /// Example:
     /// ```text
@@ -849,7 +844,6 @@ where
                 list!("query-extract", ":variants", variants, expr)
             }
             GenericCommand::Check(_ann, facts) => list!("check", ++ facts),
-            GenericCommand::CheckProof => list!("check-proof"),
             GenericCommand::Push(n) => list!("push", n),
             GenericCommand::Pop(_span, n) => list!("pop", n),
             GenericCommand::PrintFunction(_span, name, n) => list!("print-function", name, n),

src/ast/parse.lalrpop

@@ -83,7 +83,6 @@ Command: Command = {
         => Command::Simplify { span: Span(srcfile.clone(), lo, hi), expr, schedule },
     <lo:LParen> "query-extract" <variants:(":variants" <UNum>)?> <expr:Expr> <hi:RParen> => Command::QueryExtract { span: Span(srcfile.clone(), lo, hi), expr, variants: variants.unwrap_or(0) },
     <lo:LParen> "check" <facts:(Fact)*> <hi:RParen> => Command::Check(Span(srcfile.clone(), lo, hi), facts),
-    LParen "check-proof" RParen => Command::CheckProof,
       <lo:LParen> "run-schedule" <scheds:Schedule*> <hi:RParen> => 
         Command::RunSchedule(Schedule::Sequence(Span(srcfile.clone(), lo, hi), scheds)),
     LParen "print-stats" RParen => Command::PrintOverallStatistics,

src/lib.rs

@@ -485,14 +485,6 @@ struct SearchResult {
 }
 
 impl EGraph {
-    /// Use the rust backend implimentation of eqsat,
-    /// including a rust implementation of the union-find
-    /// data structure and the rust implementation of
-    /// the rebuilding algorithm (maintains congruence closure).
-    pub fn enable_terms_encoding(&mut self) {
-        panic!("terms are not implemented")
-    }
-
     pub fn is_interactive_mode(&self) -> bool {
         self.interactive_mode
     }
@@ -1145,9 +1137,6 @@ impl EGraph {
 
     fn set_option(&mut self, name: &str, value: ResolvedExpr) {
         match name {
-            "enable_proofs" => {
-                panic!("Proofs are not implemented")
-            }
             "interactive_mode" => {
                 if let ResolvedExpr::Lit(_ann, Literal::Int(i)) = value {
                     self.interactive_mode = i != 0;
@@ -1243,7 +1232,6 @@ impl EGraph {
                 self.check_facts(&span, &facts)?;
                 log::info!("Checked fact {:?}.", facts);
             }
-            ResolvedNCommand::CheckProof => log::error!("TODO implement proofs"),
             ResolvedNCommand::CoreAction(action) => match &action {
                 ResolvedAction::Let(_, name, contents) => {
                     panic!("Globals should have been desugared away: {name} = {contents}")

src/main.rs

@@ -14,16 +14,6 @@ struct Args {
     desugar: bool,
     #[clap(long)]
     resugar: bool,
-    /// Currently unused.
-    #[clap(long)]
-    proofs: bool,
-    /// Currently unused.
-    /// Use the rust backend implimentation of eqsat,
-    /// including a rust implementation of the union-find
-    /// data structure and the rust implementation of
-    /// the rebuilding algorithm (maintains congruence closure).
-    #[clap(long)]
-    terms_encoding: bool,
     #[clap(long, default_value_t = RunMode::Normal)]
     show: RunMode,
     // TODO remove this evil hack
@@ -113,15 +103,6 @@ fn main() {
         egraph.fact_directory = args.fact_directory.clone();
         egraph.seminaive = !args.naive;
         egraph.run_mode = args.show;
-        // NB: both terms_encoding and proofs are currently unused
-        if args.terms_encoding {
-            egraph.enable_terms_encoding();
-        }
-        if args.proofs {
-            egraph
-                .parse_and_run_program(None, "(set-option enable_proofs 1)")
-                .unwrap();
-        }
         egraph
     };
 

src/typechecking.rs

@@ -218,7 +218,6 @@ impl TypeInfo {
                 ResolvedNCommand::UnstableCombinedRuleset(*name, sub_rulesets.clone())
             }
             NCommand::PrintOverallStatistics => ResolvedNCommand::PrintOverallStatistics,
-            NCommand::CheckProof => ResolvedNCommand::CheckProof,
             NCommand::PrintTable(span, table, size) => {
                 ResolvedNCommand::PrintTable(span.clone(), *table, *size)
             }

tests/merge-saturates.egg

@@ -1,6 +1,3 @@
-;; SKIP_PROOFS
-;; doesn't work with proofs because of the side effect in
-;; the merge function
 (function foo () i64 :merge (min old new))
 
 (set (foo) 0)