charon_lib/ast/items/
trait_impl.rs

1use crate::ast::*;
2use crate::ids::IndexVec;
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use macros::EnumAsGetters;
5use macros::EnumIsA;
6use serde_state::DeserializeState;
7use serde_state::SerializeState;
8
9/// A trait **implementation**.
10///
11/// For instance:
12/// ```text
13/// impl Foo for List {
14///   type Bar = ...
15///
16///   fn baz(...) { ... }
17/// }
18/// ```
19#[derive(Debug, Clone)]
20#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
21pub struct TraitImpl {
22    pub def_id: TraitImplId,
23    pub item_meta: ItemMeta,
24    pub src: TraitImplSource,
25    /// The information about the implemented trait.
26    /// Note that this contains the instantiation of the "parent"
27    /// clauses.
28    pub impl_trait: TraitDeclRef,
29    /// Whether this is a negative impl (`impl !Trait for Type`).
30    pub is_negative: bool,
31    /// Whether this is an `unsafe impl`.
32    pub is_unsafe: bool,
33    pub generics: GenericParams,
34    /// The trait references for the parent clauses (see [TraitDecl]).
35    pub implied_trait_refs: IndexVec<TraitClauseId, TraitRef>,
36    /// The implemented associated constants.
37    pub consts: IndexMap<AssocConstId, GlobalDeclRef>,
38    /// The implemented associated types.
39    pub types: IndexMap<AssocTypeId, Binder<TraitAssocTyImpl>>,
40    /// The implemented methods
41    pub methods: IndexMap<TraitMethodId, Binder<FunDeclRef>>,
42    /// The virtual table instance for this trait implementation.
43    pub vtable: VTableDecl,
44}
45
46/// The value of a trait associated type.
47#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
48#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
49pub struct TraitAssocTyImpl {
50    pub value: Ty,
51    /// This matches the corresponding vector in `TraitAssocTy`. In the same way, this is empty
52    /// after the `lift_associated_item_clauses` pass.
53    pub implied_trait_refs: IndexVec<TraitClauseId, TraitRef>,
54}
55
56/// Where the impl comes from.
57#[derive(Debug, Clone)]
58#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
59#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("TraitImpl"))]
60pub enum TraitImplSource {
61    /// A regular trait implementation.
62    Normal,
63    /// The blanket implementation generated for a trait alias.
64    TraitAlias,
65    /// An implementation of one of the `Fn*` traits, generated for a closure.
66    Closure {
67        #[serde_state(stateless)]
68        kind: ClosureKind,
69    },
70    /// The `Destruct` implementation generated for an ADT or closure.
71    Destruct,
72}
73
74/// The virtual table instance for a trait implementation.
75#[derive(Debug, Clone)]
76#[derive(EnumIsA, EnumAsGetters)]
77#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
78pub enum VTableDecl {
79    /// The trait is not dyn-compatible, so no vtable exists.
80    NotDynCompatible,
81    /// The trait is dyn-compatible, but we have not computed a vtable for it, as it is not used.
82    Lazy,
83    /// The trait is dyn-compatible, and we have computed a vtable for it.
84    #[cfg_attr(feature = "charon_on_charon", charon::rename("VTableInstance"))]
85    VTable(GlobalDeclRef),
86    /// We don't support computing a vtable for this impl; the string explains why.
87    #[cfg_attr(feature = "charon_on_charon", charon::rename("UnknownVTable"))]
88    Unknown(String),
89}
90
91impl TraitImpl {
92    pub fn methods(&self) -> impl Iterator<Item = &Binder<FunDeclRef>> {
93        self.methods.iter()
94    }
95
96    /// Whether this trait impl is unsafe to declare, because it is an `unsafe impl` (safety.unsafe-impl)
97    /// or it has an unsafe attribute (safety.unsafe-attribute).
98    pub fn is_unsafe_to_declare(&self, _krate: &TranslatedCrate) -> bool {
99        self.is_unsafe || self.item_meta.is_unsafe_to_declare()
100    }
101}
charon_lib/ast/items/trait_impl.rs

charon_lib/ast/items/
trait_impl.rs
