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

charon_lib/ast/types/
vars.rs
