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

charon_driver/translate/
translate_items.rs
