catlog/zero/
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::{Deref, From};
15
16/// Forward indices (aka DeBruijn levels).
17#[derive(Copy, Clone, PartialEq, Eq, Debug, Deref, From)]
18pub struct FwdIdx(usize);
19
20impl FwdIdx {
21    /// The forward index refering the the next variable in the scope.
22    pub fn next(&self) -> Self {
23        Self(self.0 + 1)
24    }
25
26    /// Convert into a backward index, assuming that the scope is of
27    /// length `scope_length`.
28    pub fn as_bwd(&self, scope_length: usize) -> BwdIdx {
29        BwdIdx(scope_length - self.0 - 1)
30    }
31}
32
33/// Backward indices (aka DeBruijn indices).
34#[derive(Copy, Clone, PartialEq, Eq, Debug, Deref, From)]
35pub struct BwdIdx(usize);
36
37impl BwdIdx {
38    /// The backwards index refering to the previous variable in the scope.
39    pub fn prev(&self) -> Self {
40        Self(self.0 + 1)
41    }
42}
catlog/zero/idx.rs

catlog/zero/
idx.rs
