Skip to content

Commit

Permalink
Make Self clause explicit in trait global declarations too
Browse files Browse the repository at this point in the history 
Both for consistency fir the corresponding method generics and in case
the default const uses values from `Self`.
  • Loading branch information
@Nadrieril
Nadrieril committed Jan 7, 2025
1 parent 9f6f217 commit 0c3cbb3
Show file tree
Hide file tree
Showing 5 changed files with 48 additions and 24 deletions.
30 changes: 22 additions & 8 deletions charon/src/bin/charon-driver/translate/translate_traits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,10 +138,10 @@ impl BodyTransCtx<'_, '_> {
// declares them.
let id = self.register_global_decl_id(item_span, item_def_id);
let generics_target = GenericsSource::item(id);
let gref = GlobalDeclRef {
id,
generics: self.the_only_binder().params.identity_args(generics_target),
};
let mut generics =
self.the_only_binder().params.identity_args(generics_target);
generics.trait_refs.push(self_trait_ref.clone());
let gref = GlobalDeclRef { id, generics };
const_defaults.insert(item_name.clone(), gref);
};
let ty = self.translate_ty(item_span, ty)?;
Expand Down Expand Up @@ -238,6 +238,16 @@ impl BodyTransCtx<'_, '_> {
)?;
TraitDeclRef { trait_id, generics }
};
// A `TraitRef` that points to this impl with the correct generics.
let self_predicate = TraitRef {
kind: TraitRefKind::TraitImpl(
def_id,
self.the_only_binder()
.params
.identity_args(GenericsSource::item(def_id)),
),
trait_decl_ref: RegionBinder::empty(implemented_trait.clone()),
};

// The trait refs which implement the parent clauses of the implemented trait decl.
let parent_trait_refs = self.translate_trait_impl_exprs(span, &required_impl_exprs)?;
Expand Down Expand Up @@ -322,10 +332,14 @@ impl BodyTransCtx<'_, '_> {
Provided { .. } => {
self.the_only_binder().params.identity_args(generics_target)
}
_ => implemented_trait
.generics
.clone()
.with_target(generics_target),
_ => {
let mut generics = implemented_trait
.generics
.clone()
.with_target(generics_target);
generics.trait_refs.push(self_predicate.clone());
generics
}
};
let gref = GlobalDeclRef { id, generics };
consts.push((name, gref));
Expand Down
5 changes: 2 additions & 3 deletions charon/src/bin/charon-driver/translate/translate_types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -593,9 +593,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
| Variant { .. } => {
let parent_def_id = def.parent.as_ref().unwrap();
let parent_def = self.t_ctx.hax_def(parent_def_id)?;
let explicit_self_clause = matches!(def.kind(), AssocFn { .. })
&& matches!(parent_def.kind(), Trait { .. });
// Add an explicit `Self` clause to trait method declarations.
// Add an explicit `Self` clause to trait item declarations.
let explicit_self_clause = matches!(parent_def.kind(), Trait { .. });
self.push_generics_for_def(span, &parent_def, true, explicit_self_clause)?;
}
_ => {}
Expand Down
8 changes: 2 additions & 6 deletions charon/tests/crate_data.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -612,14 +612,10 @@ fn declaration_groups() -> anyhow::Result<()> {
"#,
)?;

// There are two function ids registered, but only one is nonempty. `functions.len() == 2` as
// `len()` counts the empty slots too.
let decl_groups = crate_data.ordered_decls.unwrap();
// There are two function items: one for `foo`, one for the initializer of `Trait::FOO`.
assert_eq!(crate_data.fun_decls.iter().count(), 2);
let decl_groups = crate_data.ordered_decls.unwrap();
assert_eq!(decl_groups.len(), 5);
assert!(decl_groups
.iter()
.all(|group| group.to_mixed_group().is_non_rec()));

Ok(())
}
Expand Down
20 changes: 15 additions & 5 deletions charon/tests/ui/assoc-const-with-generics.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,14 +94,19 @@ where
}

fn test_crate::HasDefaultLen::LEN<Self, const M : usize>() -> usize
where
[@TraitClause0]: test_crate::HasDefaultLen<Self, const M : usize>,
{
let @0: usize; // return

@0 := const (const M : usize)
return
}

