catlog/tt/util/
idx.rs

1//! Indices.
2//!
3//! We find it useful to distinguish between backward indices (used in syntax, where
4//! 0 refers to the *end* of the context) and forward indices (used in values, where
5//! 0 refers to the *beginning* of the context).
6//!
7//! In the literature, backward indices are known as DeBruijn indices and forward
8//! indices are known as DeBruijn levels, but we think that "backwards and forwards"
9//! is more clear, and it corresponds with "backwards and forwards linked lists". A forwards linked list uses `cons` to put a new element on the front; a backwards
10//! linked list uses `snoc` to put a new element on the back.
11//!
12//! We take this terminology from [narya](https://github.com/gwaithimirdain/narya).
13
14use derive_more::From;
15use std::ops::Deref;
16
17/// Forward indices (aka DeBruijn levels)
18///
19/// Get the underlying `usize` using the [Deref] implementation.
20#[derive(Copy, Clone, PartialEq, Eq, Debug, From)]
21pub struct FwdIdx(usize);
22
23impl Deref for FwdIdx {
24    type Target = usize;
25
26    fn deref(&self) -> &Self::Target {
27        &self.0
28    }
29}
30
31impl FwdIdx {
32    /// The forward index refering the the next variable in the scope
33    pub fn next(&self) -> Self {
34        Self(self.0 + 1)
35    }
36
37    /// Convert into a backward index, assuming that the scope is of
38    /// length `scope_length`
39    pub fn as_bwd(&self, scope_length: usize) -> BwdIdx {
40        BwdIdx(scope_length - self.0 - 1)
41    }
42}
43
44/// Backward indices (aka DeBruijn indices).
45///
46/// Get the underlying `usize` using the [Deref] implementation.
47#[derive(Copy, Clone, PartialEq, Eq, Debug, From)]
48pub struct BwdIdx(usize);
49
50impl Deref for BwdIdx {
51    type Target = usize;
52
53    fn deref(&self) -> &Self::Target {
54        &self.0
55    }
56}
57
58impl BwdIdx {
59    /// The backwards index refering to the previous variable in the scope
60    pub fn prev(&self) -> Self {
61        Self(self.0 + 1)
62    }
63}
catlog/tt/util/idx.rs

catlog/tt/util/
idx.rs
