Remove unused proofs option

egraphs-good · Oct 5, 2024 · 59030f4 · 59030f4
1 parent 8ac9cae
commit 59030f4
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 22 deletions.
diff --git a/src/ast/desugar.rs b/src/ast/desugar.rs
@@ -179,7 +179,6 @@ fn desugar_simplify(
             },
             desugar,
             false,
-            false,
         )
         .unwrap(),
     );
@@ -198,7 +197,6 @@ pub(crate) fn rewrite_name(rewrite: &Rewrite) -> String {
 pub(crate) fn desugar_command(
     command: Command,
     desugar: &mut Desugar,
-    get_all_proofs: bool,
     seminaive_transform: bool,
 ) -> Result<Vec<NCommand>, Error> {
     let res = match command {
@@ -232,7 +230,6 @@ pub(crate) fn desugar_command(
             return desugar_commands(
                 desugar.parse_program(Some(file), &s)?,
                 desugar,
-                get_all_proofs,
                 seminaive_transform,
             );
         }
@@ -333,15 +330,7 @@ pub(crate) fn desugar_command(
                 ]
             }
         }
-        Command::Check(span, facts) => {
-            let res = vec![NCommand::Check(span, facts)];
-
-            if get_all_proofs {
-                // TODO check proofs
-            }
-
-            res
-        }
+        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)]
@@ -355,7 +344,7 @@ pub(crate) fn desugar_command(
             vec![NCommand::Pop(span, num)]
         }
         Command::Fail(span, cmd) => {
-            let mut desugared = desugar_command(*cmd, desugar, false, seminaive_transform)?;
+            let mut desugared = desugar_command(*cmd, desugar, seminaive_transform)?;
 
             let last = desugared.pop().unwrap();
             desugared.push(NCommand::Fail(span, Box::new(last)));
@@ -372,12 +361,11 @@ pub(crate) fn desugar_command(
 pub(crate) fn desugar_commands(
     program: Vec<Command>,
     desugar: &mut Desugar,
-    get_all_proofs: bool,
     seminaive_transform: bool,
 ) -> Result<Vec<NCommand>, Error> {
     let mut res = vec![];
     for command in program {
-        let desugared = desugar_command(command, desugar, get_all_proofs, seminaive_transform)?;
+        let desugared = desugar_command(command, desugar, seminaive_transform)?;
         res.extend(desugared);
     }
     Ok(res)
@@ -400,10 +388,9 @@ impl Desugar {
     pub(crate) fn desugar_program(
         &mut self,
         program: Vec<Command>,
-        get_all_proofs: bool,
         seminaive_transform: bool,
     ) -> Result<Vec<NCommand>, Error> {
-        let res = desugar_commands(program, self, get_all_proofs, seminaive_transform)?;
+        let res = desugar_commands(program, self, seminaive_transform)?;
         Ok(res)
     }
 

diff --git a/src/lib.rs b/src/lib.rs
@@ -433,7 +433,6 @@ pub struct EGraph {
     interactive_mode: bool,
     timestamp: u32,
     pub run_mode: RunMode,
-    pub test_proofs: bool,
     pub fact_directory: Option<PathBuf>,
     pub seminaive: bool,
     type_info: TypeInfo,
@@ -457,7 +456,6 @@ impl Default for EGraph {
             timestamp: 0,
             run_mode: RunMode::Normal,
             interactive_mode: false,
-            test_proofs: false,
             fact_directory: None,
             seminaive: true,
             extract_report: None,
@@ -1419,9 +1417,9 @@ impl EGraph {
     }
 
     fn process_command(&mut self, command: Command) -> Result<Vec<ResolvedNCommand>, Error> {
-        let program =
-            self.desugar
-                .desugar_program(vec![command], self.test_proofs, self.seminaive)?;
+        let program = self
+            .desugar
+            .desugar_program(vec![command], self.seminaive)?;
 
         let program = self.type_info.typecheck_program(&program)?;