charon_lib/ast/items/
trait_decl.rs

1use crate::ast::*;
2use crate::ids::IndexVec;
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use serde_state::DeserializeState;
5use serde_state::SerializeState;
6
7#[derive(
8    Debug,
9    Clone,
10    Copy,
11    SerializeState,
12    DeserializeState,
13    Drive,
14    DriveMut,
15    DriveTwo,
16    PartialEq,
17    Eq,
18    Hash,
19    PartialOrd,
20    Ord,
21)]
22#[drive(skip)]
23#[serde_state(stateless)]
24pub struct TraitItemName(pub ustr::Ustr);
25
26generate_index_type!(TraitMethodId, "TraitMethod");
27generate_index_type!(AssocTypeId, "AssocType");
28generate_index_type!(AssocConstId, "AssocConst");
29
30/// A trait **declaration**.
31///
32/// For instance:
33/// ```text
34/// trait Foo {
35///   type Bar;
36///
37///   fn baz(...); // required method (see below)
38///
39///   fn test() -> bool { true } // provided method (see below)
40/// }
41/// ```
42///
43/// In case of a trait declaration, we don't include the provided methods (the methods
44/// with a default implementation): they will be translated on a per-need basis. This is
45/// important for two reasons:
46/// - this makes the trait definitions a lot smaller (the Iterator trait
47///   has *one* declared function and more than 70 provided functions)
48/// - this is important for the external traits, whose provided methods
49///   often use features we don't support yet
50///
51/// Remark:
52/// In Aeneas, we still translate the provided methods on an individual basis,
53/// and in such a way thay they take as input a trait instance. This means that
54/// we can use default methods *but*:
55/// - implementations of required methods shoudln't call default methods
56/// - trait implementations shouldn't redefine required methods
57///
58/// The use case we have in mind is [std::iter::Iterator]: it declares one required
59/// method (`next`) that should be implemented for every iterator, and defines many
60/// helpers like `all`, `map`, etc. that shouldn't be re-implemented.
61/// Of course, this forbids other useful use cases such as visitors implemented
62/// by means of traits.
63#[allow(clippy::type_complexity)]
64#[derive(
65    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
66)]
67pub struct TraitDecl {
68    pub def_id: TraitDeclId,
69    pub item_meta: ItemMeta,
70    /// Distinguishes normal traits from trait aliases.
71    pub src: TraitDeclSource,
72    pub generics: GenericParams,
73    /// The "parent" clauses: the supertraits.
74    ///
75    /// Supertraits are actually regular where clauses, but we decided to have
76    /// a custom treatment.
77    /// ```text
78    /// trait Foo : Bar {
79    ///             ^^^
80    ///         supertrait, that we treat as a parent predicate
81    /// }
82    /// ```
83    /// TODO: actually, as of today, we consider that all trait clauses of
84    /// trait declarations are parent clauses.
85    pub implied_clauses: IndexVec<TraitClauseId, TraitParam>,
86    /// The associated constants declared in the trait.
87    pub consts: IndexMap<AssocConstId, TraitAssocConst>,
88    /// The associated types declared in the trait. The binder binds the generic parameters of the
89    /// type if it is a GAT (Generic Associated Type). For a plain associated type the binder binds
90    /// nothing.
91    pub types: IndexMap<AssocTypeId, Binder<TraitAssocTy>>,
92    /// The methods declared by the trait. The binder binds the generic parameters of the method.
93    ///
94    /// ```rust
95    /// trait Trait<T> {
96    ///   // The `Binder` for this method binds `'a` and `U`.
97    ///   fn method<'a, U>(x: &'a U);
98    /// }
99    /// ```
100    pub methods: IndexMap<TraitMethodId, Binder<TraitMethod>>,
101    /// The virtual table struct for this trait, if it has one.
102    /// It is guaranteed that the trait has a vtable iff it is dyn-compatible.
103    pub vtable: Option<TypeDeclRef>,
104}
105
106/// An associated constant in a trait.
107#[derive(
108    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
109)]
110pub struct TraitAssocConst {
111    pub name: TraitItemName,
112    #[serde_state(stateless)]
113    pub attr_info: AttrInfo,
114    pub ty: Ty,
115    pub default: Option<GlobalDeclRef>,
116}
117
118/// An associated type in a trait.
119#[derive(
120    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
121)]
122pub struct TraitAssocTy {
123    pub name: TraitItemName,
124    #[serde_state(stateless)]
125    pub attr_info: AttrInfo,
126    pub default: Option<TraitAssocTyImpl>,
127    /// List of trait clauses that apply to this type.
128    pub implied_clauses: IndexVec<TraitClauseId, TraitParam>,
129}
130
131/// A trait method.
132#[derive(
133    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
134)]
135pub struct TraitMethod {
136    pub name: TraitItemName,
137    pub item_meta: ItemMeta,
138    pub signature: FunSig,
139    /// The default method implementation, if there is one.
140    pub default: Option<FunDeclRef>,
141}
142
143/// Where the trait comes from.
144#[derive(
145    Debug, Clone, Copy, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
146)]
147#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("TraitDecl"))]
148pub enum TraitDeclSource {
149    /// A regular trait.
150    Normal,
151    /// The trait declaration coming from a trait alias.
152    TraitAlias,
153}
154
155impl TraitDecl {
156    pub fn methods(&self) -> impl Iterator<Item = &Binder<TraitMethod>> {
157        self.methods.iter()
158    }
159}
160
161impl Binder<TraitAssocTy> {
162    pub fn name(&self) -> &TraitItemName {
163        &self.skip_binder.name
164    }
165}
166impl Binder<TraitMethod> {
167    pub fn name(&self) -> TraitItemName {
168        self.skip_binder.name
169    }
170}
charon_lib/ast/items/trait_decl.rs

charon_lib/ast/items/
trait_decl.rs
