@@ -7,7 +7,8 @@ use crate::split::Split;
7
7
use crate :: RustIrDatabase ;
8
8
use chalk_ir:: cast:: * ;
9
9
use chalk_ir:: fold:: shift:: Shift ;
10
- use chalk_ir:: interner:: { HasInterner , Interner } ;
10
+ use chalk_ir:: interner:: Interner ;
11
+ use chalk_ir:: visit:: { Visit , Visitor } ;
11
12
use chalk_ir:: * ;
12
13
use chalk_rust_ir:: * ;
13
14
@@ -41,69 +42,63 @@ pub struct WfSolver<'db, I: Interner> {
41
42
solver_choice : SolverChoice ,
42
43
}
43
44
44
- /// A trait for retrieving all types appearing in some Chalk construction.
45
- ///
46
- /// FIXME: why is this not a `Folder`?
47
- trait FoldInputTypes : HasInterner {
48
- fn fold ( & self , interner : & Self :: Interner , accumulator : & mut Vec < Ty < Self :: Interner > > ) ;
45
+ struct InputTypeCollector < ' i , I : Interner > {
46
+ types : Vec < Ty < I > > ,
47
+ interner : & ' i I ,
49
48
}
50
49
51
- impl < T : FoldInputTypes > FoldInputTypes for [ T ] {
52
- fn fold ( & self , interner : & T :: Interner , accumulator : & mut Vec < Ty < T :: Interner > > ) {
53
- for f in self {
54
- f. fold ( interner, accumulator) ;
50
+ impl < ' i , I : Interner > InputTypeCollector < ' i , I > {
51
+ fn new ( interner : & ' i I ) -> Self {
52
+ Self {
53
+ types : Vec :: new ( ) ,
54
+ interner,
55
55
}
56
56
}
57
57
}
58
58
59
- impl < T : FoldInputTypes > FoldInputTypes for Vec < T > {
60
- fn fold ( & self , interner : & T :: Interner , accumulator : & mut Vec < Ty < T :: Interner > > ) {
61
- for f in self {
62
- f. fold ( interner, accumulator) ;
63
- }
64
- }
65
- }
59
+ impl < ' i , ' t , I : Interner > Visitor < ' i , I > for InputTypeCollector < ' i , I > {
60
+ type Result = ( ) ;
66
61
67
- impl < I : Interner > FoldInputTypes for Parameter < I > {
68
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
69
- if let ParameterKind :: Ty ( ty) = self . data ( interner) {
70
- ty. fold ( interner, accumulator)
71
- }
62
+ fn as_dyn ( & mut self ) -> & mut dyn Visitor < ' i , I , Result = Self :: Result > {
63
+ self
72
64
}
73
- }
74
65
75
- impl < I : Interner > FoldInputTypes for Substitution < I > {
76
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
77
- self . parameters ( interner) . fold ( interner, accumulator)
66
+ fn interner ( & self ) -> & ' i I {
67
+ self . interner
78
68
}
79
- }
80
69
81
- impl < I : Interner > FoldInputTypes for QuantifiedWhereClauses < I > {
82
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
83
- self . as_slice ( interner) . fold ( interner, accumulator)
70
+ fn visit_alias_eq ( & mut self , alias_eq : & AliasEq < I > , outer_binder : DebruijnIndex ) {
71
+ TyData :: Alias ( alias_eq. alias . clone ( ) )
72
+ . intern ( self . interner )
73
+ . visit_with ( self , outer_binder) ;
74
+ alias_eq. ty . visit_with ( self , outer_binder) ;
84
75
}
85
- }
86
76
87
- impl < I : Interner > FoldInputTypes for Ty < I > {
88
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
89
- match self . data ( interner) {
90
- TyData :: Apply ( app) => {
91
- accumulator. push ( self . clone ( ) ) ;
92
- app. substitution . fold ( interner, accumulator) ;
77
+ fn visit_ty ( & mut self , ty : & Ty < I > , outer_binder : DebruijnIndex ) {
78
+ let interner = self . interner ( ) ;
79
+
80
+ let mut push_ty = || {
81
+ self . types
82
+ . push ( ty. shifted_out_to ( interner, outer_binder) . unwrap ( ) )
83
+ } ;
84
+ match ty. data ( interner) {
85
+ TyData :: Apply ( apply) => {
86
+ push_ty ( ) ;
87
+ apply. visit_with ( self , outer_binder) ;
93
88
}
94
89
95
- TyData :: Dyn ( qwc ) => {
96
- accumulator . push ( self . clone ( ) ) ;
97
- qwc . bounds . fold ( interner , accumulator ) ;
90
+ TyData :: Dyn ( clauses ) => {
91
+ push_ty ( ) ;
92
+ clauses . visit_with ( self , outer_binder ) ;
98
93
}
99
94
100
95
TyData :: Alias ( alias) => {
101
- accumulator . push ( self . clone ( ) ) ;
102
- alias. substitution . fold ( interner , accumulator ) ;
96
+ push_ty ( ) ;
97
+ alias. visit_with ( self , outer_binder ) ;
103
98
}
104
99
105
100
TyData :: Placeholder ( _) => {
106
- accumulator . push ( self . clone ( ) ) ;
101
+ push_ty ( ) ;
107
102
}
108
103
109
104
// Type parameters do not carry any input types (so we can sort of assume they are
@@ -117,53 +112,12 @@ impl<I: Interner> FoldInputTypes for Ty<I> {
117
112
TyData :: Function ( ..) => ( ) ,
118
113
119
114
TyData :: InferenceVar ( ..) => {
120
- panic ! ( "unexpected inference variable in wf rules: {:?}" , self )
115
+ panic ! ( "unexpected inference variable in wf rules: {:?}" , ty )
121
116
}
122
117
}
123
118
}
124
119
}
125
120
126
- impl < I : Interner > FoldInputTypes for TraitRef < I > {
127
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
128
- self . substitution . fold ( interner, accumulator) ;
129
- }
130
- }
131
-
132
- impl < I : Interner > FoldInputTypes for AliasEq < I > {
133
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
134
- TyData :: Alias ( self . alias . clone ( ) )
135
- . intern ( interner)
136
- . fold ( interner, accumulator) ;
137
- self . ty . fold ( interner, accumulator) ;
138
- }
139
- }
140
-
141
- impl < I : Interner > FoldInputTypes for WhereClause < I > {
142
- fn fold ( & self , interner : & I , accumulator : & mut Vec < Ty < I > > ) {
143
- match self {
144
- WhereClause :: Implemented ( tr) => tr. fold ( interner, accumulator) ,
145
- WhereClause :: AliasEq ( p) => p. fold ( interner, accumulator) ,
146
- }
147
- }
148
- }
149
-
150
- impl < T : FoldInputTypes > FoldInputTypes for Binders < T > {
151
- fn fold ( & self , interner : & T :: Interner , accumulator : & mut Vec < Ty < T :: Interner > > ) {
152
- // FIXME: This aspect of how we've formulated implied bounds
153
- // seems to have an "eager normalization" problem, what about
154
- // where clauses like `for<T> { <Self as Foo<T>>::Bar }`?
155
- //
156
- // For now, the unwrap will panic.
157
- let mut types = vec ! [ ] ;
158
- self . value . fold ( interner, & mut types) ;
159
- accumulator. extend (
160
- types
161
- . into_iter ( )
162
- . map ( |ty| ty. shifted_out ( interner) . unwrap ( ) ) ,
163
- ) ;
164
- }
165
- }
166
-
167
121
impl < ' db , I > WfSolver < ' db , I >
168
122
where
169
123
I : Interner ,
@@ -207,18 +161,13 @@ where
207
161
. map ( |wc| wc. into_from_env_goal ( interner) ) ,
208
162
|gb| {
209
163
// WellFormed(Vec<T>), for each field type `Vec<T>` or type that appears in the where clauses
210
- let mut input_types = Vec :: new ( ) ;
164
+ let mut type_collector = InputTypeCollector :: new ( gb. interner ( ) ) ;
165
+
211
166
// ...in a field type...
212
- fields. fold ( gb . interner ( ) , & mut input_types ) ;
167
+ fields. visit_with ( & mut type_collector , DebruijnIndex :: INNERMOST ) ;
213
168
// ...in a where clause.
214
- where_clauses. fold ( gb. interner ( ) , & mut input_types) ;
215
-
216
- gb. all (
217
- input_types
218
- . into_iter ( )
219
- . map ( |ty| ty. well_formed ( ) . cast ( interner) )
220
- . chain ( sized_constraint_goal. into_iter ( ) ) ,
221
- )
169
+ where_clauses. visit_with ( & mut type_collector, DebruijnIndex :: INNERMOST ) ;
170
+ gb. all ( type_collector. types . into_iter ( ) . map ( |ty| ty. well_formed ( ) ) . chain ( sized_constraint_goal. into_iter ( ) ) )
222
171
} ,
223
172
)
224
173
} ) ;
@@ -308,13 +257,14 @@ fn impl_header_wf_goal<I: Interner>(
308
257
// we would retrieve `HashSet<K>`, `Box<T>`, `Vec<Box<T>>`, `(HashSet<K>, Vec<Box<T>>)`.
309
258
// We will have to prove that these types are well-formed (e.g. an additional `K: Hash`
310
259
// bound would be needed here).
311
- let mut input_types = Vec :: new ( ) ;
312
- where_clauses. fold ( interner , & mut input_types ) ;
260
+ let mut type_collector = InputTypeCollector :: new ( interner ) ;
261
+ where_clauses. visit_with ( & mut type_collector , DebruijnIndex :: INNERMOST ) ;
313
262
314
263
// Things to prove well-formed: input types of the where-clauses, projection types
315
264
// appearing in the header, associated type values, and of course the trait ref.
316
- debug ! ( "verify_trait_impl: input_types={:?}" , input_types) ;
317
- let goals = input_types
265
+ debug ! ( "verify_trait_impl: input_types={:?}" , type_collector. types) ;
266
+ let goals = type_collector
267
+ . types
318
268
. into_iter ( )
319
269
. map ( |ty| ty. well_formed ( ) . cast ( interner) )
320
270
. chain ( Some ( ( * trait_ref) . clone ( ) . well_formed ( ) . cast ( interner) ) ) ;
@@ -350,10 +300,11 @@ fn impl_wf_environment<'i, I: Interner>(
350
300
// // Inside here, we can rely on the fact that `K: Hash` holds
351
301
// }
352
302
// ```
353
- let mut header_input_types = Vec :: new ( ) ;
354
- trait_ref. fold ( interner , & mut header_input_types ) ;
303
+ let mut type_collector = InputTypeCollector :: new ( interner ) ;
304
+ trait_ref. visit_with ( & mut type_collector , DebruijnIndex :: INNERMOST ) ;
355
305
356
- let types_wf = header_input_types
306
+ let types_wf = type_collector
307
+ . types
357
308
. into_iter ( )
358
309
. map ( move |ty| ty. into_from_env_goal ( interner) . cast ( interner) ) ;
359
310
@@ -454,11 +405,12 @@ fn compute_assoc_ty_goal<I: Interner>(
454
405
. cloned ( )
455
406
. map ( |qwc| qwc. into_from_env_goal ( interner) ) ,
456
407
|gb| {
457
- let mut input_types = Vec :: new ( ) ;
458
- value_ty. fold ( interner , & mut input_types ) ;
408
+ let mut type_collector = InputTypeCollector :: new ( interner ) ;
409
+ value_ty. visit_with ( & mut type_collector , DebruijnIndex :: INNERMOST ) ;
459
410
460
411
// We require that `WellFormed(T)` for each type that appears in the value
461
- let wf_goals = input_types
412
+ let wf_goals = type_collector
413
+ . types
462
414
. into_iter ( )
463
415
. map ( |ty| ty. well_formed ( ) )
464
416
. casted ( interner) ;
0 commit comments