Skip to content

Commit 514aacc

Browse files
jackh726jackh726
committed
Fmt
1 parent ae690eb commit 514aacc

File tree

11 files changed

+64
-58
lines changed

11 files changed

+64
-58
lines changed

‎chalk-engine/src/boring_impls.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use crate::{ExClause, FlounderedSubgoal, Literal};
22
use chalk_base::results::Fallible;
3-
use chalk_ir::interner::{Interner, HasInterner, TargetInterner};
43
use chalk_ir::fold::{Fold, Folder};
4+
use chalk_ir::interner::{HasInterner, Interner, TargetInterner};
55
use chalk_ir::visit::{Visit, VisitResult, Visitor};
66
use chalk_ir::{Canonical, ConstrainedSubst, Constraint, DebruijnIndex, InEnvironment};
77
use std::fmt::Debug;

‎chalk-engine/src/context.rs

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,11 @@
88
use crate::{CompleteAnswer, ExClause};
99
use chalk_base::results::{Fallible, Floundered};
1010
use chalk_ir::interner::Interner;
11-
use chalk_ir::{AnswerSubst, Binders, Canonical, ConstrainedSubst, Constraint, DomainGoal, Environment, GenericArg, Goal, InEnvironment, ProgramClause, ProgramClauses, Substitution, UCanonical, UniverseMap};
11+
use chalk_ir::{
12+
AnswerSubst, Binders, Canonical, ConstrainedSubst, Constraint, DomainGoal, Environment,
13+
GenericArg, Goal, InEnvironment, ProgramClause, ProgramClauses, Substitution, UCanonical,
14+
UniverseMap,
15+
};
1216
use std::fmt::Debug;
1317

1418
/// The "context" in which the SLG solver operates. It defines all the
@@ -44,7 +48,9 @@ pub trait Context<I: Interner>: Clone + Debug {
4448
fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize;
4549
}
4650

