]>
Commit | Line | Data |
---|---|---|
3dfed10e | 1 | use crate::debug_span; |
487cf647 | 2 | use chalk_derive::FallibleTypeFolder; |
f9f354fc | 3 | use chalk_ir::fold::shift::Shift; |
487cf647 | 4 | use chalk_ir::fold::{TypeFoldable, TypeFolder}; |
f9f354fc XL |
5 | use chalk_ir::interner::{HasInterner, Interner}; |
6 | use chalk_ir::*; | |
7 | use std::cmp::max; | |
f035d41b | 8 | use tracing::{debug, instrument}; |
f9f354fc | 9 | |
f035d41b | 10 | use super::{InferenceTable, ParameterEnaVariable}; |
f9f354fc XL |
11 | |
12 | impl<I: Interner> InferenceTable<I> { | |
13 | /// Given a value `value` with variables in it, replaces those variables | |
14 | /// with their instantiated values; any variables not yet instantiated are | |
15 | /// replaced with a small integer index 0..N in order of appearance. The | |
16 | /// result is a canonicalized representation of `value`. | |
17 | /// | |
18 | /// Example: | |
19 | /// | |
20 | /// ?22: Foo<?23> | |
21 | /// | |
22 | /// would be quantified to | |
23 | /// | |
24 | /// Canonical { value: `?0: Foo<?1>`, binders: [ui(?22), ui(?23)] } | |
25 | /// | |
26 | /// where `ui(?22)` and `ui(?23)` are the universe indices of `?22` and | |
27 | /// `?23` respectively. | |
28 | /// | |
29 | /// A substitution mapping from the free variables to their re-bound form is | |
30 | /// also returned. | |
487cf647 | 31 | pub fn canonicalize<T>(&mut self, interner: I, value: T) -> Canonicalized<T> |
f9f354fc | 32 | where |
487cf647 FG |
33 | T: TypeFoldable<I>, |
34 | T: HasInterner<Interner = I>, | |
f9f354fc | 35 | { |
3dfed10e | 36 | debug_span!("canonicalize", "{:#?}", value); |
f9f354fc XL |
37 | let mut q = Canonicalizer { |
38 | table: self, | |
39 | free_vars: Vec::new(), | |
40 | max_universe: UniverseIndex::root(), | |
41 | interner, | |
42 | }; | |
487cf647 FG |
43 | let value = value |
44 | .try_fold_with(&mut q, DebruijnIndex::INNERMOST) | |
45 | .unwrap(); | |
f9f354fc | 46 | let free_vars = q.free_vars.clone(); |
f9f354fc XL |
47 | |
48 | Canonicalized { | |
49 | quantified: Canonical { | |
50 | value, | |
51 | binders: q.into_binders(), | |
52 | }, | |
f9f354fc XL |
53 | free_vars, |
54 | } | |
55 | } | |
56 | } | |
57 | ||
58 | #[derive(Debug)] | |
3dfed10e | 59 | pub struct Canonicalized<T: HasInterner> { |
f9f354fc | 60 | /// The canonicalized result. |
3dfed10e | 61 | pub quantified: Canonical<T>, |
f9f354fc XL |
62 | |
63 | /// The free existential variables, along with the universes they inhabit. | |
3dfed10e | 64 | pub free_vars: Vec<ParameterEnaVariable<T::Interner>>, |
f9f354fc XL |
65 | } |
66 | ||
487cf647 | 67 | #[derive(FallibleTypeFolder)] |
f9f354fc XL |
68 | struct Canonicalizer<'q, I: Interner> { |
69 | table: &'q mut InferenceTable<I>, | |
70 | free_vars: Vec<ParameterEnaVariable<I>>, | |
71 | max_universe: UniverseIndex, | |
a2a8927a | 72 | interner: I, |
f9f354fc XL |
73 | } |
74 | ||
75 | impl<'q, I: Interner> Canonicalizer<'q, I> { | |
76 | fn into_binders(self) -> CanonicalVarKinds<I> { | |
77 | let Canonicalizer { | |
78 | table, | |
79 | free_vars, | |
80 | interner, | |
81 | .. | |
82 | } = self; | |
3dfed10e | 83 | CanonicalVarKinds::from_iter( |
f9f354fc XL |
84 | interner, |
85 | free_vars | |
86 | .into_iter() | |
87 | .map(|p_v| p_v.map(|v| table.universe_of_unbound_var(v))), | |
88 | ) | |
89 | } | |
90 | ||
91 | fn add(&mut self, free_var: ParameterEnaVariable<I>) -> usize { | |
f035d41b XL |
92 | self.max_universe = max( |
93 | self.max_universe, | |
94 | self.table.universe_of_unbound_var(*free_var.skip_kind()), | |
95 | ); | |
96 | ||
f9f354fc XL |
97 | self.free_vars |
98 | .iter() | |
f035d41b | 99 | .position(|v| v.skip_kind() == free_var.skip_kind()) |
f9f354fc XL |
100 | .unwrap_or_else(|| { |
101 | let next_index = self.free_vars.len(); | |
102 | self.free_vars.push(free_var); | |
103 | next_index | |
104 | }) | |
105 | } | |
106 | } | |
107 | ||
487cf647 FG |
108 | impl<'i, I: Interner> TypeFolder<I> for Canonicalizer<'i, I> { |
109 | fn as_dyn(&mut self) -> &mut dyn TypeFolder<I> { | |
f9f354fc XL |
110 | self |
111 | } | |
112 | ||
113 | fn fold_free_placeholder_ty( | |
114 | &mut self, | |
115 | universe: PlaceholderIndex, | |
116 | _outer_binder: DebruijnIndex, | |
487cf647 | 117 | ) -> Ty<I> { |
f9f354fc XL |
118 | let interner = self.interner; |
119 | self.max_universe = max(self.max_universe, universe.ui); | |
487cf647 | 120 | universe.to_ty(interner) |
f9f354fc XL |
121 | } |
122 | ||
123 | fn fold_free_placeholder_lifetime( | |
124 | &mut self, | |
125 | universe: PlaceholderIndex, | |
126 | _outer_binder: DebruijnIndex, | |
487cf647 | 127 | ) -> Lifetime<I> { |
f9f354fc XL |
128 | let interner = self.interner; |
129 | self.max_universe = max(self.max_universe, universe.ui); | |
487cf647 | 130 | universe.to_lifetime(interner) |
f9f354fc XL |
131 | } |
132 | ||
f035d41b XL |
133 | fn fold_free_placeholder_const( |
134 | &mut self, | |
5869c6ff | 135 | ty: Ty<I>, |
f035d41b XL |
136 | universe: PlaceholderIndex, |
137 | _outer_binder: DebruijnIndex, | |
487cf647 | 138 | ) -> Const<I> { |
f035d41b XL |
139 | let interner = self.interner; |
140 | self.max_universe = max(self.max_universe, universe.ui); | |
487cf647 | 141 | universe.to_const(interner, ty) |
f035d41b XL |
142 | } |
143 | ||
f9f354fc XL |
144 | fn forbid_free_vars(&self) -> bool { |
145 | true | |
146 | } | |
147 | ||
f035d41b | 148 | #[instrument(level = "debug", skip(self))] |
f9f354fc XL |
149 | fn fold_inference_ty( |
150 | &mut self, | |
151 | var: InferenceVar, | |
29967ef6 | 152 | kind: TyVariableKind, |
f9f354fc | 153 | outer_binder: DebruijnIndex, |
487cf647 | 154 | ) -> Ty<I> { |
f9f354fc | 155 | let interner = self.interner; |
f035d41b | 156 | match self.table.probe_var(var) { |
f9f354fc | 157 | Some(ty) => { |
f035d41b | 158 | let ty = ty.assert_ty_ref(interner); |
f9f354fc | 159 | debug!("bound to {:?}", ty); |
487cf647 FG |
160 | ty.clone() |
161 | .fold_with(self, DebruijnIndex::INNERMOST) | |
162 | .shifted_in_from(interner, outer_binder) | |
f9f354fc XL |
163 | } |
164 | None => { | |
165 | // If this variable is not yet bound, find its | |
166 | // canonical index `root_var` in the union-find table, | |
167 | // and then map `root_var` to a fresh index that is | |
168 | // unique to this quantification. | |
f035d41b XL |
169 | let free_var = |
170 | ParameterEnaVariable::new(VariableKind::Ty(kind), self.table.unify.find(var)); | |
171 | ||
f9f354fc | 172 | let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.add(free_var)); |
3dfed10e | 173 | debug!(position=?bound_var, "not yet unified"); |
487cf647 | 174 | TyKind::BoundVar(bound_var.shifted_in_from(outer_binder)).intern(interner) |
f9f354fc XL |
175 | } |
176 | } | |
177 | } | |
178 | ||
f035d41b | 179 | #[instrument(level = "debug", skip(self))] |
f9f354fc XL |
180 | fn fold_inference_lifetime( |
181 | &mut self, | |
182 | var: InferenceVar, | |
183 | outer_binder: DebruijnIndex, | |
487cf647 | 184 | ) -> Lifetime<I> { |
f9f354fc | 185 | let interner = self.interner; |
f035d41b | 186 | match self.table.probe_var(var) { |
f9f354fc | 187 | Some(l) => { |
f035d41b | 188 | let l = l.assert_lifetime_ref(interner); |
f9f354fc | 189 | debug!("bound to {:?}", l); |
487cf647 FG |
190 | l.clone() |
191 | .fold_with(self, DebruijnIndex::INNERMOST) | |
192 | .shifted_in_from(interner, outer_binder) | |
f9f354fc XL |
193 | } |
194 | None => { | |
f035d41b XL |
195 | let free_var = |
196 | ParameterEnaVariable::new(VariableKind::Lifetime, self.table.unify.find(var)); | |
f9f354fc | 197 | let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.add(free_var)); |
3dfed10e | 198 | debug!(position=?bound_var, "not yet unified"); |
487cf647 | 199 | LifetimeData::BoundVar(bound_var.shifted_in_from(outer_binder)).intern(interner) |
f9f354fc XL |
200 | } |
201 | } | |
202 | } | |
203 | ||
f035d41b XL |
204 | #[instrument(level = "debug", skip(self, ty))] |
205 | fn fold_inference_const( | |
206 | &mut self, | |
5869c6ff | 207 | ty: Ty<I>, |
f035d41b XL |
208 | var: InferenceVar, |
209 | outer_binder: DebruijnIndex, | |
487cf647 | 210 | ) -> Const<I> { |
f035d41b XL |
211 | let interner = self.interner; |
212 | match self.table.probe_var(var) { | |
213 | Some(c) => { | |
214 | let c = c.assert_const_ref(interner); | |
215 | debug!("bound to {:?}", c); | |
487cf647 FG |
216 | c.clone() |
217 | .fold_with(self, DebruijnIndex::INNERMOST) | |
218 | .shifted_in_from(interner, outer_binder) | |
f035d41b XL |
219 | } |
220 | None => { | |
221 | let free_var = ParameterEnaVariable::new( | |
222 | VariableKind::Const(ty.clone()), | |
223 | self.table.unify.find(var), | |
224 | ); | |
225 | let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.add(free_var)); | |
3dfed10e | 226 | debug!(position = ?bound_var, "not yet unified"); |
487cf647 | 227 | bound_var |
f035d41b | 228 | .shifted_in_from(outer_binder) |
487cf647 | 229 | .to_const(interner, ty) |
5869c6ff | 230 | } |
5869c6ff | 231 | } |
f9f354fc XL |
232 | } |
233 | ||
a2a8927a | 234 | fn interner(&self) -> I { |
5869c6ff | 235 | self.interner |
f9f354fc XL |
236 | } |
237 | } |