use crate::debug_span;
use chalk_ir::fold::{Fold, Folder};
use chalk_ir::interner::{HasInterner, Interner};
use chalk_ir::visit::{Visit, Visitor};
use chalk_ir::*;
use super::InferenceTable;
impl<I: Interner> InferenceTable<I> {
pub fn u_canonicalize<T>(
&mut self,
interner: &I,
value0: &Canonical<T>,
) -> UCanonicalized<T::Result>
where
T: HasInterner<Interner = I> + Fold<I> + Visit<I>,
T::Result: HasInterner<Interner = I>,
{
debug_span!("u_canonicalize", "{:#?}", value0);
let mut universes = UniverseMap::new();
for universe in value0.binders.iter(interner) {
universes.add(*universe.skip_kind());
}
value0.value.visit_with(
&mut UCollector {
universes: &mut universes,
interner,
},
DebruijnIndex::INNERMOST,
);
let value1 = value0
.value
.fold_with(
&mut UMapToCanonical {
universes: &universes,
interner,
},
DebruijnIndex::INNERMOST,
)
.unwrap();
let binders = CanonicalVarKinds::from_iter(
interner,
value0
.binders
.iter(interner)
.map(|pk| pk.map_ref(|&ui| universes.map_universe_to_canonical(ui).unwrap())),
);
UCanonicalized {
quantified: UCanonical {
universes: universes.num_canonical_universes(),
canonical: Canonical {
value: value1,
binders,
},
},
universes,
}
}
}
#[derive(Debug)]
pub struct UCanonicalized<T: HasInterner> {
pub quantified: UCanonical<T>,
pub universes: UniverseMap,
}
pub trait UniverseMapExt {
fn add(&mut self, universe: UniverseIndex);
fn map_universe_to_canonical(&self, universe: UniverseIndex) -> Option<UniverseIndex>;
fn map_universe_from_canonical(&self, universe: UniverseIndex) -> UniverseIndex;
fn map_from_canonical<T, I>(
&self,
interner: &I,
canonical_value: &Canonical<T>,
) -> Canonical<T::Result>
where
T: Fold<I> + HasInterner<Interner = I>,
T::Result: HasInterner<Interner = I>,
I: Interner;
}
impl UniverseMapExt for UniverseMap {
fn add(&mut self, universe: UniverseIndex) {
if let Err(i) = self.universes.binary_search(&universe) {
self.universes.insert(i, universe);
}
}
fn map_universe_to_canonical(&self, universe: UniverseIndex) -> Option<UniverseIndex> {
self.universes
.binary_search(&universe)
.ok()
.map(|index| UniverseIndex { counter: index })
}
fn map_universe_from_canonical(&self, universe: UniverseIndex) -> UniverseIndex {
if universe.counter < self.universes.len() {
self.universes[universe.counter]
} else {
let difference = universe.counter - self.universes.len();
let max_counter = self.universes.last().unwrap().counter;
let new_counter = max_counter + difference + 1;
UniverseIndex {
counter: new_counter,
}
}
}
fn map_from_canonical<T, I>(
&self,
interner: &I,
canonical_value: &Canonical<T>,
) -> Canonical<T::Result>
where
T: Fold<I> + HasInterner<Interner = I>,
T::Result: HasInterner<Interner = I>,
I: Interner,
{
debug_span!("map_from_canonical", ?canonical_value, universes = ?self.universes);
let binders = canonical_value
.binders
.iter(interner)
.map(|cvk| cvk.map_ref(|&universe| self.map_universe_from_canonical(universe)));
let value = canonical_value
.value
.fold_with(
&mut UMapFromCanonical {
interner,
universes: self,
},
DebruijnIndex::INNERMOST,
)
.unwrap();
Canonical {
binders: CanonicalVarKinds::from_iter(interner, binders),
value,
}
}
}
struct UCollector<'q, 'i, I> {
universes: &'q mut UniverseMap,
interner: &'i I,
}
impl<'i, I: Interner> Visitor<'i, I> for UCollector<'_, 'i, I>
where
I: 'i,
{
type Result = ();
fn as_dyn(&mut self) -> &mut dyn Visitor<'i, I, Result = ()> {
self
}
fn visit_free_placeholder(&mut self, universe: PlaceholderIndex, _outer_binder: DebruijnIndex) {
self.universes.add(universe.ui);
}
fn forbid_inference_vars(&self) -> bool {
true
}
fn interner(&self) -> &'i I {
self.interner
}
}
struct UMapToCanonical<'q, I> {
interner: &'q I,
universes: &'q UniverseMap,
}
impl<'i, I: Interner> Folder<'i, I> for UMapToCanonical<'i, I>
where
I: 'i,
{
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
self
}
fn forbid_inference_vars(&self) -> bool {
true
}
fn fold_free_placeholder_ty(
&mut self,
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Ty<I>> {
let ui = self
.universes
.map_universe_to_canonical(universe0.ui)
.expect("Expected UCollector to encounter this universe");
Ok(PlaceholderIndex {
ui,
idx: universe0.idx,
}
.to_ty(self.interner()))
}
fn fold_free_placeholder_lifetime(
&mut self,
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Lifetime<I>> {
let universe = self
.universes
.map_universe_to_canonical(universe0.ui)
.expect("Expected UCollector to encounter this universe");
Ok(PlaceholderIndex {
ui: universe,
idx: universe0.idx,
}
.to_lifetime(self.interner()))
}
fn fold_free_placeholder_const(
&mut self,
ty: &Ty<I>,
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Const<I>> {
let universe = self
.universes
.map_universe_to_canonical(universe0.ui)
.expect("Expected UCollector to encounter this universe");
Ok(PlaceholderIndex {
ui: universe,
idx: universe0.idx,
}
.to_const(self.interner(), ty.clone()))
}
fn interner(&self) -> &'i I {
self.interner
}
fn target_interner(&self) -> &'i I {
self.interner()
}
}
struct UMapFromCanonical<'q, I> {
interner: &'q I,
universes: &'q UniverseMap,
}
impl<'i, I: Interner> Folder<'i, I> for UMapFromCanonical<'i, I>
where
I: 'i,
{
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
self
}
fn fold_free_placeholder_ty(
&mut self,
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Ty<I>> {
let ui = self.universes.map_universe_from_canonical(universe0.ui);
Ok(PlaceholderIndex {
ui,
idx: universe0.idx,
}
.to_ty(self.interner()))
}
fn fold_free_placeholder_lifetime(
&mut self,
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Lifetime<I>> {
let universe = self.universes.map_universe_from_canonical(universe0.ui);
Ok(PlaceholderIndex {
ui: universe,
idx: universe0.idx,
}
.to_lifetime(self.interner()))
}
fn forbid_inference_vars(&self) -> bool {
true
}
fn interner(&self) -> &'i I {
self.interner
}
fn target_interner(&self) -> &'i I {
self.interner()
}
}