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

charon_driver/translate/
translate_items.rs
