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

charon_lib/ast/items/
trait_decl.rs
