Skip to content

Commit 5f1fc74

Browse files
tmandrytmandry
committed
cargo fmt
1 parent 0e30fab commit 5f1fc74

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

49 files changed

+568
-477
lines changed

‎chalk-engine/src/context/prelude.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
#![allow(unused_imports)] // rustc bug
22

3+
pub(crate) use super::AggregateOps;
34
pub(crate) use super::Context;
45
pub(crate) use super::ContextOps;
5-
pub(crate) use super::AggregateOps;
6+
pub(crate) use super::InferenceTable;
67
pub(crate) use super::ResolventOps;
78
pub(crate) use super::TruncateOps;
8-
pub(crate) use super::InferenceTable;

‎chalk-engine/src/derived.rs

+17-18
Original file line numberDiff line numberDiff line change
@@ -2,21 +2,24 @@
22
// because the `#[derive()]` would add requirements onto the context
33
// object that are not needed.
44

5-
use std::cmp::{PartialEq, Eq};
5+
use super::*;
6+
use std::cmp::{Eq, PartialEq};
67
use std::hash::{Hash, Hasher};
78
use std::mem;
8-
use super::*;
99

1010
impl<C: Context> PartialEq for DelayedLiteralSet<C> {
1111
fn eq(&self, other: &Self) -> bool {
12-
let DelayedLiteralSet { delayed_literals: a1 } = self;
13-
let DelayedLiteralSet { delayed_literals: a2 } = other;
12+
let DelayedLiteralSet {
13+
delayed_literals: a1,
14+
} = self;
15+
let DelayedLiteralSet {
16+
delayed_literals: a2,
17+
} = other;
1418
a1 == a2
1519
}
1620
}
1721

18-
impl<C: Context> Eq for DelayedLiteralSet<C> {
19-
}
22+
impl<C: Context> Eq for DelayedLiteralSet<C> {}
2023

2124
///////////////////////////////////////////////////////////////////////////
2225

@@ -27,22 +30,20 @@ impl<C: Context> PartialEq for DelayedLiteral<C> {
2730
}
2831

2932
match (self, other) {
30-
(DelayedLiteral::CannotProve(()), DelayedLiteral::CannotProve(())) =>
31-
true,
33+
(DelayedLiteral::CannotProve(()), DelayedLiteral::CannotProve(())) => true,
3234

33-
(DelayedLiteral::Negative(a1), DelayedLiteral::Negative(a2)) =>
34-
a1 == a2,
35+
(DelayedLiteral::Negative(a1), DelayedLiteral::Negative(a2)) => a1 == a2,
3536

36-
(DelayedLiteral::Positive(a1, b1), DelayedLiteral::Positive(a2, b2)) =>
37-
a1 == a2 && b1 == b2,
37+
(DelayedLiteral::Positive(a1, b1), DelayedLiteral::Positive(a2, b2)) => {
38+
a1 == a2 && b1 == b2
39+
}
3840

39-
_ => panic!()
41+
_ => panic!(),
4042
}
4143
}
4244
}
4345

44-
impl<C: Context> Eq for DelayedLiteral<C> {
45-
}
46+
impl<C: Context> Eq for DelayedLiteral<C> {}
4647

4748
impl<C: Context> Hash for DelayedLiteral<C> {
4849
fn hash<H: Hasher>(&self, hasher: &mut H) {
@@ -76,8 +77,7 @@ impl<C: Context> PartialEq for Literal<C> {
7677
}
7778
}
7879

79-
impl<C: Context> Eq for Literal<C> {
80-
}
80+
impl<C: Context> Eq for Literal<C> {}
8181

8282
impl<C: Context> Hash for Literal<C> {
8383
fn hash<H: Hasher>(&self, state: &mut H) {
@@ -89,4 +89,3 @@ impl<C: Context> Hash for Literal<C> {
8989
}
9090
}
9191
}
92-

‎chalk-engine/src/forest.rs

+5-3
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
use crate::{DepthFirstNumber, SimplifiedAnswer, TableIndex};
21
use crate::context::prelude::*;
32
use crate::context::AnswerStream;
43
use crate::logic::RootSearchFail;
54
use crate::stack::{Stack, StackIndex};
6-
use crate::tables::Tables;
75
use crate::table::{Answer, AnswerIndex};
6+
use crate::tables::Tables;
7+
use crate::{DepthFirstNumber, SimplifiedAnswer, TableIndex};
88

99
pub struct Forest<C: Context, CO: ContextOps<C>> {
1010
#[allow(dead_code)]
@@ -79,7 +79,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
7979
/// as much work towards `goal` as it has to (and that works is
8080
/// cached for future attempts).
8181
pub fn solve(&mut self, goal: &C::UCanonicalGoalInEnvironment) -> Option<C::Solution> {
82-
self.context.clone().make_solution(CO::canonical(&goal), self.iter_answers(goal))
82+
self.context
83+
.clone()
84+
.make_solution(CO::canonical(&goal), self.iter_answers(goal))
8385
}
8486

8587
/// True if all the tables on the stack starting from `depth` and

‎chalk-engine/src/hh.rs

-1
Original file line numberDiff line numberDiff line change
@@ -22,4 +22,3 @@ pub enum HhGoal<C: Context> {
2222
/// as cannot prove.
2323
CannotProve,
2424
}
25-

‎chalk-engine/src/logic.rs

+26-12
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
1-
use crate::{DelayedLiteral, DelayedLiteralSet, DepthFirstNumber, ExClause, Literal, Minimums,
2-
TableIndex};
1+
use crate::context::{prelude::*, WithInstantiatedExClause, WithInstantiatedUCanonicalGoal};
32
use crate::fallible::NoSolution;
4-
use crate::context::{WithInstantiatedExClause, WithInstantiatedUCanonicalGoal, prelude::*};
53
use crate::forest::Forest;
64
use crate::hh::HhGoal;
75
use crate::stack::StackIndex;
86
use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand};
97
use crate::table::{Answer, AnswerIndex};
8+
use crate::{
9+
DelayedLiteral, DelayedLiteralSet, DepthFirstNumber, ExClause, Literal, Minimums, TableIndex,
10+
};
1011
use rustc_hash::FxHashSet;
1112
use std::marker::PhantomData;
1213
use std::mem;
@@ -117,7 +118,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
117118
}
118119

