charon_lib/ast/
types_utils.rs

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

charon_lib/ast/
types_utils.rs
