fix warnings

Author: arshiamoeini

hakim-engine/src/brain.rs

@@ -321,7 +321,7 @@ pub fn remove_unused_var(t: TermRef) -> Option<TermRef> {
             x - 1
         }
     });
-    is_unused.then(|| t)
+    is_unused.then_some(t)
 }
 
 fn deny_wild(t: &Term) -> Result<()> {

hakim-engine/src/interactive.rs

@@ -409,11 +409,11 @@ impl Frame {
         let hyp = self
             .hyps
             .get(index)
-            .ok_or(tactic::Error::UnknownHyp(index.to_string()))?;
+            .ok_or_else(|| tactic::Error::UnknownHyp(index.to_string()))?;
         self.deny_dependency(&hyp.name)?;
         self.engine.remove_name_unchecked(&hyp.name);
         let hyp = self.hyps.remove(index);
-        return Ok(hyp);
+        Ok(hyp)
     }
 
     pub fn suggest_on_goal_dblclk(&self) -> Option<Suggestion> {
@@ -431,7 +431,6 @@ impl Frame {
     pub fn suggest_on_hyp_menu(&self, hyp_name: &str) -> Vec<Suggestion> {
         suggest_on_hyp(self, hyp_name)
     }
-
     pub fn run_tactic(&self, line: &str) -> Result<Vec<Self>, tactic::Error> {
         let parts = smart_split(line);
         let mut parts = parts.iter().map(|x| x.as_str());

hakim-engine/src/interactive/suggest/goal.rs

@@ -42,10 +42,5 @@ pub fn suggest_on_goal(goal: &Term, frame: &Frame) -> Vec<Suggestion> {
 
 pub fn suggest_on_goal_dblclk(goal: &Term, frame: &Frame) -> Option<Suggestion> {
     let suggs = suggest_on_goal(goal, frame);
-    for sugg in suggs {
-        if sugg.is_default() {
-            return Some(sugg);
-        }
-    }
-    None
+    suggs.into_iter().find(|sugg| sugg.is_default())
 }

hakim-engine/src/interactive/suggest/hyp.rs

@@ -71,10 +71,5 @@ fn seq_builder<'a>(l: impl IntoIterator<Item = &'a str>) -> String {
 
 pub fn suggest_on_hyp_dblclk(frame: &Frame, name: &str) -> Option<Suggestion> {
     let suggs = suggest_on_hyp(frame, name);
-    for sugg in suggs {
-        if sugg.is_default() {
-            return Some(sugg);
-        }
-    }
-    None
+    suggs.into_iter().find(|sugg| sugg.is_default())
 }

hakim-engine/src/interactive/tactic/apply.rs

@@ -73,7 +73,7 @@ impl FindInstance {
         for i in dep_list
             .iter()
             .enumerate()
-            .filter_map(|(i, x)| (!x).then(|| i))
+            .filter_map(|(i, x)| (!x).then_some(i))
         {
             if self.infer.terms[i] == VarCategory::Term(i).to_term(None) {
                 writeln!(r, "\u{2068}{:?}\u{2069}", self.infer.tys[i]).unwrap();

hakim-engine/src/interactive/tactic/auto_list.rs

@@ -36,29 +36,26 @@ fn list_item_from_term(t: TermRef) -> ListItem {
                         Term::Axiom { unique_name, .. } => {
                             if unique_name == "tail" {
                                 let mut list = f(op2.clone());
-                                if let Some(first) = list.next() {
-                                    match first {
-                                        ListPart::Element(_) => return Box::new(list),
-                                        /*ListPart::Atom(_x) => {
-                                            todo!();
-                                            /*let tail_of_first = Term::App {
-                                                func: Term::App {
-                                                    func: TermRef::Axiom {
-                                                        ty: axiom_ty,
-                                                        unique_name: unique_name,
-                                                    },
-                                                    op: op1,
+                                if let Some(ListPart::Element(_)) = list.next() {
+                                    return Box::new(list);
+                                    /*ListPart::Atom(_x) => {
+                                        todo!();
+                                        /*let tail_of_first = Term::App {
+                                            func: Term::App {
+                                                func: TermRef::Axiom {
+                                                    ty: axiom_ty,
+                                                    unique_name: unique_name,
                                                 },
-                                                op: x,
-                                            };
-                                            //tail_of_first := tail op1 x
-                                            return Box::new(
-                                                iter::once(ListPart::Atom(tail_of_first))
-                                                    .chain(list),
-                                            );*/
-                                        }*/
-                                        _ => (),
-                                    };
+                                                op: op1,
+                                            },
+                                            op: x,
+                                        };
+                                        //tail_of_first := tail op1 x
+                                        return Box::new(
+                                            iter::once(ListPart::Atom(tail_of_first))
+                                                .chain(list),
+                                        );*/
+                                    }*/
                                 }
                             }
                         }

hakim-engine/src/interactive/tactic/chain.rs

@@ -1,11 +1,9 @@
-use serde::__private::de;
-
 use super::{next_arg, next_arg_constant, rewrite::replace_term, Result};
 use crate::{
-    app, app_ref,
+    app_ref,
     brain::{Term, TermRef},
-    interactive::{tactic::rewrite::replace_term_in_frame, Frame},
-    library::prelude::{cons, list, nil},
+    interactive::Frame,
+    library::prelude::{list, nil},
 };
 
 fn eat_paren(mut x: &str) -> &str {
@@ -121,9 +119,7 @@ fn destruct_varible_with_term(
 
 #[cfg(test)]
 mod tests {
-    use crate::interactive::tests::{
-        run_interactive, run_interactive_to_end, run_interactive_to_fail,
-    };
+    use crate::interactive::tests::run_interactive_to_end;
 
     #[test]
     fn and_destruct() {

hakim-engine/src/interactive/tactic/lia.rs

@@ -384,6 +384,5 @@ mod tests {
     #[test]
     fn sets() {
         success(r#"|set_empty ℤ| = 0"#);
-
     }
 }

hakim-engine/src/interactive/tactic/rewrite.rs

@@ -3,7 +3,7 @@ use std::collections::HashSet;
 use crate::{
     brain::{Term, TermRef},
     interactive::Frame,
-    parser::{term_pretty_print, BinOp},
+    parser::BinOp,
     Abstraction,
 };
 
@@ -120,7 +120,7 @@ pub fn rewrite<'a>(mut frame: Frame, args: impl Iterator<Item = &'a str>) -> Res
     let exp = &get_one_arg(args, "rewrite")?;
     let term = frame.engine.calc_type(exp)?;
     let [op1, op2, _] =
-        get_eq_params(&(term)).ok_or(BadHyp("rewrite expect eq but got", term.clone()))?;
+        get_eq_params(&(term)).ok_or_else(|| BadHyp("rewrite expect eq but got", term.clone()))?;
     let result = if is_reverse {
         replace_term_in_frame(&mut frame, usize::MAX, op2, op1, &mut None)
     } else {

hakim-wasm/src/lib.rs

@@ -161,7 +161,7 @@ impl Instance {
 
     #[wasm_bindgen]
     pub fn natural(&self) -> Option<String> {
-        let s = (&self.session).as_ref()?;
+        let s = self.session.as_ref()?;
         Some(s.natural())
     }
 
@@ -174,7 +174,7 @@ impl Instance {
     }
 
     pub fn try_auto(&self) -> Option<String> {
-        let s = (&self.session).as_ref()?.clone();
+        let s = self.session.as_ref()?.clone();
         s.try_auto()
     }