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

charon_lib/ast/items/
trait_impl.rs
