]>
Commit | Line | Data |
---|---|---|
c34b1796 AL |
1 | // Copyright 2012-2013 The Rust Project Developers. See the COPYRIGHT |
2 | // file at the top-level directory of this distribution and at | |
3 | // http://rust-lang.org/COPYRIGHT. | |
4 | // | |
5 | // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or | |
6 | // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license | |
7 | // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your | |
8 | // option. This file may not be copied, modified, or distributed | |
9 | // except according to those terms. | |
10 | ||
11 | //! Generalized type relating mechanism. A type relation R relates a | |
12 | //! pair of values (A, B). A and B are usually types or regions but | |
13 | //! can be other things. Examples of type relations are subtyping, | |
14 | //! type equality, etc. | |
15 | ||
54a0048b | 16 | use hir::def_id::DefId; |
8faf50e0 | 17 | use mir::interpret::ConstValue; |
0531ce1d | 18 | use ty::subst::{Kind, UnpackedKind, Substs}; |
54a0048b SL |
19 | use ty::{self, Ty, TyCtxt, TypeFoldable}; |
20 | use ty::error::{ExpectedFound, TypeError}; | |
94b46f34 | 21 | use mir::interpret::GlobalId; |
ea8adc8c | 22 | use util::common::ErrorReported; |
8faf50e0 | 23 | use syntax_pos::DUMMY_SP; |
c34b1796 | 24 | use std::rc::Rc; |
476ff2be | 25 | use std::iter; |
83c7162d | 26 | use rustc_target::spec::abi; |
54a0048b | 27 | use hir as ast; |
a1dfa0c6 | 28 | use traits; |
c34b1796 | 29 | |
e9174d1e | 30 | pub type RelateResult<'tcx, T> = Result<T, TypeError<'tcx>>; |
c34b1796 | 31 | |
62682a34 SL |
32 | #[derive(Clone, Debug)] |
33 | pub enum Cause { | |
c1a9b12d | 34 | ExistentialRegionBound, // relating an existential region bound |
62682a34 SL |
35 | } |
36 | ||
a7813a04 XL |
37 | pub trait TypeRelation<'a, 'gcx: 'a+'tcx, 'tcx: 'a> : Sized { |
38 | fn tcx(&self) -> TyCtxt<'a, 'gcx, 'tcx>; | |
c34b1796 AL |
39 | |
40 | /// Returns a static string we can use for printouts. | |
41 | fn tag(&self) -> &'static str; | |
42 | ||
43 | /// Returns true if the value `a` is the "expected" type in the | |
44 | /// relation. Just affects error messages. | |
45 | fn a_is_expected(&self) -> bool; | |
46 | ||
62682a34 SL |
47 | fn with_cause<F,R>(&mut self, _cause: Cause, f: F) -> R |
48 | where F: FnOnce(&mut Self) -> R | |
49 | { | |
50 | f(self) | |
51 | } | |
52 | ||
c34b1796 | 53 | /// Generic relation routine suitable for most anything. |
a7813a04 | 54 | fn relate<T: Relate<'tcx>>(&mut self, a: &T, b: &T) -> RelateResult<'tcx, T> { |
c34b1796 AL |
55 | Relate::relate(self, a, b) |
56 | } | |
57 | ||
cc61c64b XL |
58 | /// Relate the two substitutions for the given item. The default |
59 | /// is to look up the variance for the item and proceed | |
60 | /// accordingly. | |
61 | fn relate_item_substs(&mut self, | |
62 | item_def_id: DefId, | |
63 | a_subst: &'tcx Substs<'tcx>, | |
64 | b_subst: &'tcx Substs<'tcx>) | |
65 | -> RelateResult<'tcx, &'tcx Substs<'tcx>> | |
66 | { | |
67 | debug!("relate_item_substs(item_def_id={:?}, a_subst={:?}, b_subst={:?})", | |
68 | item_def_id, | |
69 | a_subst, | |
70 | b_subst); | |
71 | ||
7cac9316 XL |
72 | let opt_variances = self.tcx().variances_of(item_def_id); |
73 | relate_substs(self, Some(&opt_variances), a_subst, b_subst) | |
cc61c64b XL |
74 | } |
75 | ||
c34b1796 | 76 | /// Switch variance for the purpose of relating `a` and `b`. |
a7813a04 XL |
77 | fn relate_with_variance<T: Relate<'tcx>>(&mut self, |
78 | variance: ty::Variance, | |
79 | a: &T, | |
80 | b: &T) | |
81 | -> RelateResult<'tcx, T>; | |
c34b1796 AL |
82 | |
83 | // Overrideable relations. You shouldn't typically call these | |
84 | // directly, instead call `relate()`, which in turn calls | |
85 | // these. This is both more uniform but also allows us to add | |
86 | // additional hooks for other types in the future if needed | |
87 | // without making older code, which called `relate`, obsolete. | |
88 | ||
89 | fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) | |
90 | -> RelateResult<'tcx, Ty<'tcx>>; | |
91 | ||
7cac9316 XL |
92 | fn regions(&mut self, a: ty::Region<'tcx>, b: ty::Region<'tcx>) |
93 | -> RelateResult<'tcx, ty::Region<'tcx>>; | |
c34b1796 AL |
94 | |
95 | fn binders<T>(&mut self, a: &ty::Binder<T>, b: &ty::Binder<T>) | |
96 | -> RelateResult<'tcx, ty::Binder<T>> | |
a7813a04 | 97 | where T: Relate<'tcx>; |
c34b1796 AL |
98 | } |
99 | ||
a7813a04 XL |
100 | pub trait Relate<'tcx>: TypeFoldable<'tcx> { |
101 | fn relate<'a, 'gcx, R>(relation: &mut R, a: &Self, b: &Self) | |
102 | -> RelateResult<'tcx, Self> | |
103 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a; | |
c34b1796 AL |
104 | } |
105 | ||
106 | /////////////////////////////////////////////////////////////////////////// | |
107 | // Relate impls | |
108 | ||
a7813a04 XL |
109 | impl<'tcx> Relate<'tcx> for ty::TypeAndMut<'tcx> { |
110 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
111 | a: &ty::TypeAndMut<'tcx>, | |
112 | b: &ty::TypeAndMut<'tcx>) | |
113 | -> RelateResult<'tcx, ty::TypeAndMut<'tcx>> | |
114 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 | 115 | { |
62682a34 | 116 | debug!("{}.mts({:?}, {:?})", |
c34b1796 | 117 | relation.tag(), |
62682a34 SL |
118 | a, |
119 | b); | |
c34b1796 | 120 | if a.mutbl != b.mutbl { |
c1a9b12d | 121 | Err(TypeError::Mutability) |
c34b1796 AL |
122 | } else { |
123 | let mutbl = a.mutbl; | |
124 | let variance = match mutbl { | |
7453a54e SL |
125 | ast::Mutability::MutImmutable => ty::Covariant, |
126 | ast::Mutability::MutMutable => ty::Invariant, | |
c34b1796 | 127 | }; |
54a0048b | 128 | let ty = relation.relate_with_variance(variance, &a.ty, &b.ty)?; |
c1a9b12d | 129 | Ok(ty::TypeAndMut {ty: ty, mutbl: mutbl}) |
c34b1796 AL |
130 | } |
131 | } | |
132 | } | |
133 | ||
a7813a04 | 134 | pub fn relate_substs<'a, 'gcx, 'tcx, R>(relation: &mut R, |
9e0c209e | 135 | variances: Option<&Vec<ty::Variance>>, |
a7813a04 XL |
136 | a_subst: &'tcx Substs<'tcx>, |
137 | b_subst: &'tcx Substs<'tcx>) | |
138 | -> RelateResult<'tcx, &'tcx Substs<'tcx>> | |
139 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 | 140 | { |
9e0c209e | 141 | let tcx = relation.tcx(); |
c34b1796 | 142 | |
8bb4bdeb | 143 | let params = a_subst.iter().zip(b_subst).enumerate().map(|(i, (a, b))| { |
9e0c209e | 144 | let variance = variances.map_or(ty::Invariant, |v| v[i]); |
0531ce1d | 145 | relation.relate_with_variance(variance, a, b) |
9e0c209e | 146 | }); |
c34b1796 | 147 | |
c30ab7b3 | 148 | Ok(tcx.mk_substs(params)?) |
c34b1796 AL |
149 | } |
150 | ||
a7813a04 XL |
151 | impl<'tcx> Relate<'tcx> for ty::FnSig<'tcx> { |
152 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
153 | a: &ty::FnSig<'tcx>, | |
154 | b: &ty::FnSig<'tcx>) | |
155 | -> RelateResult<'tcx, ty::FnSig<'tcx>> | |
156 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 | 157 | { |
94b46f34 XL |
158 | let tcx = relation.tcx(); |
159 | ||
c34b1796 | 160 | if a.variadic != b.variadic { |
c1a9b12d | 161 | return Err(TypeError::VariadicMismatch( |
c34b1796 AL |
162 | expected_found(relation, &a.variadic, &b.variadic))); |
163 | } | |
8bb4bdeb XL |
164 | let unsafety = relation.relate(&a.unsafety, &b.unsafety)?; |
165 | let abi = relation.relate(&a.abi, &b.abi)?; | |
c34b1796 | 166 | |
476ff2be SL |
167 | if a.inputs().len() != b.inputs().len() { |
168 | return Err(TypeError::ArgCount); | |
169 | } | |
c34b1796 | 170 | |
476ff2be SL |
171 | let inputs_and_output = a.inputs().iter().cloned() |
172 | .zip(b.inputs().iter().cloned()) | |
173 | .map(|x| (x, false)) | |
174 | .chain(iter::once(((a.output(), b.output()), true))) | |
175 | .map(|((a, b), is_output)| { | |
176 | if is_output { | |
177 | relation.relate(&a, &b) | |
178 | } else { | |
179 | relation.relate_with_variance(ty::Contravariant, &a, &b) | |
180 | } | |
94b46f34 | 181 | }); |
476ff2be | 182 | Ok(ty::FnSig { |
94b46f34 | 183 | inputs_and_output: tcx.mk_type_list(inputs_and_output)?, |
8bb4bdeb | 184 | variadic: a.variadic, |
041b39d2 XL |
185 | unsafety, |
186 | abi, | |
476ff2be | 187 | }) |
c34b1796 | 188 | } |
c34b1796 AL |
189 | } |
190 | ||
a7813a04 XL |
191 | impl<'tcx> Relate<'tcx> for ast::Unsafety { |
192 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
193 | a: &ast::Unsafety, | |
194 | b: &ast::Unsafety) | |
195 | -> RelateResult<'tcx, ast::Unsafety> | |
196 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
197 | { |
198 | if a != b { | |
c1a9b12d | 199 | Err(TypeError::UnsafetyMismatch(expected_found(relation, a, b))) |
c34b1796 AL |
200 | } else { |
201 | Ok(*a) | |
202 | } | |
203 | } | |
204 | } | |
205 | ||
a7813a04 XL |
206 | impl<'tcx> Relate<'tcx> for abi::Abi { |
207 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
208 | a: &abi::Abi, | |
209 | b: &abi::Abi) | |
210 | -> RelateResult<'tcx, abi::Abi> | |
211 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
212 | { |
213 | if a == b { | |
214 | Ok(*a) | |
215 | } else { | |
c1a9b12d | 216 | Err(TypeError::AbiMismatch(expected_found(relation, a, b))) |
c34b1796 AL |
217 | } |
218 | } | |
219 | } | |
220 | ||
a7813a04 XL |
221 | impl<'tcx> Relate<'tcx> for ty::ProjectionTy<'tcx> { |
222 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
223 | a: &ty::ProjectionTy<'tcx>, | |
224 | b: &ty::ProjectionTy<'tcx>) | |
225 | -> RelateResult<'tcx, ty::ProjectionTy<'tcx>> | |
226 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 | 227 | { |
041b39d2 XL |
228 | if a.item_def_id != b.item_def_id { |
229 | Err(TypeError::ProjectionMismatched( | |
230 | expected_found(relation, &a.item_def_id, &b.item_def_id))) | |
c34b1796 | 231 | } else { |
041b39d2 XL |
232 | let substs = relation.relate(&a.substs, &b.substs)?; |
233 | Ok(ty::ProjectionTy { | |
234 | item_def_id: a.item_def_id, | |
235 | substs: &substs, | |
236 | }) | |
c34b1796 AL |
237 | } |
238 | } | |
239 | } | |
240 | ||
9e0c209e | 241 | impl<'tcx> Relate<'tcx> for ty::ExistentialProjection<'tcx> { |
a7813a04 | 242 | fn relate<'a, 'gcx, R>(relation: &mut R, |
9e0c209e SL |
243 | a: &ty::ExistentialProjection<'tcx>, |
244 | b: &ty::ExistentialProjection<'tcx>) | |
245 | -> RelateResult<'tcx, ty::ExistentialProjection<'tcx>> | |
a7813a04 | 246 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a |
c34b1796 | 247 | { |
041b39d2 XL |
248 | if a.item_def_id != b.item_def_id { |
249 | Err(TypeError::ProjectionMismatched( | |
250 | expected_found(relation, &a.item_def_id, &b.item_def_id))) | |
9e0c209e | 251 | } else { |
9e0c209e | 252 | let ty = relation.relate(&a.ty, &b.ty)?; |
041b39d2 | 253 | let substs = relation.relate(&a.substs, &b.substs)?; |
9e0c209e | 254 | Ok(ty::ExistentialProjection { |
041b39d2 | 255 | item_def_id: a.item_def_id, |
3b2f2976 | 256 | substs, |
041b39d2 | 257 | ty, |
9e0c209e SL |
258 | }) |
259 | } | |
c34b1796 AL |
260 | } |
261 | } | |
262 | ||
9e0c209e | 263 | impl<'tcx> Relate<'tcx> for Vec<ty::PolyExistentialProjection<'tcx>> { |
a7813a04 | 264 | fn relate<'a, 'gcx, R>(relation: &mut R, |
9e0c209e SL |
265 | a: &Vec<ty::PolyExistentialProjection<'tcx>>, |
266 | b: &Vec<ty::PolyExistentialProjection<'tcx>>) | |
267 | -> RelateResult<'tcx, Vec<ty::PolyExistentialProjection<'tcx>>> | |
a7813a04 | 268 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a |
c34b1796 AL |
269 | { |
270 | // To be compatible, `a` and `b` must be for precisely the | |
271 | // same set of traits and item names. We always require that | |
272 | // projection bounds lists are sorted by trait-def-id and item-name, | |
273 | // so we can just iterate through the lists pairwise, so long as they are the | |
274 | // same length. | |
275 | if a.len() != b.len() { | |
c1a9b12d | 276 | Err(TypeError::ProjectionBoundsLength(expected_found(relation, &a.len(), &b.len()))) |
c34b1796 | 277 | } else { |
0bf4aa26 XL |
278 | a.iter() |
279 | .zip(b) | |
280 | .map(|(a, b)| relation.relate(a, b)) | |
281 | .collect() | |
c34b1796 AL |
282 | } |
283 | } | |
284 | } | |
285 | ||
a7813a04 XL |
286 | impl<'tcx> Relate<'tcx> for ty::TraitRef<'tcx> { |
287 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
288 | a: &ty::TraitRef<'tcx>, | |
289 | b: &ty::TraitRef<'tcx>) | |
290 | -> RelateResult<'tcx, ty::TraitRef<'tcx>> | |
291 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
292 | { |
293 | // Different traits cannot be related | |
294 | if a.def_id != b.def_id { | |
c1a9b12d | 295 | Err(TypeError::Traits(expected_found(relation, &a.def_id, &b.def_id))) |
c34b1796 | 296 | } else { |
041b39d2 | 297 | let substs = relate_substs(relation, None, a.substs, b.substs)?; |
a7813a04 | 298 | Ok(ty::TraitRef { def_id: a.def_id, substs: substs }) |
c34b1796 AL |
299 | } |
300 | } | |
301 | } | |
302 | ||
9e0c209e SL |
303 | impl<'tcx> Relate<'tcx> for ty::ExistentialTraitRef<'tcx> { |
304 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
305 | a: &ty::ExistentialTraitRef<'tcx>, | |
306 | b: &ty::ExistentialTraitRef<'tcx>) | |
307 | -> RelateResult<'tcx, ty::ExistentialTraitRef<'tcx>> | |
308 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
309 | { | |
310 | // Different traits cannot be related | |
311 | if a.def_id != b.def_id { | |
312 | Err(TypeError::Traits(expected_found(relation, &a.def_id, &b.def_id))) | |
313 | } else { | |
041b39d2 | 314 | let substs = relate_substs(relation, None, a.substs, b.substs)?; |
9e0c209e SL |
315 | Ok(ty::ExistentialTraitRef { def_id: a.def_id, substs: substs }) |
316 | } | |
317 | } | |
318 | } | |
319 | ||
2c00a5a8 | 320 | #[derive(Debug, Clone)] |
b7449926 | 321 | struct GeneratorWitness<'tcx>(&'tcx ty::List<Ty<'tcx>>); |
2c00a5a8 | 322 | |
0531ce1d XL |
323 | TupleStructTypeFoldableImpl! { |
324 | impl<'tcx> TypeFoldable<'tcx> for GeneratorWitness<'tcx> { | |
325 | a | |
2c00a5a8 XL |
326 | } |
327 | } | |
328 | ||
329 | impl<'tcx> Relate<'tcx> for GeneratorWitness<'tcx> { | |
330 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
331 | a: &GeneratorWitness<'tcx>, | |
332 | b: &GeneratorWitness<'tcx>) | |
333 | -> RelateResult<'tcx, GeneratorWitness<'tcx>> | |
334 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
335 | { | |
0bf4aa26 | 336 | assert_eq!(a.0.len(), b.0.len()); |
2c00a5a8 XL |
337 | let tcx = relation.tcx(); |
338 | let types = tcx.mk_type_list(a.0.iter().zip(b.0).map(|(a, b)| relation.relate(a, b)))?; | |
339 | Ok(GeneratorWitness(types)) | |
340 | } | |
341 | } | |
342 | ||
a7813a04 XL |
343 | impl<'tcx> Relate<'tcx> for Ty<'tcx> { |
344 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
345 | a: &Ty<'tcx>, | |
346 | b: &Ty<'tcx>) | |
347 | -> RelateResult<'tcx, Ty<'tcx>> | |
348 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
349 | { |
350 | relation.tys(a, b) | |
351 | } | |
352 | } | |
353 | ||
354 | /// The main "type relation" routine. Note that this does not handle | |
355 | /// inference artifacts, so you should filter those out before calling | |
356 | /// it. | |
a7813a04 XL |
357 | pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R, |
358 | a: Ty<'tcx>, | |
359 | b: Ty<'tcx>) | |
360 | -> RelateResult<'tcx, Ty<'tcx>> | |
361 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
362 | { |
363 | let tcx = relation.tcx(); | |
364 | let a_sty = &a.sty; | |
365 | let b_sty = &b.sty; | |
0bf4aa26 | 366 | debug!("super_relate_tys: a_sty={:?} b_sty={:?}", a_sty, b_sty); |
c34b1796 | 367 | match (a_sty, b_sty) { |
b7449926 XL |
368 | (&ty::Infer(_), _) | |
369 | (_, &ty::Infer(_)) => | |
c34b1796 AL |
370 | { |
371 | // The caller should handle these cases! | |
54a0048b | 372 | bug!("var types encountered in super_relate_tys") |
c34b1796 AL |
373 | } |
374 | ||
a1dfa0c6 XL |
375 | (ty::Bound(..), _) | (_, ty::Bound(..)) => { |
376 | bug!("bound types encountered in super_relate_tys") | |
377 | } | |
378 | ||
b7449926 | 379 | (&ty::Error, _) | (_, &ty::Error) => |
c34b1796 AL |
380 | { |
381 | Ok(tcx.types.err) | |
382 | } | |
383 | ||
b7449926 XL |
384 | (&ty::Never, _) | |
385 | (&ty::Char, _) | | |
386 | (&ty::Bool, _) | | |
387 | (&ty::Int(_), _) | | |
388 | (&ty::Uint(_), _) | | |
389 | (&ty::Float(_), _) | | |
390 | (&ty::Str, _) | |
c34b1796 AL |
391 | if a == b => |
392 | { | |
393 | Ok(a) | |
394 | } | |
395 | ||
b7449926 | 396 | (&ty::Param(ref a_p), &ty::Param(ref b_p)) |
9e0c209e | 397 | if a_p.idx == b_p.idx => |
c34b1796 AL |
398 | { |
399 | Ok(a) | |
400 | } | |
401 | ||
a1dfa0c6 XL |
402 | (ty::Placeholder(p1), ty::Placeholder(p2)) if p1 == p2 => { |
403 | Ok(a) | |
404 | } | |
405 | ||
b7449926 | 406 | (&ty::Adt(a_def, a_substs), &ty::Adt(b_def, b_substs)) |
e9174d1e | 407 | if a_def == b_def => |
c34b1796 | 408 | { |
cc61c64b | 409 | let substs = relation.relate_item_substs(a_def.did, a_substs, b_substs)?; |
9e0c209e | 410 | Ok(tcx.mk_adt(a_def, substs)) |
c34b1796 AL |
411 | } |
412 | ||
b7449926 | 413 | (&ty::Foreign(a_id), &ty::Foreign(b_id)) |
abe05a73 XL |
414 | if a_id == b_id => |
415 | { | |
416 | Ok(tcx.mk_foreign(a_id)) | |
417 | } | |
418 | ||
b7449926 | 419 | (&ty::Dynamic(ref a_obj, ref a_region), &ty::Dynamic(ref b_obj, ref b_region)) => { |
476ff2be SL |
420 | let region_bound = relation.with_cause(Cause::ExistentialRegionBound, |
421 | |relation| { | |
422 | relation.relate_with_variance( | |
423 | ty::Contravariant, | |
424 | a_region, | |
425 | b_region) | |
426 | })?; | |
427 | Ok(tcx.mk_dynamic(relation.relate(a_obj, b_obj)?, region_bound)) | |
c34b1796 AL |
428 | } |
429 | ||
b7449926 XL |
430 | (&ty::Generator(a_id, a_substs, movability), |
431 | &ty::Generator(b_id, b_substs, _)) | |
ea8adc8c XL |
432 | if a_id == b_id => |
433 | { | |
b7449926 | 434 | // All Generator types with the same id represent |
ea8adc8c XL |
435 | // the (anonymous) type of the same generator expression. So |
436 | // all of their regions should be equated. | |
437 | let substs = relation.relate(&a_substs, &b_substs)?; | |
94b46f34 | 438 | Ok(tcx.mk_generator(a_id, substs, movability)) |
ea8adc8c XL |
439 | } |
440 | ||
b7449926 | 441 | (&ty::GeneratorWitness(a_types), &ty::GeneratorWitness(b_types)) => |
2c00a5a8 XL |
442 | { |
443 | // Wrap our types with a temporary GeneratorWitness struct | |
444 | // inside the binder so we can related them | |
83c7162d XL |
445 | let a_types = a_types.map_bound(GeneratorWitness); |
446 | let b_types = b_types.map_bound(GeneratorWitness); | |
2c00a5a8 | 447 | // Then remove the GeneratorWitness for the result |
83c7162d | 448 | let types = relation.relate(&a_types, &b_types)?.map_bound(|witness| witness.0); |
2c00a5a8 XL |
449 | Ok(tcx.mk_generator_witness(types)) |
450 | } | |
451 | ||
b7449926 XL |
452 | (&ty::Closure(a_id, a_substs), |
453 | &ty::Closure(b_id, b_substs)) | |
c34b1796 AL |
454 | if a_id == b_id => |
455 | { | |
b7449926 | 456 | // All Closure types with the same id represent |
c34b1796 AL |
457 | // the (anonymous) type of the same closure expression. So |
458 | // all of their regions should be equated. | |
a7813a04 | 459 | let substs = relation.relate(&a_substs, &b_substs)?; |
94b46f34 | 460 | Ok(tcx.mk_closure(a_id, substs)) |
c34b1796 AL |
461 | } |
462 | ||
b7449926 | 463 | (&ty::RawPtr(ref a_mt), &ty::RawPtr(ref b_mt)) => |
c34b1796 | 464 | { |
54a0048b | 465 | let mt = relation.relate(a_mt, b_mt)?; |
c1a9b12d | 466 | Ok(tcx.mk_ptr(mt)) |
c34b1796 AL |
467 | } |
468 | ||
b7449926 | 469 | (&ty::Ref(a_r, a_ty, a_mutbl), &ty::Ref(b_r, b_ty, b_mutbl)) => |
c34b1796 | 470 | { |
9e0c209e | 471 | let r = relation.relate_with_variance(ty::Contravariant, &a_r, &b_r)?; |
94b46f34 XL |
472 | let a_mt = ty::TypeAndMut { ty: a_ty, mutbl: a_mutbl }; |
473 | let b_mt = ty::TypeAndMut { ty: b_ty, mutbl: b_mutbl }; | |
474 | let mt = relation.relate(&a_mt, &b_mt)?; | |
9e0c209e | 475 | Ok(tcx.mk_ref(r, mt)) |
c34b1796 AL |
476 | } |
477 | ||
b7449926 | 478 | (&ty::Array(a_t, sz_a), &ty::Array(b_t, sz_b)) => |
c34b1796 | 479 | { |
54a0048b | 480 | let t = relation.relate(&a_t, &b_t)?; |
ea8adc8c XL |
481 | assert_eq!(sz_a.ty, tcx.types.usize); |
482 | assert_eq!(sz_b.ty, tcx.types.usize); | |
483 | let to_u64 = |x: &'tcx ty::Const<'tcx>| -> Result<u64, ErrorReported> { | |
94b46f34 XL |
484 | if let Some(s) = x.assert_usize(tcx) { |
485 | return Ok(s); | |
486 | } | |
ea8adc8c | 487 | match x.val { |
8faf50e0 | 488 | ConstValue::Unevaluated(def_id, substs) => { |
ea8adc8c | 489 | // FIXME(eddyb) get the right param_env. |
0531ce1d | 490 | let param_env = ty::ParamEnv::empty(); |
0bf4aa26 XL |
491 | if let Some(substs) = tcx.lift_to_global(&substs) { |
492 | let instance = ty::Instance::resolve( | |
493 | tcx.global_tcx(), | |
494 | param_env, | |
495 | def_id, | |
496 | substs, | |
497 | ); | |
498 | if let Some(instance) = instance { | |
499 | let cid = GlobalId { | |
500 | instance, | |
501 | promoted: None | |
502 | }; | |
503 | if let Some(s) = tcx.const_eval(param_env.and(cid)) | |
504 | .ok() | |
505 | .map(|c| c.unwrap_usize(tcx)) { | |
506 | return Ok(s) | |
ea8adc8c | 507 | } |
0bf4aa26 | 508 | } |
ea8adc8c XL |
509 | } |
510 | tcx.sess.delay_span_bug(tcx.def_span(def_id), | |
511 | "array length could not be evaluated"); | |
512 | Err(ErrorReported) | |
513 | } | |
8faf50e0 XL |
514 | _ => { |
515 | tcx.sess.delay_span_bug(DUMMY_SP, | |
516 | &format!("arrays should not have {:?} as length", x)); | |
517 | Err(ErrorReported) | |
518 | } | |
ea8adc8c XL |
519 | } |
520 | }; | |
521 | match (to_u64(sz_a), to_u64(sz_b)) { | |
522 | (Ok(sz_a_u64), Ok(sz_b_u64)) => { | |
523 | if sz_a_u64 == sz_b_u64 { | |
b7449926 | 524 | Ok(tcx.mk_ty(ty::Array(t, sz_a))) |
ea8adc8c XL |
525 | } else { |
526 | Err(TypeError::FixedArraySize( | |
527 | expected_found(relation, &sz_a_u64, &sz_b_u64))) | |
528 | } | |
529 | } | |
b7449926 | 530 | // We reported an error or will ICE, so we can return Error. |
ea8adc8c XL |
531 | (Err(ErrorReported), _) | (_, Err(ErrorReported)) => { |
532 | Ok(tcx.types.err) | |
533 | } | |
c34b1796 AL |
534 | } |
535 | } | |
536 | ||
b7449926 | 537 | (&ty::Slice(a_t), &ty::Slice(b_t)) => |
c34b1796 | 538 | { |
54a0048b | 539 | let t = relation.relate(&a_t, &b_t)?; |
c1a9b12d | 540 | Ok(tcx.mk_slice(t)) |
c34b1796 AL |
541 | } |
542 | ||
b7449926 | 543 | (&ty::Tuple(as_), &ty::Tuple(bs)) => |
c34b1796 AL |
544 | { |
545 | if as_.len() == bs.len() { | |
0531ce1d | 546 | Ok(tcx.mk_tup(as_.iter().zip(bs).map(|(a, b)| relation.relate(a, b)))?) |
9346a6ac | 547 | } else if !(as_.is_empty() || bs.is_empty()) { |
c1a9b12d | 548 | Err(TypeError::TupleSize( |
c34b1796 AL |
549 | expected_found(relation, &as_.len(), &bs.len()))) |
550 | } else { | |
c1a9b12d | 551 | Err(TypeError::Sorts(expected_found(relation, &a, &b))) |
c34b1796 AL |
552 | } |
553 | } | |
554 | ||
b7449926 | 555 | (&ty::FnDef(a_def_id, a_substs), &ty::FnDef(b_def_id, b_substs)) |
54a0048b SL |
556 | if a_def_id == b_def_id => |
557 | { | |
041b39d2 XL |
558 | let substs = relation.relate_item_substs(a_def_id, a_substs, b_substs)?; |
559 | Ok(tcx.mk_fn_def(a_def_id, substs)) | |
54a0048b SL |
560 | } |
561 | ||
b7449926 | 562 | (&ty::FnPtr(a_fty), &ty::FnPtr(b_fty)) => |
c34b1796 | 563 | { |
a7813a04 | 564 | let fty = relation.relate(&a_fty, &b_fty)?; |
54a0048b | 565 | Ok(tcx.mk_fn_ptr(fty)) |
c34b1796 AL |
566 | } |
567 | ||
a1dfa0c6 XL |
568 | (ty::UnnormalizedProjection(a_data), ty::UnnormalizedProjection(b_data)) => { |
569 | let projection_ty = relation.relate(a_data, b_data)?; | |
570 | Ok(tcx.mk_ty(ty::UnnormalizedProjection(projection_ty))) | |
571 | } | |
572 | ||
573 | // these two are already handled downstream in case of lazy normalization | |
574 | (ty::Projection(a_data), ty::Projection(b_data)) => { | |
54a0048b | 575 | let projection_ty = relation.relate(a_data, b_data)?; |
041b39d2 | 576 | Ok(tcx.mk_projection(projection_ty.item_def_id, projection_ty.substs)) |
c34b1796 AL |
577 | } |
578 | ||
b7449926 | 579 | (&ty::Opaque(a_def_id, a_substs), &ty::Opaque(b_def_id, b_substs)) |
5bcae85e SL |
580 | if a_def_id == b_def_id => |
581 | { | |
582 | let substs = relate_substs(relation, None, a_substs, b_substs)?; | |
b7449926 | 583 | Ok(tcx.mk_opaque(a_def_id, substs)) |
5bcae85e SL |
584 | } |
585 | ||
c34b1796 AL |
586 | _ => |
587 | { | |
c1a9b12d | 588 | Err(TypeError::Sorts(expected_found(relation, &a, &b))) |
c34b1796 AL |
589 | } |
590 | } | |
591 | } | |
592 | ||
b7449926 | 593 | impl<'tcx> Relate<'tcx> for &'tcx ty::List<ty::ExistentialPredicate<'tcx>> { |
476ff2be SL |
594 | fn relate<'a, 'gcx, R>(relation: &mut R, |
595 | a: &Self, | |
596 | b: &Self) | |
597 | -> RelateResult<'tcx, Self> | |
598 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a { | |
599 | ||
600 | if a.len() != b.len() { | |
601 | return Err(TypeError::ExistentialMismatch(expected_found(relation, a, b))); | |
602 | } | |
603 | ||
604 | let tcx = relation.tcx(); | |
605 | let v = a.iter().zip(b.iter()).map(|(ep_a, ep_b)| { | |
606 | use ty::ExistentialPredicate::*; | |
607 | match (*ep_a, *ep_b) { | |
608 | (Trait(ref a), Trait(ref b)) => Ok(Trait(relation.relate(a, b)?)), | |
609 | (Projection(ref a), Projection(ref b)) => Ok(Projection(relation.relate(a, b)?)), | |
610 | (AutoTrait(ref a), AutoTrait(ref b)) if a == b => Ok(AutoTrait(*a)), | |
611 | _ => Err(TypeError::ExistentialMismatch(expected_found(relation, a, b))) | |
612 | } | |
613 | }); | |
614 | Ok(tcx.mk_existential_predicates(v)?) | |
615 | } | |
616 | } | |
617 | ||
a7813a04 XL |
618 | impl<'tcx> Relate<'tcx> for ty::ClosureSubsts<'tcx> { |
619 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
620 | a: &ty::ClosureSubsts<'tcx>, | |
621 | b: &ty::ClosureSubsts<'tcx>) | |
622 | -> RelateResult<'tcx, ty::ClosureSubsts<'tcx>> | |
623 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c1a9b12d | 624 | { |
476ff2be | 625 | let substs = relate_substs(relation, None, a.substs, b.substs)?; |
94b46f34 | 626 | Ok(ty::ClosureSubsts { substs }) |
c1a9b12d SL |
627 | } |
628 | } | |
629 | ||
94b46f34 | 630 | impl<'tcx> Relate<'tcx> for ty::GeneratorSubsts<'tcx> { |
ea8adc8c | 631 | fn relate<'a, 'gcx, R>(relation: &mut R, |
94b46f34 XL |
632 | a: &ty::GeneratorSubsts<'tcx>, |
633 | b: &ty::GeneratorSubsts<'tcx>) | |
634 | -> RelateResult<'tcx, ty::GeneratorSubsts<'tcx>> | |
ea8adc8c XL |
635 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a |
636 | { | |
94b46f34 XL |
637 | let substs = relate_substs(relation, None, a.substs, b.substs)?; |
638 | Ok(ty::GeneratorSubsts { substs }) | |
ea8adc8c XL |
639 | } |
640 | } | |
641 | ||
a7813a04 XL |
642 | impl<'tcx> Relate<'tcx> for &'tcx Substs<'tcx> { |
643 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
644 | a: &&'tcx Substs<'tcx>, | |
645 | b: &&'tcx Substs<'tcx>) | |
646 | -> RelateResult<'tcx, &'tcx Substs<'tcx>> | |
647 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
54a0048b SL |
648 | { |
649 | relate_substs(relation, None, a, b) | |
650 | } | |
651 | } | |
652 | ||
7cac9316 | 653 | impl<'tcx> Relate<'tcx> for ty::Region<'tcx> { |
a7813a04 | 654 | fn relate<'a, 'gcx, R>(relation: &mut R, |
7cac9316 XL |
655 | a: &ty::Region<'tcx>, |
656 | b: &ty::Region<'tcx>) | |
657 | -> RelateResult<'tcx, ty::Region<'tcx>> | |
a7813a04 | 658 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a |
c34b1796 AL |
659 | { |
660 | relation.regions(*a, *b) | |
661 | } | |
662 | } | |
663 | ||
a7813a04 XL |
664 | impl<'tcx, T: Relate<'tcx>> Relate<'tcx> for ty::Binder<T> { |
665 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
666 | a: &ty::Binder<T>, | |
667 | b: &ty::Binder<T>) | |
668 | -> RelateResult<'tcx, ty::Binder<T>> | |
669 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
670 | { |
671 | relation.binders(a, b) | |
672 | } | |
673 | } | |
674 | ||
a7813a04 XL |
675 | impl<'tcx, T: Relate<'tcx>> Relate<'tcx> for Rc<T> { |
676 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
677 | a: &Rc<T>, | |
678 | b: &Rc<T>) | |
679 | -> RelateResult<'tcx, Rc<T>> | |
680 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
681 | { |
682 | let a: &T = a; | |
683 | let b: &T = b; | |
54a0048b | 684 | Ok(Rc::new(relation.relate(a, b)?)) |
c34b1796 AL |
685 | } |
686 | } | |
687 | ||
a7813a04 XL |
688 | impl<'tcx, T: Relate<'tcx>> Relate<'tcx> for Box<T> { |
689 | fn relate<'a, 'gcx, R>(relation: &mut R, | |
690 | a: &Box<T>, | |
691 | b: &Box<T>) | |
692 | -> RelateResult<'tcx, Box<T>> | |
693 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
694 | { |
695 | let a: &T = a; | |
696 | let b: &T = b; | |
54a0048b | 697 | Ok(Box::new(relation.relate(a, b)?)) |
c34b1796 AL |
698 | } |
699 | } | |
700 | ||
0531ce1d XL |
701 | impl<'tcx> Relate<'tcx> for Kind<'tcx> { |
702 | fn relate<'a, 'gcx, R>( | |
703 | relation: &mut R, | |
704 | a: &Kind<'tcx>, | |
705 | b: &Kind<'tcx> | |
706 | ) -> RelateResult<'tcx, Kind<'tcx>> | |
707 | where | |
708 | R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'a+'tcx, 'tcx: 'a, | |
709 | { | |
710 | match (a.unpack(), b.unpack()) { | |
711 | (UnpackedKind::Lifetime(a_lt), UnpackedKind::Lifetime(b_lt)) => { | |
712 | Ok(relation.relate(&a_lt, &b_lt)?.into()) | |
713 | } | |
714 | (UnpackedKind::Type(a_ty), UnpackedKind::Type(b_ty)) => { | |
715 | Ok(relation.relate(&a_ty, &b_ty)?.into()) | |
716 | } | |
0bf4aa26 XL |
717 | (UnpackedKind::Lifetime(unpacked), x) => { |
718 | bug!("impossible case reached: can't relate: {:?} with {:?}", unpacked, x) | |
719 | } | |
720 | (UnpackedKind::Type(unpacked), x) => { | |
721 | bug!("impossible case reached: can't relate: {:?} with {:?}", unpacked, x) | |
722 | } | |
0531ce1d XL |
723 | } |
724 | } | |
725 | } | |
726 | ||
a1dfa0c6 XL |
727 | impl<'tcx> Relate<'tcx> for ty::TraitPredicate<'tcx> { |
728 | fn relate<'a, 'gcx, R>( | |
729 | relation: &mut R, | |
730 | a: &ty::TraitPredicate<'tcx>, | |
731 | b: &ty::TraitPredicate<'tcx> | |
732 | ) -> RelateResult<'tcx, ty::TraitPredicate<'tcx>> | |
733 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
734 | { | |
735 | Ok(ty::TraitPredicate { | |
736 | trait_ref: relation.relate(&a.trait_ref, &b.trait_ref)?, | |
737 | }) | |
738 | } | |
739 | } | |
740 | ||
741 | impl<'tcx> Relate<'tcx> for ty::ProjectionPredicate<'tcx> { | |
742 | fn relate<'a, 'gcx, R>( | |
743 | relation: &mut R, | |
744 | a: &ty::ProjectionPredicate<'tcx>, | |
745 | b: &ty::ProjectionPredicate<'tcx>, | |
746 | ) -> RelateResult<'tcx, ty::ProjectionPredicate<'tcx>> | |
747 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
748 | { | |
749 | Ok(ty::ProjectionPredicate { | |
750 | projection_ty: relation.relate(&a.projection_ty, &b.projection_ty)?, | |
751 | ty: relation.relate(&a.ty, &b.ty)?, | |
752 | }) | |
753 | } | |
754 | } | |
755 | ||
756 | impl<'tcx> Relate<'tcx> for traits::WhereClause<'tcx> { | |
757 | fn relate<'a, 'gcx, R>( | |
758 | relation: &mut R, | |
759 | a: &traits::WhereClause<'tcx>, | |
760 | b: &traits::WhereClause<'tcx> | |
761 | ) -> RelateResult<'tcx, traits::WhereClause<'tcx>> | |
762 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
763 | { | |
764 | use traits::WhereClause::*; | |
765 | match (a, b) { | |
766 | (Implemented(a_pred), Implemented(b_pred)) => { | |
767 | Ok(Implemented(relation.relate(a_pred, b_pred)?)) | |
768 | } | |
769 | ||
770 | (ProjectionEq(a_pred), ProjectionEq(b_pred)) => { | |
771 | Ok(ProjectionEq(relation.relate(a_pred, b_pred)?)) | |
772 | } | |
773 | ||
774 | (RegionOutlives(a_pred), RegionOutlives(b_pred)) => { | |
775 | Ok(RegionOutlives(ty::OutlivesPredicate( | |
776 | relation.relate(&a_pred.0, &b_pred.0)?, | |
777 | relation.relate(&a_pred.1, &b_pred.1)?, | |
778 | ))) | |
779 | } | |
780 | ||
781 | (TypeOutlives(a_pred), TypeOutlives(b_pred)) => { | |
782 | Ok(TypeOutlives(ty::OutlivesPredicate( | |
783 | relation.relate(&a_pred.0, &b_pred.0)?, | |
784 | relation.relate(&a_pred.1, &b_pred.1)?, | |
785 | ))) | |
786 | } | |
787 | ||
788 | _ => Err(TypeError::Mismatch), | |
789 | } | |
790 | } | |
791 | } | |
792 | ||
793 | impl<'tcx> Relate<'tcx> for traits::WellFormed<'tcx> { | |
794 | fn relate<'a, 'gcx, R>( | |
795 | relation: &mut R, | |
796 | a: &traits::WellFormed<'tcx>, | |
797 | b: &traits::WellFormed<'tcx> | |
798 | ) -> RelateResult<'tcx, traits::WellFormed<'tcx>> | |
799 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
800 | { | |
801 | use traits::WellFormed::*; | |
802 | match (a, b) { | |
803 | (Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)), | |
804 | (Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)), | |
805 | _ => Err(TypeError::Mismatch), | |
806 | } | |
807 | } | |
808 | } | |
809 | ||
810 | impl<'tcx> Relate<'tcx> for traits::FromEnv<'tcx> { | |
811 | fn relate<'a, 'gcx, R>( | |
812 | relation: &mut R, | |
813 | a: &traits::FromEnv<'tcx>, | |
814 | b: &traits::FromEnv<'tcx> | |
815 | ) -> RelateResult<'tcx, traits::FromEnv<'tcx>> | |
816 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
817 | { | |
818 | use traits::FromEnv::*; | |
819 | match (a, b) { | |
820 | (Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)), | |
821 | (Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)), | |
822 | _ => Err(TypeError::Mismatch), | |
823 | } | |
824 | } | |
825 | } | |
826 | ||
827 | impl<'tcx> Relate<'tcx> for traits::DomainGoal<'tcx> { | |
828 | fn relate<'a, 'gcx, R>( | |
829 | relation: &mut R, | |
830 | a: &traits::DomainGoal<'tcx>, | |
831 | b: &traits::DomainGoal<'tcx> | |
832 | ) -> RelateResult<'tcx, traits::DomainGoal<'tcx>> | |
833 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
834 | { | |
835 | use traits::DomainGoal::*; | |
836 | match (a, b) { | |
837 | (Holds(a_wc), Holds(b_wc)) => Ok(Holds(relation.relate(a_wc, b_wc)?)), | |
838 | (WellFormed(a_wf), WellFormed(b_wf)) => Ok(WellFormed(relation.relate(a_wf, b_wf)?)), | |
839 | (FromEnv(a_fe), FromEnv(b_fe)) => Ok(FromEnv(relation.relate(a_fe, b_fe)?)), | |
840 | ||
841 | (Normalize(a_pred), Normalize(b_pred)) => { | |
842 | Ok(Normalize(relation.relate(a_pred, b_pred)?)) | |
843 | } | |
844 | ||
845 | _ => Err(TypeError::Mismatch), | |
846 | } | |
847 | } | |
848 | } | |
849 | ||
850 | impl<'tcx> Relate<'tcx> for traits::Goal<'tcx> { | |
851 | fn relate<'a, 'gcx, R>( | |
852 | relation: &mut R, | |
853 | a: &traits::Goal<'tcx>, | |
854 | b: &traits::Goal<'tcx> | |
855 | ) -> RelateResult<'tcx, traits::Goal<'tcx>> | |
856 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
857 | { | |
858 | use traits::GoalKind::*; | |
859 | match (a, b) { | |
860 | (Implies(a_clauses, a_goal), Implies(b_clauses, b_goal)) => { | |
861 | let clauses = relation.relate(a_clauses, b_clauses)?; | |
862 | let goal = relation.relate(a_goal, b_goal)?; | |
863 | Ok(relation.tcx().mk_goal(Implies(clauses, goal))) | |
864 | } | |
865 | ||
866 | (And(a_left, a_right), And(b_left, b_right)) => { | |
867 | let left = relation.relate(a_left, b_left)?; | |
868 | let right = relation.relate(a_right, b_right)?; | |
869 | Ok(relation.tcx().mk_goal(And(left, right))) | |
870 | } | |
871 | ||
872 | (Not(a_goal), Not(b_goal)) => { | |
873 | let goal = relation.relate(a_goal, b_goal)?; | |
874 | Ok(relation.tcx().mk_goal(Not(goal))) | |
875 | } | |
876 | ||
877 | (DomainGoal(a_goal), DomainGoal(b_goal)) => { | |
878 | let goal = relation.relate(a_goal, b_goal)?; | |
879 | Ok(relation.tcx().mk_goal(DomainGoal(goal))) | |
880 | } | |
881 | ||
882 | (Quantified(a_qkind, a_goal), Quantified(b_qkind, b_goal)) | |
883 | if a_qkind == b_qkind => | |
884 | { | |
885 | let goal = relation.relate(a_goal, b_goal)?; | |
886 | Ok(relation.tcx().mk_goal(Quantified(*a_qkind, goal))) | |
887 | } | |
888 | ||
889 | (CannotProve, CannotProve) => Ok(*a), | |
890 | ||
891 | _ => Err(TypeError::Mismatch), | |
892 | } | |
893 | } | |
894 | } | |
895 | ||
896 | impl<'tcx> Relate<'tcx> for traits::Goals<'tcx> { | |
897 | fn relate<'a, 'gcx, R>( | |
898 | relation: &mut R, | |
899 | a: &traits::Goals<'tcx>, | |
900 | b: &traits::Goals<'tcx> | |
901 | ) -> RelateResult<'tcx, traits::Goals<'tcx>> | |
902 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
903 | { | |
904 | if a.len() != b.len() { | |
905 | return Err(TypeError::Mismatch); | |
906 | } | |
907 | ||
908 | let tcx = relation.tcx(); | |
909 | let goals = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b)); | |
910 | Ok(tcx.mk_goals(goals)?) | |
911 | } | |
912 | } | |
913 | ||
914 | impl<'tcx> Relate<'tcx> for traits::Clause<'tcx> { | |
915 | fn relate<'a, 'gcx, R>( | |
916 | relation: &mut R, | |
917 | a: &traits::Clause<'tcx>, | |
918 | b: &traits::Clause<'tcx> | |
919 | ) -> RelateResult<'tcx, traits::Clause<'tcx>> | |
920 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
921 | { | |
922 | use traits::Clause::*; | |
923 | match (a, b) { | |
924 | (Implies(a_clause), Implies(b_clause)) => { | |
925 | let clause = relation.relate(a_clause, b_clause)?; | |
926 | Ok(Implies(clause)) | |
927 | } | |
928 | ||
929 | (ForAll(a_clause), ForAll(b_clause)) => { | |
930 | let clause = relation.relate(a_clause, b_clause)?; | |
931 | Ok(ForAll(clause)) | |
932 | } | |
933 | ||
934 | _ => Err(TypeError::Mismatch), | |
935 | } | |
936 | } | |
937 | } | |
938 | ||
939 | impl<'tcx> Relate<'tcx> for traits::Clauses<'tcx> { | |
940 | fn relate<'a, 'gcx, R>( | |
941 | relation: &mut R, | |
942 | a: &traits::Clauses<'tcx>, | |
943 | b: &traits::Clauses<'tcx> | |
944 | ) -> RelateResult<'tcx, traits::Clauses<'tcx>> | |
945 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
946 | { | |
947 | if a.len() != b.len() { | |
948 | return Err(TypeError::Mismatch); | |
949 | } | |
950 | ||
951 | let tcx = relation.tcx(); | |
952 | let clauses = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b)); | |
953 | Ok(tcx.mk_clauses(clauses)?) | |
954 | } | |
955 | } | |
956 | ||
957 | impl<'tcx> Relate<'tcx> for traits::ProgramClause<'tcx> { | |
958 | fn relate<'a, 'gcx, R>( | |
959 | relation: &mut R, | |
960 | a: &traits::ProgramClause<'tcx>, | |
961 | b: &traits::ProgramClause<'tcx> | |
962 | ) -> RelateResult<'tcx, traits::ProgramClause<'tcx>> | |
963 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
964 | { | |
965 | Ok(traits::ProgramClause { | |
966 | goal: relation.relate(&a.goal, &b.goal)?, | |
967 | hypotheses: relation.relate(&a.hypotheses, &b.hypotheses)?, | |
968 | category: traits::ProgramClauseCategory::Other, | |
969 | }) | |
970 | } | |
971 | } | |
972 | ||
973 | impl<'tcx> Relate<'tcx> for traits::Environment<'tcx> { | |
974 | fn relate<'a, 'gcx, R>( | |
975 | relation: &mut R, | |
976 | a: &traits::Environment<'tcx>, | |
977 | b: &traits::Environment<'tcx> | |
978 | ) -> RelateResult<'tcx, traits::Environment<'tcx>> | |
979 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
980 | { | |
981 | Ok(traits::Environment { | |
982 | clauses: relation.relate(&a.clauses, &b.clauses)?, | |
983 | }) | |
984 | } | |
985 | } | |
986 | ||
987 | impl<'tcx, G> Relate<'tcx> for traits::InEnvironment<'tcx, G> | |
988 | where G: Relate<'tcx> | |
989 | { | |
990 | fn relate<'a, 'gcx, R>( | |
991 | relation: &mut R, | |
992 | a: &traits::InEnvironment<'tcx, G>, | |
993 | b: &traits::InEnvironment<'tcx, G> | |
994 | ) -> RelateResult<'tcx, traits::InEnvironment<'tcx, G>> | |
995 | where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a | |
996 | { | |
997 | Ok(traits::InEnvironment { | |
998 | environment: relation.relate(&a.environment, &b.environment)?, | |
999 | goal: relation.relate(&a.goal, &b.goal)?, | |
1000 | }) | |
1001 | } | |
1002 | } | |
1003 | ||
c34b1796 AL |
1004 | /////////////////////////////////////////////////////////////////////////// |
1005 | // Error handling | |
1006 | ||
a7813a04 XL |
1007 | pub fn expected_found<'a, 'gcx, 'tcx, R, T>(relation: &mut R, |
1008 | a: &T, | |
1009 | b: &T) | |
1010 | -> ExpectedFound<T> | |
1011 | where R: TypeRelation<'a, 'gcx, 'tcx>, T: Clone, 'gcx: 'a+'tcx, 'tcx: 'a | |
c34b1796 AL |
1012 | { |
1013 | expected_found_bool(relation.a_is_expected(), a, b) | |
1014 | } | |
1015 | ||
1016 | pub fn expected_found_bool<T>(a_is_expected: bool, | |
1017 | a: &T, | |
1018 | b: &T) | |
e9174d1e | 1019 | -> ExpectedFound<T> |
c34b1796 AL |
1020 | where T: Clone |
1021 | { | |
1022 | let a = a.clone(); | |
1023 | let b = b.clone(); | |
1024 | if a_is_expected { | |
e9174d1e | 1025 | ExpectedFound {expected: a, found: b} |
c34b1796 | 1026 | } else { |
e9174d1e | 1027 | ExpectedFound {expected: b, found: a} |
c34b1796 AL |
1028 | } |
1029 | } |