charon_lib/ast/
types_utils.rs

1//! This file groups everything which is linked to implementations about [crate::types]
2use crate::ast::*;
3use crate::formatter::FmtCtx;
4use crate::ids::Vector;
5use crate::pretty::FmtWithCtx;
6use derive_generic_visitor::*;
7use std::collections::HashSet;
8use std::convert::Infallible;
9use std::fmt::Debug;
10use std::iter::Iterator;
11use std::mem;
12use std::ops::Index;
13
14impl TraitClause {
15    /// Constructs the trait ref that refers to this clause.
16    pub fn identity_tref(&self) -> TraitRef {
17        self.identity_tref_at_depth(DeBruijnId::zero())
18    }
19
20    /// Like `identity_tref` but uses variables bound at the given depth.
21    pub fn identity_tref_at_depth(&self, depth: DeBruijnId) -> TraitRef {
22        TraitRef {
23            kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, self.clause_id)),
24            trait_decl_ref: self.trait_.clone().move_under_binders(depth),
25        }
26    }
27}
28impl GenericParams {
29    pub fn empty() -> Self {
30        Self::default()
31    }
32
33    pub fn is_empty(&self) -> bool {
34        self.len() == 0
35    }
36
37    pub fn has_predicates(&self) -> bool {
38        !self.trait_clauses.is_empty()
39            || !self.types_outlive.is_empty()
40            || !self.regions_outlive.is_empty()
41            || !self.trait_type_constraints.is_empty()
42    }
43
44    /// Run some sanity checks.
45    pub fn check_consistency(&self) {
46        // Sanity check: check the clause ids are consistent.
47        assert!(self
48            .trait_clauses
49            .iter()
50            .enumerate()
51            .all(|(i, c)| c.clause_id.index() == i));
52
53        // Sanity check: region names are pairwise distinct (this caused trouble when generating
54        // names for the backward functions in Aeneas): at some point, Rustc introduced names equal
55        // to `Some("'_")` for the anonymous regions, instead of using `None` (we now check in
56        // [translate_region_name] and ignore names equal to "'_").
57        let mut s = HashSet::new();
58        for r in &self.regions {
59            if let Some(name) = &r.name {
60                assert!(
61                    !s.contains(name),
62                    "Name \"{}\" reused for two different lifetimes",
63                    name
64                );
65                s.insert(name);
66            }
67        }
68    }
69
70    pub fn len(&self) -> usize {
71        let GenericParams {
72            regions,
73            types,
74            const_generics,
75            trait_clauses,
76            regions_outlive,
77            types_outlive,
78            trait_type_constraints,
79        } = self;
80        regions.elem_count()
81            + types.elem_count()
82            + const_generics.elem_count()
83            + trait_clauses.elem_count()
84            + regions_outlive.len()
85            + types_outlive.len()
86            + trait_type_constraints.elem_count()
87    }
88
89    /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds
90    /// each required parameter with itself. E.g. given parameters for `<T, U> where U:
91    /// PartialEq<T>`, the arguments would be `<T, U>[@TraitClause0]`.
92    pub fn identity_args(&self, target: GenericsSource) -> GenericArgs {
93        self.identity_args_at_depth(target, DeBruijnId::zero())
94    }
95
96    /// Like `identity_args` but uses variables bound at the given depth.
97    pub fn identity_args_at_depth(&self, target: GenericsSource, depth: DeBruijnId) -> GenericArgs {
98        GenericArgs {
99            regions: self
100                .regions
101                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::bound(depth, id))),
102            types: self
103                .types
104                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::bound(depth, id)).into_ty()),
105            const_generics: self
106                .const_generics
107                .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::bound(depth, id))),
108            trait_refs: self
109                .trait_clauses
110                .map_ref(|clause| clause.identity_tref_at_depth(depth)),
111            target,
112        }
113    }
114}
115
116impl<T> Binder<T> {
117    pub fn new(kind: BinderKind, params: GenericParams, skip_binder: T) -> Self {
118        Self {
119            params,
120            skip_binder,
121            kind,
122        }
123    }
124
125    /// Substitute the provided arguments for the variables bound in this binder and return the
126    /// substituted inner value.
127    pub fn apply(self, args: &GenericArgs) -> T
128    where
129        T: TyVisitable,
130    {
131        self.skip_binder.substitute(args)
132    }
133}
134
135impl<T: AstVisitable> Binder<Binder<T>> {
136    /// Flatten two levels of binders into a single one.
137    pub fn flatten(self) -> Binder<T> {
138        #[derive(Visitor)]
139        struct FlattenVisitor<'a> {
140            shift_by: &'a GenericParams,
141            binder_depth: DeBruijnId,
142        }
143        impl VisitAstMut for FlattenVisitor<'_> {
144            fn enter_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
145                self.binder_depth = self.binder_depth.incr()
146            }
147            fn exit_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
148                self.binder_depth = self.binder_depth.decr()
149            }
150            fn enter_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
151                self.binder_depth = self.binder_depth.incr()
152            }
153            fn exit_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
154                self.binder_depth = self.binder_depth.decr()
155            }
156            fn enter_de_bruijn_id(&mut self, db_id: &mut DeBruijnId) {
157                if *db_id > self.binder_depth {
158                    // We started visiting at the inner binder, so in this branch we're either
159                    // mentioning the outer binder or a binder further beyond. Either way we
160                    // decrease the depth; variables that point to the outer binder don't have to
161                    // be shifted.
162                    *db_id = db_id.decr();
163                }
164            }
165            fn enter_region(&mut self, x: &mut Region) {
166                if let Region::Var(var) = x
167                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
168                {
169                    *id += self.shift_by.regions.slot_count();
170                }
171            }
172            fn enter_ty_kind(&mut self, x: &mut TyKind) {
173                if let TyKind::TypeVar(var) = x
174                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
175                {
176                    *id += self.shift_by.types.slot_count();
177                }
178            }
179            fn enter_const_generic(&mut self, x: &mut ConstGeneric) {
180                if let ConstGeneric::Var(var) = x
181                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
182                {
183                    *id += self.shift_by.const_generics.slot_count();
184                }
185            }
186            fn enter_trait_ref_kind(&mut self, x: &mut TraitRefKind) {
187                if let TraitRefKind::Clause(var) = x
188                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
189                {
190                    *id += self.shift_by.trait_clauses.slot_count();
191                }
192            }
193        }
194
195        // We will concatenate both sets of params.
196        let mut outer_params = self.params;
197
198        // The inner value needs to change:
199        // - at binder level 0 we shift all variable ids to match the concatenated params;
200        // - at binder level > 0 we decrease binding level because there's one fewer binder.
201        let mut bound_value = self.skip_binder.skip_binder;
202        let _ = bound_value.drive_mut(&mut FlattenVisitor {
203            shift_by: &outer_params,
204            binder_depth: Default::default(),
205        });
206
207        // The inner params must also be updated, as they can refer to themselves and the outer
208        // one.
209        let mut inner_params = self.skip_binder.params;
210        let _ = inner_params.drive_mut(&mut FlattenVisitor {
211            shift_by: &outer_params,
212            binder_depth: Default::default(),
213        });
214        inner_params
215            .regions
216            .iter_mut()
217            .for_each(|v| v.index += outer_params.regions.slot_count());
218        inner_params
219            .types
220            .iter_mut()
221            .for_each(|v| v.index += outer_params.types.slot_count());
222        inner_params
223            .const_generics
224            .iter_mut()
225            .for_each(|v| v.index += outer_params.const_generics.slot_count());
226        inner_params
227            .trait_clauses
228            .iter_mut()
229            .for_each(|v| v.clause_id += outer_params.trait_clauses.slot_count());
230
231        let GenericParams {
232            regions,
233            types,
234            const_generics,
235            trait_clauses,
236            regions_outlive,
237            types_outlive,
238            trait_type_constraints,
239        } = &inner_params;
240        outer_params.regions.extend_from_slice(regions);
241        outer_params.types.extend_from_slice(types);
242        outer_params
243            .const_generics
244            .extend_from_slice(const_generics);
245        outer_params.trait_clauses.extend_from_slice(trait_clauses);
246        outer_params
247            .regions_outlive
248            .extend_from_slice(regions_outlive);
249        outer_params.types_outlive.extend_from_slice(types_outlive);
250        outer_params
251            .trait_type_constraints
252            .extend_from_slice(trait_type_constraints);
253
254        Binder {
255            params: outer_params,
256            skip_binder: bound_value,
257            kind: BinderKind::Other,
258        }
259    }
260}
261
262impl<T> RegionBinder<T> {
263    /// Wrap the value in an empty region binder, shifting variables appropriately.
264    pub fn empty(x: T) -> Self
265    where
266        T: TyVisitable,
267    {
268        RegionBinder {
269            regions: Default::default(),
270            skip_binder: x.move_under_binder(),
271        }
272    }
273
274    pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> RegionBinder<U> {
275        RegionBinder {
276            regions: self.regions.clone(),
277            skip_binder: f(&self.skip_binder),
278        }
279    }
280
281    /// Substitute the bound variables with erased lifetimes.
282    pub fn erase(self) -> T
283    where
284        T: AstVisitable,
285    {
286        let args = GenericArgs {
287            regions: self.regions.map_ref_indexed(|_, _| Region::Erased),
288            ..GenericArgs::empty(GenericsSource::Other)
289        };
290        self.skip_binder.substitute(&args)
291    }
292}
293
294impl GenericArgs {
295    pub fn len(&self) -> usize {
296        let GenericArgs {
297            regions,
298            types,
299            const_generics,
300            trait_refs,
301            target: _,
302        } = self;
303        regions.elem_count()
304            + types.elem_count()
305            + const_generics.elem_count()
306            + trait_refs.elem_count()
307    }
308
309    pub fn is_empty(&self) -> bool {
310        self.len() == 0
311    }
312
313    pub fn empty(target: GenericsSource) -> Self {
314        GenericArgs {
315            regions: Default::default(),
316            types: Default::default(),
317            const_generics: Default::default(),
318            trait_refs: Default::default(),
319            target,
320        }
321    }
322
323    pub fn new_for_builtin(types: Vector<TypeVarId, Ty>) -> Self {
324        GenericArgs {
325            types,
326            ..Self::empty(GenericsSource::Builtin)
327        }
328    }
329
330    pub fn new(
331        regions: Vector<RegionId, Region>,
332        types: Vector<TypeVarId, Ty>,
333        const_generics: Vector<ConstGenericVarId, ConstGeneric>,
334        trait_refs: Vector<TraitClauseId, TraitRef>,
335        target: GenericsSource,
336    ) -> Self {
337        Self {
338            regions,
339            types,
340            const_generics,
341            trait_refs,
342            target,
343        }
344    }
345
346    /// Changes the target.
347    pub fn with_target(mut self, target: GenericsSource) -> Self {
348        self.target = target;
349        self
350    }
351
352    /// Check whether this matches the given `GenericParams`.
353    /// TODO: check more things, e.g. that the trait refs use the correct trait and generics.
354    pub fn matches(&self, params: &GenericParams) -> bool {
355        params.regions.elem_count() == self.regions.elem_count()
356            && params.types.elem_count() == self.types.elem_count()
357            && params.const_generics.elem_count() == self.const_generics.elem_count()
358            && params.trait_clauses.elem_count() == self.trait_refs.elem_count()
359    }
360
361    /// Return the same generics, but where we pop the first type arguments.
362    /// This is useful for trait references (for pretty printing for instance),
363    /// because the first type argument is the type for which the trait is
364    /// implemented.
365    pub fn pop_first_type_arg(&self) -> (Ty, Self) {
366        let mut generics = self.clone();
367        let mut it = mem::take(&mut generics.types).into_iter();
368        let ty = it.next().unwrap();
369        generics.types = it.collect();
370        (ty, generics)
371    }
372
373    /// Concatenate this set of arguments with another one. Use with care, you must manage the
374    /// order of arguments correctly.
375    pub fn concat(mut self, target: GenericsSource, other: &Self) -> Self {
376        let Self {
377            regions,
378            types,
379            const_generics,
380            trait_refs,
381            target: _,
382        } = other;
383        self.regions.extend_from_slice(regions);
384        self.types.extend_from_slice(types);
385        self.const_generics.extend_from_slice(const_generics);
386        self.trait_refs.extend_from_slice(trait_refs);
387        self.target = target;
388        self
389    }
390}
391
392impl GenericsSource {
393    pub fn item<I: Into<AnyTransId>>(id: I) -> Self {
394        Self::Item(id.into())
395    }
396
397    /// Return a path that represents the target item.
398    pub fn item_name(&self, translated: &TranslatedCrate, fmt_ctx: &FmtCtx) -> String {
399        match self {
400            GenericsSource::Item(id) => translated.item_name(*id).unwrap().fmt_with_ctx(fmt_ctx),
401            GenericsSource::Method(trait_id, method_name) => format!(
402                "{}::{method_name}",
403                translated
404                    .item_name(*trait_id)
405                    .unwrap()
406                    .fmt_with_ctx(fmt_ctx),
407            ),
408            GenericsSource::Builtin => format!("<built-in>"),
409            GenericsSource::Other => format!("<unknown>"),
410        }
411    }
412}
413
414impl IntegerTy {
415    pub fn is_signed(&self) -> bool {
416        matches!(
417            self,
418            IntegerTy::Isize
419                | IntegerTy::I8
420                | IntegerTy::I16
421                | IntegerTy::I32
422                | IntegerTy::I64
423                | IntegerTy::I128
424        )
425    }
426
427    pub fn is_unsigned(&self) -> bool {
428        !(self.is_signed())
429    }
430
431    /// Return the size (in bytes) of an integer of the proper type
432    pub fn size(&self) -> usize {
433        use std::mem::size_of;
434        match self {
435            IntegerTy::Isize => size_of::<isize>(),
436            IntegerTy::I8 => size_of::<i8>(),
437            IntegerTy::I16 => size_of::<i16>(),
438            IntegerTy::I32 => size_of::<i32>(),
439            IntegerTy::I64 => size_of::<i64>(),
440            IntegerTy::I128 => size_of::<i128>(),
441            IntegerTy::Usize => size_of::<isize>(),
442            IntegerTy::U8 => size_of::<u8>(),
443            IntegerTy::U16 => size_of::<u16>(),
444            IntegerTy::U32 => size_of::<u32>(),
445            IntegerTy::U64 => size_of::<u64>(),
446            IntegerTy::U128 => size_of::<u128>(),
447        }
448    }
449}
450
451/// A value of type `T` bound by the generic parameters of item
452/// `item`. Used when dealing with multiple items at a time, to
453/// ensure we don't mix up generics.
454///
455/// To get the value, use `under_binder_of` or `subst_for`.
456#[derive(Debug, Clone, Copy)]
457pub struct ItemBinder<ItemId, T> {
458    pub item_id: ItemId,
459    val: T,
460}
461
462impl<ItemId, T> ItemBinder<ItemId, T>
463where
464    ItemId: Debug + Copy + PartialEq,
465{
466    pub fn new(item_id: ItemId, val: T) -> Self {
467        Self { item_id, val }
468    }
469
470    pub fn as_ref(&self) -> ItemBinder<ItemId, &T> {
471        ItemBinder {
472            item_id: self.item_id,
473            val: &self.val,
474        }
475    }
476
477    pub fn map_bound<U>(self, f: impl FnOnce(T) -> U) -> ItemBinder<ItemId, U> {
478        ItemBinder {
479            item_id: self.item_id,
480            val: f(self.val),
481        }
482    }
483
484    fn assert_item_id(&self, item_id: ItemId) {
485        assert_eq!(
486            self.item_id, item_id,
487            "Trying to use item bound for {:?} as if it belonged to {:?}",
488            self.item_id, item_id
489        );
490    }
491
492    /// Assert that the value is bound for item `item_id`, and returns it. This is used when we
493    /// plan to store the returned value inside that item.
494    pub fn under_binder_of(self, item_id: ItemId) -> T {
495        self.assert_item_id(item_id);
496        self.val
497    }
498
499    /// Given generic args for `item_id`, assert that the value is bound for `item_id` and
500    /// substitute it with the provided generic arguments. Because the arguments are bound in the
501    /// context of another item, so it the resulting substituted value.
502    pub fn substitute<OtherItem: Debug + Copy + PartialEq>(
503        self,
504        args: ItemBinder<OtherItem, &GenericArgs>,
505    ) -> ItemBinder<OtherItem, T>
506    where
507        ItemId: Into<AnyTransId>,
508        T: TyVisitable,
509    {
510        args.map_bound(|args| {
511            assert_eq!(
512                args.target,
513                GenericsSource::item(self.item_id),
514                "These `GenericArgs` are meant for {:?} but were used on {:?}",
515                args.target,
516                self.item_id
517            );
518            self.val.substitute(args)
519        })
520    }
521}
522
523/// Dummy item identifier that represents the current item when not ambiguous.
524#[derive(Debug, Clone, Copy, PartialEq, Eq)]
525pub struct CurrentItem;
526
527impl<T> ItemBinder<CurrentItem, T> {
528    pub fn under_current_binder(self) -> T {
529        self.val
530    }
531}
532
533impl Ty {
534    /// Return true if it is actually unit (i.e.: 0-tuple)
535    pub fn is_unit(&self) -> bool {
536        match self.kind() {
537            TyKind::Adt(TypeId::Tuple, args) => {
538                assert!(args.regions.is_empty());
539                assert!(args.const_generics.is_empty());
540                args.types.is_empty()
541            }
542            _ => false,
543        }
544    }
545
546    /// Return the unit type
547    pub fn mk_unit() -> Ty {
548        TyKind::Adt(TypeId::Tuple, GenericArgs::empty(GenericsSource::Builtin)).into_ty()
549    }
550
551    /// Return true if this is a scalar type
552    pub fn is_scalar(&self) -> bool {
553        match self.kind() {
554            TyKind::Literal(kind) => kind.is_integer(),
555            _ => false,
556        }
557    }
558
559    pub fn is_unsigned_scalar(&self) -> bool {
560        match self.kind() {
561            TyKind::Literal(LiteralTy::Integer(kind)) => kind.is_unsigned(),
562            _ => false,
563        }
564    }
565
566    pub fn is_signed_scalar(&self) -> bool {
567        match self.kind() {
568            TyKind::Literal(LiteralTy::Integer(kind)) => kind.is_signed(),
569            _ => false,
570        }
571    }
572
573    /// Return true if the type is Box
574    pub fn is_box(&self) -> bool {
575        match self.kind() {
576            TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
577                assert!(generics.regions.is_empty());
578                assert!(generics.types.elem_count() == 1);
579                assert!(generics.const_generics.is_empty());
580                true
581            }
582            _ => false,
583        }
584    }
585
586    pub fn as_box(&self) -> Option<&Ty> {
587        match self.kind() {
588            TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
589                assert!(generics.regions.is_empty());
590                assert!(generics.types.elem_count() == 1);
591                assert!(generics.const_generics.is_empty());
592                Some(&generics.types[0])
593            }
594            _ => None,
595        }
596    }
597
598    pub fn as_array_or_slice(&self) -> Option<&Ty> {
599        match self.kind() {
600            TyKind::Adt(TypeId::Builtin(BuiltinTy::Array | BuiltinTy::Slice), generics) => {
601                assert!(generics.regions.is_empty());
602                assert!(generics.types.elem_count() == 1);
603                Some(&generics.types[0])
604            }
605            _ => None,
606        }
607    }
608
609    pub fn as_tuple(&self) -> Option<&Vector<TypeVarId, Ty>> {
610        match self.kind() {
611            TyKind::Adt(TypeId::Tuple, generics) => {
612                assert!(generics.regions.is_empty());
613                assert!(generics.const_generics.is_empty());
614                Some(&generics.types)
615            }
616            _ => None,
617        }
618    }
619
620    pub fn as_adt(&self) -> Option<(TypeId, &GenericArgs)> {
621        match self.kind() {
622            TyKind::Adt(id, generics) => Some((*id, generics)),
623            _ => None,
624        }
625    }
626}
627
628impl TyKind {
629    pub fn into_ty(self) -> Ty {
630        Ty::new(self)
631    }
632}
633
634impl From<TyKind> for Ty {
635    fn from(kind: TyKind) -> Ty {
636        kind.into_ty()
637    }
638}
639
640/// Convenience for migration purposes.
641impl std::ops::Deref for Ty {
642    type Target = TyKind;
643
644    fn deref(&self) -> &Self::Target {
645        self.kind()
646    }
647}
648/// For deref patterns.
649unsafe impl std::ops::DerefPure for Ty {}
650
651impl TypeId {
652    pub fn generics_target(&self) -> GenericsSource {
653        match *self {
654            TypeId::Adt(decl_id) => GenericsSource::item(decl_id),
655            TypeId::Tuple | TypeId::Builtin(..) => GenericsSource::Builtin,
656        }
657    }
658}
659
660impl FunId {
661    pub fn generics_target(&self) -> GenericsSource {
662        match *self {
663            FunId::Regular(fun_id) => GenericsSource::item(fun_id),
664            FunId::Builtin(..) => GenericsSource::Builtin,
665        }
666    }
667}
668
669impl FunIdOrTraitMethodRef {
670    pub fn generics_target(&self) -> GenericsSource {
671        match self {
672            FunIdOrTraitMethodRef::Fun(fun_id) => fun_id.generics_target(),
673            FunIdOrTraitMethodRef::Trait(trait_ref, name, _) => {
674                GenericsSource::Method(trait_ref.trait_decl_ref.skip_binder.trait_id, name.clone())
675            }
676        }
677    }
678}
679
680impl Field {
681    /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
682    pub fn renamed_name(&self) -> Option<&str> {
683        self.attr_info.rename.as_deref().or(self.name.as_deref())
684    }
685
686    /// Whether this field has a `#[charon::opaque]` annotation.
687    pub fn is_opaque(&self) -> bool {
688        self.attr_info
689            .attributes
690            .iter()
691            .any(|attr| attr.is_opaque())
692    }
693}
694
695impl Variant {
696    /// The new name for this variant, as suggested by the `#[charon::rename]` and
697    /// `#[charon::variants_prefix]` attributes.
698    pub fn renamed_name(&self) -> &str {
699        self.attr_info
700            .rename
701            .as_deref()
702            .unwrap_or(self.name.as_ref())
703    }
704
705    /// Whether this variant has a `#[charon::opaque]` annotation.
706    pub fn is_opaque(&self) -> bool {
707        self.attr_info
708            .attributes
709            .iter()
710            .any(|attr| attr.is_opaque())
711    }
712}
713
714impl RefKind {
715    pub fn mutable(x: bool) -> Self {
716        if x {
717            Self::Mut
718        } else {
719            Self::Shared
720        }
721    }
722}
723
724/// Visitor for the [Ty::substitute] function.
725/// This substitutes variables bound at the level where we start to substitute (level 0).
726#[derive(Visitor)]
727pub(crate) struct SubstVisitor<'a> {
728    generics: &'a GenericArgs,
729    self_ref: &'a TraitRefKind,
730    // Tracks the depth of binders we're inside of.
731    // Important: we must update it whenever we go inside a binder.
732    binder_depth: DeBruijnId,
733}
734
735impl<'a> SubstVisitor<'a> {
736    pub(crate) fn new(generics: &'a GenericArgs, self_ref: &'a TraitRefKind) -> Self {
737        Self {
738            generics,
739            self_ref,
740            binder_depth: DeBruijnId::zero(),
741        }
742    }
743
744    /// Process the variable, either modifying the variable in-place or returning the new value to
745    /// assign to the type/region/const generic/trait ref that was this variable.
746    fn process_var<Id, T>(&self, var: &mut DeBruijnVar<Id>) -> Option<T>
747    where
748        Id: Copy,
749        GenericArgs: Index<Id, Output = T>,
750        T: Clone + TyVisitable,
751    {
752        use std::cmp::Ordering::*;
753        match var {
754            DeBruijnVar::Bound(dbid, varid) => match (*dbid).cmp(&self.binder_depth) {
755                Equal => Some(
756                    self.generics[*varid]
757                        .clone()
758                        .move_under_binders(self.binder_depth),
759                ),
760                Greater => {
761                    // This is bound outside the binder we're substituting for.
762                    *dbid = dbid.decr();
763                    None
764                }
765                Less => None,
766            },
767            DeBruijnVar::Free(..) => None,
768        }
769    }
770}
771
772impl VisitAstMut for SubstVisitor<'_> {
773    fn enter_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
774        self.binder_depth = self.binder_depth.incr()
775    }
776    fn exit_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
777        self.binder_depth = self.binder_depth.decr()
778    }
779    fn enter_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
780        self.binder_depth = self.binder_depth.incr()
781    }
782    fn exit_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
783        self.binder_depth = self.binder_depth.decr()
784    }
785
786    fn exit_region(&mut self, r: &mut Region) {
787        match r {
788            Region::Var(var) => {
789                if let Some(new_r) = self.process_var(var) {
790                    *r = new_r;
791                }
792            }
793            _ => (),
794        }
795    }
796
797    fn exit_ty(&mut self, ty: &mut Ty) {
798        let new_ty = ty.with_kind_mut(|kind| match kind {
799            TyKind::TypeVar(var) => self.process_var(var),
800            _ => None,
801        });
802        if let Some(new_ty) = new_ty {
803            *ty = new_ty
804        }
805    }
806
807    fn exit_const_generic(&mut self, cg: &mut ConstGeneric) {
808        match cg {
809            ConstGeneric::Var(var) => {
810                if let Some(new_cg) = self.process_var(var) {
811                    *cg = new_cg;
812                }
813            }
814            _ => (),
815        }
816    }
817
818    fn exit_trait_ref_kind(&mut self, kind: &mut TraitRefKind) {
819        match kind {
820            TraitRefKind::SelfId => {
821                *kind = self.self_ref.clone().move_under_binders(self.binder_depth);
822            }
823            TraitRefKind::Clause(var) => {
824                if let Some(new_tr) = self.process_var(var) {
825                    *kind = new_tr.kind;
826                }
827            }
828            _ => (),
829        }
830    }
831}
832
833/// Types that are involved at the type-level and may be substituted around.
834pub trait TyVisitable: Sized + AstVisitable {
835    fn substitute(self, generics: &GenericArgs) -> Self {
836        self.substitute_with_self(generics, &TraitRefKind::SelfId)
837    }
838
839    fn substitute_with_self(mut self, generics: &GenericArgs, self_ref: &TraitRefKind) -> Self {
840        let _ = self.drive_mut(&mut SubstVisitor::new(generics, self_ref));
841        self
842    }
843
844    /// Move under one binder.
845    fn move_under_binder(self) -> Self {
846        self.move_under_binders(DeBruijnId::one())
847    }
848
849    /// Move under `depth` binders.
850    fn move_under_binders(mut self, depth: DeBruijnId) -> Self {
851        if !depth.is_zero() {
852            let Continue(()) = self.visit_db_id::<Infallible>(|id| {
853                *id = id.plus(depth);
854                Continue(())
855            });
856        }
857        self
858    }
859
860    /// Move from under one binder.
861    fn move_from_under_binder(self) -> Option<Self> {
862        self.move_from_under_binders(DeBruijnId::one())
863    }
864
865    /// Move the value out of `depth` binders. Returns `None` if it contains a variable bound in
866    /// one of these `depth` binders.
867    fn move_from_under_binders(mut self, depth: DeBruijnId) -> Option<Self> {
868        self.visit_db_id::<()>(|id| match id.sub(depth) {
869            Some(sub) => {
870                *id = sub;
871                Continue(())
872            }
873            None => Break(()),
874        })
875        .is_continue()
876        .then_some(self)
877    }
878
879    /// Visit the de Bruijn ids contained in `self`, as seen from the outside of `self`. This means
880    /// that any variable bound inside `self` will be skipped, and all the seen indices will count
881    /// from the outside of self.
882    fn visit_db_id<B>(
883        &mut self,
884        f: impl FnMut(&mut DeBruijnId) -> ControlFlow<B>,
885    ) -> ControlFlow<B> {
886        struct Wrap<F> {
887            f: F,
888            depth: DeBruijnId,
889        }
890        impl<B, F> Visitor for Wrap<F>
891        where
892            F: FnMut(&mut DeBruijnId) -> ControlFlow<B>,
893        {
894            type Break = B;
895        }
896        impl<B, F> VisitAstMut for Wrap<F>
897        where
898            F: FnMut(&mut DeBruijnId) -> ControlFlow<B>,
899        {
900            fn enter_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
901                self.depth = self.depth.incr()
902            }
903            fn exit_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
904                self.depth = self.depth.decr()
905            }
906            fn enter_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
907                self.depth = self.depth.incr()
908            }
909            fn exit_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
910                self.depth = self.depth.decr()
911            }
912
913            fn visit_de_bruijn_id(&mut self, x: &mut DeBruijnId) -> ControlFlow<Self::Break> {
914                if let Some(mut shifted) = x.sub(self.depth) {
915                    (self.f)(&mut shifted)?;
916                    *x = shifted.plus(self.depth)
917                }
918                Continue(())
919            }
920        }
921        self.drive_mut(&mut Wrap {
922            f,
923            depth: DeBruijnId::zero(),
924        })
925    }
926}
927
928impl<T: AstVisitable> TyVisitable for T {}
929
930impl PartialEq for TraitClause {
931    fn eq(&self, other: &Self) -> bool {
932        // Skip `span` and `origin`
933        self.clause_id == other.clause_id && self.trait_ == other.trait_
934    }
935}
936
937impl Eq for TraitClause {}
938
939mk_index_impls!(GenericArgs.regions[RegionId]: Region);
940mk_index_impls!(GenericArgs.types[TypeVarId]: Ty);
941mk_index_impls!(GenericArgs.const_generics[ConstGenericVarId]: ConstGeneric);
942mk_index_impls!(GenericArgs.trait_refs[TraitClauseId]: TraitRef);
943mk_index_impls!(GenericParams.regions[RegionId]: RegionVar);
944mk_index_impls!(GenericParams.types[TypeVarId]: TypeVar);
945mk_index_impls!(GenericParams.const_generics[ConstGenericVarId]: ConstGenericVar);
946mk_index_impls!(GenericParams.trait_clauses[TraitClauseId]: TraitClause);
charon_lib/ast/types_utils.rs

charon_lib/ast/
types_utils.rs
