charon_driver/translate/
translate_items.rs

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

charon_driver/translate/
translate_items.rs
