charon_lib/ast/
names.rs

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

charon_lib/ast/
names.rs
