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

charon_lib/ast/types/
vars.rs
