charon_driver/translate/
translate_items.rs

1use super::translate_crate::*;
2use super::translate_ctx::*;
3use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
4use charon_lib::ast::*;
5use charon_lib::formatter::IntoFormatter;
6use charon_lib::pretty::FmtWithCtx;
7use derive_generic_visitor::Visitor;
8use itertools::Itertools;
9use rustc_span::sym;
10use std::mem;
11use std::ops::ControlFlow;
12
13impl<'tcx, 'ctx> TranslateCtx<'tcx> {
14    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
15        let trans_id = self.register_no_enqueue(&None, item_src);
16        let def_id = item_src.def_id();
17        if let Some(trans_id) = trans_id {
18            if self.translate_stack.contains(&trans_id) {
19                register_error!(
20                    self,
21                    Span::dummy(),
22                    "Cycle detected while translating {def_id:?}! Stack: {:?}",
23                    &self.translate_stack
24                );
25                return;
26            } else {
27                self.translate_stack.push(trans_id);
28            }
29        }
30        self.with_def_id(def_id, trans_id, |mut ctx| {
31            let span = ctx.def_span(def_id);
32            // Catch cycles
33            let res = {
34                // Stopgap measure because there are still many panics in charon and hax.
35                let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
36                std::panic::catch_unwind(move || ctx.translate_item_aux(item_src, trans_id))
37            };
38            match res {
39                Ok(Ok(())) => return,
40                // Translation error
41                Ok(Err(_)) => {
42                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
43                }
44                // Panic
45                Err(_) => register_error!(
46                    ctx,
47                    span,
48                    "Thread panicked when extracting item `{def_id:?}`."
49                ),
50            };
51        });
52        // We must be careful not to early-return from this function to not unbalance the stack.
53        self.translate_stack.pop();
54    }
55
56    pub(crate) fn translate_item_aux(
57        &mut self,
58        item_src: &TransItemSource,
59        trans_id: Option<ItemId>,
60    ) -> Result<(), Error> {
61        // Translate the meta information
62        let name = self.translate_name(item_src)?;
63        if let Some(trans_id) = trans_id {
64            self.translated.item_names.insert(trans_id, name.clone());
65        }
66        let opacity = self.opacity_for_name(&name);
67        if opacity.is_invisible() {
68            // Don't even start translating the item. In particular don't call `hax_def` on it.
69            return Ok(());
70        }
71        let def = self.hax_def_for_item(&item_src.item)?;
72        let item_meta = self.translate_item_meta(&def, item_src, name, opacity);
73        if item_meta.opacity.is_invisible() {
74            return Ok(());
75        }
76
77        // Initialize the item translation context
78        let mut bt_ctx = ItemTransCtx::new(item_src.clone(), trans_id, self);
79        trace!(
80            "About to translate item `{:?}` as a {:?}; \
81            target_id={trans_id:?}, mono={}",
82            def.def_id(),
83            item_src.kind,
84            bt_ctx.monomorphize()
85        );
86        if !matches!(
87            &item_src.kind,
88            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module,
89        ) {
90            bt_ctx.translate_item_generics(item_meta.span, &def, &item_src.kind)?;
91        }
92        match &item_src.kind {
93            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module => {
94                bt_ctx.register_module(item_meta, &def);
95            }
96            TransItemSourceKind::Type => {
97                let Some(ItemId::Type(id)) = trans_id else {
98                    unreachable!()
99                };
100                let ty = bt_ctx.translate_type_decl(id, item_meta, &def)?;
101                self.translated.type_decls.set_slot(id, ty);
102            }
103            TransItemSourceKind::Fun => {
104                let Some(ItemId::Fun(id)) = trans_id else {
105                    unreachable!()
106                };
107                let fun_decl = bt_ctx.translate_fun_decl(id, item_meta, &def)?;
108                self.translated.fun_decls.set_slot(id, fun_decl);
109            }
110            TransItemSourceKind::Global => {
111                let Some(ItemId::Global(id)) = trans_id else {
112                    unreachable!()
113                };
114                let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
115                self.translated.global_decls.set_slot(id, global_decl);
116            }
117            TransItemSourceKind::TraitDecl => {
118                let Some(ItemId::TraitDecl(id)) = trans_id else {
119                    unreachable!()
120                };
121                let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
122                self.translated.trait_decls.set_slot(id, trait_decl);
123            }
124            TransItemSourceKind::TraitImpl(kind) => {
125                let Some(ItemId::TraitImpl(id)) = trans_id else {
126                    unreachable!()
127                };
128                let trait_impl = match kind {
129                    TraitImplSource::Normal => bt_ctx.translate_trait_impl(id, item_meta, &def)?,
130                    TraitImplSource::TraitAlias => {
131                        bt_ctx.translate_trait_alias_blanket_impl(id, item_meta, &def)?
132                    }
133                    &TraitImplSource::Closure(kind) => {
134                        bt_ctx.translate_closure_trait_impl(id, item_meta, &def, kind)?
135                    }
136                    TraitImplSource::ImplicitDestruct => {
137                        bt_ctx.translate_implicit_destruct_impl(id, item_meta, &def)?
138                    }
139                };
140                self.translated.trait_impls.set_slot(id, trait_impl);
141            }
142            &TransItemSourceKind::DefaultedMethod(impl_kind, name) => {
143                let Some(ItemId::Fun(id)) = trans_id else {
144                    unreachable!()
145                };
146                let fun_decl =
147                    bt_ctx.translate_defaulted_method(id, item_meta, &def, impl_kind, name)?;
148                self.translated.fun_decls.set_slot(id, fun_decl);
149            }
150            &TransItemSourceKind::ClosureMethod(kind) => {
151                let Some(ItemId::Fun(id)) = trans_id else {
152                    unreachable!()
153                };
154                let fun_decl = bt_ctx.translate_closure_method(id, item_meta, &def, kind)?;
155                self.translated.fun_decls.set_slot(id, fun_decl);
156            }
157            TransItemSourceKind::ClosureAsFnCast => {
158                let Some(ItemId::Fun(id)) = trans_id else {
159                    unreachable!()
160                };
161                let fun_decl = bt_ctx.translate_stateless_closure_as_fn(id, item_meta, &def)?;
162                self.translated.fun_decls.set_slot(id, fun_decl);
163            }
164            &TransItemSourceKind::DropInPlaceMethod(impl_kind) => {
165                let Some(ItemId::Fun(id)) = trans_id else {
166                    unreachable!()
167                };
168                let fun_decl =
169                    bt_ctx.translate_drop_in_place_method(id, item_meta, &def, impl_kind)?;
170                self.translated.fun_decls.set_slot(id, fun_decl);
171            }
172            TransItemSourceKind::VTable => {
173                let Some(ItemId::Type(id)) = trans_id else {
174                    unreachable!()
175                };
176                let ty_decl = bt_ctx.translate_vtable_struct(id, item_meta, &def)?;
177                self.translated.type_decls.set_slot(id, ty_decl);
178            }
179            TransItemSourceKind::VTableInstance(impl_kind) => {
180                let Some(ItemId::Global(id)) = trans_id else {
181                    unreachable!()
182                };
183                let global_decl =
184                    bt_ctx.translate_vtable_instance(id, item_meta, &def, impl_kind)?;
185                self.translated.global_decls.set_slot(id, global_decl);
186            }
187            TransItemSourceKind::VTableInstanceInitializer(impl_kind) => {
188                let Some(ItemId::Fun(id)) = trans_id else {
189                    unreachable!()
190                };
191                let fun_decl =
192                    bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?;
193                self.translated.fun_decls.set_slot(id, fun_decl);
194            }
195            TransItemSourceKind::VTableMethod => {
196                let Some(ItemId::Fun(id)) = trans_id else {
197                    unreachable!()
198                };
199                let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
200                self.translated.fun_decls.set_slot(id, fun_decl);
201            }
202            TransItemSourceKind::VTableDropShim => {
203                let Some(ItemId::Fun(id)) = trans_id else {
204                    unreachable!()
205                };
206                let fun_decl = bt_ctx.translate_vtable_drop_shim(id, item_meta, &def)?;
207                self.translated.fun_decls.set_slot(id, fun_decl);
208            }
209        }
210        Ok(())
211    }
212
213    /// While translating an item you may need the contents of another. Use this to retreive the
214    /// translated version of this item. Use with care as this could create cycles.
215    pub(crate) fn get_or_translate(&mut self, id: ItemId) -> Result<krate::ItemRef<'_>, Error> {
216        // We have to call `get_item` a few times because we're running into the classic `Polonius`
217        // problem case.
218        if self.translated.get_item(id).is_none() {
219            let item_source = self.reverse_id_map.get(&id).unwrap().clone();
220            self.translate_item(&item_source);
221            if self.translated.get_item(id).is_none() {
222                let span = self.def_span(item_source.def_id());
223                let name = self
224                    .translated
225                    .item_name(id)
226                    .map(|n| n.to_string_with_ctx(&self.into_fmt()))
227                    .unwrap_or_else(|| id.to_string());
228                // Not a real error, its message won't be displayed.
229                return Err(Error {
230                    span,
231                    msg: format!("Failed to translate item {name}."),
232                });
233                // raise_error!(self, span, "Failed to translate item {name}.")
234            }
235            // Add to avoid the double translation of the same item
236            self.processed.insert(item_source.clone());
237        }
238        let item = self.translated.get_item(id);
239        Ok(item.unwrap())
240    }
241
242    /// Add a `const UNIT: () = ();` const, used as metadata for thin pointers/references.
243    pub fn translate_unit_metadata_const(&mut self) {
244        use charon_lib::ullbc_ast::*;
245        let name = Name::from_path(&["UNIT_METADATA"]);
246        let item_meta = ItemMeta {
247            name,
248            span: Span::dummy(),
249            source_text: None,
250            attr_info: AttrInfo::default(),
251            is_local: false,
252            opacity: ItemOpacity::Foreign,
253            lang_item: None,
254        };
255
256        let body = {
257            let mut builder = BodyBuilder::new(Span::dummy(), 0);
258            let _ = builder.new_var(None, Ty::mk_unit());
259            builder.build()
260        };
261
262        let global_id = self.translated.global_decls.reserve_slot();
263        let initializer = self.translated.fun_decls.push_with(|def_id| FunDecl {
264            def_id,
265            item_meta: item_meta.clone(),
266            src: ItemSource::TopLevel,
267            is_global_initializer: Some(global_id),
268            generics: Default::default(),
269            signature: FunSig {
270                is_unsafe: false,
271                inputs: vec![],
272                output: Ty::mk_unit(),
273            },
274            body: Body::Unstructured(body),
275        });
276        self.translated.global_decls.set_slot(
277            global_id,
278            GlobalDecl {
279                def_id: global_id,
280                item_meta,
281                generics: Default::default(),
282                ty: Ty::mk_unit(),
283                src: ItemSource::TopLevel,
284                global_kind: GlobalKind::NamedConst,
285                init: initializer,
286            },
287        );
288        self.translated.unit_metadata = Some(GlobalDeclRef {
289            id: global_id,
290            generics: Box::new(GenericArgs::empty()),
291        });
292    }
293
294    /// Keep only the methods we marked as "used".
295    pub fn remove_unused_methods(&mut self) {
296        let method_is_used = |trait_id, name| {
297            self.method_status.get(trait_id).is_some_and(|map| {
298                map.get(&name)
299                    .is_some_and(|status| matches!(status, MethodStatus::Used))
300            })
301        };
302        for tdecl in self.translated.trait_decls.iter_mut() {
303            tdecl
304                .methods
305                .retain(|m| method_is_used(tdecl.def_id, m.name()));
306        }
307        for timpl in self.translated.trait_impls.iter_mut() {
308            let trait_id = timpl.impl_trait.id;
309            timpl
310                .methods
311                .retain(|(name, _)| method_is_used(trait_id, *name));
312        }
313    }
314}
315
316impl ItemTransCtx<'_, '_> {
317    /// Register the items inside this module or inherent impl.
318    // TODO: we may want to accumulate the set of modules we found, to check that all
319    // the opaque modules given as arguments actually exist
320    #[tracing::instrument(skip(self, item_meta))]
321    pub(crate) fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef) {
322        if !item_meta.opacity.is_transparent() {
323            return;
324        }
325        match def.kind() {
326            hax::FullDefKind::InherentImpl { items, .. } => {
327                for assoc in items {
328                    self.t_ctx.enqueue_module_item(&assoc.def_id);
329                }
330            }
331            hax::FullDefKind::Mod { items, .. } => {
332                for (_, def_id) in items {
333                    self.t_ctx.enqueue_module_item(def_id);
334                }
335            }
336            hax::FullDefKind::ForeignMod { items, .. } => {
337                for def_id in items {
338                    self.t_ctx.enqueue_module_item(def_id);
339                }
340            }
341            _ => panic!("Item should be a module but isn't: {def:?}"),
342        }
343    }
344
345    pub(crate) fn get_item_source(
346        &mut self,
347        span: Span,
348        def: &hax::FullDef,
349    ) -> Result<ItemSource, Error> {
350        let assoc = match def.kind() {
351            hax::FullDefKind::AssocTy {
352                associated_item, ..
353            }
354            | hax::FullDefKind::AssocConst {
355                associated_item, ..
356            }
357            | hax::FullDefKind::AssocFn {
358                associated_item, ..
359            } => associated_item,
360            hax::FullDefKind::Closure { args, .. } => {
361                let info = self.translate_closure_info(span, args)?;
362                return Ok(ItemSource::Closure { info });
363            }
364            _ => return Ok(ItemSource::TopLevel),
365        };
366        Ok(match &assoc.container {
367            // E.g.:
368            // ```
369            // impl<T> List<T> {
370            //   fn new() -> Self { ... } <- inherent method
371            // }
372            // ```
373            hax::AssocItemContainer::InherentImplContainer { .. } => ItemSource::TopLevel,
374            // E.g.:
375            // ```
376            // impl Foo for Bar {
377            //   fn baz(...) { ... } // <- implementation of a trait method
378            // }
379            // ```
380            hax::AssocItemContainer::TraitImplContainer {
381                impl_,
382                implemented_trait_ref,
383                overrides_default,
384                ..
385            } => {
386                let impl_ref =
387                    self.translate_trait_impl_ref(span, impl_, TraitImplSource::Normal)?;
388                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
389                let item_name = self.t_ctx.translate_trait_item_name(def.def_id())?;
390                if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
391                    // If the implementation is getting translated, that means the method is
392                    // getting used.
393                    self.mark_method_as_used(trait_ref.id, item_name);
394                }
395                ItemSource::TraitImpl {
396                    impl_ref,
397                    trait_ref,
398                    item_name,
399                    reuses_default: !overrides_default,
400                }
401            }
402            // This method is the *declaration* of a trait item
403            // E.g.:
404            // ```
405            // trait Foo {
406            //   fn baz(...); // <- declaration of a trait method
407            // }
408            // ```
409            hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
410                // The trait id should be Some(...): trait markers (that we may eliminate)
411                // don't have associated items.
412                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
413                let item_name = self.t_ctx.translate_trait_item_name(def.def_id())?;
414                ItemSource::TraitDecl {
415                    trait_ref,
416                    item_name,
417                    has_default: assoc.has_value,
418                }
419            }
420        })
421    }
422
423    /// Translate a type definition.
424    ///
425    /// Note that we translate the types one by one: we don't need to take into
426    /// account the fact that some types are mutually recursive at this point
427    /// (we will need to take that into account when generating the code in a file).
428    #[tracing::instrument(skip(self, item_meta))]
429    pub fn translate_type_decl(
430        mut self,
431        trans_id: TypeDeclId,
432        item_meta: ItemMeta,
433        def: &hax::FullDef,
434    ) -> Result<TypeDecl, Error> {
435        let span = item_meta.span;
436
437        // Get the kind of the type decl -- is it a closure?
438        let src = self.get_item_source(span, def)?;
439
440        let mut repr: Option<ReprOptions> = None;
441
442        // Translate type body
443        let kind = match &def.kind {
444            _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
445            hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
446            hax::FullDefKind::TyAlias { ty, .. } => {
447                // Don't error on missing trait refs.
448                self.error_on_impl_expr_error = false;
449                self.translate_ty(span, ty).map(TypeDeclKind::Alias)
450            }
451            hax::FullDefKind::Adt { repr: hax_repr, .. } => {
452                repr = Some(self.translate_repr_options(hax_repr));
453                self.translate_adt_def(trans_id, span, &item_meta, def)
454            }
455            hax::FullDefKind::Closure { args, .. } => self.translate_closure_adt(span, &args),
456            _ => panic!("Unexpected item when translating types: {def:?}"),
457        };
458
459        let kind = match kind {
460            Ok(kind) => kind,
461            Err(err) => TypeDeclKind::Error(err.msg),
462        };
463        let layout = self.translate_layout(def.this());
464        let ptr_metadata = self.translate_ptr_metadata(span, def.this())?;
465        let type_def = TypeDecl {
466            def_id: trans_id,
467            item_meta,
468            generics: self.into_generics(),
469            kind,
470            src,
471            layout,
472            ptr_metadata,
473            repr,
474        };
475
476        Ok(type_def)
477    }
478
479    /// Translate one function.
480    #[tracing::instrument(skip(self, item_meta))]
481    pub fn translate_fun_decl(
482        mut self,
483        def_id: FunDeclId,
484        item_meta: ItemMeta,
485        def: &hax::FullDef,
486    ) -> Result<FunDecl, Error> {
487        let span = item_meta.span;
488
489        let src = self.get_item_source(span, def)?;
490
491        if let hax::FullDefKind::Ctor {
492            fields, output_ty, ..
493        } = def.kind()
494        {
495            let signature = FunSig {
496                inputs: fields
497                    .iter()
498                    .map(|field| self.translate_ty(span, &field.ty))
499                    .try_collect()?,
500                output: self.translate_ty(span, output_ty)?,
501                is_unsafe: false,
502            };
503
504            let body = if item_meta.opacity.with_private_contents().is_opaque() {
505                Body::Opaque
506            } else {
507                self.build_ctor_body(span, def)?
508            };
509            return Ok(FunDecl {
510                def_id,
511                item_meta,
512                generics: self.into_generics(),
513                signature,
514                src,
515                is_global_initializer: None,
516                body,
517            });
518        }
519
520        // Translate the function signature
521        trace!("Translating function signature");
522        let signature = match &def.kind {
523            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
524                self.translate_fun_sig(span, &sig.value)?
525            }
526            hax::FullDefKind::Const { ty, .. }
527            | hax::FullDefKind::AssocConst { ty, .. }
528            | hax::FullDefKind::Static { ty, .. } => FunSig {
529                inputs: vec![],
530                output: self.translate_ty(span, ty)?,
531                is_unsafe: false,
532            },
533            _ => panic!("Unexpected definition for function: {def:?}"),
534        };
535
536        // Check whether this function is a method declaration for a trait definition.
537        // If this is the case, it shouldn't contain a body.
538        let is_trait_method_decl_without_default = match &src {
539            ItemSource::TraitDecl { has_default, .. } => !has_default,
540            _ => false,
541        };
542
543        let is_global_initializer = matches!(
544            def.kind(),
545            hax::FullDefKind::Const { .. }
546                | hax::FullDefKind::AssocConst { .. }
547                | hax::FullDefKind::Static { .. }
548        );
549        let is_global_initializer = is_global_initializer
550            .then(|| self.register_item(span, def.this(), TransItemSourceKind::Global));
551
552        let body = if item_meta.opacity.with_private_contents().is_opaque() {
553            Body::Opaque
554        } else if is_trait_method_decl_without_default {
555            Body::TraitMethodWithoutDefault
556        } else {
557            // Translate the MIR body for this definition.
558            self.translate_def_body(item_meta.span, def)
559        };
560        Ok(FunDecl {
561            def_id,
562            item_meta,
563            generics: self.into_generics(),
564            signature,
565            src,
566            is_global_initializer,
567            body,
568        })
569    }
570
571    /// Translate one global.
572    #[tracing::instrument(skip(self, item_meta))]
573    pub fn translate_global(
574        mut self,
575        def_id: GlobalDeclId,
576        item_meta: ItemMeta,
577        def: &hax::FullDef,
578    ) -> Result<GlobalDecl, Error> {
579        let span = item_meta.span;
580
581        // Retrieve the kind
582        let item_source = self.get_item_source(span, def)?;
583
584        trace!("Translating global type");
585        let ty = match &def.kind {
586            hax::FullDefKind::Const { ty, .. }
587            | hax::FullDefKind::AssocConst { ty, .. }
588            | hax::FullDefKind::Static { ty, .. } => ty,
589            _ => panic!("Unexpected def for constant: {def:?}"),
590        };
591        let ty = self.translate_ty(span, ty)?;
592
593        let global_kind = match &def.kind {
594            hax::FullDefKind::Static { .. } => GlobalKind::Static,
595            hax::FullDefKind::Const {
596                kind: hax::ConstKind::TopLevel,
597                ..
598            }
599            | hax::FullDefKind::AssocConst { .. } => GlobalKind::NamedConst,
600            hax::FullDefKind::Const { .. } => GlobalKind::AnonConst,
601            _ => panic!("Unexpected def for constant: {def:?}"),
602        };
603
604        let initializer = self.register_item(span, def.this(), TransItemSourceKind::Fun);
605
606        Ok(GlobalDecl {
607            def_id,
608            item_meta,
609            generics: self.into_generics(),
610            ty,
611            src: item_source,
612            global_kind,
613            init: initializer,
614        })
615    }
616
617    #[tracing::instrument(skip(self, item_meta))]
618    pub fn translate_trait_decl(
619        mut self,
620        def_id: TraitDeclId,
621        item_meta: ItemMeta,
622        def: &hax::FullDef,
623    ) -> Result<TraitDecl, Error> {
624        let span = item_meta.span;
625
626        let (hax::FullDefKind::Trait {
627            implied_predicates, ..
628        }
629        | hax::FullDefKind::TraitAlias {
630            implied_predicates, ..
631        }) = def.kind()
632        else {
633            raise_error!(self, span, "Unexpected definition: {def:?}");
634        };
635
636        // Register implied predicates.
637        let mut preds =
638            self.translate_predicates(implied_predicates, PredicateOrigin::WhereClauseOnTrait)?;
639        let implied_clauses = mem::take(&mut preds.trait_clauses);
640        // Consider the other predicates as required since the distinction doesn't matter for
641        // non-trait-clauses.
642        self.innermost_generics_mut().take_predicates_from(preds);
643
644        let vtable = self.translate_vtable_struct_ref_no_enqueue(span, def.this())?;
645
646        if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
647            // Trait aliases don't have any items. Everything interesting is in the parent clauses.
648            return Ok(TraitDecl {
649                def_id,
650                item_meta,
651                implied_clauses,
652                generics: self.into_generics(),
653                consts: Default::default(),
654                types: Default::default(),
655                methods: Default::default(),
656                vtable,
657            });
658        }
659
660        let hax::FullDefKind::Trait {
661            items,
662            self_predicate,
663            ..
664        } = &def.kind
665        else {
666            unreachable!()
667        };
668        let self_trait_ref = TraitRef::new(
669            TraitRefKind::SelfId,
670            RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?),
671        );
672        let items: Vec<(TraitItemName, &hax::AssocItem)> = items
673            .iter()
674            .map(|item| -> Result<_, Error> {
675                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
676                Ok((name, item))
677            })
678            .try_collect()?;
679
680        // Translate the associated items
681        let mut consts = Vec::new();
682        let mut types = Vec::new();
683        let mut methods = Vec::new();
684
685        for &(item_name, ref hax_item) in &items {
686            let item_def_id = &hax_item.def_id;
687            let item_span = self.def_span(item_def_id);
688
689            // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
690            // polymorphic item as usual.
691            let trans_kind = match hax_item.kind {
692                hax::AssocKind::Fn { .. } => TransItemSourceKind::Fun,
693                hax::AssocKind::Const { .. } => TransItemSourceKind::Global,
694                hax::AssocKind::Type { .. } => TransItemSourceKind::Type,
695            };
696            let poly_item_def = self.poly_hax_def(item_def_id)?;
697            let (item_src, item_def) = if self.monomorphize() {
698                if poly_item_def.has_own_generics_or_predicates() {
699                    // Skip items that have generics of their own (as rustc defines these). This
700                    // skips GAT and generic methods. This does not skip methods with late-bound
701                    // lifetimes as these aren't considered generic arguments to the method itself
702                    // by rustc.
703                    continue;
704                } else {
705                    let item = def.this().with_def_id(self.hax_state(), item_def_id);
706                    let item_def = self.hax_def(&item)?;
707                    let item_src = TransItemSource::monomorphic(&item, trans_kind);
708                    (item_src, item_def)
709                }
710            } else {
711                let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
712                (item_src, poly_item_def)
713            };
714
715            match item_def.kind() {
716                hax::FullDefKind::AssocFn { .. } => {
717                    let method_id = self.register_no_enqueue(item_span, &item_src);
718                    // Register this method.
719                    self.register_method_impl(def_id, item_name, method_id);
720                    // By default we only enqueue required methods (those that don't have a default
721                    // impl). If the trait is transparent, we enqueue all its methods.
722                    if self.options.translate_all_methods
723                        || item_meta.opacity.is_transparent()
724                        || !hax_item.has_value
725                    {
726                        self.mark_method_as_used(def_id, item_name);
727                    }
728
729                    let binder_kind = BinderKind::TraitMethod(def_id, item_name);
730                    let mut method = self.translate_binder_for_def(
731                        item_span,
732                        binder_kind,
733                        &item_def,
734                        |bt_ctx| {
735                            assert_eq!(bt_ctx.binding_levels.len(), 2);
736                            let fun_generics = bt_ctx
737                                .outermost_binder()
738                                .params
739                                .identity_args_at_depth(DeBruijnId::one())
740                                .concat(
741                                    &bt_ctx
742                                        .innermost_binder()
743                                        .params
744                                        .identity_args_at_depth(DeBruijnId::zero()),
745                                );
746                            let fn_ref = FunDeclRef {
747                                id: method_id,
748                                generics: Box::new(fun_generics),
749                            };
750                            Ok(TraitMethod {
751                                name: item_name.clone(),
752                                item: fn_ref,
753                            })
754                        },
755                    )?;
756                    // In hax, associated items take an extra explicit `Self: Trait` clause, but we
757                    // don't want that to be part of the method clauses. Hence we remove the first
758                    // bound clause and replace its uses with references to the ambient `Self`
759                    // clause available in trait declarations.
760                    if !self.monomorphize() {
761                        struct ReplaceSelfVisitor;
762                        impl VarsVisitor for ReplaceSelfVisitor {
763                            fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<TraitRefKind> {
764                                if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
765                                    // Replace clause 0 and decrement the others.
766                                    Some(if let Some(new_id) = clause_id.index().checked_sub(1) {
767                                        TraitRefKind::Clause(DeBruijnVar::Bound(
768                                            DeBruijnId::ZERO,
769                                            TraitClauseId::new(new_id),
770                                        ))
771                                    } else {
772                                        TraitRefKind::SelfId
773                                    })
774                                } else {
775                                    None
776                                }
777                            }
778                        }
779                        method.params.visit_vars(&mut ReplaceSelfVisitor);
780                        method.skip_binder.visit_vars(&mut ReplaceSelfVisitor);
781                        method
782                            .params
783                            .trait_clauses
784                            .remove_and_shift_ids(TraitClauseId::ZERO);
785                        method.params.trait_clauses.iter_mut().for_each(|clause| {
786                            clause.clause_id -= 1;
787                        });
788                    }
789
790                    // We insert the `Binder<TraitMethod>` unconditionally here; we'll remove the
791                    // ones that correspond to unused methods at the end of translation.
792                    methods.push(method);
793                }
794                hax::FullDefKind::AssocConst { ty, .. } => {
795                    // Check if the constant has a value (i.e., a body).
796                    let default = hax_item.has_value.then(|| {
797                        // The parameters of the constant are the same as those of the item that
798                        // declares them.
799                        let id = self.register_and_enqueue(item_span, item_src);
800                        let mut generics = self.the_only_binder().params.identity_args();
801                        // We add an extra `Self: Trait` clause to default consts.
802                        if !self.monomorphize() {
803                            generics.trait_refs.push(self_trait_ref.clone());
804                        }
805                        GlobalDeclRef {
806                            id,
807                            generics: Box::new(generics),
808                        }
809                    });
810                    let ty = self.translate_ty(item_span, ty)?;
811                    consts.push(TraitAssocConst {
812                        name: item_name.clone(),
813                        ty,
814                        default,
815                    });
816                }
817                // Monomorphic traits need no associated types.
818                hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue,
819                hax::FullDefKind::AssocTy {
820                    value,
821                    implied_predicates,
822                    ..
823                } => {
824                    let binder_kind = BinderKind::TraitType(def_id, item_name.clone());
825                    let assoc_ty =
826                        self.translate_binder_for_def(item_span, binder_kind, &item_def, |ctx| {
827                            // Also add the implied predicates.
828                            let mut preds = ctx.translate_predicates(
829                                &implied_predicates,
830                                PredicateOrigin::TraitItem(item_name.clone()),
831                            )?;
832                            let implied_clauses = mem::take(&mut preds.trait_clauses);
833                            // Consider the other predicates as required since the distinction doesn't
834                            // matter for non-trait-clauses.
835                            ctx.innermost_generics_mut().take_predicates_from(preds);
836
837                            let default = value
838                                .as_ref()
839                                .map(|ty| ctx.translate_ty(item_span, ty))
840                                .transpose()?;
841                            Ok(TraitAssocTy {
842                                name: item_name.clone(),
843                                default,
844                                implied_clauses,
845                            })
846                        })?;
847                    types.push(assoc_ty);
848                }
849                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
850            }
851        }
852
853        if def.lang_item == Some(sym::destruct) {
854            // Add a `drop_in_place(*mut self)` method that contains the drop glue for this type.
855            let (method_name, method_binder) =
856                self.prepare_drop_in_place_method(def, span, def_id, None);
857            self.mark_method_as_used(def_id, method_name);
858            methods.push(method_binder.map(|fn_ref| TraitMethod {
859                name: method_name,
860                item: fn_ref,
861            }));
862        }
863
864        // In case of a trait implementation, some values may not have been
865        // provided, in case the declaration provided default values. We
866        // check those, and lookup the relevant values.
867        Ok(TraitDecl {
868            def_id,
869            item_meta,
870            implied_clauses,
871            generics: self.into_generics(),
872            consts,
873            types,
874            methods,
875            vtable,
876        })
877    }
878
879    #[tracing::instrument(skip(self, item_meta))]
880    pub fn translate_trait_impl(
881        mut self,
882        def_id: TraitImplId,
883        item_meta: ItemMeta,
884        def: &hax::FullDef,
885    ) -> Result<TraitImpl, Error> {
886        let span = item_meta.span;
887
888        let hax::FullDefKind::TraitImpl {
889            trait_pred,
890            implied_impl_exprs,
891            items: impl_items,
892            ..
893        } = &def.kind
894        else {
895            unreachable!()
896        };
897
898        // Retrieve the information about the implemented trait.
899        let implemented_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
900        let trait_id = implemented_trait.id;
901        // A `TraitRef` that points to this impl with the correct generics.
902        let self_predicate = TraitRef::new(
903            TraitRefKind::TraitImpl(TraitImplRef {
904                id: def_id,
905                generics: Box::new(self.the_only_binder().params.identity_args()),
906            }),
907            RegionBinder::empty(implemented_trait.clone()),
908        );
909
910        let vtable =
911            self.translate_vtable_instance_ref_no_enqueue(span, &trait_pred.trait_ref, def.this())?;
912
913        // The trait refs which implement the parent clauses of the implemented trait decl.
914        let implied_trait_refs = self.translate_trait_impl_exprs(span, &implied_impl_exprs)?;
915
916        {
917            // Debugging
918            let ctx = self.into_fmt();
919            let refs = implied_trait_refs
920                .iter()
921                .map(|c| c.with_ctx(&ctx))
922                .format("\n");
923            trace!(
924                "Trait impl: {:?}\n- implied_trait_refs:\n{}",
925                def.def_id(),
926                refs
927            );
928        }
929
930        // Explore the associated items
931        let mut consts = Vec::new();
932        let mut types = Vec::new();
933        let mut methods = Vec::new();
934
935        for impl_item in impl_items {
936            use hax::ImplAssocItemValue::*;
937            let name = self
938                .t_ctx
939                .translate_trait_item_name(&impl_item.decl_def_id)?;
940            let item_def_id = impl_item.def_id();
941            let item_span = self.def_span(item_def_id);
942            //
943            // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
944            // polymorphic item as usual.
945            let poly_item_def = self.poly_hax_def(item_def_id)?;
946            let trans_kind = match poly_item_def.kind() {
947                hax::FullDefKind::AssocFn { .. } => TransItemSourceKind::Fun,
948                hax::FullDefKind::AssocConst { .. } => TransItemSourceKind::Global,
949                hax::FullDefKind::AssocTy { .. } => TransItemSourceKind::Type,
950                _ => unreachable!(),
951            };
952            let (item_src, item_def) = if self.monomorphize() {
953                if poly_item_def.has_own_generics_or_predicates() {
954                    continue;
955                } else {
956                    let item = match &impl_item.value {
957                        // Real item: we reuse the impl arguments to get a reference to the item.
958                        Provided { def_id, .. } => def.this().with_def_id(self.hax_state(), def_id),
959                        // Defaulted item: we use the implemented trait arguments.
960                        _ => trait_pred
961                            .trait_ref
962                            .with_def_id(self.hax_state(), &impl_item.decl_def_id),
963                    };
964                    let item_src = TransItemSource::monomorphic(&item, trans_kind);
965                    let item_def = self.hax_def_for_item(&item_src.item)?;
966                    (item_src, item_def)
967                }
968            } else {
969                let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
970                (item_src, poly_item_def)
971            };
972
973            match item_def.kind() {
974                hax::FullDefKind::AssocFn { .. } => {
975                    let method_id: FunDeclId = {
976                        let method_src = match &impl_item.value {
977                            Provided { .. } => item_src,
978                            // This will generate a copy of the default method. Note that the base
979                            // item for `DefaultedMethod` is the trait impl.
980                            DefaultedFn { .. } => TransItemSource::from_item(
981                                def.this(),
982                                TransItemSourceKind::DefaultedMethod(TraitImplSource::Normal, name),
983                                self.monomorphize(),
984                            ),
985                            _ => unreachable!(),
986                        };
987                        self.register_no_enqueue(item_span, &method_src)
988                    };
989
990                    // Register this method.
991                    self.register_method_impl(trait_id, name, method_id);
992                    // By default we only enqueue required methods (those that don't have a default
993                    // impl). If the impl is transparent, we enqueue all the implemented methods.
994                    if matches!(impl_item.value, Provided { .. })
995                        && item_meta.opacity.is_transparent()
996                    {
997                        self.mark_method_as_used(trait_id, name);
998                    }
999
1000                    let binder_kind = BinderKind::TraitMethod(trait_id, name);
1001                    let bound_fn_ref = match &impl_item.value {
1002                        Provided { .. } => self.translate_binder_for_def(
1003                            item_span,
1004                            binder_kind,
1005                            &item_def,
1006                            |ctx| {
1007                                let generics = ctx
1008                                    .outermost_generics()
1009                                    .identity_args_at_depth(DeBruijnId::one())
1010                                    .concat(
1011                                        &ctx.innermost_generics()
1012                                            .identity_args_at_depth(DeBruijnId::zero()),
1013                                    );
1014                                Ok(FunDeclRef {
1015                                    id: method_id,
1016                                    generics: Box::new(generics),
1017                                })
1018                            },
1019                        )?,
1020                        DefaultedFn { .. } => {
1021                            // Retrieve the method generics from the trait decl.
1022                            let decl_methods =
1023                                match self.get_or_translate(implemented_trait.id.into()) {
1024                                    Ok(ItemRef::TraitDecl(tdecl)) => tdecl.methods.as_slice(),
1025                                    _ => &[],
1026                                };
1027                            let Some(bound_method) = decl_methods.iter().find(|m| m.name() == name)
1028                            else {
1029                                continue;
1030                            };
1031                            let method_params = bound_method
1032                                .clone()
1033                                .substitute_with_self(
1034                                    &implemented_trait.generics,
1035                                    &self_predicate.kind,
1036                                )
1037                                .params;
1038
1039                            let generics = self
1040                                .outermost_generics()
1041                                .identity_args_at_depth(DeBruijnId::one())
1042                                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
1043                            let fn_ref = FunDeclRef {
1044                                id: method_id,
1045                                generics: Box::new(generics),
1046                            };
1047                            Binder::new(binder_kind, method_params, fn_ref)
1048                        }
1049                        _ => unreachable!(),
1050                    };
1051
1052                    // We insert the `Binder<FunDeclRef>` unconditionally here; we'll remove the
1053                    // ones that correspond to unused methods at the end of translation.
1054                    methods.push((name, bound_fn_ref));
1055                }
1056                hax::FullDefKind::AssocConst { .. } => {
1057                    let id = self.register_and_enqueue(item_span, item_src);
1058                    // The parameters of the constant are the same as those of the item that
1059                    // declares them.
1060                    let generics = match &impl_item.value {
1061                        Provided { .. } => self.the_only_binder().params.identity_args(),
1062                        _ => {
1063                            let mut generics = implemented_trait.generics.as_ref().clone();
1064                            // For default consts, we add an extra `Self` predicate.
1065                            if !self.monomorphize() {
1066                                generics.trait_refs.push(self_predicate.clone());
1067                            }
1068                            generics
1069                        }
1070                    };
1071                    let gref = GlobalDeclRef {
1072                        id,
1073                        generics: Box::new(generics),
1074                    };
1075                    consts.push((name, gref));
1076                }
1077                // Monomorphic traits have no associated types.
1078                hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue,
1079                hax::FullDefKind::AssocTy { value, .. } => {
1080                    let binder_kind = BinderKind::TraitType(trait_id, name.clone());
1081                    let assoc_ty =
1082                        self.translate_binder_for_def(item_span, binder_kind, &item_def, |ctx| {
1083                            let ty = match &impl_item.value {
1084                                Provided { .. } => value.as_ref().unwrap(),
1085                                DefaultedTy { ty, .. } => ty,
1086                                _ => unreachable!(),
1087                            };
1088                            let ty = ctx.translate_ty(item_span, &ty)?;
1089                            let implied_trait_refs = ctx.translate_trait_impl_exprs(
1090                                item_span,
1091                                &impl_item.required_impl_exprs,
1092                            )?;
1093                            Ok(TraitAssocTyImpl {
1094                                value: ty,
1095                                implied_trait_refs,
1096                            })
1097                        })?;
1098                    types.push((name.clone(), assoc_ty));
1099                }
1100                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
1101            }
1102        }
1103
1104        let implemented_trait_def = self.poly_hax_def(&trait_pred.trait_ref.def_id)?;
1105        if implemented_trait_def.lang_item == Some(sym::destruct) {
1106            raise_error!(
1107                self,
1108                span,
1109                "found an explicit impl of `core::marker::Destruct`, this should not happen"
1110            );
1111        }
1112
1113        Ok(TraitImpl {
1114            def_id,
1115            item_meta,
1116            impl_trait: implemented_trait,
1117            generics: self.into_generics(),
1118            implied_trait_refs,
1119            consts,
1120            types,
1121            methods,
1122            vtable,
1123        })
1124    }
1125
1126    /// Generate a blanket impl for this trait, as in:
1127    /// ```
1128    ///     trait Alias<U> = Trait<Option<U>, Item = u32> + Clone;
1129    /// ```
1130    /// becomes:
1131    /// ```
1132    ///     trait Alias<U>: Trait<Option<U>, Item = u32> + Clone {}
1133    ///     impl<U, Self: Trait<Option<U>, Item = u32> + Clone> Alias<U> for Self {}
1134    /// ```
1135    #[tracing::instrument(skip(self, item_meta))]
1136    pub fn translate_trait_alias_blanket_impl(
1137        mut self,
1138        def_id: TraitImplId,
1139        item_meta: ItemMeta,
1140        def: &hax::FullDef,
1141    ) -> Result<TraitImpl, Error> {
1142        let span = item_meta.span;
1143
1144        let hax::FullDefKind::TraitAlias {
1145            implied_predicates, ..
1146        } = &def.kind
1147        else {
1148            raise_error!(self, span, "Unexpected definition: {def:?}");
1149        };
1150
1151        let trait_id = self.register_item(span, def.this(), TransItemSourceKind::TraitDecl);
1152
1153        // Register the trait implied clauses as required clauses for the impl.
1154        assert!(self.innermost_generics_mut().trait_clauses.is_empty());
1155        self.register_predicates(implied_predicates, PredicateOrigin::WhereClauseOnTrait)?;
1156
1157        let mut generics = self.the_only_binder().params.identity_args();
1158        // Do the inverse operation: the trait considers the clauses as implied.
1159        let implied_trait_refs = mem::take(&mut generics.trait_refs);
1160        let implemented_trait = TraitDeclRef {
1161            id: trait_id,
1162            generics: Box::new(generics),
1163        };
1164
1165        let mut timpl = TraitImpl {
1166            def_id,
1167            item_meta,
1168            impl_trait: implemented_trait,
1169            generics: self.the_only_binder().params.clone(),
1170            implied_trait_refs,
1171            consts: Default::default(),
1172            types: Default::default(),
1173            methods: Default::default(),
1174            // TODO(dyn)
1175            vtable: None,
1176        };
1177        // We got the predicates from a trait decl, so they may refer to the virtual `Self`
1178        // clause, which doesn't exist for impls. We fix that up here.
1179        {
1180            struct FixSelfVisitor {
1181                binder_depth: DeBruijnId,
1182            }
1183            struct UnhandledSelf;
1184            impl Visitor for FixSelfVisitor {
1185                type Break = UnhandledSelf;
1186            }
1187            impl VisitorWithBinderDepth for FixSelfVisitor {
1188                fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
1189                    &mut self.binder_depth
1190                }
1191            }
1192            impl VisitAstMut for FixSelfVisitor {
1193                fn visit<'a, T: AstVisitable>(&'a mut self, x: &mut T) -> ControlFlow<Self::Break> {
1194                    VisitWithBinderDepth::new(self).visit(x)
1195                }
1196                fn visit_trait_ref_kind(
1197                    &mut self,
1198                    kind: &mut TraitRefKind,
1199                ) -> ControlFlow<Self::Break> {
1200                    match kind {
1201                        TraitRefKind::SelfId => return ControlFlow::Break(UnhandledSelf),
1202                        TraitRefKind::ParentClause(sub, clause_id)
1203                            if matches!(sub.kind, TraitRefKind::SelfId) =>
1204                        {
1205                            *kind = TraitRefKind::Clause(DeBruijnVar::bound(
1206                                self.binder_depth,
1207                                *clause_id,
1208                            ))
1209                        }
1210                        _ => (),
1211                    }
1212                    self.visit_inner(kind)
1213                }
1214            }
1215            match timpl.drive_mut(&mut FixSelfVisitor {
1216                binder_depth: DeBruijnId::zero(),
1217            }) {
1218                ControlFlow::Continue(()) => {}
1219                ControlFlow::Break(UnhandledSelf) => {
1220                    register_error!(
1221                        self,
1222                        span,
1223                        "Found `Self` clause we can't handle \
1224                         in a trait alias blanket impl."
1225                    );
1226                }
1227            }
1228        };
1229
1230        Ok(timpl)
1231    }
1232
1233    /// Make a trait impl from a hax `VirtualTraitImpl`. Used for constructing fake trait impls for
1234    /// builtin types like `FnOnce`.
1235    #[tracing::instrument(skip(self, item_meta))]
1236    pub fn translate_virtual_trait_impl(
1237        &mut self,
1238        def_id: TraitImplId,
1239        item_meta: ItemMeta,
1240        vimpl: &hax::VirtualTraitImpl,
1241    ) -> Result<TraitImpl, Error> {
1242        let span = item_meta.span;
1243        let trait_def = self.hax_def(&vimpl.trait_pred.trait_ref)?;
1244        let hax::FullDefKind::Trait {
1245            items: trait_items, ..
1246        } = trait_def.kind()
1247        else {
1248            panic!()
1249        };
1250
1251        let implemented_trait = self.translate_trait_predicate(span, &vimpl.trait_pred)?;
1252        let implied_trait_refs =
1253            self.translate_trait_impl_exprs(span, &vimpl.implied_impl_exprs)?;
1254
1255        let mut types = vec![];
1256        // Monomorphic traits have no associated types.
1257        if !self.monomorphize() {
1258            let type_items = trait_items.iter().filter(|assoc| match assoc.kind {
1259                hax::AssocKind::Type { .. } => true,
1260                _ => false,
1261            });
1262            for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) {
1263                let name = self.t_ctx.translate_trait_item_name(&assoc.def_id)?;
1264                let assoc_ty = TraitAssocTyImpl {
1265                    value: self.translate_ty(span, ty)?,
1266                    implied_trait_refs: self.translate_trait_impl_exprs(span, impl_exprs)?,
1267                };
1268                let binder_kind = BinderKind::TraitType(implemented_trait.id, name.clone());
1269                types.push((name, Binder::empty(binder_kind, assoc_ty)));
1270            }
1271        }
1272
1273        let generics = self.the_only_binder().params.clone();
1274        Ok(TraitImpl {
1275            def_id,
1276            item_meta,
1277            impl_trait: implemented_trait,
1278            generics,
1279            implied_trait_refs,
1280            consts: vec![],
1281            types,
1282            methods: vec![],
1283            // TODO(dyn): generate vtable instances for builtin traits
1284            vtable: None,
1285        })
1286    }
1287
1288    /// Record that `method_id` is an implementation of the given method of the trait. If the
1289    /// method is not used anywhere yet we simply record the implementation. If the method is used
1290    /// then we enqueue it for translation.
1291    pub fn register_method_impl(
1292        &mut self,
1293        trait_id: TraitDeclId,
1294        method_name: TraitItemName,
1295        method_id: FunDeclId,
1296    ) {
1297        match self
1298            .method_status
1299            .get_or_extend_and_insert_default(trait_id)
1300            .entry(method_name)
1301            .or_default()
1302        {
1303            MethodStatus::Unused { implementors } => {
1304                implementors.insert(method_id);
1305            }
1306            MethodStatus::Used => {
1307                self.enqueue_id(method_id);
1308            }
1309        }
1310    }
1311
1312    /// Mark the method as "used", which will enqueue for translation all the implementations of
1313    /// that method.
1314    pub fn mark_method_as_used(&mut self, trait_id: TraitDeclId, method_name: TraitItemName) {
1315        let method_status = self
1316            .method_status
1317            .get_or_extend_and_insert_default(trait_id)
1318            .entry(method_name)
1319            .or_default();
1320        match method_status {
1321            MethodStatus::Unused { implementors } => {
1322                let implementors = mem::take(implementors);
1323                *method_status = MethodStatus::Used;
1324                for fun_id in implementors {
1325                    self.enqueue_id(fun_id);
1326                }
1327            }
1328            MethodStatus::Used => {}
1329        }
1330    }
1331
1332    /// In case an impl does not override a trait method, this duplicates the original trait method
1333    /// and adjusts its generics to make the corresponding impl method.
1334    #[tracing::instrument(skip(self, item_meta))]
1335    pub fn translate_defaulted_method(
1336        &mut self,
1337        def_id: FunDeclId,
1338        item_meta: ItemMeta,
1339        def: &hax::FullDef,
1340        impl_kind: TraitImplSource,
1341        method_name: TraitItemName,
1342    ) -> Result<FunDecl, Error> {
1343        let span = item_meta.span;
1344
1345        let hax::FullDefKind::TraitImpl { trait_pred, .. } = &def.kind else {
1346            unreachable!()
1347        };
1348
1349        // Retrieve the information about the implemented trait.
1350        let implemented_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
1351        // A `TraitRef` that points to this impl with the correct generics.
1352        let self_impl_ref = self.translate_trait_impl_ref(span, def.this(), impl_kind)?;
1353        let self_predicate_kind = TraitRefKind::TraitImpl(self_impl_ref.clone());
1354
1355        // Build a reference to the original declared method.
1356        let ItemRef::TraitDecl(tdecl) = self.get_or_translate(implemented_trait.id.into())? else {
1357            panic!()
1358        };
1359        let Some(bound_method) = tdecl.methods.iter().find(|m| m.name() == method_name) else {
1360            raise_error!(
1361                self,
1362                span,
1363                "Could not find a method with name \
1364                `{method_name}` in trait `{:?}`",
1365                trait_pred.trait_ref.def_id,
1366            )
1367        };
1368        let bound_fn_ref: Binder<FunDeclRef> = bound_method
1369            .clone()
1370            .substitute_with_self(&implemented_trait.generics, &self_predicate_kind)
1371            .map(|m| m.item);
1372
1373        // Now we need to create the generic params for the new method. These are the concatenation
1374        // of the impl params and the method params. We obtain that by making the two existing
1375        // binders explicit and using `binder.flatten()`.
1376        let bound_fn_ref: Binder<Binder<FunDeclRef>> = Binder {
1377            params: self.outermost_generics().clone(),
1378            skip_binder: bound_fn_ref,
1379            kind: BinderKind::Other,
1380        };
1381        let bound_fn_ref: Binder<FunDeclRef> = bound_fn_ref.flatten();
1382
1383        // Create a copy of the provided method with the new generics.
1384        let original_method_id = bound_fn_ref.skip_binder.id;
1385        let ItemRef::Fun(fun_decl) = self.get_or_translate(original_method_id.into())? else {
1386            panic!()
1387        };
1388        let mut fun_decl = fun_decl
1389            .clone()
1390            .substitute_params(bound_fn_ref.map(|x| *x.generics));
1391
1392        // Update the rest of the data.
1393        fun_decl.def_id = def_id;
1394        // We use the span of the *impl*, not the span of the default method in the
1395        // original trait declaration.
1396        fun_decl.item_meta = ItemMeta {
1397            name: item_meta.name,
1398            opacity: item_meta.opacity,
1399            is_local: item_meta.is_local,
1400            span: item_meta.span,
1401            source_text: fun_decl.item_meta.source_text,
1402            attr_info: fun_decl.item_meta.attr_info,
1403            lang_item: fun_decl.item_meta.lang_item,
1404        };
1405        fun_decl.src = if let ItemSource::TraitDecl {
1406            trait_ref,
1407            item_name,
1408            ..
1409        } = fun_decl.src
1410        {
1411            ItemSource::TraitImpl {
1412                impl_ref: self_impl_ref.clone(),
1413                trait_ref,
1414                item_name,
1415                reuses_default: true,
1416            }
1417        } else {
1418            unreachable!()
1419        };
1420        if !item_meta.opacity.is_transparent() {
1421            fun_decl.body = Body::Opaque;
1422        }
1423
1424        Ok(fun_decl)
1425    }
1426}
charon_driver/translate/translate_items.rs

charon_driver/translate/
translate_items.rs
