1 use chalk_ir
::interner
::{HasInterner, Interner}
;
3 use chalk_ir
::{cast::Cast, fold::TypeFoldable}
;
7 pub(crate) mod instantiate
;
10 pub mod ucanonicalize
;
17 pub struct InferenceTable
<I
: Interner
> {
18 unify
: ena
::unify
::InPlaceUnificationTable
<EnaVariable
<I
>>,
19 vars
: Vec
<EnaVariable
<I
>>,
20 max_universe
: UniverseIndex
,
23 pub struct InferenceSnapshot
<I
: Interner
> {
24 unify_snapshot
: ena
::unify
::Snapshot
<ena
::unify
::InPlace
<EnaVariable
<I
>>>,
25 max_universe
: UniverseIndex
,
26 vars
: Vec
<EnaVariable
<I
>>,
29 #[allow(type_alias_bounds)]
30 pub type ParameterEnaVariable
<I
: Interner
> = WithKind
<I
, EnaVariable
<I
>>;
32 impl<I
: Interner
> InferenceTable
<I
> {
33 /// Create an empty inference table with no variables.
34 pub fn new() -> Self {
36 unify
: ena
::unify
::UnificationTable
::new(),
38 max_universe
: UniverseIndex
::root(),
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.
49 pub fn from_canonical
<T
>(
52 canonical
: Canonical
<T
>,
53 ) -> (Self, Substitution
<I
>, T
)
55 T
: HasInterner
<Interner
= I
> + TypeFoldable
<I
> + Clone
,
57 let mut table
= InferenceTable
::new();
59 assert
!(num_universes
>= 1); // always have U0
60 for _
in 1..num_universes
{
64 let subst
= table
.fresh_subst(interner
, canonical
.binders
.as_slice(interner
));
65 let value
= subst
.apply(canonical
.value
, interner
);
66 // let value = canonical.value.fold_with(&mut &subst, 0).unwrap();
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 fn new_universe(&mut self) -> UniverseIndex
{
76 let u
= self.max_universe
.next();
77 self.max_universe
= u
;
78 debug
!("created new universe: {:?}", u
);
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.
85 pub fn new_variable(&mut self, ui
: UniverseIndex
) -> EnaVariable
<I
> {
86 let var
= self.unify
.new_key(InferenceValue
::Unbound(ui
));
88 debug
!(?var
, ?ui
, "created new variable");
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
98 pub 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
;
109 /// Restore the table to the state it had when the snapshot was taken.
110 pub 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
;
116 /// Make permanent the changes made since the snapshot was taken.
117 pub fn commit(&mut self, snapshot
: InferenceSnapshot
<I
>) {
118 self.unify
.commit(snapshot
.unify_snapshot
);
121 pub fn normalize_ty_shallow(&mut self, interner
: I
, leaf
: &Ty
<I
>) -> Option
<Ty
<I
>> {
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
))
130 fn normalize_ty_shallow_inner(&mut self, interner
: I
, leaf
: &Ty
<I
>) -> Option
<Ty
<I
>> {
131 self.probe_var(leaf
.inference_var(interner
)?
)
132 .map(|p
| p
.assert_ty_ref(interner
).clone())
135 pub fn normalize_lifetime_shallow(
139 ) -> Option
<Lifetime
<I
>> {
140 self.probe_var(leaf
.inference_var(interner
)?
)
141 .map(|p
| p
.assert_lifetime_ref(interner
).clone())
144 pub fn normalize_const_shallow(&mut self, interner
: I
, leaf
: &Const
<I
>) -> Option
<Const
<I
>> {
145 self.probe_var(leaf
.inference_var(interner
)?
)
146 .map(|p
| p
.assert_const_ref(interner
).clone())
149 pub fn ty_root(&mut self, interner
: I
, leaf
: &Ty
<I
>) -> Option
<Ty
<I
>> {
152 .find(leaf
.inference_var(interner
)?
)
157 pub fn lifetime_root(&mut self, interner
: I
, leaf
: &Lifetime
<I
>) -> Option
<Lifetime
<I
>> {
160 .find(leaf
.inference_var(interner
)?
)
161 .to_lifetime(interner
),
165 /// Finds the root inference var for the given variable.
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".
171 /// This is useful for `DeepNormalizer`.
172 pub fn inference_var_root(&mut self, var
: InferenceVar
) -> InferenceVar
{
173 self.unify
.find(var
).into()
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.
178 pub fn probe_var(&mut self, leaf
: InferenceVar
) -> Option
<GenericArg
<I
>> {
179 match self.unify
.probe_value(EnaVariable
::from(leaf
)) {
180 InferenceValue
::Unbound(_
) => None
,
181 InferenceValue
::Bound(val
) => Some(val
),
185 /// Given an unbound variable, returns its universe.
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"),
198 pub trait ParameterEnaVariableExt
<I
: Interner
> {
199 fn to_generic_arg(&self, interner
: I
) -> GenericArg
<I
>;
202 impl<I
: Interner
> ParameterEnaVariableExt
<I
> for ParameterEnaVariable
<I
> {
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();
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
),