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

charon_lib/ast/types/
vars.rs
