fix(sol-thir): add debruijin files

sol-thir/Cargo.toml

@@ -12,3 +12,4 @@ sol-syntax.workspace = true
 sol-vfs.workspace = true
 salsa-2022.workspace = true
 im.workspace = true
+thiserror.workspace = true

sol-thir/src/debruijin.rs

@@ -0,0 +1,79 @@
+//! Debruijin indexes and levels. It's used for type checker's efficient indexing
+//! and substitution.
+
+use super::*;
+
+/// Defines a debruijin level. It does represent the level of the context/environment
+///
+/// It can be transformed into a debruijin index by using the [`Level::as_idx`] method.
+#[derive(Default, Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct Level(pub usize);
+
+#[derive(thiserror::Error, Debug, Clone)]
+pub enum Level2IdxError {
+    /// The level is greater than the index.
+    #[error("expected l > x")]
+    LevelGreaterThanIndex,
+    /// The level is equal to zero.
+    #[error("expected l > 0")]
+    LevelEqualToZero,
+}
+
+impl Level {
+    /// Transforms a level into a debruijin index.
+    pub fn as_idx(&self, Level(l): Level) -> Result<Index, Level2IdxError> {
+        let Level(x) = *self;
+        if l > x {
+            return Err(Level2IdxError::LevelGreaterThanIndex);
+        }
+        if l == 0 {
+            return Err(Level2IdxError::LevelEqualToZero);
+        }
+        Ok(Index(0))
+    }
+}
+
+impl std::ops::Add<usize> for Level {
+    type Output = Self;
+
+    fn add(self, rhs: usize) -> Self::Output {
+        Self(self.0 + rhs)
+    }
+}
+
+impl std::ops::AddAssign<usize> for Level {
+    fn add_assign(&mut self, rhs: usize) {
+        self.0 += rhs
+    }
+}
+
+/// Defines a debruijin index. That can be converted by two levels.
+///
+/// It's used to represent a variable in the syntax tree.
+#[derive(Default, Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct Index(usize);
+
+impl From<usize> for Index {
+    fn from(value: usize) -> Self {
+        Self(value)
+    }
+}
+
+impl std::ops::Add<usize> for Index {
+    type Output = Self;
+
+    fn add(self, rhs: usize) -> Self::Output {
+        Self(self.0 + rhs)
+    }
+}
+
+impl std::ops::AddAssign<usize> for Index {
+    fn add_assign(&mut self, rhs: usize) {
+        self.0 += rhs
+    }
+}
+
+/// Debruijin indices construction, that can be used to get the names of the
+/// variables.
+#[salsa::accumulator]
+pub struct Indices((String, source::Term));

sol-thir/src/lib.rs

@@ -30,6 +30,7 @@ use crate::{
 
 extern crate salsa_2022 as salsa;
 
+pub mod debruijin;
 pub mod shared;
 pub mod source;
 pub mod value;
@@ -50,7 +51,7 @@ pub trait ThirDb:
 {
 }
 
-impl ThirDb for DB where
+impl<DB> ThirDb for DB where
     DB: ?Sized
         + ParseDb
         + DiagnosticDb

sol-thir/src/source.rs

@@ -4,7 +4,7 @@ pub type Expr = Box<Term>;
 
 #[derive(Debug, Clone, Hash, PartialEq, Eq)]
 pub enum Term {
-    Var(Index, Option<Reference>),
+    Var(debruijin::Index, Option<Reference>),
     Lam(Definition, shared::Implicitness, Expr),
     App(Expr, Expr),
     Pi(Option<Definition>, shared::Implicitness, Expr, Expr),

sol-thir/src/value.rs

@@ -33,10 +33,10 @@ pub struct Pi {
 #[derive(Debug, Clone, Hash, PartialEq, Eq)]
 pub enum ValueKind {
     U,
-    Var(Index, Option<Reference>),
+    Var(debruijin::Index, Option<Reference>),
     Constructor(shared::Constructor),
     Flexible(Meta, Vec<Value>),
-    Rigid(Level, Vec<Value>),
+    Rigid(debruijin::Level, Vec<Value>),
     Pi(Pi),
     Lam(Definition, shared::Implicitness, Closure),
     Location(Location, Box<ValueKind>),
@@ -46,8 +46,4 @@ impl ValueKind {
     pub fn located(location: Location, value: ValueKind) -> ValueKind {
         ValueKind::Location(location, Box::new(value))
     }
-
-    pub fn no() -> ValueKind {
-        ValueKind::Sorry(Location::CallSite, None)
-    }
 }