charon_lib/ast/
krate.rs

1use std::cmp::{Ord, PartialOrd};
2use std::fmt;
3
4use derive_generic_visitor::{ControlFlow, Drive, DriveMut, DriveTwo};
5use index_vec::Idx;
6use itertools::Itertools;
7use serde::{Deserialize, Serialize};
8use serde_state::{DeserializeState, SerializeState};
9
10use crate::ast::*;
11use crate::common::serialize_map_to_array::SeqHashMapToArray;
12use crate::formatter::{FmtCtx, IntoFormatter};
13use crate::ids::{IndexMap, IndexVec};
14use crate::pretty::FmtWithCtx;
15use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
16
17generate_index_type!(FunDeclId, "Fun");
18generate_index_type!(TypeDeclId, "Adt");
19generate_index_type!(GlobalDeclId, "Global");
20generate_index_type!(TraitDeclId, "TraitDecl");
21generate_index_type!(TraitImplId, "TraitImpl");
22
23/// The id of a translated item.
24#[derive(
25    Copy,
26    Clone,
27    Debug,
28    PartialOrd,
29    Ord,
30    PartialEq,
31    Eq,
32    Hash,
33    EnumIsA,
34    EnumAsGetters,
35    VariantName,
36    VariantIndexArity,
37    Serialize,
38    Deserialize,
39    SerializeState,
40    DeserializeState,
41    Drive,
42    DriveMut,
43    DriveTwo,
44)]
45#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Id"))]
46#[serde_state(stateless)]
47pub enum ItemId {
48    Type(TypeDeclId),
49    TraitDecl(TraitDeclId),
50    TraitImpl(TraitImplId),
51    Fun(FunDeclId),
52    Global(GlobalDeclId),
53}
54
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/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
85macro_rules! wrap_unwrap_enum {
86    ($enum:ident::$variant:ident($variant_ty:ident)) => {
87        impl TryFrom<$enum> for $variant_ty {
88            type Error = ();
89            fn try_from(x: $enum) -> Result<Self, Self::Error> {
90                match x {
91                    $enum::$variant(x) => Ok(x),
92                    _ => Err(()),
93                }
94            }
95        }
96
97        impl From<$variant_ty> for $enum {
98            fn from(x: $variant_ty) -> Self {
99                $enum::$variant(x)
100            }
101        }
102    };
103}
104
105wrap_unwrap_enum!(ItemId::Fun(FunDeclId));
106wrap_unwrap_enum!(ItemId::Global(GlobalDeclId));
107wrap_unwrap_enum!(ItemId::Type(TypeDeclId));
108wrap_unwrap_enum!(ItemId::TraitDecl(TraitDeclId));
109wrap_unwrap_enum!(ItemId::TraitImpl(TraitImplId));
110impl TryFrom<ItemId> for TypeId {
111    type Error = ();
112    fn try_from(x: ItemId) -> Result<Self, Self::Error> {
113        Ok(TypeId::Adt(x.try_into()?))
114    }
115}
116impl TryFrom<ItemId> for FunId {
117    type Error = ();
118    fn try_from(x: ItemId) -> Result<Self, Self::Error> {
119        Ok(FunId::Regular(x.try_into()?))
120    }
121}
122
123wrap_unwrap_enum!(AssocItemId::Type(AssocTypeId));
124wrap_unwrap_enum!(AssocItemId::Method(TraitMethodId));
125wrap_unwrap_enum!(AssocItemId::Const(AssocConstId));
126
127/// A translated item.
128#[derive(
129    Debug,
130    PartialEq,
131    Eq,
132    EnumIsA,
133    EnumAsGetters,
134    VariantName,
135    VariantIndexArity,
136    Drive,
137    DriveMut,
138    DriveTwo,
139)]
140pub enum ItemByVal {
141    Type(TypeDecl),
142    Fun(FunDecl),
143    Global(GlobalDecl),
144    TraitDecl(TraitDecl),
145    TraitImpl(TraitImpl),
146}
147
148/// A reference to a translated item.
149#[derive(
150    Debug,
151    Clone,
152    Copy,
153    EnumIsA,
154    EnumAsGetters,
155    VariantName,
156    VariantIndexArity,
157    Drive,
158    DriveMut,
159    DriveTwo,
160)]
161pub enum ItemRef<'ctx> {
162    Type(&'ctx TypeDecl),
163    Fun(&'ctx FunDecl),
164    Global(&'ctx GlobalDecl),
165    TraitDecl(&'ctx TraitDecl),
166    TraitImpl(&'ctx TraitImpl),
167}
168
169/// A mutable reference to a translated item.
170#[derive(
171    Debug,
172    PartialEq,
173    Eq,
174    EnumIsA,
175    EnumAsGetters,
176    VariantName,
177    VariantIndexArity,
178    Drive,
179    DriveMut,
180    DriveTwo,
181)]
182pub enum ItemRefMut<'ctx> {
183    Type(&'ctx mut TypeDecl),
184    Fun(&'ctx mut FunDecl),
185    Global(&'ctx mut GlobalDecl),
186    TraitDecl(&'ctx mut TraitDecl),
187    TraitImpl(&'ctx mut TraitImpl),
188}
189
190/// A (group of) top-level declaration(s), properly reordered.
191/// "G" stands for "generic"
192#[derive(
193    Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize,
194)]
195#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Group"))]
196pub enum GDeclarationGroup<Id> {
197    /// A non-recursive declaration
198    NonRec(Id),
199    /// A (group of mutually) recursive declaration(s)
200    Rec(Vec<Id>),
201}
202
203/// A (group of) top-level declaration(s), properly reordered.
204#[derive(
205    Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize,
206)]
207#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Group"))]
208pub enum DeclarationGroup {
209    /// A type declaration group
210    Type(GDeclarationGroup<TypeDeclId>),
211    /// A function declaration group
212    Fun(GDeclarationGroup<FunDeclId>),
213    /// A global declaration group
214    Global(GDeclarationGroup<GlobalDeclId>),
215    TraitDecl(GDeclarationGroup<TraitDeclId>),
216    TraitImpl(GDeclarationGroup<TraitImplId>),
217    /// Anything that doesn't fit into these categories.
218    Mixed(GDeclarationGroup<ItemId>),
219}
220
221pub type DeclarationsGroups = Vec<DeclarationGroup>;
222
223/// A target triple, e.g. `x86_64-unknown-linux-gnu`.
224pub type TargetTriple = String;
225
226#[derive(Clone, Drive, DriveMut, DriveTwo, SerializeState, DeserializeState)]
227#[serde_state(stateless)]
228pub struct TargetInfo {
229    /// The pointer size of the target in bytes.
230    pub target_pointer_size: types::ByteCount,
231    /// Whether the target platform uses little endian byte order.
232    pub is_little_endian: bool,
233    /// The minimum size of a [`repr(C)`] enum.
234    pub c_enum_min_size: types::ByteCount,
235    /// Alignments for primitive types.
236    #[serde(with = "SeqHashMapToArray::<LiteralTy, ByteCount>")]
237    pub primitive_alignments: SeqHashMap<LiteralTy, ByteCount>,
238}
239
240#[derive(Default, Clone, Drive, DriveMut, DriveTwo, SerializeState, DeserializeState)]
241pub struct AssocItemNames {
242    pub types: IndexVec<AssocTypeId, TraitItemName>,
243    pub methods: IndexVec<TraitMethodId, TraitItemName>,
244    pub consts: IndexVec<AssocConstId, TraitItemName>,
245}
246
247/// The complete data of a Rust crate.
248///
249/// A crate is mainly composed of 5 kinds of items:
250/// - Functions;
251/// - Type definitions;
252/// - Globals (constants and statics);
253/// - Trait declarations;
254/// - Trait implementations.
255///
256/// These can each be found in the corresponding `IndexVec`. They are in an unspecified (though
257/// deterministic) order.
258/// If you need a more robust order, see `ordered_decls`.
259///
260/// To get a `TranslatedCrate`, run `charon cargo` inside a Rust crate, then deserialize
261/// the resulting `crate_name.llbc` file using [`crate::deserialize_llbc`].
262#[derive(Default, Clone, Drive, DriveMut, DriveTwo, SerializeState, DeserializeState)]
263#[serde_state(state_implements = HashConsSerializerState)]
264pub struct TranslatedCrate {
265    /// The name of the crate.
266    #[drive(skip)]
267    pub crate_name: String,
268
269    /// The options used when calling Charon. Can be used to check that Charon was called with the
270    /// options that a given consumer requires.
271    #[drive(skip)]
272    #[serde_state(stateless)]
273    pub options: crate::options::CliOpts,
274
275    /// Information about each target platform for which the crate was translated. When translating
276    /// a crate normally this will have a single entry; when using `--targets` this will have one
277    /// entry per chosen target.
278    #[drive(skip)]
279    #[serde(with = "SeqHashMapToArray::<TargetTriple, TargetInfo>")]
280    pub target_information: SeqHashMap<TargetTriple, TargetInfo>,
281
282    /// The source files composing the crate and its dependencies. Each [`Span`] refers to a byte
283    /// range within one of these files.
284    // This field must come before any field containing spans, as the OCaml deserialization of
285    // spans requires the files to be deserialized already.
286    #[serde_state(stateless)]
287    pub files: IndexVec<FileId, File>,
288
289    /// The names of all registered items. Available so we can know the names even of items that
290    /// failed to translate.
291    /// Invariant: after translation, any existing `ItemId` must have an associated name, even
292    /// if the corresponding item wasn't translated.
293    #[serde(with = "SeqHashMapToArray::<ItemId, Name>")]
294    pub item_names: SeqHashMap<ItemId, Name>,
295    /// The names of all the registered associated items. Available so we can know the names even
296    /// of items that failed to translate.
297    /// Invariant: after translation, any existing `AssocItemId` must have an associated name, even
298    /// if the corresponding item wasn't translated.
299    pub assoc_item_names: IndexMap<TraitDeclId, AssocItemNames>,
300    /// Short names, for items whose last PathElem is unique.
301    #[serde(with = "SeqHashMapToArray::<ItemId, Name>")]
302    pub short_names: SeqHashMap<ItemId, Name>,
303
304    /// The type definitions (structs, enums, ...).
305    pub type_decls: IndexMap<TypeDeclId, TypeDecl>,
306    /// The function definitions.
307    ///
308    /// Each item with a body becomes a function: actual functions, methods, and unevaluated
309    /// consts/statics.
310    pub fun_decls: IndexMap<FunDeclId, FunDecl>,
311    /// The global definitions, which are constants, statics, and thread locals.
312    pub global_decls: IndexMap<GlobalDeclId, GlobalDecl>,
313    /// The trait declarations.
314    pub trait_decls: IndexMap<TraitDeclId, TraitDecl>,
315    /// The trait implementations.
316    pub trait_impls: IndexMap<TraitImplId, TraitImpl>,
317    /// This contains a list of all the reachable items in the crate in a stable, logical order
318    /// based on crate and file order, then further grouped and sorted such that every item comes
319    /// after the items it depends on.
320    /// Mutually-dependent groups of items are identified as such.
321    /// This is meant for code-generation tools that want a stable output order.
322    ///
323    /// Not all the items in the `TranslatedCrate` are included: some trait impls are never
324    /// referred to by reachable items so could in principle be removed from the crate, but we keep
325    /// them around to be able to tell method implementations apart.
326    ///
327    /// `Some` after translation unless `--no-reorder-decls` is passed.
328    #[drive(skip)]
329    #[serde_state(stateless)]
330    pub ordered_decls: Option<DeclarationsGroups>,
331}
332
333impl TranslatedCrate {
334    pub fn item_name(&self, id: impl Into<ItemId>) -> &Name {
335        // `unwrap` is ok because we ensure to translate the item name as soon as we create a new
336        // item id.
337        self.item_names.get(&id.into()).unwrap()
338    }
339    pub fn assoc_item_name(
340        &self,
341        trait_id: TraitDeclId,
342        id: impl Into<AssocItemId>,
343    ) -> TraitItemName {
344        let names = &self.assoc_item_names[trait_id];
345        match id.into() {
346            AssocItemId::Type(id) => names.types[id],
347            AssocItemId::Method(id) => names.methods[id],
348            AssocItemId::Const(id) => names.consts[id],
349        }
350    }
351
352    pub fn item_short_name(&self, id: impl Into<ItemId>) -> &Name {
353        let id = id.into();
354        self.short_names
355            .get(&id)
356            .unwrap_or_else(|| self.item_name(id))
357    }
358
359    pub fn get_item(&self, trans_id: impl Into<ItemId>) -> Option<ItemRef<'_>> {
360        match trans_id.into() {
361            ItemId::Type(id) => self.type_decls.get(id).map(ItemRef::Type),
362            ItemId::Fun(id) => self.fun_decls.get(id).map(ItemRef::Fun),
363            ItemId::Global(id) => self.global_decls.get(id).map(ItemRef::Global),
364            ItemId::TraitDecl(id) => self.trait_decls.get(id).map(ItemRef::TraitDecl),
365            ItemId::TraitImpl(id) => self.trait_impls.get(id).map(ItemRef::TraitImpl),
366        }
367    }
368    pub fn get_item_mut(&mut self, trans_id: ItemId) -> Option<ItemRefMut<'_>> {
369        match trans_id {
370            ItemId::Type(id) => self.type_decls.get_mut(id).map(ItemRefMut::Type),
371            ItemId::Fun(id) => self.fun_decls.get_mut(id).map(ItemRefMut::Fun),
372            ItemId::Global(id) => self.global_decls.get_mut(id).map(ItemRefMut::Global),
373            ItemId::TraitDecl(id) => self.trait_decls.get_mut(id).map(ItemRefMut::TraitDecl),
374            ItemId::TraitImpl(id) => self.trait_impls.get_mut(id).map(ItemRefMut::TraitImpl),
375        }
376    }
377
378    /// Remove this item from the crate, including the name information about it.
379    ///
380    /// See also [`TranslatedCrate::remove_item_temporarily`].
381    pub fn remove_item(&mut self, trans_id: ItemId) -> Option<ItemByVal> {
382        self.short_names.swap_remove(&trans_id);
383        self.item_names.swap_remove(&trans_id);
384        self.remove_item_temporarily(trans_id)
385    }
386    /// Insert a new item into a slot, and record its name in the name map.
387    pub fn set_new_item_slot(&mut self, id: ItemId, item: impl Into<ItemByVal>) {
388        let item = item.into();
389        self.item_names
390            .insert(id, item.as_ref().item_meta().name.clone());
391        self.put_item_back(id, item);
392    }
393    /// Remove this item from the crate without touching the name maps.
394    /// Useful for modifying items whilst being able to access the rest of the crate.
395    /// Put the item back using [`TranslatedCrate::put_item_back`].
396    ///
397    /// See also [`TranslatedCrate::remove_item`].
398    pub fn remove_item_temporarily(&mut self, trans_id: ItemId) -> Option<ItemByVal> {
399        match trans_id {
400            ItemId::Type(id) => self.type_decls.remove(id).map(ItemByVal::Type),
401            ItemId::Fun(id) => self.fun_decls.remove(id).map(ItemByVal::Fun),
402            ItemId::Global(id) => self.global_decls.remove(id).map(ItemByVal::Global),
403            ItemId::TraitDecl(id) => self.trait_decls.remove(id).map(ItemByVal::TraitDecl),
404            ItemId::TraitImpl(id) => self.trait_impls.remove(id).map(ItemByVal::TraitImpl),
405        }
406    }
407    /// Insert the item into the corresponding slot without recording its name in the name map.
408    /// Only use if the item already has its name registered, e.g. if you got it using
409    /// [`TranslatedCrate::remove_item_temporarily`].
410    pub fn put_item_back(&mut self, id: ItemId, item: impl Into<ItemByVal>) {
411        match item.into() {
412            ItemByVal::Type(decl) => self.type_decls.set_slot(*id.as_type().unwrap(), decl),
413            ItemByVal::Fun(decl) => self.fun_decls.set_slot(*id.as_fun().unwrap(), decl),
414            ItemByVal::Global(decl) => self.global_decls.set_slot(*id.as_global().unwrap(), decl),
415            ItemByVal::TraitDecl(decl) => self
416                .trait_decls
417                .set_slot(*id.as_trait_decl().unwrap(), decl),
418            ItemByVal::TraitImpl(decl) => self
419                .trait_impls
420                .set_slot(*id.as_trait_impl().unwrap(), decl),
421        }
422    }
423
424    pub fn all_ids(&self) -> impl Iterator<Item = ItemId> + use<> {
425        self.type_decls
426            .all_indices()
427            .map(ItemId::Type)
428            .chain(self.trait_decls.all_indices().map(ItemId::TraitDecl))
429            .chain(self.trait_impls.all_indices().map(ItemId::TraitImpl))
430            .chain(self.global_decls.all_indices().map(ItemId::Global))
431            .chain(self.fun_decls.all_indices().map(ItemId::Fun))
432    }
433    pub fn all_items(&self) -> impl Iterator<Item = ItemRef<'_>> {
434        self.type_decls
435            .iter()
436            .map(ItemRef::Type)
437            .chain(self.trait_decls.iter().map(ItemRef::TraitDecl))
438            .chain(self.trait_impls.iter().map(ItemRef::TraitImpl))
439            .chain(self.global_decls.iter().map(ItemRef::Global))
440            .chain(self.fun_decls.iter().map(ItemRef::Fun))
441    }
442    pub fn all_items_mut(&mut self) -> impl Iterator<Item = ItemRefMut<'_>> {
443        self.type_decls
444            .iter_mut()
445            .map(ItemRefMut::Type)
446            .chain(self.trait_impls.iter_mut().map(ItemRefMut::TraitImpl))
447            .chain(self.trait_decls.iter_mut().map(ItemRefMut::TraitDecl))
448            .chain(self.fun_decls.iter_mut().map(ItemRefMut::Fun))
449            .chain(self.global_decls.iter_mut().map(ItemRefMut::Global))
450    }
451    pub fn all_items_with_ids(&self) -> impl Iterator<Item = (ItemId, ItemRef<'_>)> {
452        self.all_items().map(|item| (item.id(), item))
453    }
454
455    /// When translating without `--target`, there's only one target information; this method
456    /// retrieves it.
457    /// Panics if this crate was translated in multi-target mode.
458    pub fn the_target_information(&self) -> &TargetInfo {
459        self.target_information
460            .values()
461            .exactly_one()
462            .ok()
463            .expect("called `the_target_information` on a multi-target crate")
464    }
465}
466
467impl ItemByVal {
468    pub fn as_ref(&self) -> ItemRef<'_> {
469        match self {
470            Self::Type(d) => ItemRef::Type(d),
471            Self::Fun(d) => ItemRef::Fun(d),
472            Self::Global(d) => ItemRef::Global(d),
473            Self::TraitDecl(d) => ItemRef::TraitDecl(d),
474            Self::TraitImpl(d) => ItemRef::TraitImpl(d),
475        }
476    }
477    pub fn as_mut(&mut self) -> ItemRefMut<'_> {
478        match self {
479            Self::Type(d) => ItemRefMut::Type(d),
480            Self::Fun(d) => ItemRefMut::Fun(d),
481            Self::Global(d) => ItemRefMut::Global(d),
482            Self::TraitDecl(d) => ItemRefMut::TraitDecl(d),
483            Self::TraitImpl(d) => ItemRefMut::TraitImpl(d),
484        }
485    }
486}
487
488impl<'ctx> ItemRef<'ctx> {
489    pub fn id(&self) -> ItemId {
490        match self {
491            ItemRef::Type(d) => d.def_id.into(),
492            ItemRef::Fun(d) => d.def_id.into(),
493            ItemRef::Global(d) => d.def_id.into(),
494            ItemRef::TraitDecl(d) => d.def_id.into(),
495            ItemRef::TraitImpl(d) => d.def_id.into(),
496        }
497    }
498
499    pub fn to_owned(&self) -> ItemByVal {
500        match *self {
501            Self::Type(d) => ItemByVal::Type(d.clone()),
502            Self::Fun(d) => ItemByVal::Fun(d.clone()),
503            Self::Global(d) => ItemByVal::Global(d.clone()),
504            Self::TraitDecl(d) => ItemByVal::TraitDecl(d.clone()),
505            Self::TraitImpl(d) => ItemByVal::TraitImpl(d.clone()),
506        }
507    }
508
509    pub fn item_meta(&self) -> &'ctx ItemMeta {
510        match self {
511            Self::Type(d) => &d.item_meta,
512            Self::Fun(d) => &d.item_meta,
513            Self::Global(d) => &d.item_meta,
514            Self::TraitDecl(d) => &d.item_meta,
515            Self::TraitImpl(d) => &d.item_meta,
516        }
517    }
518    /// The generic parameters of this item.
519    pub fn generic_params(&self) -> &'ctx GenericParams {
520        match self {
521            ItemRef::Type(d) => &d.generics,
522            ItemRef::Fun(d) => &d.generics,
523            ItemRef::Global(d) => &d.generics,
524            ItemRef::TraitDecl(d) => &d.generics,
525            ItemRef::TraitImpl(d) => &d.generics,
526        }
527    }
528
529    /// Get information about the parent of this item, if any.
530    pub fn parent_info(&self) -> &'ctx ItemSource {
531        match self {
532            ItemRef::Fun(d) => &d.src,
533            ItemRef::Global(d) => &d.src,
534            ItemRef::Type(_) | ItemRef::TraitDecl(_) | ItemRef::TraitImpl(_) => {
535                &ItemSource::TopLevel
536            }
537        }
538    }
539
540    /// See [`GenericParams::identity_args`].
541    pub fn identity_args(&self) -> GenericArgs {
542        self.generic_params().identity_args()
543    }
544
545    /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
546    /// `ItemRef` isn't contained in any of our types.
547    pub fn drive<V: VisitAst>(&self, visitor: &mut V) -> ControlFlow<V::Break> {
548        match *self {
549            ItemRef::Type(d) => visitor.visit(d),
550            ItemRef::Fun(d) => visitor.visit(d),
551            ItemRef::Global(d) => visitor.visit(d),
552            ItemRef::TraitDecl(d) => visitor.visit(d),
553            ItemRef::TraitImpl(d) => visitor.visit(d),
554        }
555    }
556
557    /// Visit all occurrences of that type inside `self`, in pre-order traversal.
558    pub fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
559        match *self {
560            ItemRef::Type(d) => d.dyn_visit(f),
561            ItemRef::Fun(d) => d.dyn_visit(f),
562            ItemRef::Global(d) => d.dyn_visit(f),
563            ItemRef::TraitDecl(d) => d.dyn_visit(f),
564            ItemRef::TraitImpl(d) => d.dyn_visit(f),
565        }
566    }
567}
568
569impl<'ctx> ItemRefMut<'ctx> {
570    pub fn as_ref(&self) -> ItemRef<'_> {
571        match self {
572            ItemRefMut::Type(d) => ItemRef::Type(d),
573            ItemRefMut::Fun(d) => ItemRef::Fun(d),
574            ItemRefMut::Global(d) => ItemRef::Global(d),
575            ItemRefMut::TraitDecl(d) => ItemRef::TraitDecl(d),
576            ItemRefMut::TraitImpl(d) => ItemRef::TraitImpl(d),
577        }
578    }
579    pub fn reborrow(&mut self) -> ItemRefMut<'_> {
580        match self {
581            ItemRefMut::Type(d) => ItemRefMut::Type(d),
582            ItemRefMut::Fun(d) => ItemRefMut::Fun(d),
583            ItemRefMut::Global(d) => ItemRefMut::Global(d),
584            ItemRefMut::TraitDecl(d) => ItemRefMut::TraitDecl(d),
585            ItemRefMut::TraitImpl(d) => ItemRefMut::TraitImpl(d),
586        }
587    }
588
589    pub fn set_id(&mut self, id: ItemId) {
590        match (self, id) {
591            (Self::Type(d), ItemId::Type(id)) => d.def_id = id,
592            (Self::Fun(d), ItemId::Fun(id)) => d.def_id = id,
593            (Self::Global(d), ItemId::Global(id)) => d.def_id = id,
594            (Self::TraitDecl(d), ItemId::TraitDecl(id)) => d.def_id = id,
595            (Self::TraitImpl(d), ItemId::TraitImpl(id)) => d.def_id = id,
596            _ => unreachable!(),
597        }
598    }
599
600    pub fn item_meta(&mut self) -> &mut ItemMeta {
601        match self {
602            Self::Type(d) => &mut d.item_meta,
603            Self::Fun(d) => &mut d.item_meta,
604            Self::Global(d) => &mut d.item_meta,
605            Self::TraitDecl(d) => &mut d.item_meta,
606            Self::TraitImpl(d) => &mut d.item_meta,
607        }
608    }
609    /// The generic parameters of this item.
610    pub fn generic_params(&mut self) -> &mut GenericParams {
611        match self {
612            ItemRefMut::Type(d) => &mut d.generics,
613            ItemRefMut::Fun(d) => &mut d.generics,
614            ItemRefMut::Global(d) => &mut d.generics,
615            ItemRefMut::TraitDecl(d) => &mut d.generics,
616            ItemRefMut::TraitImpl(d) => &mut d.generics,
617        }
618    }
619
620    /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
621    /// `ItemRefMut` isn't contained in any of our types.
622    pub fn drive_mut<V: VisitAstMut>(&mut self, visitor: &mut V) -> ControlFlow<V::Break> {
623        match self {
624            ItemRefMut::Type(d) => visitor.visit(*d),
625            ItemRefMut::Fun(d) => visitor.visit(*d),
626            ItemRefMut::Global(d) => visitor.visit(*d),
627            ItemRefMut::TraitDecl(d) => visitor.visit(*d),
628            ItemRefMut::TraitImpl(d) => visitor.visit(*d),
629        }
630    }
631
632    /// Visit all occurrences of that type inside `self`, in pre-order traversal.
633    pub fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T)) {
634        match self {
635            ItemRefMut::Type(d) => d.dyn_visit_mut(f),
636            ItemRefMut::Fun(d) => d.dyn_visit_mut(f),
637            ItemRefMut::Global(d) => d.dyn_visit_mut(f),
638            ItemRefMut::TraitDecl(d) => d.dyn_visit_mut(f),
639            ItemRefMut::TraitImpl(d) => d.dyn_visit_mut(f),
640        }
641    }
642}
643
644impl fmt::Display for TranslatedCrate {
645    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
646        let fmt: &FmtCtx = &self.into_fmt();
647        match &self.ordered_decls {
648            None => {
649                // We do simple: types, globals, traits, functions
650                for d in &self.type_decls {
651                    writeln!(f, "{}\n", d.with_ctx(fmt))?
652                }
653                for d in &self.global_decls {
654                    writeln!(f, "{}\n", d.with_ctx(fmt))?
655                }
656                for d in &self.trait_decls {
657                    writeln!(f, "{}\n", d.with_ctx(fmt))?
658                }
659                for d in &self.trait_impls {
660                    writeln!(f, "{}\n", d.with_ctx(fmt))?
661                }
662                for d in &self.fun_decls {
663                    writeln!(f, "{}\n", d.with_ctx(fmt))?
664                }
665            }
666            Some(ordered_decls) => {
667                for gr in ordered_decls {
668                    for id in gr.get_ids() {
669                        writeln!(f, "{}\n", fmt.format_decl_id(id))?
670                    }
671                }
672            }
673        }
674        fmt::Result::Ok(())
675    }
676}
677
678impl<'a> IntoFormatter for &'a TranslatedCrate {
679    type C = FmtCtx<'a>;
680
681    fn into_fmt(self) -> Self::C {
682        FmtCtx {
683            translated: Some(self),
684            ..Default::default()
685        }
686    }
687}
688
689pub trait HasIdxMapOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
690    fn get_idx_map(&self) -> &IndexMap<Id, Self::Output>;
691    fn get_idx_map_mut(&mut self) -> &mut IndexMap<Id, Self::Output>;
692}
693
694/// Delegate `Index` implementations to subfields.
695macro_rules! mk_index_impls {
696    ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
697        impl std::ops::Index<$idx> for $ty {
698            type Output = $output;
699            fn index(&self, index: $idx) -> &Self::Output {
700                &self.$field[index]
701            }
702        }
703        impl std::ops::IndexMut<$idx> for $ty {
704            fn index_mut(&mut self, index: $idx) -> &mut Self::Output {
705                &mut self.$field[index]
706            }
707        }
708        impl HasIdxMapOf<$idx> for $ty {
709            fn get_idx_map(&self) -> &IndexMap<$idx, Self::Output> {
710                &self.$field
711            }
712            fn get_idx_map_mut(&mut self) -> &mut IndexMap<$idx, Self::Output> {
713                &mut self.$field
714            }
715        }
716    };
717}
718mk_index_impls!(TranslatedCrate.type_decls[TypeDeclId]: TypeDecl);
719mk_index_impls!(TranslatedCrate.fun_decls[FunDeclId]: FunDecl);
720mk_index_impls!(TranslatedCrate.global_decls[GlobalDeclId]: GlobalDecl);
721mk_index_impls!(TranslatedCrate.trait_decls[TraitDeclId]: TraitDecl);
722mk_index_impls!(TranslatedCrate.trait_impls[TraitImplId]: TraitImpl);
charon_lib/ast/krate.rs

charon_lib/ast/
krate.rs
