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};
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)]
30#[serde(transparent)]
31#[drive(skip)]
32pub struct DeBruijnId {
33    pub index: usize,
34}
35
36impl DeBruijnId {
37    pub const ZERO: DeBruijnId = DeBruijnId { index: 0 };
38}
39
40/// Type-level variable.
41///
42/// Variables are bound in groups. Each item has a top-level binding group in its `generic_params`
43/// field, and then inner binders are possible using the `RegionBinder<T>` and `Binder<T>` types.
44/// Each variable is linked to exactly one binder. The `Id` then identifies the specific variable
45/// among all those bound in that group.
46///
47/// For instance, we have the following:
48/// ```text
49/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
50///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
51///        |       inner binder  |       |     inner binder  |        |        |
52///  top-level binder            |       |                   |        |        |
53///                        Bound(1, b)   |              Bound(2, b)   |     Bound(0, d)
54///                                      |                            |
55///                                  Bound(0, c)                 Bound(1, c)
56/// ```
57///
58/// To make consumption easier for projects that don't do heavy substitution, `--unbind-item-vars`
59/// changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be
60/// `Free`. The example above becomes:
61/// ```text
62/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
63///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
64///        |       inner binder  |       |     inner binder  |        |        |
65///  top-level binder            |       |                   |        |        |
66///                           Free(b)    |                Free(b)     |     Bound(0, d)
67///                                      |                            |
68///                                  Bound(0, c)                 Bound(1, c)
69/// ```
70#[derive(
71    Debug,
72    PartialEq,
73    Eq,
74    Copy,
75    Clone,
76    Hash,
77    PartialOrd,
78    Ord,
79    SerializeState,
80    DeserializeState,
81    Drive,
82    DriveMut,
83)]
84pub enum DeBruijnVar<Id> {
85    /// A variable attached to the nth binder, counting from the innermost.
86    Bound(#[serde_state(stateless)] DeBruijnId, Id),
87    /// A variable attached to the outermost binder (the one on the item). This is not used within
88    /// Charon itself, instead ewe insert it at the end if `--unbind-item-vars` is set.
89    Free(Id),
90}
91
92// We need to manipulate a lot of indices for the types, variables, definitions, etc. In order not
93// to confuse them, we define an index type for every one of them (which is just a struct with a
94// unique usize field), together with some utilities like a fresh index generator, using the
95// `generate_index_type` macro.
96generate_index_type!(RegionId, "Region");
97generate_index_type!(TypeVarId, "T");
98generate_index_type!(ConstGenericVarId, "Const");
99generate_index_type!(TraitClauseId, "TraitClause");
100generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");
101
102/// A type variable in a signature or binder.
103#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
104pub struct TypeParam {
105    /// Index identifying the variable among other variables bound at the same level.
106    pub index: TypeVarId,
107    /// Variable name
108    #[drive(skip)]
109    pub name: String,
110}
111
112/// A region variable in a signature or binder.
113#[derive(
114    Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize, Drive, DriveMut,
115)]
116pub struct RegionParam {
117    /// Index identifying the variable among other variables bound at the same level.
118    pub index: RegionId,
119    /// Region name
120    #[drive(skip)]
121    pub name: Option<String>,
122    /// Whether this lifetime is (recursively) used in a `&'a mut T` type. Only `true` if this
123    /// lifetime parameter belongs to an ADT. This is a global analysis that looks even into opaque
124    /// items. When unsure, err on the side of assuming mutability.
125    #[drive(skip)]
126    pub mutability: LifetimeMutability,
127}
128
129/// A const generic variable in a signature or binder.
130#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
131pub struct ConstGenericParam {
132    /// Index identifying the variable among other variables bound at the same level.
133    pub index: ConstGenericVarId,
134    /// Const generic name
135    #[drive(skip)]
136    pub name: String,
137    /// Type of the const generic
138    pub ty: Ty,
139}
140
141/// A trait predicate in a signature, of the form `Type: Trait<Args>`. This functions like a
142/// variable binder, to which variables of the form `TraitRefKind::Clause` can refer to.
143#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
144pub struct TraitParam {
145    /// Index identifying the clause among other clauses bound at the same level.
146    pub clause_id: TraitClauseId,
147    // TODO: does not need to be an option.
148    pub span: Option<Span>,
149    /// Where the predicate was written, relative to the item that requires it.
150    #[drive(skip)]
151    pub origin: PredicateOrigin,
152    /// The trait that is implemented.
153    #[charon::rename("trait")]
154    pub trait_: PolyTraitDeclRef,
155}
156
157impl PartialEq for TraitParam {
158    fn eq(&self, other: &Self) -> bool {
159        // Skip `span` and `origin`
160        self.clause_id == other.clause_id && self.trait_ == other.trait_
161    }
162}
163
164impl std::hash::Hash for TraitParam {
165    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
166        self.clause_id.hash(state);
167        self.trait_.hash(state);
168    }
169}
170
171pub type RegionDbVar = DeBruijnVar<RegionId>;
172pub type TypeDbVar = DeBruijnVar<TypeVarId>;
173pub type ConstGenericDbVar = DeBruijnVar<ConstGenericVarId>;
174pub type ClauseDbVar = DeBruijnVar<TraitClauseId>;
175
176impl_from_enum!(Region::Var(RegionDbVar));
177impl_from_enum!(TyKind::TypeVar(TypeDbVar));
178impl_from_enum!(ConstantExprKind::Var(ConstGenericDbVar));
179impl_from_enum!(TraitRefKind::Clause(ClauseDbVar));
180impl From<TypeDbVar> for Ty {
181    fn from(x: TypeDbVar) -> Self {
182        TyKind::TypeVar(x).into_ty()
183    }
184}
185
186impl DeBruijnId {
187    pub fn zero() -> Self {
188        DeBruijnId { index: 0 }
189    }
190
191    pub fn one() -> Self {
192        DeBruijnId { index: 1 }
193    }
194
195    pub fn new(index: usize) -> Self {
196        DeBruijnId { index }
197    }
198
199    pub fn is_zero(&self) -> bool {
200        self.index == 0
201    }
202
203    pub fn incr(&self) -> Self {
204        DeBruijnId {
205            index: self.index + 1,
206        }
207    }
208
209    pub fn decr(&self) -> Self {
210        DeBruijnId {
211            index: self.index - 1,
212        }
213    }
214
215    pub fn plus(&self, delta: Self) -> Self {
216        DeBruijnId {
217            index: self.index + delta.index,
218        }
219    }
220
221    pub fn sub(&self, delta: Self) -> Option<Self> {
222        Some(DeBruijnId {
223            index: self.index.checked_sub(delta.index)?,
224        })
225    }
226}
227
228impl<Id> DeBruijnVar<Id>
229where
230    Id: Copy,
231{
232    pub fn new_at_zero(id: Id) -> Self {
233        DeBruijnVar::Bound(DeBruijnId::new(0), id)
234    }
235
236    pub fn free(id: Id) -> Self {
237        DeBruijnVar::Free(id)
238    }
239
240    pub fn bound(index: DeBruijnId, id: Id) -> Self {
241        DeBruijnVar::Bound(index, id)
242    }
243
244    pub fn incr(&self) -> Self {
245        match *self {
246            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.incr(), varid),
247            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
248        }
249    }
250
251    pub fn decr(&self) -> Self {
252        match *self {
253            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid),
254            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
255        }
256    }
257
258    /// Returns the variable id if it is bound as the given depth.
259    pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option<Id> {
260        match *self {
261            DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid),
262            _ => None,
263        }
264    }
265    /// Returns the variable id if it is bound as the given depth.
266    pub fn bound_at_depth_mut(&mut self, depth: DeBruijnId) -> Option<&mut Id> {
267        match self {
268            DeBruijnVar::Bound(dbid, varid) if *dbid == depth => Some(varid),
269            _ => None,
270        }
271    }
272
273    /// Move the variable out of `depth` binders. Returns `None` if the variable is bound in one of
274    /// these `depth` binders.
275    pub fn move_out_from_depth(&self, depth: DeBruijnId) -> Option<Self> {
276        Some(match *self {
277            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.sub(depth)?, varid),
278            DeBruijnVar::Free(_) => *self,
279        })
280    }
281
282    /// Move under `depth` binders.
283    pub fn move_under_binders(&self, depth: DeBruijnId) -> Self {
284        match *self {
285            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.plus(depth), varid),
286            DeBruijnVar::Free(_) => *self,
287        }
288    }
289}
290
291impl TypeParam {
292    pub fn new(index: TypeVarId, name: String) -> Self {
293        Self { index, name }
294    }
295}
296
297impl RegionParam {
298    pub fn new(index: RegionId, name: Option<String>) -> Self {
299        Self {
300            index,
301            name,
302            mutability: LifetimeMutability::Unknown,
303        }
304    }
305}
306
307impl ConstGenericParam {
308    pub fn new(index: ConstGenericVarId, name: String, ty: Ty) -> Self {
309        Self { index, name, ty }
310    }
311}
312
313impl Default for DeBruijnId {
314    fn default() -> Self {
315        Self::zero()
316    }
317}
318
319/// A stack of values corresponding to nested binders. Each binder introduces an entry in this
320/// stack, with the entry as index `0` being the innermost binder. This is indexed by
321/// `DeBruijnId`s.
322/// Most methods assume that the stack is non-empty and panic if not.
323#[derive(Clone, Hash)]
324pub struct BindingStack<T> {
325    /// The stack, stored in reverse. We push/pop to the end of the `Vec`, and the last pushed
326    /// value (i.e. the end of the vec) is considered index 0.
327    stack: Vec<T>,
328}
329
330impl<T> BindingStack<T> {
331    pub fn new(x: T) -> Self {
332        Self { stack: vec![x] }
333    }
334    /// Creates an empty stack. Beware, a number of method calls will panic on an empty stack.
335    pub fn empty() -> Self {
336        Self { stack: vec![] }
337    }
338
339    pub fn is_empty(&self) -> bool {
340        self.stack.is_empty()
341    }
342    pub fn len(&self) -> usize {
343        self.stack.len()
344    }
345    pub fn depth(&self) -> DeBruijnId {
346        DeBruijnId::new(self.stack.len() - 1)
347    }
348    /// Map a bound variable to ids binding depth.
349    pub fn as_bound_var<Id>(&self, var: DeBruijnVar<Id>) -> (DeBruijnId, Id) {
350        match var {
351            DeBruijnVar::Bound(dbid, varid) => (dbid, varid),
352            DeBruijnVar::Free(varid) => (self.depth(), varid),
353        }
354    }
355    pub fn push(&mut self, x: T) {
356        self.stack.push(x);
357    }
358    pub fn pop(&mut self) -> Option<T> {
359        self.stack.pop()
360    }
361    /// Helper that computes the real index into `self.stack`.
362    fn real_index(&self, id: DeBruijnId) -> Option<usize> {
363        self.stack.len().checked_sub(id.index + 1)
364    }
365    pub fn get(&self, id: DeBruijnId) -> Option<&T> {
366        self.stack.get(self.real_index(id)?)
367    }
368    pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar<Id>) -> Option<&'a Inner::Output>
369    where
370        T: Borrow<Inner>,
371        Inner: HasIdxVecOf<Id> + 'a,
372    {
373        let (dbid, varid) = self.as_bound_var(var);
374        self.get(dbid)
375            .and_then(|x| x.borrow().get_idx_vec().get(varid))
376    }
377    pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> {
378        let index = self.real_index(id)?;
379        self.stack.get_mut(index)
380    }
381    /// Iterate over the binding levels, from the innermost (0) out.
382    pub fn iter(&self) -> impl DoubleEndedIterator<Item = &T> + ExactSizeIterator {
383        self.stack.iter().rev()
384    }
385    /// Iterate over the binding levels, from the innermost (0) out.
386    pub fn iter_enumerated(
387        &self,
388    ) -> impl DoubleEndedIterator<Item = (DeBruijnId, &T)> + ExactSizeIterator {
389        self.iter()
390            .enumerate()
391            .map(|(i, x)| (DeBruijnId::new(i), x))
392    }
393    pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack<U> {
394        BindingStack {
395            stack: self.stack.iter().map(f).collect(),
396        }
397    }
398
399    pub fn innermost(&self) -> &T {
400        self.stack.last().unwrap()
401    }
402    pub fn innermost_mut(&mut self) -> &mut T {
403        self.stack.last_mut().unwrap()
404    }
405    pub fn outermost(&self) -> &T {
406        self.stack.first().unwrap()
407    }
408    pub fn outermost_mut(&mut self) -> &mut T {
409        self.stack.first_mut().unwrap()
410    }
411}
412
413impl<T> Default for BindingStack<T> {
414    fn default() -> Self {
415        Self {
416            stack: Default::default(),
417        }
418    }
419}
420
421impl<T: std::fmt::Debug> std::fmt::Debug for BindingStack<T> {
422    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
423        write!(f, "{:?}", self.stack)
424    }
425}
426
427impl<T> Index<DeBruijnId> for BindingStack<T> {
428    type Output = T;
429    fn index(&self, id: DeBruijnId) -> &Self::Output {
430        self.get(id).unwrap()
431    }
432}
433impl<T> IndexMut<DeBruijnId> for BindingStack<T> {
434    fn index_mut(&mut self, id: DeBruijnId) -> &mut Self::Output {
435        self.get_mut(id).unwrap()
436    }
437}
charon_lib/ast/types/vars.rs

charon_lib/ast/types/
vars.rs
