charon_lib/transform/simplify_output/
lift_associated_item_clauses.rs

1//! Move clauses on non-generic associated types to be implied clauses of the trait. The
2//! distinction is not semantically meaningful.
3use std::mem;
4
5use crate::{
6    ast::*,
7    ids::{IndexMap, IndexVec},
8};
9
10use crate::transform::{TransformCtx, ctx::TransformPass};
11
12pub struct Transform;
13impl TransformPass for Transform {
14    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
15        !options.no_normalize
16    }
17    fn transform_ctx(&self, ctx: &mut TransformCtx) {
18        // For each trait, we move the item-local clauses to be top-level parent clauses, and
19        // record the mapping from the old to the new ids.
20        let trait_item_clause_ids: IndexMap<
21            TraitDeclId,
22            IndexMap<AssocTypeId, IndexVec<TraitClauseId, TraitClauseId>>,
23        > = ctx.translated.trait_decls.map_ref_mut(|decl| {
24            let mut map = IndexMap::default();
25            for (type_id, assoc_ty) in decl
26                .types
27                .iter_mut_enumerated()
28                .filter(|(_, assoc_ty)| !assoc_ty.params.has_explicits())
29            {
30                let id_map = mem::take(&mut assoc_ty.skip_binder.implied_clauses).map(|clause| {
31                    let mut clause = clause.move_from_under_binder().unwrap();
32                    decl.implied_clauses.push_with(|id| {
33                        clause.clause_id = id;
34                        clause
35                    })
36                });
37                if assoc_ty.params.trait_clauses.is_empty() {
38                    // Move non-trait-clause-predicates of non-GAT types to be predicates on
39                    // the trait itself.
40                    decl.generics.take_predicates_from(
41                        mem::take(&mut assoc_ty.params)
42                            .move_from_under_binder()
43                            .unwrap(),
44                    );
45                }
46                map.set_slot_extend(type_id, id_map);
47            }
48            map
49        });
50
51        // Move the item-local trait refs to match what we did in the trait declarations.
52        for timpl in ctx.translated.trait_impls.iter_mut() {
53            for assoc_ty in timpl.types.iter_mut() {
54                if !assoc_ty.params.has_explicits() {
55                    for trait_ref in mem::take(&mut assoc_ty.skip_binder.implied_trait_refs) {
56                        let trait_ref = trait_ref.move_from_under_binder().unwrap();
57                        // Note: this assumes that we listed the types in the same order as in the
58                        // trait decl, which we do.
59                        timpl.implied_trait_refs.push(trait_ref);
60                    }
61                }
62            }
63        }
64
65        // Update trait refs.
66        ctx.translated.dyn_visit_mut(|trkind: &mut TraitRefKind| {
67            use TraitRefKind::*;
68            match trkind {
69                ItemClause(..) => take_mut::take(trkind, |trkind| {
70                    let ItemClause(tref, type_id, item_clause_id) = trkind else {
71                        unreachable!()
72                    };
73                    let new_id = (|| {
74                        let new_id = *trait_item_clause_ids
75                            .get(tref.trait_decl_ref.skip_binder.id)?
76                            .get(type_id)?
77                            .get(item_clause_id)?;
78                        Some(new_id)
79                    })();
80                    match new_id {
81                        Some(new_id) => ParentClause(tref, new_id),
82                        None => ItemClause(tref, type_id, item_clause_id),
83                    }
84                }),
85                BuiltinOrAuto {
86                    parent_trait_refs,
87                    types,
88                    ..
89                } => {
90                    for assoc_ty in types.iter_mut() {
91                        for tref in std::mem::take(&mut assoc_ty.implied_trait_refs) {
92                            // Note: this assumes that we listed the types in the same order as in
93                            // the trait decl, which we do.
94                            parent_trait_refs.push(tref);
95                        }
96                    }
97                }
98                _ => {}
99            }
100        });
101    }
102}
charon_lib/transform/simplify_output/lift_associated_item_clauses.rs

charon_lib/transform/simplify_output/
lift_associated_item_clauses.rs
