charon_lib/ast/items/
item_ids.rs

1use std::cmp::{Ord, PartialOrd};
2
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use serde::{Deserialize, Serialize};
5use serde_state::{DeserializeState, SerializeState};
6
7use crate::ast::*;
8use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
9
10generate_index_type!(FunDeclId, "Fun");
11generate_index_type!(TypeDeclId, "Adt");
12
13impl TypeDeclId {
14    /// The declaration of the unit type `()`. With `--no-gen-tuple-structs`, this is the
15    /// declaration of every tuple.
16    pub const UNIT: Self = Self::ZERO;
17}
18generate_index_type!(GlobalDeclId, "Global");
19generate_index_type!(TraitDeclId, "TraitDecl");
20generate_index_type!(TraitImplId, "TraitImpl");
21
22/// The id of a translated item.
23#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
24#[derive(EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)]
25#[derive(
26    Serialize,
27    Deserialize,
28    SerializeState,
29    DeserializeState,
30    Drive,
31    DriveMut,
32    DriveTwo
33)]
34#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Id"))]
35#[serde_state(stateless)]
36pub enum ItemId {
37    Type(TypeDeclId),
38    TraitDecl(TraitDeclId),
39    TraitImpl(TraitImplId),
40    Fun(FunDeclId),
41    Global(GlobalDeclId),
42}
43
44/// The id of an associated item within a trait.
45#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
46#[derive(EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)]
47#[derive(
48    Serialize,
49    Deserialize,
50    SerializeState,
51    DeserializeState,
52    Drive,
53    DriveMut,
54    DriveTwo
55)]
56#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("AssocId"))]
57#[serde_state(stateless)]
58pub enum AssocItemId {
59    Type(AssocTypeId),
60    Method(TraitMethodId),
61    Const(AssocConstId),
62}
63
64/// The id of a translated item or associated item definition.
65#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
66#[derive(EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)]
67#[derive(
68    Serialize,
69    Deserialize,
70    SerializeState,
71    DeserializeState,
72    Drive,
73    DriveMut,
74    DriveTwo
75)]
76#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Item"))]
77#[serde_state(stateless)]
78pub enum MaybeAssocItemId {
79    Free(ItemId),
80    Assoc(TraitDeclId, AssocItemId),
81}
82
83/// Reference to a type declaration.
84///
85/// This includes user-defined ADTs (structs, enums, unions), but also tuples,
86/// boxes, and `str`, which we translate as `struct str([u8])`.
87#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
88#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
89pub struct TypeDeclRef {
90    pub id: TypeDeclId,
91    pub generics: BoxedArgs,
92    /// If this points to a builtin ADT, it is recorded here for easier identification.
93    pub builtin: Option<BuiltinAdt>,
94}
95
96/// Reference to a function declaration.
97#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
98#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
99pub struct FunDeclRef {
100    pub id: FunDeclId,
101    /// Generic arguments passed to the function.
102    pub generics: BoxedArgs,
103}
104
105#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
106#[derive(EnumAsGetters)]
107#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
108pub enum FnPtrKind {
109    Fun(FunDeclId),
110    /// If a trait: the reference to the trait and the id of the trait method.
111    #[cfg_attr(feature = "charon_on_charon", charon::rename("TraitMethod"))]
112    Trait(TraitRef, TraitMethodId),
113}
114
115/// Reference to a function, possibly indirected via a trait.
116#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
117#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
118pub struct FnPtr {
119    pub kind: Box<FnPtrKind>,
120    pub generics: BoxedArgs,
121}
122
123/// Reference to a global declaration.
124#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
125#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
126pub struct GlobalDeclRef {
127    pub id: GlobalDeclId,
128    pub generics: BoxedArgs,
129}
130
131/// A predicate of the form `Type: Trait<Args>`.
132///
133/// About the generics, if we write:
134/// ```text
135/// impl Foo<bool> for String { ... }
136/// ```
137///
138/// The substitution is: `[String, bool]`.
139#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
140#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
141pub struct TraitDeclRef {
142    pub id: TraitDeclId,
143    pub generics: BoxedArgs,
144}
145
146/// A reference to a tait impl, using the provided arguments.
147#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
148#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
149pub struct TraitImplRef {
150    pub id: TraitImplId,
151    pub generics: BoxedArgs,
152}
153
154impl TypeDeclRef {
155    pub fn new(id: TypeDeclId, generics: GenericArgs, builtin: Option<BuiltinAdt>) -> Self {
156        Self {
157            id,
158            generics: Box::new(generics),
159            builtin,
160        }
161    }
162
163    pub fn as_builtin(&self) -> Option<BuiltinAdt> {
164        self.builtin
165    }
166
167    pub fn is_builtin(&self) -> bool {
168        self.builtin.is_some()
169    }
170
171    /// Whether this refers to `Box`.
172    pub fn is_box(&self) -> bool {
173        matches!(self.builtin, Some(BuiltinAdt::Box))
174    }
175
176    /// Whether this refers to a tuple.
177    pub fn is_tuple(&self) -> bool {
178        matches!(self.builtin, Some(BuiltinAdt::Tuple))
179    }
180
181    /// Whether this refers to `str`.
182    pub fn is_str(&self) -> bool {
183        matches!(self.builtin, Some(BuiltinAdt::Str))
184    }
185}
186
187impl TraitDeclRef {
188    pub fn self_ty<'a>(&'a self, krate: &'a TranslatedCrate) -> Option<&'a Ty> {
189        match self.generics.types.iter().next() {
190            Some(ty) => Some(ty),
191            // TODO(mono): A monomorphized trait takes no arguments.
192            None => {
193                let name = krate.item_name(self.id);
194                let args = name.name.last()?.as_monomorphized()?;
195                args.types.iter().next()
196            }
197        }
198    }
199}
200
201impl FnPtr {
202    pub fn new(kind: FnPtrKind, generics: impl Into<BoxedArgs>) -> Self {
203        Self {
204            kind: Box::new(kind),
205            generics: generics.into(),
206        }
207    }
208
209    /// Get the generics for the pre-monomorphization item.
210    pub fn pre_mono_generics<'a>(&'a self, krate: &'a TranslatedCrate) -> &'a GenericArgs {
211        match *self.kind {
212            FnPtrKind::Fun(fun_id) => krate
213                .item_name(fun_id)
214                .mono_args()
215                .unwrap_or(&self.generics),
216            // Can't happen in mono mode.
217            FnPtrKind::Trait(..) => &self.generics,
218        }
219    }
220}
221
222/// A generic `*DeclRef`-shaped struct, used when we're generic over the type of item.
223#[derive(Debug, Clone, PartialEq, Eq)]
224#[derive(Drive, DriveMut, DriveTwo)]
225pub struct DeclRef<Id> {
226    pub id: Id,
227    pub generics: BoxedArgs,
228    /// If the item is a trait associated item, `generics` are only those of the item, and this
229    /// contains a reference to the trait.
230    // TODO: also store `AssocItemId` so that we can convert to `FnPtr` without
231    // `MaybeBuiltinFunDeclRef`.
232    pub trait_ref: Option<TraitRef>,
233}
234
235impl DeclRef<ItemId> {
236    pub fn try_convert_id<Id>(self) -> Result<DeclRef<Id>, <ItemId as TryInto<Id>>::Error>
237    where
238        ItemId: TryInto<Id>,
239    {
240        Ok(DeclRef {
241            id: self.id.try_into()?,
242            generics: self.generics,
243            trait_ref: self.trait_ref,
244        })
245    }
246}
247
248// Implement `DeclRef<_>` -> `FooDeclRef` conversions.
249macro_rules! convert_item_ref {
250    ($item_ref_ty:ident($id:ident)) => {
251        impl TryFrom<DeclRef<ItemId>> for $item_ref_ty {
252            type Error = ();
253            fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
254                assert!(item.trait_ref.is_none());
255                Ok($item_ref_ty {
256                    id: item.id.try_into()?,
257                    generics: item.generics,
258                })
259            }
260        }
261        impl From<DeclRef<$id>> for $item_ref_ty {
262            fn from(item: DeclRef<$id>) -> Self {
263                assert!(item.trait_ref.is_none());
264                $item_ref_ty {
265                    id: item.id,
266                    generics: item.generics,
267                }
268            }
269        }
270    };
271}
272// We do not provide a `DeclRef<_> -> TypeDeclRef` impl, because we lack information
273// about builtins here.
274convert_item_ref!(FunDeclRef(FunDeclId));
275convert_item_ref!(GlobalDeclRef(GlobalDeclId));
276convert_item_ref!(TraitDeclRef(TraitDeclId));
277convert_item_ref!(TraitImplRef(TraitImplId));
278impl TryFrom<DeclRef<ItemId>> for FnPtr {
279    type Error = ();
280    fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
281        if item.trait_ref.is_some() {
282            panic!(
283                "converting `DeclRef<ItemId>` to `FnPtr` cannot
284                deal with the trait method case."
285            )
286        }
287        let id: FunDeclId = item.id.try_into()?;
288        Ok(FnPtr::new(id.into(), item.generics))
289    }
290}
291impl From<FunDeclRef> for FnPtr {
292    fn from(fn_ref: FunDeclRef) -> Self {
293        FnPtr::new(fn_ref.id.into(), fn_ref.generics)
294    }
295}
296
297/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
298macro_rules! wrap_unwrap_enum {
299    ($enum:ident::$variant:ident($variant_ty:ident)) => {
300        impl TryFrom<$enum> for $variant_ty {
301            type Error = ();
302            fn try_from(x: $enum) -> Result<Self, Self::Error> {
303                match x {
304                    $enum::$variant(x) => Ok(x),
305                    _ => Err(()),
306                }
307            }
308        }
309
310        impl From<$variant_ty> for $enum {
311            fn from(x: $variant_ty) -> Self {
312                $enum::$variant(x)
313            }
314        }
315    };
316}
317
318wrap_unwrap_enum!(ItemId::Fun(FunDeclId));
319wrap_unwrap_enum!(ItemId::Global(GlobalDeclId));
320wrap_unwrap_enum!(ItemId::Type(TypeDeclId));
321wrap_unwrap_enum!(ItemId::TraitDecl(TraitDeclId));
322wrap_unwrap_enum!(ItemId::TraitImpl(TraitImplId));
323wrap_unwrap_enum!(AssocItemId::Type(AssocTypeId));
324wrap_unwrap_enum!(AssocItemId::Method(TraitMethodId));
325wrap_unwrap_enum!(AssocItemId::Const(AssocConstId));
326
327impl From<FunDeclId> for FnPtrKind {
328    fn from(id: FunDeclId) -> Self {
329        Self::Fun(id)
330    }
331}
charon_lib/ast/items/item_ids.rs

charon_lib/ast/items/
item_ids.rs
