charon_driver/translate/
translate_generics.rs

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

charon_driver/translate/
translate_generics.rs
