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#[cfg_attr(feature = "charon_on_charon", 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(
48    Debug,
49    Clone,
50    PartialEq,
51    Eq,
52    Hash,
53    SerializeState,
54    DeserializeState,
55    Drive,
56    DriveMut,
57    EnumIsA,
58    EnumAsGetters,
59)]
60#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("ImplElem"))]
61pub enum ImplElem {
62    Ty(Box<Binder<Ty>>),
63    Trait(TraitImplId),
64}
65
66/// An item name/path
67///
68/// A name really is a list of strings. However, we sometimes need to
69/// introduce unique indices to disambiguate. This mostly happens because
70/// of "impl" blocks:
71///   ```text
72///   impl<T> List<T> {
73///     ...
74///   }
75///   ```
76///
77/// A type in Rust can have several "impl" blocks, and  those blocks can
78/// contain items with similar names. For this reason, we need to disambiguate
79/// them with unique indices. Rustc calls those "disambiguators". In rustc, this
80/// gives names like this:
81/// - `betree_main::betree::NodeIdCounter{impl#0}::new`
82/// - note that impl blocks can be nested, and macros sometimes generate
83///   weird names (which require disambiguation):
84///   `betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}`
85///
86/// Finally, the paths used by rustc are a lot more precise and explicit than
87/// those we expose in LLBC: for instance, every identifier belongs to a specific
88/// namespace (value namespace, type namespace, etc.), and is coupled with a
89/// disambiguator.
90///
91/// On our side, we want to stay high-level and simple: we use string identifiers
92/// as much as possible, insert disambiguators only when necessary (for instance
93/// when we find an "impl" block or when two loaded crates have the same name)
94/// and check that the disambiguator is useless in the other situations (i.e.,
95/// the disambiguator is always equal to 0).
96///
97/// Moreover, the items are uniquely disambiguated by their (integer) ids
98/// (`TypeDeclId`, etc.), and when extracting the code we have to deal with
99/// name clashes anyway. Still, we might want to be more precise in the future.
100///
101/// Also note that the first path element in the name is always the crate name.
102#[derive(
103    Debug, Default, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut,
104)]
105#[serde(transparent)]
106#[cfg_attr(feature = "charon_on_charon", charon::transparent)]
107pub struct Name {
108    pub name: Vec<PathElem>,
109}
charon_lib/ast/names.rs

charon_lib/ast/
names.rs
