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

charon_lib/ast/type_level/
vars.rs
