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

charon_lib/ast/items/
trait_decl.rs
