]>
Commit | Line | Data |
---|---|---|
f9f354fc XL |
1 | use chalk_ir::fold::*; |
2 | use chalk_ir::interner::HasInterner; | |
3 | use std::fmt::Debug; | |
5869c6ff | 4 | use tracing::instrument; |
f9f354fc XL |
5 | |
6 | use super::*; | |
7 | ||
8 | impl<I: Interner> InferenceTable<I> { | |
9 | /// Given the binders from a canonicalized value C, returns a | |
10 | /// substitution S mapping each free variable in C to a fresh | |
11 | /// inference variable. This substitution can then be applied to | |
12 | /// C, which would be equivalent to | |
13 | /// `self.instantiate_canonical(v)`. | |
14 | pub(crate) fn fresh_subst( | |
15 | &mut self, | |
16 | interner: &I, | |
f035d41b | 17 | binders: &[CanonicalVarKind<I>], |
f9f354fc | 18 | ) -> Substitution<I> { |
3dfed10e | 19 | Substitution::from_iter( |
f9f354fc XL |
20 | interner, |
21 | binders.iter().map(|kind| { | |
f035d41b XL |
22 | let param_infer_var = kind.map_ref(|&ui| self.new_variable(ui)); |
23 | param_infer_var.to_generic_arg(interner) | |
f9f354fc XL |
24 | }), |
25 | ) | |
26 | } | |
27 | ||
28 | /// Variant on `instantiate` that takes a `Canonical<T>`. | |
5869c6ff | 29 | pub fn instantiate_canonical<T>(&mut self, interner: &I, bound: Canonical<T>) -> T::Result |
f9f354fc XL |
30 | where |
31 | T: HasInterner<Interner = I> + Fold<I> + Debug, | |
32 | { | |
33 | let subst = self.fresh_subst(interner, &bound.binders.as_slice(interner)); | |
5869c6ff | 34 | subst.apply(bound.value, interner) |
f9f354fc XL |
35 | } |
36 | ||
37 | /// Instantiates `arg` with fresh existential variables in the | |
38 | /// given universe; the kinds of the variables are implied by | |
39 | /// `binders`. This is used to apply a universally quantified | |
40 | /// clause like `forall X, 'Y. P => Q`. Here the `binders` | |
41 | /// argument is referring to `X, 'Y`. | |
5869c6ff | 42 | pub(crate) fn instantiate_in<T>( |
f9f354fc XL |
43 | &mut self, |
44 | interner: &I, | |
45 | universe: UniverseIndex, | |
5869c6ff XL |
46 | binders: impl Iterator<Item = VariableKind<I>>, |
47 | arg: T, | |
f9f354fc XL |
48 | ) -> T::Result |
49 | where | |
50 | T: Fold<I>, | |
f9f354fc XL |
51 | { |
52 | let binders: Vec<_> = binders | |
f035d41b | 53 | .map(|pk| CanonicalVarKind::new(pk, universe)) |
f9f354fc XL |
54 | .collect(); |
55 | let subst = self.fresh_subst(interner, &binders); | |
5869c6ff | 56 | subst.apply(arg, interner) |
f9f354fc XL |
57 | } |
58 | ||
59 | /// Variant on `instantiate_in` that takes a `Binders<T>`. | |
5869c6ff | 60 | #[instrument(level = "debug", skip(self, interner))] |
3dfed10e | 61 | pub fn instantiate_binders_existentially<'a, T>( |
f9f354fc XL |
62 | &mut self, |
63 | interner: &'a I, | |
5869c6ff | 64 | arg: Binders<T>, |
f9f354fc XL |
65 | ) -> T::Result |
66 | where | |
5869c6ff | 67 | T: Fold<I> + HasInterner<Interner = I>, |
f9f354fc | 68 | { |
5869c6ff XL |
69 | let (value, binders) = arg.into_value_and_skipped_binders(); |
70 | ||
f9f354fc | 71 | let max_universe = self.max_universe; |
5869c6ff XL |
72 | self.instantiate_in( |
73 | interner, | |
74 | max_universe, | |
75 | binders.iter(interner).cloned(), | |
76 | value, | |
77 | ) | |
f9f354fc XL |
78 | } |
79 | ||
5869c6ff | 80 | #[instrument(level = "debug", skip(self, interner))] |
3dfed10e | 81 | pub fn instantiate_binders_universally<'a, T>( |
f9f354fc XL |
82 | &mut self, |
83 | interner: &'a I, | |
5869c6ff | 84 | arg: Binders<T>, |
f9f354fc XL |
85 | ) -> T::Result |
86 | where | |
5869c6ff | 87 | T: Fold<I> + HasInterner<Interner = I>, |
f9f354fc | 88 | { |
5869c6ff XL |
89 | let (value, binders) = arg.into_value_and_skipped_binders(); |
90 | ||
91 | let mut lazy_ui = None; | |
92 | let mut ui = || { | |
93 | lazy_ui.unwrap_or_else(|| { | |
94 | let ui = self.new_universe(); | |
95 | lazy_ui = Some(ui); | |
96 | ui | |
97 | }) | |
98 | }; | |
f9f354fc | 99 | let parameters: Vec<_> = binders |
5869c6ff XL |
100 | .iter(interner) |
101 | .cloned() | |
f9f354fc XL |
102 | .enumerate() |
103 | .map(|(idx, pk)| { | |
5869c6ff | 104 | let placeholder_idx = PlaceholderIndex { ui: ui(), idx }; |
f9f354fc | 105 | match pk { |
f035d41b | 106 | VariableKind::Lifetime => { |
f9f354fc XL |
107 | let lt = placeholder_idx.to_lifetime(interner); |
108 | lt.cast(interner) | |
109 | } | |
f035d41b XL |
110 | VariableKind::Ty(_) => placeholder_idx.to_ty(interner).cast(interner), |
111 | VariableKind::Const(ty) => { | |
112 | placeholder_idx.to_const(interner, ty).cast(interner) | |
113 | } | |
f9f354fc XL |
114 | } |
115 | }) | |
116 | .collect(); | |
5869c6ff | 117 | Subst::apply(interner, ¶meters, value) |
f9f354fc XL |
118 | } |
119 | } |