charon_driver/translate/
translate_traits.rs

1use super::translate_ctx::*;
2use charon_lib::ast::*;
3use charon_lib::formatter::IntoFormatter;
4use charon_lib::meta::ItemMeta;
5use charon_lib::pretty::FmtWithCtx;
6use charon_lib::ullbc_ast as ast;
7use hax_frontend_exporter as hax;
8use indexmap::IndexMap;
9use itertools::Itertools;
10use std::mem;
11use std::sync::Arc;
12
13/// The context in which we are translating a clause, used to generate the appropriate ids and
14/// trait references.
15pub(crate) enum PredicateLocation {
16    /// We're translating the parent clauses of this trait.
17    Parent,
18    /// We're translating the item clauses of this trait.
19    Item(TraitItemName),
20    /// We're translating anything else.
21    Base,
22}
23
24impl<'tcx, 'ctx> TranslateCtx<'tcx> {
25    /// Remark: this **doesn't** register the def id (on purpose)
26    pub(crate) fn translate_trait_item_name(
27        &mut self,
28        def_id: &hax::DefId,
29    ) -> Result<TraitItemName, Error> {
30        // Translate the name
31        let name = self.hax_def_id_to_name(def_id)?;
32        let (name, id) = name.name.last().unwrap().as_ident().unwrap();
33        assert!(id.is_zero());
34        Ok(TraitItemName(name.to_string()))
35    }
36}
37
38impl ItemTransCtx<'_, '_> {
39    #[tracing::instrument(skip(self, item_meta))]
40    pub fn translate_trait_decl(
41        mut self,
42        def_id: TraitDeclId,
43        item_meta: ItemMeta,
44        def: &hax::FullDef,
45    ) -> Result<TraitDecl, Error> {
46        trace!("About to translate trait decl:\n{:?}", def.def_id);
47        trace!("Trait decl id:\n{:?}", def_id);
48
49        let span = item_meta.span;
50
51        if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
52            raise_error!(self, span, "Trait aliases are not supported");
53        }
54
55        let hax::FullDefKind::Trait { items, .. } = &def.kind else {
56            raise_error!(self, span, "Unexpected definition: {def:?}");
57        };
58        let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
59            .iter()
60            .map(|(item, def)| {
61                let name = TraitItemName(item.name.clone());
62                (name, item, def.clone())
63            })
64            .collect_vec();
65
66        // Translate the generics
67        // Note that in the generics returned by [translate_def_generics], the trait refs only
68        // contain the local trait clauses. The parent clauses are stored in
69        // `self.parent_trait_clauses`.
70        self.translate_def_generics(span, def)?;
71
72        // Translate the associated items
73        // We do something subtle here: TODO: explain
74        let mut consts = Vec::new();
75        let mut const_defaults = IndexMap::new();
76        let mut types = Vec::new();
77        let mut type_clauses = Vec::new();
78        let mut type_defaults = IndexMap::new();
79        let mut methods = Vec::new();
80        for (item_name, hax_item, hax_def) in &items {
81            let item_def_id = &hax_item.def_id;
82            let item_span = self.def_span(item_def_id);
83            match &hax_def.kind {
84                hax::FullDefKind::AssocFn { .. } => {
85                    let fun_def = self.t_ctx.hax_def(item_def_id)?;
86                    let binder_kind = BinderKind::TraitMethod(def_id, item_name.clone());
87                    let fn_ref = self.translate_binder_for_def(
88                        item_span,
89                        binder_kind,
90                        &fun_def,
91                        |bt_ctx| {
92                            // If the trait is opaque, we only translate the signature of a method
93                            // with default body if it's overridden or used somewhere else.
94                            // We insert the `Binder<FunDeclRef>` unconditionally here, and remove
95                            // the ones that correspond to untranslated functions in the
96                            // `remove_unused_methods` pass.
97                            // FIXME: this triggers the translation of traits used in the method
98                            // clauses, despite the fact that we may end up not needing them.
99                            let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
100                                || item_meta.opacity.is_transparent()
101                                || !hax_item.has_value
102                            {
103                                bt_ctx.register_fun_decl_id(item_span, item_def_id)
104                            } else {
105                                bt_ctx.register_fun_decl_id_no_enqueue(item_span, item_def_id)
106                            };
107
108                            // TODO: there's probably a cleaner way to write this
109                            assert_eq!(bt_ctx.binding_levels.len(), 2);
110                            let fun_generics = bt_ctx
111                                .outermost_binder()
112                                .params
113                                .identity_args_at_depth(
114                                    GenericsSource::item(def_id),
115                                    DeBruijnId::one(),
116                                )
117                                .concat(
118                                    GenericsSource::item(fun_id),
119                                    &bt_ctx.innermost_binder().params.identity_args_at_depth(
120                                        GenericsSource::Method(def_id.into(), item_name.clone()),
121                                        DeBruijnId::zero(),
122                                    ),
123                                );
124                            Ok(FunDeclRef {
125                                id: fun_id,
126                                generics: Box::new(fun_generics),
127                            })
128                        },
129                    )?;
130                    methods.push((item_name.clone(), fn_ref));
131                }
132                hax::FullDefKind::AssocConst { ty, .. } => {
133                    // Check if the constant has a value (i.e., a body).
134                    if hax_item.has_value {
135                        // The parameters of the constant are the same as those of the item that
136                        // declares them.
137                        let id = self.register_global_decl_id(item_span, item_def_id);
138                        let generics_target = GenericsSource::item(id);
139                        let gref = GlobalDeclRef {
140                            id,
141                            generics: Box::new(
142                                self.the_only_binder().params.identity_args(generics_target),
143                            ),
144                        };
145                        const_defaults.insert(item_name.clone(), gref);
146                    };
147                    let ty = self.translate_ty(item_span, ty)?;
148                    consts.push((item_name.clone(), ty));
149                }
150                hax::FullDefKind::AssocTy { param_env, .. }
151                    if !param_env.generics.params.is_empty() =>
152                {
153                    raise_error!(
154                        self,
155                        item_span,
156                        "Generic associated types are not supported"
157                    );
158                }
159                hax::FullDefKind::AssocTy { value, .. } => {
160                    // TODO: handle generics (i.e. GATs).
161                    if let Some(clauses) = self.item_trait_clauses.get(item_name) {
162                        type_clauses.push((item_name.clone(), clauses.clone()));
163                    }
164                    if let Some(ty) = value {
165                        let ty = self.translate_ty(item_span, &ty)?;
166                        type_defaults.insert(item_name.clone(), ty);
167                    };
168                    types.push(item_name.clone());
169                }
170                _ => panic!("Unexpected definition for trait item: {hax_def:?}"),
171            }
172        }
173
174        // In case of a trait implementation, some values may not have been
175        // provided, in case the declaration provided default values. We
176        // check those, and lookup the relevant values.
177        Ok(ast::TraitDecl {
178            def_id,
179            item_meta,
180            parent_clauses: mem::take(&mut self.parent_trait_clauses),
181            generics: self.into_generics(),
182            type_clauses,
183            consts,
184            const_defaults,
185            types,
186            type_defaults,
187            methods,
188        })
189    }
190
191    #[tracing::instrument(skip(self, item_meta))]
192    pub fn translate_trait_impl(
193        mut self,
194        def_id: TraitImplId,
195        item_meta: ItemMeta,
196        def: &hax::FullDef,
197    ) -> Result<TraitImpl, Error> {
198        trace!("About to translate trait impl:\n{:?}", def.def_id);
199        trace!("Trait impl id:\n{:?}", def_id);
200
201        let span = item_meta.span;
202
203        self.translate_def_generics(span, def)?;
204
205        let hax::FullDefKind::TraitImpl {
206            trait_pred,
207            implied_impl_exprs,
208            items: impl_items,
209            ..
210        } = &def.kind
211        else {
212            unreachable!()
213        };
214
215        // Retrieve the information about the implemented trait.
216        let implemented_trait_id = &trait_pred.trait_ref.def_id;
217        let trait_id = self.register_trait_decl_id(span, implemented_trait_id);
218        let implemented_trait = {
219            let implemented_trait = &trait_pred.trait_ref;
220            let generics = self.translate_generic_args(
221                span,
222                &implemented_trait.generic_args,
223                &[],
224                None,
225                GenericsSource::item(trait_id),
226            )?;
227            TraitDeclRef {
228                trait_id,
229                generics: Box::new(generics),
230            }
231        };
232
233        // The trait refs which implement the parent clauses of the implemented trait decl.
234        let parent_trait_refs = self.translate_trait_impl_exprs(span, &implied_impl_exprs)?;
235
236        {
237            // Debugging
238            let ctx = self.into_fmt();
239            let refs = parent_trait_refs
240                .iter()
241                .map(|c| c.fmt_with_ctx(&ctx))
242                .collect::<Vec<String>>()
243                .join("\n");
244            trace!(
245                "Trait impl: {:?}\n- parent_trait_refs:\n{}",
246                def.def_id,
247                refs
248            );
249        }
250
251        // Explore the associated items
252        let mut consts = Vec::new();
253        let mut types: Vec<(TraitItemName, Ty)> = Vec::new();
254        let mut methods = Vec::new();
255        let mut type_clauses = Vec::new();
256
257        for impl_item in impl_items {
258            use hax::ImplAssocItemValue::*;
259            let name = TraitItemName(impl_item.name.clone());
260            let item_def = impl_item.def(); // The impl item or the corresponding trait default.
261            let item_span = self.def_span(&item_def.def_id);
262            let item_def_id = &item_def.def_id;
263            match item_def.kind() {
264                hax::FullDefKind::AssocFn { .. } => {
265                    match &impl_item.value {
266                        Provided { is_override, .. } => {
267                            let fun_def = self.t_ctx.hax_def(item_def_id)?;
268                            let binder_kind = BinderKind::TraitMethod(trait_id, name.clone());
269                            let fn_ref = self.translate_binder_for_def(
270                                item_span,
271                                binder_kind,
272                                &fun_def,
273                                |bt_ctx| {
274                                    // If the impl is opaque, we only translate the signature of a
275                                    // method with a default body if it's directly used somewhere
276                                    // else.
277                                    // We insert the `Binder<FunDeclRef>` unconditionally here, and
278                                    // remove the ones that correspond to untranslated functions in
279                                    // the `remove_unused_methods` pass.
280                                    let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
281                                        || item_meta.opacity.is_transparent()
282                                        || !*is_override
283                                    {
284                                        bt_ctx.register_fun_decl_id(item_span, item_def_id)
285                                    } else {
286                                        bt_ctx
287                                            .register_fun_decl_id_no_enqueue(item_span, item_def_id)
288                                    };
289
290                                    // TODO: there's probably a cleaner way to write this
291                                    assert_eq!(bt_ctx.binding_levels.len(), 2);
292                                    let fun_generics = bt_ctx
293                                        .outermost_binder()
294                                        .params
295                                        .identity_args_at_depth(
296                                            GenericsSource::item(def_id),
297                                            DeBruijnId::one(),
298                                        )
299                                        .concat(
300                                            GenericsSource::item(fun_id),
301                                            &bt_ctx
302                                                .innermost_binder()
303                                                .params
304                                                .identity_args_at_depth(
305                                                    GenericsSource::Method(
306                                                        trait_id.into(),
307                                                        name.clone(),
308                                                    ),
309                                                    DeBruijnId::zero(),
310                                                ),
311                                        );
312                                    Ok(FunDeclRef {
313                                        id: fun_id,
314                                        generics: Box::new(fun_generics),
315                                    })
316                                },
317                            )?;
318                            methods.push((name, fn_ref));
319                        }
320                        DefaultedFn { .. } => {
321                            // TODO: handle defaulted methods
322                        }
323                        _ => unreachable!(),
324                    }
325                }
326                hax::FullDefKind::AssocConst { .. } => {
327                    let id = self.register_global_decl_id(item_span, item_def_id);
328                    let generics_target = GenericsSource::item(id);
329                    // The parameters of the constant are the same as those of the item that
330                    // declares them.
331                    let generics = match &impl_item.value {
332                        Provided { .. } => {
333                            self.the_only_binder().params.identity_args(generics_target)
334                        }
335                        _ => implemented_trait
336                            .generics
337                            .clone()
338                            .with_target(generics_target),
339                    };
340                    let gref = GlobalDeclRef {
341                        id,
342                        generics: Box::new(generics),
343                    };
344                    consts.push((name, gref));
345                }
346                hax::FullDefKind::AssocTy { param_env, .. }
347                    if !param_env.generics.params.is_empty() =>
348                {
349                    // We don't support GATs; the error was already reported in the trait declaration.
350                }
351                hax::FullDefKind::AssocTy { value, .. } => {
352                    let ty = match &impl_item.value {
353                        Provided { .. } => value.as_ref().unwrap(),
354                        DefaultedTy { ty, .. } => ty,
355                        _ => unreachable!(),
356                    };
357                    let ty = self.translate_ty(item_span, &ty)?;
358                    types.push((name.clone(), ty));
359
360                    let trait_refs =
361                        self.translate_trait_impl_exprs(item_span, &impl_item.required_impl_exprs)?;
362                    type_clauses.push((name, trait_refs));
363                }
364                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
365            }
366        }
367
368        Ok(ast::TraitImpl {
369            def_id,
370            item_meta,
371            impl_trait: implemented_trait,
372            generics: self.into_generics(),
373            parent_trait_refs,
374            type_clauses,
375            consts,
376            types,
377            methods,
378        })
379    }
380}
charon_driver/translate/translate_traits.rs

charon_driver/translate/
translate_traits.rs
