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        let var_id = self.params.types.push_with(|index| TypeParam {
115            index,
116            name: name.to_string(),
117        });
118        self.type_vars_map.insert(rid, var_id);
119        var_id
120    }
121
122    pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: Ty, name: hax::Symbol) {
123        let var_id = self
124            .params
125            .const_generics
126            .push_with(|index| ConstGenericParam {
127                index,
128                name: name.to_string(),
129                ty,
130            });
131        self.const_generic_vars_map.insert(rid, var_id);
132    }
133
134    /// Translate a binder of regions by appending the stored reguions to the given vector.
135    pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> {
136        assert!(
137            self.bound_region_vars.is_empty(),
138            "Trying to use two binders at the same binding level"
139        );
140        use hax::BoundVariableKind::*;
141        for p in binder.bound_vars {
142            match p {
143                Region(region) => {
144                    self.push_bound_region(region);
145                }
146                Ty(_) => {
147                    panic!("Unexpected locally bound type variable");
148                }
149                Const => {
150                    panic!("Unexpected locally bound const generic variable");
151                }
152            }
153        }
154        Ok(())
155    }
156}
157
158impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
159    /// Get the only binding level. Panics if there are other binding levels.
160    pub(crate) fn the_only_binder(&self) -> &BindingLevel {
161        assert_eq!(self.binding_levels.len(), 1);
162        self.innermost_binder()
163    }
164    /// Get the only binding level. Panics if there are other binding levels.
165    pub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel {
166        assert_eq!(self.binding_levels.len(), 1);
167        self.innermost_binder_mut()
168    }
169
170    pub(crate) fn outermost_binder(&self) -> &BindingLevel {
171        self.binding_levels.outermost()
172    }
173    pub(crate) fn outermost_binder_mut(&mut self) -> &mut BindingLevel {
174        self.binding_levels.outermost_mut()
175    }
176    pub(crate) fn innermost_binder(&self) -> &BindingLevel {
177        self.binding_levels.innermost()
178    }
179    pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel {
180        self.binding_levels.innermost_mut()
181    }
182
183    pub(crate) fn outermost_generics(&self) -> &GenericParams {
184        &self.outermost_binder().params
185    }
186    #[expect(dead_code)]
187    pub(crate) fn outermost_generics_mut(&mut self) -> &mut GenericParams {
188        &mut self.outermost_binder_mut().params
189    }
190    pub(crate) fn innermost_generics(&self) -> &GenericParams {
191        &self.innermost_binder().params
192    }
193    pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams {
194        &mut self.innermost_binder_mut().params
195    }
196
197    pub(crate) fn lookup_bound_region(
198        &mut self,
199        span: Span,
200        dbid: hax::DebruijnIndex,
201        var: hax::BoundVar,
202    ) -> Result<RegionDbVar, Error> {
203        let dbid = DeBruijnId::new(dbid);
204        if let Some(rid) = self
205            .binding_levels
206            .get(dbid)
207            .and_then(|bl| bl.bound_region_vars.get(var))
208        {
209            Ok(DeBruijnVar::bound(dbid, *rid))
210        } else {
211            raise_error!(
212                self,
213                span,
214                "Unexpected error: could not find region '{dbid}_{var}"
215            )
216        }
217    }
218
219    pub(crate) fn lookup_param<Id: Copy>(
220        &mut self,
221        span: Span,
222        f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>,
223        mk_err: impl FnOnce() -> String,
224    ) -> Result<DeBruijnVar<Id>, Error> {
225        for (dbid, bl) in self.binding_levels.iter_enumerated() {
226            if let Some(id) = f(bl) {
227                return Ok(DeBruijnVar::bound(dbid, id));
228            }
229        }
230        let err = mk_err();
231        raise_error!(self, span, "Unexpected error: could not find {}", err)
232    }
233
234    pub(crate) fn lookup_early_region(
235        &mut self,
236        span: Span,
237        region: &hax::EarlyParamRegion,
238    ) -> Result<RegionDbVar, Error> {
239        self.lookup_param(
240            span,
241            |bl| bl.early_region_vars.get(region).copied(),
242            || format!("the region variable {region:?}"),
243        )
244    }
245
246    pub(crate) fn lookup_type_var(
247        &mut self,
248        span: Span,
249        param: &hax::ParamTy,
250    ) -> Result<TypeDbVar, Error> {
251        self.lookup_param(
252            span,
253            |bl| bl.type_vars_map.get(&param.index).copied(),
254            || format!("the type variable {}", param.name),
255        )
256    }
257
258    pub(crate) fn lookup_const_generic_var(
259        &mut self,
260        span: Span,
261        param: &hax::ParamConst,
262    ) -> Result<ConstGenericDbVar, Error> {
263        self.lookup_param(
264            span,
265            |bl| bl.const_generic_vars_map.get(&param.index).copied(),
266            || format!("the const generic variable {}", param.name),
267        )
268    }
269
270    pub(crate) fn lookup_clause_var(
271        &mut self,
272        span: Span,
273        mut id: usize,
274    ) -> Result<ClauseDbVar, Error> {
275        // The clause indices returned by hax count clauses in order, starting from the parentmost.
276        // While adding clauses to a binding level we already need to translate types and clauses,
277        // so the innermost item binder may not have all the clauses yet. Hence for that binder we
278        // ignore the clause count.
279        let innermost_item_binder_id = self
280            .binding_levels
281            .iter_enumerated()
282            .find(|(_, bl)| bl.is_item_binder)
283            .unwrap()
284            .0;
285        // Iterate over the binders, starting from the outermost.
286        for (dbid, bl) in self.binding_levels.iter_enumerated().rev() {
287            let num_clauses_bound_at_this_level = bl.params.trait_clauses.elem_count();
288            if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id {
289                let id = TraitClauseId::from_usize(id);
290                return Ok(DeBruijnVar::bound(dbid, id));
291            } else {
292                id -= num_clauses_bound_at_this_level
293            }
294        }
295        // Actually unreachable
296        raise_error!(
297            self,
298            span,
299            "Unexpected error: could not find clause variable {}",
300            id
301        )
302    }
303
304    pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
305        for param in &generics.params {
306            self.push_generic_param(param)?;
307        }
308        Ok(())
309    }
310
311    pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
312        match &param.kind {
313            hax::GenericParamDefKind::Lifetime => {
314                let region = hax::EarlyParamRegion {
315                    index: param.index,
316                    name: param.name.clone(),
317                };
318                let _ = self.innermost_binder_mut().push_early_region(region);
319            }
320            hax::GenericParamDefKind::Type { .. } => {
321                let _ = self
322                    .innermost_binder_mut()
323                    .push_type_var(param.index, param.name);
324            }
325            hax::GenericParamDefKind::Const { ty, .. } => {
326                let span = self.def_span(&param.def_id);
327                // The type should be primitive, meaning it shouldn't contain variables,
328                // non-primitive adts, etc. As a result, we can use an empty context.
329                let ty = self.translate_ty(span, ty)?;
330                self.innermost_binder_mut()
331                    .push_const_generic_var(param.index, ty, param.name);
332            }
333        }
334
335        Ok(())
336    }
337
338    // The parameters (and in particular the lifetimes) are split between
339    // early bound and late bound parameters. See those blog posts for explanations:
340    // https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
341    // https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
342    // Note that only lifetimes can be late bound at the moment.
343    //
344    // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound parameters
345    // here.
346    fn push_late_bound_generics_for_def(
347        &mut self,
348        _span: Span,
349        def: &hax::FullDef,
350    ) -> Result<(), Error> {
351        if let hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } = def.kind()
352        {
353            let innermost_binder = self.innermost_binder_mut();
354            assert!(innermost_binder.bound_region_vars.is_empty());
355            innermost_binder.push_params_from_binder(sig.rebind(()))?;
356        }
357        Ok(())
358    }
359
360    /// Add the generics and predicates of this item and its parents to the current context.
361    #[tracing::instrument(skip(self, span))]
362    fn push_generics_for_def(&mut self, span: Span, def: &hax::FullDef) -> Result<(), Error> {
363        // Add generics from the parent item, recursively (recursivity is important for closures,
364        // as they can be nested).
365        if let Some(parent_item) = def.typing_parent(self.hax_state()) {
366            let parent_def = self.hax_def(&parent_item)?;
367            self.push_generics_for_def(span, &parent_def)?;
368        }
369        self.push_generics_for_def_without_parents(span, def)?;
370        Ok(())
371    }
372
373    /// Add the generics and predicates of this item. This does not include the parent generics;
374    /// use `push_generics_for_def` to get the full list.
375    fn push_generics_for_def_without_parents(
376        &mut self,
377        _span: Span,
378        def: &hax::FullDef,
379    ) -> Result<(), Error> {
380        use hax::FullDefKind;
381        if let Some(param_env) = def.param_env() {
382            // Add the generic params.
383            self.push_generic_params(&param_env.generics)?;
384            // Add the predicates.
385            let origin = match &def.kind {
386                FullDefKind::Adt { .. }
387                | FullDefKind::TyAlias { .. }
388                | FullDefKind::AssocTy { .. } => PredicateOrigin::WhereClauseOnType,
389                FullDefKind::Fn { .. }
390                | FullDefKind::AssocFn { .. }
391                | FullDefKind::Closure { .. }
392                | FullDefKind::Const { .. }
393                | FullDefKind::AssocConst { .. }
394                | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
395                FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
396                    PredicateOrigin::WhereClauseOnImpl
397                }
398                FullDefKind::Trait { .. } | FullDefKind::TraitAlias { .. } => {
399                    PredicateOrigin::WhereClauseOnTrait
400                }
401                _ => panic!("Unexpected def: {:?}", def.def_id().kind),
402            };
403            self.register_predicates(&param_env.predicates, origin.clone())?;
404        }
405
406        Ok(())
407    }
408
409    /// Translate the generics and predicates of this item and its parents. This adds generic
410    /// parameters and predicates to the current environment (as a binder in
411    /// `self.binding_levels`). The constructed `GenericParams` can be recovered at the end using
412    /// `self.into_generics()` and stored in the translated item.
413    ///
414    /// On top of the generics introduced by `push_generics_for_def`, this adds extra parameters
415    /// required by the `TransItemSourceKind`.
416    pub fn translate_item_generics(
417        &mut self,
418        span: Span,
419        def: &hax::FullDef,
420        kind: &TransItemSourceKind,
421    ) -> Result<(), Error> {
422        assert!(self.binding_levels.len() == 0);
423        self.binding_levels.push(BindingLevel::new(true));
424        self.push_generics_for_def(span, def)?;
425        self.push_late_bound_generics_for_def(span, def)?;
426
427        if let hax::FullDefKind::Closure { args, .. } = def.kind() {
428            // Add the lifetime generics coming from the upvars. We translate the upvar types early
429            // to know what lifetimes are needed.
430            let closure_upvar_tys = self.translate_closure_upvar_tys(span, args)?;
431            self.the_only_binder_mut().closure_upvar_tys = Some(closure_upvar_tys);
432            // Add the lifetime generics coming from the higher-kindedness of the signature.
433            if let TransItemSourceKind::TraitImpl(TraitImplSource::Closure(..))
434            | TransItemSourceKind::ClosureMethod(..)
435            | TransItemSourceKind::ClosureAsFnCast = kind
436            {
437                self.the_only_binder_mut()
438                    .push_params_from_binder(args.fn_sig.rebind(()))?;
439            }
440            if let TransItemSourceKind::ClosureMethod(ClosureKind::Fn | ClosureKind::FnMut) = kind {
441                // Add the lifetime generics coming from the method itself.
442                let rid = self
443                    .the_only_binder_mut()
444                    .params
445                    .regions
446                    .push_with(|index| RegionParam { index, name: None });
447                self.the_only_binder_mut().closure_call_method_region = Some(rid);
448            }
449        }
450
451        self.innermost_binder_mut().params.check_consistency();
452        Ok(())
453    }
454
455    /// Push a new binding level, run the provided function inside it, then return the bound value.
456    pub(crate) fn inside_binder<F, U>(
457        &mut self,
458        kind: BinderKind,
459        is_item_binder: bool,
460        f: F,
461    ) -> Result<Binder<U>, Error>
462    where
463        F: FnOnce(&mut Self) -> Result<U, Error>,
464    {
465        assert!(!self.binding_levels.is_empty());
466        self.binding_levels.push(BindingLevel::new(is_item_binder));
467
468        // Call the continuation. Important: do not short-circuit on error here.
469        let res = f(self);
470
471        // Reset
472        let params = self.binding_levels.pop().unwrap().params;
473
474        // Return
475        res.map(|skip_binder| Binder {
476            kind,
477            params,
478            skip_binder,
479        })
480    }
481
482    /// Push a new binding level corresponding to the provided `def` for the duration of the inner
483    /// function call.
484    pub(crate) fn translate_binder_for_def<F, U>(
485        &mut self,
486        span: Span,
487        kind: BinderKind,
488        def: &hax::FullDef,
489        f: F,
490    ) -> Result<Binder<U>, Error>
491    where
492        F: FnOnce(&mut Self) -> Result<U, Error>,
493    {
494        self.inside_binder(kind, true, |this| {
495            this.push_generics_for_def_without_parents(span, def)?;
496            this.push_late_bound_generics_for_def(span, def)?;
497            this.innermost_binder().params.check_consistency();
498            f(this)
499        })
500    }
501
502    /// Push a group of bound regions and call the continuation.
503    /// We use this when diving into a `for<'a>`, or inside an arrow type (because
504    /// it contains universally quantified regions).
505    pub(crate) fn translate_region_binder<F, T, U>(
506        &mut self,
507        _span: Span,
508        binder: &hax::Binder<T>,
509        f: F,
510    ) -> Result<RegionBinder<U>, Error>
511    where
512        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
513    {
514        let binder = self.inside_binder(BinderKind::Other, false, |this| {
515            this.innermost_binder_mut()
516                .push_params_from_binder(binder.rebind(()))?;
517            f(this, binder.hax_skip_binder_ref())
518        })?;
519        // Convert to a region-only binder.
520        Ok(RegionBinder {
521            regions: binder.params.regions,
522            skip_binder: binder.skip_binder,
523        })
524    }
525
526    pub(crate) fn into_generics(mut self) -> GenericParams {
527        assert!(self.binding_levels.len() == 1);
528        self.binding_levels.pop().unwrap().params
529    }
530}
charon_driver/translate/translate_generics.rs

charon_driver/translate/
translate_generics.rs
