Enforce cargo fmt

.travis.yml

@@ -2,9 +2,13 @@ language: rust
 rust:
   - beta
   - nightly
+cache: cargo
 script:
+  # RUSTC_BOOTSTRAP enables e.g. #![feature] on beta
+  - rustup component add rustfmt
   - cd chalk-engine && RUSTC_BOOTSTRAP=1 cargo build --no-default-features && cd ..
   - cd chalk-engine && RUSTC_BOOTSTRAP=1 cargo build --all-features && cd ..
+  - cargo fmt --all -- --check
   - RUSTC_BOOTSTRAP=1 cargo test --all
   - RUSTC_BOOTSTRAP=1 cargo doc --all --document-private-items
 deploy:

chalk-engine/src/context/prelude.rs

@@ -1,8 +1,8 @@
 #![allow(unused_imports)] // rustc bug
 
+pub(crate) use super::AggregateOps;
 pub(crate) use super::Context;
 pub(crate) use super::ContextOps;
-pub(crate) use super::AggregateOps;
+pub(crate) use super::InferenceTable;
 pub(crate) use super::ResolventOps;
 pub(crate) use super::TruncateOps;
-pub(crate) use super::InferenceTable;

chalk-engine/src/derived.rs

@@ -2,21 +2,24 @@
 // because the `#[derive()]` would add requirements onto the context
 // object that are not needed.
 
-use std::cmp::{PartialEq, Eq};
+use super::*;
+use std::cmp::{Eq, PartialEq};
 use std::hash::{Hash, Hasher};
 use std::mem;
-use super::*;
 
 impl<C: Context> PartialEq for DelayedLiteralSet<C> {
     fn eq(&self, other: &Self) -> bool {
-        let DelayedLiteralSet { delayed_literals: a1 } = self;
-        let DelayedLiteralSet { delayed_literals: a2 } = other;
+        let DelayedLiteralSet {
+            delayed_literals: a1,
+        } = self;
+        let DelayedLiteralSet {
+            delayed_literals: a2,
+        } = other;
         a1 == a2
     }
 }
 
-impl<C: Context> Eq for DelayedLiteralSet<C> {
-}
+impl<C: Context> Eq for DelayedLiteralSet<C> {}
 
 ///////////////////////////////////////////////////////////////////////////
 
@@ -27,22 +30,20 @@ impl<C: Context> PartialEq for DelayedLiteral<C> {
         }
 
         match (self, other) {
-            (DelayedLiteral::CannotProve(()), DelayedLiteral::CannotProve(())) =>
-                true,
+            (DelayedLiteral::CannotProve(()), DelayedLiteral::CannotProve(())) => true,
 
-            (DelayedLiteral::Negative(a1), DelayedLiteral::Negative(a2)) =>
-                a1 == a2,
+            (DelayedLiteral::Negative(a1), DelayedLiteral::Negative(a2)) => a1 == a2,
 
-            (DelayedLiteral::Positive(a1, b1), DelayedLiteral::Positive(a2, b2)) =>
-                a1 == a2 && b1 == b2,
+            (DelayedLiteral::Positive(a1, b1), DelayedLiteral::Positive(a2, b2)) => {
+                a1 == a2 && b1 == b2
+            }
 
-            _ => panic!()
+            _ => panic!(),
         }
     }
 }
 
