charon_driver/translate/
translate_items.rs

1use super::translate_bodies::BodyTransCtx;
2use super::translate_crate::TransItemSource;
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use charon_lib::formatter::IntoFormatter;
6use charon_lib::pretty::FmtWithCtx;
7use hax_frontend_exporter as hax;
8use indexmap::IndexMap;
9use itertools::Itertools;
10use std::mem;
11use std::sync::Arc;
12
13impl<'tcx, 'ctx> TranslateCtx<'tcx> {
14    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
15        let trans_id = self.id_map.get(&item_src).copied();
16        let def_id = item_src.as_def_id();
17        self.with_def_id(def_id, trans_id, |mut ctx| {
18            let span = ctx.def_span(def_id);
19            // Catch cycles
20            let res = {
21                // Stopgap measure because there are still many panics in charon and hax.
22                let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
23                std::panic::catch_unwind(move || ctx.translate_item_aux(item_src, trans_id))
24            };
25            match res {
26                Ok(Ok(())) => return,
27                // Translation error
28                Ok(Err(_)) => {
29                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
30                }
31                // Panic
32                Err(_) => register_error!(
33                    ctx,
34                    span,
35                    "Thread panicked when extracting item `{def_id:?}`."
36                ),
37            };
38        })
39    }
40
41    pub(crate) fn translate_item_aux(
42        &mut self,
43        item_src: &TransItemSource,
44        trans_id: Option<AnyTransId>,
45    ) -> Result<(), Error> {
46        // Translate the meta information
47        let name = self.translate_name(item_src)?;
48        if let Some(trans_id) = trans_id {
49            self.translated.item_names.insert(trans_id, name.clone());
50        }
51        let opacity = self.opacity_for_name(&name);
52        if opacity.is_invisible() {
53            // Don't even start translating the item. In particular don't call `hax_def` on it.
54            return Ok(());
55        }
56        let def = self.hax_def(item_src.as_def_id())?;
57        let item_meta = self.translate_item_meta(&def, item_src, name, opacity);
58
59        // Initialize the item translation context
60        let bt_ctx = ItemTransCtx::new(def.def_id.clone(), trans_id, self);
61        match item_src {
62            TransItemSource::Type(_) => {
63                let Some(AnyTransId::Type(id)) = trans_id else {
64                    unreachable!()
65                };
66                let ty = bt_ctx.translate_type_decl(id, item_meta, &def)?;
67                self.translated.type_decls.set_slot(id, ty);
68            }
69            TransItemSource::Fun(_) => {
70                let Some(AnyTransId::Fun(id)) = trans_id else {
71                    unreachable!()
72                };
73                let fun_decl = bt_ctx.translate_function(id, item_meta, &def)?;
74                self.translated.fun_decls.set_slot(id, fun_decl);
75            }
76            TransItemSource::Global(_) => {
77                let Some(AnyTransId::Global(id)) = trans_id else {
78                    unreachable!()
79                };
80                let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
81                self.translated.global_decls.set_slot(id, global_decl);
82            }
83            TransItemSource::TraitDecl(_) => {
84                let Some(AnyTransId::TraitDecl(id)) = trans_id else {
85                    unreachable!()
86                };
87                let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
88                self.translated.trait_decls.set_slot(id, trait_decl);
89            }
90            TransItemSource::TraitImpl(_) => {
91                let Some(AnyTransId::TraitImpl(id)) = trans_id else {
92                    unreachable!()
93                };
94                let trait_impl = bt_ctx.translate_trait_impl(id, item_meta, &def)?;
95                self.translated.trait_impls.set_slot(id, trait_impl);
96            }
97            TransItemSource::ClosureTraitImpl(_, kind) => {
98                let Some(AnyTransId::TraitImpl(id)) = trans_id else {
99                    unreachable!()
100                };
101                let closure_trait_impl =
102                    bt_ctx.translate_closure_trait_impl(id, item_meta, &def, *kind)?;
103                self.translated.trait_impls.set_slot(id, closure_trait_impl);
104            }
105            TransItemSource::ClosureMethod(_, kind) => {
106                let Some(AnyTransId::Fun(id)) = trans_id else {
107                    unreachable!()
108                };
109                let fun_decl = bt_ctx.translate_closure_method(id, item_meta, &def, *kind)?;
110                self.translated.fun_decls.set_slot(id, fun_decl);
111            }
112        }
113        Ok(())
114    }
115}
116
117impl ItemTransCtx<'_, '_> {
118    pub(crate) fn get_item_kind(
119        &mut self,
120        span: Span,
121        def: &hax::FullDef,
122    ) -> Result<ItemKind, Error> {
123        let assoc = match def.kind() {
124            hax::FullDefKind::AssocTy {
125                associated_item, ..
126            }
127            | hax::FullDefKind::AssocConst {
128                associated_item, ..
129            }
130            | hax::FullDefKind::AssocFn {
131                associated_item, ..
132            } => associated_item,
133            hax::FullDefKind::Closure { args, .. } => {
134                let info = self.translate_closure_info(span, args)?;
135                return Ok(ItemKind::Closure { info });
136            }
137            _ => return Ok(ItemKind::TopLevel),
138        };
139        Ok(match &assoc.container {
140            // E.g.:
141            // ```
142            // impl<T> List<T> {
143            //   fn new() -> Self { ... } <- inherent method
144            // }
145            // ```
146            hax::AssocItemContainer::InherentImplContainer { .. } => ItemKind::TopLevel,
147            // E.g.:
148            // ```
149            // impl Foo for Bar {
150            //   fn baz(...) { ... } // <- implementation of a trait method
151            // }
152            // ```
153            hax::AssocItemContainer::TraitImplContainer {
154                impl_id,
155                impl_generics,
156                impl_required_impl_exprs,
157                implemented_trait_ref,
158                implemented_trait_item,
159                overrides_default,
160                ..
161            } => {
162                let impl_id = self.register_trait_impl_id(span, impl_id);
163                let impl_ref = TraitImplRef {
164                    impl_id,
165                    generics: Box::new(self.translate_generic_args(
166                        span,
167                        impl_generics,
168                        impl_required_impl_exprs,
169                        None,
170                        GenericsSource::item(impl_id),
171                    )?),
172                };
173                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
174                if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
175                    // Ensure we translate the corresponding decl signature.
176                    // FIXME(self_clause): also ensure we translate associated globals
177                    // consistently; to do once we have clearer `Self` clause handling.
178                    let _ = self.register_fun_decl_id(span, implemented_trait_item);
179                }
180                ItemKind::TraitImpl {
181                    impl_ref,
182                    trait_ref,
183                    item_name: TraitItemName(assoc.name.clone()),
184                    reuses_default: !overrides_default,
185                }
186            }
187            // This method is the *declaration* of a trait item
188            // E.g.:
189            // ```
190            // trait Foo {
191            //   fn baz(...); // <- declaration of a trait method
192            // }
193            // ```
194            hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
195                // The trait id should be Some(...): trait markers (that we may eliminate)
196                // don't have associated items.
197                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
198                let item_name = TraitItemName(assoc.name.clone());
199                ItemKind::TraitDecl {
200                    trait_ref,
201                    item_name,
202                    has_default: assoc.has_value,
203                }
204            }
205        })
206    }
207
208    /// Translate a type definition.
209    ///
210    /// Note that we translate the types one by one: we don't need to take into
211    /// account the fact that some types are mutually recursive at this point
212    /// (we will need to take that into account when generating the code in a file).
213    #[tracing::instrument(skip(self, item_meta))]
214    pub fn translate_type_decl(
215        mut self,
216        trans_id: TypeDeclId,
217        item_meta: ItemMeta,
218        def: &hax::FullDef,
219    ) -> Result<TypeDecl, Error> {
220        let span = item_meta.span;
221
222        // Translate generics and predicates
223        self.translate_def_generics(span, def)?;
224
225        // Translate type body
226        let kind = match &def.kind {
227            _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
228            hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
229            hax::FullDefKind::TyAlias { ty, .. } => {
230                // Don't error on missing trait refs.
231                self.error_on_impl_expr_error = false;
232                // We only translate crate-local type aliases so the `unwrap` is ok.
233                let ty = ty.as_ref().unwrap();
234                self.translate_ty(span, ty).map(TypeDeclKind::Alias)
235            }
236            hax::FullDefKind::Struct { def, .. }
237            | hax::FullDefKind::Enum { def, .. }
238            | hax::FullDefKind::Union { def, .. } => {
239                self.translate_adt_def(trans_id, span, &item_meta, def)
240            }
241            hax::FullDefKind::Closure { args, .. } => {
242                self.translate_closure_adt(trans_id, span, &args)
243            }
244            _ => panic!("Unexpected item when translating types: {def:?}"),
245        };
246
247        let kind = match kind {
248            Ok(kind) => kind,
249            Err(err) => TypeDeclKind::Error(err.msg),
250        };
251        let layout = self.translate_layout();
252        let type_def = TypeDecl {
253            def_id: trans_id,
254            item_meta,
255            generics: self.into_generics(),
256            kind,
257            layout,
258        };
259
260        Ok(type_def)
261    }
262
263    /// Translate one function.
264    #[tracing::instrument(skip(self, item_meta))]
265    pub fn translate_function(
266        mut self,
267        def_id: FunDeclId,
268        item_meta: ItemMeta,
269        def: &hax::FullDef,
270    ) -> Result<FunDecl, Error> {
271        trace!("About to translate function:\n{:?}", def.def_id);
272        let span = item_meta.span;
273
274        // Translate the function signature
275        trace!("Translating function signature");
276        let signature = self.translate_function_signature(def, &item_meta)?;
277
278        // Check whether this function is a method declaration for a trait definition.
279        // If this is the case, it shouldn't contain a body.
280        let kind = self.get_item_kind(span, def)?;
281        let is_trait_method_decl_without_default = match &kind {
282            ItemKind::TraitDecl { has_default, .. } => !has_default,
283            _ => false,
284        };
285
286        let is_global_initializer = matches!(
287            def.kind(),
288            hax::FullDefKind::Const { .. }
289                | hax::FullDefKind::AssocConst { .. }
290                | hax::FullDefKind::AnonConst { .. }
291                | hax::FullDefKind::InlineConst { .. }
292                | hax::FullDefKind::PromotedConst { .. }
293                | hax::FullDefKind::Static { .. }
294        );
295        let is_global_initializer =
296            is_global_initializer.then(|| self.register_global_decl_id(span, &def.def_id));
297
298        let body = if item_meta.opacity.with_private_contents().is_opaque()
299            || is_trait_method_decl_without_default
300        {
301            Err(Opaque)
302        } else if let hax::FullDefKind::Ctor {
303            adt_def_id,
304            ctor_of,
305            variant_id,
306            fields,
307            output_ty,
308            ..
309        } = def.kind()
310        {
311            let body = self.build_ctor_body(
312                span,
313                &signature,
314                adt_def_id,
315                ctor_of,
316                *variant_id,
317                fields,
318                output_ty,
319            )?;
320            Ok(body)
321        } else {
322            // Translate the body. This doesn't store anything if we can't/decide not to translate
323            // this body.
324            let mut bt_ctx = BodyTransCtx::new(&mut self);
325            match bt_ctx.translate_def_body(item_meta.span, def) {
326                Ok(Ok(body)) => Ok(body),
327                // Opaque declaration
328                Ok(Err(Opaque)) => Err(Opaque),
329                // Translation error.
330                // FIXME: handle error cases more explicitly.
331                Err(_) => Err(Opaque),
332            }
333        };
334        Ok(FunDecl {
335            def_id,
336            item_meta,
337            signature,
338            kind,
339            is_global_initializer,
340            body,
341        })
342    }
343
344    /// Translate one global.
345    #[tracing::instrument(skip(self, item_meta))]
346    pub fn translate_global(
347        mut self,
348        def_id: GlobalDeclId,
349        item_meta: ItemMeta,
350        def: &hax::FullDef,
351    ) -> Result<GlobalDecl, Error> {
352        trace!("About to translate global:\n{:?}", def.def_id);
353        let span = item_meta.span;
354
355        // Translate the generics and predicates - globals *can* have generics
356        // Ex.:
357        // ```
358        // impl<const N : usize> Foo<N> {
359        //   const LEN : usize = N;
360        // }
361        // ```
362        self.translate_def_generics(span, def)?;
363
364        // Retrieve the kind
365        let item_kind = self.get_item_kind(span, def)?;
366
367        trace!("Translating global type");
368        let ty = match &def.kind {
369            hax::FullDefKind::Const { ty, .. }
370            | hax::FullDefKind::AssocConst { ty, .. }
371            | hax::FullDefKind::AnonConst { ty, .. }
372            | hax::FullDefKind::InlineConst { ty, .. }
373            | hax::FullDefKind::PromotedConst { ty, .. }
374            | hax::FullDefKind::Static { ty, .. } => ty,
375            _ => panic!("Unexpected def for constant: {def:?}"),
376        };
377        let ty = self.translate_ty(span, ty)?;
378
379        let global_kind = match &def.kind {
380            hax::FullDefKind::Static { .. } => GlobalKind::Static,
381            hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. } => {
382                GlobalKind::NamedConst
383            }
384            hax::FullDefKind::AnonConst { .. }
385            | hax::FullDefKind::InlineConst { .. }
386            | hax::FullDefKind::PromotedConst { .. } => GlobalKind::AnonConst,
387            _ => panic!("Unexpected def for constant: {def:?}"),
388        };
389
390        let initializer = self.register_fun_decl_id(span, &def.def_id);
391
392        Ok(GlobalDecl {
393            def_id,
394            item_meta,
395            generics: self.into_generics(),
396            ty,
397            kind: item_kind,
398            global_kind,
399            init: initializer,
400        })
401    }
402
403    #[tracing::instrument(skip(self, item_meta))]
404    pub fn translate_trait_decl(
405        mut self,
406        def_id: TraitDeclId,
407        item_meta: ItemMeta,
408        def: &hax::FullDef,
409    ) -> Result<TraitDecl, Error> {
410        trace!("About to translate trait decl:\n{:?}", def.def_id);
411        trace!("Trait decl id:\n{:?}", def_id);
412
413        let span = item_meta.span;
414
415        if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
416            raise_error!(self, span, "Trait aliases are not supported");
417        }
418
419        let hax::FullDefKind::Trait {
420            items,
421            self_predicate,
422            ..
423        } = &def.kind
424        else {
425            raise_error!(self, span, "Unexpected definition: {def:?}");
426        };
427        let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
428            .iter()
429            .map(|(item, def)| {
430                let name = TraitItemName(item.name.clone());
431                (name, item, def.clone())
432            })
433            .collect_vec();
434
435        // Translate the generics
436        // Note that in the generics returned by [translate_def_generics], the trait refs only
437        // contain the local trait clauses. The parent clauses are stored in
438        // `self.parent_trait_clauses`.
439        self.translate_def_generics(span, def)?;
440        let self_trait_ref = TraitRef {
441            kind: TraitRefKind::SelfId,
442            trait_decl_ref: RegionBinder::empty(
443                self.translate_trait_predicate(span, self_predicate)?,
444            ),
445        };
446
447        // Translate the associated items
448        // We do something subtle here: TODO: explain
449        let mut consts = Vec::new();
450        let mut const_defaults = IndexMap::new();
451        let mut types = Vec::new();
452        let mut type_clauses = Vec::new();
453        let mut type_defaults = IndexMap::new();
454        let mut methods = Vec::new();
455        for (item_name, hax_item, hax_def) in &items {
456            let item_def_id = &hax_item.def_id;
457            let item_span = self.def_span(item_def_id);
458            match &hax_def.kind {
459                hax::FullDefKind::AssocFn { .. } => {
460                    let fun_def = self.t_ctx.hax_def(item_def_id)?;
461                    let binder_kind = BinderKind::TraitMethod(def_id, item_name.clone());
462                    let fn_ref = self.translate_binder_for_def(
463                        item_span,
464                        binder_kind,
465                        &fun_def,
466                        |bt_ctx| {
467                            // If the trait is opaque, we only translate the signature of a method
468                            // with default body if it's overridden or used somewhere else.
469                            // We insert the `Binder<FunDeclRef>` unconditionally here, and remove
470                            // the ones that correspond to untranslated functions in the
471                            // `remove_unused_methods` pass.
472                            // FIXME: this triggers the translation of traits used in the method
473                            // clauses, despite the fact that we may end up not needing them.
474                            let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
475                                || item_meta.opacity.is_transparent()
476                                || !hax_item.has_value
477                            {
478                                bt_ctx.register_fun_decl_id(item_span, item_def_id)
479                            } else {
480                                bt_ctx.register_fun_decl_id_no_enqueue(item_span, item_def_id)
481                            };
482
483                            assert_eq!(bt_ctx.binding_levels.len(), 2);
484                            let mut fun_generics =
485                                bt_ctx.outermost_binder().params.identity_args_at_depth(
486                                    GenericsSource::item(def_id),
487                                    DeBruijnId::one(),
488                                );
489                            // Add the necessary explicit `Self` clause at the start.
490                            fun_generics.trait_refs.insert_and_shift_ids(
491                                0.into(),
492                                self_trait_ref.clone().move_under_binder(),
493                            );
494                            fun_generics = fun_generics.concat(
495                                GenericsSource::item(fun_id),
496                                &bt_ctx.innermost_binder().params.identity_args_at_depth(
497                                    GenericsSource::Method(def_id.into(), item_name.clone()),
498                                    DeBruijnId::zero(),
499                                ),
500                            );
501                            Ok(FunDeclRef {
502                                id: fun_id,
503                                generics: Box::new(fun_generics),
504                            })
505                        },
506                    )?;
507                    methods.push((item_name.clone(), fn_ref));
508                }
509                hax::FullDefKind::AssocConst { ty, .. } => {
510                    // Check if the constant has a value (i.e., a body).
511                    if hax_item.has_value {
512                        // The parameters of the constant are the same as those of the item that
513                        // declares them.
514                        let id = self.register_global_decl_id(item_span, item_def_id);
515                        let generics_target = GenericsSource::item(id);
516                        let mut generics =
517                            self.the_only_binder().params.identity_args(generics_target);
518                        generics.trait_refs.push(self_trait_ref.clone());
519                        let gref = GlobalDeclRef {
520                            id,
521                            generics: Box::new(generics),
522                        };
523                        const_defaults.insert(item_name.clone(), gref);
524                    };
525                    let ty = self.translate_ty(item_span, ty)?;
526                    consts.push((item_name.clone(), ty));
527                }
528                hax::FullDefKind::AssocTy { param_env, .. }
529                    if !param_env.generics.params.is_empty() =>
530                {
531                    raise_error!(
532                        self,
533                        item_span,
534                        "Generic associated types are not supported"
535                    );
536                }
537                hax::FullDefKind::AssocTy { value, .. } => {
538                    // TODO: handle generics (i.e. GATs).
539                    if let Some(clauses) = self.item_trait_clauses.get(item_name) {
540                        type_clauses.push((item_name.clone(), clauses.clone()));
541                    }
542                    if let Some(ty) = value {
543                        let ty = self.translate_ty(item_span, &ty)?;
544                        type_defaults.insert(item_name.clone(), ty);
545                    };
546                    types.push(item_name.clone());
547                }
548                _ => panic!("Unexpected definition for trait item: {hax_def:?}"),
549            }
550        }
551
552        // In case of a trait implementation, some values may not have been
553        // provided, in case the declaration provided default values. We
554        // check those, and lookup the relevant values.
555        Ok(TraitDecl {
556            def_id,
557            item_meta,
558            parent_clauses: mem::take(&mut self.parent_trait_clauses),
559            generics: self.into_generics(),
560            type_clauses,
561            consts,
562            const_defaults,
563            types,
564            type_defaults,
565            methods,
566        })
567    }
568
569    #[tracing::instrument(skip(self, item_meta))]
570    pub fn translate_trait_impl(
571        mut self,
572        def_id: TraitImplId,
573        item_meta: ItemMeta,
574        def: &hax::FullDef,
575    ) -> Result<TraitImpl, Error> {
576        trace!("About to translate trait impl:\n{:?}", def.def_id);
577        trace!("Trait impl id:\n{:?}", def_id);
578
579        let span = item_meta.span;
580
581        self.translate_def_generics(span, def)?;
582
583        let hax::FullDefKind::TraitImpl {
584            trait_pred,
585            implied_impl_exprs,
586            items: impl_items,
587            ..
588        } = &def.kind
589        else {
590            unreachable!()
591        };
592
593        // Retrieve the information about the implemented trait.
594        let implemented_trait_id = &trait_pred.trait_ref.def_id;
595        let trait_id = self.register_trait_decl_id(span, implemented_trait_id);
596        let implemented_trait = {
597            let implemented_trait = &trait_pred.trait_ref;
598            let generics = self.translate_generic_args(
599                span,
600                &implemented_trait.generic_args,
601                &[],
602                None,
603                GenericsSource::item(trait_id),
604            )?;
605            TraitDeclRef {
606                trait_id,
607                generics: Box::new(generics),
608            }
609        };
610        // A `TraitRef` that points to this impl with the correct generics.
611        let self_predicate = TraitRef {
612            kind: TraitRefKind::TraitImpl(
613                def_id,
614                Box::new(
615                    self.the_only_binder()
616                        .params
617                        .identity_args(GenericsSource::item(def_id)),
618                ),
619            ),
620            trait_decl_ref: RegionBinder::empty(implemented_trait.clone()),
621        };
622
623        // The trait refs which implement the parent clauses of the implemented trait decl.
624        let parent_trait_refs = self.translate_trait_impl_exprs(span, &implied_impl_exprs)?;
625
626        {
627            // Debugging
628            let ctx = self.into_fmt();
629            let refs = parent_trait_refs
630                .iter()
631                .map(|c| c.with_ctx(&ctx))
632                .format("\n");
633            trace!(
634                "Trait impl: {:?}\n- parent_trait_refs:\n{}",
635                def.def_id,
636                refs
637            );
638        }
639
640        // Explore the associated items
641        let mut consts = Vec::new();
642        let mut types: Vec<(TraitItemName, Ty)> = Vec::new();
643        let mut methods = Vec::new();
644        let mut type_clauses = Vec::new();
645
646        for impl_item in impl_items {
647            use hax::ImplAssocItemValue::*;
648            let name = TraitItemName(impl_item.name.clone());
649            let item_def = impl_item.def(); // The impl item or the corresponding trait default.
650            let item_span = self.def_span(&item_def.def_id);
651            let item_def_id = &item_def.def_id;
652            match item_def.kind() {
653                hax::FullDefKind::AssocFn { .. } => {
654                    match &impl_item.value {
655                        Provided { is_override, .. } => {
656                            let fun_def = self.t_ctx.hax_def(item_def_id)?;
657                            let binder_kind = BinderKind::TraitMethod(trait_id, name.clone());
658                            let fn_ref = self.translate_binder_for_def(
659                                item_span,
660                                binder_kind,
661                                &fun_def,
662                                |bt_ctx| {
663                                    // If the impl is opaque, we only translate the signature of a
664                                    // method with a default body if it's directly used somewhere
665                                    // else.
666                                    // We insert the `Binder<FunDeclRef>` unconditionally here, and
667                                    // remove the ones that correspond to untranslated functions in
668                                    // the `remove_unused_methods` pass.
669                                    let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
670                                        || item_meta.opacity.is_transparent()
671                                        || !*is_override
672                                    {
673                                        bt_ctx.register_fun_decl_id(item_span, item_def_id)
674                                    } else {
675                                        bt_ctx
676                                            .register_fun_decl_id_no_enqueue(item_span, item_def_id)
677                                    };
678
679                                    // TODO: there's probably a cleaner way to write this
680                                    assert_eq!(bt_ctx.binding_levels.len(), 2);
681                                    let fun_generics = bt_ctx
682                                        .outermost_binder()
683                                        .params
684                                        .identity_args_at_depth(
685                                            GenericsSource::item(def_id),
686                                            DeBruijnId::one(),
687                                        )
688                                        .concat(
689                                            GenericsSource::item(fun_id),
690                                            &bt_ctx
691                                                .innermost_binder()
692                                                .params
693                                                .identity_args_at_depth(
694                                                    GenericsSource::Method(
695                                                        trait_id.into(),
696                                                        name.clone(),
697                                                    ),
698                                                    DeBruijnId::zero(),
699                                                ),
700                                        );
701                                    Ok(FunDeclRef {
702                                        id: fun_id,
703                                        generics: Box::new(fun_generics),
704                                    })
705                                },
706                            )?;
707                            methods.push((name, fn_ref));
708                        }
709                        DefaultedFn { .. } => {
710                            // TODO: handle defaulted methods
711                        }
712                        _ => unreachable!(),
713                    }
714                }
715                hax::FullDefKind::AssocConst { .. } => {
716                    let id = self.register_global_decl_id(item_span, item_def_id);
717                    let generics_target = GenericsSource::item(id);
718                    // The parameters of the constant are the same as those of the item that
719                    // declares them.
720                    let generics = match &impl_item.value {
721                        Provided { .. } => {
722                            self.the_only_binder().params.identity_args(generics_target)
723                        }
724                        _ => {
725                            let mut generics = implemented_trait
726                                .generics
727                                .clone()
728                                .with_target(generics_target);
729                            generics.trait_refs.push(self_predicate.clone());
730                            generics
731                        }
732                    };
733                    let gref = GlobalDeclRef {
734                        id,
735                        generics: Box::new(generics),
736                    };
737                    consts.push((name, gref));
738                }
739                hax::FullDefKind::AssocTy { param_env, .. }
740                    if !param_env.generics.params.is_empty() =>
741                {
742                    // We don't support GATs; the error was already reported in the trait declaration.
743                }
744                hax::FullDefKind::AssocTy { value, .. } => {
745                    let ty = match &impl_item.value {
746                        Provided { .. } => value.as_ref().unwrap(),
747                        DefaultedTy { ty, .. } => ty,
748                        _ => unreachable!(),
749                    };
750                    let ty = self.translate_ty(item_span, &ty)?;
751                    types.push((name.clone(), ty));
752
753                    let trait_refs =
754                        self.translate_trait_impl_exprs(item_span, &impl_item.required_impl_exprs)?;
755                    type_clauses.push((name, trait_refs));
756                }
757                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
758            }
759        }
760
761        Ok(TraitImpl {
762            def_id,
763            item_meta,
764            impl_trait: implemented_trait,
765            generics: self.into_generics(),
766            parent_trait_refs,
767            type_clauses,
768            consts,
769            types,
770            methods,
771        })
772    }
773}
charon_driver/translate/translate_items.rs

charon_driver/translate/
translate_items.rs
