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;
10use std::ops::Index;
11
12impl TraitClause {
13    /// Constructs the trait ref that refers to this clause.
14    pub fn identity_tref(&self) -> TraitRef {
15        self.identity_tref_at_depth(DeBruijnId::zero())
16    }
17
18    /// Like `identity_tref` but uses variables bound at the given depth.
19    pub fn identity_tref_at_depth(&self, depth: DeBruijnId) -> TraitRef {
20        TraitRef {
21            kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, self.clause_id)),
22            trait_decl_ref: self.trait_.clone().move_under_binders(depth),
23        }
24    }
25}
26
27impl GenericParams {
28    pub fn empty() -> Self {
29        Self::default()
30    }
31
32    pub fn is_empty(&self) -> bool {
33        self.len() == 0
34    }
35    /// Whether this has any explicit arguments (types, regions or const generics).
36    pub fn has_explicits(&self) -> bool {
37        !self.regions.is_empty() || !self.types.is_empty() || !self.const_generics.is_empty()
38    }
39    /// Whether this has any implicit arguments (trait clauses, outlives relations, associated type
40    /// equality constraints).
41    pub fn has_predicates(&self) -> bool {
42        !self.trait_clauses.is_empty()
43            || !self.types_outlive.is_empty()
44            || !self.regions_outlive.is_empty()
45            || !self.trait_type_constraints.is_empty()
46    }
47
48    /// Run some sanity checks.
49    pub fn check_consistency(&self) {
50        // Sanity check: check the clause ids are consistent.
51        assert!(self
52            .trait_clauses
53            .iter()
54            .enumerate()
55            .all(|(i, c)| c.clause_id.index() == i));
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 erased lifetimes.
292    pub fn erase(self) -> T
293    where
294        T: AstVisitable,
295    {
296        let args = GenericArgs {
297            regions: self.regions.map_ref_indexed(|_, _| Region::Erased),
298            ..GenericArgs::empty()
299        };
300        self.skip_binder.substitute(&args)
301    }
302}
303
304impl GenericArgs {
305    pub fn len(&self) -> usize {
306        let GenericArgs {
307            regions,
308            types,
309            const_generics,
310            trait_refs,
311        } = self;
312        regions.elem_count()
313            + types.elem_count()
314            + const_generics.elem_count()
315            + trait_refs.elem_count()
316    }
317
318    pub fn is_empty(&self) -> bool {
319        self.len() == 0
320    }
321    /// Whether this has any explicit arguments (types, regions or const generics).
322    pub fn has_explicits(&self) -> bool {
323        !self.regions.is_empty() || !self.types.is_empty() || !self.const_generics.is_empty()
324    }
325    /// Whether this has any implicit arguments (trait refs).
326    pub fn has_implicits(&self) -> bool {
327        !self.trait_refs.is_empty()
328    }
329
330    pub fn empty() -> Self {
331        GenericArgs {
332            regions: Default::default(),
333            types: Default::default(),
334            const_generics: Default::default(),
335            trait_refs: Default::default(),
336        }
337    }
338
339    pub fn new_for_builtin(types: Vector<TypeVarId, Ty>) -> Self {
340        GenericArgs {
341            types,
342            ..Self::empty()
343        }
344    }
345
346    pub fn new(
347        regions: Vector<RegionId, Region>,
348        types: Vector<TypeVarId, Ty>,
349        const_generics: Vector<ConstGenericVarId, ConstGeneric>,
350        trait_refs: Vector<TraitClauseId, TraitRef>,
351    ) -> Self {
352        Self {
353            regions,
354            types,
355            const_generics,
356            trait_refs,
357        }
358    }
359
360    pub fn new_types(types: Vector<TypeVarId, Ty>) -> Self {
361        Self {
362            types,
363            ..Self::empty()
364        }
365    }
366
367    /// Check whether this matches the given `GenericParams`.
368    /// TODO: check more things, e.g. that the trait refs use the correct trait and generics.
369    pub fn matches(&self, params: &GenericParams) -> bool {
370        params.regions.elem_count() == self.regions.elem_count()
371            && params.types.elem_count() == self.types.elem_count()
372            && params.const_generics.elem_count() == self.const_generics.elem_count()
373            && params.trait_clauses.elem_count() == self.trait_refs.elem_count()
374    }
375
376    /// Return the same generics, but where we pop the first type arguments.
377    /// This is useful for trait references (for pretty printing for instance),
378    /// because the first type argument is the type for which the trait is
379    /// implemented.
380    pub fn pop_first_type_arg(&self) -> (Ty, Self) {
381        let mut generics = self.clone();
382        let mut it = mem::take(&mut generics.types).into_iter();
383        let ty = it.next().unwrap();
384        generics.types = it.collect();
385        (ty, generics)
386    }
387
388    /// Concatenate this set of arguments with another one. Use with care, you must manage the
389    /// order of arguments correctly.
390    pub fn concat(mut self, other: &Self) -> Self {
391        let Self {
392            regions,
393            types,
394            const_generics,
395            trait_refs,
396        } = other;
397        self.regions.extend_from_slice(regions);
398        self.types.extend_from_slice(types);
399        self.const_generics.extend_from_slice(const_generics);
400        self.trait_refs.extend_from_slice(trait_refs);
401        self
402    }
403}
404
405impl IntegerTy {
406    pub fn is_signed(&self) -> bool {
407        matches!(
408            self,
409            IntegerTy::Isize
410                | IntegerTy::I8
411                | IntegerTy::I16
412                | IntegerTy::I32
413                | IntegerTy::I64
414                | IntegerTy::I128
415        )
416    }
417
418    pub fn is_unsigned(&self) -> bool {
419        !(self.is_signed())
420    }
421
422    /// Return the size (in bytes) of an integer of the proper type
423    pub fn size(&self) -> usize {
424        use std::mem::size_of;
425        match self {
426            IntegerTy::Isize => size_of::<isize>(),
427            IntegerTy::I8 => size_of::<i8>(),
428            IntegerTy::I16 => size_of::<i16>(),
429            IntegerTy::I32 => size_of::<i32>(),
430            IntegerTy::I64 => size_of::<i64>(),
431            IntegerTy::I128 => size_of::<i128>(),
432            IntegerTy::Usize => size_of::<isize>(),
433            IntegerTy::U8 => size_of::<u8>(),
434            IntegerTy::U16 => size_of::<u16>(),
435            IntegerTy::U32 => size_of::<u32>(),
436            IntegerTy::U64 => size_of::<u64>(),
437            IntegerTy::U128 => size_of::<u128>(),
438        }
439    }
440
441    pub fn to_unsigned(&self) -> Self {
442        match self {
443            IntegerTy::Isize => IntegerTy::Usize,
444            IntegerTy::I8 => IntegerTy::U8,
445            IntegerTy::I16 => IntegerTy::U16,
446            IntegerTy::I32 => IntegerTy::U32,
447            IntegerTy::I64 => IntegerTy::U64,
448            IntegerTy::I128 => IntegerTy::U128,
449            _ => *self,
450        }
451    }
452}
453
454/// A value of type `T` bound by the generic parameters of item
455/// `item`. Used when dealing with multiple items at a time, to
456/// ensure we don't mix up generics.
457///
458/// To get the value, use `under_binder_of` or `subst_for`.
459#[derive(Debug, Clone, Copy)]
460pub struct ItemBinder<ItemId, T> {
461    pub item_id: ItemId,
462    val: T,
463}
464
465impl<ItemId, T> ItemBinder<ItemId, T>
466where
467    ItemId: Debug + Copy + PartialEq,
468{
469    pub fn new(item_id: ItemId, val: T) -> Self {
470        Self { item_id, val }
471    }
472
473    pub fn as_ref(&self) -> ItemBinder<ItemId, &T> {
474        ItemBinder {
475            item_id: self.item_id,
476            val: &self.val,
477        }
478    }
479
480    pub fn map_bound<U>(self, f: impl FnOnce(T) -> U) -> ItemBinder<ItemId, U> {
481        ItemBinder {
482            item_id: self.item_id,
483            val: f(self.val),
484        }
485    }
486
487    fn assert_item_id(&self, item_id: ItemId) {
488        assert_eq!(
489            self.item_id, item_id,
490            "Trying to use item bound for {:?} as if it belonged to {:?}",
491            self.item_id, item_id
492        );
493    }
494
495    /// Assert that the value is bound for item `item_id`, and returns it. This is used when we
496    /// plan to store the returned value inside that item.
497    pub fn under_binder_of(self, item_id: ItemId) -> T {
498        self.assert_item_id(item_id);
499        self.val
500    }
501
502    /// Given generic args for `item_id`, assert that the value is bound for `item_id` and
503    /// substitute it with the provided generic arguments. Because the arguments are bound in the
504    /// context of another item, so it the resulting substituted value.
505    pub fn substitute<OtherItem: Debug + Copy + PartialEq>(
506        self,
507        args: ItemBinder<OtherItem, &GenericArgs>,
508    ) -> ItemBinder<OtherItem, T>
509    where
510        ItemId: Into<AnyTransId>,
511        T: TyVisitable,
512    {
513        args.map_bound(|args| self.val.substitute(args))
514    }
515}
516
517/// Dummy item identifier that represents the current item when not ambiguous.
518#[derive(Debug, Clone, Copy, PartialEq, Eq)]
519pub struct CurrentItem;
520
521impl<T> ItemBinder<CurrentItem, T> {
522    pub fn under_current_binder(self) -> T {
523        self.val
524    }
525}
526
527impl Ty {
528    /// Return the unit type
529    pub fn mk_unit() -> Ty {
530        Self::mk_tuple(vec![])
531    }
532
533    pub fn mk_tuple(tys: Vec<Ty>) -> Ty {
534        TyKind::Adt(TypeDeclRef {
535            id: TypeId::Tuple,
536            generics: Box::new(GenericArgs::new_for_builtin(tys.into())),
537        })
538        .into_ty()
539    }
540
541    pub fn mk_slice(ty: Ty) -> Ty {
542        TyKind::Adt(TypeDeclRef {
543            id: TypeId::Builtin(BuiltinTy::Slice),
544            generics: Box::new(GenericArgs::new_for_builtin(vec![ty].into())),
545        })
546        .into_ty()
547    }
548    /// Return true if it is actually unit (i.e.: 0-tuple)
549    pub fn is_unit(&self) -> bool {
550        match self.as_tuple() {
551            Some(tys) => tys.is_empty(),
552            None => false,
553        }
554    }
555
556    /// Return true if this is a scalar type
557    pub fn is_scalar(&self) -> bool {
558        match self.kind() {
559            TyKind::Literal(kind) => kind.is_integer(),
560            _ => false,
561        }
562    }
563
564    pub fn is_unsigned_scalar(&self) -> bool {
565        match self.kind() {
566            TyKind::Literal(LiteralTy::Integer(kind)) => kind.is_unsigned(),
567            _ => false,
568        }
569    }
570
571    pub fn is_signed_scalar(&self) -> bool {
572        match self.kind() {
573            TyKind::Literal(LiteralTy::Integer(kind)) => kind.is_signed(),
574            _ => false,
575        }
576    }
577
578    /// Return true if the type is Box
579    pub fn is_box(&self) -> bool {
580        match self.kind() {
581            TyKind::Adt(ty_ref) if let TypeId::Builtin(BuiltinTy::Box) = ty_ref.id => true,
582            _ => false,
583        }
584    }
585
586    pub fn as_box(&self) -> Option<&Ty> {
587        match self.kind() {
588            TyKind::Adt(ty_ref) if let TypeId::Builtin(BuiltinTy::Box) = ty_ref.id => {
589                Some(&ty_ref.generics.types[0])
590            }
591            _ => None,
592        }
593    }
594
595    pub fn as_array_or_slice(&self) -> Option<&Ty> {
596        match self.kind() {
597            TyKind::Adt(ty_ref)
598                if let TypeId::Builtin(BuiltinTy::Array | BuiltinTy::Slice) = ty_ref.id =>
599            {
600                Some(&ty_ref.generics.types[0])
601            }
602            _ => None,
603        }
604    }
605
606    pub fn as_tuple(&self) -> Option<&Vector<TypeVarId, Ty>> {
607        match self.kind() {
608            TyKind::Adt(ty_ref) if let TypeId::Tuple = ty_ref.id => Some(&ty_ref.generics.types),
609            _ => None,
610        }
611    }
612
613    pub fn as_adt(&self) -> Option<&TypeDeclRef> {
614        self.kind().as_adt()
615    }
616}
617
618impl TyKind {
619    pub fn into_ty(self) -> Ty {
620        Ty::new(self)
621    }
622}
623
624impl From<TyKind> for Ty {
625    fn from(kind: TyKind) -> Ty {
626        kind.into_ty()
627    }
628}
629
630/// Convenience for migration purposes.
631impl std::ops::Deref for Ty {
632    type Target = TyKind;
633
634    fn deref(&self) -> &Self::Target {
635        self.kind()
636    }
637}
638/// For deref patterns.
639unsafe impl std::ops::DerefPure for Ty {}
640
641impl TypeDeclRef {
642    pub fn new(id: TypeId, generics: GenericArgs) -> Self {
643        Self {
644            id,
645            generics: Box::new(generics),
646        }
647    }
648}
649
650impl Field {
651    /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
652    pub fn renamed_name(&self) -> Option<&str> {
653        self.attr_info.rename.as_deref().or(self.name.as_deref())
654    }
655
656    /// Whether this field has a `#[charon::opaque]` annotation.
657    pub fn is_opaque(&self) -> bool {
658        self.attr_info
659            .attributes
660            .iter()
661            .any(|attr| attr.is_opaque())
662    }
663}
664
665impl Variant {
666    /// The new name for this variant, as suggested by the `#[charon::rename]` and
667    /// `#[charon::variants_prefix]` attributes.
668    pub fn renamed_name(&self) -> &str {
669        self.attr_info
670            .rename
671            .as_deref()
672            .unwrap_or(self.name.as_ref())
673    }
674
675    /// Whether this variant has a `#[charon::opaque]` annotation.
676    pub fn is_opaque(&self) -> bool {
677        self.attr_info
678            .attributes
679            .iter()
680            .any(|attr| attr.is_opaque())
681    }
682}
683
684impl RefKind {
685    pub fn mutable(x: bool) -> Self {
686        if x {
687            Self::Mut
688        } else {
689            Self::Shared
690        }
691    }
692}
693
694/// Visitor for the [TyVisitable::substitute] function.
695/// This substitutes variables bound at the level where we start to substitute (level 0).
696#[derive(Visitor)]
697pub(crate) struct SubstVisitor<'a> {
698    generics: &'a GenericArgs,
699    self_ref: &'a TraitRefKind,
700    // Tracks the depth of binders we're inside of.
701    // Important: we must update it whenever we go inside a binder.
702    binder_depth: DeBruijnId,
703}
704
705impl<'a> SubstVisitor<'a> {
706    pub(crate) fn new(generics: &'a GenericArgs, self_ref: &'a TraitRefKind) -> Self {
707        Self {
708            generics,
709            self_ref,
710            binder_depth: DeBruijnId::zero(),
711        }
712    }
713
714    /// Process the variable, either modifying the variable in-place or returning the new value to
715    /// assign to the type/region/const generic/trait ref that was this variable.
716    fn process_var<Id, T>(&self, var: &mut DeBruijnVar<Id>) -> Option<T>
717    where
718        Id: Copy,
719        GenericArgs: Index<Id, Output = T>,
720        T: Clone + TyVisitable,
721    {
722        use std::cmp::Ordering::*;
723        match var {
724            DeBruijnVar::Bound(dbid, varid) => match (*dbid).cmp(&self.binder_depth) {
725                Equal => Some(
726                    self.generics[*varid]
727                        .clone()
728                        .move_under_binders(self.binder_depth),
729                ),
730                Greater => {
731                    // This is bound outside the binder we're substituting for.
732                    *dbid = dbid.decr();
733                    None
734                }
735                Less => None,
736            },
737            DeBruijnVar::Free(..) => None,
738        }
739    }
740}
741
742impl VisitAstMut for SubstVisitor<'_> {
743    fn enter_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
744        self.binder_depth = self.binder_depth.incr()
745    }
746    fn exit_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
747        self.binder_depth = self.binder_depth.decr()
748    }
749    fn enter_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
750        self.binder_depth = self.binder_depth.incr()
751    }
752    fn exit_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
753        self.binder_depth = self.binder_depth.decr()
754    }
755
756    fn exit_region(&mut self, r: &mut Region) {
757        match r {
758            Region::Var(var) => {
759                if let Some(new_r) = self.process_var(var) {
760                    *r = new_r;
761                }
762            }
763            _ => (),
764        }
765    }
766
767    fn exit_ty(&mut self, ty: &mut Ty) {
768        let new_ty = ty.with_kind_mut(|kind| match kind {
769            TyKind::TypeVar(var) => self.process_var(var),
770            _ => None,
771        });
772        if let Some(new_ty) = new_ty {
773            *ty = new_ty
774        }
775    }
776
777    fn exit_const_generic(&mut self, cg: &mut ConstGeneric) {
778        match cg {
779            ConstGeneric::Var(var) => {
780                if let Some(new_cg) = self.process_var(var) {
781                    *cg = new_cg;
782                }
783            }
784            _ => (),
785        }
786    }
787
788    fn exit_constant_expr(&mut self, ce: &mut ConstantExpr) {
789        match &mut ce.value {
790            RawConstantExpr::Var(var) => {
791                if let Some(new_ce) = self.process_var(var) {
792                    ce.value = match new_ce {
793                        ConstGeneric::Global(id) => RawConstantExpr::Global(GlobalDeclRef {
794                            id,
795                            generics: Box::new(GenericArgs::empty()),
796                        }),
797                        ConstGeneric::Var(var) => RawConstantExpr::Var(var),
798                        ConstGeneric::Value(lit) => RawConstantExpr::Literal(lit),
799                    };
800                }
801            }
802            _ => (),
803        }
804    }
805
806    fn exit_trait_ref_kind(&mut self, kind: &mut TraitRefKind) {
807        match kind {
808            TraitRefKind::SelfId => {
809                *kind = self.self_ref.clone().move_under_binders(self.binder_depth);
810            }
811            TraitRefKind::Clause(var) => {
812                if let Some(new_tr) = self.process_var(var) {
813                    *kind = new_tr.kind;
814                }
815            }
816            _ => (),
817        }
818    }
819}
820
821/// Types that are involved at the type-level and may be substituted around.
822pub trait TyVisitable: Sized + AstVisitable {
823    fn substitute(self, generics: &GenericArgs) -> Self {
824        self.substitute_with_self(generics, &TraitRefKind::SelfId)
825    }
826
827    fn substitute_with_self(mut self, generics: &GenericArgs, self_ref: &TraitRefKind) -> Self {
828        let _ = self.drive_mut(&mut SubstVisitor::new(generics, self_ref));
829        self
830    }
831
832    /// Move under one binder.
833    fn move_under_binder(self) -> Self {
834        self.move_under_binders(DeBruijnId::one())
835    }
836
837    /// Move under `depth` binders.
838    fn move_under_binders(mut self, depth: DeBruijnId) -> Self {
839        if !depth.is_zero() {
840            let Continue(()) = self.visit_db_id::<Infallible>(|id| {
841                *id = id.plus(depth);
842                Continue(())
843            });
844        }
845        self
846    }
847
848    /// Move from under one binder.
849    fn move_from_under_binder(self) -> Option<Self> {
850        self.move_from_under_binders(DeBruijnId::one())
851    }
852
853    /// Move the value out of `depth` binders. Returns `None` if it contains a variable bound in
854    /// one of these `depth` binders.
855    fn move_from_under_binders(mut self, depth: DeBruijnId) -> Option<Self> {
856        self.visit_db_id::<()>(|id| match id.sub(depth) {
857            Some(sub) => {
858                *id = sub;
859                Continue(())
860            }
861            None => Break(()),
862        })
863        .is_continue()
864        .then_some(self)
865    }
866
867    /// Visit the de Bruijn ids contained in `self`, as seen from the outside of `self`. This means
868    /// that any variable bound inside `self` will be skipped, and all the seen indices will count
869    /// from the outside of self.
870    fn visit_db_id<B>(
871        &mut self,
872        f: impl FnMut(&mut DeBruijnId) -> ControlFlow<B>,
873    ) -> ControlFlow<B> {
874        struct Wrap<F> {
875            f: F,
876            depth: DeBruijnId,
877        }
878        impl<B, F> Visitor for Wrap<F>
879        where
880            F: FnMut(&mut DeBruijnId) -> ControlFlow<B>,
881        {
882            type Break = B;
883        }
884        impl<B, F> VisitAstMut for Wrap<F>
885        where
886            F: FnMut(&mut DeBruijnId) -> ControlFlow<B>,
887        {
888            fn enter_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
889                self.depth = self.depth.incr()
890            }
891            fn exit_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
892                self.depth = self.depth.decr()
893            }
894            fn enter_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
895                self.depth = self.depth.incr()
896            }
897            fn exit_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
898                self.depth = self.depth.decr()
899            }
900
901            fn visit_de_bruijn_id(&mut self, x: &mut DeBruijnId) -> ControlFlow<Self::Break> {
902                if let Some(mut shifted) = x.sub(self.depth) {
903                    (self.f)(&mut shifted)?;
904                    *x = shifted.plus(self.depth)
905                }
906                Continue(())
907            }
908        }
909        self.drive_mut(&mut Wrap {
910            f,
911            depth: DeBruijnId::zero(),
912        })
913    }
914}
915
916impl TypeDecl {
917    /// Looks up the variant corresponding to the tag (i.e. the in-memory bytes that represent the discriminant).
918    /// Returns `None` for types that don't have a relevant discriminant (e.g. uninhabited types).
919    ///
920    /// If the `tag` does not correspond to any valid discriminant but there is a niche,
921    /// the resulting `VariantId` will be for the untagged variant [`TagEncoding::Niche::untagged_variant`].
922    pub fn get_variant_from_tag(&self, tag: ScalarValue) -> Option<VariantId> {
923        let layout = self.layout.as_ref()?;
924        if layout.uninhabited {
925            return None;
926        };
927        let discr_layout = layout.discriminant_layout.as_ref()?;
928
929        let variant_for_tag =
930            layout
931                .variant_layouts
932                .iter_indexed()
933                .find_map(|(id, variant_layout)| {
934                    if variant_layout.tag == Some(tag) {
935                        Some(id)
936                    } else {
937                        None
938                    }
939                });
940
941        match &discr_layout.encoding {
942            TagEncoding::Direct => {
943                assert_eq!(tag.get_integer_ty(), discr_layout.tag_ty);
944                variant_for_tag
945            }
946            TagEncoding::Niche { untagged_variant } => variant_for_tag.or(Some(*untagged_variant)),
947        }
948    }
949}
950
951impl Layout {
952    pub fn is_variant_uninhabited(&self, variant_id: VariantId) -> bool {
953        if let Some(v) = self.variant_layouts.get(variant_id) {
954            v.uninhabited
955        } else {
956            false
957        }
958    }
959}
960
961impl<T: AstVisitable> TyVisitable for T {}
962
963impl Eq for TraitClause {}
964
965mk_index_impls!(GenericArgs.regions[RegionId]: Region);
966mk_index_impls!(GenericArgs.types[TypeVarId]: Ty);
967mk_index_impls!(GenericArgs.const_generics[ConstGenericVarId]: ConstGeneric);
968mk_index_impls!(GenericArgs.trait_refs[TraitClauseId]: TraitRef);
969mk_index_impls!(GenericParams.regions[RegionId]: RegionVar);
970mk_index_impls!(GenericParams.types[TypeVarId]: TypeVar);
971mk_index_impls!(GenericParams.const_generics[ConstGenericVarId]: ConstGenericVar);
972mk_index_impls!(GenericParams.trait_clauses[TraitClauseId]: TraitClause);
charon_lib/ast/types_utils.rs

charon_lib/ast/
types_utils.rs
