Implement `Min` trait in new solver

This commit is contained in:
Deadbeef 2024-06-24 16:25:17 +00:00
parent 72e8244e64
commit c7d27a15d0
10 changed files with 182 additions and 5 deletions

View File

@ -122,7 +122,7 @@ fn gather_explicit_predicates_of(tcx: TyCtxt<'_>, def_id: LocalDefId) -> ty::Gen
let identity_args = ty::GenericArgs::identity_for_item(tcx, def_id);
let preds = tcx.explicit_predicates_of(parent);
predicates.extend(preds.instantiate_own(tcx, identity_args));
if let ty::AssocItemContainer::TraitContainer = tcx.associated_item(def_id).container {
// for traits, emit `type Effects: TyCompat<<(T1::Effects, ..) as Min>::Output>`
// TODO do the same for impls

View File

@ -598,6 +598,11 @@ fn trait_lang_item_to_lang_item(lang_item: TraitSolverLangItem) -> LangItem {
TraitSolverLangItem::Destruct => LangItem::Destruct,
TraitSolverLangItem::DiscriminantKind => LangItem::DiscriminantKind,
TraitSolverLangItem::DynMetadata => LangItem::DynMetadata,
TraitSolverLangItem::EffectsMaybe => LangItem::EffectsMaybe,
TraitSolverLangItem::EffectsMin => LangItem::EffectsMin,
TraitSolverLangItem::EffectsMinOutput => LangItem::EffectsMinOutput,
TraitSolverLangItem::EffectsNoRuntime => LangItem::EffectsNoRuntime,
TraitSolverLangItem::EffectsRuntime => LangItem::EffectsRuntime,
TraitSolverLangItem::FnPtrTrait => LangItem::FnPtrTrait,
TraitSolverLangItem::FusedIterator => LangItem::FusedIterator,
TraitSolverLangItem::Future => LangItem::Future,

View File

@ -269,6 +269,11 @@ where
ecx: &mut EvalCtxt<'_, D>,
goal: Goal<I, Self>,
) -> Vec<Candidate<I>>;
fn consider_builtin_effects_min_candidate(
ecx: &mut EvalCtxt<'_, D>,
goal: Goal<I, Self>,
) -> Result<Candidate<I>, NoSolution>;
}
impl<D, I> EvalCtxt<'_, D>
@ -420,6 +425,8 @@ where
G::consider_builtin_destruct_candidate(self, goal)
} else if cx.is_lang_item(trait_def_id, TraitSolverLangItem::TransmuteTrait) {
G::consider_builtin_transmute_candidate(self, goal)
} else if tcx.is_lang_item(trait_def_id, TraitSolverLangItem::EffectsMin) {
G::consider_builtin_effects_min_candidate(self, goal)
} else {
Err(NoSolution)
};

View File

@ -864,6 +864,65 @@ where
) -> Result<Candidate<I>, NoSolution> {
panic!("`BikeshedIntrinsicFrom` does not have an associated type: {:?}", goal)
}
fn consider_builtin_effects_min_candidate(
ecx: &mut EvalCtxt<'_, D>,
goal: Goal<I, Self>,
) -> Result<Candidate<I>, NoSolution> {
let ty::Tuple(types) = goal.predicate.self_ty().kind() else {
return Err(NoSolution);
};
let cx = ecx.cx();
let mut first_non_maybe = None;
let mut non_maybe_count = 0;
for ty in types {
if !matches!(ty::EffectKind::try_from_ty(cx, ty), Some(ty::EffectKind::Maybe)) {
first_non_maybe.get_or_insert(ty);
non_maybe_count += 1;
}
}
match non_maybe_count {
0 => {
let ty = ty::EffectKind::Maybe.to_ty(cx);
ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc).enter(|ecx| {
ecx.instantiate_normalizes_to_term(goal, ty.into());
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
1 => {
let ty = first_non_maybe.unwrap();
ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc).enter(|ecx| {
ecx.instantiate_normalizes_to_term(goal, ty.into());
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
_ => {
let mut min = ty::EffectKind::Maybe;
for ty in types {
let Some(kind) = ty::EffectKind::try_from_ty(cx, ty) else {
return Err(NoSolution);
};
let Some(result) = ty::EffectKind::min(min, kind) else {
return Err(NoSolution);
};
min = result;
}
let ty = min.to_ty(cx);
ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc).enter(|ecx| {
ecx.instantiate_normalizes_to_term(goal, ty.into());
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
}
}
}
impl<D, I> EvalCtxt<'_, D>

View File

@ -702,6 +702,47 @@ where
}
})
}
fn consider_builtin_effects_min_candidate(
ecx: &mut EvalCtxt<'_, D>,
goal: Goal<I, Self>,
) -> Result<Candidate<I>, NoSolution> {
if goal.predicate.polarity != ty::PredicatePolarity::Positive {
return Err(NoSolution);
}
let ty::Tuple(types) = goal.predicate.self_ty().kind() else {
return Err(NoSolution);
};
let cx = ecx.cx();
let maybe_count = types
.into_iter()
.filter_map(|ty| ty::EffectKind::try_from_ty(cx, ty))
.filter(|&ty| ty == ty::EffectKind::Maybe)
.count();
// Don't do concrete type check unless there are more than one type that will influence the result.
// This would allow `(Maybe, T): Min` pass even if we know nothing about `T`.
if types.len() - maybe_count > 1 {
let mut min = ty::EffectKind::Maybe;
for ty in types {
let Some(kind) = ty::EffectKind::try_from_ty(ecx.cx(), ty) else {
return Err(NoSolution);
};
let Some(result) = ty::EffectKind::min(min, kind) else {
return Err(NoSolution);
};
min = result;
}
}
ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc)
.enter(|ecx| ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes))
}
}
impl<D, I> EvalCtxt<'_, D>

