fmt

egraphs-good · Oct 23, 2024 · 9d6c6ce · 9d6c6ce
1 parent 876c63f
commit 9d6c6ce
Show file tree

Hide file tree

Showing 11 changed files with 263 additions and 57 deletions.
diff --git a/src/actions.rs b/src/actions.rs
@@ -97,10 +97,8 @@ impl<'a> ActionCompiler<'a> {
     }
 
     fn do_prim(&mut self, prim: &SpecializedPrimitive) {
-        self.instructions.push(Instruction::CallPrimitive(
-            prim.clone(),
-            prim.input.len(),
-        ));
+        self.instructions
+            .push(Instruction::CallPrimitive(prim.clone(), prim.input.len()));
     }
 }
 
@@ -321,7 +319,9 @@ impl EGraph {
                 Instruction::CallPrimitive(p, arity) => {
                     let new_len = stack.len() - arity;
                     let values = &stack[new_len..];
-                    if let Some(value) = p.primitive.apply(values, (&p.input, &p.output), Some(self)) {
+                    if let Some(value) =
+                        p.primitive.apply(values, (&p.input, &p.output), Some(self))
+                    {
                         stack.truncate(new_len);
                         stack.push(value);
                     } else {

diff --git a/src/constraint.rs b/src/constraint.rs
@@ -108,10 +108,9 @@ impl ConstraintError<AtomTerm, ArcSort> {
             ConstraintError::ImpossibleCaseIdentified(
                 ImpossibleConstraint::CompileTimeConstantExpected { span, sort },
             ) => TypeError::CompileTimeConstantExpected(sort.clone(), span.clone()),
-            ConstraintError::ImpossibleCaseIdentified(ImpossibleConstraint::UnboundedFunction {
-                head,
-                span,
-            }) => TypeError::UnboundFunction(*head, span.clone()),
+            ConstraintError::ImpossibleCaseIdentified(
+                ImpossibleConstraint::UnboundedFunction { head, span },
+            ) => TypeError::UnboundFunction(*head, span.clone()),
         }
     }
 }
@@ -243,7 +242,7 @@ where
         if let Some(new_self) = new_self {
             *self = new_self;
         }
-        return result;
+        result
     }
 }
 
@@ -732,11 +731,11 @@ fn get_literal_and_global_constraints<'a, 'b>(
             AtomTerm::Var(_, _) => None,
             // Literal to type constraint
             AtomTerm::Literal(_, lit) => {
-                let typ = crate::sort::literal_sort(&lit);
+                let typ = crate::sort::literal_sort(lit);
                 Some(Constraint::Assign(arg.clone(), typ))
             }
             AtomTerm::Global(_, v) => {
-                if let Some(typ) = type_info.lookup_global(&v) {
+                if let Some(typ) = type_info.lookup_global(v) {
                     Some(Constraint::Assign(arg.clone(), typ.clone()))
                 } else {
                     panic!("All global variables should be bound before type checking")

diff --git a/src/lib.rs b/src/lib.rs
@@ -76,7 +76,12 @@ pub trait PrimitiveLike {
     /// Constructs a type constraint for the primitive that uses the span information
     /// for error localization.
     fn get_type_constraints(&self, span: &Span) -> Box<dyn TypeConstraint>;
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), egraph: Option<&mut EGraph>) -> Option<Value>;
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        egraph: Option<&mut EGraph>,
+    ) -> Option<Value>;
 }
 
 /// Running a schedule produces a report of the results.
@@ -371,7 +376,12 @@ impl PrimitiveLike for SimplePrimitive {
             .collect();
         SimpleTypeConstraint::new(self.name(), sorts, span.clone()).into_box()
     }
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         (self.f)(values)
     }
 }
