charon_driver/translate/
translate_trait_objects.rs

1use crate::translate::{translate_generics::BindingLevel, translate_predicates::PredicateLocation};
2
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use hax_frontend_exporter as hax;
6
7impl ItemTransCtx<'_, '_> {
8    pub fn check_at_most_one_pred_has_methods(
9        &mut self,
10        span: Span,
11        preds: &hax::GenericPredicates,
12    ) -> Result<(), Error> {
13        // Only the first clause is allowed to have methods.
14        for (clause, _) in preds.predicates.iter().skip(1) {
15            if let hax::ClauseKind::Trait(trait_predicate) = clause.kind.hax_skip_binder_ref() {
16                let trait_def_id = &trait_predicate.trait_ref.def_id;
17                let trait_def = self.hax_def(trait_def_id)?;
18                let has_methods = match trait_def.kind() {
19                    hax::FullDefKind::Trait { items, .. } => items
20                        .iter()
21                        .any(|(assoc, _)| matches!(assoc.kind, hax::AssocKind::Fn { .. })),
22                    hax::FullDefKind::TraitAlias { .. } => false,
23                    _ => unreachable!(),
24                };
25                if has_methods {
26                    raise_error!(
27                        self,
28                        span,
29                        "`dyn Trait` with multiple method-bearing predicates is not supported"
30                    );
31                }
32            }
33        }
34        Ok(())
35    }
36
37    pub fn translate_existential_predicates(
38        &mut self,
39        span: Span,
40        self_ty: &hax::ParamTy,
41        preds: &hax::GenericPredicates,
42        region: &hax::Region,
43    ) -> Result<DynPredicate, Error> {
44        // This is a robustness check: the current version of Rustc
45        // accepts at most one method-bearing predicate in a trait object.
46        // But things may change in the future.
47        self.check_at_most_one_pred_has_methods(span, preds)?;
48
49        // Translate the region outside the binder.
50        let region = self.translate_region(span, region)?;
51        let region = region.move_under_binder();
52
53        // Add a binder that contains the existentially quantified type.
54        self.binding_levels.push(BindingLevel::new(true));
55
56        // Add the existentially quantified type.
57        let ty_id = self
58            .innermost_binder_mut()
59            .push_type_var(self_ty.index, self_ty.name.clone());
60        let ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(ty_id)).into_ty();
61
62        self.innermost_binder_mut()
63            .params
64            .types_outlive
65            .push(RegionBinder::empty(OutlivesPred(ty.clone(), region)));
66        self.register_predicates(preds, PredicateOrigin::Dyn, &PredicateLocation::Base)?;
67
68        let params = self.binding_levels.pop().unwrap().params;
69        let binder = Binder {
70            params: params,
71            skip_binder: ty,
72            kind: BinderKind::Dyn,
73        };
74        Ok(DynPredicate { binder })
75    }
76}
charon_driver/translate/translate_trait_objects.rs

charon_driver/translate/
translate_trait_objects.rs