global test_crate::HasDefaultLen::LEN<Self, const M : usize>: usize = test_crate::HasDefaultLen::LEN()
global test_crate::HasDefaultLen::LEN<Self, const M : usize>: usize
where
[@TraitClause0]: test_crate::HasDefaultLen<Self, const M : usize>,
= test_crate::HasDefaultLen::LEN()

trait test_crate::HasDefaultLen<Self, const M : usize>
{
Expand All @@ -110,7 +115,7 @@ trait test_crate::HasDefaultLen<Self, const M : usize>

impl<const N : usize> test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<(), const N : usize>}#4<const N : usize> : test_crate::HasDefaultLen<Array<(), const N : usize>, const N : usize>
{
const LEN = test_crate::HasDefaultLen::LEN<Array<(), const N : usize>, const N : usize>
const LEN = test_crate::HasDefaultLen::LEN<Array<(), const N : usize>, const N : usize>[test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<(), const N : usize>}#4<const N : usize>]
}

fn test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<bool, const N : usize>}#5::LEN<const N : usize>() -> usize
Expand All @@ -137,14 +142,19 @@ impl<const N : usize> test_crate::{impl test_crate::HasDefaultLen<const N : usiz
}

fn test_crate::AlsoHasLen::ALSO_LEN<Self>() -> usize
where
[@TraitClause0]: test_crate::AlsoHasLen<Self>,
{
let @0: usize; // return

@0 := const (Self::parent_clause0::LEN) + const (1 : usize)
@0 := const (@TraitClause0::parent_clause0::LEN) + const (1 : usize)
return
}

global test_crate::AlsoHasLen::ALSO_LEN<Self>: usize = test_crate::AlsoHasLen::ALSO_LEN()
global test_crate::AlsoHasLen::ALSO_LEN<Self>: usize
where
[@TraitClause0]: test_crate::AlsoHasLen<Self>,
= test_crate::AlsoHasLen::ALSO_LEN()

trait test_crate::AlsoHasLen<Self>
{
Expand All @@ -155,7 +165,7 @@ trait test_crate::AlsoHasLen<Self>
impl<const N : usize> test_crate::{impl test_crate::AlsoHasLen for Array<(), const N : usize>}#6<const N : usize> : test_crate::AlsoHasLen<Array<(), const N : usize>>
{
parent_clause0 = test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1<const N : usize>
const ALSO_LEN = test_crate::AlsoHasLen::ALSO_LEN<Array<(), const N : usize>>
const ALSO_LEN = test_crate::AlsoHasLen::ALSO_LEN<Array<(), const N : usize>>[test_crate::{impl test_crate::AlsoHasLen for Array<(), const N : usize>}#6<const N : usize>]
}


Expand Down
9 changes: 7 additions & 2 deletions charon/tests/ui/traits.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -488,14 +488,19 @@ where
}

fn test_crate::WithConstTy::LEN2<Self, const LEN : usize>() -> usize
where
[@TraitClause0]: test_crate::WithConstTy<Self, const LEN : usize>,
{
let @0: usize; // return

@0 := const (32 : usize)
return
}

global test_crate::WithConstTy::LEN2<Self, const LEN : usize>: usize = test_crate::WithConstTy::LEN2()
global test_crate::WithConstTy::LEN2<Self, const LEN : usize>: usize
where
[@TraitClause0]: test_crate::WithConstTy<Self, const LEN : usize>,
= test_crate::WithConstTy::LEN2()

trait test_crate::WithConstTy<Self, const LEN : usize>
{
Expand Down Expand Up @@ -538,7 +543,7 @@ impl test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8 : test_cr
parent_clause1 = test_crate::{impl test_crate::ToU64 for u64}#2
parent_clause2 = core::marker::Sized<u64>
const LEN1 = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1
const LEN2 = test_crate::WithConstTy::LEN2<bool, 32 : usize>
const LEN2 = test_crate::WithConstTy::LEN2<bool, 32 : usize>[test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8]
type V = u8
type W = u64
fn f<'_0, '_1> = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0_0, '_0_1>
Expand Down

0 comments on commit 0c3cbb3

Please sign in to comment.