Skip to content

Commit 114716d

Browse files
basil-cowbasil-cow
committed
rework VisitResult design, add helper method in wf
1 parent 88614f6 commit 114716d

File tree

5 files changed

+87
-55
lines changed

5 files changed

+87
-55
lines changed

‎chalk-derive/src/lib.rs

Lines changed: 20 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -494,11 +494,16 @@ fn derive_visit_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream
494494
Data::Struct(s) => {
495495
let fields = s.fields.into_iter().map(|f| {
496496
let name = f.ident.as_ref().expect("Unnamed field in a struct");
497-
quote! { .and_then(|| self.#name.visit_with(visitor, outer_binder)) }
497+
quote! {
498+
result = result.combine(self.#name.visit_with(visitor, outer_binder));
499+
if result.return_early() { return result; }
500+
}
498501
});
499502
quote! {
500-
R::new()
501-
#(#fields)*
503+
let mut result = R::new();
504+
#(#fields)*
505+
506+
result
502507
}
503508
}
504509
Data::Enum(e) => {
@@ -509,8 +514,12 @@ fn derive_visit_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream
509514
let fnames: &Vec<_> = &fields.named.iter().map(|f| &f.ident).collect();
510515
quote! {
511516
#type_name :: #variant { #(#fnames),* } => {
512-
R::new()
513-
#(.and_then(|| #fnames.visit_with(visitor, outer_binder)))*
517+
let mut result = R::new();
518+
#(
519+
result = result.combine(#fnames.visit_with(visitor, outer_binder));
520+
if result.return_early() { return result; }
521+
)*
522+
result
514523
}
515524
}
516525
}
@@ -521,8 +530,12 @@ fn derive_visit_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream
521530
.collect();
522531
quote! {
523532
#type_name::#variant( #(ref #names),* ) => {
524-
R::new()
525-
#(.and_then(|| #names.visit_with(visitor, outer_binder)))*
533+
let mut result = R::new();
534+
#(
535+
result = result.combine(#names.visit_with(visitor, outer_binder));
536+
if result.return_early() { return result; }
537+
)*
538+
result
526539
}
527540
}
528541
}

‎chalk-ir/src/visit.rs

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,14 +15,25 @@ pub use visitors::VisitExt;
1515
pub trait VisitResult: Sized {
1616
fn new() -> Self;
1717

18-
fn and_then(self, op: impl FnOnce() -> Self) -> Self;
18+
fn return_early(&self) -> bool;
19+
fn combine(self, other: Self) -> Self;
20+
21+
fn and_then(self, op: impl FnOnce() -> Self) -> Self {
22+
if self.return_early() {
23+
self
24+
} else {
25+
self.combine(op())
26+
}
27+
}
1928
}
2029

