charon_lib/transform/add_missing_info/
compute_short_names.rs

1use std::collections::{HashMap, hash_map::Entry};
2
3use crate::ast::*;
4
5use crate::transform::{TransformCtx, ctx::TransformPass};
6
7enum FoundName<'a> {
8    Unique {
9        long: &'a [PathElem],
10        ids: Vec<ItemId>,
11    },
12    Multiple,
13}
14
15fn register_short_name_candidate<'a>(
16    short_names: &mut HashMap<PathElem, FoundName<'a>>,
17    short: PathElem,
18    long: &'a [PathElem],
19    id: ItemId,
20) {
21    match short_names.entry(short) {
22        Entry::Occupied(mut e) => match e.get_mut() {
23            FoundName::Unique {
24                long: found_long,
25                ids,
26            } => {
27                if *found_long == long {
28                    ids.push(id)
29                } else {
30                    e.insert(FoundName::Multiple);
31                }
32            }
33            FoundName::Multiple => {}
34        },
35        Entry::Vacant(e) => {
36            e.insert(FoundName::Unique {
37                long,
38                ids: vec![id],
39            });
40        }
41    }
42}
43
44pub struct Transform;
45impl TransformPass for Transform {
46    fn transform_ctx(&self, ctx: &mut TransformCtx) {
47        ctx.translated.short_names.clear();
48        let mut short_names: HashMap<PathElem, FoundName> = Default::default();
49        for (&id, name) in &ctx.translated.item_names {
50            let mut name_slice = name.name.as_slice();
51
52            // Trait impls are sufficiently unique information, so truncate starting from the
53            // rightmost impl.
54            if let Some((i, _)) = name_slice
55                .iter()
56                .enumerate()
57                .rfind(|(_, elem)| matches!(elem, PathElem::Impl(ImplElem::Trait(..), ..)))
58            {
59                name_slice = &name.name[i..];
60                let trunc_name = Name {
61                    name: name_slice.to_vec(),
62                };
63                ctx.translated.short_names.insert(id, trunc_name);
64            }
65
66            if let [prefix @ .., PathElem::Instantiated(..)] = name_slice {
67                name_slice = prefix;
68            }
69            // Ignoring monomorphizations and disambiguators, if a name is the only one to end with
70            // a given suffix, we accumulate the ids of all the items with that name (there may be
71            // several thanks to monomorphizations).
72            let candidate = match name_slice {
73                [.., PathElem::Ident(ident, _)] => {
74                    Some(PathElem::Ident(ident.clone(), Disambiguator::ZERO))
75                }
76                // Tuples and `str` are excluded: those are types with a syntax of their own.
77                [.., PathElem::Builtin(builtin, _)] if !builtin.is_tuple() && !builtin.is_str() => {
78                    Some(PathElem::Builtin(*builtin, Disambiguator::ZERO))
79                }
80                [PathElem::Impl(ImplElem::Trait(impl_id))]
81                    if let Some(trait_impl) = ctx.translated.trait_impls.get(*impl_id) =>
82                {
83                    trait_impl_short_name(&ctx.translated.item_names, trait_impl)
84                        .map(|short| PathElem::Ident(short, Disambiguator::ZERO))
85                }
86
87                _ => None,
88            };
89            if let Some(short) = candidate {
90                register_short_name_candidate(&mut short_names, short, name_slice, id);
91            }
92        }
93
94        for (short, found) in short_names {
95            if let FoundName::Unique { ids, .. } = found {
96                for id in ids {
97                    let mut short_name = Name {
98                        name: vec![short.clone()],
99                    };
100                    if let [.., mono @ PathElem::Instantiated(..)] =
101                        ctx.translated.item_names[&id].name.as_slice()
102                    {
103                        short_name.name.push(mono.clone());
104                    }
105                    ctx.translated.short_names.insert(id, short_name);
106                }
107            }
108        }
109    }
110}
111
112fn trait_impl_short_name(
113    item_names: &SeqHashMap<ItemId, Name>,
114    trait_impl: &TraitImpl,
115) -> Option<String> {
116    fn args_to_idents(
117        item_names: &SeqHashMap<ItemId, Name>,
118        generics: &GenericArgs,
119    ) -> Vec<String> {
120        generics
121            .types
122            .iter()
123            .filter_map(|t| ty_to_idents(item_names, t))
124            .collect()
125    }
126
127    fn ty_to_idents(item_names: &SeqHashMap<ItemId, Name>, ty: &Ty) -> Option<String> {
128        Some(match ty.kind() {
129            TyKind::Scalar(scalar) => scalar.to_string(),
130            TyKind::Slice(..) => "slice".to_owned(),
131            TyKind::Array(..) => "array".to_owned(),
132            TyKind::Adt(tref) => item_to_ident(item_names, ItemId::Type(tref.id))?,
133            _ => return None,
134        })
135    }
136
137    fn item_to_ident(item_names: &SeqHashMap<ItemId, Name>, id: ItemId) -> Option<String> {
138        Some(item_names.get(&id)?.short_str()?.to_owned())
139    }
140
141    let trait_id = trait_impl.impl_trait.id;
142    let (self_ty, partial_trait_ref) = trait_impl.impl_trait.split_self();
143    let self_ty = self_ty.as_ref()?;
144
145    let mut candidate = vec!["impl".to_owned()];
146    candidate.push(item_to_ident(item_names, trait_id.into())?);
147    candidate.extend(args_to_idents(item_names, &partial_trait_ref.generics));
148    candidate.push("for".to_owned());
149    candidate.push(if let TyKind::TypeVar(_) = self_ty.kind() {
150        "T".to_string()
151    } else {
152        ty_to_idents(item_names, self_ty)?
153    });
154    if let TyKind::Adt(tref) = self_ty.kind() {
155        candidate.extend(args_to_idents(item_names, &tref.generics));
156    };
157    Some(candidate.join("_"))
158}
charon_lib/transform/add_missing_info/compute_short_names.rs

charon_lib/transform/add_missing_info/
compute_short_names.rs
