Skip to content

Commit

Permalink
Move FnTraitPredicate and CoroutineOblig out of Clausekind (#892)
Browse files Browse the repository at this point in the history
  • Loading branch information
@nilehmann
nilehmann authored Nov 19, 2024
1 parent 7a583ef commit f80576d
Show file tree
Hide file tree
Showing 9 changed files with 242 additions and 207 deletions.
70 changes: 15 additions & 55 deletions crates/flux-fhir-analysis/src/conv/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,7 @@ impl WfckResultsProvider for WfckResults {
}
}

#[derive(Debug)]
pub(crate) struct Env {
layers: Vec<Layer>,
early_params: FxIndexMap<fhir::ParamId, Symbol>,
Expand Down Expand Up @@ -673,25 +674,13 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> {
for bound in bounds {
match bound {
fhir::GenericBound::Trait(poly_trait_ref, fhir::TraitBoundModifier::None) => {
let trait_id = poly_trait_ref.trait_def_id();
if let Some(closure_kind) = self.genv.tcx().fn_trait_kind_from_def_id(trait_id)
{
self.conv_fn_bound(
env,
&bounded_ty,
poly_trait_ref,
closure_kind,
&mut clauses,
)?;
} else {
self.conv_poly_trait_ref(
env,
bounded_ty_span,
&bounded_ty,
poly_trait_ref,
&mut clauses,
)?;
}
self.conv_poly_trait_ref(
env,
bounded_ty_span,
&bounded_ty,
poly_trait_ref,
&mut clauses,
)?;
}
fhir::GenericBound::Outlives(lft) => {
let re = self.conv_lifetime(env, *lft);
Expand Down Expand Up @@ -721,6 +710,10 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> {
poly_trait_ref: &fhir::PolyTraitRef,
clauses: &mut Vec<rty::Clause>,
) -> QueryResult {
let generic_params = &poly_trait_ref.bound_generic_params;
let layer = Layer::list(self.results(), generic_params.len() as u32, &[]);
env.push_layer(layer);

let trait_id = poly_trait_ref.trait_def_id();
let generics = self.genv.generics_of(trait_id)?;
let trait_segment = poly_trait_ref.trait_ref.last_segment();
Expand All @@ -731,8 +724,8 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> {
.into()];
self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;

let vars = poly_trait_ref
.bound_generic_params
env.pop_layer();
let vars = generic_params
.iter()
.map(|param| self.param_as_bound_var(param))
.try_collect_vec()?;
Expand Down Expand Up @@ -800,37 +793,6 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> {
Ok(())
}

fn conv_fn_bound(
&mut self,
env: &mut Env,
self_ty: &rty::Ty,
trait_ref: &fhir::PolyTraitRef,
kind: rty::ClosureKind,
clauses: &mut Vec<rty::Clause>,
) -> QueryResult {
let path = &trait_ref.trait_ref;
let layer = Layer::list(self.results(), trait_ref.bound_generic_params.len() as u32, &[]);
env.push_layer(layer);

let fhir::AssocItemConstraintKind::Equality { term } =
&path.last_segment().constraints[0].kind;

let pred = rty::FnTraitPredicate {
self_ty: self_ty.clone(),
tupled_args: self.conv_ty(env, path.last_segment().args[0].expect_type())?,
output: self.conv_ty(env, term)?,
kind,
};
// FIXME(nilehmann) We should use `tcx.late_bound_vars` here instead of trusting our lowering
let vars = trait_ref
.bound_generic_params
.iter()
.map(|param| self.param_as_bound_var(param))
.try_collect_vec()?;
clauses.push(rty::Clause::new(vars, rty::ClauseKind::FnTrait(pred)));
Ok(())
}

fn trait_defines_associated_item_named(
&self,
trait_def_id: DefId,
Expand Down Expand Up @@ -997,9 +959,7 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> {
projection_bounds.push(rty::Binder::bind_with_vars(proj, vars));
}
rty::ClauseKind::TypeOutlives(_) => {}
rty::ClauseKind::FnTrait(..)
| rty::ClauseKind::ConstArgHasType(..)
| rty::ClauseKind::CoroutineOblig(..) => {
rty::ClauseKind::ConstArgHasType(..) => {
bug!("did not expect {pred:?} clause in object bounds");
}
}
Expand Down
39 changes: 17 additions & 22 deletions crates/flux-infer/src/infer.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,7 @@ impl<'a, 'infcx, 'genv, 'tcx> InferCtxtAt<'a, 'infcx, 'genv, 'tcx> {
a: &Ty,
b: &Ty,
reason: ConstrReason,
) -> InferResult<Vec<rty::Clause>> {
) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
let mut sub = Sub::new(reason, self.span);
sub.tys(self.infcx, a, b)?;
Ok(sub.obligations)
Expand Down Expand Up @@ -441,7 +441,7 @@ struct Sub {
/// FIXME(nilehmann) This is used to store coroutine obligations generated during subtyping when
/// relating an opaque type. Other obligations related to relating opaque types are resolved
/// directly here. The implementation is really messy and we may be missing some obligations.
obligations: Vec<rty::Clause>,
obligations: Vec<Binder<rty::CoroutineObligPredicate>>,
}

impl Sub {
Expand Down Expand Up @@ -760,22 +760,17 @@ impl Sub {
);
for clause in &bounds {
if let rty::ClauseKind::Projection(pred) = clause.kind_skipping_binder() {
let ty1 = Self::project_ty(infcx, bty, pred.projection_ty.def_id)?;
let alias_ty = pred.projection_ty.with_self_ty(bty.to_subset_ty_ctor());
let ty1 = BaseTy::Alias(AliasKind::Projection, alias_ty)
.to_ty()
.normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)?;
let ty2 = pred.term.to_ty();
self.tys(infcx, &ty1, &ty2)?;
}
}
}
Ok(())
}

fn project_ty(infcx: &InferCtxt, self_ty: &BaseTy, assoc_item_id: DefId) -> InferResult<Ty> {
let args = List::singleton(GenericArg::Base(self_ty.to_subset_ty_ctor()));
let alias_ty = rty::AliasTy::new(assoc_item_id, args, List::empty());
Ok(BaseTy::Alias(AliasKind::Projection, alias_ty)
.to_ty()
.normalize_projections(infcx.genv, infcx.region_infcx, infcx.def_id)?)
}
}

fn mk_coroutine_obligations(
Expand All @@ -784,19 +779,19 @@ fn mk_coroutine_obligations(
resume_ty: &Ty,
upvar_tys: &List<Ty>,
opaque_def_id: &DefId,
) -> InferResult<Vec<rty::Clause>> {
) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
let bounds = genv.item_bounds(*opaque_def_id)?.skip_binder();
for bound in &bounds {
if let rty::ClauseKind::Projection(proj) = bound.kind_skipping_binder() {
let output = proj.term;
let pred = CoroutineObligPredicate {
def_id: *generator_did,
resume_ty: resume_ty.clone(),
upvar_tys: upvar_tys.clone(),
output: output.to_ty(),
};
let clause = rty::Clause::new(vec![], rty::ClauseKind::CoroutineOblig(pred));
return Ok(vec![clause]);
if let Some(proj_clause) = bound.as_projection_clause() {
return Ok(vec![proj_clause.map(|proj_clause| {
let output = proj_clause.term;
CoroutineObligPredicate {
def_id: *generator_did,
resume_ty: resume_ty.clone(),
upvar_tys: upvar_tys.clone(),
output: output.to_ty(),
}
})]);
}
}
bug!("no projection predicate")
Expand Down
4 changes: 2 additions & 2 deletions crates/flux-middle/src/rty/binder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,8 @@ impl<T> Binder<T> {
self.as_ref().skip_binder()
}

pub fn rebind<U>(self, value: U) -> Binder<U> {
Binder { vars: self.vars, value }
pub fn rebind<U>(&self, value: U) -> Binder<U> {
Binder { vars: self.vars.clone(), value }
}

pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U> {
Expand Down
Loading

0 comments on commit f80576d

Please sign in to comment.