Skip to content

Commit

Permalink
Add type outlives constraints to fhir
Browse files Browse the repository at this point in the history
  • Loading branch information
nilehmann committed Jun 20, 2024
1 parent a6baf28 commit 25b3055
Show file tree
Hide file tree
Showing 5 changed files with 20 additions and 0 deletions.
10 changes: 10 additions & 0 deletions crates/flux-fhir-analysis/src/conv.rs
Original file line number Diff line number Diff line change
Expand Up @@ -409,6 +409,16 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> {
)?;
}
}
fhir::GenericBound::Outlives(lft) => {
let re = self.conv_lifetime(env, *lft);
clauses.push(rty::Clause::new(
List::empty(),
rty::ClauseKind::TypeOutlives(rty::OutlivesPredicate(
bounded_ty.clone(),
re,
)),
));
}
// Maybe bounds are only supported for `?Sized`. The effect of the maybe bound is to
// relax the default which is `Sized` to not have the `Sized` bound, so we just skip
// it here.
Expand Down
1 change: 1 addition & 0 deletions crates/flux-middle/src/fhir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -309,6 +309,7 @@ pub type GenericBounds<'fhir> = &'fhir [GenericBound<'fhir>];
#[derive(Debug, Clone, Copy)]
pub enum GenericBound<'fhir> {
Trait(PolyTraitRef<'fhir>, TraitBoundModifier),
Outlives(Lifetime),
}

#[derive(Debug, Clone, Copy)]
Expand Down
4 changes: 4 additions & 0 deletions crates/flux-middle/src/fhir/lift.rs
Original file line number Diff line number Diff line change
Expand Up @@ -212,6 +212,10 @@ impl<'a, 'genv, 'tcx> LiftCtxt<'a, 'genv, 'tcx> {
fhir::TraitBoundModifier::Maybe,
))
}
hir::GenericBound::Outlives(lft) => {
let lft = self.lift_lifetime(lft)?;
Ok(fhir::GenericBound::Outlives(lft))
}
_ => self.emit_unsupported(&format!("unsupported generic bound: `{bound:?}`")),
}
}
Expand Down
1 change: 1 addition & 0 deletions crates/flux-middle/src/fhir/visit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,7 @@ pub fn walk_opaque_ty<'v, V: Visitor<'v>>(vis: &mut V, opaque_ty: &OpaqueTy<'v>)
pub fn walk_generic_bound<'v, V: Visitor<'v>>(vis: &mut V, bound: &GenericBound<'v>) {
match bound {
GenericBound::Trait(trait_ref, _) => vis.visit_poly_trait_ref(trait_ref),
GenericBound::Outlives(_) => {}
}
}

Expand Down
4 changes: 4 additions & 0 deletions tests/tests/pos/surface/type-outlives.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
struct S<'a, T: 'a> {
x: T,
y: &'a i32,
}

0 comments on commit 25b3055

Please sign in to comment.