chalk_solve/infer/
instantiate.rs

1use chalk_ir::fold::*;
2use chalk_ir::interner::HasInterner;
3use std::fmt::Debug;
4use tracing::instrument;
5
6use super::*;
7
8impl<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(super) fn fresh_subst(
15        &mut self,
16        interner: I,
17        binders: &[CanonicalVarKind<I>],
18    ) -> Substitution<I> {
19        Substitution::from_iter(
20            interner,
21            binders.iter().map(|kind| {
22                let param_infer_var = kind.map_ref(|&ui| self.new_variable(ui));
23                param_infer_var.to_generic_arg(interner)
24            }),
25        )
26    }
27
28    /// Variant on `instantiate` that takes a `Canonical<T>`.
29    pub fn instantiate_canonical<T>(&mut self, interner: I, bound: Canonical<T>) -> T
30    where
31        T: HasInterner<Interner = I> + TypeFoldable<I> + Debug,
32    {
33        let subst = self.fresh_subst(interner, bound.binders.as_slice(interner));
34        subst.apply(bound.value, interner)
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`.
42    fn instantiate_in<T>(
43        &mut self,
44        interner: I,
45        universe: UniverseIndex,
46        binders: impl Iterator<Item = VariableKind<I>>,
47        arg: T,
48    ) -> T
49    where
50        T: TypeFoldable<I>,
51    {
52        let binders: Vec<_> = binders
53            .map(|pk| CanonicalVarKind::new(pk, universe))
54            .collect();
55        let subst = self.fresh_subst(interner, &binders);
56        subst.apply(arg, interner)
57    }
58
59    /// Variant on `instantiate_in` that takes a `Binders<T>`.
60    #[instrument(level = "debug", skip(self, interner))]
61    pub fn instantiate_binders_existentially<T>(&mut self, interner: I, arg: Binders<T>) -> T
62    where
63        T: TypeFoldable<I> + HasInterner<Interner = I>,
64    {
65        let (value, binders) = arg.into_value_and_skipped_binders();
66
67        let max_universe = self.max_universe;
68        self.instantiate_in(
69            interner,
70            max_universe,
71            binders.iter(interner).cloned(),
72            value,
73        )
74    }
75
76    #[instrument(level = "debug", skip(self, interner))]
77    pub fn instantiate_binders_universally<T>(&mut self, interner: I, arg: Binders<T>) -> T
78    where
79        T: TypeFoldable<I> + HasInterner<Interner = I>,
80    {
81        let (value, binders) = arg.into_value_and_skipped_binders();
82
83        let mut lazy_ui = None;
84        let mut ui = || {
85            lazy_ui.unwrap_or_else(|| {
86                let ui = self.new_universe();
87                lazy_ui = Some(ui);
88                ui
89            })
90        };
91        let parameters: Vec<_> = binders
92            .iter(interner)
93            .cloned()
94            .enumerate()
95            .map(|(idx, pk)| {
96                let placeholder_idx = PlaceholderIndex { ui: ui(), idx };
97                match pk {
98                    VariableKind::Lifetime => {
99                        let lt = placeholder_idx.to_lifetime(interner);
100                        lt.cast(interner)
101                    }
102                    VariableKind::Ty(_) => placeholder_idx.to_ty(interner).cast(interner),
103                    VariableKind::Const(ty) => {
104                        placeholder_idx.to_const(interner, ty).cast(interner)
105                    }
106                }
107            })
108            .collect();
109        Subst::apply(interner, &parameters, value)
110    }
111}
chalk_solve/infer/instantiate.rs

chalk_solve/infer/
instantiate.rs
