diff options
Diffstat (limited to 'rust/macros')
| -rw-r--r-- | rust/macros/for_lt.rs | 41 | ||||
| -rw-r--r-- | rust/macros/lib.rs | 18 |
2 files changed, 46 insertions, 13 deletions
diff --git a/rust/macros/for_lt.rs b/rust/macros/for_lt.rs index 364d4113c..4372cbad3 100644 --- a/rust/macros/for_lt.rs +++ b/rust/macros/for_lt.rs @@ -154,8 +154,8 @@ impl<'a> Prover<'a> { // Note that if we encounter `&'other_lt T`, then we still need to make sure the type // is wellformed if `T` involves `&'lt`, so we defer to the compiler. // - // This is to block cases like `ForLt!(for<'a> &'static &'a u32)`, as the presence of - // the type implies `'a: 'static` but this is unsound. + // This is to block cases like `CovariantForLt!(for<'a> &'static &'a u32)`, as the + // presence of the type implies `'a: 'static` but this is unsound. Type::Reference(ty) if ty.mutability.is_none() && ty.lifetime.as_ref() == Some(self.0) => { @@ -176,7 +176,12 @@ impl<'a> Prover<'a> { } } -pub(crate) fn for_lt(input: HigherRankedType) -> TokenStream { +/// Shared implementation for both `ForLt!` and `CovariantForLt!`. +/// +/// Both macros run the prover and emit `ProveWf` structs to check well-formedness for all lifetime +/// instances (workaround for <https://github.com/rust-lang/rust/issues/152489>). `CovariantForLt!` +/// additionally emits covariance proof functions and sets `N = 1`. +fn for_lt_inner(input: HigherRankedType, prove_covariance: bool) -> TokenStream { let (ty, lifetime) = match input { HigherRankedType::Explicit { lifetime, ty, .. } => (ty, lifetime), HigherRankedType::Implicit { ty } => { @@ -211,14 +216,16 @@ pub(crate) fn for_lt(input: HigherRankedType) -> TokenStream { )); // Insert a proof that the type is covariant. - let cov_proof_name = format_ident!("prove_covariant_{idx}"); - proof.push(quote!( - fn #cov_proof_name<'__short, '__long: '__short>( - long: #wf_proof_name<'__long> - ) -> #wf_proof_name<'__short> { - long - } - )); + if prove_covariance { + let cov_proof_name = format_ident!("prove_covariant_{idx}"); + proof.push(quote!( + fn #cov_proof_name<'__short, '__long: '__short>( + long: #wf_proof_name<'__long> + ) -> #wf_proof_name<'__short> { + long + } + )); + } } // Make sure that the type is wellformed when substituting lifetime with `'static`. @@ -234,6 +241,8 @@ pub(crate) fn for_lt(input: HigherRankedType) -> TokenStream { }, ); + let n: usize = prove_covariance.into(); + quote!( ::kernel::types::for_lt::UnsafeForLtImpl::< dyn for<#lifetime> ::kernel::types::for_lt::WithLt<#lifetime, Of = #ty>, @@ -241,8 +250,16 @@ pub(crate) fn for_lt(input: HigherRankedType) -> TokenStream { { #(#proof)* - 0 + #n } > ) } + +pub(crate) fn for_lt(input: HigherRankedType) -> TokenStream { + for_lt_inner(input, false) +} + +pub(crate) fn covariant_for_lt(input: HigherRankedType) -> TokenStream { + for_lt_inner(input, true) +} diff --git a/rust/macros/lib.rs b/rust/macros/lib.rs index 408a90567..37a6643db 100644 --- a/rust/macros/lib.rs +++ b/rust/macros/lib.rs @@ -515,8 +515,24 @@ pub fn kunit_tests(attr: TokenStream, input: TokenStream) -> TokenStream { /// /// [`ForLt`]: trait.ForLt.html #[proc_macro] -// The macro shares the name with the trait. #[allow(non_snake_case)] pub fn ForLt(input: TokenStream) -> TokenStream { for_lt::for_lt(parse_macro_input!(input)).into() } + +/// Obtain a type that implements [`CovariantForLt`] (and [`ForLt`]) for the given higher-ranked +/// type. +/// +/// Unlike [`ForLt!`], this macro additionally proves that the type is covariant over the lifetime, +/// providing a safe [`CovariantForLt::cast_ref`] method. +/// +/// Please refer to the documentation of the [`CovariantForLt`] trait. +/// +/// [`CovariantForLt`]: trait.CovariantForLt.html +/// [`CovariantForLt::cast_ref`]: trait.CovariantForLt.html#method.cast_ref +/// [`ForLt`]: trait.ForLt.html +#[proc_macro] +#[allow(non_snake_case)] +pub fn CovariantForLt(input: TokenStream) -> TokenStream { + for_lt::covariant_for_lt(parse_macro_input!(input)).into() +} |