119120
self.tables[table].strands_mut().any(|strand| {
120-
test(CO::inference_normalized_subst_from_ex_clause(&strand.canonical_ex_clause))
121+
test(CO::inference_normalized_subst_from_ex_clause(
122+
&strand.canonical_ex_clause,
123+
))
121124
})
122125
}
123126

@@ -291,7 +294,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
291294
}
292295

293296
impl<C: Context, CO: ContextOps<C>, OP: WithInstantiatedStrand<C, CO>>
294-
WithInstantiatedExClause<C> for With<C, CO, OP> {
297+
WithInstantiatedExClause<C> for With<C, CO, OP>
298+
{
295299
type Output = OP::Output;
296300

297301
fn with<I: Context>(
@@ -401,7 +405,11 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
401405
/// encounters a cycle, and that some of those cycles involve
402406
/// negative edges. In that case, walks all negative edges and
403407
/// converts them to delayed literals.
404-
fn delay_strands_after_cycle(&mut self, table: TableIndex, visited: &mut FxHashSet<TableIndex>) {
408+
fn delay_strands_after_cycle(
409+
&mut self,
410+
table: TableIndex,
411+
visited: &mut FxHashSet<TableIndex>,
412+
) {
405413
let mut tables = vec![];
406414

407415
let num_universes = CO::num_universes(&self.tables[table].table_goal);
@@ -562,7 +570,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
562570
debug!("answer: table={:?}, answer_subst={:?}", table, answer_subst);
563571

564572
let delayed_literals = {
565-
let delayed_literals: FxHashSet<_> = delayed_literals.into_iter()
573+
let delayed_literals: FxHashSet<_> = delayed_literals
574+
.into_iter()
566575
.map(|dl| infer.lift_delayed_literal(dl))
567576
.collect();
568577
DelayedLiteralSet { delayed_literals }
@@ -739,7 +748,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
739748
}
740749

741750
impl<C: Context, CO: ContextOps<C>> WithInstantiatedUCanonicalGoal<C>
742-
for PushInitialStrandsInstantiated<'a, C, CO> {
751+
for PushInitialStrandsInstantiated<'a, C, CO>
752+
{
743753
type Output = ();
744754

745755
fn with<I: Context>(
@@ -1052,10 +1062,14 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
10521062
),
10531063
};
10541064

1055-
let table_goal = &CO::map_goal_from_canonical(&universe_map,
1056-
&CO::canonical(&self.tables[subgoal_table].table_goal));
1057-
let answer_subst =
1058-
&CO::map_subst_from_canonical(&universe_map, &self.answer(subgoal_table, answer_index).subst);
1065+
let table_goal = &CO::map_goal_from_canonical(
1066+
&universe_map,
1067+
&CO::canonical(&self.tables[subgoal_table].table_goal),
1068+
);
1069+
let answer_subst = &CO::map_subst_from_canonical(
1070+
&universe_map,
1071+
&self.answer(subgoal_table, answer_index).subst,
1072+
);
10591073
match infer.apply_answer_subst(ex_clause, &subgoal, table_goal, answer_subst) {
10601074
Ok(mut ex_clause) => {
10611075
// If the answer had delayed literals, we have to

‎chalk-engine/src/simplify.rs

+10-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1+
use crate::context::prelude::*;
12
use crate::fallible::Fallible;
2-
use crate::{ExClause, Literal};
33
use crate::forest::Forest;
44
use crate::hh::HhGoal;
5-
use crate::context::prelude::*;
5+
use crate::{ExClause, Literal};
66

77
impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
88
/// Simplifies an HH goal into a series of positive domain goals
@@ -45,7 +45,10 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
4545
HhGoal::Not(subgoal) => {
4646
ex_clause
4747
.subgoals
48-
.push(Literal::Negative(I::goal_in_environment(&environment, subgoal)));
48+
.push(Literal::Negative(I::goal_in_environment(
49+
&environment,
50+
subgoal,
51+
)));
4952
}
5053
HhGoal::Unify(variance, a, b) => {
5154
let result = infer.unify_parameters(&environment, variance, &a, &b)?;
@@ -69,7 +72,10 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
6972
let goal = infer.cannot_prove();
7073
ex_clause
7174
.subgoals
72-
.push(Literal::Negative(I::goal_in_environment(&environment, goal)));
75+
.push(Literal::Negative(I::goal_in_environment(
76+
&environment,
77+
goal,
78+
)));
7379
}
7480
}
7581
}

‎chalk-engine/src/stack.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ impl Stack {
4848
}
4949

5050
pub(super) fn top_of_stack_from(&self, depth: StackIndex) -> Range<StackIndex> {
51-
depth .. StackIndex::from(self.stack.len())
51+
depth..StackIndex::from(self.stack.len())
5252
}
5353

5454
pub(super) fn push(&mut self, table: TableIndex, dfn: DepthFirstNumber) -> StackIndex {

‎chalk-engine/src/strand.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
use std::fmt::{Debug, Error, Formatter};
2-
use crate::{ExClause, TableIndex};
31
use crate::context::{Context, InferenceTable};
42
use crate::table::AnswerIndex;
3+
use crate::{ExClause, TableIndex};
4+
use std::fmt::{Debug, Error, Formatter};
55

66
#[derive(Debug)]
77
pub(crate) struct CanonicalStrand<C: Context> {

‎chalk-engine/src/table.rs

+9-5
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
use crate::{DelayedLiteralSet, DelayedLiteralSets};
21
use crate::context::prelude::*;
32
use crate::strand::CanonicalStrand;
3+
use crate::{DelayedLiteralSet, DelayedLiteralSets};
44
use rustc_hash::FxHashMap;
5-
use std::collections::VecDeque;
65
use std::collections::hash_map::Entry;
6+
use std::collections::VecDeque;
77
use std::mem;
88

99
pub(crate) struct Table<C: Context> {
@@ -37,7 +37,6 @@ index_struct! {
3737
}
3838
}
3939

40-
4140
/// An "answer" in the on-demand solver corresponds to a fully solved
4241
/// goal for a particular table (modulo delayed literals). It contains
4342
/// a substitution
@@ -48,7 +47,10 @@ pub struct Answer<C: Context> {
4847
}
4948

5049
impl<C: Context> Table<C> {
51-
pub(crate) fn new(table_goal: C::UCanonicalGoalInEnvironment, coinductive_goal: bool) -> Table<C> {
50+
pub(crate) fn new(
51+
table_goal: C::UCanonicalGoalInEnvironment,
52+
coinductive_goal: bool,
53+
) -> Table<C> {
5254
Table {
5355
table_goal,
5456
coinductive_goal,
@@ -93,7 +95,9 @@ impl<C: Context> Table<C> {
9395

9496
let added = match self.answers_hash.entry(answer.subst.clone()) {
9597
Entry::Vacant(entry) => {
96-
entry.insert(DelayedLiteralSets::singleton(answer.delayed_literals.clone()));
98+
entry.insert(DelayedLiteralSets::singleton(
99+
answer.delayed_literals.clone(),
100+
));
97101
true
98102
}
99103

‎chalk-engine/src/tables.rs

+6-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
use crate::TableIndex;
21
use crate::context::prelude::*;
32
use crate::table::Table;
3+
use crate::TableIndex;
44
use rustc_hash::FxHashMap;
55
use std::ops::{Index, IndexMut};
66

@@ -29,7 +29,11 @@ impl<C: Context> Tables<C> {
2929
}
3030
}
3131

32-
pub(super) fn insert(&mut self, goal: C::UCanonicalGoalInEnvironment, coinductive_goal: bool) -> TableIndex {
32+
pub(super) fn insert(
33+
&mut self,
34+
goal: C::UCanonicalGoalInEnvironment,
35+
coinductive_goal: bool,
36+
) -> TableIndex {
3337
let index = self.next_index();
3438
self.tables.push(Table::new(goal.clone(), coinductive_goal));
3539
self.table_indices.insert(goal, index);
@@ -63,4 +67,3 @@ impl<'a, C: Context> IntoIterator for &'a mut Tables<C> {
6367
IntoIterator::into_iter(&mut self.tables)
6468
}
6569
}
66-

0 commit comments

Comments
 (0)