1use crate::translate::translate_predicates::PredicateLocation;
2
3use super::translate_ctx::ItemTransCtx;
4use charon_lib::ast::*;
5use charon_lib::common::hash_by_addr::HashByAddr;
6use hax_frontend_exporter as hax;
7use std::collections::HashMap;
8use std::fmt::Debug;
9use std::sync::Arc;
10
11#[derive(Debug, Default)]
23pub(crate) struct BindingLevel {
24 pub params: GenericParams,
26 pub is_item_binder: bool,
30 pub early_region_vars: std::collections::BTreeMap<hax::EarlyParamRegion, RegionId>,
37 pub bound_region_vars: Vec<RegionId>,
39 pub by_ref_upvar_regions: Vec<RegionId>,
41 pub type_vars_map: HashMap<u32, TypeVarId>,
43 pub const_generic_vars_map: HashMap<u32, ConstGenericVarId>,
45 pub type_trans_cache: HashMap<HashByAddr<Arc<hax::TyKind>>, Ty>,
49}
50
51fn translate_region_name(s: String) -> Option<String> {
53 if s == "'_" {
54 None
55 } else {
56 Some(s)
57 }
58}
59
60impl BindingLevel {
61 pub(crate) fn new(is_item_binder: bool) -> Self {
62 Self {
63 is_item_binder,
64 ..Default::default()
65 }
66 }
67
68 pub(crate) fn push_early_region(&mut self, region: hax::EarlyParamRegion) -> RegionId {
70 let name = translate_region_name(region.name.clone());
71 assert!(
73 self.bound_region_vars.is_empty(),
74 "Early regions must be translated before late ones"
75 );
76 let rid = self
77 .params
78 .regions
79 .push_with(|index| RegionVar { index, name });
80 self.early_region_vars.insert(region, rid);
81 rid
82 }
83
84 pub(crate) fn push_bound_region(&mut self, region: hax::BoundRegionKind) -> RegionId {
86 use hax::BoundRegionKind::*;
87 let name = match region {
88 Anon => None,
89 Named(_, symbol) => translate_region_name(symbol.clone()),
90 ClosureEnv => Some("@env".to_owned()),
91 };
92 let rid = self
93 .params
94 .regions
95 .push_with(|index| RegionVar { index, name });
96 self.bound_region_vars.push(rid);
97 rid
98 }
99
100 pub fn push_upvar_region(&mut self) -> RegionId {
102 let region_id = self
105 .params
106 .regions
107 .push_with(|index| RegionVar { index, name: None });
108 self.by_ref_upvar_regions.push(region_id);
109 region_id
110 }
111
112 pub(crate) fn push_type_var(&mut self, rid: u32, name: String) -> TypeVarId {
113 let var_id = self.params.types.push_with(|index| TypeVar { index, name });
114 self.type_vars_map.insert(rid, var_id);
115 var_id
116 }
117
118 pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: LiteralTy, name: String) {
119 let var_id = self
120 .params
121 .const_generics
122 .push_with(|index| ConstGenericVar { index, name, ty });
123 self.const_generic_vars_map.insert(rid, var_id);
124 }
125
126 pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> {
128 assert!(
129 self.bound_region_vars.is_empty(),
130 "Trying to use two binders at the same binding level"
131 );
132 use hax::BoundVariableKind::*;
133 for p in binder.bound_vars {
134 match p {
135 Region(region) => {
136 self.push_bound_region(region);
137 }
138 Ty(_) => {
139 panic!("Unexpected locally bound type variable");
140 }
141 Const => {
142 panic!("Unexpected locally bound const generic variable");
143 }
144 }
145 }
146 Ok(())
147 }
148}
149
150impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
151 pub(crate) fn the_only_binder(&self) -> &BindingLevel {
153 assert_eq!(self.binding_levels.len(), 1);
154 self.innermost_binder()
155 }
156
157 pub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel {
159 assert_eq!(self.binding_levels.len(), 1);
160 self.innermost_binder_mut()
161 }
162
163 pub(crate) fn outermost_binder(&self) -> &BindingLevel {
164 self.binding_levels.outermost()
165 }
166
167 pub(crate) fn innermost_binder(&self) -> &BindingLevel {
168 self.binding_levels.innermost()
169 }
170
171 pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel {
172 self.binding_levels.innermost_mut()
173 }
174
175 pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams {
176 &mut self.innermost_binder_mut().params
177 }
178
179 pub(crate) fn lookup_bound_region(
180 &mut self,
181 span: Span,
182 dbid: hax::DebruijnIndex,
183 var: hax::BoundVar,
184 ) -> Result<RegionDbVar, Error> {
185 let dbid = DeBruijnId::new(dbid);
186 if let Some(rid) = self
187 .binding_levels
188 .get(dbid)
189 .and_then(|bl| bl.bound_region_vars.get(var))
190 {
191 Ok(DeBruijnVar::bound(dbid, *rid))
192 } else {
193 raise_error!(
194 self,
195 span,
196 "Unexpected error: could not find region '{dbid}_{var}"
197 )
198 }
199 }
200
201 pub(crate) fn lookup_param<Id: Copy>(
202 &mut self,
203 span: Span,
204 f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>,
205 mk_err: impl FnOnce() -> String,
206 ) -> Result<DeBruijnVar<Id>, Error> {
207 for (dbid, bl) in self.binding_levels.iter_enumerated() {
208 if let Some(id) = f(bl) {
209 return Ok(DeBruijnVar::bound(dbid, id));
210 }
211 }
212 let err = mk_err();
213 raise_error!(self, span, "Unexpected error: could not find {}", err)
214 }
215
216 pub(crate) fn lookup_early_region(
217 &mut self,
218 span: Span,
219 region: &hax::EarlyParamRegion,
220 ) -> Result<RegionDbVar, Error> {
221 self.lookup_param(
222 span,
223 |bl| bl.early_region_vars.get(region).copied(),
224 || format!("the region variable {region:?}"),
225 )
226 }
227
228 pub(crate) fn lookup_type_var(
229 &mut self,
230 span: Span,
231 param: &hax::ParamTy,
232 ) -> Result<TypeDbVar, Error> {
233 self.lookup_param(
234 span,
235 |bl| bl.type_vars_map.get(¶m.index).copied(),
236 || format!("the type variable {}", param.name),
237 )
238 }
239
240 pub(crate) fn lookup_const_generic_var(
241 &mut self,
242 span: Span,
243 param: &hax::ParamConst,
244 ) -> Result<ConstGenericDbVar, Error> {
245 self.lookup_param(
246 span,
247 |bl| bl.const_generic_vars_map.get(¶m.index).copied(),
248 || format!("the const generic variable {}", param.name),
249 )
250 }
251
252 pub(crate) fn lookup_clause_var(
253 &mut self,
254 span: Span,
255 mut id: usize,
256 ) -> Result<ClauseDbVar, Error> {
257 if self.self_clause_id.is_some() {
258 id += 1;
262 }
263 let innermost_item_binder_id = self
268 .binding_levels
269 .iter_enumerated()
270 .find(|(_, bl)| bl.is_item_binder)
271 .unwrap()
272 .0;
273 for (dbid, bl) in self.binding_levels.iter_enumerated().rev() {
275 let num_clauses_bound_at_this_level = bl.params.trait_clauses.elem_count();
276 if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id {
277 let id = TraitClauseId::from_usize(id);
278 return Ok(DeBruijnVar::bound(dbid, id));
279 } else {
280 id -= num_clauses_bound_at_this_level
281 }
282 }
283 raise_error!(
285 self,
286 span,
287 "Unexpected error: could not find clause variable {}",
288 id
289 )
290 }
291
292 pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
293 for param in &generics.params {
294 self.push_generic_param(param)?;
295 }
296 Ok(())
297 }
298
299 pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
300 match ¶m.kind {
301 hax::GenericParamDefKind::Lifetime => {
302 let region = hax::EarlyParamRegion {
303 index: param.index,
304 name: param.name.clone(),
305 };
306 let _ = self.innermost_binder_mut().push_early_region(region);
307 }
308 hax::GenericParamDefKind::Type { .. } => {
309 let _ = self
310 .innermost_binder_mut()
311 .push_type_var(param.index, param.name.clone());
312 }
313 hax::GenericParamDefKind::Const { ty, .. } => {
314 let span = self.def_span(¶m.def_id);
315 let ty = self.translate_ty(span, ty)?;
318 match ty.kind().as_literal() {
319 Some(ty) => self.innermost_binder_mut().push_const_generic_var(
320 param.index,
321 *ty,
322 param.name.clone(),
323 ),
324 None => raise_error!(
325 self,
326 span,
327 "Constant parameters of non-literal type are not supported"
328 ),
329 }
330 }
331 }
332
333 Ok(())
334 }
335
336 #[tracing::instrument(skip(self, span))]
338 fn push_generics_for_def(
339 &mut self,
340 span: Span,
341 def: &hax::FullDef,
342 is_parent: bool,
343 explicit_self_clause: bool,
344 ) -> Result<(), Error> {
345 use hax::FullDefKind::*;
346 match def.kind() {
349 AssocTy { .. }
350 | AssocFn { .. }
351 | AssocConst { .. }
352 | AnonConst { .. }
353 | InlineConst { .. }
354 | PromotedConst { .. }
355 | Closure { .. }
356 | Ctor { .. }
357 | Variant { .. } => {
358 let parent_def_id = def.parent.as_ref().unwrap();
359 let parent_def = self.t_ctx.hax_def(parent_def_id)?;
360 let explicit_self_clause = matches!(parent_def.kind(), Trait { .. });
362 self.push_generics_for_def(span, &parent_def, true, explicit_self_clause)?;
363 }
364 _ => {}
365 }
366 self.push_generics_for_def_without_parents(
367 span,
368 def,
369 !is_parent,
370 !is_parent,
371 explicit_self_clause,
372 )?;
373 Ok(())
374 }
375
376 fn push_generics_for_def_without_parents(
379 &mut self,
380 span: Span,
381 def: &hax::FullDef,
382 include_late_bound: bool,
383 include_assoc_ty_clauses: bool,
384 explicit_self_clause: bool,
385 ) -> Result<(), Error> {
386 use hax::FullDefKind;
387 if let Some(param_env) = def.param_env() {
388 self.push_generic_params(¶m_env.generics)?;
390 if let FullDefKind::Trait { self_predicate, .. } = &def.kind
392 && explicit_self_clause
393 {
394 let self_predicate =
399 RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?);
400 let clause_id =
401 self.innermost_generics_mut()
402 .trait_clauses
403 .push_with(|clause_id| TraitClause {
404 clause_id,
405 origin: PredicateOrigin::TraitSelf,
406 span: Some(span),
407 trait_: self_predicate,
408 });
409 self.self_clause_id = Some(clause_id);
411 }
412 let origin = match &def.kind {
414 FullDefKind::Struct { .. }
415 | FullDefKind::Union { .. }
416 | FullDefKind::Enum { .. }
417 | FullDefKind::TyAlias { .. }
418 | FullDefKind::AssocTy { .. } => PredicateOrigin::WhereClauseOnType,
419 FullDefKind::Fn { .. }
420 | FullDefKind::AssocFn { .. }
421 | FullDefKind::Const { .. }
422 | FullDefKind::AssocConst { .. }
423 | FullDefKind::AnonConst { .. }
424 | FullDefKind::InlineConst { .. }
425 | FullDefKind::PromotedConst { .. }
426 | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
427 FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
428 PredicateOrigin::WhereClauseOnImpl
429 }
430 FullDefKind::Trait { .. } => {
431 let _ = self.register_trait_decl_id(span, &def.def_id);
432 PredicateOrigin::WhereClauseOnTrait
433 }
434 _ => panic!("Unexpected def: {def:?}"),
435 };
436 self.register_predicates(
437 ¶m_env.predicates,
438 origin.clone(),
439 &PredicateLocation::Base,
440 )?;
441 if let FullDefKind::Trait {
443 implied_predicates, ..
444 }
445 | FullDefKind::AssocTy {
446 implied_predicates, ..
447 } = &def.kind
448 {
449 self.register_predicates(implied_predicates, origin, &PredicateLocation::Parent)?;
450 }
451
452 if let hax::FullDefKind::Trait { items, .. } = &def.kind
453 && include_assoc_ty_clauses
454 {
455 for (item, item_def) in items {
459 if let hax::FullDefKind::AssocTy {
460 param_env,
461 implied_predicates,
462 ..
463 } = &item_def.kind
464 && param_env.generics.params.is_empty()
465 {
466 let name = TraitItemName(item.name.clone());
467 self.register_predicates(
468 &implied_predicates,
469 PredicateOrigin::TraitItem(name.clone()),
470 &PredicateLocation::Item(name),
471 )?;
472 }
473 }
474 }
475 }
476
477 if let hax::FullDefKind::Closure { args, .. } = def.kind()
478 && include_late_bound
479 {
480 args.upvar_tys.iter().for_each(|ty| {
482 if matches!(
483 ty.kind(),
484 hax::TyKind::Ref(
485 hax::Region {
486 kind: hax::RegionKind::ReErased
487 },
488 ..
489 )
490 ) {
491 self.the_only_binder_mut().push_upvar_region();
492 }
493 });
494 }
495
496 let signature = match &def.kind {
505 hax::FullDefKind::Fn { sig, .. } => Some(sig),
506 hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
507 _ => None,
508 };
509 if let Some(signature) = signature
510 && include_late_bound
511 {
512 let innermost_binder = self.innermost_binder_mut();
513 assert!(innermost_binder.bound_region_vars.is_empty());
514 innermost_binder.push_params_from_binder(signature.rebind(()))?;
515 }
516
517 Ok(())
518 }
519
520 pub(crate) fn translate_def_generics(
522 &mut self,
523 span: Span,
524 def: &hax::FullDef,
525 ) -> Result<(), Error> {
526 assert!(self.binding_levels.len() == 0);
527 self.binding_levels.push(BindingLevel::new(true));
528 self.push_generics_for_def(span, def, false, false)?;
529 self.innermost_binder_mut().params.check_consistency();
530 Ok(())
531 }
532
533 pub(crate) fn translate_def_generics_without_parents(
535 &mut self,
536 span: Span,
537 def: &hax::FullDef,
538 ) -> Result<(), Error> {
539 self.binding_levels.push(BindingLevel::new(true));
540 self.push_generics_for_def_without_parents(span, def, true, true, false)?;
541 self.innermost_binder().params.check_consistency();
542 Ok(())
543 }
544
545 pub(crate) fn translate_binder_for_def<F, U>(
548 &mut self,
549 span: Span,
550 kind: BinderKind,
551 def: &hax::FullDef,
552 f: F,
553 ) -> Result<Binder<U>, Error>
554 where
555 F: FnOnce(&mut Self) -> Result<U, Error>,
556 {
557 assert!(!self.binding_levels.is_empty());
558
559 self.translate_def_generics_without_parents(span, def)?;
561
562 let res = f(self);
564
565 let params = self.binding_levels.pop().unwrap().params;
567
568 res.map(|skip_binder| Binder {
570 kind,
571 params,
572 skip_binder,
573 })
574 }
575
576 pub(crate) fn translate_region_binder<F, T, U>(
580 &mut self,
581 _span: Span,
582 binder: &hax::Binder<T>,
583 f: F,
584 ) -> Result<RegionBinder<U>, Error>
585 where
586 F: FnOnce(&mut Self, &T) -> Result<U, Error>,
587 {
588 assert!(!self.binding_levels.is_empty());
589
590 let mut binding_level = BindingLevel::new(false);
592 binding_level.push_params_from_binder(binder.rebind(()))?;
593 self.binding_levels.push(binding_level);
594
595 let res = f(self, binder.hax_skip_binder_ref());
597
598 let regions = self.binding_levels.pop().unwrap().params.regions;
600
601 res.map(|skip_binder| RegionBinder {
603 regions,
604 skip_binder,
605 })
606 }
607
608 pub(crate) fn into_generics(mut self) -> GenericParams {
609 assert!(self.binding_levels.len() == 1);
610 self.binding_levels.pop().unwrap().params
611 }
612}