Merge pull request #434 from Alex-Fischman/unused

More dead code removal

src/ast/desugar.rs

@@ -175,7 +175,6 @@ fn desugar_simplify(
             },
             desugar,
             false,
-            false,
         )
         .unwrap(),
     );
@@ -194,7 +193,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 {
@@ -228,7 +226,6 @@ pub(crate) fn desugar_command(
             return desugar_commands(
                 parse_program(Some(file), &s)?,
                 desugar,
-                get_all_proofs,
                 seminaive_transform,
             );
         }
@@ -329,16 +326,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::CheckProof => vec![NCommand::CheckProof],
+        Command::Check(span, facts) => vec![NCommand::Check(span, facts)],
         Command::PrintFunction(span, symbol, size) => {
             vec![NCommand::PrintTable(span, symbol, size)]
         }
@@ -351,7 +339,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)));
@@ -368,12 +356,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)
@@ -395,10 +382,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)
     }
 }

src/ast/mod.rs

@@ -222,7 +222,6 @@ where
     RunSchedule(GenericSchedule<Head, Leaf>),
     PrintOverallStatistics,
     Check(Span, Vec<GenericFact<Head, Leaf>>),
-    CheckProof,
     PrintTable(Span, Symbol, usize),
     PrintSize(Span, Option<Symbol>),
     Output {
@@ -274,7 +273,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)
             }
@@ -334,7 +332,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)
             }
@@ -784,8 +781,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
@@ -867,7 +862,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

@@ -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,
@@ -487,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
     }
@@ -1147,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;
@@ -1245,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}")
@@ -1419,9 +1405,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)?;
 

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)