Skip to content

Commit 6944f22

Browse files
Propagate results of Fold signature change up the call graph
1 parent f66f093 commit 6944f22

37 files changed

+482
-414
lines changed

chalk-engine/src/logic.rs

Lines changed: 18 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ impl<I: Interner> Forest<I> {
149149
Forest::canonicalize_strand_from(
150150
context,
151151
&mut infer,
152-
&ex_clause,
152+
ex_clause,
153153
selected_subgoal,
154154
last_pursued_time,
155155
)
@@ -158,12 +158,12 @@ impl<I: Interner> Forest<I> {
158158
fn canonicalize_strand_from(
159159
context: &SlgContextOps<I>,
160160
infer: &mut TruncatingInferenceTable<I>,
161-
ex_clause: &ExClause<I>,
161+
ex_clause: ExClause<I>,
162162
selected_subgoal: Option<SelectedSubgoal>,
163163
last_pursued_time: TimeStamp,
164164
) -> CanonicalStrand<I> {
165165
let canonical_ex_clause =
166-
infer.canonicalize_ex_clause(context.program().interner(), &ex_clause);
166+
infer.canonicalize_ex_clause(context.program().interner(), ex_clause);
167167
CanonicalStrand {
168168
canonical_ex_clause,
169169
selected_subgoal,
@@ -194,10 +194,10 @@ impl<I: Interner> Forest<I> {
194194
// Subgoal abstraction:
195195
let (ucanonical_subgoal, universe_map) = match subgoal {
196196
Literal::Positive(subgoal) => {
197-
Forest::abstract_positive_literal(context, infer, subgoal)?
197+
Forest::abstract_positive_literal(context, infer, subgoal.clone())?
198198
}
199199
Literal::Negative(subgoal) => {
200-
Forest::abstract_negative_literal(context, infer, subgoal)?
200+
Forest::abstract_negative_literal(context, infer, subgoal.clone())?
201201
}
202202
};
203203

@@ -257,7 +257,7 @@ impl<I: Interner> Forest<I> {
257257
chalk_solve::infer::InferenceTable::from_canonical(
258258
context.program().interner(),
259259
goal.universes,
260-
&goal.canonical,
260+
goal.canonical,
261261
);
262262
let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
263263
let goal_data = goal.data(context.program().interner());
@@ -350,9 +350,9 @@ impl<I: Interner> Forest<I> {
350350
fn abstract_positive_literal(
351351
context: &SlgContextOps<I>,
352352
infer: &mut TruncatingInferenceTable<I>,
353-
subgoal: &InEnvironment<Goal<I>>,
353+
subgoal: InEnvironment<Goal<I>>,
354354
) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> {
355-
if infer.goal_needs_truncation(context.program().interner(), subgoal) {
355+
if infer.goal_needs_truncation(context.program().interner(), &subgoal) {
356356
None
357357
} else {
358358
Some(infer.fully_canonicalize_goal(context.program().interner(), subgoal))
@@ -369,7 +369,7 @@ impl<I: Interner> Forest<I> {
369369
fn abstract_negative_literal(
370370
context: &SlgContextOps<I>,
371371
infer: &mut TruncatingInferenceTable<I>,
372-
subgoal: &InEnvironment<Goal<I>>,
372+
subgoal: InEnvironment<Goal<I>>,
373373
) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> {
374374
// First, we have to check that the selected negative literal
375375
// is ground, and invert any universally quantified variables.
@@ -413,7 +413,7 @@ impl<I: Interner> Forest<I> {
413413
if infer.goal_needs_truncation(context.program().interner(), &inverted_subgoal) {
414414
None
415415
} else {
416-
Some(infer.fully_canonicalize_goal(context.program().interner(), &inverted_subgoal))
416+
Some(infer.fully_canonicalize_goal(context.program().interner(), inverted_subgoal))
417417
}
418418
}
419419
}
@@ -494,7 +494,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
494494
let (_, _, ex_clause) = chalk_solve::infer::InferenceTable::from_canonical(
495495
context.program().interner(),
496496
num_universes,
497-
&strand.canonical_ex_clause,
497+
strand.canonical_ex_clause.clone(),
498498
);
499499
let time_eligble = strand.last_pursued_time < clock;
500500
let mode_eligble = match (table_answer_mode, ex_clause.ambiguous) {
@@ -515,7 +515,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
515515
chalk_solve::infer::InferenceTable::from_canonical(
516516
context.program().interner(),
517517
num_universes,
518-
&canonical_ex_clause,
518+
canonical_ex_clause,
519519
);
520520
let infer = TruncatingInferenceTable::new(context.max_size(), infer);
521521
Strand {
@@ -660,7 +660,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
660660
&mut strand.ex_clause,
661661
&subgoal,
662662
&table_goal,
663-
&answer_subst,
663+
answer_subst,
664664
) {
665665
Ok(()) => {
666666
let Strand {
@@ -1078,7 +1078,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
10781078
) = chalk_solve::infer::InferenceTable::from_canonical(
10791079
self.context.program().interner(),
10801080
num_universes,
1081-
&answer.subst,
1081+
answer.subst.clone(),
10821082
);
10831083
let table = TruncatingInferenceTable::new(self.context.max_size(), infer);
10841084

@@ -1414,8 +1414,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
14141414
let filtered_delayed_subgoals = delayed_subgoals
14151415
.into_iter()
14161416
.filter(|delayed_subgoal| {
1417-
let (canonicalized, _) = infer
1418-
.fully_canonicalize_goal(self.context.program().interner(), delayed_subgoal);
1417+
let (canonicalized, _) = infer.fully_canonicalize_goal(
1418+
self.context.program().interner(),
1419+
delayed_subgoal.clone(),
1420+
);
14191421
*table_goal != canonicalized
14201422
})
14211423
.collect();

chalk-engine/src/normalize_deep.rs

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ impl<I: Interner> DeepNormalizer<'_, '_, I> {
2424
pub fn normalize_deep<T: Fold<I>>(
2525
table: &mut InferenceTable<I>,
2626
interner: &I,
27-
value: &T,
27+
value: T,
2828
) -> T::Result {
2929
value
3030
.fold_with(
@@ -53,6 +53,7 @@ where
5353
match self.table.probe_var(var) {
5454
Some(ty) => Ok(ty
5555
.assert_ty_ref(interner)
56+
.clone()
5657
.fold_with(self, DebruijnIndex::INNERMOST)?
5758
.shifted_in(interner)), // FIXME shift
5859
None => {
@@ -72,6 +73,7 @@ where
7273
match self.table.probe_var(var) {
7374
Some(l) => Ok(l
7475
.assert_lifetime_ref(interner)
76+
.clone()
7577
.fold_with(self, DebruijnIndex::INNERMOST)?
7678
.shifted_in(interner)),
7779
None => Ok(var.to_lifetime(interner)), // FIXME shift
@@ -80,17 +82,18 @@ where
8082

8183
fn fold_inference_const(
8284
&mut self,
83-
ty: &Ty<I>,
85+
ty: Ty<I>,
8486
var: InferenceVar,
8587
_outer_binder: DebruijnIndex,
8688
) -> Fallible<Const<I>> {
8789
let interner = self.interner;
8890
match self.table.probe_var(var) {
8991
Some(c) => Ok(c
9092
.assert_const_ref(interner)
93+
.clone()
9194
.fold_with(self, DebruijnIndex::INNERMOST)?
9295
.shifted_in(interner)),
93-
None => Ok(var.to_const(interner, ty.clone())), // FIXME shift
96+
None => Ok(var.to_const(interner, ty)), // FIXME shift
9497
}
9598
}
9699

@@ -149,8 +152,8 @@ mod test {
149152
// _which_ of 'b' and 'c' becomes the root. We need to normalize
150153
// "b" too, then, to ensure we get a consistent result.
151154
assert_eq!(
152-
DeepNormalizer::normalize_deep(&mut table, interner, &a),
153-
ty!(apply (item 0) (expr DeepNormalizer::normalize_deep(&mut table, interner, &b))),
155+
DeepNormalizer::normalize_deep(&mut table, interner, a.clone()),
156+
ty!(apply (item 0) (expr DeepNormalizer::normalize_deep(&mut table, interner, b.clone()))),
154157
);
155158
table
156159
.relate(
@@ -163,7 +166,7 @@ mod test {
163166
)
164167
.unwrap();
165168
assert_eq!(
166-
DeepNormalizer::normalize_deep(&mut table, interner, &a),
169+
DeepNormalizer::normalize_deep(&mut table, interner, a),
167170
ty!(apply (item 0) (apply (item 1)))
168171
);
169172
}

chalk-engine/src/simplify.rs

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,13 +37,17 @@ impl<I: Interner> Forest<I> {
3737
while let Some((environment, goal)) = pending_goals.pop() {
3838
match goal.data(context.program().interner()) {
3939
GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
40-
let subgoal = infer
41-
.instantiate_binders_universally(context.program().interner(), &subgoal);
40+
let subgoal = infer.instantiate_binders_universally(
41+
context.program().interner(),
42+
subgoal.clone(),
43+
);
4244
pending_goals.push((environment, subgoal.clone()));
4345
}
4446
GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
45-
let subgoal = infer
46-
.instantiate_binders_existentially(context.program().interner(), &subgoal);
47+
let subgoal = infer.instantiate_binders_existentially(
48+
context.program().interner(),
49+
subgoal.clone(),
50+
);
4751
pending_goals.push((environment, subgoal.clone()));
4852
}
4953
GoalData::Implies(wc, subgoal) => {

chalk-engine/src/slg.rs

Lines changed: 17 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -61,12 +61,12 @@ impl<I: Interner> SlgContextOps<'_, I> {
6161
let (mut infer, subst, _) = InferenceTable::from_canonical(
6262
self.program.interner(),
6363
goal.universes,
64-
&goal.canonical,
64+
goal.canonical.clone(),
6565
);
6666
infer
6767
.canonicalize(
6868
self.program.interner(),
69-
&ConstrainedSubst {
69+
ConstrainedSubst {
7070
subst,
7171
constraints: Constraints::empty(self.program.interner()),
7272
},
@@ -130,21 +130,18 @@ pub trait ResolventOps<I: Interner> {
130130
ex_clause: &mut ExClause<I>,
131131
selected_goal: &InEnvironment<Goal<I>>,
132132
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
133-
canonical_answer_subst: &Canonical<AnswerSubst<I>>,
133+
canonical_answer_subst: Canonical<AnswerSubst<I>>,
134134
) -> Fallible<()>;
135135
}
136136

137137
/// Methods for unifying and manipulating terms and binders.
138138
pub trait UnificationOps<I: Interner> {
139139
// Used by: simplify
140-
fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I>;
140+
fn instantiate_binders_universally(&mut self, interner: &I, arg: Binders<Goal<I>>) -> Goal<I>;
141141

142142
// Used by: simplify
143-
fn instantiate_binders_existentially(
144-
&mut self,
145-
interner: &I,
146-
arg: &Binders<Goal<I>>,
147-
) -> Goal<I>;
143+
fn instantiate_binders_existentially(&mut self, interner: &I, arg: Binders<Goal<I>>)
144+
-> Goal<I>;
148145

149146
// Used by: logic (but for debugging only)
150147
fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause<I>) -> Box<dyn Debug + 'v>;
@@ -153,14 +150,14 @@ pub trait UnificationOps<I: Interner> {
153150
fn fully_canonicalize_goal(
154151
&mut self,
155152
interner: &I,
156-
value: &InEnvironment<Goal<I>>,
153+
value: InEnvironment<Goal<I>>,
157154
) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap);
158155

159156
// Used by: logic
160157
fn canonicalize_ex_clause(
161158
&mut self,
162159
interner: &I,
163-
value: &ExClause<I>,
160+
value: ExClause<I>,
164161
) -> Canonical<ExClause<I>>;
165162

166163
// Used by: logic
@@ -184,7 +181,7 @@ pub trait UnificationOps<I: Interner> {
184181
fn invert_goal(
185182
&mut self,
186183
interner: &I,
187-
value: &InEnvironment<Goal<I>>,
184+
value: InEnvironment<Goal<I>>,
188185
) -> Option<InEnvironment<Goal<I>>>;
189186

190187
/// First unify the parameters, then add the residual subgoals
@@ -239,14 +236,14 @@ impl<I: Interner> TruncateOps<I> for TruncatingInferenceTable<I> {
239236
}
240237

241238
impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
242-
fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I> {
239+
fn instantiate_binders_universally(&mut self, interner: &I, arg: Binders<Goal<I>>) -> Goal<I> {
243240
self.infer.instantiate_binders_universally(interner, arg)
244241
}
245242

246243
fn instantiate_binders_existentially(
247244
&mut self,
248245
interner: &I,
249-
arg: &Binders<Goal<I>>,
246+
arg: Binders<Goal<I>>,
250247
) -> Goal<I> {
251248
self.infer.instantiate_binders_existentially(interner, arg)
252249
}
@@ -255,14 +252,14 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
255252
Box::new(DeepNormalizer::normalize_deep(
256253
&mut self.infer,
257254
interner,
258-
value,
255+
value.clone(),
259256
))
260257
}
261258

262259
fn fully_canonicalize_goal(
263260
&mut self,
264261
interner: &I,
265-
value: &InEnvironment<Goal<I>>,
262+
value: InEnvironment<Goal<I>>,
266263
) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap) {
267264
let canonicalized_goal = self.infer.canonicalize(interner, value).quantified;
268265
let UCanonicalized {
@@ -275,7 +272,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
275272
fn canonicalize_ex_clause(
276273
&mut self,
277274
interner: &I,
278-
value: &ExClause<I>,
275+
value: ExClause<I>,
279276
) -> Canonical<ExClause<I>> {
280277
self.infer.canonicalize(interner, value).quantified
281278
}
@@ -289,7 +286,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
289286
self.infer
290287
.canonicalize(
291288
interner,
292-
&ConstrainedSubst {
289+
ConstrainedSubst {
293290
subst,
294291
constraints: Constraints::from_iter(interner, constraints),
295292
},
@@ -307,7 +304,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
307304
self.infer
308305
.canonicalize(
309306
interner,
310-
&AnswerSubst {
307+
AnswerSubst {
311308
subst,
312309
constraints: Constraints::from_iter(interner, constraints),
313310
delayed_subgoals,
@@ -319,7 +316,7 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
319316
fn invert_goal(
320317
&mut self,
321318
interner: &I,
322-
value: &InEnvironment<Goal<I>>,
319+
value: InEnvironment<Goal<I>>,
323320
) -> Option<InEnvironment<Goal<I>>> {
324321
self.infer.invert(interner, value)
325322
}

chalk-engine/src/slg/aggregate.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ fn merge_into_guidance<I: Interner>(
181181

182182
let aggr_subst = Substitution::from_iter(interner, aggr_generic_args);
183183

184-
infer.canonicalize(interner, &aggr_subst).quantified
184+
infer.canonicalize(interner, aggr_subst).quantified
185185
}
186186

187187
fn is_trivial<I: Interner>(interner: &I, subst: &Canonical<Substitution<I>>) -> bool {

0 commit comments

Comments
 (0)