-impl<C: Context> Eq for DelayedLiteral<C> {
-}
+impl<C: Context> Eq for DelayedLiteral<C> {}
 
 impl<C: Context> Hash for DelayedLiteral<C> {
     fn hash<H: Hasher>(&self, hasher: &mut H) {
@@ -76,8 +77,7 @@ impl<C: Context> PartialEq for Literal<C> {
     }
 }
 
-impl<C: Context> Eq for Literal<C> {
-}
+impl<C: Context> Eq for Literal<C> {}
 
 impl<C: Context> Hash for Literal<C> {
     fn hash<H: Hasher>(&self, state: &mut H) {
@@ -89,4 +89,3 @@ impl<C: Context> Hash for Literal<C> {
         }
     }
 }
-

chalk-engine/src/forest.rs

@@ -1,10 +1,10 @@
-use crate::{DepthFirstNumber, SimplifiedAnswer, TableIndex};
 use crate::context::prelude::*;
 use crate::context::AnswerStream;
 use crate::logic::RootSearchFail;
 use crate::stack::{Stack, StackIndex};
-use crate::tables::Tables;
 use crate::table::{Answer, AnswerIndex};
+use crate::tables::Tables;
+use crate::{DepthFirstNumber, SimplifiedAnswer, TableIndex};
 
 pub struct Forest<C: Context, CO: ContextOps<C>> {
     #[allow(dead_code)]
@@ -79,7 +79,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// as much work towards `goal` as it has to (and that works is
     /// cached for future attempts).
     pub fn solve(&mut self, goal: &C::UCanonicalGoalInEnvironment) -> Option<C::Solution> {
-        self.context.clone().make_solution(CO::canonical(&goal), self.iter_answers(goal))
+        self.context
+            .clone()
+            .make_solution(CO::canonical(&goal), self.iter_answers(goal))
     }
 
     /// True if all the tables on the stack starting from `depth` and

chalk-engine/src/hh.rs

@@ -22,4 +22,3 @@ pub enum HhGoal<C: Context> {
     /// as cannot prove.
     CannotProve,
 }
-

chalk-engine/src/logic.rs

@@ -1,12 +1,13 @@
-use crate::{DelayedLiteral, DelayedLiteralSet, DepthFirstNumber, ExClause, Literal, Minimums,
-            TableIndex};
+use crate::context::{prelude::*, WithInstantiatedExClause, WithInstantiatedUCanonicalGoal};
 use crate::fallible::NoSolution;
-use crate::context::{WithInstantiatedExClause, WithInstantiatedUCanonicalGoal, prelude::*};
 use crate::forest::Forest;
 use crate::hh::HhGoal;
 use crate::stack::StackIndex;
 use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand};
 use crate::table::{Answer, AnswerIndex};
+use crate::{
+    DelayedLiteral, DelayedLiteralSet, DepthFirstNumber, ExClause, Literal, Minimums, TableIndex,
+};
 use rustc_hash::FxHashSet;
 use std::marker::PhantomData;
 use std::mem;
@@ -117,7 +118,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         }
 
         self.tables[table].strands_mut().any(|strand| {
-            test(CO::inference_normalized_subst_from_ex_clause(&strand.canonical_ex_clause))
+            test(CO::inference_normalized_subst_from_ex_clause(
+                &strand.canonical_ex_clause,
+            ))
         })
     }
 
@@ -291,7 +294,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         }
 
         impl<C: Context, CO: ContextOps<C>, OP: WithInstantiatedStrand<C, CO>>