@@ -1550,7 +1560,9 @@ mod tests {
     use std::sync::Arc;
 
     use crate::{
-        constraint::SimpleTypeConstraint, sort::{FromSort, I64Sort, IntoSort, Sort, VecSort}, ArcSort, EGraph, PrimitiveLike, Span, Value
+        constraint::SimpleTypeConstraint,
+        sort::{FromSort, I64Sort, IntoSort, Sort, VecSort},
+        ArcSort, EGraph, PrimitiveLike, Span, Value,
     };
 
     struct InnerProduct {

diff --git a/src/sort/fn.rs b/src/sort/fn.rs
@@ -322,7 +322,7 @@ impl TypeConstraint for FunctionCTorTypeConstraint {
                 ImpossibleConstraint::ArityMismatch {
                     atom: Atom {
                         span: self.span.clone(),
-                        head: self.name.clone(),
+                        head: self.name,
                         args: arguments.to_vec(),
                     },
                     expected: 1,
@@ -334,7 +334,7 @@ impl TypeConstraint for FunctionCTorTypeConstraint {
         let this = self.clone();
         let arguments = arguments.to_vec();
         let argument = arguments[0].clone();
-        return vec![Constraint::LazyConstraint(
+        vec![Constraint::LazyConstraint(
             arguments[0].clone(),
             Box::new(move |sort| {
                 let sort = sort.clone().as_arc_any();
@@ -386,7 +386,7 @@ impl TypeConstraint for FunctionCTorTypeConstraint {
 
                 Constraint::And(all_constraints)
             }),
-        )];
+        )]
     }
 }
 

diff --git a/src/sort/i64.rs b/src/sort/i64.rs
@@ -115,7 +115,12 @@ impl PrimitiveLike for CountMatches {
             .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let string1 = Symbol::load(&self.string, &values[0]).to_string();
         let string2 = Symbol::load(&self.string, &values[1]).to_string();
         Some(Value::from(string1.matches(&string2).count() as i64))

diff --git a/src/sort/map.rs b/src/sort/map.rs
@@ -237,7 +237,12 @@ impl PrimitiveLike for MapRebuild {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let egraph = egraph.unwrap();
         let maps = self.map.maps.lock().unwrap();
         let map = maps.get_index(values[0].bits as usize).unwrap();
@@ -272,7 +277,12 @@ impl PrimitiveLike for TermOrderingMin {
             .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         assert_eq!(values.len(), 2);
         if values[0] < values[1] {
             Some(values[0])
@@ -295,7 +305,12 @@ impl PrimitiveLike for TermOrderingMax {
             .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         assert_eq!(values.len(), 2);
         if values[0] > values[1] {
             Some(values[0])
@@ -314,7 +329,12 @@ impl PrimitiveLike for Ctor {
         SimpleTypeConstraint::new(self.name(), vec![self.map.clone()], span.clone()).into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         assert!(values.is_empty());
         ValueMap::default().store(&self.map)
     }
@@ -344,7 +364,12 @@ impl PrimitiveLike for Insert {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let mut map = ValueMap::load(&self.map, &values[0]);
         map.insert(values[1], values[2]);
         map.store(&self.map)
@@ -370,7 +395,12 @@ impl PrimitiveLike for Get {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let map = ValueMap::load(&self.map, &values[0]);
         map.get(&values[1]).copied()
     }
@@ -395,7 +425,12 @@ impl PrimitiveLike for NotContains {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let map = ValueMap::load(&self.map, &values[0]);
         if map.contains_key(&values[1]) {
             None
@@ -424,7 +459,12 @@ impl PrimitiveLike for Contains {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let map = ValueMap::load(&self.map, &values[0]);
         if map.contains_key(&values[1]) {
             Some(Value::unit())
@@ -453,7 +493,12 @@ impl PrimitiveLike for Remove {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let mut map = ValueMap::load(&self.map, &values[0]);
         map.remove(&values[1]);
         map.store(&self.map)
@@ -479,7 +524,12 @@ impl PrimitiveLike for Length {
         .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         let map = ValueMap::load(&self.map, &values[0]);
         Some(Value::from(map.len() as i64))
     }

diff --git a/src/sort/mod.rs b/src/sort/mod.rs
@@ -187,7 +187,12 @@ impl PrimitiveLike for ValueEq {
             .into_box()
     }
 
-    fn apply(&self, values: &[Value], _sorts: (&[ArcSort], &ArcSort), _egraph: Option<&mut EGraph>) -> Option<Value> {
+    fn apply(
+        &self,
+        values: &[Value],
+        _sorts: (&[ArcSort], &ArcSort),
+        _egraph: Option<&mut EGraph>,
+    ) -> Option<Value> {
         assert_eq!(values.len(), 2);
         if values[0] == values[1] {
             Some(Value::unit())