Fix clippy lints

ufmg-smite · Jun 20, 2024 · 97ca792 · 97ca792
1 parent d04b5e6
commit 97ca792
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 61 deletions.
diff --git a/carcara/src/ast/polyeq.rs b/carcara/src/ast/polyeq.rs
@@ -364,70 +364,33 @@ impl Polyeq for Term {
                     _ => false,
                 }
             }
-            (Term::Const(Constant::Integer(i1)), Term::Op(Operator::Sub, args)) => {
-                if i1.is_negative() && args.len() == 1 {
-                    match args[0].as_ref() {
-                        Term::Const(Constant::Integer(i2)) if i1.clone().abs() == i2.clone() => {
-                            true
-                        }
-                        _ => false,
-                    }
-                } else {
-                    false
-                }
-            }
-            (Term::Op(Operator::Sub, args), Term::Const(Constant::Integer(i1))) => {
-                if i1.is_negative() && args.len() == 1 {
-                    match args[0].as_ref() {
-                        Term::Const(Constant::Integer(i2)) if i1.clone().abs() == i2.clone() => {
-                            true
-                        }
-                        _ => false,
-                    }
-                } else {
-                    false
-                }
-            }
-            (Term::Op(Operator::Sub, args), Term::Const(Constant::Real(r))) => {
-                if r.is_negative() && args.len() == 1 {
-                    match args[0].as_ref() {
-                        Term::Op(Operator::RealDiv, sub_args) => {
-                            match (sub_args[0].as_ref(), sub_args[1].as_ref()) {
-                                (
-                                    Term::Const(Constant::Real(r1)),
-                                    Term::Const(Constant::Real(r2)),
-                                ) if r1.is_integer() && r2.is_integer() => {
-                                    Rational::from((r1.numer(), r2.numer())) == r.clone().abs()
-                                }
-                                _ => false,
-                            }
-                        }
-                        Term::Const(Constant::Real(r1)) => r1.clone() == r.clone().abs(),
-                        _ => false,
-                    }
+            (Term::Const(Constant::Integer(i1)), Term::Op(Operator::Sub, args))
+            | (Term::Op(Operator::Sub, args), Term::Const(Constant::Integer(i1)))
+                if i1.is_negative() && args.len() == 1 =>
+            {
+                if let Term::Const(Constant::Integer(i2)) = args[0].as_ref() {
+                    i1.clone().abs() == i2.clone()
                 } else {
                     false
                 }
             }
-            (Term::Const(Constant::Real(r)), Term::Op(Operator::Sub, args)) => {
-                if r.is_negative() && args.len() == 1 {
-                    match args[0].as_ref() {
-                        Term::Op(Operator::RealDiv, sub_args) => {
-                            match (sub_args[0].as_ref(), sub_args[1].as_ref()) {
-                                (
-                                    Term::Const(Constant::Real(r1)),
-                                    Term::Const(Constant::Real(r2)),
-                                ) if r1.is_integer() && r2.is_integer() => {
-                                    Rational::from((r1.numer(), r2.numer())) == r.clone().abs()
-                                }
-                                _ => false,
+            (Term::Op(Operator::Sub, args), Term::Const(Constant::Real(r)))
+            | (Term::Const(Constant::Real(r)), Term::Op(Operator::Sub, args))
+                if r.is_negative() && args.len() == 1 =>
+            {
+                match args[0].as_ref() {
+                    Term::Op(Operator::RealDiv, sub_args) => {
+                        match (sub_args[0].as_ref(), sub_args[1].as_ref()) {
+                            (Term::Const(Constant::Real(r1)), Term::Const(Constant::Real(r2)))
+                                if r1.is_integer() && r2.is_integer() =>
+                            {
+                                Rational::from((r1.numer(), r2.numer())) == r.clone().abs()
                             }
+                            _ => false,
                         }
-                        Term::Const(Constant::Real(r1)) => r1.clone() == r.clone().abs(),
-                        _ => false,
                     }
-                } else {
-                    false
+                    Term::Const(Constant::Real(r1)) => r1.clone() == r.clone().abs(),
+                    _ => false,
                 }
             }
             _ => false,

diff --git a/carcara/src/elaborator/hole.rs b/carcara/src/elaborator/hole.rs
@@ -44,7 +44,7 @@ fn get_problem_string(
     use std::fmt::Write;
 
     let mut problem = String::new();
-    write!(&mut problem, "(set-option :produce-proofs true)\n").unwrap();
+    writeln!(&mut problem, "(set-option :produce-proofs true)").unwrap();
     write!(&mut problem, "{}", prelude).unwrap();
 
     let mut bytes = Vec::new();

diff --git a/carcara/src/elaborator/lia_generic.rs b/carcara/src/elaborator/lia_generic.rs
@@ -217,15 +217,15 @@ fn insert_solver_proof(
             if !covered.contains(&term) {
                 covered.insert(term.clone());
                 if assume_term_to_node.contains_key(&term) {
-                    return assume_term_to_node.get(&term).unwrap().clone();
+                    return assume_term_to_node[&term].clone();
                 }
             }
             // build new assumption proof node
-            return Rc::new(ProofNode::Assume {
+            Rc::new(ProofNode::Assume {
                 id: ids.next_id(),
                 depth: depth + 1,
                 term,
-            });
+            })
         })
         .collect();
 

diff --git a/carcara/tests/test_example_files.rs b/carcara/tests/test_example_files.rs
@@ -49,6 +49,7 @@ fn run_test(problem_path: &Path, proof_path: &Path) -> CarcaraResult<()> {
     // Then we elaborate it
     let config = elaborator::Config {
         lia_options: None,
+        hole_options: None,
         uncrowd_rotation: true,
     };
     let node = ast::ProofNode::from_commands(proof.commands.clone());