charon_lib/ast/
names.rs

1//! Defines some utilities for the variables
2use crate::ast::*;
3use derive_generic_visitor::{Drive, DriveMut};
4use macros::{EnumAsGetters, EnumIsA};
5use serde_state::{DeserializeState, SerializeState};
6
7generate_index_type!(Disambiguator);
8
9/// See the comments for [Name]
10#[derive(
11    Debug,
12    Clone,
13    PartialEq,
14    Eq,
15    Hash,
16    SerializeState,
17    DeserializeState,
18    Drive,
19    DriveMut,
20    EnumIsA,
21    EnumAsGetters,
22)]
23#[charon::variants_prefix("Pe")]
24pub enum PathElem {
25    #[serde_state(stateless)]
26    Ident(#[drive(skip)] String, Disambiguator),
27    Impl(ImplElem),
28    /// This item was obtained by instantiating its parent with the given args. The binder binds
29    /// the parameters of the new items. If the binder binds nothing then this is a
30    /// monomorphization.
31    Instantiated(Box<Binder<GenericArgs>>),
32    /// This item is only available on the given target. Only appears in multi-target mode.
33    #[serde_state(stateless)]
34    Target(#[drive(skip)] TargetTriple),
35}
36
37/// There are two kinds of `impl` blocks:
38/// - impl blocks linked to a type ("inherent" impl blocks following Rust terminology):
39///   ```text
40///   impl<T> List<T> { ...}
41///   ```
42/// - trait impl blocks:
43///   ```text
44///   impl<T> PartialEq for List<T> { ...}
45///   ```
46/// We distinguish the two.
47#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
48#[charon::variants_prefix("ImplElem")]
49pub enum ImplElem {
50    Ty(Box<Binder<Ty>>),
51    Trait(TraitImplId),
52}
53
54/// An item name/path
55///
56/// A name really is a list of strings. However, we sometimes need to
57/// introduce unique indices to disambiguate. This mostly happens because
58/// of "impl" blocks:
59///   ```text
60///   impl<T> List<T> {
61///     ...
62///   }
63///   ```
64///
65/// A type in Rust can have several "impl" blocks, and  those blocks can
66/// contain items with similar names. For this reason, we need to disambiguate
67/// them with unique indices. Rustc calls those "disambiguators". In rustc, this
68/// gives names like this:
69/// - `betree_main::betree::NodeIdCounter{impl#0}::new`
70/// - note that impl blocks can be nested, and macros sometimes generate
71///   weird names (which require disambiguation):
72///   `betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}`
73///
74/// Finally, the paths used by rustc are a lot more precise and explicit than
75/// those we expose in LLBC: for instance, every identifier belongs to a specific
76/// namespace (value namespace, type namespace, etc.), and is coupled with a
77/// disambiguator.
78///
79/// On our side, we want to stay high-level and simple: we use string identifiers
80/// as much as possible, insert disambiguators only when necessary (whenever
81/// we find an "impl" block, typically) and check that the disambiguator is useless
82/// in the other situations (i.e., the disambiguator is always equal to 0).
83///
84/// Moreover, the items are uniquely disambiguated by their (integer) ids
85/// (`TypeDeclId`, etc.), and when extracting the code we have to deal with
86/// name clashes anyway. Still, we might want to be more precise in the future.
87///
88/// Also note that the first path element in the name is always the crate name.
89#[derive(
90    Debug, Default, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut,
91)]
92#[serde(transparent)]
93pub struct Name {
94    pub name: Vec<PathElem>,
95}
charon_lib/ast/names.rs

charon_lib/ast/
names.rs