47-
pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + AggregateOps<I, C> {
51+
pub trait ContextOps<I: Interner, C: Context<I>>:
52+
Sized + Clone + Debug + AggregateOps<I, C>
53+
{
4854
/// True if this is a coinductive goal -- e.g., proving an auto trait.
4955
fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool;
5056

@@ -149,16 +155,15 @@ pub trait AggregateOps<I: Interner, C: Context<I>> {
149155

150156
/// An "inference table" contains the state to support unification and
151157
/// other operations on terms.
152-
pub trait InferenceTable<I: Interner, C: Context<I>>: ResolventOps<I, C> + TruncateOps<I, C> + UnificationOps<I, C> {}
158+
pub trait InferenceTable<I: Interner, C: Context<I>>:
159+
ResolventOps<I, C> + TruncateOps<I, C> + UnificationOps<I, C>
160+
{
161+
}
153162

154163
/// Methods for unifying and manipulating terms and binders.
155164
pub trait UnificationOps<I: Interner, C: Context<I>> {
156165
// Used by: simplify
157-
fn instantiate_binders_universally(
158-
&mut self,
159-
interner: &I,
160-
arg: &Binders<Goal<I>>,
161-
) -> Goal<I>;
166+
fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I>;
162167

163168
// Used by: simplify
164169
fn instantiate_binders_existentially(
@@ -168,11 +173,7 @@ pub trait UnificationOps<I: Interner, C: Context<I>> {
168173
) -> Goal<I>;
169174

170175
// Used by: logic (but for debugging only)
171-
fn debug_ex_clause<'v>(
172-
&mut self,
173-
interner: &I,
174-
value: &'v ExClause<I>,
175-
) -> Box<dyn Debug + 'v>;
176+
fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause<I>) -> Box<dyn Debug + 'v>;
176177

177178
// Used by: logic
178179
fn fully_canonicalize_goal(
@@ -242,11 +243,7 @@ pub trait UnificationOps<I: Interner, C: Context<I>> {
242243
/// - Grosof and Swift; 2013
243244
pub trait TruncateOps<I: Interner, C: Context<I>> {
244245
/// Check if `subgoal` is too large
245-
fn goal_needs_truncation(
246-
&mut self,
247-
interner: &I,
248-
subgoal: &InEnvironment<Goal<I>>,
249-
) -> bool;
246+
fn goal_needs_truncation(&mut self, interner: &I, subgoal: &InEnvironment<Goal<I>>) -> bool;
250247

251248
/// Check if `subst` is too large
252249
fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution<I>) -> bool;

‎chalk-engine/src/forest.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,9 @@ struct ForestSolver<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> {
150150
answer: AnswerIndex,
151151
}
152152

153-
impl<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> AnswerStream<I, C> for ForestSolver<'me, I, C, CO> {
153+
impl<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> AnswerStream<I, C>
154+
for ForestSolver<'me, I, C, CO>
155+
{
154156
/// # Panics
155157
///
156158
/// Panics if a negative cycle was detected.

‎chalk-engine/src/lib.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,9 @@ use std::cmp::min;
6060
use std::usize;
6161

6262
use chalk_ir::interner::Interner;
63-
use chalk_ir::{AnswerSubst, Canonical, Constraint, ConstrainedSubst, Goal, InEnvironment, Substitution};
63+
use chalk_ir::{
64+
AnswerSubst, Canonical, ConstrainedSubst, Constraint, Goal, InEnvironment, Substitution,
65+
};
6466

6567
mod boring_impls;
6668
pub mod context;

‎chalk-engine/src/logic.rs

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,10 @@ use crate::{
1111
use chalk_base::results::{Floundered, NoSolution};
1212

1313
use chalk_ir::interner::Interner;
14-
use chalk_ir::{Canonical, ConstrainedSubst, Goal, GoalData, InEnvironment, Substitution, UCanonical, UniverseMap};
14+
use chalk_ir::{
15+
Canonical, ConstrainedSubst, Goal, GoalData, InEnvironment, Substitution, UCanonical,
16+
UniverseMap,
17+
};
1518

1619
type RootSearchResult<T> = Result<T, RootSearchFail>;
1720

@@ -121,16 +124,19 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
121124
return test(&answer.subst.value.subst);
122125
}
123126

124-
self.tables[table].strands().any(|strand| {
125-
test(&strand.canonical_ex_clause.value.subst)
126-
})
127+
self.tables[table]
128+
.strands()
129+
.any(|strand| test(&strand.canonical_ex_clause.value.subst))
127130
}
128131

129132
pub(crate) fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer<I> {
130133
self.tables[table].answer(answer).unwrap()
131134
}
132135

133-
fn canonicalize_strand(context: &impl ContextOps<I, C>, strand: Strand<I, C>) -> CanonicalStrand<I> {
136+
fn canonicalize_strand(
137+
context: &impl ContextOps<I, C>,
138+
strand: Strand<I, C>,
139+
) -> CanonicalStrand<I> {
134140
let Strand {
135141
mut infer,
136142
ex_clause,
@@ -409,7 +415,9 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
409415
}
410416
}
411417

412-
impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'forest> SolveState<'forest, I, C, CO> {
418+
impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'forest>
419+
SolveState<'forest, I, C, CO>
420+
{
413421
/// Ensures that answer with the given index is available from the
414422
/// given table. Returns `Ok` if there is an answer.
415423
///

‎chalk-engine/src/simplify.rs

Lines changed: 16 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use crate::{ExClause, Literal, TimeStamp};
44
use chalk_base::results::Fallible;
55

66
use chalk_ir::interner::Interner;
7-
use chalk_ir::{Environment, InEnvironment, Goal, GoalData, Substitution, QuantifierKind};
7+
use chalk_ir::{Environment, Goal, GoalData, InEnvironment, QuantifierKind, Substitution};
88

99
impl<I: Interner, C: Context<I>> Forest<I, C> {
1010
/// Simplifies an HH goal into a series of positive domain goals
@@ -54,21 +54,25 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
5454
GoalData::Not(subgoal) => {
5555
ex_clause
5656
.subgoals
57-
.push(Literal::Negative(InEnvironment::new(&environment, subgoal.clone())));
57+
.push(Literal::Negative(InEnvironment::new(
58+
&environment,
59+
subgoal.clone(),
60+
)));
5861
}
59-
GoalData::EqGoal(goal) => {
60-
infer.unify_generic_args_into_ex_clause(
61-
context.interner(),
62-
&environment,
63-
&goal.a,
64-
&goal.b,
65-
&mut ex_clause,
66-
)?
67-
},
62+
GoalData::EqGoal(goal) => infer.unify_generic_args_into_ex_clause(
63+
context.interner(),
64+
&environment,
65+
&goal.a,
66+
&goal.b,
67+
&mut ex_clause,
68+
)?,
6869
GoalData::DomainGoal(domain_goal) => {
6970
ex_clause
7071
.subgoals
71-
.push(Literal::Positive(InEnvironment::new(&environment, context.into_goal(domain_goal.clone()))));
72+
.push(Literal::Positive(InEnvironment::new(
73+
&environment,
74+
context.into_goal(domain_goal.clone()),
75+
)));
7276
}
7377
GoalData::CannotProve(()) => {
7478
ex_clause.ambiguous = true;

‎chalk-engine/src/tables.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,10 @@ impl<I: Interner> Tables<I> {
3939
index
4040
}
4141

42-
pub(super) fn index_of(&self, literal: &UCanonical<InEnvironment<Goal<I>>>) -> Option<TableIndex> {
42+
pub(super) fn index_of(
43+
&self,
44+
literal: &UCanonical<InEnvironment<Goal<I>>>,
45+
) -> Option<TableIndex> {
4346
self.table_indices.get(literal).cloned()
4447
}
4548
}

‎chalk-solve/src/recursive/fulfill.rs

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
use crate::infer::{
2-
canonicalize::Canonicalized,
3-
instantiate::IntoBindersAndValue,
4-
ucanonicalize::UCanonicalized,
5-
unify::UnificationResult,
6-
InferenceTable, ParameterEnaVariable, ParameterEnaVariableExt,
2+
canonicalize::Canonicalized, instantiate::IntoBindersAndValue, ucanonicalize::UCanonicalized,
3+
unify::UnificationResult, InferenceTable, ParameterEnaVariable, ParameterEnaVariableExt,
74
};
85
use crate::recursive::{Minimums, Solver};
96
use crate::solve::{truncate, Guidance, Solution};
@@ -14,7 +11,7 @@ use chalk_ir::interner::{HasInterner, Interner};
1411
use chalk_ir::zip::Zip;
1512
use chalk_ir::{
1613
Canonical, ConstrainedSubst, Constraint, Environment, EqGoal, Goal, GoalData, InEnvironment,
17-
QuantifierKind, Substitution, UCanonical, UniverseMap
14+
QuantifierKind, Substitution, UCanonical, UniverseMap,
1815
};
1916
use rustc_hash::FxHashSet;
2017
use std::fmt::Debug;

‎chalk-solve/src/solve.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -269,7 +269,9 @@ pub struct Solver<I: Interner>(SolverImpl<I>);
269269

270270
enum SolverImpl<I: Interner> {
271271
#[cfg(feature = "slg-solver")]
272-
Slg { forest: Box<Forest<I, SlgContext<I>>> },
272+
Slg {
273+
forest: Box<Forest<I, SlgContext<I>>>,
274+
},
273275
#[cfg(feature = "recursive-solver")]
274276
Recursive(Box<RecursiveContext<I>>),
275277
}

‎chalk-solve/src/solve/slg.rs

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -241,11 +241,7 @@ impl<I: Interner> context::UnificationOps<I, SlgContext<I>> for TruncatingInfere
241241
self.infer.instantiate_binders_existentially(interner, arg)
242242
}
243243

244-
fn debug_ex_clause<'v>(
245-
&mut self,
246-
interner: &I,
247-
value: &'v ExClause<I>,
248-
) -> Box<dyn Debug + 'v> {
244+
fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause<I>) -> Box<dyn Debug + 'v> {
249245
Box::new(self.infer.normalize_deep(interner, value))
250246
}
251247

0 commit comments

Comments
 (0)