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

charon_lib/ast/type_level/
vars.rs
