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

charon_lib/ast/
names.rs