View File

@ -0,0 +1,56 @@
use crate::lang_items::TraitSolverLangItem::{EffectsMaybe, EffectsRuntime, EffectsNoRuntime};
use crate::Interner;
use crate::inherent::{AdtDef, IntoKind, Ty};
#[derive(Clone, Copy, PartialEq, Eq)]
pub enum EffectKind {
Maybe,
Runtime,
NoRuntime,
}
impl EffectKind {
pub fn try_from_def_id<I: Interner>(tcx: I, def_id: I::DefId) -> Option<EffectKind> {
if tcx.is_lang_item(def_id, EffectsMaybe) {
Some(EffectKind::Maybe)
} else if tcx.is_lang_item(def_id, EffectsRuntime) {
Some(EffectKind::Runtime)
} else if tcx.is_lang_item(def_id, EffectsNoRuntime) {
Some(EffectKind::NoRuntime)
} else {
None
}
}
pub fn to_def_id<I: Interner>(self, tcx: I) -> I::DefId {
let lang_item = match self {
EffectKind::Maybe => EffectsMaybe,
EffectKind::NoRuntime => EffectsNoRuntime,
EffectKind::Runtime => EffectsRuntime,
};
tcx.require_lang_item(lang_item)
}
pub fn try_from_ty<I: Interner>(tcx: I, ty: I::Ty) -> Option<EffectKind> {
if let crate::Adt(def, _) = ty.kind() {
Self::try_from_def_id(tcx, def.def_id())
} else {
None
}
}
pub fn to_ty<I: Interner>(self, tcx: I) -> I::Ty {
I::Ty::new_adt(tcx, tcx.adt_def(self.to_def_id(tcx)), Default::default())
}
pub fn min(a: Self, b: Self) -> Option<Self> {
use EffectKind::*;
match (a, b) {
(Maybe, x) | (x, Maybe) => Some(x),
(Runtime, Runtime) => Some(Runtime),
(NoRuntime, NoRuntime) => Some(NoRuntime),
(Runtime, NoRuntime) | (NoRuntime, Runtime) => None,
}
}
}

View File

@ -17,6 +17,11 @@ pub enum TraitSolverLangItem {
Destruct,
DiscriminantKind,
DynMetadata,
EffectsMaybe,
EffectsMin,
EffectsMinOutput,
EffectsNoRuntime,
EffectsRuntime,
FnPtrTrait,
FusedIterator,
Future,

View File

@ -35,6 +35,7 @@ mod macros;
mod binder;
mod canonical;
mod const_kind;
mod effects;
mod flags;
mod generic_arg;
mod interner;
@ -51,6 +52,7 @@ pub use canonical::*;
#[cfg(feature = "nightly")]
pub use codec::*;
pub use const_kind::*;
pub use effects::*;
pub use flags::*;
pub use generic_arg::*;
pub use interner::*;

View File

@ -1054,14 +1054,15 @@ pub mod effects {
#[lang = "EffectsTyCompat"]
#[marker]
pub trait TyCompat<T> {}
pub trait TyCompat<T: ?Sized> {}
impl<T> TyCompat<T> for T {}
impl<T> TyCompat<T> for Maybe {}
impl<T: ?Sized> TyCompat<T> for T {}
impl<T: ?Sized> TyCompat<T> for Maybe {}
impl<T: ?Sized> TyCompat<Maybe> for T {}
#[lang = "EffectsMin"]
pub trait Min {
#[lang = "EffectsMinOutput"]
type Output;
type Output: ?Sized;
}
}

View File

@ -1,4 +1,5 @@
//@ run-pass
//@ compile-flags: -Znext-solver
#![feature(const_trait_impl, effects)] //~ WARN the feature `effects` is incomplete