2019-04-20 12:34:36 +02:00
|
|
|
//! Unification and canonicalization logic.
|
|
|
|
|
2021-04-11 11:20:45 +02:00
|
|
|
use std::{borrow::Cow, fmt, sync::Arc};
|
2019-12-01 20:30:28 +01:00
|
|
|
|
2021-04-03 17:49:29 +02:00
|
|
|
use chalk_ir::{
|
2021-05-15 23:09:18 +02:00
|
|
|
cast::Cast, fold::Fold, interner::HasInterner, zip::Zip, FloatTy, IntTy, TyVariableKind,
|
|
|
|
UniverseIndex,
|
2021-04-03 17:49:29 +02:00
|
|
|
};
|
2021-04-11 11:20:45 +02:00
|
|
|
use chalk_solve::infer::ParameterEnaVariableExt;
|
|
|
|
use ena::unify::UnifyKey;
|
2019-12-01 20:30:28 +01:00
|
|
|
|
2021-05-01 21:53:10 +02:00
|
|
|
use super::{InferOk, InferResult, InferenceContext, TypeError};
|
2020-04-05 18:24:18 +02:00
|
|
|
use crate::{
|
2021-04-11 11:20:45 +02:00
|
|
|
db::HirDatabase, fold_tys, static_lifetime, BoundVar, Canonical, DebruijnIndex, GenericArg,
|
2021-05-09 20:06:24 +02:00
|
|
|
InferenceVar, Interner, Scalar, Substitution, TraitEnvironment, Ty, TyKind, VariableKind,
|
2020-04-05 18:24:18 +02:00
|
|
|
};
|
2019-04-20 12:34:36 +02:00
|
|
|
|
2020-03-13 16:05:46 +01:00
|
|
|
impl<'a> InferenceContext<'a> {
|
2021-04-11 11:20:45 +02:00
|
|
|
pub(super) fn canonicalize<T: Fold<Interner> + HasInterner<Interner = Interner>>(
|
|
|
|
&mut self,
|
|
|
|
t: T,
|
|
|
|
) -> Canonicalized<T::Result>
|
2019-04-20 12:34:36 +02:00
|
|
|
where
|
2021-04-11 11:20:45 +02:00
|
|
|
T::Result: HasInterner<Interner = Interner>,
|
2019-04-20 12:34:36 +02:00
|
|
|
{
|
2021-04-11 11:20:45 +02:00
|
|
|
let result = self.table.var_unification_table.canonicalize(&Interner, t);
|
|
|
|
let free_vars = result
|
|
|
|
.free_vars
|
|
|
|
.into_iter()
|
|
|
|
.map(|free_var| free_var.to_generic_arg(&Interner))
|
|
|
|
.collect();
|
|
|
|
Canonicalized { value: result.quantified, free_vars }
|
2019-04-20 12:34:36 +02:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-04-10 17:44:43 +02:00
|
|
|
#[derive(Debug)]
|
2021-04-03 17:49:29 +02:00
|
|
|
pub(super) struct Canonicalized<T>
|
|
|
|
where
|
|
|
|
T: HasInterner<Interner = Interner>,
|
|
|
|
{
|
2020-11-02 16:31:38 +01:00
|
|
|
pub(super) value: Canonical<T>,
|
2021-04-11 11:20:45 +02:00
|
|
|
free_vars: Vec<GenericArg>,
|
2019-05-04 15:42:00 +02:00
|
|
|
}
|
|
|
|
|
2021-04-03 17:49:29 +02:00
|
|
|
impl<T: HasInterner<Interner = Interner>> Canonicalized<T> {
|
2021-04-05 18:54:31 +02:00
|
|
|
pub(super) fn decanonicalize_ty(&self, ty: Ty) -> Ty {
|
2021-05-15 23:09:18 +02:00
|
|
|
chalk_ir::Substitute::apply(&self.free_vars, ty, &Interner)
|
2019-05-01 17:57:56 +02:00
|
|
|
}
|
|
|
|
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(super) fn apply_solution(
|
|
|
|
&self,
|
|
|
|
ctx: &mut InferenceContext<'_>,
|
2021-03-15 21:02:34 +01:00
|
|
|
solution: Canonical<Substitution>,
|
2020-11-02 13:13:32 +01:00
|
|
|
) {
|
2019-04-20 12:34:36 +02:00
|
|
|
// the solution may contain new variables, which we need to convert to new inference vars
|
2021-04-01 21:04:02 +02:00
|
|
|
let new_vars = Substitution::from_iter(
|
|
|
|
&Interner,
|
|
|
|
solution.binders.iter(&Interner).map(|k| match k.kind {
|
2021-04-08 13:58:03 +02:00
|
|
|
VariableKind::Ty(TyVariableKind::General) => {
|
|
|
|
ctx.table.new_type_var().cast(&Interner)
|
|
|
|
}
|
|
|
|
VariableKind::Ty(TyVariableKind::Integer) => {
|
|
|
|
ctx.table.new_integer_var().cast(&Interner)
|
|
|
|
}
|
|
|
|
VariableKind::Ty(TyVariableKind::Float) => {
|
|
|
|
ctx.table.new_float_var().cast(&Interner)
|
|
|
|
}
|
|
|
|
// Chalk can sometimes return new lifetime variables. We just use the static lifetime everywhere
|
|
|
|
VariableKind::Lifetime => static_lifetime().cast(&Interner),
|
2021-04-01 21:04:02 +02:00
|
|
|
_ => panic!("const variable in solution"),
|
|
|
|
}),
|
2020-06-28 21:17:27 +02:00
|
|
|
);
|
2021-05-15 23:09:18 +02:00
|
|
|
for (i, v) in solution.value.iter(&Interner).enumerate() {
|
2021-05-01 21:53:10 +02:00
|
|
|
let var = self.free_vars[i].clone();
|
2021-05-15 23:09:18 +02:00
|
|
|
if let Some(ty) = v.ty(&Interner) {
|
|
|
|
// eagerly replace projections in the type; we may be getting types
|
|
|
|
// e.g. from where clauses where this hasn't happened yet
|
|
|
|
let ty = ctx.normalize_associated_types_in(new_vars.apply(ty.clone(), &Interner));
|
|
|
|
ctx.table.unify(var.assert_ty_ref(&Interner), &ty);
|
|
|
|
} else {
|
|
|
|
let _ = ctx.table.unify_inner(&var, &new_vars.apply(v.clone(), &Interner));
|
|
|
|
}
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-05-15 20:28:07 +02:00
|
|
|
pub fn could_unify(
|
|
|
|
db: &dyn HirDatabase,
|
|
|
|
env: Arc<TraitEnvironment>,
|
|
|
|
tys: &Canonical<(Ty, Ty)>,
|
|
|
|
) -> bool {
|
|
|
|
unify(db, env, tys).is_some()
|
2021-03-16 08:45:46 -07:00
|
|
|
}
|
|
|
|
|
2021-04-11 11:20:45 +02:00
|
|
|
pub(crate) fn unify(
|
|
|
|
db: &dyn HirDatabase,
|
|
|
|
env: Arc<TraitEnvironment>,
|
|
|
|
tys: &Canonical<(Ty, Ty)>,
|
|
|
|
) -> Option<Substitution> {
|
|
|
|
let mut table = InferenceTable::new(db, env);
|
2021-04-01 21:04:02 +02:00
|
|
|
let vars = Substitution::from_iter(
|
|
|
|
&Interner,
|
2021-03-21 20:05:38 +01:00
|
|
|
tys.binders
|
|
|
|
.iter(&Interner)
|
2020-06-28 21:17:27 +02:00
|
|
|
// we always use type vars here because we want everything to
|
|
|
|
// fallback to Unknown in the end (kind of hacky, as below)
|
2021-04-01 21:04:02 +02:00
|
|
|
.map(|_| table.new_type_var()),
|
2020-06-28 21:17:27 +02:00
|
|
|
);
|
2021-04-05 19:01:41 +02:00
|
|
|
let ty1_with_vars = vars.apply(tys.value.0.clone(), &Interner);
|
|
|
|
let ty2_with_vars = vars.apply(tys.value.1.clone(), &Interner);
|
2020-03-01 14:31:35 +01:00
|
|
|
if !table.unify(&ty1_with_vars, &ty2_with_vars) {
|
2019-12-01 22:14:28 +01:00
|
|
|
return None;
|
|
|
|
}
|
2020-03-01 14:31:35 +01:00
|
|
|
// default any type vars that weren't unified back to their original bound vars
|
|
|
|
// (kind of hacky)
|
2021-05-09 20:06:24 +02:00
|
|
|
let find_var = |iv| {
|
|
|
|
vars.iter(&Interner).position(|v| match v.interned() {
|
|
|
|
chalk_ir::GenericArgData::Ty(ty) => ty.inference_var(&Interner),
|
|
|
|
chalk_ir::GenericArgData::Lifetime(lt) => lt.inference_var(&Interner),
|
|
|
|
chalk_ir::GenericArgData::Const(c) => c.inference_var(&Interner),
|
|
|
|
} == Some(iv))
|
|
|
|
};
|
2021-05-13 19:44:29 +02:00
|
|
|
let fallback = |iv, kind, default, binder| match kind {
|
|
|
|
chalk_ir::VariableKind::Ty(_ty_kind) => find_var(iv)
|
|
|
|
.map_or(default, |i| BoundVar::new(binder, i).to_ty(&Interner).cast(&Interner)),
|
|
|
|
chalk_ir::VariableKind::Lifetime => find_var(iv)
|
|
|
|
.map_or(default, |i| BoundVar::new(binder, i).to_lifetime(&Interner).cast(&Interner)),
|
|
|
|
chalk_ir::VariableKind::Const(ty) => find_var(iv)
|
|
|
|
.map_or(default, |i| BoundVar::new(binder, i).to_const(&Interner, ty).cast(&Interner)),
|
2021-05-09 20:06:24 +02:00
|
|
|
};
|
2021-04-04 12:48:10 +02:00
|
|
|
Some(Substitution::from_iter(
|
|
|
|
&Interner,
|
|
|
|
vars.iter(&Interner)
|
2021-05-09 20:06:24 +02:00
|
|
|
.map(|v| table.resolve_with_fallback(v.assert_ty_ref(&Interner).clone(), fallback)),
|
2021-04-04 12:48:10 +02:00
|
|
|
))
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2021-03-01 12:35:11 +01:00
|
|
|
#[derive(Clone, Debug)]
|
|
|
|
pub(super) struct TypeVariableTable {
|
|
|
|
inner: Vec<TypeVariableData>,
|
|
|
|
}
|
|
|
|
|
|
|
|
impl TypeVariableTable {
|
|
|
|
pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
|
2021-04-11 11:20:45 +02:00
|
|
|
self.inner[iv.index() as usize].diverging = diverging;
|
2021-03-01 12:35:11 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty {
|
|
|
|
match kind {
|
2021-05-15 21:30:40 +02:00
|
|
|
_ if self.inner.get(iv.index() as usize).map_or(false, |data| data.diverging) => {
|
|
|
|
TyKind::Never
|
|
|
|
}
|
2021-04-05 15:37:11 +03:00
|
|
|
TyVariableKind::General => TyKind::Error,
|
2021-03-13 14:44:51 +01:00
|
|
|
TyVariableKind::Integer => TyKind::Scalar(Scalar::Int(IntTy::I32)),
|
|
|
|
TyVariableKind::Float => TyKind::Scalar(Scalar::Float(FloatTy::F64)),
|
2021-03-01 12:35:11 +01:00
|
|
|
}
|
2021-03-13 14:44:51 +01:00
|
|
|
.intern(&Interner)
|
2021-03-01 12:35:11 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
#[derive(Copy, Clone, Debug)]
|
|
|
|
pub(crate) struct TypeVariableData {
|
|
|
|
diverging: bool,
|
|
|
|
}
|
|
|
|
|
2021-04-11 11:20:45 +02:00
|
|
|
type ChalkInferenceTable = chalk_solve::infer::InferenceTable<Interner>;
|
|
|
|
|
|
|
|
#[derive(Clone)]
|
|
|
|
pub(crate) struct InferenceTable<'a> {
|
|
|
|
db: &'a dyn HirDatabase,
|
|
|
|
trait_env: Arc<TraitEnvironment>,
|
|
|
|
pub(super) var_unification_table: ChalkInferenceTable,
|
2021-03-01 12:35:11 +01:00
|
|
|
pub(super) type_variable_table: TypeVariableTable,
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2021-04-11 11:20:45 +02:00
|
|
|
impl<'a> InferenceTable<'a> {
|
|
|
|
pub(crate) fn new(db: &'a dyn HirDatabase, trait_env: Arc<TraitEnvironment>) -> Self {
|
2021-03-01 12:35:11 +01:00
|
|
|
InferenceTable {
|
2021-04-11 11:20:45 +02:00
|
|
|
db,
|
|
|
|
trait_env,
|
|
|
|
var_unification_table: ChalkInferenceTable::new(),
|
2021-03-01 12:35:11 +01:00
|
|
|
type_variable_table: TypeVariableTable { inner: Vec::new() },
|
|
|
|
}
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2021-05-15 19:28:58 +02:00
|
|
|
/// Chalk doesn't know about the `diverging` flag, so when it unifies two
|
|
|
|
/// type variables of which one is diverging, the chosen root might not be
|
|
|
|
/// diverging and we have no way of marking it as such at that time. This
|
|
|
|
/// function goes through all type variables and make sure their root is
|
|
|
|
/// marked as diverging if necessary, so that resolving them gives the right
|
|
|
|
/// result.
|
|
|
|
pub(super) fn propagate_diverging_flag(&mut self) {
|
|
|
|
for i in 0..self.type_variable_table.inner.len() {
|
|
|
|
if !self.type_variable_table.inner[i].diverging {
|
|
|
|
continue;
|
|
|
|
}
|
|
|
|
let v = InferenceVar::from(i as u32);
|
|
|
|
let root = self.var_unification_table.inference_var_root(v);
|
|
|
|
if let Some(data) = self.type_variable_table.inner.get_mut(root.index() as usize) {
|
|
|
|
data.diverging = true;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-03-01 13:54:17 +01:00
|
|
|
fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty {
|
2021-04-11 11:20:45 +02:00
|
|
|
let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
|
2021-05-15 19:28:58 +02:00
|
|
|
// Chalk might have created some type variables for its own purposes that we don't know about...
|
2021-05-15 21:30:40 +02:00
|
|
|
// TODO refactor this?
|
2021-04-11 11:20:45 +02:00
|
|
|
self.type_variable_table.inner.extend(
|
|
|
|
(0..1 + var.index() as usize - self.type_variable_table.inner.len())
|
|
|
|
.map(|_| TypeVariableData { diverging: false }),
|
|
|
|
);
|
|
|
|
assert_eq!(var.index() as usize, self.type_variable_table.inner.len() - 1);
|
|
|
|
self.type_variable_table.inner[var.index() as usize].diverging = diverging;
|
|
|
|
var.to_ty_with_kind(&Interner, kind)
|
2021-03-01 13:54:17 +01:00
|
|
|
}
|
|
|
|
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn new_type_var(&mut self) -> Ty {
|
2021-03-01 13:54:17 +01:00
|
|
|
self.new_var(TyVariableKind::General, false)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn new_integer_var(&mut self) -> Ty {
|
2021-03-01 13:54:17 +01:00
|
|
|
self.new_var(TyVariableKind::Integer, false)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn new_float_var(&mut self) -> Ty {
|
2021-03-01 13:54:17 +01:00
|
|
|
self.new_var(TyVariableKind::Float, false)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2021-03-01 12:35:11 +01:00
|
|
|
pub(crate) fn new_maybe_never_var(&mut self) -> Ty {
|
2021-03-01 13:54:17 +01:00
|
|
|
self.new_var(TyVariableKind::General, true)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2021-05-09 20:06:24 +02:00
|
|
|
pub(crate) fn resolve_with_fallback<T>(
|
|
|
|
&mut self,
|
|
|
|
t: T,
|
2021-05-13 19:44:29 +02:00
|
|
|
fallback: impl Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
|
2021-05-09 20:06:24 +02:00
|
|
|
) -> T::Result
|
|
|
|
where
|
|
|
|
T: HasInterner<Interner = Interner> + Fold<Interner>,
|
|
|
|
{
|
|
|
|
self.resolve_with_fallback_inner(&mut Vec::new(), t, &fallback)
|
|
|
|
}
|
|
|
|
|
|
|
|
fn resolve_with_fallback_inner<T>(
|
|
|
|
&mut self,
|
|
|
|
var_stack: &mut Vec<InferenceVar>,
|
|
|
|
t: T,
|
2021-05-13 19:44:29 +02:00
|
|
|
fallback: &impl Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
|
2021-05-09 20:06:24 +02:00
|
|
|
) -> T::Result
|
|
|
|
where
|
|
|
|
T: HasInterner<Interner = Interner> + Fold<Interner>,
|
|
|
|
{
|
2021-05-13 19:44:29 +02:00
|
|
|
t.fold_with(
|
|
|
|
&mut resolve::Resolver {
|
|
|
|
type_variable_table: &self.type_variable_table,
|
|
|
|
var_unification_table: &mut self.var_unification_table,
|
|
|
|
var_stack,
|
|
|
|
fallback,
|
2021-05-09 20:06:24 +02:00
|
|
|
},
|
|
|
|
DebruijnIndex::INNERMOST,
|
|
|
|
)
|
2021-05-13 19:44:29 +02:00
|
|
|
.expect("fold failed unexpectedly")
|
2021-05-09 20:06:24 +02:00
|
|
|
}
|
|
|
|
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn resolve_ty_completely(&mut self, ty: Ty) -> Ty {
|
2021-05-13 19:44:29 +02:00
|
|
|
self.resolve_with_fallback(ty, |_, _, d, _| d)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
2021-04-11 11:20:45 +02:00
|
|
|
// FIXME get rid of this, instead resolve shallowly where necessary
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn resolve_ty_as_possible(&mut self, ty: Ty) -> Ty {
|
2019-12-01 20:30:28 +01:00
|
|
|
self.resolve_ty_as_possible_inner(&mut Vec::new(), ty)
|
|
|
|
}
|
|
|
|
|
2021-05-01 21:53:10 +02:00
|
|
|
/// Unify two types and register new trait goals that arise from that.
|
|
|
|
// TODO give these two functions better names
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool {
|
2021-05-02 16:20:37 +02:00
|
|
|
let _result = if let Ok(r) = self.unify_inner(ty1, ty2) {
|
2021-04-11 11:20:45 +02:00
|
|
|
r
|
2021-02-28 19:13:37 +01:00
|
|
|
} else {
|
2021-04-11 11:20:45 +02:00
|
|
|
return false;
|
|
|
|
};
|
|
|
|
// TODO deal with new goals
|
|
|
|
true
|
2020-04-17 19:41:37 +02:00
|
|
|
}
|
|
|
|
|
2021-05-01 21:53:10 +02:00
|
|
|
/// Unify two types and return new trait goals arising from it, so the
|
|
|
|
/// caller needs to deal with them.
|
2021-05-15 23:09:18 +02:00
|
|
|
pub(crate) fn unify_inner<T: Zip<Interner>>(&mut self, t1: &T, t2: &T) -> InferResult {
|
2021-05-01 21:53:10 +02:00
|
|
|
match self.var_unification_table.relate(
|
|
|
|
&Interner,
|
|
|
|
&self.db,
|
|
|
|
&self.trait_env.env,
|
|
|
|
chalk_ir::Variance::Invariant,
|
2021-05-15 23:09:18 +02:00
|
|
|
t1,
|
|
|
|
t2,
|
2021-05-01 21:53:10 +02:00
|
|
|
) {
|
2021-05-02 16:20:37 +02:00
|
|
|
Ok(_result) => {
|
2021-05-01 21:53:10 +02:00
|
|
|
// TODO deal with new goals
|
|
|
|
Ok(InferOk {})
|
|
|
|
}
|
2021-05-02 16:20:37 +02:00
|
|
|
Err(chalk_ir::NoSolution) => Err(TypeError),
|
2021-05-01 21:53:10 +02:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-12-01 20:30:28 +01:00
|
|
|
/// If `ty` is a type variable with known type, returns that type;
|
|
|
|
/// otherwise, return ty.
|
2021-04-11 11:20:45 +02:00
|
|
|
// FIXME this could probably just return Ty
|
2020-11-02 13:13:32 +01:00
|
|
|
pub(crate) fn resolve_ty_shallow<'b>(&mut self, ty: &'b Ty) -> Cow<'b, Ty> {
|
2021-04-11 11:20:45 +02:00
|
|
|
self.var_unification_table
|
|
|
|
.normalize_ty_shallow(&Interner, ty)
|
|
|
|
.map_or(Cow::Borrowed(ty), Cow::Owned)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
/// Resolves the type as far as currently possible, replacing type variables
|
2021-05-13 19:44:29 +02:00
|
|
|
/// by their known types.
|
2021-04-11 11:20:45 +02:00
|
|
|
fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<InferenceVar>, ty: Ty) -> Ty {
|
2021-04-08 13:32:48 +02:00
|
|
|
fold_tys(
|
|
|
|
ty,
|
|
|
|
|ty, _| match ty.kind(&Interner) {
|
|
|
|
&TyKind::InferenceVar(tv, kind) => {
|
2021-04-11 11:20:45 +02:00
|
|
|
if tv_stack.contains(&tv) {
|
2021-04-08 13:32:48 +02:00
|
|
|
// recursive type
|
|
|
|
return self.type_variable_table.fallback_value(tv, kind);
|
|
|
|
}
|
2021-04-11 11:20:45 +02:00
|
|
|
if let Some(known_ty) = self.var_unification_table.probe_var(tv) {
|
2021-04-08 13:32:48 +02:00
|
|
|
// known_ty may contain other variables that are known by now
|
2021-04-11 11:20:45 +02:00
|
|
|
tv_stack.push(tv);
|
|
|
|
let result = self.resolve_ty_as_possible_inner(
|
|
|
|
tv_stack,
|
|
|
|
known_ty.assert_ty_ref(&Interner).clone(),
|
|
|
|
);
|
2021-04-08 13:32:48 +02:00
|
|
|
tv_stack.pop();
|
|
|
|
result
|
|
|
|
} else {
|
|
|
|
ty
|
|
|
|
}
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
2021-04-08 13:32:48 +02:00
|
|
|
_ => ty,
|
|
|
|
},
|
|
|
|
DebruijnIndex::INNERMOST,
|
|
|
|
)
|
2019-12-01 20:30:28 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-04-11 11:20:45 +02:00
|
|
|
impl<'a> fmt::Debug for InferenceTable<'a> {
|
|
|
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
|
|
|
f.debug_struct("InferenceTable")
|
|
|
|
.field("num_vars", &self.type_variable_table.inner.len())
|
|
|
|
.finish()
|
2019-04-20 12:34:36 +02:00
|
|
|
}
|
|
|
|
}
|
2021-05-13 19:44:29 +02:00
|
|
|
|
|
|
|
mod resolve {
|
|
|
|
use super::{ChalkInferenceTable, TypeVariableTable};
|
|
|
|
use crate::{
|
|
|
|
ConcreteConst, Const, ConstData, ConstValue, DebruijnIndex, GenericArg, InferenceVar,
|
|
|
|
Interner, Ty, TyVariableKind, VariableKind,
|
|
|
|
};
|
|
|
|
use chalk_ir::{
|
|
|
|
cast::Cast,
|
|
|
|
fold::{Fold, Folder},
|
|
|
|
Fallible,
|
|
|
|
};
|
|
|
|
use hir_def::type_ref::ConstScalar;
|
|
|
|
|
|
|
|
pub(super) struct Resolver<'a, F> {
|
|
|
|
pub type_variable_table: &'a TypeVariableTable,
|
|
|
|
pub var_unification_table: &'a mut ChalkInferenceTable,
|
|
|
|
pub var_stack: &'a mut Vec<InferenceVar>,
|
|
|
|
pub fallback: F,
|
|
|
|
}
|
|
|
|
impl<'a, 'i, F> Folder<'i, Interner> for Resolver<'a, F>
|
|
|
|
where
|
|
|
|
F: Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg + 'i,
|
|
|
|
{
|
|
|
|
fn as_dyn(&mut self) -> &mut dyn Folder<'i, Interner> {
|
|
|
|
self
|
|
|
|
}
|
|
|
|
|
|
|
|
fn interner(&self) -> &'i Interner {
|
|
|
|
&Interner
|
|
|
|
}
|
|
|
|
|
|
|
|
fn fold_inference_ty(
|
|
|
|
&mut self,
|
|
|
|
var: InferenceVar,
|
|
|
|
kind: TyVariableKind,
|
|
|
|
outer_binder: DebruijnIndex,
|
|
|
|
) -> Fallible<Ty> {
|
|
|
|
let var = self.var_unification_table.inference_var_root(var);
|
|
|
|
if self.var_stack.contains(&var) {
|
|
|
|
// recursive type
|
|
|
|
let default = self.type_variable_table.fallback_value(var, kind).cast(&Interner);
|
|
|
|
return Ok((self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
|
|
|
|
.assert_ty_ref(&Interner)
|
|
|
|
.clone());
|
|
|
|
}
|
|
|
|
let result = if let Some(known_ty) = self.var_unification_table.probe_var(var) {
|
|
|
|
// known_ty may contain other variables that are known by now
|
|
|
|
self.var_stack.push(var);
|
|
|
|
let result =
|
|
|
|
known_ty.fold_with(self, outer_binder).expect("fold failed unexpectedly");
|
|
|
|
self.var_stack.pop();
|
|
|
|
result.assert_ty_ref(&Interner).clone()
|
|
|
|
} else {
|
|
|
|
let default = self.type_variable_table.fallback_value(var, kind).cast(&Interner);
|
|
|
|
(self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
|
|
|
|
.assert_ty_ref(&Interner)
|
|
|
|
.clone()
|
|
|
|
};
|
|
|
|
Ok(result)
|
|
|
|
}
|
|
|
|
|
|
|
|
fn fold_inference_const(
|
|
|
|
&mut self,
|
|
|
|
ty: Ty,
|
|
|
|
var: InferenceVar,
|
|
|
|
outer_binder: DebruijnIndex,
|
|
|
|
) -> Fallible<Const> {
|
|
|
|
let var = self.var_unification_table.inference_var_root(var);
|
|
|
|
let default = ConstData {
|
|
|
|
ty: ty.clone(),
|
|
|
|
value: ConstValue::Concrete(ConcreteConst { interned: ConstScalar::Unknown }),
|
|
|
|
}
|
|
|
|
.intern(&Interner)
|
|
|
|
.cast(&Interner);
|
|
|
|
if self.var_stack.contains(&var) {
|
|
|
|
// recursive
|
|
|
|
return Ok((self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
|
|
|
|
.assert_const_ref(&Interner)
|
|
|
|
.clone());
|
|
|
|
}
|
|
|
|
let result = if let Some(known_ty) = self.var_unification_table.probe_var(var) {
|
|
|
|
// known_ty may contain other variables that are known by now
|
|
|
|
self.var_stack.push(var);
|
|
|
|
let result =
|
|
|
|
known_ty.fold_with(self, outer_binder).expect("fold failed unexpectedly");
|
|
|
|
self.var_stack.pop();
|
|
|
|
result.assert_const_ref(&Interner).clone()
|
|
|
|
} else {
|
|
|
|
(self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
|
|
|
|
.assert_const_ref(&Interner)
|
|
|
|
.clone()
|
|
|
|
};
|
|
|
|
Ok(result)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|