]>
Commit | Line | Data |
---|---|---|
f9f354fc XL |
1 | use chalk_ir::interner::{HasInterner, Interner}; |
2 | use chalk_ir::*; | |
3 | use chalk_ir::{cast::Cast, fold::Fold}; | |
5869c6ff | 4 | use tracing::debug; |
f9f354fc | 5 | |
3dfed10e | 6 | mod canonicalize; |
f9f354fc XL |
7 | pub(crate) mod instantiate; |
8 | mod invert; | |
f9f354fc | 9 | mod test; |
3dfed10e XL |
10 | pub mod ucanonicalize; |
11 | pub mod unify; | |
12 | mod var; | |
f9f354fc XL |
13 | |
14 | use self::var::*; | |
15 | ||
16 | #[derive(Clone)] | |
3dfed10e | 17 | pub struct InferenceTable<I: Interner> { |
f9f354fc XL |
18 | unify: ena::unify::InPlaceUnificationTable<EnaVariable<I>>, |
19 | vars: Vec<EnaVariable<I>>, | |
20 | max_universe: UniverseIndex, | |
21 | } | |
22 | ||
23 | pub(crate) struct InferenceSnapshot<I: Interner> { | |
24 | unify_snapshot: ena::unify::Snapshot<ena::unify::InPlace<EnaVariable<I>>>, | |
25 | max_universe: UniverseIndex, | |
26 | vars: Vec<EnaVariable<I>>, | |
27 | } | |
28 | ||
29 | #[allow(type_alias_bounds)] | |
f035d41b | 30 | pub(crate) type ParameterEnaVariable<I: Interner> = WithKind<I, EnaVariable<I>>; |
f9f354fc XL |
31 | |
32 | impl<I: Interner> InferenceTable<I> { | |
33 | /// Create an empty inference table with no variables. | |
3dfed10e | 34 | pub fn new() -> Self { |
f9f354fc XL |
35 | InferenceTable { |
36 | unify: ena::unify::UnificationTable::new(), | |
37 | vars: vec![], | |
38 | max_universe: UniverseIndex::root(), | |
39 | } | |
40 | } | |
41 | ||
42 | /// Creates a new inference table, pre-populated with | |
43 | /// `num_universes` fresh universes. Instantiates the canonical | |
44 | /// value `canonical` within those universes (which must not | |
45 | /// reference any universe greater than `num_universes`). Returns | |
46 | /// the substitution mapping from each canonical binder to its | |
47 | /// corresponding existential variable, along with the | |
48 | /// instantiated result. | |
3dfed10e | 49 | pub fn from_canonical<T>( |
f9f354fc XL |
50 | interner: &I, |
51 | num_universes: usize, | |
5869c6ff | 52 | canonical: Canonical<T>, |
f9f354fc XL |
53 | ) -> (Self, Substitution<I>, T) |
54 | where | |
55 | T: HasInterner<Interner = I> + Fold<I, Result = T> + Clone, | |
56 | { | |
57 | let mut table = InferenceTable::new(); | |
58 | ||
59 | assert!(num_universes >= 1); // always have U0 | |
60 | for _ in 1..num_universes { | |
61 | table.new_universe(); | |
62 | } | |
63 | ||
64 | let subst = table.fresh_subst(interner, canonical.binders.as_slice(interner)); | |
5869c6ff | 65 | let value = subst.apply(canonical.value, interner); |
f9f354fc XL |
66 | // let value = canonical.value.fold_with(&mut &subst, 0).unwrap(); |
67 | ||
68 | (table, subst, value) | |
69 | } | |
70 | ||
71 | /// Creates and returns a fresh universe that is distinct from all | |
72 | /// others created within this inference table. This universe is | |
73 | /// able to see all previously created universes (though hopefully | |
74 | /// it is only brought into contact with its logical *parents*). | |
75 | pub(crate) fn new_universe(&mut self) -> UniverseIndex { | |
76 | let u = self.max_universe.next(); | |
77 | self.max_universe = u; | |
3dfed10e | 78 | debug!("created new universe: {:?}", u); |
f9f354fc XL |
79 | u |
80 | } | |
81 | ||
82 | /// Creates a new inference variable and returns its index. The | |
83 | /// kind of the variable should be known by the caller, but is not | |
84 | /// tracked directly by the inference table. | |
3dfed10e | 85 | pub fn new_variable(&mut self, ui: UniverseIndex) -> EnaVariable<I> { |
f9f354fc XL |
86 | let var = self.unify.new_key(InferenceValue::Unbound(ui)); |
87 | self.vars.push(var); | |
3dfed10e | 88 | debug!(?var, ?ui, "created new variable"); |
f9f354fc XL |
89 | var |
90 | } | |
91 | ||
92 | /// Takes a "snapshot" of the current state of the inference | |
93 | /// table. Later, you must invoke either `rollback_to` or | |
94 | /// `commit` with that snapshot. Snapshots can be nested, but you | |
95 | /// must respect a stack discipline (i.e., rollback or commit | |
96 | /// snapshots in reverse order of that with which they were | |
97 | /// created). | |
98 | pub(crate) fn snapshot(&mut self) -> InferenceSnapshot<I> { | |
99 | let unify_snapshot = self.unify.snapshot(); | |
100 | let vars = self.vars.clone(); | |
101 | let max_universe = self.max_universe; | |
102 | InferenceSnapshot { | |
103 | unify_snapshot, | |
104 | max_universe, | |
105 | vars, | |
106 | } | |
107 | } | |
108 | ||
109 | /// Restore the table to the state it had when the snapshot was taken. | |
110 | pub(crate) fn rollback_to(&mut self, snapshot: InferenceSnapshot<I>) { | |
111 | self.unify.rollback_to(snapshot.unify_snapshot); | |
112 | self.vars = snapshot.vars; | |
113 | self.max_universe = snapshot.max_universe; | |
114 | } | |
115 | ||
116 | /// Make permanent the changes made since the snapshot was taken. | |
117 | pub(crate) fn commit(&mut self, snapshot: InferenceSnapshot<I>) { | |
118 | self.unify.commit(snapshot.unify_snapshot); | |
119 | } | |
120 | ||
3dfed10e | 121 | pub fn normalize_ty_shallow(&mut self, interner: &I, leaf: &Ty<I>) -> Option<Ty<I>> { |
5869c6ff XL |
122 | // An integer/float type variable will never normalize to another |
123 | // variable; but a general type variable might normalize to an | |
124 | // integer/float variable. So we potentially need to normalize twice to | |
125 | // get at the actual value. | |
126 | self.normalize_ty_shallow_inner(interner, leaf) | |
127 | .map(|ty| self.normalize_ty_shallow_inner(interner, &ty).unwrap_or(ty)) | |
128 | } | |
129 | ||
130 | fn normalize_ty_shallow_inner(&mut self, interner: &I, leaf: &Ty<I>) -> Option<Ty<I>> { | |
f035d41b XL |
131 | self.probe_var(leaf.inference_var(interner)?) |
132 | .map(|p| p.assert_ty_ref(interner).clone()) | |
f9f354fc XL |
133 | } |
134 | ||
3dfed10e | 135 | pub fn normalize_lifetime_shallow( |
f9f354fc XL |
136 | &mut self, |
137 | interner: &I, | |
138 | leaf: &Lifetime<I>, | |
139 | ) -> Option<Lifetime<I>> { | |
f035d41b XL |
140 | self.probe_var(leaf.inference_var(interner)?) |
141 | .map(|p| p.assert_lifetime_ref(interner).clone()) | |
f9f354fc XL |
142 | } |
143 | ||
3dfed10e | 144 | pub fn normalize_const_shallow(&mut self, interner: &I, leaf: &Const<I>) -> Option<Const<I>> { |
f035d41b XL |
145 | self.probe_var(leaf.inference_var(interner)?) |
146 | .map(|p| p.assert_const_ref(interner).clone()) | |
f9f354fc XL |
147 | } |
148 | ||
5869c6ff XL |
149 | pub fn ty_root(&mut self, interner: &I, leaf: &Ty<I>) -> Option<Ty<I>> { |
150 | Some( | |
151 | self.unify | |
152 | .find(leaf.inference_var(interner)?) | |
153 | .to_ty(interner), | |
154 | ) | |
155 | } | |
156 | ||
157 | pub fn lifetime_root(&mut self, interner: &I, leaf: &Lifetime<I>) -> Option<Lifetime<I>> { | |
158 | Some( | |
159 | self.unify | |
160 | .find(leaf.inference_var(interner)?) | |
161 | .to_lifetime(interner), | |
162 | ) | |
163 | } | |
164 | ||
165 | /// Finds the root inference var for the given variable. | |
166 | /// | |
167 | /// The returned variable will be exactly equivalent to the given | |
168 | /// variable except in name. All variables which have been unified to | |
169 | /// eachother (but don't yet have a value) have the same "root". | |
170 | /// | |
171 | /// This is useful for `DeepNormalizer`. | |
172 | pub fn inference_var_root(&mut self, var: InferenceVar) -> InferenceVar { | |
173 | self.unify.find(var).into() | |
174 | } | |
175 | ||
f035d41b XL |
176 | /// If type `leaf` is a free inference variable, and that variable has been |
177 | /// bound, returns `Some(P)` where `P` is the parameter to which it has been bound. | |
3dfed10e | 178 | pub fn probe_var(&mut self, leaf: InferenceVar) -> Option<GenericArg<I>> { |
f035d41b | 179 | match self.unify.probe_value(EnaVariable::from(leaf)) { |
f9f354fc | 180 | InferenceValue::Unbound(_) => None, |
f035d41b | 181 | InferenceValue::Bound(val) => Some(val), |
f9f354fc XL |
182 | } |
183 | } | |
184 | ||
185 | /// Given an unbound variable, returns its universe. | |
186 | /// | |
187 | /// # Panics | |
188 | /// | |
189 | /// Panics if the variable is bound. | |
190 | fn universe_of_unbound_var(&mut self, var: EnaVariable<I>) -> UniverseIndex { | |
191 | match self.unify.probe_value(var) { | |
192 | InferenceValue::Unbound(ui) => ui, | |
193 | InferenceValue::Bound(_) => panic!("var_universe invoked on bound variable"), | |
194 | } | |
195 | } | |
f9f354fc XL |
196 | } |
197 | ||
3dfed10e | 198 | pub trait ParameterEnaVariableExt<I: Interner> { |
f035d41b | 199 | fn to_generic_arg(&self, interner: &I) -> GenericArg<I>; |
f9f354fc XL |
200 | } |
201 | ||
202 | impl<I: Interner> ParameterEnaVariableExt<I> for ParameterEnaVariable<I> { | |
f035d41b XL |
203 | fn to_generic_arg(&self, interner: &I) -> GenericArg<I> { |
204 | // we are matching on kind, so skipping it is fine | |
205 | let ena_variable = self.skip_kind(); | |
206 | match &self.kind { | |
207 | VariableKind::Ty(kind) => ena_variable.to_ty_with_kind(interner, *kind).cast(interner), | |
208 | VariableKind::Lifetime => ena_variable.to_lifetime(interner).cast(interner), | |
209 | VariableKind::Const(ty) => ena_variable.to_const(interner, ty.clone()).cast(interner), | |
f9f354fc XL |
210 | } |
211 | } | |
212 | } |