charon_lib/transform/normalize/
normalize_trait_refs.rs

1use crate::{
2    ast::*,
3    ids::{IndexMap, IndexVec},
4    transform::{TransformCtx, ctx::TransformPass},
5};
6
7const MAX_NORMALIZATION_STEPS: usize = 100;
8
9#[derive(Visitor)]
10struct NormalizeTraitRefs<'a> {
11    impl_parent_refs: &'a IndexMap<TraitImplId, IndexVec<TraitClauseId, TraitRef>>,
12    /// Charon can end up with self-referential clauses, see e.g.
13    /// `issue-1078-default-assoc-ty-self-ref-clause.rs`. Therefore we simply give up normalizing
14    /// after a number of steps.
15    steps: usize,
16}
17
18impl VisitAstMut for NormalizeTraitRefs<'_> {
19    fn exit_trait_ref(&mut self, tref: &mut TraitRef) {
20        if self.steps >= MAX_NORMALIZATION_STEPS {
21            return;
22        }
23        if let TraitRefKind::ParentClause(parent, clause_id) = &tref.kind {
24            *tref = match &parent.kind {
25                TraitRefKind::TraitImpl(impl_ref) => {
26                    let Some(proof) = self.impl_parent_refs.get(impl_ref.id) else {
27                        return;
28                    };
29                    let mut proof = ItemBinder::new(impl_ref.id, proof[*clause_id].clone())
30                        .substitute(ItemBinder::new(CurrentItem, &impl_ref.generics))
31                        .under_current_binder();
32                    if *tref == proof {
33                        return;
34                    }
35                    // Recursively normalize.
36                    self.steps += 1;
37                    self.visit(&mut proof);
38                    proof
39                }
40                TraitRefKind::BuiltinOrAuto {
41                    parent_trait_refs, ..
42                } => {
43                    let Some(proof) = parent_trait_refs.get(*clause_id) else {
44                        return;
45                    };
46                    proof.clone()
47                }
48                _ => return,
49            };
50        }
51    }
52}
53
54pub struct Transform;
55impl TransformPass for Transform {
56    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
57        !options.no_normalize
58    }
59
60    fn transform_ctx(&self, ctx: &mut TransformCtx) {
61        // Items are temporarily removed from the crate while we mutate them, so keep the original
62        // impl proofs separately.
63        let impl_parent_refs = ctx
64            .translated
65            .trait_impls
66            .map_ref(|timpl| timpl.implied_trait_refs.clone());
67        ctx.for_each_item_mut(|_, mut item| {
68            let _ = item.drive_mut(&mut NormalizeTraitRefs {
69                impl_parent_refs: &impl_parent_refs,
70                steps: 0,
71            });
72        });
73    }
74}
charon_lib/transform/normalize/normalize_trait_refs.rs

charon_lib/transform/normalize/
normalize_trait_refs.rs
