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

charon_lib/ast/types/
vars.rs
