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, 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
151impl PartialEq for TraitClause {
152    fn eq(&self, other: &Self) -> bool {
153        // Skip `span` and `origin`
154        self.clause_id == other.clause_id && self.trait_ == other.trait_
155    }
156}
157
158impl std::hash::Hash for TraitClause {
159    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
160        self.clause_id.hash(state);
161        self.trait_.hash(state);
162    }
163}
164
165pub type RegionDbVar = DeBruijnVar<RegionId>;
166pub type TypeDbVar = DeBruijnVar<TypeVarId>;
167pub type ConstGenericDbVar = DeBruijnVar<ConstGenericVarId>;
168pub type ClauseDbVar = DeBruijnVar<TraitClauseId>;
169
170impl DeBruijnId {
171    pub fn zero() -> Self {
172        DeBruijnId { index: 0 }
173    }
174
175    pub fn one() -> Self {
176        DeBruijnId { index: 1 }
177    }
178
179    pub fn new(index: usize) -> Self {
180        DeBruijnId { index }
181    }
182
183    pub fn is_zero(&self) -> bool {
184        self.index == 0
185    }
186
187    pub fn incr(&self) -> Self {
188        DeBruijnId {
189            index: self.index + 1,
190        }
191    }
192
193    pub fn decr(&self) -> Self {
194        DeBruijnId {
195            index: self.index - 1,
196        }
197    }
198
199    pub fn plus(&self, delta: Self) -> Self {
200        DeBruijnId {
201            index: self.index + delta.index,
202        }
203    }
204
205    pub fn sub(&self, delta: Self) -> Option<Self> {
206        Some(DeBruijnId {
207            index: self.index.checked_sub(delta.index)?,
208        })
209    }
210}
211
212impl<Id> DeBruijnVar<Id>
213where
214    Id: Copy,
215{
216    pub fn new_at_zero(id: Id) -> Self {
217        DeBruijnVar::Bound(DeBruijnId::new(0), id)
218    }
219
220    pub fn free(id: Id) -> Self {
221        DeBruijnVar::Free(id)
222    }
223
224    pub fn bound(index: DeBruijnId, id: Id) -> Self {
225        DeBruijnVar::Bound(index, id)
226    }
227
228    pub fn incr(&self) -> Self {
229        match *self {
230            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.incr(), varid),
231            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
232        }
233    }
234
235    pub fn decr(&self) -> Self {
236        match *self {
237            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid),
238            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
239        }
240    }
241
242    /// Returns the variable id if it is bound as the given depth.
243    pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option<Id> {
244        match *self {
245            DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid),
246            _ => None,
247        }
248    }
249    /// Returns the variable id if it is bound as the given depth.
250    pub fn bound_at_depth_mut(&mut self, depth: DeBruijnId) -> Option<&mut Id> {
251        match self {
252            DeBruijnVar::Bound(dbid, varid) if *dbid == depth => Some(varid),
253            _ => None,
254        }
255    }
256
257    /// Move the variable out of `depth` binders. Returns `None` if the variable is bound in one of
258    /// these `depth` binders.
259    pub fn move_out_from_depth(&self, depth: DeBruijnId) -> Option<Self> {
260        Some(match *self {
261            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.sub(depth)?, varid),
262            DeBruijnVar::Free(_) => *self,
263        })
264    }
265
266    /// Move under `depth` binders.
267    pub fn move_under_binders(&self, depth: DeBruijnId) -> Self {
268        match *self {
269            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.plus(depth), varid),
270            DeBruijnVar::Free(_) => *self,
271        }
272    }
273}
274
275impl TypeVar {
276    pub fn new(index: TypeVarId, name: String) -> TypeVar {
277        TypeVar { index, name }
278    }
279}
280
281impl Default for DeBruijnId {
282    fn default() -> Self {
283        Self::zero()
284    }
285}
286
287/// A stack of values corresponding to nested binders. Each binder introduces an entry in this
288/// stack, with the entry as index `0` being the innermost binder. This is indexed by
289/// `DeBruijnId`s.
290/// Most methods assume that the stack is non-empty and panic if not.
291#[derive(Clone, Hash)]
292pub struct BindingStack<T> {
293    /// The stack, stored in reverse. We push/pop to the end of the `Vec`, and the last pushed
294    /// value (i.e. the end of the vec) is considered index 0.
295    stack: Vec<T>,
296}
297
298impl<T> BindingStack<T> {
299    pub fn new(x: T) -> Self {
300        Self { stack: vec![x] }
301    }
302
303    pub fn is_empty(&self) -> bool {
304        self.stack.is_empty()
305    }
306    pub fn len(&self) -> usize {
307        self.stack.len()
308    }
309    pub fn depth(&self) -> DeBruijnId {
310        DeBruijnId::new(self.stack.len() - 1)
311    }
312    /// Map a bound variable to ids binding depth.
313    pub fn as_bound_var<Id>(&self, var: DeBruijnVar<Id>) -> (DeBruijnId, Id) {
314        match var {
315            DeBruijnVar::Bound(dbid, varid) => (dbid, varid),
316            DeBruijnVar::Free(varid) => (self.depth(), varid),
317        }
318    }
319    pub fn push(&mut self, x: T) {
320        self.stack.push(x);
321    }
322    pub fn pop(&mut self) -> Option<T> {
323        self.stack.pop()
324    }
325    /// Helper that computes the real index into `self.stack`.
326    fn real_index(&self, id: DeBruijnId) -> Option<usize> {
327        self.stack.len().checked_sub(id.index + 1)
328    }
329    pub fn get(&self, id: DeBruijnId) -> Option<&T> {
330        self.stack.get(self.real_index(id)?)
331    }
332    pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar<Id>) -> Option<&'a Inner::Output>
333    where
334        T: Borrow<Inner>,
335        Inner: HasVectorOf<Id> + 'a,
336    {
337        let (dbid, varid) = self.as_bound_var(var);
338        self.get(dbid)
339            .and_then(|x| x.borrow().get_vector().get(varid))
340    }
341    pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> {
342        let index = self.real_index(id)?;
343        self.stack.get_mut(index)
344    }
345    /// Iterate over the binding levels, from the innermost (0) out.
346    pub fn iter(&self) -> impl Iterator<Item = &T> + DoubleEndedIterator + ExactSizeIterator {
347        self.stack.iter().rev()
348    }
349    /// Iterate over the binding levels, from the innermost (0) out.
350    pub fn iter_enumerated(
351        &self,
352    ) -> impl Iterator<Item = (DeBruijnId, &T)> + DoubleEndedIterator + ExactSizeIterator {
353        self.iter()
354            .enumerate()
355            .map(|(i, x)| (DeBruijnId::new(i), x))
356    }
357    pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack<U> {
358        BindingStack {
359            stack: self.stack.iter().map(f).collect(),
360        }
361    }
362
363    pub fn innermost(&self) -> &T {
364        self.stack.last().unwrap()
365    }
366    pub fn innermost_mut(&mut self) -> &mut T {
367        self.stack.last_mut().unwrap()
368    }
369    pub fn outermost(&self) -> &T {
370        self.stack.first().unwrap()
371    }
372    pub fn outermost_mut(&mut self) -> &mut T {
373        self.stack.first_mut().unwrap()
374    }
375}
376
377impl<T> Default for BindingStack<T> {
378    fn default() -> Self {
379        Self {
380            stack: Default::default(),
381        }
382    }
383}
384
385impl<T: std::fmt::Debug> std::fmt::Debug for BindingStack<T> {
386    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
387        write!(f, "{:?}", self.stack)
388    }
389}
390
391impl<T> Index<DeBruijnId> for BindingStack<T> {
392    type Output = T;
393    fn index(&self, id: DeBruijnId) -> &Self::Output {
394        self.get(id).unwrap()
395    }
396}
397impl<T> IndexMut<DeBruijnId> for BindingStack<T> {
398    fn index_mut(&mut self, id: DeBruijnId) -> &mut Self::Output {
399        self.get_mut(id).unwrap()
400    }
401}
charon_lib/ast/types/vars.rs

charon_lib/ast/types/
vars.rs
