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
12fn 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 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 ®ion.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 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 #[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 let type_id = self.translate_type_id(span, def_id)?;
147
148 let mut generics = self.translate_generic_args(
150 span,
151 substs,
152 trait_refs,
153 None,
154 type_id.generics_target(),
155 )?;
156
157 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 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 trace!("Param");
248
249 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 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 GenericsSource::Builtin,
329 )?;
330 TyKind::Closure {
331 fun_id,
332 signature,
333 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 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 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 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 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 let contents_are_public = match adt.adt_kind {
457 AdtKind::Enum => true,
458 AdtKind::Struct | AdtKind::Union => {
459 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 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 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 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 let field_name = field_def.name.clone();
495 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 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 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 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 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 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 #[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 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 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 self.push_generic_params(¶m_env.generics)?;
651 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 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 ¶m_env.predicates,
689 origin.clone(),
690 &PredicateLocation::Base,
691 )?;
692 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 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 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 ¶m.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(¶m.def_id);
776 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 #[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 self.translate_def_generics(span, def)?;
815
816 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 self.error_on_impl_expr_error = false;
823 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}