charon_lib/ast/type_level/
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::{Deref, DerefMut, Index, IndexMut, RangeFrom},
6};
7
8use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
9use index_vec::Idx;
10use macros::EnumIsA;
11use serde::{Deserialize, Serialize};
12use serde_state::{DeserializeState, SerializeState};
13
14use crate::{ast::*, impl_from_enum};
15
16/// The index of a binder, counting from the innermost. See [`DeBruijnVar`] for details.
17#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
18#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
19#[serde(transparent)]
20#[cfg_attr(feature = "charon_on_charon", charon::transparent)]
21pub struct DeBruijnId {
22    pub index: usize,
23}
24
25impl DeBruijnId {
26    pub const ZERO: DeBruijnId = DeBruijnId { index: 0 };
27}
28
29/// Type-level variable.
30///
31/// Variables are bound in binders, which each bind a set of variables. The `DeBruijnId` identifies
32/// the binder (counting outward), and the `Id` identifies the variable among all those bound at
33/// that level.
34///
35/// There are two kinds of binders: `RegionBinder`s bind only regions, and occur whenever there can
36/// be a `for<...>` in Rust, e.g. function pointers types; `Binder`s can bind any type-level
37/// variable (types, const, and trait clauses), and are used for `dyn Trait` types as well as trait
38/// methods. Each item also works as a binder, using its `generic_params` as parameters.
39///
40/// For instance, we have the following:
41/// ```text
42/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
43///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
44///        |       inner binder  |       |     inner binder  |        |        |
45///    item binder               |       |                   |        |        |
46///                        Bound(1, b)   |              Bound(2, b)   |     Bound(0, d)
47///                                      |                            |
48///                                  Bound(0, c)                 Bound(1, c)
49/// ```
50///
51/// To make consumption easier for projects that don't do heavy substitution, `--unbind-item-vars`
52/// changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be
53/// `Free`. The example above becomes:
54/// ```text
55/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
56///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
57///        |       inner binder  |       |     inner binder  |        |        |
58///  top-level binder            |       |                   |        |        |
59///                           Free(b)    |                Free(b)     |     Bound(0, d)
60///                                      |                            |
61///                                  Bound(0, c)                 Bound(1, c)
62/// ```
63#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
64#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
65pub enum DeBruijnVar<Id> {
66    /// A variable attached to the nth binder, counting from the innermost.
67    Bound(#[serde_state(stateless)] DeBruijnId, Id),
68    /// A variable not attached to a particular binder. Can be used for various purposes which
69    /// manipulating types, e.g. as inference variables or placeholders. If `--unbind-item-vars` is
70    /// set, we use `Free` variables to refer to the item binders; `Free` variables should not
71    /// otherwise be found in the output of running `charon`.
72    Free(Id),
73}
74
75// We need to manipulate a lot of indices for the types, variables, definitions, etc. In order not
76// to confuse them, we define an index type for every one of them (which is just a struct with a
77// unique usize field), together with some utilities like a fresh index generator, using the
78// `generate_index_type` macro.
79generate_index_type!(RegionId, "Region");
80generate_index_type!(TypeVarId, "T");
81generate_index_type!(ConstGenericVarId, "Const");
82generate_index_type!(TraitClauseId, "TraitClause");
83generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");
84
85/// The variance of a lifetime or type parameter.
86#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
87#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
88pub enum Variance {
89    Covariant,
90    Invariant,
91    Contravariant,
92    // TODO: when does this happen?
93    Bivariant,
94    /// Variance was not sensible (e.g. on impls), not available (e.g. on higher-kinded
95    /// predicates), or not computed (e.g. on parameters that Charon invents).
96    #[cfg_attr(feature = "charon_on_charon", charon::rename("VaUnknown"))]
97    Unknown,
98}
99
100impl Variance {
101    pub fn compose(outer: Variance, inner: Variance) -> Variance {
102        match (outer, inner) {
103            (Variance::Unknown, _) | (_, Variance::Unknown) => Variance::Unknown,
104            (Variance::Bivariant, _) | (_, Variance::Bivariant) => Variance::Bivariant,
105            (Variance::Invariant, _) | (_, Variance::Invariant) => Variance::Invariant,
106            (Variance::Covariant, variance) => variance,
107            (Variance::Contravariant, Variance::Covariant) => Variance::Contravariant,
108            (Variance::Contravariant, Variance::Contravariant) => Variance::Covariant,
109        }
110    }
111}
112
113/// A type variable in a signature or binder.
114#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
115#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
116pub struct TypeParam {
117    /// Index identifying the variable among other variables bound at the same level.
118    pub index: TypeVarId,
119    /// Variable name
120    pub name: String,
121    /// Variance of this parameter.
122    pub variance: Variance,
123}
124
125/// A region variable in a signature or binder.
126#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
127#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
128pub struct RegionParam {
129    /// Index identifying the variable among other variables bound at the same level.
130    pub index: RegionId,
131    /// Region name
132    pub name: Option<String>,
133    /// Variance of this parameter.
134    pub variance: Variance,
135    /// Whether this lifetime is (recursively) used in a `&'a mut T` type. Only `true` if this
136    /// lifetime parameter belongs to an ADT. This is a global analysis that looks even into opaque
137    /// items. When unsure, err on the side of assuming mutability.
138    pub mutability: LifetimeMutability,
139    /// Whether this region is "late bound", which means that it is unconstrained by the trait
140    /// system and thus may be used in a `for<..>` binder.
141    pub late_bound: bool,
142}
143
144/// The nature of locations where a given lifetime parameter is used. If this lifetime ever flows
145/// to be used as the lifetime of a mutable reference `&'a mut` then we consider it mutable.
146#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
147#[derive(EnumIsA)]
148#[derive(Serialize, Deserialize)]
149#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Lt"))]
150pub enum LifetimeMutability {
151    /// A lifetime that is used for a mutable reference.
152    Mutable,
153    /// A lifetime used only in shared references.
154    Shared,
155    /// A lifetime for which we couldn't/didn't compute mutability.
156    Unknown,
157}
158
159/// A const generic variable in a signature or binder.
160#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
161#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
162pub struct ConstGenericParam {
163    /// Index identifying the variable among other variables bound at the same level.
164    pub index: ConstGenericVarId,
165    /// Const generic name
166    pub name: String,
167    /// Type of the const generic
168    pub ty: Ty,
169}
170
171/// A trait predicate in a signature, of the form `Type: Trait<Args>`. This functions like a
172/// variable binder, to which variables of the form `TraitRefKind::Clause` can refer to.
173#[derive(Debug, Clone)]
174#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
175pub struct TraitParam {
176    /// Index identifying the clause among other clauses bound at the same level.
177    pub clause_id: TraitClauseId,
178    // TODO: does not need to be an option.
179    pub span: Option<Span>,
180    /// Where the predicate was written, relative to the item that requires it.
181    pub origin: PredicateOrigin,
182    /// The trait that is implemented.
183    #[cfg_attr(feature = "charon_on_charon", charon::rename("trait"))]
184    pub trait_: PolyTraitDeclRef,
185}
186
187/// Where a given predicate came from.
188#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
189#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
190pub enum PredicateOrigin {
191    // Note: we use this for globals too, but that's only available with an unstable feature.
192    // ```
193    // fn function<T: Clone>() {}
194    // fn function<T>() where T: Clone {}
195    // const NONE<T: Copy>: Option<T> = None;
196    // ```
197    WhereClauseOnFn,
198    // ```
199    // struct Struct<T: Clone> {}
200    // struct Struct<T> where T: Clone {}
201    // type TypeAlias<T: Clone> = ...;
202    // ```
203    WhereClauseOnType,
204    // Note: this is both trait impls and inherent impl blocks.
205    // ```
206    // impl<T: Clone> Type<T> {}
207    // impl<T> Type<T> where T: Clone {}
208    // impl<T> Trait for Type<T> where T: Clone {}
209    // ```
210    WhereClauseOnImpl,
211    // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
212    // implementation of it.
213    // ```
214    // trait Trait {}
215    // ```
216    TraitSelf,
217    // Note: this also includes supertrait constraints.
218    // ```
219    // trait Trait<T: Clone> {}
220    // trait Trait<T> where T: Clone {}
221    // trait Trait: Clone {}
222    // ```
223    WhereClauseOnTrait,
224    // ```
225    // trait Trait {
226    //     type AssocType: Clone;
227    // }
228    // ```
229    TraitItem(AssocTypeId),
230    /// Clauses that are part of a `dyn Trait` type.
231    #[cfg_attr(feature = "charon_on_charon", charon::rename("OriginDyn"))]
232    Dyn,
233}
234
235impl TypeParam {
236    pub fn new(index: TypeVarId, name: String, variance: Variance) -> Self {
237        Self {
238            index,
239            name,
240            variance,
241        }
242    }
243}
244
245impl RegionParam {
246    pub fn new(index: RegionId, name: Option<String>, variance: Variance) -> Self {
247        Self {
248            index,
249            name,
250            variance,
251            mutability: LifetimeMutability::Unknown,
252            late_bound: false,
253        }
254    }
255}
256
257impl ConstGenericParam {
258    pub fn new(index: ConstGenericVarId, name: String, ty: Ty) -> Self {
259        Self { index, name, ty }
260    }
261}
262
263impl TraitParam {
264    /// Constructs the trait ref that refers to this clause.
265    pub fn identity_tref(&self) -> PolyTraitRef {
266        self.identity_tref_at_depth(DeBruijnId::zero())
267    }
268
269    /// Like `identity_tref` but uses variables bound at the given depth.
270    pub fn identity_tref_at_depth(&self, depth: DeBruijnId) -> PolyTraitRef {
271        let regions = self.trait_.identity_region_args();
272        PolyTraitRef(
273            self.trait_
274                .clone()
275                .move_under_binders(depth)
276                .map(|trait_decl_ref| {
277                    TraitRef::new(
278                        TraitRefKind::Clause(
279                            DeBruijnVar::bound(depth.incr(), self.clause_id),
280                            regions,
281                        ),
282                        trait_decl_ref,
283                    )
284                }),
285        )
286    }
287}
288
289impl PartialEq for TraitParam {
290    fn eq(&self, other: &Self) -> bool {
291        // Skip `span` and `origin`
292        self.clause_id == other.clause_id && self.trait_ == other.trait_
293    }
294}
295
296impl Eq for TraitParam {}
297
298impl PartialOrd for TraitParam {
299    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
300        Some(self.cmp(other))
301    }
302}
303
304impl Ord for TraitParam {
305    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
306        (&self.clause_id, &self.trait_).cmp(&(&other.clause_id, &other.trait_))
307    }
308}
309
310impl std::hash::Hash for TraitParam {
311    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
312        self.clause_id.hash(state);
313        self.trait_.hash(state);
314    }
315}
316
317pub type RegionDbVar = DeBruijnVar<RegionId>;
318pub type TypeDbVar = DeBruijnVar<TypeVarId>;
319pub type ConstGenericDbVar = DeBruijnVar<ConstGenericVarId>;
320pub type ClauseDbVar = DeBruijnVar<TraitClauseId>;
321
322impl_from_enum!(Region::Var(RegionDbVar));
323impl_from_enum!(TyKind::TypeVar(TypeDbVar));
324impl_from_enum!(ConstantExprKind::Var(ConstGenericDbVar));
325impl From<TypeDbVar> for Ty {
326    fn from(x: TypeDbVar) -> Self {
327        TyKind::TypeVar(x).into_ty()
328    }
329}
330
331impl DeBruijnId {
332    pub fn zero() -> Self {
333        DeBruijnId { index: 0 }
334    }
335
336    pub fn one() -> Self {
337        DeBruijnId { index: 1 }
338    }
339
340    pub fn new(index: usize) -> Self {
341        DeBruijnId { index }
342    }
343
344    pub fn is_zero(&self) -> bool {
345        self.index == 0
346    }
347
348    pub fn incr(&self) -> Self {
349        DeBruijnId {
350            index: self.index + 1,
351        }
352    }
353
354    pub fn decr(&self) -> Self {
355        DeBruijnId {
356            index: self.index - 1,
357        }
358    }
359
360    pub fn plus(&self, delta: Self) -> Self {
361        DeBruijnId {
362            index: self.index + delta.index,
363        }
364    }
365
366    pub fn sub(&self, delta: Self) -> Option<Self> {
367        Some(DeBruijnId {
368            index: self.index.checked_sub(delta.index)?,
369        })
370    }
371}
372
373impl<Id> DeBruijnVar<Id>
374where
375    Id: Copy,
376{
377    pub fn new_at_zero(id: Id) -> Self {
378        DeBruijnVar::Bound(DeBruijnId::new(0), id)
379    }
380
381    pub fn free(id: Id) -> Self {
382        DeBruijnVar::Free(id)
383    }
384
385    pub fn bound(index: DeBruijnId, id: Id) -> Self {
386        DeBruijnVar::Bound(index, id)
387    }
388
389    pub fn incr(&self) -> Self {
390        match *self {
391            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.incr(), varid),
392            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
393        }
394    }
395
396    pub fn decr(&self) -> Self {
397        match *self {
398            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid),
399            DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
400        }
401    }
402
403    /// Returns the variable id if it is bound as the given depth.
404    pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option<Id> {
405        match *self {
406            DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid),
407            _ => None,
408        }
409    }
410    /// Returns the variable id if it is bound as the given depth.
411    pub fn bound_at_depth_mut(&mut self, depth: DeBruijnId) -> Option<&mut Id> {
412        match self {
413            DeBruijnVar::Bound(dbid, varid) if *dbid == depth => Some(varid),
414            _ => None,
415        }
416    }
417
418    /// Move the variable out of `depth` binders. Returns `None` if the variable is bound in one of
419    /// these `depth` binders.
420    pub fn move_out_from_depth(&self, depth: DeBruijnId) -> Option<Self> {
421        Some(match *self {
422            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.sub(depth)?, varid),
423            DeBruijnVar::Free(_) => *self,
424        })
425    }
426
427    /// Move under `depth` binders.
428    pub fn move_under_binders(&self, depth: DeBruijnId) -> Self {
429        match *self {
430            DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.plus(depth), varid),
431            DeBruijnVar::Free(_) => *self,
432        }
433    }
434}
435
436impl Default for DeBruijnId {
437    fn default() -> Self {
438        Self::zero()
439    }
440}
441
442/// A stack of values corresponding to nested binders. Each binder introduces an entry in this
443/// stack, with the entry as index `0` being the innermost binder. This is indexed by
444/// `DeBruijnId`s.
445/// Most methods assume that the stack is non-empty and panic if not.
446#[derive(Clone, Hash)]
447pub struct BindingStack<T> {
448    /// The stack, stored in reverse. We push/pop to the end of the `Vec`, and the last pushed
449    /// value (i.e. the end of the vec) is considered index 0.
450    stack: Vec<T>,
451}
452
453impl<T> BindingStack<T> {
454    pub fn new(x: T) -> Self {
455        Self { stack: vec![x] }
456    }
457    /// Creates an empty stack. Beware, a number of method calls will panic on an empty stack.
458    pub fn empty() -> Self {
459        Self { stack: vec![] }
460    }
461
462    pub fn push(&mut self, x: T) {
463        self.stack.push(x);
464    }
465    pub fn pop(&mut self) -> Option<T> {
466        self.stack.pop()
467    }
468    /// Iterate over the binding levels, from the innermost (0) out.
469    pub fn into_iter(self) -> impl DoubleEndedIterator<Item = T> + ExactSizeIterator {
470        self.stack.into_iter().rev()
471    }
472}
473
474/// A borrowed portion of a [`BindingStack`].
475#[repr(transparent)]
476pub struct BinderSlice<T>([T]);
477
478impl<T> BinderSlice<T> {
479    fn from_slice(stack: &[T]) -> &Self {
480        // SAFETY: BinderStackSlice is a transparent wrapper around [T].
481        unsafe { &*(stack as *const [T] as *const Self) }
482    }
483
484    fn from_slice_mut(stack: &mut [T]) -> &mut Self {
485        // SAFETY: BinderStackSlice is a transparent wrapper around [T].
486        unsafe { &mut *(stack as *mut [T] as *mut Self) }
487    }
488
489    pub fn is_empty(&self) -> bool {
490        self.0.is_empty()
491    }
492    pub fn len(&self) -> usize {
493        self.0.len()
494    }
495    pub fn depth(&self) -> DeBruijnId {
496        DeBruijnId::new(self.0.len() - 1)
497    }
498
499    /// Map a bound variable to its binding depth. Considers free variables to be bound at the
500    /// outermost binder, like when `--unbind-item-vars` is set.
501    pub fn as_bound_var<Id>(&self, var: DeBruijnVar<Id>) -> (DeBruijnId, Id) {
502        match var {
503            DeBruijnVar::Bound(dbid, varid) => (dbid, varid),
504            DeBruijnVar::Free(varid) => (self.depth(), varid),
505        }
506    }
507    /// Helper that computes the real index into the underlying slice.
508    fn real_index(&self, id: DeBruijnId) -> Option<usize> {
509        self.0.len().checked_sub(id.index + 1)
510    }
511    pub fn get(&self, id: DeBruijnId) -> Option<&T> {
512        self.0.get(self.real_index(id)?)
513    }
514    pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar<Id>) -> Option<&'a Inner::Output>
515    where
516        T: Borrow<Inner>,
517        Inner: HasIdxVecOf<Id> + 'a,
518    {
519        let (dbid, varid) = self.as_bound_var(var);
520        self.get(dbid)
521            .and_then(|x| x.borrow().get_idx_vec().get(varid))
522    }
523    pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> {
524        let index = self.real_index(id)?;
525        self.0.get_mut(index)
526    }
527
528    /// Iterate over the binding levels, from the innermost (0) out.
529    pub fn iter(&self) -> impl DoubleEndedIterator<Item = &T> + ExactSizeIterator {
530        self.0.iter().rev()
531    }
532    /// Iterate mutably over the binding levels, from the innermost (0) out.
533    pub fn iter_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut T> + ExactSizeIterator {
534        self.0.iter_mut().rev()
535    }
536    /// Iterate over the binding levels, from the innermost (0) out.
537    pub fn indices(
538        &self,
539    ) -> impl DoubleEndedIterator<Item = DeBruijnId> + ExactSizeIterator + use<T> {
540        (0..self.0.len()).map(DeBruijnId::new)
541    }
542    /// Iterate over the binding levels, from the innermost (0) out.
543    pub fn iter_enumerated(
544        &self,
545    ) -> impl DoubleEndedIterator<Item = (DeBruijnId, &T)> + ExactSizeIterator {
546        self.iter()
547            .enumerate()
548            .map(|(i, x)| (DeBruijnId::new(i), x))
549    }
550    /// Iterate over the binding levels, from the innermost (0) out.
551    pub fn iter_mut_enumerated(
552        &mut self,
553    ) -> impl DoubleEndedIterator<Item = (DeBruijnId, &mut T)> + ExactSizeIterator {
554        self.iter_mut()
555            .enumerate()
556            .map(|(i, x)| (DeBruijnId::new(i), x))
557    }
558
559    pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack<U> {
560        BindingStack {
561            stack: self.0.iter().map(f).collect(),
562        }
563    }
564
565    /// Find the outermost binder where the given `U` can be moved to.
566    pub fn place_at_outermost<U>(&mut self, val: &U) -> (U, &mut T)
567    where
568        U: TyVisitable + Clone,
569    {
570        for (depth, binder) in self.iter_mut_enumerated().rev() {
571            if let Some(val) = val.clone().move_from_under_binders(depth) {
572                return (val, binder);
573            }
574        }
575        // Binder level `0` always works.
576        unreachable!()
577    }
578
579    pub fn innermost(&self) -> &T {
580        self.0.last().unwrap()
581    }
582    pub fn innermost_mut(&mut self) -> &mut T {
583        self.0.last_mut().unwrap()
584    }
585    pub fn outermost(&self) -> &T {
586        self.0.first().unwrap()
587    }
588    pub fn outermost_mut(&mut self) -> &mut T {
589        self.0.first_mut().unwrap()
590    }
591}
592
593impl<T> Deref for BindingStack<T> {
594    type Target = BinderSlice<T>;
595    fn deref(&self) -> &Self::Target {
596        BinderSlice::from_slice(&self.stack)
597    }
598}
599impl<T> DerefMut for BindingStack<T> {
600    fn deref_mut(&mut self) -> &mut Self::Target {
601        BinderSlice::from_slice_mut(&mut self.stack)
602    }
603}
604
605impl<T> Default for BindingStack<T> {
606    fn default() -> Self {
607        Self {
608            stack: Default::default(),
609        }
610    }
611}
612
613impl<T: std::fmt::Debug> std::fmt::Debug for BindingStack<T> {
614    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
615        write!(f, "{:?}", self.stack)
616    }
617}
618
619impl<T> Index<DeBruijnId> for BinderSlice<T> {
620    type Output = T;
621    fn index(&self, id: DeBruijnId) -> &Self::Output {
622        self.get(id).unwrap()
623    }
624}
625impl<T> IndexMut<DeBruijnId> for BinderSlice<T> {
626    fn index_mut(&mut self, id: DeBruijnId) -> &mut Self::Output {
627        self.get_mut(id).unwrap()
628    }
629}
630
631/// `self[depth..]` represents the binding stack seen from `depth`.
632impl<T> Index<RangeFrom<DeBruijnId>> for BinderSlice<T> {
633    type Output = BinderSlice<T>;
634    fn index(&self, range: RangeFrom<DeBruijnId>) -> &Self::Output {
635        let end = self.0.len() - range.start.index;
636        BinderSlice::from_slice(&self.0[..end])
637    }
638}
639impl<T> IndexMut<RangeFrom<DeBruijnId>> for BinderSlice<T> {
640    fn index_mut(&mut self, range: RangeFrom<DeBruijnId>) -> &mut Self::Output {
641        let end = self.0.len() - range.start.index;
642        BinderSlice::from_slice_mut(&mut self.0[..end])
643    }
644}
charon_lib/ast/type_level/vars.rs

charon_lib/ast/type_level/
vars.rs
