charon_lib/ast/
type_level.rs

1use derive_generic_visitor::*;
2use itertools::Itertools;
3use serde_state::{DeserializeState, SerializeState};
4use std::{collections::HashSet, mem};
5
6use crate::ast::*;
7
8pub mod regions;
9pub mod substitute;
10pub mod trait_proofs;
11pub mod type_info;
12pub mod types;
13pub mod vars;
14
15pub use regions::*;
16pub use substitute::*;
17pub use trait_proofs::*;
18pub use type_info::*;
19pub use types::*;
20pub use vars::*;
21
22/// A set of generic arguments.
23#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
24#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
25pub struct GenericArgs {
26    pub regions: IndexVec<RegionId, Region>,
27    pub types: IndexVec<TypeVarId, Ty>,
28    pub const_generics: IndexVec<ConstGenericVarId, ConstantExpr>,
29    pub trait_refs: IndexVec<TraitClauseId, PolyTraitRef>,
30}
31
32/// Region arguments used to instantiate a [`RegionBinder`].
33#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
34#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
35pub struct RegionArgs {
36    pub regions: IndexVec<RegionId, Region>,
37}
38
39/// A quantified trait predicate, e.g. `for<'a> Type<'a>: Trait<'a, Args>`.
40pub type PolyTraitDeclRef = RegionBinder<TraitDeclRef>;
41
42/// .0 outlives .1
43#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
44#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
45pub struct OutlivesPred<T, U>(pub T, pub U);
46
47pub type RegionOutlives = OutlivesPred<Region, Region>;
48pub type TypeOutlives = OutlivesPred<Ty, Region>;
49pub type PolyRegionOutlives = RegionBinder<RegionOutlives>;
50pub type PolyTypeOutlives = RegionBinder<TypeOutlives>;
51
52/// A constraint over a trait associated type.
53///
54/// Example:
55/// ```text
56/// T : Foo<S = String>
57///         ^^^^^^^^^^
58/// ```
59#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
60#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
61pub struct TraitTypeConstraint {
62    pub trait_ref: TraitRef,
63    pub type_id: AssocTypeId,
64    pub ty: Ty,
65}
66
67pub type BoxedArgs = Box<GenericArgs>;
68
69/// Generic parameters for a declaration, including predicates.
70#[derive(Default, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
71#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
72pub struct GenericParams {
73    #[serde_state(stateless)]
74    pub regions: IndexVec<RegionId, RegionParam>,
75    #[serde_state(stateless)]
76    pub types: IndexVec<TypeVarId, TypeParam>,
77    pub const_generics: IndexVec<ConstGenericVarId, ConstGenericParam>,
78    // TODO: rename to match [GenericArgs]?
79    pub trait_clauses: IndexVec<TraitClauseId, TraitParam>,
80    /// The first region in the pair outlives the second region
81    pub regions_outlive: Vec<PolyRegionOutlives>,
82    /// The type outlives the region
83    pub types_outlive: Vec<PolyTypeOutlives>,
84    /// Constraints over trait associated types
85    pub trait_type_constraints: IndexVec<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
86}
87
88#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
89#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
90#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("BK"))]
91pub enum BinderKind {
92    /// The parameters of a generic associated type.
93    TraitType(TraitDeclId, AssocTypeId),
94    /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
95    /// impls.
96    TraitMethod(TraitDeclId, TraitMethodId),
97    /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
98    InherentImplBlock,
99    /// Binder used for `dyn Trait` existential predicates.
100    Dyn,
101    /// Some other use of a binder outside the main Charon ast.
102    Other,
103}
104
105/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
106/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
107/// now), trait methods, GATs (TODO).
108#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
109#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
110pub struct Binder<T> {
111    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_params"))]
112    pub params: GenericParams,
113    /// Named this way to highlight accesses to the inner value that might be handling parameters
114    /// incorrectly. Prefer using helper methods.
115    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_value"))]
116    pub skip_binder: T,
117    /// The kind of binder this is.
118    #[cfg_attr(feature = "charon_on_charon", charon::opaque)]
119    pub kind: BinderKind,
120}
121
122/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
123/// issues in the derived ocaml visitors.
124#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
125#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
126#[serde_state(state_implements = DedupSerializerState)] // Avoid corecursive impls due to perfect derive
127pub struct RegionBinder<T> {
128    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_regions"))]
129    #[serde_state(stateless)]
130    pub regions: IndexVec<RegionId, RegionParam>,
131    /// Outlives relations involving the bound regions.
132    pub regions_outlive: Vec<PolyRegionOutlives>,
133    /// Outlives relations involving the bound regions.
134    pub types_outlive: Vec<PolyTypeOutlives>,
135    /// Named this way to highlight accesses to the inner value that might be handling parameters
136    /// incorrectly. Prefer using helper methods.
137    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_value"))]
138    pub skip_binder: T,
139}
140
141impl GenericArgs {
142    pub fn len(&self) -> usize {
143        let GenericArgs {
144            regions,
145            types,
146            const_generics,
147            trait_refs,
148        } = self;
149        regions.len() + types.len() + const_generics.len() + trait_refs.len()
150    }
151
152    pub fn is_empty(&self) -> bool {
153        self.len() == 0
154    }
155    /// Whether this has any explicit arguments (types, regions or const generics).
156    pub fn has_explicits(&self) -> bool {
157        !self.regions.is_empty() || !self.types.is_empty() || !self.const_generics.is_empty()
158    }
159    /// Whether this has any implicit arguments (trait refs).
160    pub fn has_implicits(&self) -> bool {
161        !self.trait_refs.is_empty()
162    }
163
164    pub fn empty() -> Self {
165        GenericArgs {
166            regions: Default::default(),
167            types: Default::default(),
168            const_generics: Default::default(),
169            trait_refs: Default::default(),
170        }
171    }
172
173    pub fn new(
174        regions: IndexVec<RegionId, Region>,
175        types: IndexVec<TypeVarId, Ty>,
176        const_generics: IndexVec<ConstGenericVarId, ConstantExpr>,
177        trait_refs: IndexVec<TraitClauseId, PolyTraitRef>,
178    ) -> Self {
179        Self {
180            regions,
181            types,
182            const_generics,
183            trait_refs,
184        }
185    }
186    pub fn new_types(types: IndexVec<TypeVarId, Ty>) -> Self {
187        Self {
188            types,
189            ..Self::empty()
190        }
191    }
192    pub fn new_lifetimes(regions: IndexVec<RegionId, Region>) -> Self {
193        Self {
194            regions,
195            ..Self::empty()
196        }
197    }
198
199    /// Check whether this matches the given `GenericParams`.
200    /// TODO: check more things, e.g. that the trait refs use the correct trait and generics.
201    pub fn matches(&self, params: &GenericParams) -> bool {
202        params.regions.len() == self.regions.len()
203            && params.types.len() == self.types.len()
204            && params.const_generics.len() == self.const_generics.len()
205            && params.trait_clauses.len() == self.trait_refs.len()
206    }
207
208    /// Return the same generics, but where we pop the first type arguments.
209    /// This is useful for trait references (for pretty printing for instance),
210    /// because the first type argument is the type for which the trait is
211    /// implemented.
212    pub fn pop_first_type_arg(&self) -> (Ty, Self) {
213        let mut generics = self.clone();
214        let mut it = mem::take(&mut generics.types).into_iter();
215        let ty = it.next().unwrap();
216        generics.types = it.collect();
217        (ty, generics)
218    }
219
220    /// Concatenate this set of arguments with another one. Use with care, you must manage the
221    /// order of arguments correctly.
222    pub fn concat(mut self, other: &Self) -> Self {
223        let Self {
224            regions,
225            types,
226            const_generics,
227            trait_refs,
228        } = other;
229        self.regions.clone_extend_from_other(regions);
230        self.types.clone_extend_from_other(types);
231        self.const_generics.clone_extend_from_other(const_generics);
232        self.trait_refs.clone_extend_from_other(trait_refs);
233        self
234    }
235}
236
237impl RegionArgs {
238    pub fn empty() -> Self {
239        Self {
240            regions: Default::default(),
241        }
242    }
243
244    pub fn erased(len: usize) -> Self {
245        Self::new(std::iter::repeat_n(Region::Erased, len).collect())
246    }
247
248    pub fn new(regions: IndexVec<RegionId, Region>) -> Self {
249        Self { regions }
250    }
251
252    pub fn iter(&self) -> impl DoubleEndedIterator<Item = &Region> + ExactSizeIterator {
253        self.regions.iter()
254    }
255
256    pub fn is_empty(&self) -> bool {
257        self.regions.is_empty()
258    }
259}
260
261impl GenericParams {
262    pub fn empty() -> Self {
263        Self::default()
264    }
265
266    pub fn is_empty(&self) -> bool {
267        self.len() == 0
268    }
269    /// Whether this has any explicit arguments (types, regions or const generics).
270    pub fn has_explicits(&self) -> bool {
271        !self.regions.is_empty() || !self.types.is_empty() || !self.const_generics.is_empty()
272    }
273    /// Whether this has any implicit arguments (trait clauses, outlives relations, associated type
274    /// equality constraints).
275    pub fn has_predicates(&self) -> bool {
276        !self.trait_clauses.is_empty()
277            || !self.types_outlive.is_empty()
278            || !self.regions_outlive.is_empty()
279            || !self.trait_type_constraints.is_empty()
280    }
281
282    /// Run some sanity checks.
283    pub fn check_consistency(&self) {
284        // Sanity check: check the clause ids are consistent.
285        assert!(
286            self.trait_clauses
287                .iter()
288                .enumerate()
289                .all(|(i, c)| c.clause_id.index() == i)
290        );
291
292        // Sanity check: region names are pairwise distinct (this caused trouble when generating
293        // names for the backward functions in Aeneas): at some point, Rustc introduced names equal
294        // to `Some("'_")` for the anonymous regions, instead of using `None` (we now check in
295        // [translate_region_name] and ignore names equal to "'_").
296        let mut s = HashSet::new();
297        for r in &self.regions {
298            if let Some(name) = &r.name {
299                assert!(
300                    !s.contains(name),
301                    "Name \"{}\" reused for two different lifetimes",
302                    name
303                );
304                s.insert(name);
305            }
306        }
307    }
308
309    pub fn len(&self) -> usize {
310        let GenericParams {
311            regions,
312            types,
313            const_generics,
314            trait_clauses,
315            regions_outlive,
316            types_outlive,
317            trait_type_constraints,
318        } = self;
319        regions.len()
320            + types.len()
321            + const_generics.len()
322            + trait_clauses.len()
323            + regions_outlive.len()
324            + types_outlive.len()
325            + trait_type_constraints.len()
326    }
327
328    /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds
329    /// each required parameter with itself. E.g. given parameters for `<T, U> where U:
330    /// PartialEq<T>`, the arguments would be `<T, U>[TraitClause0]`.
331    pub fn identity_args(&self) -> GenericArgs {
332        self.identity_args_at_depth(DeBruijnId::zero())
333    }
334
335    /// Like `identity_args` but uses variables bound at the given depth.
336    pub fn identity_args_at_depth(&self, depth: DeBruijnId) -> GenericArgs {
337        GenericArgs {
338            regions: self
339                .regions
340                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::bound(depth, id))),
341            types: self
342                .types
343                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::bound(depth, id)).into_ty()),
344            const_generics: self.const_generics.map_ref_indexed(|id, c| {
345                ConstantExpr::new(
346                    ConstantExprKind::Var(DeBruijnVar::bound(depth, id)),
347                    c.ty.clone(),
348                )
349            }),
350            trait_refs: self
351                .trait_clauses
352                .map_ref(|clause| clause.identity_tref_at_depth(depth)),
353        }
354    }
355
356    /// Take the predicates from the another `GenericParams`. This assumes the clause ids etc are
357    /// already consistent.
358    pub fn take_predicates_from(&mut self, other: GenericParams) {
359        assert!(!other.has_explicits());
360        let num_clauses = self.trait_clauses.len();
361        let GenericParams {
362            regions: _,
363            types: _,
364            const_generics: _,
365            trait_clauses,
366            regions_outlive,
367            types_outlive,
368            trait_type_constraints,
369        } = other;
370        self.trait_clauses
371            .extend(trait_clauses.into_iter().update(|clause| {
372                clause.clause_id += num_clauses;
373            }));
374        self.regions_outlive.extend(regions_outlive);
375        self.types_outlive.extend(types_outlive);
376        self.trait_type_constraints.extend(trait_type_constraints);
377    }
378
379    /// Take the predicates from the another `GenericParams`. This assumes that the two
380    /// `GenericParams` are independent, hence will shift clause ids if `other` has any
381    /// trait refs that reference its own clauses.
382    pub fn merge_predicates_from(&mut self, mut other: GenericParams) {
383        // Drop the explicits params.
384        other.types.clear();
385        other.regions.clear();
386        other.const_generics.clear();
387        // The contents of `other` may refer to its own trait clauses, so we must shift clause ids.
388        struct ShiftClausesVisitor(usize);
389        impl VarsVisitor for ShiftClausesVisitor {
390            fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<ClauseReplacement> {
391                if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
392                    // Replace clause 0 and decrement the others.
393                    Some(ClauseReplacement::Var(DeBruijnVar::Bound(
394                        DeBruijnId::ZERO,
395                        clause_id + self.0,
396                    )))
397                } else {
398                    None
399                }
400            }
401        }
402        let num_clauses = self.trait_clauses.len();
403        other.visit_vars(&mut ShiftClausesVisitor(num_clauses));
404        self.take_predicates_from(other);
405    }
406}
407
408impl<T> Binder<T> {
409    /// Wrap the value in an empty binder, shifting variables appropriately.
410    pub fn empty(kind: BinderKind, x: T) -> Self
411    where
412        T: TyVisitable,
413    {
414        Binder {
415            params: Default::default(),
416            skip_binder: x.move_under_binder(),
417            kind,
418        }
419    }
420    pub fn new(kind: BinderKind, params: GenericParams, skip_binder: T) -> Self {
421        Self {
422            params,
423            skip_binder,
424            kind,
425        }
426    }
427
428    /// Whether this binder binds any variables.
429    pub fn binds_anything(&self) -> bool {
430        !self.params.is_empty()
431    }
432
433    /// Retreive the contents of this binder if the binder binds no variables. This is the invers
434    /// of `Binder::empty`.
435    pub fn get_if_binds_nothing(&self) -> Option<T>
436    where
437        T: TyVisitable + Clone,
438    {
439        self.params
440            .is_empty()
441            .then(|| self.skip_binder.clone().move_from_under_binder().unwrap())
442    }
443
444    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U> {
445        Binder {
446            params: self.params,
447            skip_binder: f(self.skip_binder),
448            kind: self.kind,
449        }
450    }
451
452    pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> Binder<U> {
453        Binder {
454            params: self.params.clone(),
455            skip_binder: f(&self.skip_binder),
456            kind: self.kind.clone(),
457        }
458    }
459
460    /// Substitute the provided arguments for the variables bound in this binder and return the
461    /// substituted inner value.
462    pub fn apply(self, args: &GenericArgs) -> T
463    where
464        T: TyVisitable,
465    {
466        self.skip_binder.substitute(args)
467    }
468
469    /// Like `apply`, but also keep the parameters: predicates mention them and therefore need to
470    /// be substituted before use too.
471    pub fn apply_keep_params(self, args: &GenericArgs) -> (GenericParams, T)
472    where
473        T: TyVisitable,
474    {
475        (
476            self.params.substitute(args),
477            self.skip_binder.substitute(args),
478        )
479    }
480}
481
482impl<T: AstVisitable> Binder<Binder<T>> {
483    /// Flatten two levels of binders into a single one.
484    pub fn flatten(self) -> Binder<T> {
485        #[derive(Visitor)]
486        struct FlattenVisitor<'a> {
487            shift_by: &'a GenericParams,
488            binder_depth: DeBruijnId,
489        }
490        impl VisitorWithBinderDepth for FlattenVisitor<'_> {
491            fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
492                &mut self.binder_depth
493            }
494        }
495        impl VisitAstMut for FlattenVisitor<'_> {
496            fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
497                VisitWithBinderDepth::new(self).visit(x)
498            }
499
500            fn enter_de_bruijn_id(&mut self, db_id: &mut DeBruijnId) {
501                if *db_id > self.binder_depth {
502                    // We started visiting at the inner binder, so in this branch we're either
503                    // mentioning the outer binder or a binder further beyond. Either way we
504                    // decrease the depth; variables that point to the outer binder don't have to
505                    // be shifted.
506                    *db_id = db_id.decr();
507                }
508            }
509            fn enter_region(&mut self, x: &mut Region) {
510                if let Region::Var(var) = x
511                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
512                {
513                    *id += self.shift_by.regions.len();
514                }
515            }
516            fn enter_ty_kind(&mut self, x: &mut TyKind) {
517                if let TyKind::TypeVar(var) = x
518                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
519                {
520                    *id += self.shift_by.types.len();
521                }
522            }
523            fn enter_constant_expr_kind(&mut self, kind: &mut ConstantExprKind) {
524                if let ConstantExprKind::Var(var) = kind
525                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
526                {
527                    *id += self.shift_by.const_generics.len();
528                }
529            }
530            fn enter_trait_ref_kind(&mut self, x: &mut TraitRefKind) {
531                if let TraitRefKind::Clause(var, _) = x
532                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
533                {
534                    *id += self.shift_by.trait_clauses.len();
535                }
536            }
537        }
538
539        // We will concatenate both sets of params.
540        let mut outer_params = self.params;
541
542        // The inner value needs to change:
543        // - at binder level 0 we shift all variable ids to match the concatenated params;
544        // - at binder level > 0 we decrease binding level because there's one fewer binder.
545        let mut bound_value = self.skip_binder.skip_binder;
546        let _ = bound_value.drive_mut(&mut FlattenVisitor {
547            shift_by: &outer_params,
548            binder_depth: Default::default(),
549        });
550
551        // The inner params must also be updated, as they can refer to themselves and the outer
552        // one.
553        let mut inner_params = self.skip_binder.params;
554        let _ = inner_params.drive_mut(&mut FlattenVisitor {
555            shift_by: &outer_params,
556            binder_depth: Default::default(),
557        });
558        inner_params
559            .regions
560            .iter_mut()
561            .for_each(|v| v.index += outer_params.regions.len());
562        inner_params
563            .types
564            .iter_mut()
565            .for_each(|v| v.index += outer_params.types.len());
566        inner_params
567            .const_generics
568            .iter_mut()
569            .for_each(|v| v.index += outer_params.const_generics.len());
570        inner_params
571            .trait_clauses
572            .iter_mut()
573            .for_each(|v| v.clause_id += outer_params.trait_clauses.len());
574
575        let GenericParams {
576            regions,
577            types,
578            const_generics,
579            trait_clauses,
580            regions_outlive,
581            types_outlive,
582            trait_type_constraints,
583        } = &inner_params;
584        outer_params.regions.clone_extend_from_other(regions);
585        outer_params.types.clone_extend_from_other(types);
586        outer_params
587            .const_generics
588            .clone_extend_from_other(const_generics);
589        outer_params
590            .trait_clauses
591            .clone_extend_from_other(trait_clauses);
592        outer_params
593            .regions_outlive
594            .extend_from_slice(regions_outlive);
595        outer_params.types_outlive.extend_from_slice(types_outlive);
596        outer_params
597            .trait_type_constraints
598            .clone_extend_from_other(trait_type_constraints);
599
600        Binder {
601            params: outer_params,
602            skip_binder: bound_value,
603            kind: BinderKind::Other,
604        }
605    }
606}
607
608impl<T> RegionBinder<T> {
609    /// Wrap the value in an empty region binder, shifting variables appropriately.
610    pub fn empty(x: T) -> Self
611    where
612        T: TyVisitable,
613    {
614        RegionBinder {
615            regions: Default::default(),
616            regions_outlive: Default::default(),
617            types_outlive: Default::default(),
618            skip_binder: x.move_under_binder(),
619        }
620    }
621
622    /// The parameters and predicates introduced by this binder.
623    pub fn to_params(&self) -> GenericParams {
624        GenericParams {
625            regions: self.regions.clone(),
626            regions_outlive: self.regions_outlive.clone(),
627            types_outlive: self.types_outlive.clone(),
628            ..GenericParams::default()
629        }
630    }
631
632    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> RegionBinder<U> {
633        RegionBinder {
634            regions: self.regions,
635            regions_outlive: self.regions_outlive,
636            types_outlive: self.types_outlive,
637            skip_binder: f(self.skip_binder),
638        }
639    }
640
641    pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> RegionBinder<U> {
642        RegionBinder {
643            regions: self.regions.clone(),
644            regions_outlive: self.regions_outlive.clone(),
645            types_outlive: self.types_outlive.clone(),
646            skip_binder: f(&self.skip_binder),
647        }
648    }
649
650    pub fn map_ref_opt<U>(&self, f: impl FnOnce(&T) -> Option<U>) -> Option<RegionBinder<U>> {
651        Some(RegionBinder {
652            regions: self.regions.clone(),
653            regions_outlive: self.regions_outlive.clone(),
654            types_outlive: self.types_outlive.clone(),
655            skip_binder: f(&self.skip_binder)?,
656        })
657    }
658
659    /// Substitute the bound variables with the given lifetimes.
660    pub fn apply(self, args: RegionArgs) -> T
661    where
662        T: TyVisitable,
663    {
664        assert_eq!(args.regions.len(), self.regions.len());
665        let args = GenericArgs::new_lifetimes(args.regions);
666        self.skip_binder.substitute_inner_binder(&args)
667    }
668
669    /// Like `apply`, but also keep the predicates: they mention the bound regions and therefore
670    /// need to be substituted before use too.
671    pub fn apply_keep_params(
672        self,
673        args: RegionArgs,
674    ) -> (T, Vec<PolyRegionOutlives>, Vec<PolyTypeOutlives>)
675    where
676        T: TyVisitable,
677    {
678        assert_eq!(args.regions.len(), self.regions.len());
679        let args = GenericArgs::new_lifetimes(args.regions);
680        (
681            self.skip_binder.substitute_inner_binder(&args),
682            self.regions_outlive.substitute_inner_binder(&args),
683            self.types_outlive.substitute_inner_binder(&args),
684        )
685    }
686
687    /// Extract the contents when we now the binder binds nothing.
688    #[track_caller]
689    pub fn no_bound_vars(self) -> T
690    where
691        T: TyVisitable,
692    {
693        assert!(self.regions.is_empty());
694        self.skip_binder.move_from_under_binder().unwrap()
695    }
696
697    /// Substitute the bound variables with erased lifetimes.
698    pub fn erase(self) -> T
699    where
700        T: TyVisitable,
701    {
702        let args = RegionArgs::erased(self.regions.len());
703        self.apply(args)
704    }
705}
706
707pub trait HasIdxVecOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
708    fn get_idx_vec(&self) -> &IndexVec<Id, Self::Output>;
709    fn get_idx_vec_mut(&mut self) -> &mut IndexVec<Id, Self::Output>;
710}
711
712/// Delegate `Index` implementations to subfields.
713macro_rules! mk_index_impls {
714    ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
715        impl std::ops::Index<$idx> for $ty {
716            type Output = $output;
717            fn index(&self, index: $idx) -> &Self::Output {
718                &self.$field[index]
719            }
720        }
721        impl std::ops::IndexMut<$idx> for $ty {
722            fn index_mut(&mut self, index: $idx) -> &mut Self::Output {
723                &mut self.$field[index]
724            }
725        }
726        impl HasIdxVecOf<$idx> for $ty {
727            fn get_idx_vec(&self) -> &IndexVec<$idx, Self::Output> {
728                &self.$field
729            }
730            fn get_idx_vec_mut(&mut self) -> &mut IndexVec<$idx, Self::Output> {
731                &mut self.$field
732            }
733        }
734    };
735}
736mk_index_impls!(GenericArgs.regions[RegionId]: Region);
737mk_index_impls!(GenericArgs.types[TypeVarId]: Ty);
738mk_index_impls!(GenericArgs.const_generics[ConstGenericVarId]: ConstantExpr);
739mk_index_impls!(GenericArgs.trait_refs[TraitClauseId]: PolyTraitRef);
740mk_index_impls!(GenericParams.regions[RegionId]: RegionParam);
741mk_index_impls!(GenericParams.types[TypeVarId]: TypeParam);
742mk_index_impls!(GenericParams.const_generics[ConstGenericVarId]: ConstGenericParam);
743mk_index_impls!(GenericParams.trait_clauses[TraitClauseId]: TraitParam);
744
745impl FromIterator<Region> for RegionArgs {
746    fn from_iter<T: IntoIterator<Item = Region>>(iter: T) -> Self {
747        Self::new(iter.into_iter().collect())
748    }
749}
charon_lib/ast/type_level.rs

charon_lib/ast/
type_level.rs
