charon_lib/ast/types/
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 serde::{Deserialize, Serialize};
11use serde_state::{DeserializeState, SerializeState};
12
13use crate::{ast::*, impl_from_enum};
14
15/// The index of a binder, counting from the innermost. See [`DeBruijnVar`] for details.
16#[derive(
17    Debug,
18    PartialEq,
19    Eq,
20    Copy,
21    Clone,
22    Hash,
23    PartialOrd,
24    Ord,
25    Serialize,
26    Deserialize,
27    Drive,
28    DriveMut,
29    DriveTwo,
30)]
31#[serde(transparent)]
32#[cfg_attr(feature = "charon_on_charon", charon::transparent)]
33#[drive(skip)]
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    #[drive(skip)]
152    pub name: String,
153    /// Variance of this parameter.
154    #[drive(skip)]
155    pub variance: Variance,
156}
157
158/// A region variable in a signature or binder.
159#[derive(
160    Debug,
161    Clone,
162    PartialEq,
163    Eq,
164    PartialOrd,
165    Ord,
166    Hash,
167    Serialize,
168    Deserialize,
169    Drive,
170    DriveMut,
171    DriveTwo,
172)]
173pub struct RegionParam {
174    /// Index identifying the variable among other variables bound at the same level.
175    pub index: RegionId,
176    /// Region name
177    #[drive(skip)]
178    pub name: Option<String>,
179    /// Variance of this parameter.
180    #[drive(skip)]
181    pub variance: Variance,
182    /// Whether this lifetime is (recursively) used in a `&'a mut T` type. Only `true` if this
183    /// lifetime parameter belongs to an ADT. This is a global analysis that looks even into opaque
184    /// items. When unsure, err on the side of assuming mutability.
185    #[drive(skip)]
186    pub mutability: LifetimeMutability,
187}
188
189/// A const generic variable in a signature or binder.
190#[derive(
191    Debug,
192    Clone,
193    PartialEq,
194    Eq,
195    PartialOrd,
196    Ord,
197    Hash,
198    SerializeState,
199    DeserializeState,
200    Drive,
201    DriveMut,
202    DriveTwo,
203)]
204pub struct ConstGenericParam {
205    /// Index identifying the variable among other variables bound at the same level.
206    pub index: ConstGenericVarId,
207    /// Const generic name
208    #[drive(skip)]
209    pub name: String,
210    /// Type of the const generic
211    pub ty: Ty,
212}
213
214/// A trait predicate in a signature, of the form `Type: Trait<Args>`. This functions like a
215/// variable binder, to which variables of the form `TraitRefKind::Clause` can refer to.
216#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
217pub struct TraitParam {
218    /// Index identifying the clause among other clauses bound at the same level.
219    pub clause_id: TraitClauseId,
220    // TODO: does not need to be an option.
221    pub span: Option<Span>,
222    /// Where the predicate was written, relative to the item that requires it.
223    #[drive(skip)]
224    pub origin: PredicateOrigin,
225    /// The trait that is implemented.
226    #[cfg_attr(feature = "charon_on_charon", charon::rename("trait"))]
227    pub trait_: PolyTraitDeclRef,
228}
229
230impl PartialEq for TraitParam {
231    fn eq(&self, other: &Self) -> bool {
232        // Skip `span` and `origin`
233        self.clause_id == other.clause_id && self.trait_ == other.trait_
234    }
235}
236
237impl PartialOrd for TraitParam {
238    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
239        Some(self.cmp(other))
240    }
241}
242
243impl Ord for TraitParam {
244    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
245        (&self.clause_id, &self.trait_).cmp(&(&other.clause_id, &other.trait_))
246    }
247}
248
249impl std::hash::Hash for TraitParam {
250    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
251        self.clause_id.hash(state);
252        self.trait_.hash(state);
253    }
254}
255
256pub type RegionDbVar = DeBruijnVar<RegionId>;
257pub type TypeDbVar = DeBruijnVar<TypeVarId>;
258pub type ConstGenericDbVar = DeBruijnVar<ConstGenericVarId>;
259pub type ClauseDbVar = DeBruijnVar<TraitClauseId>;
260
261impl_from_enum!(Region::Var(RegionDbVar));
262impl_from_enum!(TyKind::TypeVar(TypeDbVar));
263impl_from_enum!(ConstantExprKind::Var(ConstGenericDbVar));
264impl_from_enum!(TraitRefKind::Clause(ClauseDbVar));
265impl From<TypeDbVar> for Ty {
266    fn from(x: TypeDbVar) -> Self {
267        TyKind::TypeVar(x).into_ty()
268    }
269}
270
271impl DeBruijnId {
272    pub fn zero() -> Self {
273        DeBruijnId { index: 0 }
274    }
275
276    pub fn one() -> Self {
277        DeBruijnId { index: 1 }
278    }
279
280    pub fn new(index: usize) -> Self {
281        DeBruijnId { index }
282    }
283
284    pub fn is_zero(&self) -> bool {
285        self.index == 0
286    }
287
288    pub fn incr(&self) -> Self {
289        DeBruijnId {
290            index: self.index + 1,
291        }
292    }
293
294    pub fn decr(&self) -> Self {
295        DeBruijnId {
296            index: self.index - 1,
297        }
298    }
299
300    pub fn plus(&self, delta: Self) -> Self {
301        DeBruijnId {
302            index: self.index + delta.index,
303        }
304    }
305
306    pub fn sub(&self, delta: Self) -> Option<Self> {
307        Some(DeBruijnId {
308            index: self.index.checked_sub(delta.index)?,
309        })
310    }
311}
312
313impl<Id> DeBruijnVar<Id>
314where
315    Id: Copy,
316{
317    pub fn new_at_zero(id: Id) -> Self {
318        DeBruijnVar::Bound(DeBruijnId::new(0), id)
319    }
320
321    pub fn free(id: Id) -> Self {
322        DeBruijnVar::Free(id)
323    }
324
325    pub fn bound(index: DeBruijnId, id: Id) -> Self {
326        DeBruijnVar::Bound(index, id)
327    }
328
329    pub fn incr(&self) -> Self {
330        match *self {
331            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.incr(), varid),
332            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
333        }
334    }
335
336    pub fn decr(&self) -> Self {
337        match *self {
338            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid),
339            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
340        }
341    }
342
343    /// Returns the variable id if it is bound as the given depth.
344    pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option<Id> {
345        match *self {
346            DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid),
347            _ => None,
348        }
349    }
350    /// Returns the variable id if it is bound as the given depth.
351    pub fn bound_at_depth_mut(&mut self, depth: DeBruijnId) -> Option<&mut Id> {
352        match self {
353            DeBruijnVar::Bound(dbid, varid) if *dbid == depth => Some(varid),
354            _ => None,
355        }
356    }
357
358    /// Move the variable out of `depth` binders. Returns `None` if the variable is bound in one of
359    /// these `depth` binders.
360    pub fn move_out_from_depth(&self, depth: DeBruijnId) -> Option<Self> {
361        Some(match *self {
362            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.sub(depth)?, varid),
363            DeBruijnVar::Free(_) => *self,
364        })
365    }
366
367    /// Move under `depth` binders.
368    pub fn move_under_binders(&self, depth: DeBruijnId) -> Self {
369        match *self {
370            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.plus(depth), varid),
371            DeBruijnVar::Free(_) => *self,
372        }
373    }
374}
375
376impl TypeParam {
377    pub fn new(index: TypeVarId, name: String, variance: Variance) -> Self {
378        Self {
379            index,
380            name,
381            variance,
382        }
383    }
384}
385
386impl RegionParam {
387    pub fn new(index: RegionId, name: Option<String>, variance: Variance) -> Self {
388        Self {
389            index,
390            name,
391            variance,
392            mutability: LifetimeMutability::Unknown,
393        }
394    }
395}
396
397impl ConstGenericParam {
398    pub fn new(index: ConstGenericVarId, name: String, ty: Ty) -> Self {
399        Self { index, name, ty }
400    }
401}
402
403impl Default for DeBruijnId {
404    fn default() -> Self {
405        Self::zero()
406    }
407}
408
409/// A stack of values corresponding to nested binders. Each binder introduces an entry in this
410/// stack, with the entry as index `0` being the innermost binder. This is indexed by
411/// `DeBruijnId`s.
412/// Most methods assume that the stack is non-empty and panic if not.
413#[derive(Clone, Hash)]
414pub struct BindingStack<T> {
415    /// The stack, stored in reverse. We push/pop to the end of the `Vec`, and the last pushed
416    /// value (i.e. the end of the vec) is considered index 0.
417    stack: Vec<T>,
418}
419
420impl<T> BindingStack<T> {
421    pub fn new(x: T) -> Self {
422        Self { stack: vec![x] }
423    }
424    /// Creates an empty stack. Beware, a number of method calls will panic on an empty stack.
425    pub fn empty() -> Self {
426        Self { stack: vec![] }
427    }
428
429    pub fn is_empty(&self) -> bool {
430        self.stack.is_empty()
431    }
432    pub fn len(&self) -> usize {
433        self.stack.len()
434    }
435    pub fn depth(&self) -> DeBruijnId {
436        DeBruijnId::new(self.stack.len() - 1)
437    }
438    /// Map a bound variable to ids binding depth.
439    pub fn as_bound_var<Id>(&self, var: DeBruijnVar<Id>) -> (DeBruijnId, Id) {
440        match var {
441            DeBruijnVar::Bound(dbid, varid) => (dbid, varid),
442            DeBruijnVar::Free(varid) => (self.depth(), varid),
443        }
444    }
445    pub fn push(&mut self, x: T) {
446        self.stack.push(x);
447    }
448    pub fn pop(&mut self) -> Option<T> {
449        self.stack.pop()
450    }
451    /// Helper that computes the real index into `self.stack`.
452    fn real_index(&self, id: DeBruijnId) -> Option<usize> {
453        self.stack.len().checked_sub(id.index + 1)
454    }
455    pub fn get(&self, id: DeBruijnId) -> Option<&T> {
456        self.stack.get(self.real_index(id)?)
457    }
458    pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar<Id>) -> Option<&'a Inner::Output>
459    where
460        T: Borrow<Inner>,
461        Inner: HasIdxVecOf<Id> + 'a,
462    {
463        let (dbid, varid) = self.as_bound_var(var);
464        self.get(dbid)
465            .and_then(|x| x.borrow().get_idx_vec().get(varid))
466    }
467    pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> {
468        let index = self.real_index(id)?;
469        self.stack.get_mut(index)
470    }
471    /// Iterate over the binding levels, from the innermost (0) out.
472    pub fn iter(&self) -> impl DoubleEndedIterator<Item = &T> + ExactSizeIterator {
473        self.stack.iter().rev()
474    }
475    /// Iterate over the binding levels, from the innermost (0) out.
476    pub fn iter_enumerated(
477        &self,
478    ) -> impl DoubleEndedIterator<Item = (DeBruijnId, &T)> + ExactSizeIterator {
479        self.iter()
480            .enumerate()
481            .map(|(i, x)| (DeBruijnId::new(i), x))
482    }
483    pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack<U> {
484        BindingStack {
485            stack: self.stack.iter().map(f).collect(),
486        }
487    }
488
489    pub fn innermost(&self) -> &T {
490        self.stack.last().unwrap()
491    }
492    pub fn innermost_mut(&mut self) -> &mut T {
493        self.stack.last_mut().unwrap()
494    }
495    pub fn outermost(&self) -> &T {
496        self.stack.first().unwrap()
497    }
498    pub fn outermost_mut(&mut self) -> &mut T {
499        self.stack.first_mut().unwrap()
500    }
501}
502
503impl<T> Default for BindingStack<T> {
504    fn default() -> Self {
505        Self {
506            stack: Default::default(),
507        }
508    }
509}
510
511impl<T: std::fmt::Debug> std::fmt::Debug for BindingStack<T> {
512    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
513        write!(f, "{:?}", self.stack)
514    }
515}
516
517impl<T> Index<DeBruijnId> for BindingStack<T> {
518    type Output = T;
519    fn index(&self, id: DeBruijnId) -> &Self::Output {
520        self.get(id).unwrap()
521    }
522}
523impl<T> IndexMut<DeBruijnId> for BindingStack<T> {
524    fn index_mut(&mut self, id: DeBruijnId) -> &mut Self::Output {
525        self.get_mut(id).unwrap()
526    }
527}
charon_lib/ast/types/vars.rs

charon_lib/ast/types/
vars.rs
