diff options
author | Seivan Heidari <[email protected]> | 2019-12-23 14:35:31 +0000 |
---|---|---|
committer | Seivan Heidari <[email protected]> | 2019-12-23 14:35:31 +0000 |
commit | b21d9337d9200e2cfdc90b386591c72c302dc03e (patch) | |
tree | f81f5c08f821115cee26fa4d3ceaae88c7807fd5 /crates/ra_hir_ty/src/infer/unify.rs | |
parent | 18a0937585b836ec5ed054b9ae48e0156ab6d9ef (diff) | |
parent | ce07a2daa9e53aa86a769f8641b14c2878444fbc (diff) |
Merge branch 'master' into feature/themes
Diffstat (limited to 'crates/ra_hir_ty/src/infer/unify.rs')
-rw-r--r-- | crates/ra_hir_ty/src/infer/unify.rs | 276 |
1 files changed, 270 insertions, 6 deletions
diff --git a/crates/ra_hir_ty/src/infer/unify.rs b/crates/ra_hir_ty/src/infer/unify.rs index f3a875678..fe05642ae 100644 --- a/crates/ra_hir_ty/src/infer/unify.rs +++ b/crates/ra_hir_ty/src/infer/unify.rs | |||
@@ -1,9 +1,15 @@ | |||
1 | //! Unification and canonicalization logic. | 1 | //! Unification and canonicalization logic. |
2 | 2 | ||
3 | use std::borrow::Cow; | ||
4 | |||
5 | use ena::unify::{InPlaceUnificationTable, NoError, UnifyKey, UnifyValue}; | ||
6 | |||
7 | use test_utils::tested_by; | ||
8 | |||
3 | use super::{InferenceContext, Obligation}; | 9 | use super::{InferenceContext, Obligation}; |
4 | use crate::{ | 10 | use crate::{ |
5 | db::HirDatabase, utils::make_mut_slice, Canonical, InEnvironment, InferTy, ProjectionPredicate, | 11 | db::HirDatabase, utils::make_mut_slice, Canonical, InEnvironment, InferTy, ProjectionPredicate, |
6 | ProjectionTy, Substs, TraitRef, Ty, TypeWalk, | 12 | ProjectionTy, Substs, TraitRef, Ty, TypeCtor, TypeWalk, |
7 | }; | 13 | }; |
8 | 14 | ||
9 | impl<'a, D: HirDatabase> InferenceContext<'a, D> { | 15 | impl<'a, D: HirDatabase> InferenceContext<'a, D> { |
@@ -24,7 +30,7 @@ where | |||
24 | /// A stack of type variables that is used to detect recursive types (which | 30 | /// A stack of type variables that is used to detect recursive types (which |
25 | /// are an error, but we need to protect against them to avoid stack | 31 | /// are an error, but we need to protect against them to avoid stack |
26 | /// overflows). | 32 | /// overflows). |
27 | var_stack: Vec<super::TypeVarId>, | 33 | var_stack: Vec<TypeVarId>, |
28 | } | 34 | } |
29 | 35 | ||
30 | pub(super) struct Canonicalized<T> { | 36 | pub(super) struct Canonicalized<T> { |
@@ -53,14 +59,14 @@ where | |||
53 | return tv.fallback_value(); | 59 | return tv.fallback_value(); |
54 | } | 60 | } |
55 | if let Some(known_ty) = | 61 | if let Some(known_ty) = |
56 | self.ctx.var_unification_table.inlined_probe_value(inner).known() | 62 | self.ctx.table.var_unification_table.inlined_probe_value(inner).known() |
57 | { | 63 | { |
58 | self.var_stack.push(inner); | 64 | self.var_stack.push(inner); |
59 | let result = self.do_canonicalize_ty(known_ty.clone()); | 65 | let result = self.do_canonicalize_ty(known_ty.clone()); |
60 | self.var_stack.pop(); | 66 | self.var_stack.pop(); |
61 | result | 67 | result |
62 | } else { | 68 | } else { |
63 | let root = self.ctx.var_unification_table.find(inner); | 69 | let root = self.ctx.table.var_unification_table.find(inner); |
64 | let free_var = match tv { | 70 | let free_var = match tv { |
65 | InferTy::TypeVar(_) => InferTy::TypeVar(root), | 71 | InferTy::TypeVar(_) => InferTy::TypeVar(root), |
66 | InferTy::IntVar(_) => InferTy::IntVar(root), | 72 | InferTy::IntVar(_) => InferTy::IntVar(root), |
@@ -153,10 +159,268 @@ impl<T> Canonicalized<T> { | |||
153 | solution: Canonical<Vec<Ty>>, | 159 | solution: Canonical<Vec<Ty>>, |
154 | ) { | 160 | ) { |
155 | // the solution may contain new variables, which we need to convert to new inference vars | 161 | // the solution may contain new variables, which we need to convert to new inference vars |
156 | let new_vars = Substs((0..solution.num_vars).map(|_| ctx.new_type_var()).collect()); | 162 | let new_vars = Substs((0..solution.num_vars).map(|_| ctx.table.new_type_var()).collect()); |
157 | for (i, ty) in solution.value.into_iter().enumerate() { | 163 | for (i, ty) in solution.value.into_iter().enumerate() { |
158 | let var = self.free_vars[i]; | 164 | let var = self.free_vars[i]; |
159 | ctx.unify(&Ty::Infer(var), &ty.subst_bound_vars(&new_vars)); | 165 | ctx.table.unify(&Ty::Infer(var), &ty.subst_bound_vars(&new_vars)); |
166 | } | ||
167 | } | ||
168 | } | ||
169 | |||
170 | pub fn unify(ty1: &Canonical<Ty>, ty2: &Canonical<Ty>) -> Option<Substs> { | ||
171 | let mut table = InferenceTable::new(); | ||
172 | let vars = | ||
173 | Substs::builder(ty1.num_vars).fill(std::iter::repeat_with(|| table.new_type_var())).build(); | ||
174 | let ty_with_vars = ty1.value.clone().subst_bound_vars(&vars); | ||
175 | if !table.unify(&ty_with_vars, &ty2.value) { | ||
176 | return None; | ||
177 | } | ||
178 | Some( | ||
179 | Substs::builder(ty1.num_vars) | ||
180 | .fill(vars.iter().map(|v| table.resolve_ty_completely(v.clone()))) | ||
181 | .build(), | ||
182 | ) | ||
183 | } | ||
184 | |||
185 | #[derive(Clone, Debug)] | ||
186 | pub(crate) struct InferenceTable { | ||
187 | pub(super) var_unification_table: InPlaceUnificationTable<TypeVarId>, | ||
188 | } | ||
189 | |||
190 | impl InferenceTable { | ||
191 | pub fn new() -> Self { | ||
192 | InferenceTable { var_unification_table: InPlaceUnificationTable::new() } | ||
193 | } | ||
194 | |||
195 | pub fn new_type_var(&mut self) -> Ty { | ||
196 | Ty::Infer(InferTy::TypeVar(self.var_unification_table.new_key(TypeVarValue::Unknown))) | ||
197 | } | ||
198 | |||
199 | pub fn new_integer_var(&mut self) -> Ty { | ||
200 | Ty::Infer(InferTy::IntVar(self.var_unification_table.new_key(TypeVarValue::Unknown))) | ||
201 | } | ||
202 | |||
203 | pub fn new_float_var(&mut self) -> Ty { | ||
204 | Ty::Infer(InferTy::FloatVar(self.var_unification_table.new_key(TypeVarValue::Unknown))) | ||
205 | } | ||
206 | |||
207 | pub fn new_maybe_never_type_var(&mut self) -> Ty { | ||
208 | Ty::Infer(InferTy::MaybeNeverTypeVar( | ||
209 | self.var_unification_table.new_key(TypeVarValue::Unknown), | ||
210 | )) | ||
211 | } | ||
212 | |||
213 | pub fn resolve_ty_completely(&mut self, ty: Ty) -> Ty { | ||
214 | self.resolve_ty_completely_inner(&mut Vec::new(), ty) | ||
215 | } | ||
216 | |||
217 | pub fn resolve_ty_as_possible(&mut self, ty: Ty) -> Ty { | ||
218 | self.resolve_ty_as_possible_inner(&mut Vec::new(), ty) | ||
219 | } | ||
220 | |||
221 | pub fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool { | ||
222 | self.unify_inner(ty1, ty2, 0) | ||
223 | } | ||
224 | |||
225 | pub fn unify_substs(&mut self, substs1: &Substs, substs2: &Substs, depth: usize) -> bool { | ||
226 | substs1.0.iter().zip(substs2.0.iter()).all(|(t1, t2)| self.unify_inner(t1, t2, depth)) | ||
227 | } | ||
228 | |||
229 | fn unify_inner(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool { | ||
230 | if depth > 1000 { | ||
231 | // prevent stackoverflows | ||
232 | panic!("infinite recursion in unification"); | ||
233 | } | ||
234 | if ty1 == ty2 { | ||
235 | return true; | ||
236 | } | ||
237 | // try to resolve type vars first | ||
238 | let ty1 = self.resolve_ty_shallow(ty1); | ||
239 | let ty2 = self.resolve_ty_shallow(ty2); | ||
240 | match (&*ty1, &*ty2) { | ||
241 | (Ty::Apply(a_ty1), Ty::Apply(a_ty2)) if a_ty1.ctor == a_ty2.ctor => { | ||
242 | self.unify_substs(&a_ty1.parameters, &a_ty2.parameters, depth + 1) | ||
243 | } | ||
244 | _ => self.unify_inner_trivial(&ty1, &ty2), | ||
245 | } | ||
246 | } | ||
247 | |||
248 | pub(super) fn unify_inner_trivial(&mut self, ty1: &Ty, ty2: &Ty) -> bool { | ||
249 | match (ty1, ty2) { | ||
250 | (Ty::Unknown, _) | (_, Ty::Unknown) => true, | ||
251 | |||
252 | (Ty::Infer(InferTy::TypeVar(tv1)), Ty::Infer(InferTy::TypeVar(tv2))) | ||
253 | | (Ty::Infer(InferTy::IntVar(tv1)), Ty::Infer(InferTy::IntVar(tv2))) | ||
254 | | (Ty::Infer(InferTy::FloatVar(tv1)), Ty::Infer(InferTy::FloatVar(tv2))) | ||
255 | | ( | ||
256 | Ty::Infer(InferTy::MaybeNeverTypeVar(tv1)), | ||
257 | Ty::Infer(InferTy::MaybeNeverTypeVar(tv2)), | ||
258 | ) => { | ||
259 | // both type vars are unknown since we tried to resolve them | ||
260 | self.var_unification_table.union(*tv1, *tv2); | ||
261 | true | ||
262 | } | ||
263 | |||
264 | // The order of MaybeNeverTypeVar matters here. | ||
265 | // Unifying MaybeNeverTypeVar and TypeVar will let the latter become MaybeNeverTypeVar. | ||
266 | // Unifying MaybeNeverTypeVar and other concrete type will let the former become it. | ||
267 | (Ty::Infer(InferTy::TypeVar(tv)), other) | ||
268 | | (other, Ty::Infer(InferTy::TypeVar(tv))) | ||
269 | | (Ty::Infer(InferTy::MaybeNeverTypeVar(tv)), other) | ||
270 | | (other, Ty::Infer(InferTy::MaybeNeverTypeVar(tv))) | ||
271 | | (Ty::Infer(InferTy::IntVar(tv)), other @ ty_app!(TypeCtor::Int(_))) | ||
272 | | (other @ ty_app!(TypeCtor::Int(_)), Ty::Infer(InferTy::IntVar(tv))) | ||
273 | | (Ty::Infer(InferTy::FloatVar(tv)), other @ ty_app!(TypeCtor::Float(_))) | ||
274 | | (other @ ty_app!(TypeCtor::Float(_)), Ty::Infer(InferTy::FloatVar(tv))) => { | ||
275 | // the type var is unknown since we tried to resolve it | ||
276 | self.var_unification_table.union_value(*tv, TypeVarValue::Known(other.clone())); | ||
277 | true | ||
278 | } | ||
279 | |||
280 | _ => false, | ||
281 | } | ||
282 | } | ||
283 | |||
284 | /// If `ty` is a type variable with known type, returns that type; | ||
285 | /// otherwise, return ty. | ||
286 | pub fn resolve_ty_shallow<'b>(&mut self, ty: &'b Ty) -> Cow<'b, Ty> { | ||
287 | let mut ty = Cow::Borrowed(ty); | ||
288 | // The type variable could resolve to a int/float variable. Hence try | ||
289 | // resolving up to three times; each type of variable shouldn't occur | ||
290 | // more than once | ||
291 | for i in 0..3 { | ||
292 | if i > 0 { | ||
293 | tested_by!(type_var_resolves_to_int_var); | ||
294 | } | ||
295 | match &*ty { | ||
296 | Ty::Infer(tv) => { | ||
297 | let inner = tv.to_inner(); | ||
298 | match self.var_unification_table.inlined_probe_value(inner).known() { | ||
299 | Some(known_ty) => { | ||
300 | // The known_ty can't be a type var itself | ||
301 | ty = Cow::Owned(known_ty.clone()); | ||
302 | } | ||
303 | _ => return ty, | ||
304 | } | ||
305 | } | ||
306 | _ => return ty, | ||
307 | } | ||
308 | } | ||
309 | log::error!("Inference variable still not resolved: {:?}", ty); | ||
310 | ty | ||
311 | } | ||
312 | |||
313 | /// Resolves the type as far as currently possible, replacing type variables | ||
314 | /// by their known types. All types returned by the infer_* functions should | ||
315 | /// be resolved as far as possible, i.e. contain no type variables with | ||
316 | /// known type. | ||
317 | fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty { | ||
318 | ty.fold(&mut |ty| match ty { | ||
319 | Ty::Infer(tv) => { | ||
320 | let inner = tv.to_inner(); | ||
321 | if tv_stack.contains(&inner) { | ||
322 | tested_by!(type_var_cycles_resolve_as_possible); | ||
323 | // recursive type | ||
324 | return tv.fallback_value(); | ||
325 | } | ||
326 | if let Some(known_ty) = | ||
327 | self.var_unification_table.inlined_probe_value(inner).known() | ||
328 | { | ||
329 | // known_ty may contain other variables that are known by now | ||
330 | tv_stack.push(inner); | ||
331 | let result = self.resolve_ty_as_possible_inner(tv_stack, known_ty.clone()); | ||
332 | tv_stack.pop(); | ||
333 | result | ||
334 | } else { | ||
335 | ty | ||
336 | } | ||
337 | } | ||
338 | _ => ty, | ||
339 | }) | ||
340 | } | ||
341 | |||
342 | /// Resolves the type completely; type variables without known type are | ||
343 | /// replaced by Ty::Unknown. | ||
344 | fn resolve_ty_completely_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty { | ||
345 | ty.fold(&mut |ty| match ty { | ||
346 | Ty::Infer(tv) => { | ||
347 | let inner = tv.to_inner(); | ||
348 | if tv_stack.contains(&inner) { | ||
349 | tested_by!(type_var_cycles_resolve_completely); | ||
350 | // recursive type | ||
351 | return tv.fallback_value(); | ||
352 | } | ||
353 | if let Some(known_ty) = | ||
354 | self.var_unification_table.inlined_probe_value(inner).known() | ||
355 | { | ||
356 | // known_ty may contain other variables that are known by now | ||
357 | tv_stack.push(inner); | ||
358 | let result = self.resolve_ty_completely_inner(tv_stack, known_ty.clone()); | ||
359 | tv_stack.pop(); | ||
360 | result | ||
361 | } else { | ||
362 | tv.fallback_value() | ||
363 | } | ||
364 | } | ||
365 | _ => ty, | ||
366 | }) | ||
367 | } | ||
368 | } | ||
369 | |||
370 | /// The ID of a type variable. | ||
371 | #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)] | ||
372 | pub struct TypeVarId(pub(super) u32); | ||
373 | |||
374 | impl UnifyKey for TypeVarId { | ||
375 | type Value = TypeVarValue; | ||
376 | |||
377 | fn index(&self) -> u32 { | ||
378 | self.0 | ||
379 | } | ||
380 | |||
381 | fn from_index(i: u32) -> Self { | ||
382 | TypeVarId(i) | ||
383 | } | ||
384 | |||
385 | fn tag() -> &'static str { | ||
386 | "TypeVarId" | ||
387 | } | ||
388 | } | ||
389 | |||
390 | /// The value of a type variable: either we already know the type, or we don't | ||
391 | /// know it yet. | ||
392 | #[derive(Clone, PartialEq, Eq, Debug)] | ||
393 | pub enum TypeVarValue { | ||
394 | Known(Ty), | ||
395 | Unknown, | ||
396 | } | ||
397 | |||
398 | impl TypeVarValue { | ||
399 | fn known(&self) -> Option<&Ty> { | ||
400 | match self { | ||
401 | TypeVarValue::Known(ty) => Some(ty), | ||
402 | TypeVarValue::Unknown => None, | ||
403 | } | ||
404 | } | ||
405 | } | ||
406 | |||
407 | impl UnifyValue for TypeVarValue { | ||
408 | type Error = NoError; | ||
409 | |||
410 | fn unify_values(value1: &Self, value2: &Self) -> Result<Self, NoError> { | ||
411 | match (value1, value2) { | ||
412 | // We should never equate two type variables, both of which have | ||
413 | // known types. Instead, we recursively equate those types. | ||
414 | (TypeVarValue::Known(t1), TypeVarValue::Known(t2)) => panic!( | ||
415 | "equating two type variables, both of which have known types: {:?} and {:?}", | ||
416 | t1, t2 | ||
417 | ), | ||
418 | |||
419 | // If one side is known, prefer that one. | ||
420 | (TypeVarValue::Known(..), TypeVarValue::Unknown) => Ok(value1.clone()), | ||
421 | (TypeVarValue::Unknown, TypeVarValue::Known(..)) => Ok(value2.clone()), | ||
422 | |||
423 | (TypeVarValue::Unknown, TypeVarValue::Unknown) => Ok(TypeVarValue::Unknown), | ||
160 | } | 424 | } |
161 | } | 425 | } |
162 | } | 426 | } |