diff --git a/.travis.yml b/.travis.yml index 2fc4e348713..8c002296a97 100644 --- a/.travis.yml +++ b/.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: diff --git a/chalk-engine/src/context/prelude.rs b/chalk-engine/src/context/prelude.rs index 4cb85c47173..721354f89f7 100644 --- a/chalk-engine/src/context/prelude.rs +++ b/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; diff --git a/chalk-engine/src/derived.rs b/chalk-engine/src/derived.rs index 37b95ad1909..fc9449d25e1 100644 --- a/chalk-engine/src/derived.rs +++ b/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 PartialEq for DelayedLiteralSet { 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 Eq for DelayedLiteralSet { -} +impl Eq for DelayedLiteralSet {} /////////////////////////////////////////////////////////////////////////// @@ -27,22 +30,20 @@ impl PartialEq for DelayedLiteral { } 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 Eq for DelayedLiteral { -} +impl Eq for DelayedLiteral {} impl Hash for DelayedLiteral { fn hash(&self, hasher: &mut H) { @@ -76,8 +77,7 @@ impl PartialEq for Literal { } } -impl Eq for Literal { -} +impl Eq for Literal {} impl Hash for Literal { fn hash(&self, state: &mut H) { @@ -89,4 +89,3 @@ impl Hash for Literal { } } } - diff --git a/chalk-engine/src/forest.rs b/chalk-engine/src/forest.rs index 03f73451387..5d0fe06f839 100644 --- a/chalk-engine/src/forest.rs +++ b/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> { #[allow(dead_code)] @@ -79,7 +79,9 @@ impl> Forest { /// 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 { - 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 diff --git a/chalk-engine/src/hh.rs b/chalk-engine/src/hh.rs index d42156b920e..11c8967cba0 100644 --- a/chalk-engine/src/hh.rs +++ b/chalk-engine/src/hh.rs @@ -22,4 +22,3 @@ pub enum HhGoal { /// as cannot prove. CannotProve, } - diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index d0787611938..8b6e89de381 100644 --- a/chalk-engine/src/logic.rs +++ b/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> Forest { } 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> Forest { } impl, OP: WithInstantiatedStrand> - WithInstantiatedExClause for With { + WithInstantiatedExClause for With + { type Output = OP::Output; fn with( @@ -401,7 +405,11 @@ impl> Forest { /// 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) { + fn delay_strands_after_cycle( + &mut self, + table: TableIndex, + visited: &mut FxHashSet, + ) { let mut tables = vec![]; let num_universes = CO::num_universes(&self.tables[table].table_goal); @@ -562,7 +570,8 @@ impl> Forest { 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> Forest { } impl> WithInstantiatedUCanonicalGoal - for PushInitialStrandsInstantiated<'a, C, CO> { + for PushInitialStrandsInstantiated<'a, C, CO> + { type Output = (); fn with( @@ -1052,10 +1062,14 @@ impl> Forest { ), }; - 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 diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs index b06ac2a64f6..d46f3d8e99a 100644 --- a/chalk-engine/src/simplify.rs +++ b/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> Forest { /// Simplifies an HH goal into a series of positive domain goals @@ -45,7 +45,10 @@ impl> Forest { 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> Forest { 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, + ))); } } } diff --git a/chalk-engine/src/stack.rs b/chalk-engine/src/stack.rs index 98569c5b3c3..7ce6cfe7b97 100644 --- a/chalk-engine/src/stack.rs +++ b/chalk-engine/src/stack.rs @@ -48,7 +48,7 @@ impl Stack { } pub(super) fn top_of_stack_from(&self, depth: StackIndex) -> Range { - depth .. StackIndex::from(self.stack.len()) + depth..StackIndex::from(self.stack.len()) } pub(super) fn push(&mut self, table: TableIndex, dfn: DepthFirstNumber) -> StackIndex { diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs index 58e79fc709c..5102b6520b8 100644 --- a/chalk-engine/src/strand.rs +++ b/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 { diff --git a/chalk-engine/src/table.rs b/chalk-engine/src/table.rs index 207ec391347..2600d2d748b 100644 --- a/chalk-engine/src/table.rs +++ b/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 { @@ -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 { } impl Table { - pub(crate) fn new(table_goal: C::UCanonicalGoalInEnvironment, coinductive_goal: bool) -> Table { + pub(crate) fn new( + table_goal: C::UCanonicalGoalInEnvironment, + coinductive_goal: bool, + ) -> Table { Table { table_goal, coinductive_goal, @@ -93,7 +95,9 @@ impl Table { 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 } diff --git a/chalk-engine/src/tables.rs b/chalk-engine/src/tables.rs index 68580bb199d..44f97d78808 100644 --- a/chalk-engine/src/tables.rs +++ b/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 Tables { } } - 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 { IntoIterator::into_iter(&mut self.tables) } } - diff --git a/chalk-ir/src/cast.rs b/chalk-ir/src/cast.rs index 80436fa73e9..6ad4ea154e7 100644 --- a/chalk-ir/src/cast.rs +++ b/chalk-ir/src/cast.rs @@ -64,19 +64,28 @@ impl Cast for ProjectionEq { } } -impl Cast for T where T: Cast { +impl Cast for T +where + T: Cast, +{ fn cast(self) -> DomainGoal { DomainGoal::Holds(self.cast()) } } -impl Cast for T where T: Cast { +impl Cast for T +where + T: Cast, +{ fn cast(self) -> LeafGoal { LeafGoal::DomainGoal(self.cast()) } } -impl Cast for T where T: Cast { +impl Cast for T +where + T: Cast, +{ fn cast(self) -> Goal { Goal::Leaf(self.cast()) } @@ -119,7 +128,7 @@ impl> Cast for Binders { } else { Goal::Quantified( QuantifierKind::ForAll, - self.map(|bound| Box::new(bound.cast())) + self.map(|bound| Box::new(bound.cast())), ) } } @@ -149,7 +158,10 @@ impl Cast for Lifetime { } } -impl Cast for T where T: Cast { +impl Cast for T +where + T: Cast, +{ fn cast(self) -> ProgramClause { ProgramClause::Implies(ProgramClauseImplication { consequence: self.cast(), @@ -161,14 +173,12 @@ impl Cast for T where T: Cast { impl> Cast for Binders { fn cast(self) -> ProgramClause { if self.binders.is_empty() { - Cast::::cast(self.value) + Cast::::cast(self.value) } else { - ProgramClause::ForAll( - self.map(|bound| ProgramClauseImplication { - consequence: bound.cast(), - conditions: vec![], - }) - ) + ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication { + consequence: bound.cast(), + conditions: vec![], + })) } } } diff --git a/chalk-ir/src/could_match.rs b/chalk-ir/src/could_match.rs index 7143199b0c6..45053057c1c 100644 --- a/chalk-ir/src/could_match.rs +++ b/chalk-ir/src/could_match.rs @@ -1,5 +1,5 @@ -use crate::*; use crate::zip::{Zip, Zipper}; +use crate::*; /// A fast check to see whether two things could ever possibly match. pub trait CouldMatch { @@ -52,12 +52,8 @@ impl CouldMatch for T { impl CouldMatch for ProgramClause { fn could_match(&self, other: &DomainGoal) -> bool { match self { - ProgramClause::Implies(implication) => { - implication.consequence.could_match(other) - } - ProgramClause::ForAll(clause) => { - clause.value.consequence.could_match(other) - } + ProgramClause::Implies(implication) => implication.consequence.could_match(other), + ProgramClause::ForAll(clause) => clause.value.consequence.could_match(other), } } } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 91f0a70de4c..b4e6dfe65e6 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -55,7 +55,6 @@ impl Debug for InferenceVar { } } - impl Debug for QuantifiedTy { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { // FIXME -- we should introduce some names or something here diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs index 2ae4537ab5a..4e0f7511729 100644 --- a/chalk-ir/src/fold.rs +++ b/chalk-ir/src/fold.rs @@ -1,7 +1,7 @@ //! Traits for transforming bits of IR. -use crate::*; use crate::cast::Cast; +use crate::*; use chalk_engine::context::Context; use chalk_engine::{DelayedLiteral, ExClause, Literal}; use std::fmt::Debug; @@ -135,11 +135,7 @@ impl FreeVarFolder for T { } } - fn fold_free_var_lifetime( - &mut self, - depth: usize, - binders: usize, - ) -> Fallible { + fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible { if T::forbid() { panic!("unexpected free variable with depth `{:?}`", depth) } else { @@ -183,7 +179,11 @@ pub trait DefaultPlaceholderFolder { } impl PlaceholderFolder for T { - fn fold_free_placeholder_ty(&mut self, universe: PlaceholderIndex, _binders: usize) -> Fallible { + fn fold_free_placeholder_ty( + &mut self, + universe: PlaceholderIndex, + _binders: usize, + ) -> Fallible { if T::forbid() { panic!("unexpected placeholder type `{:?}`", universe) } else { @@ -334,11 +334,13 @@ impl Fold for Ty { pub fn super_fold_ty(folder: &mut dyn Folder, ty: &Ty, binders: usize) -> Fallible { match *ty { - Ty::BoundVar(depth) => if depth >= binders { - folder.fold_free_var_ty(depth - binders, binders) - } else { - Ok(Ty::BoundVar(depth)) - }, + Ty::BoundVar(depth) => { + if depth >= binders { + folder.fold_free_var_ty(depth - binders, binders) + } else { + Ok(Ty::BoundVar(depth)) + } + } Ty::InferenceVar(var) => folder.fold_inference_ty(var, binders), Ty::Apply(ref apply) => { let ApplicationTy { @@ -433,11 +435,13 @@ pub fn super_fold_lifetime( binders: usize, ) -> Fallible { match *lifetime { - Lifetime::BoundVar(depth) => if depth >= binders { - folder.fold_free_var_lifetime(depth - binders, binders) - } else { - Ok(Lifetime::BoundVar(depth)) - }, + Lifetime::BoundVar(depth) => { + if depth >= binders { + folder.fold_free_var_lifetime(depth - binders, binders) + } else { + Ok(Lifetime::BoundVar(depth)) + } + } Lifetime::InferenceVar(var) => folder.fold_inference_lifetime(var, binders), Lifetime::Placeholder(universe) => folder.fold_free_placeholder_lifetime(universe, binders), } diff --git a/chalk-ir/src/fold/shift.rs b/chalk-ir/src/fold/shift.rs index f01205a3cde..0da29acf687 100644 --- a/chalk-ir/src/fold/shift.rs +++ b/chalk-ir/src/fold/shift.rs @@ -1,7 +1,7 @@ -use crate::*; use super::{ - DefaultTypeFolder, Fold, FreeVarFolder, DefaultInferenceFolder, DefaultPlaceholderFolder, + DefaultInferenceFolder, DefaultPlaceholderFolder, DefaultTypeFolder, Fold, FreeVarFolder, }; +use crate::*; /// Methods for converting debruijn indices to move values into or out /// of binders. diff --git a/chalk-ir/src/fold/subst.rs b/chalk-ir/src/fold/subst.rs index a4cb85621e7..b7d4d53a29e 100644 --- a/chalk-ir/src/fold/subst.rs +++ b/chalk-ir/src/fold/subst.rs @@ -1,6 +1,5 @@ -use crate::fold::shift::Shift; -use crate::*; use super::*; +use crate::fold::shift::Shift; pub struct Subst<'s> { /// Values to substitute. A reference to a free variable with @@ -36,11 +35,7 @@ impl<'b> FreeVarFolder for Subst<'b> { } } - fn fold_free_var_lifetime( - &mut self, - depth: usize, - binders: usize, - ) -> Fallible { + fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible { if depth >= self.parameters.len() { Ok(Lifetime::BoundVar(depth - self.parameters.len() + binders)) } else { diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 4144b562ddb..308eac62a46 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -2,11 +2,11 @@ #![feature(specialization)] use crate::cast::Cast; -use chalk_engine::fallible::*; use crate::fold::shift::Shift; use crate::fold::{ DefaultInferenceFolder, DefaultPlaceholderFolder, DefaultTypeFolder, Fold, FreeVarFolder, }; +use chalk_engine::fallible::*; use lalrpop_intern::InternedString; use std::collections::BTreeSet; use std::iter; @@ -296,10 +296,7 @@ pub struct ApplicationTy { impl ApplicationTy { pub fn type_parameters<'a>(&'a self) -> impl Iterator + 'a { - self.parameters - .iter() - .cloned() - .filter_map(|p| p.ty()) + self.parameters.iter().cloned().filter_map(|p| p.ty()) } pub fn first_type_parameter(&self) -> Option { @@ -404,10 +401,7 @@ pub struct TraitRef { impl TraitRef { pub fn type_parameters<'a>(&'a self) -> impl Iterator + 'a { - self.parameters - .iter() - .cloned() - .filter_map(|p| p.ty()) + self.parameters.iter().cloned().filter_map(|p| p.ty()) } } @@ -858,7 +852,8 @@ impl Goal { Binders { value: Box::new(self), binders: Vec::new(), - }.with_fresh_type_var(|goal, ty| { + } + .with_fresh_type_var(|goal, ty| { Box::new(Goal::Implies( vec![ DomainGoal::Compatible(()).cast(), diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs index 84cdcbd192b..5e4784fb73b 100644 --- a/chalk-ir/src/macros.rs +++ b/chalk-ir/src/macros.rs @@ -76,11 +76,13 @@ macro_rules! lifetime { #[macro_export] macro_rules! ty_name { - ((item $n:expr)) => { $crate::TypeName::ItemId(ItemId { index: $n }) }; - ((placeholder $n:expr)) => { $crate::TypeName::Placeholder( - PlaceholderIndex { - ui: UniverseIndex { counter: $n }, - idx: 0, - }) - } + ((item $n:expr)) => { + $crate::TypeName::ItemId(ItemId { index: $n }) + }; + ((placeholder $n:expr)) => { + $crate::TypeName::Placeholder(PlaceholderIndex { + ui: UniverseIndex { counter: $n }, + idx: 0, + }) + }; } diff --git a/chalk-macros/src/lib.rs b/chalk-macros/src/lib.rs index 31e5e319265..81be02f5a77 100644 --- a/chalk-macros/src/lib.rs +++ b/chalk-macros/src/lib.rs @@ -17,7 +17,6 @@ lazy_static! { .map(|x| x >= 2) .unwrap_or(false) }; - pub static ref INFO_ENABLED: bool = { use std::env; env::var("CHALK_DEBUG") diff --git a/chalk-parse/src/errors.rs b/chalk-parse/src/errors.rs index 0c6d43c7948..4420a5c5170 100644 --- a/chalk-parse/src/errors.rs +++ b/chalk-parse/src/errors.rs @@ -1 +1 @@ -error_chain!{} +error_chain! {} diff --git a/chalk-parse/src/lib.rs b/chalk-parse/src/lib.rs index 288c9aa017a..93b8e2f3e8b 100644 --- a/chalk-parse/src/lib.rs +++ b/chalk-parse/src/lib.rs @@ -3,7 +3,7 @@ #[macro_use] extern crate error_chain; -#[macro_use] +#[macro_use] extern crate lalrpop_util; extern crate lalrpop_intern; diff --git a/chalk-solve/src/ext.rs b/chalk-solve/src/ext.rs index 9f1502f6316..a9677ed38fe 100644 --- a/chalk-solve/src/ext.rs +++ b/chalk-solve/src/ext.rs @@ -1,6 +1,6 @@ -use chalk_ir::*; -use chalk_ir::fold::Fold; use crate::infer::InferenceTable; +use chalk_ir::fold::Fold; +use chalk_ir::*; pub trait CanonicalExt { fn map(self, op: OP) -> Canonical diff --git a/chalk-solve/src/infer.rs b/chalk-solve/src/infer.rs index 8f0b75c311a..29a6bc3b43b 100644 --- a/chalk-solve/src/infer.rs +++ b/chalk-solve/src/infer.rs @@ -1,15 +1,15 @@ use ::ena::unify as ena; -use chalk_ir::*; use chalk_ir::fold::Fold; +use chalk_ir::*; pub mod canonicalize; -pub mod ucanonicalize; -mod normalize_deep; pub mod instantiate; mod invert; +mod normalize_deep; +mod test; +pub mod ucanonicalize; pub mod unify; pub mod var; -mod test; use self::var::*; diff --git a/chalk-solve/src/infer/canonicalize.rs b/chalk-solve/src/infer/canonicalize.rs index 1c2f61e845a..a683d3f944a 100644 --- a/chalk-solve/src/infer/canonicalize.rs +++ b/chalk-solve/src/infer/canonicalize.rs @@ -1,7 +1,7 @@ use chalk_engine::fallible::*; use chalk_ir::fold::shift::Shift; use chalk_ir::fold::{ - DefaultTypeFolder, Fold, DefaultFreeVarFolder, InferenceFolder, PlaceholderFolder, + DefaultFreeVarFolder, DefaultTypeFolder, Fold, InferenceFolder, PlaceholderFolder, }; use chalk_ir::*; use std::cmp::max; @@ -82,11 +82,14 @@ impl<'q> Canonicalizer<'q> { } fn add(&mut self, free_var: ParameterEnaVariable) -> usize { - self.free_vars.iter().position(|&v| v == free_var).unwrap_or_else(|| { - let next_index = self.free_vars.len(); - self.free_vars.push(free_var); - next_index - }) + self.free_vars + .iter() + .position(|&v| v == free_var) + .unwrap_or_else(|| { + let next_index = self.free_vars.len(); + self.free_vars.push(free_var); + next_index + }) } } @@ -120,11 +123,7 @@ impl<'q> DefaultFreeVarFolder for Canonicalizer<'q> { impl<'q> InferenceFolder for Canonicalizer<'q> { fn fold_inference_ty(&mut self, var: InferenceVar, binders: usize) -> Fallible { - debug_heading!( - "fold_inference_ty(depth={:?}, binders={:?})", - var, - binders - ); + debug_heading!("fold_inference_ty(depth={:?}, binders={:?})", var, binders); let var = EnaVariable::from(var); match self.table.probe_ty_var(var) { Some(ty) => { diff --git a/chalk-solve/src/infer/instantiate.rs b/chalk-solve/src/infer/instantiate.rs index 6f182d614d5..1f65f867924 100644 --- a/chalk-solve/src/infer/instantiate.rs +++ b/chalk-solve/src/infer/instantiate.rs @@ -45,7 +45,10 @@ impl InferenceTable { T: Fold, U: IntoIterator>, { - let binders: Vec<_> = binders.into_iter().map(|pk| pk.map(|()| universe)).collect(); + let binders: Vec<_> = binders + .into_iter() + .map(|pk| pk.map(|()| universe)) + .collect(); let subst = self.fresh_subst(&binders); arg.fold_with(&mut &subst, 0).unwrap() } diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs index cb5c43136ec..d342b6888dc 100644 --- a/chalk-solve/src/infer/test.rs +++ b/chalk-solve/src/infer/test.rs @@ -1,7 +1,7 @@ #![cfg(test)] -use super::*; use super::unify::UnificationResult; +use super::*; #[test] fn infer() { @@ -16,7 +16,10 @@ fn infer() { table .unify(&environment0, &b, &ty!(apply (item 1))) .unwrap(); - assert_eq!(table.normalize_deep(&a), ty!(apply (item 0) (apply (item 1)))); + assert_eq!( + table.normalize_deep(&a), + ty!(apply (item 0) (apply (item 1))) + ); } #[test] diff --git a/chalk-solve/src/infer/ucanonicalize.rs b/chalk-solve/src/infer/ucanonicalize.rs index f599f7bfb95..a28efbb38ab 100644 --- a/chalk-solve/src/infer/ucanonicalize.rs +++ b/chalk-solve/src/infer/ucanonicalize.rs @@ -19,7 +19,8 @@ impl InferenceTable { universes: &mut universes, }, 0, - ).unwrap(); + ) + .unwrap(); // Now re-map the universes found in value. We have to do this // in a second pass because it is only then that we know the @@ -31,7 +32,8 @@ impl InferenceTable { universes: &universes, }, 0, - ).unwrap(); + ) + .unwrap(); let binders = value0 .binders .iter() @@ -273,7 +275,8 @@ impl<'q> PlaceholderFolder for UMapToCanonical<'q> { Ok(PlaceholderIndex { ui, idx: universe0.idx, - }.to_ty()) + } + .to_ty()) } fn fold_free_placeholder_lifetime( @@ -285,7 +288,8 @@ impl<'q> PlaceholderFolder for UMapToCanonical<'q> { Ok(PlaceholderIndex { ui: universe, idx: universe0.idx, - }.to_lifetime()) + } + .to_lifetime()) } } @@ -307,7 +311,8 @@ impl<'q> PlaceholderFolder for UMapFromCanonical<'q> { Ok(PlaceholderIndex { ui, idx: universe0.idx, - }.to_ty()) + } + .to_ty()) } fn fold_free_placeholder_lifetime( @@ -319,7 +324,8 @@ impl<'q> PlaceholderFolder for UMapFromCanonical<'q> { Ok(PlaceholderIndex { ui: universe, idx: universe0.idx, - }.to_lifetime()) + } + .to_lifetime()) } } @@ -330,4 +336,3 @@ impl<'q> DefaultInferenceFolder for UMapFromCanonical<'q> { true } } - diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 8eecedc8d7a..1a4c6806a1b 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -119,9 +119,7 @@ impl<'t> Unifier<'t> { (&Ty::InferenceVar(var), ty @ &Ty::Apply(_)) | (ty @ &Ty::Apply(_), &Ty::InferenceVar(var)) | (&Ty::InferenceVar(var), ty @ &Ty::ForAll(_)) - | (ty @ &Ty::ForAll(_), &Ty::InferenceVar(var)) => { - self.unify_var_ty(var, ty) - } + | (ty @ &Ty::ForAll(_), &Ty::InferenceVar(var)) => self.unify_var_ty(var, ty), (&Ty::ForAll(ref quantified_ty1), &Ty::ForAll(ref quantified_ty2)) => { self.unify_forall_tys(quantified_ty1, quantified_ty2) @@ -164,9 +162,10 @@ impl<'t> Unifier<'t> { self.unify_unselected_projection_ty(proj, ty) } - (Ty::BoundVar(_), _) | (_, Ty::BoundVar(_)) => { - panic!("unification encountered bound variable: a={:?} b={:?}", a, b) - } + (Ty::BoundVar(_), _) | (_, Ty::BoundVar(_)) => panic!( + "unification encountered bound variable: a={:?} b={:?}", + a, b + ), } } @@ -226,7 +225,8 @@ impl<'t> Unifier<'t> { ProjectionEq { projection: proj.clone(), ty: ty.clone(), - }.cast(), + } + .cast(), ))) } @@ -240,7 +240,8 @@ impl<'t> Unifier<'t> { UnselectedNormalize { projection: proj.clone(), ty: ty.clone(), - }.cast(), + } + .cast(), ))) } @@ -324,15 +325,18 @@ impl<'t> Unifier<'t> { } } - (&Lifetime::Placeholder(_), &Lifetime::Placeholder(_)) => if a != b { - Ok(self.push_lifetime_eq_constraint(*a, *b)) - } else { - Ok(()) - }, - - (Lifetime::BoundVar(_), _) | (_, Lifetime::BoundVar(_)) => { - panic!("unification encountered bound variable: a={:?} b={:?}", a, b) + (&Lifetime::Placeholder(_), &Lifetime::Placeholder(_)) => { + if a != b { + Ok(self.push_lifetime_eq_constraint(*a, *b)) + } else { + Ok(()) + } } + + (Lifetime::BoundVar(_), _) | (_, Lifetime::BoundVar(_)) => panic!( + "unification encountered bound variable: a={:?} b={:?}", + a, b + ), } } diff --git a/chalk-solve/src/infer/var.rs b/chalk-solve/src/infer/var.rs index 676b4f99dcf..6c3de6ce047 100644 --- a/chalk-solve/src/infer/var.rs +++ b/chalk-solve/src/infer/var.rs @@ -1,5 +1,5 @@ -use ena::unify::{UnifyKey, UnifyValue}; use chalk_ir::*; +use ena::unify::{UnifyKey, UnifyValue}; use std::cmp::min; use std::fmt; use std::u32; @@ -105,8 +105,8 @@ impl UnifyValue for InferenceValue { (&InferenceValue::Unbound(ui_a), &InferenceValue::Unbound(ui_b)) => { Ok(InferenceValue::Unbound(min(ui_a, ui_b))) } - (bound @ &InferenceValue::Bound(_), &InferenceValue::Unbound(_)) | - (&InferenceValue::Unbound(_), bound @ &InferenceValue::Bound(_)) => Ok(bound.clone()), + (bound @ &InferenceValue::Bound(_), &InferenceValue::Unbound(_)) + | (&InferenceValue::Unbound(_), bound @ &InferenceValue::Bound(_)) => Ok(bound.clone()), (&InferenceValue::Bound(_), &InferenceValue::Bound(_)) => { panic!("we should not be asked to unify two bound things") } diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index 743fd82ea95..ced521d3445 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -6,6 +6,6 @@ extern crate chalk_engine; extern crate chalk_ir; extern crate ena; +pub mod ext; pub mod infer; pub mod solve; -pub mod ext; diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 3beb84a44d9..84732d57275 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -1,8 +1,8 @@ +use crate::solve::slg::implementation::SlgContext; use chalk_engine::context::Context; use chalk_engine::context::ContextOps; use chalk_engine::fallible::*; use chalk_engine::forest::Forest; -use crate::solve::slg::implementation::SlgContext; use chalk_ir::*; use std::fmt; use std::sync::Arc; diff --git a/chalk-solve/src/solve/slg/implementation.rs b/chalk-solve/src/solve/slg/implementation.rs index d222de688c1..81a19465890 100644 --- a/chalk-solve/src/solve/slg/implementation.rs +++ b/chalk-solve/src/solve/slg/implementation.rs @@ -1,12 +1,12 @@ -use chalk_engine::fallible::Fallible; -use chalk_ir::cast::{Cast, Caster}; -use chalk_ir::could_match::CouldMatch; -use chalk_ir::*; use crate::infer::ucanonicalize::{UCanonicalized, UniverseMap}; use crate::infer::unify::UnificationResult; use crate::infer::InferenceTable; use crate::solve::truncate::{self, Truncated}; use crate::solve::Solution; +use chalk_engine::fallible::Fallible; +use chalk_ir::cast::{Cast, Caster}; +use chalk_ir::could_match::CouldMatch; +use chalk_ir::*; use chalk_engine::context; use chalk_engine::hh::HhGoal; diff --git a/chalk-solve/src/solve/slg/implementation/aggregate.rs b/chalk-solve/src/solve/slg/implementation/aggregate.rs index 58189f20ee7..0c20d735522 100644 --- a/chalk-solve/src/solve/slg/implementation/aggregate.rs +++ b/chalk-solve/src/solve/slg/implementation/aggregate.rs @@ -1,9 +1,9 @@ -use chalk_ir::cast::Cast; -use chalk_ir::*; use crate::ext::*; use crate::infer::InferenceTable; use crate::solve::slg::implementation::SubstitutionExt; use crate::solve::{Guidance, Solution}; +use chalk_ir::cast::Cast; +use chalk_ir::*; use chalk_engine::context; use chalk_engine::SimplifiedAnswer; @@ -123,7 +123,8 @@ fn merge_into_guidance( universe, }; aggr.aggregate_tys(&ty, ty1).cast() - }).collect(); + }) + .collect(); let aggr_subst = Substitution { parameters: aggr_parameters, @@ -236,7 +237,8 @@ impl<'infer> AntiUnifier<'infer> { associated_ty_id, parameters, }) - }).unwrap_or_else(|| self.new_variable()) + }) + .unwrap_or_else(|| self.new_variable()) } fn aggregate_unselected_projection_tys( @@ -259,7 +261,8 @@ impl<'infer> AntiUnifier<'infer> { type_name, parameters, }) - }).unwrap_or_else(|| self.new_variable()) + }) + .unwrap_or_else(|| self.new_variable()) } fn aggregate_name_and_substs( @@ -316,15 +319,15 @@ impl<'infer> AntiUnifier<'infer> { self.new_lifetime_variable() } - (Lifetime::BoundVar(_), _) | (_, Lifetime::BoundVar(_)) => { - self.new_lifetime_variable() - } + (Lifetime::BoundVar(_), _) | (_, Lifetime::BoundVar(_)) => self.new_lifetime_variable(), - (Lifetime::Placeholder(_), Lifetime::Placeholder(_)) => if l1 == l2 { - *l1 - } else { - self.new_lifetime_variable() - }, + (Lifetime::Placeholder(_), Lifetime::Placeholder(_)) => { + if l1 == l2 { + *l1 + } else { + self.new_lifetime_variable() + } + } } } diff --git a/chalk-solve/src/solve/slg/implementation/resolvent.rs b/chalk-solve/src/solve/slg/implementation/resolvent.rs index 9390f980493..319d0f5c7bc 100644 --- a/chalk-solve/src/solve/slg/implementation/resolvent.rs +++ b/chalk-solve/src/solve/slg/implementation/resolvent.rs @@ -1,10 +1,10 @@ +use crate::infer::InferenceTable; +use crate::solve::slg::implementation::{self, SlgContext, TruncatingInferenceTable}; use chalk_engine::fallible::Fallible; use chalk_ir::fold::shift::Shift; use chalk_ir::fold::Fold; use chalk_ir::zip::{Zip, Zipper}; use chalk_ir::*; -use crate::infer::InferenceTable; -use crate::solve::slg::implementation::{self, SlgContext, TruncatingInferenceTable}; use chalk_engine::context; use chalk_engine::{ExClause, Literal}; diff --git a/chalk-solve/src/solve/truncate.rs b/chalk-solve/src/solve/truncate.rs index 5bfcec2cc13..0d583ff9549 100644 --- a/chalk-solve/src/solve/truncate.rs +++ b/chalk-solve/src/solve/truncate.rs @@ -1,12 +1,12 @@ //! +use crate::infer::InferenceTable; use chalk_engine::fallible::*; use chalk_ir::fold::shift::Shift; use chalk_ir::fold::{ self, DefaultFreeVarFolder, DefaultInferenceFolder, DefaultPlaceholderFolder, Fold, TypeFolder, }; use chalk_ir::*; -use crate::infer::InferenceTable; crate fn truncate(infer: &mut InferenceTable, max_size: usize, value: &T) -> Truncated where diff --git a/src/bin/chalki.rs b/src/bin/chalki.rs index 066ac3357a5..289b150cf07 100644 --- a/src/bin/chalki.rs +++ b/src/bin/chalki.rs @@ -1,8 +1,8 @@ extern crate chalk; extern crate chalk_engine; extern crate chalk_ir; -extern crate chalk_solve; extern crate chalk_parse; +extern crate chalk_solve; extern crate docopt; extern crate rustyline; @@ -12,16 +12,16 @@ extern crate serde_derive; #[macro_use] extern crate error_chain; -use std::io::Read; use std::fs::File; -use std::sync::Arc; +use std::io::Read; use std::process::exit; +use std::sync::Arc; use chalk::rust_ir; use chalk::rust_ir::lowering::*; +use chalk_engine::fallible::NoSolution; use chalk_solve::ext::*; use chalk_solve::solve::SolverChoice; -use chalk_engine::fallible::NoSolution; use docopt::Docopt; use rustyline::error::ReadlineError; @@ -196,7 +196,8 @@ fn process( // The command is either "print", "lowered", or a goal. // Check that a program has been loaded. - let prog = prog.as_ref() + let prog = prog + .as_ref() .ok_or("no program currently loaded; type 'help' to see available commands")?; // Attempt to parse the program. @@ -260,7 +261,8 @@ fn read_program(rl: &mut rustyline::Editor<()>) -> Result { fn goal(args: &Args, text: &str, prog: &Program) -> Result<()> { let goal = chalk_parse::parse_goal(text)?.lower(&*prog.ir)?; let peeled_goal = goal.into_peeled_goal(); - match args.solver_choice() + match args + .solver_choice() .solve_root_goal(&prog.env, &peeled_goal) { Ok(Some(v)) => println!("{}\n", v), diff --git a/src/coherence.rs b/src/coherence.rs index ead90506f0e..0264409a576 100644 --- a/src/coherence.rs +++ b/src/coherence.rs @@ -1,17 +1,20 @@ use petgraph::prelude::*; use crate::errors::Result; -use chalk_ir::{self, ItemId}; use crate::rust_ir::Program; +use chalk_ir::{self, ItemId}; use chalk_solve::solve::SolverChoice; use std::sync::Arc; -mod solve; mod orphan; +mod solve; mod test; impl Program { - crate fn record_specialization_priorities(&mut self, solver_choice: SolverChoice) -> Result<()> { + crate fn record_specialization_priorities( + &mut self, + solver_choice: SolverChoice, + ) -> Result<()> { chalk_ir::tls::set_current_program(&Arc::new(self.clone()), || { let forest = self.build_specialization_forest(solver_choice)?; @@ -51,7 +54,8 @@ impl Program { let impl_id = forest .node_weight(idx) .expect("index should be a valid index into graph"); - let impl_datum = self.impl_data + let impl_datum = self + .impl_data .get_mut(impl_id) .expect("node should be valid impl id"); impl_datum.binders.value.specialization_priority = p; diff --git a/src/coherence/orphan.rs b/src/coherence/orphan.rs index 6d2d343ffb1..de4cff5c381 100644 --- a/src/coherence/orphan.rs +++ b/src/coherence/orphan.rs @@ -1,9 +1,9 @@ use std::sync::Arc; use crate::errors::*; -use chalk_ir::*; use crate::rust_ir::*; use chalk_ir::cast::*; +use chalk_ir::*; use chalk_solve::ext::*; use chalk_solve::solve::SolverChoice; @@ -19,7 +19,8 @@ impl Program { solver_choice, }; - let local_impls = self.impl_data + let local_impls = self + .impl_data .values() // Only keep local impls (i.e. impls in the current crate) .filter(|impl_datum| impl_datum.binders.value.impl_type == ImplType::Local); @@ -47,13 +48,17 @@ impl OrphanSolver { fn orphan_check(&self, impl_datum: &ImplDatum) -> bool { debug_heading!("orphan_check(impl={:#?})", impl_datum); - let impl_allowed: Goal = impl_datum.binders.map_ref(|bound_impl| { - // Ignoring the polarization of the impl's polarized trait ref - DomainGoal::LocalImplAllowed(bound_impl.trait_ref.trait_ref().clone()) - }).cast(); + let impl_allowed: Goal = impl_datum + .binders + .map_ref(|bound_impl| { + // Ignoring the polarization of the impl's polarized trait ref + DomainGoal::LocalImplAllowed(bound_impl.trait_ref.trait_ref().clone()) + }) + .cast(); let canonical_goal = &impl_allowed.into_closed_goal(); - let result = self.solver_choice + let result = self + .solver_choice .solve_root_goal(&self.env, canonical_goal) .unwrap() .is_some(); diff --git a/src/coherence/solve.rs b/src/coherence/solve.rs index 98924dc1ad0..8bdb5e51f1a 100644 --- a/src/coherence/solve.rs +++ b/src/coherence/solve.rs @@ -1,13 +1,13 @@ use std::sync::Arc; -use chalk_ir::fold::shift::Shift; -use itertools::Itertools; use crate::errors::*; -use chalk_ir::*; use crate::rust_ir::*; use chalk_ir::cast::*; +use chalk_ir::fold::shift::Shift; +use chalk_ir::*; use chalk_solve::ext::*; -use chalk_solve::solve::{SolverChoice, Solution}; +use chalk_solve::solve::{Solution, SolverChoice}; +use itertools::Itertools; struct DisjointSolver { env: Arc, @@ -29,7 +29,8 @@ impl Program { }; // Create a vector of references to impl datums, sorted by trait ref. - let impl_data = self.impl_data + let impl_data = self + .impl_data .iter() .filter(|&(_, impl_datum)| { // Ignore impls for marker traits as they are allowed to overlap. @@ -47,10 +48,9 @@ impl Program { }); // Group impls by trait. - let impl_groupings = impl_data.into_iter().group_by(|&(_, impl_datum)| { - impl_datum.binders.value.trait_ref.trait_ref().trait_id - }); - + let impl_groupings = impl_data + .into_iter() + .group_by(|&(_, impl_datum)| impl_datum.binders.value.trait_ref.trait_ref().trait_id); // Iterate over every pair of impls for the same trait. for (trait_id, impls) in &impl_groupings { @@ -139,7 +139,8 @@ impl DisjointSolver { // Upshift the rhs variables in where clauses let lhs_where_clauses = lhs.binders.value.where_clauses.iter().cloned(); - let rhs_where_clauses = rhs.binders + let rhs_where_clauses = rhs + .binders .value .where_clauses .iter() @@ -161,7 +162,8 @@ impl DisjointSolver { .negate(); let canonical_goal = &goal.into_closed_goal(); - let solution = self.solver_choice + let solution = self + .solver_choice .solve_root_goal(&self.env, canonical_goal) .unwrap(); // internal errors in the solver are fatal let result = match solution { @@ -242,7 +244,8 @@ impl DisjointSolver { .quantify(QuantifierKind::ForAll, more_special.binders.binders.clone()); let canonical_goal = &goal.into_closed_goal(); - let result = match self.solver_choice + let result = match self + .solver_choice .solve_root_goal(&self.env, canonical_goal) .unwrap() { diff --git a/src/coherence/test.rs b/src/coherence/test.rs index 313f2c82724..e761a6b929e 100644 --- a/src/coherence/test.rs +++ b/src/coherence/test.rs @@ -287,7 +287,6 @@ fn fundamental_traits() { impl Bar for T where T: Sized { } } } - } #[test] diff --git a/src/errors.rs b/src/errors.rs index 16aa1bdb458..a3acca284df 100644 --- a/src/errors.rs +++ b/src/errors.rs @@ -1,6 +1,6 @@ -use chalk_parse::{self, ast}; -use chalk_ir; use crate::rust_ir; +use chalk_ir; +use chalk_parse::{self, ast}; error_chain! { links { diff --git a/src/lib.rs b/src/lib.rs index a57b68c422a..24327093942 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -26,8 +26,7 @@ mod test_util; pub mod rust_ir; crate mod coherence; -crate mod rules; pub mod errors; +crate mod rules; mod test; - diff --git a/src/rules.rs b/src/rules.rs index fedb0bb5093..db03dbbc3bf 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -1,8 +1,8 @@ +use crate::rust_ir::*; use chalk_ir::cast::{Cast, Caster}; use chalk_ir::fold::shift::Shift; use chalk_ir::fold::Subst; use chalk_ir::*; -use crate::rust_ir::*; use std::iter; mod default; @@ -14,21 +14,27 @@ impl Program { // of the data above that always has the form: // // forall P0...Pn. Something :- Conditions - let mut program_clauses = self.custom_clauses.iter().cloned().chain( - self.struct_data - .values() - .flat_map(|d| d.to_program_clauses()) - ).chain( - self.trait_data - .values() - .flat_map(|d| d.to_program_clauses()), - ).chain( - self.associated_ty_data - .values() - .flat_map(|d| d.to_program_clauses(self)), - ).chain( - self.default_impl_data.iter().map(|d| d.to_program_clause()) - ).collect::>(); + let mut program_clauses = self + .custom_clauses + .iter() + .cloned() + .chain( + self.struct_data + .values() + .flat_map(|d| d.to_program_clauses()), + ) + .chain( + self.trait_data + .values() + .flat_map(|d| d.to_program_clauses()), + ) + .chain( + self.associated_ty_data + .values() + .flat_map(|d| d.to_program_clauses(self)), + ) + .chain(self.default_impl_data.iter().map(|d| d.to_program_clause())) + .collect::>(); // Adds clause that defines the Derefs domain goal: // forall { Derefs(T, U) :- ProjectionEq(::Target = U>) } @@ -50,17 +56,17 @@ impl Program { source: t(), target: u(), }), - conditions: vec![ - ProjectionEq { - projection: ProjectionTy { - associated_ty_id, - parameters: vec![t().cast()], - }, - ty: u(), - }.cast(), - ], + conditions: vec![ProjectionEq { + projection: ProjectionTy { + associated_ty_id, + parameters: vec![t().cast()], + }, + ty: u(), + } + .cast()], }, - }.cast(), + } + .cast(), ); } @@ -89,7 +95,8 @@ impl Program { } else { None } - }).collect(); + }) + .collect(); ProgramEnvironment { coinductive_traits, @@ -112,7 +119,8 @@ impl ImplDatum { .map_ref(|bound| ProgramClauseImplication { consequence: bound.trait_ref.trait_ref().clone().cast(), conditions: bound.where_clauses.iter().cloned().casted().collect(), - }).cast() + }) + .cast() } } @@ -152,7 +160,8 @@ impl DefaultImplDatum { wc.casted().collect() }, - }).cast() + }) + .cast() } } @@ -270,7 +279,8 @@ impl AssociatedTyValue { consequence: normalize_goal.clone(), conditions: conditions, }, - }.cast(); + } + .cast(); let unselected_projection = UnselectedProjectionTy { type_name: associated_ty.name.clone(), @@ -289,7 +299,8 @@ impl AssociatedTyValue { DomainGoal::InScope(impl_trait_ref.trait_id).cast(), ], }, - }.cast(); + } + .cast(); vec![normalization, unselected_normalization] } @@ -351,7 +362,8 @@ impl StructDatum { consequence: WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(), conditions: { bound_datum.where_clauses.iter().cloned().casted().collect() }, - }).cast(); + }) + .cast(); let is_fully_visible = self .binders @@ -362,7 +374,8 @@ impl StructDatum { .type_parameters() .map(|ty| DomainGoal::IsFullyVisible(ty).cast()) .collect(), - }).cast(); + }) + .cast(); let mut clauses = vec![wf, is_fully_visible]; @@ -400,7 +413,8 @@ impl StructDatum { .map_ref(|bound_datum| ProgramClauseImplication { consequence: DomainGoal::IsLocal(bound_datum.self_ty.clone().cast()), conditions: Vec::new(), - }).cast(); + }) + .cast(); clauses.push(is_local); } else if self.binders.value.flags.fundamental { @@ -416,7 +430,8 @@ impl StructDatum { .map_ref(|bound_datum| ProgramClauseImplication { consequence: DomainGoal::IsUpstream(bound_datum.self_ty.clone().cast()), conditions: Vec::new(), - }).cast(); + }) + .cast(); clauses.push(is_upstream); } @@ -455,7 +470,8 @@ impl StructDatum { consequence: wc.value, conditions: vec![condition.clone().shifted_in(shift).cast()], }, - }.cast(), + } + .cast(), ); } @@ -597,7 +613,8 @@ impl TraitDatum { .chain(Some(DomainGoal::Holds(trait_ref_impl.clone()).cast())) .collect() }, - }).cast(); + }) + .cast(); let mut clauses = vec![wf]; @@ -622,11 +639,14 @@ impl TraitDatum { .chain(iter::once(DomainGoal::Compatible(()).cast())) .chain((0..i).map(|j| { DomainGoal::IsFullyVisible(type_parameters[j].clone()).cast() - })).chain(iter::once( + })) + .chain(iter::once( DomainGoal::DownstreamType(type_parameters[i].clone()).cast(), - )).chain(iter::once(Goal::CannotProve(()))) + )) + .chain(iter::once(Goal::CannotProve(()))) .collect(), - }).cast(); + }) + .cast(); impl_may_exist })); @@ -637,7 +657,8 @@ impl TraitDatum { .map_ref(|bound_datum| ProgramClauseImplication { consequence: DomainGoal::LocalImplAllowed(bound_datum.trait_ref.clone()), conditions: Vec::new(), - }).cast(); + }) + .cast(); clauses.push(impl_allowed); } else { @@ -650,8 +671,10 @@ impl TraitDatum { .map(|j| DomainGoal::IsFullyVisible(type_parameters[j].clone()).cast()) .chain(iter::once( DomainGoal::IsLocal(type_parameters[i].clone()).cast(), - )).collect(), - }).cast(); + )) + .collect(), + }) + .cast(); impl_maybe_allowed })); @@ -676,9 +699,11 @@ impl TraitDatum { .trait_ref .type_parameters() .map(|ty| DomainGoal::IsUpstream(ty).cast()), - ).chain(iter::once(Goal::CannotProve(()))) + ) + .chain(iter::once(Goal::CannotProve(()))) .collect(), - }).cast(); + }) + .cast(); clauses.push(impl_may_exist); } @@ -708,8 +733,9 @@ impl TraitDatum { consequence: wc.value, conditions: vec![condition.clone().shifted_in(shift).cast()], }, - }.cast() - }) + } + .cast() + }), ); clauses.push( @@ -717,7 +743,8 @@ impl TraitDatum { .map_ref(|_| ProgramClauseImplication { consequence: DomainGoal::Holds(trait_ref_impl), conditions: vec![condition.cast()], - }).cast(), + }) + .cast(), ); clauses @@ -842,7 +869,8 @@ impl AssociatedTyDatum { consequence: projection_eq.clone().cast(), conditions: vec![], }, - }.cast(), + } + .cast(), ); // Well-formedness of projection type. @@ -859,7 +887,8 @@ impl AssociatedTyDatum { .chain(self.where_clauses.iter().cloned().casted()) .collect(), }, - }.cast(), + } + .cast(), ); // Assuming well-formedness of projection type means we can assume @@ -875,7 +904,8 @@ impl AssociatedTyDatum { consequence: FromEnv::Trait(trait_ref.clone()).cast(), conditions: vec![FromEnv::Ty(app_ty.clone()).cast()], }, - }.cast(), + } + .cast(), ); // Reverse rule for where clauses. @@ -894,7 +924,8 @@ impl AssociatedTyDatum { consequence: wc.value.clone().into_from_env_goal(), conditions: vec![FromEnv::Ty(app_ty.clone()).shifted_in(shift).cast()], }, - }.cast() + } + .cast() })); // Reverse rule for implied bounds. @@ -905,14 +936,10 @@ impl AssociatedTyDatum { clauses.extend(self.bounds_on_self().into_iter().map(|bound| { // Same as above in case of higher-ranked inline bounds. let shift = bound.binders.len(); - let from_env_trait = iter::once( - FromEnv::Trait(trait_ref.clone()).shifted_in(shift).cast() - ); + let from_env_trait = + iter::once(FromEnv::Trait(trait_ref.clone()).shifted_in(shift).cast()); - let where_clauses = self.where_clauses - .iter() - .cloned() - .casted(); + let where_clauses = self.where_clauses.iter().cloned().casted(); Binders { binders: bound @@ -925,7 +952,8 @@ impl AssociatedTyDatum { consequence: bound.value.clone().into_from_env_goal(), conditions: from_env_trait.chain(where_clauses).collect(), }, - }.cast() + } + .cast() })); // add new type parameter U @@ -958,7 +986,8 @@ impl AssociatedTyDatum { consequence: projection_eq.clone().cast(), conditions: vec![normalize.clone().cast()], }, - }.cast(), + } + .cast(), ); clauses diff --git a/src/rules/default.rs b/src/rules/default.rs index 2b78c5d9a41..118e109a8b5 100644 --- a/src/rules/default.rs +++ b/src/rules/default.rs @@ -1,12 +1,13 @@ -use chalk_ir::*; use crate::rust_ir::*; -use chalk_solve::infer::InferenceTable; use chalk_ir::cast::Cast; +use chalk_ir::*; +use chalk_solve::infer::InferenceTable; impl Program { pub fn add_default_impls(&mut self) { // For each auto trait `MyAutoTrait` and for each struct/type `MyStruct` - for auto_trait in self.trait_data + for auto_trait in self + .trait_data .values() .filter(|t| t.binders.value.flags.auto) { @@ -14,9 +15,9 @@ impl Program { // `MyStruct: MyAutoTrait` let trait_ref = TraitRef { trait_id: auto_trait.binders.value.trait_ref.trait_id, - parameters: vec![ - ParameterKind::Ty(Ty::Apply(struct_datum.binders.value.self_ty.clone())), - ], + parameters: vec![ParameterKind::Ty(Ty::Apply( + struct_datum.binders.value.self_ty.clone(), + ))], }; // If a positive or negative impl is already provided for a type family diff --git a/src/rules/wf.rs b/src/rules/wf.rs index 5c073099433..7861ab50469 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -1,14 +1,14 @@ use std::sync::Arc; -use chalk_ir::*; use crate::errors::*; +use crate::rust_ir::*; use chalk_ir::cast::*; -use chalk_ir::fold::*; use chalk_ir::fold::shift::Shift; -use itertools::Itertools; -use crate::rust_ir::*; +use chalk_ir::fold::*; +use chalk_ir::*; use chalk_solve::ext::*; use chalk_solve::solve::SolverChoice; +use itertools::Itertools; mod test; @@ -20,7 +20,9 @@ struct WfSolver<'me> { impl Program { pub fn verify_well_formedness(&self, solver_choice: SolverChoice) -> Result<()> { - tls::set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice)) + tls::set_current_program(&Arc::new(self.clone()), || { + self.solve_wf_requirements(solver_choice) + }) } fn solve_wf_requirements(&self, solver_choice: SolverChoice) -> Result<()> { @@ -96,10 +98,9 @@ impl FoldInputTypes for Ty { // lazily, so no need to include them here. Ty::ForAll(..) => (), - Ty::InferenceVar(..) => panic!( - "unexpected inference variable in wf rules: {:?}", - self, - ), + Ty::InferenceVar(..) => { + panic!("unexpected inference variable in wf rules: {:?}", self,) + } } } } @@ -137,34 +138,44 @@ impl<'me> WfSolver<'me> { // We retrieve all the input types of the struct fields. let mut input_types = Vec::new(); struct_datum.binders.value.fields.fold(&mut input_types); - struct_datum.binders.value.where_clauses.fold(&mut input_types); + struct_datum + .binders + .value + .where_clauses + .fold(&mut input_types); if input_types.is_empty() { return true; } - let goals = input_types.into_iter() - .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))) - .casted(); - let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) - .expect("at least one goal"); - - let hypotheses = - struct_datum.binders - .value - .where_clauses - .iter() - .cloned() - .map(|wc| wc.map(|bound| bound.into_from_env_goal())) - .casted() - .collect(); + let goals = input_types + .into_iter() + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))) + .casted(); + let goal = goals + .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + + let hypotheses = struct_datum + .binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.map(|bound| bound.into_from_env_goal())) + .casted() + .collect(); // We ask that the above input types are well-formed provided that all the where-clauses // on the struct definition hold. let goal = Goal::Implies(hypotheses, Box::new(goal)) .quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone()); - match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { + match self + .solver_choice + .solve_root_goal(&self.env, &goal.into_closed_goal()) + .unwrap() + { Some(sol) => sol.is_unique(), None => false, } @@ -173,7 +184,7 @@ impl<'me> WfSolver<'me> { fn verify_trait_impl(&self, impl_datum: &ImplDatum) -> bool { let trait_ref = match impl_datum.binders.value.trait_ref { PolarizedTraitRef::Positive(ref trait_ref) => trait_ref, - _ => return true + _ => return true, }; // We retrieve all the input types of the where clauses appearing on the trait impl, @@ -185,7 +196,11 @@ impl<'me> WfSolver<'me> { // We will have to prove that these types are well-formed (e.g. an additional `K: Hash` // bound would be needed here). let mut input_types = Vec::new(); - impl_datum.binders.value.where_clauses.fold(&mut input_types); + impl_datum + .binders + .value + .where_clauses + .fold(&mut input_types); // We retrieve all the input types of the type on which we implement the trait: we will // *assume* that these types are well-formed, e.g. we will be able to derive that @@ -222,29 +237,31 @@ impl<'me> WfSolver<'me> { let mut input_types = Vec::new(); assoc_ty.value.value.ty.fold(&mut input_types); - let wf_goals = - input_types.into_iter() - .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))) - .casted(); - + let wf_goals = input_types + .into_iter() + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))) + .casted(); + let trait_ref = trait_ref.shifted_in(assoc_ty.value.binders.len()); - let all_parameters: Vec<_> = - assoc_ty.value.binders.iter() - .zip(0..) - .map(|p| p.to_parameter()) - .chain(trait_ref.parameters.iter().cloned()) - .collect(); + let all_parameters: Vec<_> = assoc_ty + .value + .binders + .iter() + .zip(0..) + .map(|p| p.to_parameter()) + .chain(trait_ref.parameters.iter().cloned()) + .collect(); // Add bounds from the trait. Because they are defined on the trait, // their parameters must be substituted with those of the impl. - let bound_goals = - bounds.iter() - .map(|b| Subst::apply(&all_parameters, b)) - .flat_map(|b| b.into_where_clauses(assoc_ty.value.value.ty.clone())) - .map(|wc| wc.map(|bound| bound.into_well_formed_goal())) - .casted(); - + let bound_goals = bounds + .iter() + .map(|b| Subst::apply(&all_parameters, b)) + .flat_map(|b| b.into_where_clauses(assoc_ty.value.value.ty.clone())) + .map(|wc| wc.map(|bound| bound.into_well_formed_goal())) + .casted(); + let goals = wf_goals.chain(bound_goals); let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) { Some(goal) => goal, @@ -253,67 +270,68 @@ impl<'me> WfSolver<'me> { // Add where clauses from the associated ty definition. We must // substitute parameters here, like we did with the bounds above. - let hypotheses = - assoc_ty_datum.where_clauses - .iter() - .map(|wc| Subst::apply(&all_parameters, wc)) - .map(|wc| wc.map(|bound| bound.into_from_env_goal())) - .casted() - .collect(); - - let goal = Goal::Implies( - hypotheses, - Box::new(goal) - ); + let hypotheses = assoc_ty_datum + .where_clauses + .iter() + .map(|wc| Subst::apply(&all_parameters, wc)) + .map(|wc| wc.map(|bound| bound.into_from_env_goal())) + .casted() + .collect(); + + let goal = Goal::Implies(hypotheses, Box::new(goal)); Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone())) }; - let assoc_ty_goals = - impl_datum.binders - .value - .associated_ty_values - .iter() - .filter_map(compute_assoc_ty_goal); + let assoc_ty_goals = impl_datum + .binders + .value + .associated_ty_values + .iter() + .filter_map(compute_assoc_ty_goal); // Things to prove well-formed: input types of the where-clauses, projection types // appearing in the header, associated type values, and of course the trait ref. - let trait_ref_wf = DomainGoal::WellFormed( - WellFormed::Trait(trait_ref.clone()) - ); - let goals = - input_types.into_iter() - .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)).cast()) - .chain(assoc_ty_goals) - .chain(Some(trait_ref_wf).cast()); - - let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) - .expect("at least one goal"); + let trait_ref_wf = DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone())); + let goals = input_types + .into_iter() + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)).cast()) + .chain(assoc_ty_goals) + .chain(Some(trait_ref_wf).cast()); + + let goal = goals + .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); // Assumptions: types appearing in the header which are not projection types are // assumed to be well-formed, and where clauses declared on the impl are assumed // to hold. - let hypotheses = - impl_datum.binders - .value - .where_clauses - .iter() - .cloned() - .map(|wc| wc.map(|bound| bound.into_from_env_goal())) - .casted() - .chain( - header_input_types.into_iter() - .map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty))) - .casted() - ) - .collect(); + let hypotheses = impl_datum + .binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.map(|bound| bound.into_from_env_goal())) + .casted() + .chain( + header_input_types + .into_iter() + .map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty))) + .casted(), + ) + .collect(); let goal = Goal::Implies(hypotheses, Box::new(goal)) .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone()); debug!("WF trait goal: {:?}", goal); - match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { + match self + .solver_choice + .solve_root_goal(&self.env, &goal.into_closed_goal()) + .unwrap() + { Some(sol) => sol.is_unique(), None => false, } diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index 00cc6715016..5923dc6d970 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -623,7 +623,7 @@ fn assoc_type_recursive_bound() { // } // fn bar { - // // ok, we have `FromEnv(T: Bar)` hence + // // ok, we have `FromEnv(T: Bar)` hence // // `::Assoc` is well-formed and // // `Implemented(::Assoc: Print)` hold // foo<::Assoc>( diff --git a/src/rust_ir.rs b/src/rust_ir.rs index 8d8eaae639a..b87af1f1173 100644 --- a/src/rust_ir.rs +++ b/src/rust_ir.rs @@ -2,13 +2,13 @@ //! version of the AST, roughly corresponding to [the HIR] in the Rust //! compiler. +use chalk_ir::debug::Angle; use chalk_ir::fold::shift::Shift; use chalk_ir::tls; use chalk_ir::{ ApplicationTy, Binders, Identifier, ItemId, Lifetime, Parameter, ParameterKind, ProgramClause, ProjectionEq, ProjectionTy, QuantifiedWhereClause, TraitRef, Ty, WhereClause, }; -use chalk_ir::debug::Angle; use std::collections::BTreeMap; use std::fmt; use std::iter; @@ -88,8 +88,7 @@ impl tls::DebugContext for Program { projection_ty: &ProjectionTy, fmt: &mut fmt::Formatter, ) -> Result<(), fmt::Error> { - let (associated_ty_data, trait_params, other_params) = - self.split_projection(projection_ty); + let (associated_ty_data, trait_params, other_params) = self.split_projection(projection_ty); write!( fmt, "<{:?} as {:?}{:?}>::{}{:?}", @@ -222,7 +221,8 @@ impl IntoWhereClauses for QuantifiedInlineBound { .map(|wc| Binders { binders: self.binders.clone(), value: wc, - }).collect() + }) + .collect() } } diff --git a/src/rust_ir/lowering.rs b/src/rust_ir/lowering.rs index b08e75069e3..4cbd249fe7e 100644 --- a/src/rust_ir/lowering.rs +++ b/src/rust_ir/lowering.rs @@ -3,12 +3,12 @@ use std::collections::BTreeMap; use chalk_parse::ast::*; use lalrpop_intern::intern; +use crate::errors::*; +use crate::rust_ir::{self, Anonymize, ToParameter}; use chalk_ir; use chalk_ir::cast::{Cast, Caster}; use chalk_solve::solve::SolverChoice; -use crate::errors::*; use itertools::Itertools; -use crate::rust_ir::{self, Anonymize, ToParameter}; mod test; @@ -288,10 +288,7 @@ trait LowerParameterMap { // trait is not object-safe, and hence not supposed to be used // as an object. Actually the handling of object types is // probably just kind of messed up right now. That's ok. - self.all_parameters() - .into_iter() - .zip(0..) - .collect() + self.all_parameters().into_iter().zip(0..).collect() } } @@ -432,7 +429,8 @@ impl LowerWhereClauseVec for [QuantifiedWhereClause] { .flat_map(|wc| match wc.lower(env) { Ok(v) => v.into_iter().map(Ok).collect(), Err(e) => vec![Err(e)], - }).collect() + }) + .collect() } } @@ -547,18 +545,16 @@ impl LowerLeafGoal for LeafGoal { .into_iter() .map(|goal| chalk_ir::LeafGoal::DomainGoal(goal)) .collect(), - LeafGoal::UnifyTys { a, b } => vec![ - chalk_ir::EqGoal { - a: chalk_ir::ParameterKind::Ty(a.lower(env)?), - b: chalk_ir::ParameterKind::Ty(b.lower(env)?), - }.cast(), - ], - LeafGoal::UnifyLifetimes { ref a, ref b } => vec![ - chalk_ir::EqGoal { - a: chalk_ir::ParameterKind::Lifetime(a.lower(env)?), - b: chalk_ir::ParameterKind::Lifetime(b.lower(env)?), - }.cast(), - ], + LeafGoal::UnifyTys { a, b } => vec![chalk_ir::EqGoal { + a: chalk_ir::ParameterKind::Ty(a.lower(env)?), + b: chalk_ir::ParameterKind::Ty(b.lower(env)?), + } + .cast()], + LeafGoal::UnifyLifetimes { ref a, ref b } => vec![chalk_ir::EqGoal { + a: chalk_ir::ParameterKind::Lifetime(a.lower(env)?), + b: chalk_ir::ParameterKind::Lifetime(b.lower(env)?), + } + .cast()], }; Ok(goals) } @@ -623,7 +619,8 @@ impl LowerTraitRef for TraitRef { let without_self = TraitBound { trait_name: self.trait_name, args_no_self: self.args.iter().cloned().skip(1).collect(), - }.lower(env)?; + } + .lower(env)?; let self_parameter = self.args[0].lower(env)?; Ok(without_self.as_trait_ref(self_parameter.ty().unwrap())) @@ -685,7 +682,8 @@ impl LowerProjectionEqBound for ProjectionEqBound { Some(info) => info, None => bail!("no associated type `{}` defined in trait", self.name.str), }; - let args: Vec<_> = self.args + let args: Vec<_> = self + .args .iter() .map(|a| a.lower(env)) .collect::>()?; @@ -785,10 +783,7 @@ impl LowerProjectionTy for ProjectionTy { Some(info) => info, None => bail!("no associated type `{}` defined in trait", name.str), }; - let mut args: Vec<_> = args - .iter() - .map(|a| a.lower(env)) - .collect::>()?; + let mut args: Vec<_> = args.iter().map(|a| a.lower(env)).collect::>()?; if args.len() != info.addl_parameter_kinds.len() { bail!( @@ -817,7 +812,8 @@ trait LowerUnselectedProjectionTy { impl LowerUnselectedProjectionTy for UnselectedProjectionTy { fn lower(&self, env: &Env) -> Result { - let parameters: Vec<_> = self.args + let parameters: Vec<_> = self + .args .iter() .map(|a| a.lower(env)) .collect::>()?; @@ -954,10 +950,11 @@ impl LowerImpl for Impl { let trait_id = trait_ref.trait_ref().trait_id; let where_clauses = self.lower_where_clauses(&env)?; - let associated_ty_values = self.assoc_ty_values - .iter() - .map(|v| v.lower(trait_id, env)) - .collect::>()?; + let associated_ty_values = self + .assoc_ty_values + .iter() + .map(|v| v.lower(trait_id, env)) + .collect::>()?; Ok(rust_ir::ImplDatumBound { trait_ref, where_clauses, @@ -999,7 +996,8 @@ impl LowerClause for Clause { .map(|consequence| chalk_ir::ProgramClauseImplication { consequence, conditions: conditions.clone(), - }).collect::>(); + }) + .collect::>(); Ok(implications) })?; @@ -1013,7 +1011,8 @@ impl LowerClause for Clause { chalk_ir::ProgramClause::ForAll(implication) } }, - ).collect(); + ) + .collect(); Ok(clauses) } } @@ -1094,7 +1093,8 @@ impl LowerGoal for Goal { addl_parameter_kinds, }; ((datum.trait_id, datum.name), info) - }).collect(); + }) + .collect(); let env = Env { type_ids: &program.type_ids, diff --git a/src/rust_ir/lowering/test.rs b/src/rust_ir/lowering/test.rs index 57ee8b99903..1dcd78e8414 100644 --- a/src/rust_ir/lowering/test.rs +++ b/src/rust_ir/lowering/test.rs @@ -1,9 +1,9 @@ #![cfg(test)] +use crate::test_util::*; use chalk_ir::tls; use chalk_solve::solve::SolverChoice; use std::sync::Arc; -use crate::test_util::*; #[test] fn lower_success() { @@ -158,16 +158,10 @@ fn assoc_tys() { #[test] fn goal_quantifiers() { - let program = Arc::new( - parse_and_lower_program( - "trait Foo { }", - SolverChoice::default() - ).unwrap() - ); - let goal = parse_and_lower_goal( - &program, - "forall {exists {forall {Z: Foo}}}" - ).unwrap(); + let program = + Arc::new(parse_and_lower_program("trait Foo { }", SolverChoice::default()).unwrap()); + let goal = + parse_and_lower_goal(&program, "forall {exists {forall {Z: Foo}}}").unwrap(); tls::set_current_program(&program, || { assert_eq!( format!("{:?}", goal), @@ -193,8 +187,9 @@ fn atc_accounting() { struct Iter<'a, T> { } ", - SolverChoice::default() - ).unwrap(), + SolverChoice::default(), + ) + .unwrap(), ); tls::set_current_program(&program, || { let impl_text = format!("{:#?}", &program.impl_data.values().next().unwrap()); @@ -224,19 +219,20 @@ fn atc_accounting() { &program, "forall { forall<'a> { forall { \ X: Iterable = Y> } } }", - ).unwrap(); + ) + .unwrap(); let goal_text = format!("{:?}", goal); println!("{}", goal_text); assert_eq!( goal_text, "ForAll { \ - ForAll { \ - ForAll { \ - (ProjectionEq(<^2 as Iterable>::Iter<'^1> = ^0), \ - Implemented(^2: Iterable)) \ - } \ - } \ - }" + ForAll { \ + ForAll { \ + (ProjectionEq(<^2 as Iterable>::Iter<'^1> = ^0), \ + Implemented(^2: Iterable)) \ + } \ + } \ + }" ); }); } diff --git a/src/test.rs b/src/test.rs index f3f987af619..d583647c22f 100644 --- a/src/test.rs +++ b/src/test.rs @@ -1,12 +1,12 @@ #![cfg(test)] +use crate::test_util::*; use chalk_engine::fallible::{Fallible, NoSolution}; use chalk_ir; use chalk_solve::ext::*; use chalk_solve::solve::{Solution, SolverChoice}; use std::collections::HashMap; use std::sync::Arc; -use crate::test_util::*; mod bench; mod slg; @@ -90,8 +90,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, &str)>) { for (goal_text, solver_choice, expected) in goals { let (program, env) = program_env_cache.entry(solver_choice).or_insert_with(|| { let program_text = &program_text[1..program_text.len() - 1]; // exclude `{}` - let program = - Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); + let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); let env = Arc::new(program.environment()); (program, env) }); diff --git a/src/test/bench.rs b/src/test/bench.rs index 9d80bf375d8..7e304c5368d 100644 --- a/src/test/bench.rs +++ b/src/test/bench.rs @@ -8,16 +8,14 @@ use chalk_solve::ext::*; use chalk_solve::solve::SolverChoice; use std::sync::Arc; -use super::{parse_and_lower_program, - parse_and_lower_goal, - assert_result}; +use super::{assert_result, parse_and_lower_goal, parse_and_lower_program}; fn run_bench( program_text: &str, solver_choice: SolverChoice, goal_text: &str, bencher: &mut Bencher, - expected: &str + expected: &str, ) { let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); let env = Arc::new(program.environment()); @@ -102,11 +100,9 @@ forall { fn cycley_slg(b: &mut Bencher) { run_bench( CYCLEY, - SolverChoice::SLG { - max_size: 20, - }, + SolverChoice::SLG { max_size: 20 }, CYCLEY_GOAL, b, - "Unique" + "Unique", ); } diff --git a/src/test/slg.rs b/src/test/slg.rs index 28f52775854..3e9712a3085 100644 --- a/src/test/slg.rs +++ b/src/test/slg.rs @@ -1,11 +1,11 @@ #![cfg(test)] +use crate::test_util::*; +use chalk_engine::forest::Forest; use chalk_solve::ext::*; use chalk_solve::solve::slg::implementation::SlgContext; -use chalk_engine::forest::Forest; -use std::sync::Arc; -use crate::test_util::*; use chalk_solve::solve::SolverChoice; +use std::sync::Arc; macro_rules! test { (program $program:tt $(goal $goal:tt first $n:tt with max $depth:tt { $expected:expr })*) => { @@ -24,11 +24,12 @@ fn solve_goal(program_text: &str, goals: Vec<(usize, usize, &str, &str)>) { println!("program {}", program_text); assert!(program_text.starts_with("{")); assert!(program_text.ends_with("}")); - let program = &Arc::new( + let program = &Arc::new( parse_and_lower_program( &program_text[1..program_text.len() - 1], - SolverChoice::default() - ).unwrap() + SolverChoice::default(), + ) + .unwrap(), ); let env = &Arc::new(program.environment()); chalk_ir::tls::set_current_program(&program, || { @@ -54,8 +55,9 @@ fn solve_goal_fixed_num_answers(program_text: &str, goals: Vec<(usize, usize, &s let program = &Arc::new( parse_and_lower_program( &program_text[1..program_text.len() - 1], - SolverChoice::default() - ).unwrap() + SolverChoice::default(), + ) + .unwrap(), ); let env = &Arc::new(program.environment()); chalk_ir::tls::set_current_program(&program, || { diff --git a/src/test_util.rs b/src/test_util.rs index c711684fd9a..69206422143 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -1,14 +1,14 @@ #![cfg(test)] -use diff; +use crate::errors::Result; +use crate::rust_ir::lowering::{LowerGoal, LowerProgram}; +use crate::rust_ir::Program; +use chalk_ir::Goal; use chalk_parse; +use chalk_solve::solve::SolverChoice; +use diff; use itertools::Itertools; use std::fmt::Write; -use crate::rust_ir::lowering::{LowerProgram, LowerGoal}; -use chalk_ir::Goal; -use crate::rust_ir::Program; -use chalk_solve::solve::SolverChoice; -use crate::errors::Result; pub fn parse_and_lower_program(text: &str, solver_choice: SolverChoice) -> Result { chalk_parse::parse_program(text)?.lower(solver_choice) @@ -24,16 +24,14 @@ macro_rules! lowering_success { assert!(program_text.starts_with("{")); assert!(program_text.ends_with("}")); let result = parse_and_lower_program( - &program_text[1..program_text.len()-1], - chalk_solve::solve::SolverChoice::default() + &program_text[1..program_text.len() - 1], + chalk_solve::solve::SolverChoice::default(), ); if let Err(ref e) = result { println!("lowering error: {}", e); } - assert!( - result.is_ok() - ); - } + assert!(result.is_ok()); + }; } macro_rules! lowering_error { @@ -42,15 +40,13 @@ macro_rules! lowering_error { assert!(program_text.starts_with("{")); assert!(program_text.ends_with("}")); let error = parse_and_lower_program( - &program_text[1..program_text.len()-1], - chalk_solve::solve::SolverChoice::default() - ).unwrap_err(); + &program_text[1..program_text.len() - 1], + chalk_solve::solve::SolverChoice::default(), + ) + .unwrap_err(); let expected = $crate::errors::Error::from($expected); - assert_eq!( - error.to_string(), - expected.to_string() - ); - } + assert_eq!(error.to_string(), expected.to_string()); + }; } crate fn assert_test_result_eq(expected: &str, actual: &str) { @@ -60,11 +56,7 @@ crate fn assert_test_result_eq(expected: &str, actual: &str) { .intersperse("\n") .collect(); - let actual_trimmed: String = actual - .lines() - .map(|l| l.trim()) - .intersperse("\n") - .collect(); + let actual_trimmed: String = actual.lines().map(|l| l.trim()).intersperse("\n").collect(); if expected_trimmed == actual_trimmed { return; @@ -73,10 +65,7 @@ crate fn assert_test_result_eq(expected: &str, actual: &str) { println!("expected:\n{}", expected); println!("actual:\n{}", actual); - let diff = diff::lines( - &expected_trimmed, - &actual_trimmed, - ); + let diff = diff::lines(&expected_trimmed, &actual_trimmed); // Skip to the first error: let diff = diff.iter().skip_while(|r| match r { @@ -106,5 +95,9 @@ crate fn assert_test_result_eq(expected: &str, actual: &str) { writeln!(&mut final_diff, "{}{}", prefix, s).unwrap(); } - assert!(false, "expected did not match actual, diff:\n{}", final_diff); + assert!( + false, + "expected did not match actual, diff:\n{}", + final_diff + ); }