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

charon_lib/ast/
names.rs
