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                // Try to move them all out of the binder, or bail.
31                if let Some(clauses) = assoc_ty
32                    .skip_binder
33                    .clone()
34                    .implied_clauses
35                    .move_from_under_binder()
36                {
37                    assoc_ty.skip_binder.implied_clauses.clear();
38                    let id_map = clauses.map(|mut clause| {
39                        decl.implied_clauses.push_with(|id| {
40                            clause.clause_id = id;
41                            clause
42                        })
43                    });
44                    if assoc_ty.params.trait_clauses.is_empty() {
45                        // Move non-trait-clause-predicates of non-GAT types to be predicates on
46                        // the trait itself.
47                        decl.generics.take_predicates_from(
48                            mem::take(&mut assoc_ty.params)
49                                .move_from_under_binder()
50                                .unwrap(),
51                        );
52                    }
53                    map.set_slot_extend(type_id, id_map);
54                }
55            }
56            map
57        });
58
59        // Move the item-local trait refs to match what we did in the trait declarations.
60        for timpl in ctx.translated.trait_impls.iter_mut() {
61            for (type_id, assoc_ty) in timpl.types.iter_mut_indexed() {
62                if let Some(m) = trait_item_clause_ids.get(timpl.impl_trait.id)
63                    && m.get(type_id).is_some()
64                {
65                    for trait_ref in mem::take(&mut assoc_ty.skip_binder.implied_trait_refs) {
66                        let trait_ref = trait_ref.move_from_under_binder().unwrap();
67                        // Note: this assumes that we listed the types in the same order as in the
68                        // trait decl, which we do.
69                        timpl.implied_trait_refs.push(trait_ref);
70                    }
71                }
72            }
73        }
74
75        // Update trait refs.
76        ctx.translated.dyn_visit_mut(|trkind: &mut TraitRefKind| {
77            use TraitRefKind::*;
78            match trkind {
79                ItemClause { .. } => take_mut::take(trkind, |trkind| {
80                    let ItemClause {
81                        trait_ref,
82                        type_id,
83                        generics,
84                        clause_id,
85                        clause_args,
86                    } = trkind
87                    else {
88                        unreachable!()
89                    };
90                    let new_id = (|| {
91                        let new_id = *trait_item_clause_ids
92                            .get(trait_ref.trait_decl_ref.id)?
93                            .get(type_id)?
94                            .get(clause_id)?;
95                        Some(new_id)
96                    })();
97                    match new_id {
98                        Some(new_id) => ParentClause(trait_ref, new_id, clause_args),
99                        None => ItemClause {
100                            trait_ref,
101                            type_id,
102                            generics,
103                            clause_id,
104                            clause_args,
105                        },
106                    }
107                }),
108                BuiltinOrAuto {
109                    parent_trait_refs,
110                    types,
111                    ..
112                } => {
113                    for assoc_ty in types.iter_mut() {
114                        for tref in std::mem::take(&mut assoc_ty.implied_trait_refs) {
115                            // Note: this assumes that we listed the types in the same order as in
116                            // the trait decl, which we do. And that builtin assoc types are never
117                            // GATs, which they so far aren't.
118                            parent_trait_refs.push(tref);
119                        }
120                    }
121                }
122                _ => {}
123            }
124        });
125    }
126}
charon_lib/transform/simplify_output/lift_associated_item_clauses.rs

charon_lib/transform/simplify_output/
lift_associated_item_clauses.rs
