vendor/chalk-engine/src/normalize_deep.rs

   1 use chalk_ir::fold::shift::Shift;
   2 use chalk_ir::fold::{Fold, Folder};
   3 use chalk_ir::interner::Interner;
   4 use chalk_ir::*;
   5 use chalk_solve::infer::InferenceTable;
   6
   7 pub(crate) struct DeepNormalizer<'table, 'i, I: Interner> {
   8     table: &'table mut InferenceTable<I>,
   9     interner: &'i I,
  10 }
  11
  12 impl<I: Interner> DeepNormalizer<'_, '_, I> {
  13     /// Given a value `value` with variables in it, replaces those variables
  14     /// with their instantiated values (if any). Uninstantiated variables are
  15     /// left as-is.
  16     ///
  17     /// This is mainly intended for getting final values to dump to
  18     /// the user and its use should otherwise be avoided, particularly
  19     /// given the possibility of snapshots and rollbacks.
  20     ///
  21     /// See also `InferenceTable::canonicalize`, which -- during real
  22     /// processing -- is often used to capture the "current state" of
  23     /// variables.
  24     pub fn normalize_deep<T: Fold<I>>(
  25         table: &mut InferenceTable<I>,
  26         interner: &I,
  27         value: &T,
  28     ) -> T::Result {
  29         value
  30             .fold_with(
  31                 &mut DeepNormalizer { interner, table },
  32                 DebruijnIndex::INNERMOST,
  33             )
  34             .unwrap()
  35     }
  36 }
  37
  38 impl<'i, I: Interner> Folder<'i, I> for DeepNormalizer<'_, 'i, I>
  39 where
  40     I: 'i,
  41 {
  42     fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
  43         self
  44     }
  45
  46     fn fold_inference_ty(
  47         &mut self,
  48         var: InferenceVar,
  49         kind: TyKind,
  50         _outer_binder: DebruijnIndex,
  51     ) -> Fallible<Ty<I>> {
  52         let interner = self.interner;
  53         match self.table.probe_var(var) {
  54             Some(ty) => Ok(ty
  55                 .assert_ty_ref(interner)
  56                 .fold_with(self, DebruijnIndex::INNERMOST)?
  57                 .shifted_in(interner)), // FIXME shift
  58             None => Ok(var.to_ty(interner, kind)),
  59         }
  60     }
  61
  62     fn fold_inference_lifetime(
  63         &mut self,
  64         var: InferenceVar,
  65         _outer_binder: DebruijnIndex,
  66     ) -> Fallible<Lifetime<I>> {
  67         let interner = self.interner;
  68         match self.table.probe_var(var) {
  69             Some(l) => Ok(l
  70                 .assert_lifetime_ref(interner)
  71                 .fold_with(self, DebruijnIndex::INNERMOST)?
  72                 .shifted_in(interner)),
  73             None => Ok(var.to_lifetime(interner)), // FIXME shift
  74         }
  75     }
  76
  77     fn fold_inference_const(
  78         &mut self,
  79         ty: &Ty<I>,
  80         var: InferenceVar,
  81         _outer_binder: DebruijnIndex,
  82     ) -> Fallible<Const<I>> {
  83         let interner = self.interner;
  84         match self.table.probe_var(var) {
  85             Some(c) => Ok(c
  86                 .assert_const_ref(interner)
  87                 .fold_with(self, DebruijnIndex::INNERMOST)?
  88                 .shifted_in(interner)),
  89             None => Ok(var.to_const(interner, ty.clone())), // FIXME shift
  90         }
  91     }
  92
  93     fn forbid_free_vars(&self) -> bool {
  94         true
  95     }
  96
  97     fn interner(&self) -> &'i I {
  98         self.interner
  99     }
 100
 101     fn target_interner(&self) -> &'i I {
 102         self.interner()
 103     }
 104 }
 105
 106 #[cfg(test)]
 107 mod test {
 108     use super::*;
 109     use chalk_integration::interner::ChalkIr;
 110     use chalk_integration::{arg, ty, ty_name};
 111
 112     const U0: UniverseIndex = UniverseIndex { counter: 0 };
 113
 114     #[test]
 115     fn infer() {
 116         let interner = &ChalkIr;
 117         let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
 118         let environment0 = Environment::new(interner);
 119         let a = table.new_variable(U0).to_ty(interner);
 120         let b = table.new_variable(U0).to_ty(interner);
 121         table
 122             .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
 123             .unwrap();
 124         assert_eq!(
 125             DeepNormalizer::normalize_deep(&mut table, interner, &a),
 126             ty!(apply (item 0) (expr b))
 127         );
 128         table
 129             .unify(interner, &environment0, &b, &ty!(apply (item 1)))
 130             .unwrap();
 131         assert_eq!(
 132             DeepNormalizer::normalize_deep(&mut table, interner, &a),
 133             ty!(apply (item 0) (apply (item 1)))
 134         );
 135     }
 136 }