charon_driver/translate/
translate_types.rs

1use crate::translate::translate_traits::PredicateLocation;
2
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use charon_lib::builtins;
6use charon_lib::common::hash_by_addr::HashByAddr;
7use charon_lib::ids::Vector;
8use core::convert::*;
9use hax::Visibility;
10use hax_frontend_exporter as hax;
11
12/// Small helper: we ignore some region names (when they are equal to "'_")
13fn check_region_name(s: String) -> Option<String> {
14    if s == "'_" {
15        None
16    } else {
17        Some(s)
18    }
19}
20
21pub fn translate_bound_region_kind_name(kind: &hax::BoundRegionKind) -> Option<String> {
22    use hax::BoundRegionKind::*;
23    let s = match kind {
24        Anon => None,
25        Named(_, symbol) => Some(symbol.clone()),
26        ClosureEnv => Some("@env".to_owned()),
27    };
28    s.and_then(check_region_name)
29}
30
31pub fn translate_region_name(region: &hax::EarlyParamRegion) -> Option<String> {
32    let s = region.name.clone();
33    check_region_name(s)
34}
35
36impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
37    // Translate a region
38    pub(crate) fn translate_region(
39        &mut self,
40        span: Span,
41        region: &hax::Region,
42    ) -> Result<Region, Error> {
43        use hax::RegionKind::*;
44        match &region.kind {
45            ReErased => Ok(Region::Erased),
46            ReStatic => Ok(Region::Static),
47            ReBound(id, br) => {
48                let var = self.lookup_bound_region(span, *id, br.var)?;
49                Ok(Region::Var(var))
50            }
51            ReEarlyParam(region) => {
52                let var = self.lookup_early_region(span, region)?;
53                Ok(Region::Var(var))
54            }
55            ReVar(..) | RePlaceholder(..) => {
56                // Shouldn't exist outside of type inference.
57                raise_error!(
58                    self,
59                    span,
60                    "Should not exist outside of type inference: {region:?}"
61                )
62            }
63            ReLateParam(..) | ReError(..) => {
64                raise_error!(self, span, "Unexpected region kind: {region:?}")
65            }
66        }
67    }
68
69    /// Translate a Ty.
70    ///
71    /// Typically used in this module to translate the fields of a structure/
72    /// enumeration definition, or later to translate the type of a variable.
73    ///
74    /// Note that we take as parameter a function to translate regions, because
75    /// regions can be translated in several manners (non-erased region or erased
76    /// regions), in which case the return type is different.
77    #[tracing::instrument(skip(self, span))]
78    pub(crate) fn translate_ty(&mut self, span: Span, ty: &hax::Ty) -> Result<Ty, Error> {
79        trace!("{:?}", ty);
80        let cache_key = HashByAddr(ty.inner().clone());
81        if let Some(ty) = self.lookup_cached_type(&cache_key) {
82            return Ok(ty.clone());
83        }
84
85        let kind = match ty.kind() {
86            hax::TyKind::Bool => TyKind::Literal(LiteralTy::Bool),
87            hax::TyKind::Char => TyKind::Literal(LiteralTy::Char),
88            hax::TyKind::Int(int_ty) => {
89                use hax::IntTy;
90                TyKind::Literal(LiteralTy::Integer(match int_ty {
91                    IntTy::Isize => IntegerTy::Isize,
92                    IntTy::I8 => IntegerTy::I8,
93                    IntTy::I16 => IntegerTy::I16,
94                    IntTy::I32 => IntegerTy::I32,
95                    IntTy::I64 => IntegerTy::I64,
96                    IntTy::I128 => IntegerTy::I128,
97                }))
98            }
99            hax::TyKind::Uint(int_ty) => {
100                use hax::UintTy;
101                TyKind::Literal(LiteralTy::Integer(match int_ty {
102                    UintTy::Usize => IntegerTy::Usize,
103                    UintTy::U8 => IntegerTy::U8,
104                    UintTy::U16 => IntegerTy::U16,
105                    UintTy::U32 => IntegerTy::U32,
106                    UintTy::U64 => IntegerTy::U64,
107                    UintTy::U128 => IntegerTy::U128,
108                }))
109            }
110            hax::TyKind::Float(float_ty) => {
111                use hax::FloatTy;
112                TyKind::Literal(LiteralTy::Float(match float_ty {
113                    FloatTy::F16 => charon_lib::ast::types::FloatTy::F16,
114                    FloatTy::F32 => charon_lib::ast::types::FloatTy::F32,
115                    FloatTy::F64 => charon_lib::ast::types::FloatTy::F64,
116                    FloatTy::F128 => charon_lib::ast::types::FloatTy::F128,
117                }))
118            }
119            hax::TyKind::Never => TyKind::Never,
120
121            hax::TyKind::Alias(alias) => match &alias.kind {
122                hax::AliasKind::Projection {
123                    impl_expr,
124                    assoc_item,
125                } => {
126                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
127                    let name = TraitItemName(assoc_item.name.clone());
128                    TyKind::TraitType(trait_ref, name)
129                }
130                hax::AliasKind::Opaque { hidden_ty, .. } => {
131                    return self.translate_ty(span, hidden_ty)
132                }
133                _ => {
134                    raise_error!(self, span, "Unsupported alias type: {:?}", alias.kind)
135                }
136            },
137
138            hax::TyKind::Adt {
139                generic_args: substs,
140                trait_refs,
141                def_id,
142            } => {
143                trace!("Adt: {:?}", def_id);
144
145                // Retrieve the type identifier
146                let type_id = self.translate_type_id(span, def_id)?;
147
148                // Translate the type parameters instantiation
149                let mut generics = self.translate_generic_args(
150                    span,
151                    substs,
152                    trait_refs,
153                    None,
154                    type_id.generics_target(),
155                )?;
156
157                // Filter the type arguments.
158                // TODO: do this in a micro-pass
159                if let TypeId::Builtin(builtin_ty) = type_id {
160                    let used_args = builtins::type_to_used_params(builtin_ty);
161                    error_assert!(self, span, generics.types.elem_count() == used_args.len());
162                    let types = std::mem::take(&mut generics.types)
163                        .into_iter()
164                        .zip(used_args)
165                        .filter(|(_, used)| *used)
166                        .map(|(ty, _)| ty)
167                        .collect();
168                    generics.types = types;
169                }
170
171                // Return the instantiated ADT
172                TyKind::Adt(type_id, generics)
173            }
174            hax::TyKind::Str => {
175                trace!("Str");
176
177                let id = TypeId::Builtin(BuiltinTy::Str);
178                TyKind::Adt(id, GenericArgs::empty(GenericsSource::Builtin))
179            }
180            hax::TyKind::Array(ty, const_param) => {
181                trace!("Array");
182
183                let c = self.translate_constant_expr_to_const_generic(span, const_param)?;
184                let tys = vec![self.translate_ty(span, ty)?].into();
185                let cgs = vec![c].into();
186                let id = TypeId::Builtin(BuiltinTy::Array);
187                TyKind::Adt(
188                    id,
189                    GenericArgs::new(
190                        Vector::new(),
191                        tys,
192                        cgs,
193                        Vector::new(),
194                        GenericsSource::Builtin,
195                    ),
196                )
197            }
198            hax::TyKind::Slice(ty) => {
199                trace!("Slice");
200
201                let tys = vec![self.translate_ty(span, ty)?].into();
202                let id = TypeId::Builtin(BuiltinTy::Slice);
203                TyKind::Adt(id, GenericArgs::new_for_builtin(tys))
204            }
205            hax::TyKind::Ref(region, ty, mutability) => {
206                trace!("Ref");
207
208                let region = self.translate_region(span, region)?;
209                let ty = self.translate_ty(span, ty)?;
210                let kind = if *mutability {
211                    RefKind::Mut
212                } else {
213                    RefKind::Shared
214                };
215                TyKind::Ref(region, ty, kind)
216            }
217            hax::TyKind::RawPtr(ty, mutbl) => {
218                trace!("RawPtr: {:?}", (ty, mutbl));
219                let ty = self.translate_ty(span, ty)?;
220                let kind = if *mutbl {
221                    RefKind::Mut
222                } else {
223                    RefKind::Shared
224                };
225                TyKind::RawPtr(ty, kind)
226            }
227            hax::TyKind::Tuple(substs) => {
228                trace!("Tuple");
229
230                let mut params = Vector::new();
231                for param in substs.iter() {
232                    let param_ty = self.translate_ty(span, param)?;
233                    params.push(param_ty);
234                }
235
236                TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(params))
237            }
238
239            hax::TyKind::Param(param) => {
240                // A type parameter, for example `T` in `fn f<T>(x : T) {}`.
241                // Note that this type parameter may actually have been
242                // instantiated (in our environment, we may map it to another
243                // type): we just have to look it up.
244                // Note that if we are using this function to translate a field
245                // type in a type definition, it should actually map to a type
246                // parameter.
247                trace!("Param");
248
249                // Retrieve the translation of the substituted type:
250                let var = self.lookup_type_var(span, param)?;
251                TyKind::TypeVar(var)
252            }
253
254            hax::TyKind::Foreign(def_id) => {
255                trace!("Foreign");
256                let adt_id = self.translate_type_id(span, def_id)?;
257                TyKind::Adt(adt_id, GenericArgs::empty(adt_id.generics_target()))
258            }
259            hax::TyKind::Infer(_) => {
260                trace!("Infer");
261                raise_error!(self, span, "Unsupported type: infer type")
262            }
263
264            hax::TyKind::Dynamic(_existential_preds, _region, _) => {
265                // TODO: we don't translate the predicates yet because our machinery can't handle
266                // it.
267                trace!("Dynamic");
268                TyKind::DynTrait(ExistentialPredicate)
269            }
270
271            hax::TyKind::Coroutine(..) => {
272                trace!("Coroutine");
273                raise_error!(self, span, "Coroutine types are not supported yet")
274            }
275
276            hax::TyKind::Bound(_, _) => {
277                trace!("Bound");
278                raise_error!(self, span, "Unexpected type kind: bound")
279            }
280            hax::TyKind::Placeholder(_) => {
281                trace!("PlaceHolder");
282                raise_error!(self, span, "Unsupported type: placeholder")
283            }
284            hax::TyKind::Arrow(box sig) => {
285                trace!("Arrow");
286                trace!("bound vars: {:?}", sig.bound_vars);
287                let sig = self.translate_region_binder(span, sig, |ctx, sig| {
288                    let inputs = sig
289                        .inputs
290                        .iter()
291                        .map(|x| ctx.translate_ty(span, x))
292                        .try_collect()?;
293                    let output = ctx.translate_ty(span, &sig.output)?;
294                    Ok((inputs, output))
295                })?;
296                TyKind::Arrow(sig)
297            }
298            hax::TyKind::Closure(
299                def_id,
300                hax::ClosureArgs {
301                    untupled_sig: sig,
302                    parent_args,
303                    parent_trait_refs,
304                    upvar_tys,
305                    ..
306                },
307            ) => {
308                let signature = self.translate_region_binder(span, sig, |ctx, sig| {
309                    let inputs = sig
310                        .inputs
311                        .iter()
312                        .map(|x| ctx.translate_ty(span, x))
313                        .try_collect()?;
314                    let output = ctx.translate_ty(span, &sig.output)?;
315                    Ok((inputs, output))
316                })?;
317                let fun_id = self.register_fun_decl_id(span, def_id);
318                let upvar_tys = upvar_tys
319                    .iter()
320                    .map(|ty| self.translate_ty(span, ty))
321                    .try_collect()?;
322                let parent_args = self.translate_generic_args(
323                    span,
324                    &parent_args,
325                    &parent_trait_refs,
326                    None,
327                    // We don't know the item these generics apply to.
328                    GenericsSource::Builtin,
329                )?;
330                TyKind::Closure {
331                    fun_id,
332                    signature,
333                    parent_args: Box::new(parent_args),
334                    upvar_tys,
335                }
336            }
337            hax::TyKind::Error => {
338                trace!("Error");
339                raise_error!(self, span, "Type checking error")
340            }
341            hax::TyKind::Todo(s) => {
342                trace!("Todo: {s}");
343                raise_error!(self, span, "Unsupported type: {:?}", s)
344            }
345        };
346        let ty = kind.into_ty();
347        self.innermost_binder_mut()
348            .type_trans_cache
349            .insert(cache_key, ty.clone());
350        Ok(ty)
351    }
352
353    pub fn translate_generic_args(
354        &mut self,
355        span: Span,
356        substs: &[hax::GenericArg],
357        trait_refs: &[hax::ImplExpr],
358        late_bound: Option<hax::Binder<()>>,
359        target: GenericsSource,
360    ) -> Result<GenericArgs, Error> {
361        use hax::GenericArg::*;
362        trace!("{:?}", substs);
363
364        let mut regions = Vector::new();
365        let mut types = Vector::new();
366        let mut const_generics = Vector::new();
367        for param in substs {
368            match param {
369                Type(param_ty) => {
370                    types.push(self.translate_ty(span, param_ty)?);
371                }
372                Lifetime(region) => {
373                    regions.push(self.translate_region(span, region)?);
374                }
375                Const(c) => {
376                    const_generics.push(self.translate_constant_expr_to_const_generic(span, c)?);
377                }
378            }
379        }
380        // Add the late-bounds lifetimes if any.
381        if let Some(binder) = late_bound {
382            for v in &binder.bound_vars {
383                match v {
384                    hax::BoundVariableKind::Region(_) => {
385                        regions.push(Region::Erased);
386                    }
387                    hax::BoundVariableKind::Ty(_) => {
388                        raise_error!(self, span, "Unexpected locally bound type variable")
389                    }
390                    hax::BoundVariableKind::Const => {
391                        raise_error!(self, span, "Unexpected locally bound const generic")
392                    }
393                }
394            }
395        }
396        let trait_refs = self.translate_trait_impl_exprs(span, trait_refs)?;
397
398        Ok(GenericArgs {
399            regions,
400            types,
401            const_generics,
402            trait_refs,
403            target,
404        })
405    }
406
407    /// Checks whether the given id corresponds to a built-in type.
408    fn recognize_builtin_type(&mut self, def_id: &hax::DefId) -> Result<Option<BuiltinTy>, Error> {
409        let def = self.t_ctx.hax_def(def_id)?;
410        let ty = if def.lang_item.as_deref() == Some("owned_box") {
411            Some(BuiltinTy::Box)
412        } else {
413            None
414        };
415        Ok(ty)
416    }
417
418    /// Translate a type def id
419    pub(crate) fn translate_type_id(
420        &mut self,
421        span: Span,
422        def_id: &hax::DefId,
423    ) -> Result<TypeId, Error> {
424        trace!("{:?}", def_id);
425        let type_id = match self.recognize_builtin_type(def_id)? {
426            Some(id) => TypeId::Builtin(id),
427            None => TypeId::Adt(self.register_type_decl_id(span, def_id)),
428        };
429        Ok(type_id)
430    }
431
432    /// Translate the body of a type declaration.
433    ///
434    /// Note that the type may be external, in which case we translate the body
435    /// only if it is public (i.e., it is a public enumeration, or it is a
436    /// struct with only public fields).
437    fn translate_adt_def(
438        &mut self,
439        trans_id: TypeDeclId,
440        def_span: Span,
441        item_meta: &ItemMeta,
442        adt: &hax::AdtDef,
443    ) -> Result<TypeDeclKind, Error> {
444        use hax::AdtKind;
445
446        if item_meta.opacity.is_opaque() {
447            return Ok(TypeDeclKind::Opaque);
448        }
449
450        trace!("{}", trans_id);
451
452        // In case the type is external, check if we should consider the type as
453        // transparent (i.e., extract its body). If it is an enumeration, then yes
454        // (because the variants of public enumerations are public, together with their
455        // fields). If it is a structure, we check if all the fields are public.
456        let contents_are_public = match adt.adt_kind {
457            AdtKind::Enum => true,
458            AdtKind::Struct | AdtKind::Union => {
459                // Check the unique variant
460                error_assert!(self, def_span, adt.variants.len() == 1);
461                adt.variants[0]
462                    .fields
463                    .iter()
464                    .all(|f| matches!(f.vis, Visibility::Public))
465            }
466        };
467
468        if item_meta
469            .opacity
470            .with_content_visibility(contents_are_public)
471            .is_opaque()
472        {
473            return Ok(TypeDeclKind::Opaque);
474        }
475
476        // The type is transparent: explore the variants
477        let mut variants: Vector<VariantId, Variant> = Default::default();
478        for (i, var_def) in adt.variants.iter().enumerate() {
479            trace!("variant {i}: {var_def:?}");
480
481            let mut fields: Vector<FieldId, Field> = Default::default();
482            /* This is for sanity: check that either all the fields have names, or
483             * none of them has */
484            let mut have_names: Option<bool> = None;
485            for (j, field_def) in var_def.fields.iter().enumerate() {
486                trace!("variant {i}: field {j}: {field_def:?}");
487                let field_span = self.t_ctx.translate_span_from_hax(&field_def.span);
488                // Translate the field type
489                let ty = self.translate_ty(field_span, &field_def.ty)?;
490                let field_full_def = self.t_ctx.hax_def(&field_def.did)?;
491                let field_attrs = self.t_ctx.translate_attr_info(&field_full_def);
492
493                // Retrieve the field name.
494                let field_name = field_def.name.clone();
495                // Sanity check
496                match &have_names {
497                    None => {
498                        have_names = match &field_name {
499                            None => Some(false),
500                            Some(_) => Some(true),
501                        }
502                    }
503                    Some(b) => {
504                        error_assert!(self, field_span, *b == field_name.is_some());
505                    }
506                };
507
508                // Store the field
509                let field = Field {
510                    span: field_span,
511                    attr_info: field_attrs,
512                    name: field_name.clone(),
513                    ty,
514                };
515                fields.push(field);
516            }
517
518            let discriminant = self.translate_discriminant(def_span, &var_def.discr_val)?;
519            let variant_span = self.t_ctx.translate_span_from_hax(&var_def.span);
520            let variant_name = var_def.name.clone();
521            let variant_full_def = self.t_ctx.hax_def(&var_def.def_id)?;
522            let variant_attrs = self.t_ctx.translate_attr_info(&variant_full_def);
523
524            let mut variant = Variant {
525                span: variant_span,
526                attr_info: variant_attrs,
527                name: variant_name,
528                fields,
529                discriminant,
530            };
531            // Propagate a `#[charon::variants_prefix(..)]` or `#[charon::variants_suffix(..)]` attribute to the variants.
532            if variant.attr_info.rename.is_none() {
533                let prefix = item_meta
534                    .attr_info
535                    .attributes
536                    .iter()
537                    .filter_map(|a| a.as_variants_prefix())
538                    .next()
539                    .map(|attr| attr.as_str());
540                let suffix = item_meta
541                    .attr_info
542                    .attributes
543                    .iter()
544                    .filter_map(|a| a.as_variants_suffix())
545                    .next()
546                    .map(|attr| attr.as_str());
547                if prefix.is_some() || suffix.is_some() {
548                    let prefix = prefix.unwrap_or_default();
549                    let suffix = suffix.unwrap_or_default();
550                    let name = &variant.name;
551                    variant.attr_info.rename = Some(format!("{prefix}{name}{suffix}"));
552                }
553            }
554            variants.push(variant);
555        }
556
557        // Register the type
558        let type_def_kind: TypeDeclKind = match adt.adt_kind {
559            AdtKind::Struct => TypeDeclKind::Struct(variants[0].fields.clone()),
560            AdtKind::Enum => TypeDeclKind::Enum(variants),
561            AdtKind::Union => TypeDeclKind::Union(variants[0].fields.clone()),
562        };
563
564        Ok(type_def_kind)
565    }
566
567    fn translate_discriminant(
568        &mut self,
569        def_span: Span,
570        discr: &hax::DiscriminantValue,
571    ) -> Result<ScalarValue, Error> {
572        let ty = self.translate_ty(def_span, &discr.ty)?;
573        let int_ty = *ty.kind().as_literal().unwrap().as_integer().unwrap();
574        Ok(ScalarValue::from_bits(int_ty, discr.val))
575    }
576
577    /// Translate the generics and predicates of this item and its parents.
578    pub(crate) fn translate_def_generics(
579        &mut self,
580        span: Span,
581        def: &hax::FullDef,
582    ) -> Result<(), Error> {
583        assert!(self.binding_levels.len() == 0);
584        self.binding_levels.push(BindingLevel::new(true));
585        self.push_generics_for_def(span, def, false)?;
586        self.innermost_binder_mut().params.check_consistency();
587        Ok(())
588    }
589
590    /// Translate the generics and predicates of this item without its parents.
591    pub(crate) fn translate_def_generics_without_parents(
592        &mut self,
593        span: Span,
594        def: &hax::FullDef,
595    ) -> Result<(), Error> {
596        self.binding_levels.push(BindingLevel::new(true));
597        self.push_generics_for_def_without_parents(span, def, true, true)?;
598        self.innermost_binder().params.check_consistency();
599        Ok(())
600    }
601
602    pub(crate) fn into_generics(mut self) -> GenericParams {
603        assert!(self.binding_levels.len() == 1);
604        self.binding_levels.pop().unwrap().params
605    }
606
607    /// Add the generics and predicates of this item and its parents to the current context.
608    #[tracing::instrument(skip(self, span))]
609    fn push_generics_for_def(
610        &mut self,
611        span: Span,
612        def: &hax::FullDef,
613        is_parent: bool,
614    ) -> Result<(), Error> {
615        use hax::FullDefKind;
616        // Add generics from the parent item, recursively (recursivity is important for closures,
617        // as they could be nested).
618        match &def.kind {
619            FullDefKind::AssocTy { .. }
620            | FullDefKind::AssocFn { .. }
621            | FullDefKind::AssocConst { .. }
622            | FullDefKind::AnonConst { .. }
623            | FullDefKind::InlineConst { .. }
624            | FullDefKind::PromotedConst { .. }
625            | FullDefKind::Closure { .. }
626            | FullDefKind::Ctor { .. }
627            | FullDefKind::Variant { .. } => {
628                let parent_def_id = def.parent.as_ref().unwrap();
629                let parent_def = self.t_ctx.hax_def(parent_def_id)?;
630                self.push_generics_for_def(span, &parent_def, true)?;
631            }
632            _ => {}
633        }
634        self.push_generics_for_def_without_parents(span, def, !is_parent, !is_parent)?;
635        Ok(())
636    }
637
638    /// Add the generics and predicates of this item. This does not include the parent generics;
639    /// use `push_generics_for_def` to get the full list.
640    fn push_generics_for_def_without_parents(
641        &mut self,
642        span: Span,
643        def: &hax::FullDef,
644        include_late_bound: bool,
645        include_assoc_ty_clauses: bool,
646    ) -> Result<(), Error> {
647        use hax::FullDefKind;
648        if let Some(param_env) = def.param_env() {
649            // Add the generic params.
650            self.push_generic_params(&param_env.generics)?;
651            // Add the self trait clause.
652            match &def.kind {
653                FullDefKind::TraitImpl {
654                    trait_pred: self_predicate,
655                    ..
656                }
657                | FullDefKind::Trait { self_predicate, .. } => {
658                    self.register_trait_decl_id(span, &self_predicate.trait_ref.def_id);
659                    let _ = self.translate_trait_predicate(span, self_predicate)?;
660                }
661                _ => {}
662            }
663            // Add the predicates.
664            let origin = match &def.kind {
665                FullDefKind::Struct { .. }
666                | FullDefKind::Union { .. }
667                | FullDefKind::Enum { .. }
668                | FullDefKind::TyAlias { .. }
669                | FullDefKind::AssocTy { .. } => PredicateOrigin::WhereClauseOnType,
670                FullDefKind::Fn { .. }
671                | FullDefKind::AssocFn { .. }
672                | FullDefKind::Const { .. }
673                | FullDefKind::AssocConst { .. }
674                | FullDefKind::AnonConst { .. }
675                | FullDefKind::InlineConst { .. }
676                | FullDefKind::PromotedConst { .. }
677                | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
678                FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
679                    PredicateOrigin::WhereClauseOnImpl
680                }
681                FullDefKind::Trait { .. } => {
682                    let _ = self.register_trait_decl_id(span, &def.def_id);
683                    PredicateOrigin::WhereClauseOnTrait
684                }
685                _ => panic!("Unexpected def: {def:?}"),
686            };
687            self.register_predicates(
688                &param_env.predicates,
689                origin.clone(),
690                &PredicateLocation::Base,
691            )?;
692            // Also register implied predicates.
693            if let FullDefKind::Trait {
694                implied_predicates, ..
695            }
696            | FullDefKind::AssocTy {
697                implied_predicates, ..
698            } = &def.kind
699            {
700                self.register_predicates(implied_predicates, origin, &PredicateLocation::Parent)?;
701            }
702
703            if let hax::FullDefKind::Trait { items, .. } = &def.kind
704                && include_assoc_ty_clauses
705            {
706                // Also add the predicates on associated types.
707                // FIXME(gat): don't skip GATs.
708                // FIXME: don't mix up implied and required predicates.
709                for (item, item_def) in items {
710                    if let hax::FullDefKind::AssocTy {
711                        param_env,
712                        implied_predicates,
713                        ..
714                    } = &item_def.kind
715                        && param_env.generics.params.is_empty()
716                    {
717                        let name = TraitItemName(item.name.clone());
718                        self.register_predicates(
719                            &implied_predicates,
720                            PredicateOrigin::TraitItem(name.clone()),
721                            &PredicateLocation::Item(name),
722                        )?;
723                    }
724                }
725            }
726        }
727
728        // The parameters (and in particular the lifetimes) are split between
729        // early bound and late bound parameters. See those blog posts for explanations:
730        // https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
731        // https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
732        // Note that only lifetimes can be late bound.
733        //
734        // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
735        // parameters here.
736        let signature = match &def.kind {
737            hax::FullDefKind::Closure { args, .. } => Some(&args.tupled_sig),
738            hax::FullDefKind::Fn { sig, .. } => Some(sig),
739            hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
740            _ => None,
741        };
742        if let Some(signature) = signature
743            && include_late_bound
744        {
745            let innermost_binder = self.innermost_binder_mut();
746            assert!(innermost_binder.bound_region_vars.is_empty());
747            innermost_binder.push_params_from_binder(signature.rebind(()))?;
748        }
749
750        Ok(())
751    }
752
753    pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
754        for param in &generics.params {
755            self.push_generic_param(param)?;
756        }
757        Ok(())
758    }
759
760    pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
761        match &param.kind {
762            hax::GenericParamDefKind::Lifetime => {
763                let region = hax::EarlyParamRegion {
764                    index: param.index,
765                    name: param.name.clone(),
766                };
767                let _ = self.innermost_binder_mut().push_early_region(region);
768            }
769            hax::GenericParamDefKind::Type { .. } => {
770                let _ = self
771                    .innermost_binder_mut()
772                    .push_type_var(param.index, param.name.clone());
773            }
774            hax::GenericParamDefKind::Const { ty, .. } => {
775                let span = self.def_span(&param.def_id);
776                // The type should be primitive, meaning it shouldn't contain variables,
777                // non-primitive adts, etc. As a result, we can use an empty context.
778                let ty = self.translate_ty(span, ty)?;
779                match ty.kind().as_literal() {
780                    Some(ty) => self.innermost_binder_mut().push_const_generic_var(
781                        param.index,
782                        *ty,
783                        param.name.clone(),
784                    ),
785                    None => raise_error!(
786                        self,
787                        span,
788                        "Constant parameters of non-literal type are not supported"
789                    ),
790                }
791            }
792        }
793
794        Ok(())
795    }
796}
797
798impl ItemTransCtx<'_, '_> {
799    /// Translate a type definition.
800    ///
801    /// Note that we translate the types one by one: we don't need to take into
802    /// account the fact that some types are mutually recursive at this point
803    /// (we will need to take that into account when generating the code in a file).
804    #[tracing::instrument(skip(self, item_meta))]
805    pub fn translate_type(
806        mut self,
807        trans_id: TypeDeclId,
808        item_meta: ItemMeta,
809        def: &hax::FullDef,
810    ) -> Result<TypeDecl, Error> {
811        let span = item_meta.span;
812
813        // Translate generics and predicates
814        self.translate_def_generics(span, def)?;
815
816        // Translate type body
817        let kind = match &def.kind {
818            _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
819            hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
820            hax::FullDefKind::TyAlias { ty, .. } => {
821                // Don't error on missing trait refs.
822                self.error_on_impl_expr_error = false;
823                // We only translate crate-local type aliases so the `unwrap` is ok.
824                let ty = ty.as_ref().unwrap();
825                self.translate_ty(span, ty).map(TypeDeclKind::Alias)
826            }
827            hax::FullDefKind::Struct { def, .. }
828            | hax::FullDefKind::Enum { def, .. }
829            | hax::FullDefKind::Union { def, .. } => {
830                self.translate_adt_def(trans_id, span, &item_meta, def)
831            }
832            _ => panic!("Unexpected item when translating types: {def:?}"),
833        };
834
835        let kind = match kind {
836            Ok(kind) => kind,
837            Err(err) => TypeDeclKind::Error(err.msg),
838        };
839        let type_def = TypeDecl {
840            def_id: trans_id,
841            item_meta,
842            generics: self.into_generics(),
843            kind,
844        };
845
846        Ok(type_def)
847    }
848}
charon_driver/translate/translate_types.rs

charon_driver/translate/
translate_types.rs
