Struct BindingLevel 

pub(crate) struct BindingLevel<'tcx> {

    pub is_hax_binder: bool,
    pub def_id: Option<DefId>,
    pub late_bound_scope_alias: Option<DefId>,
    pub params: GenericParams,
    pub early_region_vars: FxHashMap<EarlyParamRegion, RegionId>,
    pub region_vars_by_def_id: FxHashMap<DefId, RegionId>,
    pub bound_region_vars: Vec<RegionId>,
    pub closure_extra_self_regions: FxHashMap<PlaceholderRegion, RegionId>,
    pub closure_call_method_region: Option<RegionId>,
    pub drop_glue_region: Option<RegionId>,
    pub type_vars_map: FxHashMap<u32, Ty>,
    pub const_generic_vars_map: FxHashMap<u32, ConstGenericVarId>,
    pub trait_preds: FxHashMap<GenericPredicateId, (TraitClauseId, usize)>,
    pub used_region_names: FxHashSet<Symbol>,
    pub type_trans_cache: FxHashMap<Ty<'tcx>, Ty>,
}

A level of binding for type-level variables. Each item has a top-level binding level corresponding to the parameters and clauses to the items. We may then encounter inner binding levels in the following cases:

• for<..> binders in predicates;
• fn<..> function pointer types;
• dyn Trait types, represented as dyn<T: Trait>;
• types in a trait declaration or implementation block;
• methods in a trait declaration or implementation block.

At each level, we store two things: a GenericParams that contains the parameters bound at this level, and various maps from the rustc-internal indices to our indices.

Fields

is_hax_binder: bool

Whether this binding level exists in Hax’s De Bruijn indices. dyn Trait introduces an existential binder in Charon that has no corresponding binder in rustc/Hax.

def_id: Option<DefId>

The definition whose generics this binding level contains, if this is an item binder.

late_bound_scope_alias: Option<DefId>

Dummy rustc DefId that we use to liberate_bound_regions for our synthetic fn pointer items.

params: GenericParams

The parameters and predicates bound at this level.

early_region_vars: FxHashMap<EarlyParamRegion, RegionId>

Rust makes the distinction between early and late-bound region parameters. We do not make this distinction, and merge early and late bound regions. For details, see: https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/ https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/

The map from rust early regions to translated region indices.

region_vars_by_def_id: FxHashMap<DefId, RegionId>

The map from rust named region parameter ids to translated region indices.

bound_region_vars: Vec<RegionId>

The map from rust late/bound regions to translated region indices.

closure_extra_self_regions: FxHashMap<PlaceholderRegion, RegionId>

Extra lifetimes unerased from the closure arguments. Hax represents them with placeholder regions; they are parameters of the closure struct.

closure_call_method_region: Option<RegionId>

Region added for the lifetime bound in the signature of the call/call_mut methods.

drop_glue_region: Option<RegionId>

Region added for the borrow accepted by a drop glue method or vtable drop shim.

type_vars_map: FxHashMap<u32, Ty>

The map from rust type variable indices to the value they take in this scope. Ordinary parameters map to type variables; inference-only parameters map to their known types.

const_generic_vars_map: FxHashMap<u32, ConstGenericVarId>

The map from rust const generic variables to translated const generic variable indices.

trait_preds: FxHashMap<GenericPredicateId, (TraitClauseId, usize)>

The map from trait predicates to the translated trait clause indices, and the number of bound higher-kinded regions.

used_region_names: FxHashSet<Symbol>

RPITIT can cause region names to be reused. To avoid clashes in our output, we rename duplicate names.

type_trans_cache: FxHashMap<Ty<'tcx>, Ty>

Cache the translation of types. This harnesses the deduplication of Ty that hax does.

Implementations

impl<'tcx> BindingLevel<'tcx>

pub(crate) fn new(def_id: Option<DefId>) -> Self

pub(crate) fn new_dyn() -> Self

pub(crate) fn push_early_region( &mut self, region: EarlyParamRegion, def_id: DefId, variance: Variance, mutability: LifetimeMutability, ) -> RegionId

Important: we must push all the early-bound regions before pushing any other region.

pub(crate) fn push_bound_region( &mut self, region: BoundRegionKind, variance: Variance, ) -> RegionId

Important: we must push all the early-bound regions before pushing any other region.

pub fn push_unerased_region(&mut self, region: PlaceholderRegion)

Extra lifetimes unerased from the closure arguments. Hax represents them with placeholder regions; they are parameters of the closure struct.

pub fn push_drop_glue_region(&mut self) -> RegionId

pub(crate) fn push_type_var( &mut self, rid: u32, name: Symbol, variance: Variance, ) -> TypeVarId

pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: Ty, name: Symbol)

pub(crate) fn push_params_from_binder( &mut self, binder: Binder<()>, ) -> Result<(), Error>

Translate a binder of regions by appending the stored reguions to the given vector.

Trait Implementations

impl<'tcx> Debug for BindingLevel<'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'tcx> Default for BindingLevel<'tcx>

fn default() -> BindingLevel<'tcx>

Returns the “default value” for a type.