charon_lib/ast/type_level/
vars.rs

1//! Type-level variables. There are 4 kinds of variables at the type-level: regions, types, const
2//! generics and trait clauses. The relevant definitions are in this module.
3use std::{
4    borrow::Borrow,
5    ops::{Index, IndexMut},
6};
7
8use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
9use index_vec::Idx;
10use macros::EnumIsA;
11use serde::{Deserialize, Serialize};
12use serde_state::{DeserializeState, SerializeState};
13
14use crate::{ast::*, impl_from_enum};
15
16/// The index of a binder, counting from the innermost. See [`DeBruijnVar`] for details.
17#[derive(
18    Debug,
19    PartialEq,
20    Eq,
21    Copy,
22    Clone,
23    Hash,
24    PartialOrd,
25    Ord,
26    Serialize,
27    Deserialize,
28    Drive,
29    DriveMut,
30    DriveTwo,
31)]
32#[serde(transparent)]
33#[cfg_attr(feature = "charon_on_charon", charon::transparent)]
34pub struct DeBruijnId {
35    pub index: usize,
36}
37
38impl DeBruijnId {
39    pub const ZERO: DeBruijnId = DeBruijnId { index: 0 };
40}
41
42/// Type-level variable.
43///
44/// Variables are bound in groups. Each item has a top-level binding group in its `generic_params`
45/// field, and then inner binders are possible using the `RegionBinder<T>` and `Binder<T>` types.
46/// Each variable is linked to exactly one binder. The `Id` then identifies the specific variable
47/// among all those bound in that group.
48///
49/// For instance, we have the following:
50/// ```text
51/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
52///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
53///        |       inner binder  |       |     inner binder  |        |        |
54///  top-level binder            |       |                   |        |        |
55///                        Bound(1, b)   |              Bound(2, b)   |     Bound(0, d)
56///                                      |                            |
57///                                  Bound(0, c)                 Bound(1, c)
58/// ```
59///
60/// To make consumption easier for projects that don't do heavy substitution, `--unbind-item-vars`
61/// changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be
62/// `Free`. The example above becomes:
63/// ```text
64/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
65///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
66///        |       inner binder  |       |     inner binder  |        |        |
67///  top-level binder            |       |                   |        |        |
68///                           Free(b)    |                Free(b)     |     Bound(0, d)
69///                                      |                            |
70///                                  Bound(0, c)                 Bound(1, c)
71/// ```
72#[derive(
73    Debug,
74    PartialEq,
75    Eq,
76    Copy,
77    Clone,
78    Hash,
79    PartialOrd,
80    Ord,
81    SerializeState,
82    DeserializeState,
83    Drive,
84    DriveMut,
85    DriveTwo,
86)]
87pub enum DeBruijnVar<Id> {
88    /// A variable attached to the nth binder, counting from the innermost.
89    Bound(#[serde_state(stateless)] DeBruijnId, Id),
90    /// A variable attached to the outermost binder (the one on the item). This is not used within
91    /// Charon itself, instead ewe insert it at the end if `--unbind-item-vars` is set.
92    Free(Id),
93}
94
95// We need to manipulate a lot of indices for the types, variables, definitions, etc. In order not
96// to confuse them, we define an index type for every one of them (which is just a struct with a
97// unique usize field), together with some utilities like a fresh index generator, using the
98// `generate_index_type` macro.
99generate_index_type!(RegionId, "Region");
100generate_index_type!(TypeVarId, "T");
101generate_index_type!(ConstGenericVarId, "Const");
102generate_index_type!(TraitClauseId, "TraitClause");
103generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");
104
105/// The variance of a lifetime or type parameter.
106#[derive(
107    Debug,
108    Clone,
109    Copy,
110    PartialEq,
111    Eq,
112    PartialOrd,
113    Ord,
114    Hash,
115    Serialize,
116    Deserialize,
117    Drive,
118    DriveMut,
119    DriveTwo,
120)]
121pub enum Variance {
122    Covariant,
123    Invariant,
124    Contravariant,
125    Bivariant,
126    /// Variance was not sensible (e.g. on impls), not available (e.g. on higher-kinded
127    /// predicates), or not computed (e.g. on parameters that Charon invents).
128    #[cfg_attr(feature = "charon_on_charon", charon::rename("VaUnknown"))]
129    Unknown,
130}
131
132/// A type variable in a signature or binder.
133#[derive(
134    Debug,
135    Clone,
136    PartialEq,
137    Eq,
138    PartialOrd,
139    Ord,
140    Hash,
141    Serialize,
142    Deserialize,
143    Drive,
144    DriveMut,
145    DriveTwo,
146)]
147pub struct TypeParam {
148    /// Index identifying the variable among other variables bound at the same level.
149    pub index: TypeVarId,
150    /// Variable name
151    pub name: String,
152    /// Variance of this parameter.
153    pub variance: Variance,
154}
155
156/// A region variable in a signature or binder.
157#[derive(
158    Debug,
159    Clone,
160    PartialEq,
161    Eq,
162    PartialOrd,
163    Ord,
164    Hash,
165    Serialize,
166    Deserialize,
167    Drive,
168    DriveMut,
169    DriveTwo,
170)]
171pub struct RegionParam {
172    /// Index identifying the variable among other variables bound at the same level.
173    pub index: RegionId,
174    /// Region name
175    pub name: Option<String>,
176    /// Variance of this parameter.
177    pub variance: Variance,
178    /// Whether this lifetime is (recursively) used in a `&'a mut T` type. Only `true` if this
179    /// lifetime parameter belongs to an ADT. This is a global analysis that looks even into opaque
180    /// items. When unsure, err on the side of assuming mutability.
181    pub mutability: LifetimeMutability,
182}
183
184/// The nature of locations where a given lifetime parameter is used. If this lifetime ever flows
185/// to be used as the lifetime of a mutable reference `&'a mut` then we consider it mutable.
186#[derive(
187    Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize, EnumIsA,
188)]
189#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Lt"))]
190pub enum LifetimeMutability {
191    /// A lifetime that is used for a mutable reference.
192    Mutable,
193    /// A lifetime used only in shared references.
194    Shared,
195    /// A lifetime for which we couldn't/didn't compute mutability.
196    Unknown,
197}
198
199/// A const generic variable in a signature or binder.
200#[derive(
201    Debug,
202    Clone,
203    PartialEq,
204    Eq,
205    PartialOrd,
206    Ord,
207    Hash,
208    SerializeState,
209    DeserializeState,
210    Drive,
211    DriveMut,
212    DriveTwo,
213)]
214pub struct ConstGenericParam {
215    /// Index identifying the variable among other variables bound at the same level.
216    pub index: ConstGenericVarId,
217    /// Const generic name
218    pub name: String,
219    /// Type of the const generic
220    pub ty: Ty,
221}
222
223/// A trait predicate in a signature, of the form `Type: Trait<Args>`. This functions like a
224/// variable binder, to which variables of the form `TraitRefKind::Clause` can refer to.
225#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
226pub struct TraitParam {
227    /// Index identifying the clause among other clauses bound at the same level.
228    pub clause_id: TraitClauseId,
229    // TODO: does not need to be an option.
230    pub span: Option<Span>,
231    /// Where the predicate was written, relative to the item that requires it.
232    pub origin: PredicateOrigin,
233    /// The trait that is implemented.
234    #[cfg_attr(feature = "charon_on_charon", charon::rename("trait"))]
235    pub trait_: PolyTraitDeclRef,
236}
237
238/// Where a given predicate came from.
239#[derive(
240    Debug,
241    Clone,
242    PartialEq,
243    Eq,
244    PartialOrd,
245    Ord,
246    Hash,
247    SerializeState,
248    DeserializeState,
249    Drive,
250    DriveMut,
251    DriveTwo,
252)]
253pub enum PredicateOrigin {
254    // Note: we use this for globals too, but that's only available with an unstable feature.
255    // ```
256    // fn function<T: Clone>() {}
257    // fn function<T>() where T: Clone {}
258    // const NONE<T: Copy>: Option<T> = None;
259    // ```
260    WhereClauseOnFn,
261    // ```
262    // struct Struct<T: Clone> {}
263    // struct Struct<T> where T: Clone {}
264    // type TypeAlias<T: Clone> = ...;
265    // ```
266    WhereClauseOnType,
267    // Note: this is both trait impls and inherent impl blocks.
268    // ```
269    // impl<T: Clone> Type<T> {}
270    // impl<T> Type<T> where T: Clone {}
271    // impl<T> Trait for Type<T> where T: Clone {}
272    // ```
273    WhereClauseOnImpl,
274    // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
275    // implementation of it.
276    // ```
277    // trait Trait {}
278    // ```
279    TraitSelf,
280    // Note: this also includes supertrait constraints.
281    // ```
282    // trait Trait<T: Clone> {}
283    // trait Trait<T> where T: Clone {}
284    // trait Trait: Clone {}
285    // ```
286    WhereClauseOnTrait,
287    // ```
288    // trait Trait {
289    //     type AssocType: Clone;
290    // }
291    // ```
292    TraitItem(AssocTypeId),
293    /// Clauses that are part of a `dyn Trait` type.
294    #[cfg_attr(feature = "charon_on_charon", charon::rename("OriginDyn"))]
295    Dyn,
296}
297
298impl TypeParam {
299    pub fn new(index: TypeVarId, name: String, variance: Variance) -> Self {
300        Self {
301            index,
302            name,
303            variance,
304        }
305    }
306}
307
308impl RegionParam {
309    pub fn new(index: RegionId, name: Option<String>, variance: Variance) -> Self {
310        Self {
311            index,
312            name,
313            variance,
314            mutability: LifetimeMutability::Unknown,
315        }
316    }
317}
318
319impl ConstGenericParam {
320    pub fn new(index: ConstGenericVarId, name: String, ty: Ty) -> Self {
321        Self { index, name, ty }
322    }
323}
324
325impl TraitParam {
326    /// Constructs the trait ref that refers to this clause.
327    pub fn identity_tref(&self) -> TraitRef {
328        self.identity_tref_at_depth(DeBruijnId::zero())
329    }
330
331    /// Like `identity_tref` but uses variables bound at the given depth.
332    pub fn identity_tref_at_depth(&self, depth: DeBruijnId) -> TraitRef {
333        TraitRef::new(
334            TraitRefKind::Clause(DeBruijnVar::bound(depth, self.clause_id)),
335            self.trait_.clone().move_under_binders(depth),
336        )
337    }
338}
339
340impl PartialEq for TraitParam {
341    fn eq(&self, other: &Self) -> bool {
342        // Skip `span` and `origin`
343        self.clause_id == other.clause_id && self.trait_ == other.trait_
344    }
345}
346
347impl Eq for TraitParam {}
348
349impl PartialOrd for TraitParam {
350    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
351        Some(self.cmp(other))
352    }
353}
354
355impl Ord for TraitParam {
356    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
357        (&self.clause_id, &self.trait_).cmp(&(&other.clause_id, &other.trait_))
358    }
359}
360
361impl std::hash::Hash for TraitParam {
362    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
363        self.clause_id.hash(state);
364        self.trait_.hash(state);
365    }
366}
367
368pub type RegionDbVar = DeBruijnVar<RegionId>;
369pub type TypeDbVar = DeBruijnVar<TypeVarId>;
370pub type ConstGenericDbVar = DeBruijnVar<ConstGenericVarId>;
371pub type ClauseDbVar = DeBruijnVar<TraitClauseId>;
372
373impl_from_enum!(Region::Var(RegionDbVar));
374impl_from_enum!(TyKind::TypeVar(TypeDbVar));
375impl_from_enum!(ConstantExprKind::Var(ConstGenericDbVar));
376impl_from_enum!(TraitRefKind::Clause(ClauseDbVar));
377impl From<TypeDbVar> for Ty {
378    fn from(x: TypeDbVar) -> Self {
379        TyKind::TypeVar(x).into_ty()
380    }
381}
382
383impl DeBruijnId {
384    pub fn zero() -> Self {
385        DeBruijnId { index: 0 }
386    }
387
388    pub fn one() -> Self {
389        DeBruijnId { index: 1 }
390    }
391
392    pub fn new(index: usize) -> Self {
393        DeBruijnId { index }
394    }
395
396    pub fn is_zero(&self) -> bool {
397        self.index == 0
398    }
399
400    pub fn incr(&self) -> Self {
401        DeBruijnId {
402            index: self.index + 1,
403        }
404    }
405
406    pub fn decr(&self) -> Self {
407        DeBruijnId {
408            index: self.index - 1,
409        }
410    }
411
412    pub fn plus(&self, delta: Self) -> Self {
413        DeBruijnId {
414            index: self.index + delta.index,
415        }
416    }
417
418    pub fn sub(&self, delta: Self) -> Option<Self> {
419        Some(DeBruijnId {
420            index: self.index.checked_sub(delta.index)?,
421        })
422    }
423}
424
425impl<Id> DeBruijnVar<Id>
426where
427    Id: Copy,
428{
429    pub fn new_at_zero(id: Id) -> Self {
430        DeBruijnVar::Bound(DeBruijnId::new(0), id)
431    }
432
433    pub fn free(id: Id) -> Self {
434        DeBruijnVar::Free(id)
435    }
436
437    pub fn bound(index: DeBruijnId, id: Id) -> Self {
438        DeBruijnVar::Bound(index, id)
439    }
440
441    pub fn incr(&self) -> Self {
442        match *self {
443            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.incr(), varid),
444            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
445        }
446    }
447
448    pub fn decr(&self) -> Self {
449        match *self {
450            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid),
451            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
452        }
453    }
454
455    /// Returns the variable id if it is bound as the given depth.
456    pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option<Id> {
457        match *self {
458            DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid),
459            _ => None,
460        }
461    }
462    /// Returns the variable id if it is bound as the given depth.
463    pub fn bound_at_depth_mut(&mut self, depth: DeBruijnId) -> Option<&mut Id> {
464        match self {
465            DeBruijnVar::Bound(dbid, varid) if *dbid == depth => Some(varid),
466            _ => None,
467        }
468    }
469
470    /// Move the variable out of `depth` binders. Returns `None` if the variable is bound in one of
471    /// these `depth` binders.
472    pub fn move_out_from_depth(&self, depth: DeBruijnId) -> Option<Self> {
473        Some(match *self {
474            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.sub(depth)?, varid),
475            DeBruijnVar::Free(_) => *self,
476        })
477    }
478
479    /// Move under `depth` binders.
480    pub fn move_under_binders(&self, depth: DeBruijnId) -> Self {
481        match *self {
482            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.plus(depth), varid),
483            DeBruijnVar::Free(_) => *self,
484        }
485    }
486}
487
488impl Default for DeBruijnId {
489    fn default() -> Self {
490        Self::zero()
491    }
492}
493
494/// A stack of values corresponding to nested binders. Each binder introduces an entry in this
495/// stack, with the entry as index `0` being the innermost binder. This is indexed by
496/// `DeBruijnId`s.
497/// Most methods assume that the stack is non-empty and panic if not.
498#[derive(Clone, Hash)]
499pub struct BindingStack<T> {
500    /// The stack, stored in reverse. We push/pop to the end of the `Vec`, and the last pushed
501    /// value (i.e. the end of the vec) is considered index 0.
502    stack: Vec<T>,
503}
504
505impl<T> BindingStack<T> {
506    pub fn new(x: T) -> Self {
507        Self { stack: vec![x] }
508    }
509    /// Creates an empty stack. Beware, a number of method calls will panic on an empty stack.
510    pub fn empty() -> Self {
511        Self { stack: vec![] }
512    }
513
514    pub fn is_empty(&self) -> bool {
515        self.stack.is_empty()
516    }
517    pub fn len(&self) -> usize {
518        self.stack.len()
519    }
520    pub fn depth(&self) -> DeBruijnId {
521        DeBruijnId::new(self.stack.len() - 1)
522    }
523    /// Map a bound variable to ids binding depth.
524    pub fn as_bound_var<Id>(&self, var: DeBruijnVar<Id>) -> (DeBruijnId, Id) {
525        match var {
526            DeBruijnVar::Bound(dbid, varid) => (dbid, varid),
527            DeBruijnVar::Free(varid) => (self.depth(), varid),
528        }
529    }
530    pub fn push(&mut self, x: T) {
531        self.stack.push(x);
532    }
533    pub fn pop(&mut self) -> Option<T> {
534        self.stack.pop()
535    }
536    /// Helper that computes the real index into `self.stack`.
537    fn real_index(&self, id: DeBruijnId) -> Option<usize> {
538        self.stack.len().checked_sub(id.index + 1)
539    }
540    pub fn get(&self, id: DeBruijnId) -> Option<&T> {
541        self.stack.get(self.real_index(id)?)
542    }
543    pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar<Id>) -> Option<&'a Inner::Output>
544    where
545        T: Borrow<Inner>,
546        Inner: HasIdxVecOf<Id> + 'a,
547    {
548        let (dbid, varid) = self.as_bound_var(var);
549        self.get(dbid)
550            .and_then(|x| x.borrow().get_idx_vec().get(varid))
551    }
552    pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> {
553        let index = self.real_index(id)?;
554        self.stack.get_mut(index)
555    }
556    /// Iterate over the binding levels, from the innermost (0) out.
557    pub fn iter(&self) -> impl DoubleEndedIterator<Item = &T> + ExactSizeIterator {
558        self.stack.iter().rev()
559    }
560    /// Iterate over the binding levels, from the innermost (0) out.
561    pub fn iter_enumerated(
562        &self,
563    ) -> impl DoubleEndedIterator<Item = (DeBruijnId, &T)> + ExactSizeIterator {
564        self.iter()
565            .enumerate()
566            .map(|(i, x)| (DeBruijnId::new(i), x))
567    }
568    pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack<U> {
569        BindingStack {
570            stack: self.stack.iter().map(f).collect(),
571        }
572    }
573
574    pub fn innermost(&self) -> &T {
575        self.stack.last().unwrap()
576    }
577    pub fn innermost_mut(&mut self) -> &mut T {
578        self.stack.last_mut().unwrap()
579    }
580    pub fn outermost(&self) -> &T {
581        self.stack.first().unwrap()
582    }
583    pub fn outermost_mut(&mut self) -> &mut T {
584        self.stack.first_mut().unwrap()
585    }
586}
587
588impl<T> Default for BindingStack<T> {
589    fn default() -> Self {
590        Self {
591            stack: Default::default(),
592        }
593    }
594}
595
596impl<T: std::fmt::Debug> std::fmt::Debug for BindingStack<T> {
597    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
598        write!(f, "{:?}", self.stack)
599    }
600}
601
602impl<T> Index<DeBruijnId> for BindingStack<T> {
603    type Output = T;
604    fn index(&self, id: DeBruijnId) -> &Self::Output {
605        self.get(id).unwrap()
606    }
607}
608impl<T> IndexMut<DeBruijnId> for BindingStack<T> {
609    fn index_mut(&mut self, id: DeBruijnId) -> &mut Self::Output {
610        self.get_mut(id).unwrap()
611    }
612}
charon_lib/ast/type_level/vars.rs

charon_lib/ast/type_level/
vars.rs
