charon_lib/ast/items/
trait_impl.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/// A trait **implementation**.
8///
9/// For instance:
10/// ```text
11/// impl Foo for List {
12///   type Bar = ...
13///
14///   fn baz(...) { ... }
15/// }
16/// ```
17#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
18pub struct TraitImpl {
19    pub def_id: TraitImplId,
20    pub item_meta: ItemMeta,
21    pub src: TraitImplSource,
22    /// The information about the implemented trait.
23    /// Note that this contains the instantiation of the "parent"
24    /// clauses.
25    pub impl_trait: TraitDeclRef,
26    pub generics: GenericParams,
27    /// The trait references for the parent clauses (see [TraitDecl]).
28    pub implied_trait_refs: IndexVec<TraitClauseId, TraitRef>,
29    /// The implemented associated constants.
30    pub consts: IndexMap<AssocConstId, GlobalDeclRef>,
31    /// The implemented associated types.
32    pub types: IndexMap<AssocTypeId, Binder<TraitAssocTyImpl>>,
33    /// The implemented methods
34    pub methods: IndexMap<TraitMethodId, Binder<FunDeclRef>>,
35    /// The virtual table instance for this trait implementation. This is `Some` iff the trait is
36    /// dyn-compatible.
37    pub vtable: Option<GlobalDeclRef>,
38}
39
40/// The value of a trait associated type.
41#[derive(
42    Debug,
43    Clone,
44    PartialEq,
45    Eq,
46    PartialOrd,
47    Ord,
48    Hash,
49    SerializeState,
50    DeserializeState,
51    Drive,
52    DriveMut,
53    DriveTwo,
54)]
55pub struct TraitAssocTyImpl {
56    pub value: Ty,
57    /// This matches the corresponding vector in `TraitAssocTy`. In the same way, this is empty
58    /// after the `lift_associated_item_clauses` pass.
59    pub implied_trait_refs: IndexVec<TraitClauseId, TraitRef>,
60}
61
62/// Where the impl comes from.
63#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
64#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("TraitImpl"))]
65pub enum TraitImplSource {
66    /// A regular trait implementation.
67    Normal,
68    /// The blanket implementation generated for a trait alias.
69    TraitAlias,
70    /// An implementation of one of the `Fn*` traits, generated for a closure.
71    Closure {
72        #[serde_state(stateless)]
73        kind: ClosureKind,
74    },
75    /// The `Destruct` implementation generated for an ADT or closure.
76    Destruct,
77}
78
79impl TraitImpl {
80    pub fn methods(&self) -> impl Iterator<Item = &Binder<FunDeclRef>> {
81        self.methods.iter()
82    }
83}
charon_lib/ast/items/trait_impl.rs

charon_lib/ast/items/
trait_impl.rs