-            WithInstantiatedExClause<C> for With<C, CO, OP> {
+            WithInstantiatedExClause<C> for With<C, CO, OP>
+        {
             type Output = OP::Output;
 
             fn with<I: Context>(
@@ -401,7 +405,11 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// encounters a cycle, and that some of those cycles involve
     /// negative edges. In that case, walks all negative edges and
     /// converts them to delayed literals.
-    fn delay_strands_after_cycle(&mut self, table: TableIndex, visited: &mut FxHashSet<TableIndex>) {
+    fn delay_strands_after_cycle(
+        &mut self,
+        table: TableIndex,
+        visited: &mut FxHashSet<TableIndex>,
+    ) {
         let mut tables = vec![];
 
         let num_universes = CO::num_universes(&self.tables[table].table_goal);
@@ -562,7 +570,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         debug!("answer: table={:?}, answer_subst={:?}", table, answer_subst);
 
         let delayed_literals = {
-            let delayed_literals: FxHashSet<_> = delayed_literals.into_iter()
+            let delayed_literals: FxHashSet<_> = delayed_literals
+                .into_iter()
                 .map(|dl| infer.lift_delayed_literal(dl))
                 .collect();
             DelayedLiteralSet { delayed_literals }
@@ -739,7 +748,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         }
 
         impl<C: Context, CO: ContextOps<C>> WithInstantiatedUCanonicalGoal<C>
-                                                for PushInitialStrandsInstantiated<'a, C, CO> {
+            for PushInitialStrandsInstantiated<'a, C, CO>
+        {
             type Output = ();
 
             fn with<I: Context>(
@@ -1052,10 +1062,14 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
             ),
         };
 
-        let table_goal = &CO::map_goal_from_canonical(&universe_map,
-                                                     &CO::canonical(&self.tables[subgoal_table].table_goal));
-        let answer_subst =
-            &CO::map_subst_from_canonical(&universe_map, &self.answer(subgoal_table, answer_index).subst);
+        let table_goal = &CO::map_goal_from_canonical(
+            &universe_map,
+            &CO::canonical(&self.tables[subgoal_table].table_goal),
+        );
+        let answer_subst = &CO::map_subst_from_canonical(
+            &universe_map,
+            &self.answer(subgoal_table, answer_index).subst,
+        );
         match infer.apply_answer_subst(ex_clause, &subgoal, table_goal, answer_subst) {
             Ok(mut ex_clause) => {
                 // If the answer had delayed literals, we have to

chalk-engine/src/simplify.rs

@@ -1,8 +1,8 @@
+use crate::context::prelude::*;
 use crate::fallible::Fallible;
-use crate::{ExClause, Literal};
 use crate::forest::Forest;
 use crate::hh::HhGoal;
-use crate::context::prelude::*;
+use crate::{ExClause, Literal};
 
 impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// Simplifies an HH goal into a series of positive domain goals
@@ -45,7 +45,10 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
                 HhGoal::Not(subgoal) => {
                     ex_clause
                         .subgoals
-                        .push(Literal::Negative(I::goal_in_environment(&environment, subgoal)));
+                        .push(Literal::Negative(I::goal_in_environment(
+                            &environment,
+                            subgoal,
+                        )));
                 }
                 HhGoal::Unify(variance, a, b) => {
                     let result = infer.unify_parameters(&environment, variance, &a, &b)?;
@@ -69,7 +72,10 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
                     let goal = infer.cannot_prove();
                     ex_clause
                         .subgoals
-                        .push(Literal::Negative(I::goal_in_environment(&environment, goal)));
+                        .push(Literal::Negative(I::goal_in_environment(
+                            &environment,
+                            goal,
+                        )));
                 }
             }
         }

chalk-engine/src/stack.rs

@@ -48,7 +48,7 @@ impl Stack {
     }
 
     pub(super) fn top_of_stack_from(&self, depth: StackIndex) -> Range<StackIndex> {
-        depth .. StackIndex::from(self.stack.len())
+        depth..StackIndex::from(self.stack.len())
     }
 
     pub(super) fn push(&mut self, table: TableIndex, dfn: DepthFirstNumber) -> StackIndex {

chalk-engine/src/strand.rs

@@ -1,7 +1,7 @@
-use std::fmt::{Debug, Error, Formatter};
-use crate::{ExClause, TableIndex};
 use crate::context::{Context, InferenceTable};
 use crate::table::AnswerIndex;
+use crate::{ExClause, TableIndex};
+use std::fmt::{Debug, Error, Formatter};
 
 #[derive(Debug)]
 pub(crate) struct CanonicalStrand<C: Context> {

chalk-engine/src/table.rs

@@ -1,9 +1,9 @@
-use crate::{DelayedLiteralSet, DelayedLiteralSets};
 use crate::context::prelude::*;
 use crate::strand::CanonicalStrand;
+use crate::{DelayedLiteralSet, DelayedLiteralSets};
 use rustc_hash::FxHashMap;
-use std::collections::VecDeque;
 use std::collections::hash_map::Entry;
+use std::collections::VecDeque;
 use std::mem;
 
 pub(crate) struct Table<C: Context> {
@@ -37,7 +37,6 @@ index_struct! {
     }
 }
 
-
 /// An "answer" in the on-demand solver corresponds to a fully solved
 /// goal for a particular table (modulo delayed literals). It contains
 /// a substitution
@@ -48,7 +47,10 @@ pub struct Answer<C: Context> {
 }
 
 impl<C: Context> Table<C> {
-    pub(crate) fn new(table_goal: C::UCanonicalGoalInEnvironment, coinductive_goal: bool) -> Table<C> {
+    pub(crate) fn new(
+        table_goal: C::UCanonicalGoalInEnvironment,
+        coinductive_goal: bool,
+    ) -> Table<C> {
         Table {
             table_goal,
             coinductive_goal,
@@ -93,7 +95,9 @@ impl<C: Context> Table<C> {
 
         let added = match self.answers_hash.entry(answer.subst.clone()) {
             Entry::Vacant(entry) => {
-                entry.insert(DelayedLiteralSets::singleton(answer.delayed_literals.clone()));
+                entry.insert(DelayedLiteralSets::singleton(
+                    answer.delayed_literals.clone(),
+                ));
                 true
             }
 

chalk-engine/src/tables.rs

@@ -1,6 +1,6 @@
-use crate::TableIndex;
 use crate::context::prelude::*;
 use crate::table::Table;
+use crate::TableIndex;
 use rustc_hash::FxHashMap;
 use std::ops::{Index, IndexMut};
 
@@ -29,7 +29,11 @@ impl<C: Context> Tables<C> {
         }
     }
 
-    pub(super) fn insert(&mut self, goal: C::UCanonicalGoalInEnvironment, coinductive_goal: bool) -> TableIndex {
+    pub(super) fn insert(
+        &mut self,
+        goal: C::UCanonicalGoalInEnvironment,
+        coinductive_goal: bool,
+    ) -> TableIndex {
         let index = self.next_index();
         self.tables.push(Table::new(goal.clone(), coinductive_goal));
         self.table_indices.insert(goal, index);
@@ -63,4 +67,3 @@ impl<'a, C: Context> IntoIterator for &'a mut Tables<C> {
         IntoIterator::into_iter(&mut self.tables)
     }
 }
-