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(
24    Copy,
25    Clone,
26    Debug,
27    PartialOrd,
28    Ord,
29    PartialEq,
30    Eq,
31    Hash,
32    EnumIsA,
33    EnumAsGetters,
34    VariantName,
35    VariantIndexArity,
36    Serialize,
37    Deserialize,
38    SerializeState,
39    DeserializeState,
40    Drive,
41    DriveMut,
42    DriveTwo,
43)]
44#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Id"))]
45#[serde_state(stateless)]
46pub enum ItemId {
47    Type(TypeDeclId),
48    TraitDecl(TraitDeclId),
49    TraitImpl(TraitImplId),
50    Fun(FunDeclId),
51    Global(GlobalDeclId),
52}
53
54/// The id of an associated item within a trait.
55#[derive(
56    Copy,
57    Clone,
58    Debug,
59    PartialOrd,
60    Ord,
61    PartialEq,
62    Eq,
63    Hash,
64    EnumIsA,
65    EnumAsGetters,
66    VariantName,
67    VariantIndexArity,
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("AssocId"))]
77#[serde_state(stateless)]
78pub enum AssocItemId {
79    Type(AssocTypeId),
80    Method(TraitMethodId),
81    Const(AssocConstId),
82}
83
84/// The id of a translated item or associated item definition.
85#[derive(
86    Copy,
87    Clone,
88    Debug,
89    PartialOrd,
90    Ord,
91    PartialEq,
92    Eq,
93    Hash,
94    EnumIsA,
95    EnumAsGetters,
96    VariantName,
97    VariantIndexArity,
98    Serialize,
99    Deserialize,
100    SerializeState,
101    DeserializeState,
102    Drive,
103    DriveMut,
104    DriveTwo,
105)]
106#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Item"))]
107#[serde_state(stateless)]
108pub enum MaybeAssocItemId {
109    Free(ItemId),
110    Assoc(TraitDeclId, AssocItemId),
111}
112
113/// Reference to a type declaration.
114///
115/// This includes user-defined ADTs (structs, enums, unions), but also tuples,
116/// boxes, and `str`, which we translate as `struct str([u8])`.
117#[derive(
118    Debug,
119    Clone,
120    PartialEq,
121    Eq,
122    PartialOrd,
123    Ord,
124    Hash,
125    SerializeState,
126    DeserializeState,
127    Drive,
128    DriveMut,
129    DriveTwo,
130)]
131pub struct TypeDeclRef {
132    pub id: TypeDeclId,
133    pub generics: BoxedArgs,
134    /// If this points to a builtin ADT, it is recorded here for easier identification.
135    pub builtin: Option<BuiltinAdt>,
136}
137
138/// Reference to a function declaration.
139#[derive(
140    Debug,
141    Clone,
142    PartialEq,
143    Eq,
144    PartialOrd,
145    Ord,
146    Hash,
147    SerializeState,
148    DeserializeState,
149    Drive,
150    DriveMut,
151    DriveTwo,
152)]
153pub struct FunDeclRef {
154    pub id: FunDeclId,
155    /// Generic arguments passed to the function.
156    pub generics: BoxedArgs,
157}
158
159#[derive(
160    Debug,
161    Clone,
162    PartialEq,
163    Eq,
164    PartialOrd,
165    Ord,
166    EnumAsGetters,
167    SerializeState,
168    DeserializeState,
169    Drive,
170    DriveMut,
171    DriveTwo,
172    Hash,
173)]
174pub enum FnPtrKind {
175    Fun(FunDeclId),
176    /// If a trait: the reference to the trait and the id of the trait method.
177    #[cfg_attr(feature = "charon_on_charon", charon::rename("TraitMethod"))]
178    Trait(TraitRef, TraitMethodId),
179}
180
181/// Reference to a function, possibly indirected via a trait.
182#[derive(
183    Debug,
184    PartialEq,
185    Eq,
186    PartialOrd,
187    Ord,
188    Clone,
189    Hash,
190    SerializeState,
191    DeserializeState,
192    Drive,
193    DriveMut,
194    DriveTwo,
195)]
196pub struct FnPtr {
197    pub kind: Box<FnPtrKind>,
198    pub generics: BoxedArgs,
199}
200
201/// Reference to a global declaration.
202#[derive(
203    Debug,
204    Clone,
205    PartialEq,
206    Eq,
207    PartialOrd,
208    Ord,
209    Hash,
210    SerializeState,
211    DeserializeState,
212    Drive,
213    DriveMut,
214    DriveTwo,
215)]
216pub struct GlobalDeclRef {
217    pub id: GlobalDeclId,
218    pub generics: BoxedArgs,
219}
220
221/// A predicate of the form `Type: Trait<Args>`.
222///
223/// About the generics, if we write:
224/// ```text
225/// impl Foo<bool> for String { ... }
226/// ```
227///
228/// The substitution is: `[String, bool]`.
229#[derive(
230    Debug,
231    Clone,
232    PartialEq,
233    Eq,
234    PartialOrd,
235    Ord,
236    Hash,
237    SerializeState,
238    DeserializeState,
239    Drive,
240    DriveMut,
241    DriveTwo,
242)]
243pub struct TraitDeclRef {
244    pub id: TraitDeclId,
245    pub generics: BoxedArgs,
246}
247
248/// A reference to a tait impl, using the provided arguments.
249#[derive(
250    Debug,
251    Clone,
252    PartialEq,
253    Eq,
254    PartialOrd,
255    Ord,
256    Hash,
257    SerializeState,
258    DeserializeState,
259    Drive,
260    DriveMut,
261    DriveTwo,
262)]
263pub struct TraitImplRef {
264    pub id: TraitImplId,
265    pub generics: BoxedArgs,
266}
267
268impl TypeDeclRef {
269    pub fn new(id: TypeDeclId, generics: GenericArgs, builtin: Option<BuiltinAdt>) -> Self {
270        Self {
271            id,
272            generics: Box::new(generics),
273            builtin,
274        }
275    }
276
277    pub fn as_builtin(&self) -> Option<BuiltinAdt> {
278        self.builtin
279    }
280
281    /// Whether this refers to `Box`.
282    pub fn is_box(&self) -> bool {
283        matches!(self.builtin, Some(BuiltinAdt::Box))
284    }
285
286    /// Whether this refers to a tuple.
287    pub fn is_tuple(&self) -> bool {
288        matches!(self.builtin, Some(BuiltinAdt::Tuple))
289    }
290
291    /// Whether this refers to `str`.
292    pub fn is_str(&self) -> bool {
293        matches!(self.builtin, Some(BuiltinAdt::Str))
294    }
295}
296
297impl TraitDeclRef {
298    pub fn self_ty<'a>(&'a self, krate: &'a TranslatedCrate) -> Option<&'a Ty> {
299        match self.generics.types.iter().next() {
300            Some(ty) => Some(ty),
301            // TODO(mono): A monomorphized trait takes no arguments.
302            None => {
303                let name = krate.item_name(self.id);
304                let args = name.name.last()?.as_monomorphized()?;
305                args.types.iter().next()
306            }
307        }
308    }
309}
310
311impl FnPtr {
312    pub fn new(kind: FnPtrKind, generics: impl Into<BoxedArgs>) -> Self {
313        Self {
314            kind: Box::new(kind),
315            generics: generics.into(),
316        }
317    }
318
319    /// Get the generics for the pre-monomorphization item.
320    pub fn pre_mono_generics<'a>(&'a self, krate: &'a TranslatedCrate) -> &'a GenericArgs {
321        match *self.kind {
322            FnPtrKind::Fun(fun_id) => krate
323                .item_name(fun_id)
324                .mono_args()
325                .unwrap_or(&self.generics),
326            // Can't happen in mono mode.
327            FnPtrKind::Trait(..) => &self.generics,
328        }
329    }
330}
331
332/// A generic `*DeclRef`-shaped struct, used when we're generic over the type of item.
333#[derive(Debug, PartialEq, Eq, Clone, Drive, DriveMut, DriveTwo)]
334pub struct DeclRef<Id> {
335    pub id: Id,
336    pub generics: BoxedArgs,
337    /// If the item is a trait associated item, `generics` are only those of the item, and this
338    /// contains a reference to the trait.
339    // TODO: also store `AssocItemId` so that we can convert to `FnPtr` without
340    // `MaybeBuiltinFunDeclRef`.
341    pub trait_ref: Option<TraitRef>,
342}
343
344impl DeclRef<ItemId> {
345    pub fn try_convert_id<Id>(self) -> Result<DeclRef<Id>, <ItemId as TryInto<Id>>::Error>
346    where
347        ItemId: TryInto<Id>,
348    {
349        Ok(DeclRef {
350            id: self.id.try_into()?,
351            generics: self.generics,
352            trait_ref: self.trait_ref,
353        })
354    }
355}
356
357// Implement `DeclRef<_>` -> `FooDeclRef` conversions.
358macro_rules! convert_item_ref {
359    ($item_ref_ty:ident($id:ident)) => {
360        impl TryFrom<DeclRef<ItemId>> for $item_ref_ty {
361            type Error = ();
362            fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
363                assert!(item.trait_ref.is_none());
364                Ok($item_ref_ty {
365                    id: item.id.try_into()?,
366                    generics: item.generics,
367                })
368            }
369        }
370        impl From<DeclRef<$id>> for $item_ref_ty {
371            fn from(item: DeclRef<$id>) -> Self {
372                assert!(item.trait_ref.is_none());
373                $item_ref_ty {
374                    id: item.id,
375                    generics: item.generics,
376                }
377            }
378        }
379    };
380}
381// We do not provide a `DeclRef<_> -> TypeDeclRef` impl, because we lack information
382// about builtins here.
383convert_item_ref!(FunDeclRef(FunDeclId));
384convert_item_ref!(GlobalDeclRef(GlobalDeclId));
385convert_item_ref!(TraitDeclRef(TraitDeclId));
386convert_item_ref!(TraitImplRef(TraitImplId));
387impl TryFrom<DeclRef<ItemId>> for FnPtr {
388    type Error = ();
389    fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
390        if item.trait_ref.is_some() {
391            panic!(
392                "converting `DeclRef<ItemId>` to `FnPtr` cannot
393                deal with the trait method case."
394            )
395        }
396        let id: FunDeclId = item.id.try_into()?;
397        Ok(FnPtr::new(id.into(), item.generics))
398    }
399}
400impl From<FunDeclRef> for FnPtr {
401    fn from(fn_ref: FunDeclRef) -> Self {
402        FnPtr::new(fn_ref.id.into(), fn_ref.generics)
403    }
404}
405
406/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
407macro_rules! wrap_unwrap_enum {
408    ($enum:ident::$variant:ident($variant_ty:ident)) => {
409        impl TryFrom<$enum> for $variant_ty {
410            type Error = ();
411            fn try_from(x: $enum) -> Result<Self, Self::Error> {
412                match x {
413                    $enum::$variant(x) => Ok(x),
414                    _ => Err(()),
415                }
416            }
417        }
418
419        impl From<$variant_ty> for $enum {
420            fn from(x: $variant_ty) -> Self {
421                $enum::$variant(x)
422            }
423        }
424    };
425}
426
427wrap_unwrap_enum!(ItemId::Fun(FunDeclId));
428wrap_unwrap_enum!(ItemId::Global(GlobalDeclId));
429wrap_unwrap_enum!(ItemId::Type(TypeDeclId));
430wrap_unwrap_enum!(ItemId::TraitDecl(TraitDeclId));
431wrap_unwrap_enum!(ItemId::TraitImpl(TraitImplId));
432wrap_unwrap_enum!(AssocItemId::Type(AssocTypeId));
433wrap_unwrap_enum!(AssocItemId::Method(TraitMethodId));
434wrap_unwrap_enum!(AssocItemId::Const(AssocConstId));
435
436impl From<FunDeclId> for FnPtrKind {
437    fn from(id: FunDeclId) -> Self {
438        Self::Fun(id)
439    }
440}
charon_lib/ast/items/item_ids.rs

charon_lib/ast/items/
item_ids.rs
