vendor/chalk-solve-0.14.0/src/infer.rs

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