1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
use chalk_ir::interner::{HasInterner, Interner};
use chalk_ir::*;
use chalk_ir::{cast::Cast, fold::TypeFoldable};
use tracing::debug;

mod canonicalize;
pub(crate) mod instantiate;
mod invert;
mod test;
pub mod ucanonicalize;
pub mod unify;
mod var;

use self::var::*;

#[derive(Clone)]
pub struct InferenceTable<I: Interner> {
    unify: ena::unify::InPlaceUnificationTable<EnaVariable<I>>,
    vars: Vec<EnaVariable<I>>,
    max_universe: UniverseIndex,
}

pub struct InferenceSnapshot<I: Interner> {
    unify_snapshot: ena::unify::Snapshot<ena::unify::InPlace<EnaVariable<I>>>,
    max_universe: UniverseIndex,
    vars: Vec<EnaVariable<I>>,
}

#[allow(type_alias_bounds)]
pub type ParameterEnaVariable<I: Interner> = WithKind<I, EnaVariable<I>>;

impl<I: Interner> InferenceTable<I> {
    /// Create an empty inference table with no variables.
    pub fn new() -> Self {
        InferenceTable {
            unify: ena::unify::UnificationTable::new(),
            vars: vec![],
            max_universe: UniverseIndex::root(),
        }
    }

    /// Creates a new inference table, pre-populated with
    /// `num_universes` fresh universes. Instantiates the canonical
    /// value `canonical` within those universes (which must not
    /// reference any universe greater than `num_universes`). Returns
    /// the substitution mapping from each canonical binder to its
    /// corresponding existential variable, along with the
    /// instantiated result.
    pub fn from_canonical<T>(
        interner: I,
        num_universes: usize,
        canonical: Canonical<T>,
    ) -> (Self, Substitution<I>, T)
    where
        T: HasInterner<Interner = I> + TypeFoldable<I> + Clone,
    {
        let mut table = InferenceTable::new();

        assert!(num_universes >= 1); // always have U0
        for _ in 1..num_universes {
            table.new_universe();
        }

        let subst = table.fresh_subst(interner, canonical.binders.as_slice(interner));
        let value = subst.apply(canonical.value, interner);
        // let value = canonical.value.fold_with(&mut &subst, 0).unwrap();

        (table, subst, value)
    }

    /// Creates and returns a fresh universe that is distinct from all
    /// others created within this inference table. This universe is
    /// able to see all previously created universes (though hopefully
    /// it is only brought into contact with its logical *parents*).
    pub fn new_universe(&mut self) -> UniverseIndex {
        let u = self.max_universe.next();
        self.max_universe = u;
        debug!("created new universe: {:?}", u);
        u
    }

    /// Creates a new inference variable and returns its index. The
    /// kind of the variable should be known by the caller, but is not
    /// tracked directly by the inference table.
    pub fn new_variable(&mut self, ui: UniverseIndex) -> EnaVariable<I> {
        let var = self.unify.new_key(InferenceValue::Unbound(ui));
        self.vars.push(var);
        debug!(?var, ?ui, "created new variable");
        var
    }

    /// Takes a "snapshot" of the current state of the inference
    /// table.  Later, you must invoke either `rollback_to` or
    /// `commit` with that snapshot.  Snapshots can be nested, but you
    /// must respect a stack discipline (i.e., rollback or commit
    /// snapshots in reverse order of that with which they were
    /// created).
    pub fn snapshot(&mut self) -> InferenceSnapshot<I> {
        let unify_snapshot = self.unify.snapshot();
        let vars = self.vars.clone();
        let max_universe = self.max_universe;
        InferenceSnapshot {
            unify_snapshot,
            max_universe,
            vars,
        }
    }

    /// Restore the table to the state it had when the snapshot was taken.
    pub fn rollback_to(&mut self, snapshot: InferenceSnapshot<I>) {
        self.unify.rollback_to(snapshot.unify_snapshot);
        self.vars = snapshot.vars;
        self.max_universe = snapshot.max_universe;
    }

