charon_lib/ast/
krate.rs

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

charon_lib/ast/
krate.rs
