chalk_engine/
normalize_deep.rs

1use chalk_derive::FallibleTypeFolder;
2use chalk_ir::fold::shift::Shift;
3use chalk_ir::fold::{TypeFoldable, TypeFolder};
4use chalk_ir::interner::Interner;
5use chalk_ir::*;
6use chalk_solve::infer::InferenceTable;
7
8#[derive(FallibleTypeFolder)]
9pub(crate) struct DeepNormalizer<'table, I: Interner> {
10    table: &'table mut InferenceTable<I>,
11    interner: I,
12}
13
14impl<I: Interner> DeepNormalizer<'_, I> {
15    /// Given a value `value` with variables in it, replaces those variables
16    /// with their instantiated values (if any). Uninstantiated variables are
17    /// left as-is.
18    ///
19    /// This is mainly intended for getting final values to dump to
20    /// the user and its use should otherwise be avoided, particularly
21    /// given the possibility of snapshots and rollbacks.
22    ///
23    /// See also `InferenceTable::canonicalize`, which -- during real
24    /// processing -- is often used to capture the "current state" of
25    /// variables.
26    pub fn normalize_deep<T: TypeFoldable<I>>(
27        table: &mut InferenceTable<I>,
28        interner: I,
29        value: T,
30    ) -> T {
31        value
32            .try_fold_with(
33                &mut DeepNormalizer { interner, table },
34                DebruijnIndex::INNERMOST,
35            )
36            .unwrap()
37    }
38}
39
40impl<I: Interner> TypeFolder<I> for DeepNormalizer<'_, I> {
41    fn as_dyn(&mut self) -> &mut dyn TypeFolder<I> {
42        self
43    }
44
45    fn fold_inference_ty(
46        &mut self,
47        var: InferenceVar,
48        kind: TyVariableKind,
49        _outer_binder: DebruijnIndex,
50    ) -> Ty<I> {
51        let interner = self.interner;
52        match self.table.probe_var(var) {
53            Some(ty) => ty
54                .assert_ty_ref(interner)
55                .clone()
56                .fold_with(self, DebruijnIndex::INNERMOST)
57                .shifted_in(interner), // FIXME shift
58            None => {
59                // Normalize all inference vars which have been unified into a
60                // single variable. Ena calls this the "root" variable.
61                self.table.inference_var_root(var).to_ty(interner, kind)
62            }
63        }
64    }
65
66    fn fold_inference_lifetime(
67        &mut self,
68        var: InferenceVar,
69        _outer_binder: DebruijnIndex,
70    ) -> Lifetime<I> {
71        let interner = self.interner;
72        match self.table.probe_var(var) {
73            Some(l) => l
74                .assert_lifetime_ref(interner)
75                .clone()
76                .fold_with(self, DebruijnIndex::INNERMOST)
77                .shifted_in(interner),
78            None => var.to_lifetime(interner), // FIXME shift
79        }
80    }
81
82    fn fold_inference_const(
83        &mut self,
84        ty: Ty<I>,
85        var: InferenceVar,
86        _outer_binder: DebruijnIndex,
87    ) -> Const<I> {
88        let interner = self.interner;
89        match self.table.probe_var(var) {
90            Some(c) => c
91                .assert_const_ref(interner)
92                .clone()
93                .fold_with(self, DebruijnIndex::INNERMOST)
94                .shifted_in(interner),
95            None => var.to_const(interner, ty), // FIXME shift
96        }
97    }
98
99    fn forbid_free_vars(&self) -> bool {
100        true
101    }
102
103    fn interner(&self) -> I {
104        self.interner
105    }
106}
107
108#[cfg(test)]
109mod test {
110    use super::*;
111    use chalk_integration::interner::ChalkIr;
112    use chalk_integration::{arg, ty};
113
114    const U0: UniverseIndex = UniverseIndex { counter: 0 };
115
116    // We just use a vec of 20 `Invariant`, since this is zipped and no substs are
117    // longer than this
118    #[derive(Debug)]
119    struct TestDatabase;
120    impl UnificationDatabase<ChalkIr> for TestDatabase {
121        fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> {
122            Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied())
123        }
124
125        fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> {
126            Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied())
127        }
128    }
129
130    #[test]
131    fn infer() {
132        let interner = ChalkIr;
133        let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
134        let environment0 = Environment::new(interner);
135        let a = table.new_variable(U0).to_ty(interner);
136        let b = table.new_variable(U0).to_ty(interner);
137        table
138            .relate(
139                interner,
140                &TestDatabase,
141                &environment0,
142                Variance::Invariant,
143                &a,
144                &ty!(apply (item 0) (expr b)),
145            )
146            .unwrap();
147        // a is unified to Adt<#0>(c), where 'c' is a new inference var
148        // created by the generalizer to generalize 'b'. It then unifies 'b'
149        // and 'c', and when we normalize them, they'll both be output as
150        // the same "root" variable. However, there are no guarantees for
151        // _which_ of 'b' and 'c' becomes the root. We need to normalize
152        // "b" too, then, to ensure we get a consistent result.
153        assert_eq!(
154            DeepNormalizer::normalize_deep(&mut table, interner, a.clone()),
155            ty!(apply (item 0) (expr DeepNormalizer::normalize_deep(&mut table, interner, b.clone()))),
156        );
157        table
158            .relate(
159                interner,
160                &TestDatabase,
161                &environment0,
162                Variance::Invariant,
163                &b,
164                &ty!(apply (item 1)),
165            )
166            .unwrap();
167        assert_eq!(
168            DeepNormalizer::normalize_deep(&mut table, interner, a),
169            ty!(apply (item 0) (apply (item 1)))
170        );
171    }
172}
chalk_engine/normalize_deep.rs

chalk_engine/
normalize_deep.rs