    /// Make permanent the changes made since the snapshot was taken.
    pub fn commit(&mut self, snapshot: InferenceSnapshot<I>) {
        self.unify.commit(snapshot.unify_snapshot);
    }

    pub fn normalize_ty_shallow(&mut self, interner: I, leaf: &Ty<I>) -> Option<Ty<I>> {
        // An integer/float type variable will never normalize to another
        // variable; but a general type variable might normalize to an
        // integer/float variable. So we potentially need to normalize twice to
        // get at the actual value.
        self.normalize_ty_shallow_inner(interner, leaf)
            .map(|ty| self.normalize_ty_shallow_inner(interner, &ty).unwrap_or(ty))
    }

    fn normalize_ty_shallow_inner(&mut self, interner: I, leaf: &Ty<I>) -> Option<Ty<I>> {
        self.probe_var(leaf.inference_var(interner)?)
            .map(|p| p.assert_ty_ref(interner).clone())
    }

    pub fn normalize_lifetime_shallow(
        &mut self,
        interner: I,
        leaf: &Lifetime<I>,
    ) -> Option<Lifetime<I>> {
        self.probe_var(leaf.inference_var(interner)?)
            .map(|p| p.assert_lifetime_ref(interner).clone())
    }

    pub fn normalize_const_shallow(&mut self, interner: I, leaf: &Const<I>) -> Option<Const<I>> {
        self.probe_var(leaf.inference_var(interner)?)
            .map(|p| p.assert_const_ref(interner).clone())
    }

    pub fn ty_root(&mut self, interner: I, leaf: &Ty<I>) -> Option<Ty<I>> {
        Some(
            self.unify
                .find(leaf.inference_var(interner)?)
                .to_ty(interner),
        )
    }

    pub fn lifetime_root(&mut self, interner: I, leaf: &Lifetime<I>) -> Option<Lifetime<I>> {
        Some(
            self.unify
                .find(leaf.inference_var(interner)?)
                .to_lifetime(interner),
        )
    }

    /// Finds the root inference var for the given variable.
    ///
    /// The returned variable will be exactly equivalent to the given
    /// variable except in name. All variables which have been unified to
    /// eachother (but don't yet have a value) have the same "root".
    ///
    /// This is useful for `DeepNormalizer`.
    pub fn inference_var_root(&mut self, var: InferenceVar) -> InferenceVar {
        self.unify.find(var).into()
    }

    /// If type `leaf` is a free inference variable, and that variable has been
    /// bound, returns `Some(P)` where `P` is the parameter to which it has been bound.
    pub fn probe_var(&mut self, leaf: InferenceVar) -> Option<GenericArg<I>> {
        match self.unify.probe_value(EnaVariable::from(leaf)) {
            InferenceValue::Unbound(_) => None,
            InferenceValue::Bound(val) => Some(val),
        }
    }

    /// Given an unbound variable, returns its universe.
    ///
    /// # Panics
    ///
    /// Panics if the variable is bound.
    fn universe_of_unbound_var(&mut self, var: EnaVariable<I>) -> UniverseIndex {
        match self.unify.probe_value(var) {
            InferenceValue::Unbound(ui) => ui,
            InferenceValue::Bound(_) => panic!("var_universe invoked on bound variable"),
        }
    }
}

pub trait ParameterEnaVariableExt<I: Interner> {
    fn to_generic_arg(&self, interner: I) -> GenericArg<I>;
}

impl<I: Interner> ParameterEnaVariableExt<I> for ParameterEnaVariable<I> {
    fn to_generic_arg(&self, interner: I) -> GenericArg<I> {
        // we are matching on kind, so skipping it is fine
        let ena_variable = self.skip_kind();
        match &self.kind {
            VariableKind::Ty(kind) => ena_variable.to_ty_with_kind(interner, *kind).cast(interner),
            VariableKind::Lifetime => ena_variable.to_lifetime(interner).cast(interner),
            VariableKind::Const(ty) => ena_variable.to_const(interner, ty.clone()).cast(interner),
        }
    }
}