charon_lib/ast/
type_level.rs

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

charon_lib/ast/
type_level.rs