2130
impl VisitResult for () {
2231
fn new() -> () {}
23-
fn and_then(self, op: impl FnOnce() -> ()) -> () {
24-
op()
32+
33+
fn return_early(&self) -> bool {
34+
false
2535
}
36+
fn combine(self, _other: Self) {}
2637
}
2738

2839
/// A "visitor" recursively folds some term -- that is, some bit of IR,

‎chalk-ir/src/visit/boring_impls.rs

Lines changed: 30 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,27 @@ use crate::{
1212
use chalk_engine::{context::Context, ExClause, FlounderedSubgoal, Literal};
1313
use std::{marker::PhantomData, sync::Arc};
1414

15+
pub fn visit_iter<'i, T, I, IT, R>(
16+
it: IT,
17+
visitor: &mut dyn Visitor<'i, I, Result = R>,
18+
outer_binder: DebruijnIndex,
19+
) -> R
20+
where
21+
T: Visit<I>,
22+
I: 'i + Interner,
23+
IT: Iterator<Item = T>,
24+
R: VisitResult,
25+
{
26+
let mut result = R::new();
27+
for e in it {
28+
result = result.combine(e.visit_with(visitor, outer_binder));
29+
if result.return_early() {
30+
return result;
31+
}
32+
}
33+
result
34+
}
35+
1536
impl<T: Visit<I>, I: Interner> Visit<I> for &T {
1637
fn visit_with<'i, R: VisitResult>(
1738
&self,
@@ -34,11 +55,7 @@ impl<T: Visit<I>, I: Interner> Visit<I> for Vec<T> {
3455
where
3556
I: 'i,
3657
{
37-
let mut result = R::new();
38-
for e in self {
39-
result = result.and_then(|| e.visit_with(visitor, outer_binder))
40-
}
41-
result
58+
visit_iter(self.iter(), visitor, outer_binder)
4259
}
4360
}
4461

@@ -75,8 +92,12 @@ macro_rules! tuple_visit {
7592
{
7693
#[allow(non_snake_case)]
7794
let &($(ref $n),*) = self;
78-
R::new()
79-
$(.and_then(|| $n.visit_with(visitor, outer_binder)))*
95+
let mut result = R::new();
96+
$(
97+
result = result.combine($n.visit_with(visitor, outer_binder));
98+
if result.return_early() { return result; }
99+
)*
100+
result
80101
}
81102
}
82103
}
@@ -127,13 +148,7 @@ impl<I: Interner> Visit<I> for Substitution<I> {
127148
I: 'i,
128149
{
129150
let interner = visitor.interner();
130-
let mut result = R::new();
131-
132-
for p in self.iter(interner) {
133-
result = result.and_then(|| p.visit_with(visitor, outer_binder));
134-
}
135-
136-
result
151+
visit_iter(self.iter(interner), visitor, outer_binder)
137152
}
138153
}
139154

@@ -147,13 +162,7 @@ impl<I: Interner> Visit<I> for Goals<I> {
147162
I: 'i,
148163
{
149164
let interner = visitor.interner();
150-
let mut result = R::new();
151-
152-
for p in self.iter(interner) {
153-
result = result.and_then(|| p.visit_with(visitor, outer_binder));
154-
}
155-
156-
result
165+
visit_iter(self.iter(interner), visitor, outer_binder)
157166
}
158167
}
159168

‎chalk-ir/src/visit/visitors.rs

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,13 @@ impl VisitResult for FindAny {
2727
fn new() -> Self {
2828
FindAny { found: false }
2929
}
30-
fn and_then(self, op: impl FnOnce() -> Self) -> Self {
31-
if self.found {
32-
self
33-
} else {
34-
op()
30+
31+
fn return_early(&self) -> bool {
32+
self.found
33+
}
34+
fn combine(self, other: Self) -> Self {
35+
FindAny {
36+
found: self.found || other.found,
3537
}
3638
}
3739
}

‎chalk-solve/src/wf.rs

Lines changed: 16 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,12 @@ impl<'i, I: Interner> InputTypeCollector<'i, I> {
5454
interner,
5555
}
5656
}
57+
58+
fn types_in(interner: &'i I, value: impl Visit<I>) -> Vec<Ty<I>> {
59+
let mut collector = Self::new(interner);
60+
value.visit_with(&mut collector, DebruijnIndex::INNERMOST);
61+
collector.types
62+
}
5763
}
5864

5965
impl<'i, 't, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> {
@@ -168,13 +174,10 @@ where
168174
.map(|wc| wc.into_from_env_goal(interner)),
169175
|gb| {
170176
// WellFormed(Vec<T>), for each field type `Vec<T>` or type that appears in the where clauses
171-
let mut type_collector = InputTypeCollector::new(gb.interner());
177+
let types =
178+
InputTypeCollector::types_in(gb.interner(), (&fields, &where_clauses));
172179

173-
// ...in a field type...
174-
fields.visit_with(&mut type_collector, DebruijnIndex::INNERMOST);
175-
// ...in a where clause.
176-
where_clauses.visit_with(&mut type_collector, DebruijnIndex::INNERMOST);
177-
gb.all(type_collector.types.into_iter().map(|ty| ty.well_formed()).chain(sized_constraint_goal.into_iter()))
180+
gb.all(types.into_iter().map(|ty| ty.well_formed()).chain(sized_constraint_goal.into_iter()))
178181
},
179182
)
180183
});
@@ -264,14 +267,12 @@ fn impl_header_wf_goal<I: Interner>(
264267
// we would retrieve `HashSet<K>`, `Box<T>`, `Vec<Box<T>>`, `(HashSet<K>, Vec<Box<T>>)`.
265268
// We will have to prove that these types are well-formed (e.g. an additional `K: Hash`
266269
// bound would be needed here).
267-
let mut type_collector = InputTypeCollector::new(interner);
268-
where_clauses.visit_with(&mut type_collector, DebruijnIndex::INNERMOST);
270+
let types = InputTypeCollector::types_in(gb.interner(), &where_clauses);
269271

270272
// Things to prove well-formed: input types of the where-clauses, projection types
271273
// appearing in the header, associated type values, and of course the trait ref.
272-
debug!("verify_trait_impl: input_types={:?}", type_collector.types);
273-
let goals = type_collector
274-
.types
274+
debug!("verify_trait_impl: input_types={:?}", types);
275+
let goals = types
275276
.into_iter()
276277
.map(|ty| ty.well_formed().cast(interner))
277278
.chain(Some((*trait_ref).clone().well_formed().cast(interner)));
@@ -307,11 +308,9 @@ fn impl_wf_environment<'i, I: Interner>(
307308
// // Inside here, we can rely on the fact that `K: Hash` holds
308309
// }
309310
// ```
310-
let mut type_collector = InputTypeCollector::new(interner);
311-
trait_ref.visit_with(&mut type_collector, DebruijnIndex::INNERMOST);
311+
let types = InputTypeCollector::types_in(interner, trait_ref);
312312

313-
let types_wf = type_collector
314-
.types
313+
let types_wf = types
315314
.into_iter()
316315
.map(move |ty| ty.into_from_env_goal(interner).cast(interner));
317316

@@ -412,12 +411,10 @@ fn compute_assoc_ty_goal<I: Interner>(
412411
.cloned()
413412
.map(|qwc| qwc.into_from_env_goal(interner)),
414413
|gb| {
415-
let mut type_collector = InputTypeCollector::new(interner);
416-
value_ty.visit_with(&mut type_collector, DebruijnIndex::INNERMOST);
414+
let types = InputTypeCollector::types_in(gb.interner(), value_ty);
417415

418416
// We require that `WellFormed(T)` for each type that appears in the value
419-
let wf_goals = type_collector
420-
.types
417+
let wf_goals = types
421418
.into_iter()
422419
.map(|ty| ty.well_formed())
423420
.casted(interner);

0 commit comments

Comments
 (0)