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