charon_driver/translate/
translate_generics.rs

1use super::translate_ctx::ItemTransCtx;
2use charon_lib::ast::*;
3use std::collections::HashMap;
4use std::fmt::Debug;
5
6/// A level of binding for type-level variables. Each item has a top-level binding level
7/// corresponding to the parameters and clauses to the items. We may then encounter inner binding
8/// levels in the following cases:
9/// - `for<..>` binders in predicates;
10/// - `fn<..>` function pointer types;
11/// - `dyn Trait` types, represented as `dyn<T: Trait>` (TODO);
12/// - types in a trait declaration or implementation block (TODO);
13/// - methods in a trait declaration or implementation block (TODO).
14///
15/// At each level, we store two things: a `GenericParams` that contains the parameters bound at
16/// this level, and various maps from the rustc-internal indices to our indices.
17#[derive(Debug, Default)]
18pub(crate) struct BindingLevel {
19    /// The parameters and predicates bound at this level.
20    pub params: GenericParams,
21    /// Whether this binder corresponds to an item (method, type) or not (`for<..>` predicate, `fn`
22    /// pointer, etc). This indicates whether it corresponds to a rustc `ParamEnv` and therefore
23    /// whether we should resolve rustc variables there.
24    pub is_item_binder: bool,
25    /// Rust makes the distinction between early and late-bound region parameters. We do not make
26    /// this distinction, and merge early and late bound regions. For details, see:
27    /// <https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/>
28    /// <https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/>
29    ///
30    /// The map from rust early regions to translated region indices.
31    pub early_region_vars: std::collections::BTreeMap<hax::EarlyParamRegion, RegionId>,
32    /// The map from rust late/bound regions to translated region indices.
33    pub bound_region_vars: Vec<RegionId>,
34    /// The regions added for by-ref upvars, in order of upvars.
35    pub by_ref_upvar_regions: Vec<RegionId>,
36    /// The map from rust type variable indices to translated type variable indices.
37    pub type_vars_map: HashMap<u32, TypeVarId>,
38    /// The map from rust const generic variables to translate const generic variable indices.
39    pub const_generic_vars_map: HashMap<u32, ConstGenericVarId>,
40    /// Cache the translation of types. This harnesses the deduplication of `Ty` that hax does.
41    // Important: we can't reuse type caches from earlier binders as the new binder may change what
42    // a given variable resolves to.
43    pub type_trans_cache: HashMap<hax::Ty, Ty>,
44}
45
46/// Small helper: we ignore some region names (when they are equal to "'_")
47fn translate_region_name(s: String) -> Option<String> {
48    if s == "'_" { None } else { Some(s) }
49}
50
51impl BindingLevel {
52    pub(crate) fn new(is_item_binder: bool) -> Self {
53        Self {
54            is_item_binder,
55            ..Default::default()
56        }
57    }
58
59    /// Important: we must push all the early-bound regions before pushing any other region.
60    pub(crate) fn push_early_region(&mut self, region: hax::EarlyParamRegion) -> RegionId {
61        let name = translate_region_name(region.name.clone());
62        // Check that there are no late-bound regions
63        assert!(
64            self.bound_region_vars.is_empty(),
65            "Early regions must be translated before late ones"
66        );
67        let rid = self
68            .params
69            .regions
70            .push_with(|index| RegionParam { index, name });
71        self.early_region_vars.insert(region, rid);
72        rid
73    }
74
75    /// Important: we must push all the early-bound regions before pushing any other region.
76    pub(crate) fn push_bound_region(&mut self, region: hax::BoundRegionKind) -> RegionId {
77        use hax::BoundRegionKind::*;
78        let name = match region {
79            Anon => None,
80            NamedAnon(symbol) | Named(_, symbol) => translate_region_name(symbol.clone()),
81            ClosureEnv => Some("@env".to_owned()),
82        };
83        let rid = self
84            .params
85            .regions
86            .push_with(|index| RegionParam { index, name });
87        self.bound_region_vars.push(rid);
88        rid
89    }
90
91    /// Add a region for a by_ref upvar in a closure.
92    pub fn push_upvar_region(&mut self) -> RegionId {
93        // We musn't push to `bound_region_vars` because that will contain the higher-kinded
94        // signature lifetimes if any and they must be lookup-able.
95        let region_id = self
96            .params
97            .regions
98            .push_with(|index| RegionParam { index, name: None });
99        self.by_ref_upvar_regions.push(region_id);
100        region_id
101    }
102
103    pub(crate) fn push_type_var(&mut self, rid: u32, name: String) -> TypeVarId {
104        let var_id = self
105            .params
106            .types
107            .push_with(|index| TypeParam { index, name });
108        self.type_vars_map.insert(rid, var_id);
109        var_id
110    }
111
112    pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: LiteralTy, name: String) {
113        let var_id = self
114            .params
115            .const_generics
116            .push_with(|index| ConstGenericParam { index, name, ty });
117        self.const_generic_vars_map.insert(rid, var_id);
118    }
119
120    /// Translate a binder of regions by appending the stored reguions to the given vector.
121    pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> {
122        assert!(
123            self.bound_region_vars.is_empty(),
124            "Trying to use two binders at the same binding level"
125        );
126        use hax::BoundVariableKind::*;
127        for p in binder.bound_vars {
128            match p {
129                Region(region) => {
130                    self.push_bound_region(region);
131                }
132                Ty(_) => {
133                    panic!("Unexpected locally bound type variable");
134                }
135                Const => {
136                    panic!("Unexpected locally bound const generic variable");
137                }
138            }
139        }
140        Ok(())
141    }
142}
143
144impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
145    /// Get the only binding level. Panics if there are other binding levels.
146    pub(crate) fn the_only_binder(&self) -> &BindingLevel {
147        assert_eq!(self.binding_levels.len(), 1);
148        self.innermost_binder()
149    }
150    /// Get the only binding level. Panics if there are other binding levels.
151    pub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel {
152        assert_eq!(self.binding_levels.len(), 1);
153        self.innermost_binder_mut()
154    }
155
156    pub(crate) fn outermost_binder(&self) -> &BindingLevel {
157        self.binding_levels.outermost()
158    }
159    pub(crate) fn outermost_binder_mut(&mut self) -> &mut BindingLevel {
160        self.binding_levels.outermost_mut()
161    }
162    pub(crate) fn innermost_binder(&self) -> &BindingLevel {
163        self.binding_levels.innermost()
164    }
165    pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel {
166        self.binding_levels.innermost_mut()
167    }
168
169    pub(crate) fn outermost_generics(&self) -> &GenericParams {
170        &self.outermost_binder().params
171    }
172    #[expect(dead_code)]
173    pub(crate) fn outermost_generics_mut(&mut self) -> &mut GenericParams {
174        &mut self.outermost_binder_mut().params
175    }
176    pub(crate) fn innermost_generics(&self) -> &GenericParams {
177        &self.innermost_binder().params
178    }
179    pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams {
180        &mut self.innermost_binder_mut().params
181    }
182
183    pub(crate) fn lookup_bound_region(
184        &mut self,
185        span: Span,
186        dbid: hax::DebruijnIndex,
187        var: hax::BoundVar,
188    ) -> Result<RegionDbVar, Error> {
189        let dbid = DeBruijnId::new(dbid);
190        if let Some(rid) = self
191            .binding_levels
192            .get(dbid)
193            .and_then(|bl| bl.bound_region_vars.get(var))
194        {
195            Ok(DeBruijnVar::bound(dbid, *rid))
196        } else {
197            raise_error!(
198                self,
199                span,
200                "Unexpected error: could not find region '{dbid}_{var}"
201            )
202        }
203    }
204
205    pub(crate) fn lookup_param<Id: Copy>(
206        &mut self,
207        span: Span,
208        f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>,
209        mk_err: impl FnOnce() -> String,
210    ) -> Result<DeBruijnVar<Id>, Error> {
211        for (dbid, bl) in self.binding_levels.iter_enumerated() {
212            if let Some(id) = f(bl) {
213                return Ok(DeBruijnVar::bound(dbid, id));
214            }
215        }
216        let err = mk_err();
217        raise_error!(self, span, "Unexpected error: could not find {}", err)
218    }
219
220    pub(crate) fn lookup_early_region(
221        &mut self,
222        span: Span,
223        region: &hax::EarlyParamRegion,
224    ) -> Result<RegionDbVar, Error> {
225        self.lookup_param(
226            span,
227            |bl| bl.early_region_vars.get(region).copied(),
228            || format!("the region variable {region:?}"),
229        )
230    }
231
232    pub(crate) fn lookup_type_var(
233        &mut self,
234        span: Span,
235        param: &hax::ParamTy,
236    ) -> Result<TypeDbVar, Error> {
237        self.lookup_param(
238            span,
239            |bl| bl.type_vars_map.get(&param.index).copied(),
240            || format!("the type variable {}", param.name),
241        )
242    }
243
244    pub(crate) fn lookup_const_generic_var(
245        &mut self,
246        span: Span,
247        param: &hax::ParamConst,
248    ) -> Result<ConstGenericDbVar, Error> {
249        self.lookup_param(
250            span,
251            |bl| bl.const_generic_vars_map.get(&param.index).copied(),
252            || format!("the const generic variable {}", param.name),
253        )
254    }
255
256    pub(crate) fn lookup_clause_var(
257        &mut self,
258        span: Span,
259        mut id: usize,
260    ) -> Result<ClauseDbVar, Error> {
261        // The clause indices returned by hax count clauses in order, starting from the parentmost.
262        // While adding clauses to a binding level we already need to translate types and clauses,
263        // so the innermost item binder may not have all the clauses yet. Hence for that binder we
264        // ignore the clause count.
265        let innermost_item_binder_id = self
266            .binding_levels
267            .iter_enumerated()
268            .find(|(_, bl)| bl.is_item_binder)
269            .unwrap()
270            .0;
271        // Iterate over the binders, starting from the outermost.
272        for (dbid, bl) in self.binding_levels.iter_enumerated().rev() {
273            let num_clauses_bound_at_this_level = bl.params.trait_clauses.elem_count();
274            if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id {
275                let id = TraitClauseId::from_usize(id);
276                return Ok(DeBruijnVar::bound(dbid, id));
277            } else {
278                id -= num_clauses_bound_at_this_level
279            }
280        }
281        // Actually unreachable
282        raise_error!(
283            self,
284            span,
285            "Unexpected error: could not find clause variable {}",
286            id
287        )
288    }
289
290    pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
291        for param in &generics.params {
292            self.push_generic_param(param)?;
293        }
294        Ok(())
295    }
296
297    pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
298        match &param.kind {
299            hax::GenericParamDefKind::Lifetime => {
300                let region = hax::EarlyParamRegion {
301                    index: param.index,
302                    name: param.name.clone(),
303                };
304                let _ = self.innermost_binder_mut().push_early_region(region);
305            }
306            hax::GenericParamDefKind::Type { .. } => {
307                let _ = self
308                    .innermost_binder_mut()
309                    .push_type_var(param.index, param.name.clone());
310            }
311            hax::GenericParamDefKind::Const { ty, .. } => {
312                let span = self.def_span(&param.def_id);
313                // The type should be primitive, meaning it shouldn't contain variables,
314                // non-primitive adts, etc. As a result, we can use an empty context.
315                let ty = self.translate_ty(span, ty)?;
316                match ty.kind().as_literal() {
317                    Some(ty) => self.innermost_binder_mut().push_const_generic_var(
318                        param.index,
319                        *ty,
320                        param.name.clone(),
321                    ),
322                    None => raise_error!(
323                        self,
324                        span,
325                        "Constant parameters of non-literal type are not supported"
326                    ),
327                }
328            }
329        }
330
331        Ok(())
332    }
333
334    /// Add the generics and predicates of this item and its parents to the current context.
335    #[tracing::instrument(skip(self, span))]
336    fn push_generics_for_def(
337        &mut self,
338        span: Span,
339        def: &hax::FullDef,
340        is_parent: bool,
341    ) -> Result<(), Error> {
342        // Add generics from the parent item, recursively (recursivity is important for closures,
343        // as they can be nested).
344        if let Some(parent_item) = def.typing_parent(self.hax_state()) {
345            let parent_def = self.hax_def(&parent_item)?;
346            self.push_generics_for_def(span, &parent_def, true)?;
347        }
348        self.push_generics_for_def_without_parents(span, def, !is_parent)?;
349        Ok(())
350    }
351
352    /// Add the generics and predicates of this item. This does not include the parent generics;
353    /// use `push_generics_for_def` to get the full list.
354    fn push_generics_for_def_without_parents(
355        &mut self,
356        _span: Span,
357        def: &hax::FullDef,
358        include_late_bound: bool,
359    ) -> Result<(), Error> {
360        use hax::FullDefKind;
361        if let Some(param_env) = def.param_env() {
362            // Add the generic params.
363            self.push_generic_params(&param_env.generics)?;
364            // Add the predicates.
365            let origin = match &def.kind {
366                FullDefKind::Adt { .. }
367                | FullDefKind::TyAlias { .. }
368                | FullDefKind::AssocTy { .. } => PredicateOrigin::WhereClauseOnType,
369                FullDefKind::Fn { .. }
370                | FullDefKind::AssocFn { .. }
371                | FullDefKind::Closure { .. }
372                | FullDefKind::Const { .. }
373                | FullDefKind::AssocConst { .. }
374                | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
375                FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
376                    PredicateOrigin::WhereClauseOnImpl
377                }
378                FullDefKind::Trait { .. } | FullDefKind::TraitAlias { .. } => {
379                    PredicateOrigin::WhereClauseOnTrait
380                }
381                _ => panic!("Unexpected def: {:?}", def.def_id().kind),
382            };
383            self.register_predicates(&param_env.predicates, origin.clone())?;
384        }
385
386        if let hax::FullDefKind::Closure { args, .. } = def.kind()
387            && include_late_bound
388        {
389            // Add the lifetime generics coming from the by-ref upvars.
390            args.iter_upvar_borrows().for_each(|_| {
391                self.the_only_binder_mut().push_upvar_region();
392            });
393        }
394
395        // The parameters (and in particular the lifetimes) are split between
396        // early bound and late bound parameters. See those blog posts for explanations:
397        // https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
398        // https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
399        // Note that only lifetimes can be late bound.
400        //
401        // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
402        // parameters here.
403        let signature = match &def.kind {
404            hax::FullDefKind::Fn { sig, .. } => Some(sig),
405            hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
406            _ => None,
407        };
408        if let Some(signature) = signature
409            && include_late_bound
410        {
411            let innermost_binder = self.innermost_binder_mut();
412            assert!(innermost_binder.bound_region_vars.is_empty());
413            innermost_binder.push_params_from_binder(signature.rebind(()))?;
414        }
415
416        Ok(())
417    }
418
419    /// Translate the generics and predicates of this item and its parents.
420    /// This adds generic parameters and predicates to the current environment (as a binder in `self.binding_levels`).
421    /// This is necessary to translate types that depend on these generics (such as `Ty` and `TraitRef`).
422    /// The constructed `GenericParams` can be recovered at the end using `self.into_generics()` and stored in the translated item.
423    pub(crate) fn translate_def_generics(
424        &mut self,
425        span: Span,
426        def: &hax::FullDef,
427    ) -> Result<(), Error> {
428        assert!(self.binding_levels.len() == 0);
429        self.binding_levels.push(BindingLevel::new(true));
430        self.push_generics_for_def(span, def, false)?;
431        self.innermost_binder_mut().params.check_consistency();
432        Ok(())
433    }
434
435    /// Translate the generics and predicates of this item without its parents.
436    pub(crate) fn translate_def_generics_without_parents(
437        &mut self,
438        span: Span,
439        def: &hax::FullDef,
440    ) -> Result<(), Error> {
441        self.binding_levels.push(BindingLevel::new(true));
442        self.push_generics_for_def_without_parents(span, def, true)?;
443        self.innermost_binder().params.check_consistency();
444        Ok(())
445    }
446
447    /// Push a new binding level corresponding to the provided `def` for the duration of the inner
448    /// function call.
449    pub(crate) fn translate_binder_for_def<F, U>(
450        &mut self,
451        span: Span,
452        kind: BinderKind,
453        def: &hax::FullDef,
454        f: F,
455    ) -> Result<Binder<U>, Error>
456    where
457        F: FnOnce(&mut Self) -> Result<U, Error>,
458    {
459        assert!(!self.binding_levels.is_empty());
460
461        // Register the type-level parameters. This pushes a new binding level.
462        self.translate_def_generics_without_parents(span, def)?;
463
464        // Call the continuation. Important: do not short-circuit on error here.
465        let res = f(self);
466
467        // Reset
468        let params = self.binding_levels.pop().unwrap().params;
469
470        // Return
471        res.map(|skip_binder| Binder {
472            kind,
473            params,
474            skip_binder,
475        })
476    }
477
478    /// Push a group of bound regions and call the continuation.
479    /// We use this when diving into a `for<'a>`, or inside an arrow type (because
480    /// it contains universally quantified regions).
481    pub(crate) fn translate_region_binder<F, T, U>(
482        &mut self,
483        _span: Span,
484        binder: &hax::Binder<T>,
485        f: F,
486    ) -> Result<RegionBinder<U>, Error>
487    where
488        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
489    {
490        assert!(!self.binding_levels.is_empty());
491
492        // Register the variables
493        let mut binding_level = BindingLevel::new(false);
494        binding_level.push_params_from_binder(binder.rebind(()))?;
495        self.binding_levels.push(binding_level);
496
497        // Call the continuation. Important: do not short-circuit on error here.
498        let res = f(self, binder.hax_skip_binder_ref());
499
500        // Reset
501        let regions = self.binding_levels.pop().unwrap().params.regions;
502
503        // Return
504        res.map(|skip_binder| RegionBinder {
505            regions,
506            skip_binder,
507        })
508    }
509
510    pub(crate) fn into_generics(mut self) -> GenericParams {
511        assert!(self.binding_levels.len() == 1);
512        self.binding_levels.pop().unwrap().params
513    }
514}
charon_driver/translate/translate_generics.rs

charon_driver/translate/
translate_generics.rs
