Cargo.lock

@@ -13,12 +13,6 @@ dependencies = [
  "winapi",
 ]
 
-[[package]]
-name = "autocfg"
-version = "1.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
-
 [[package]]
 name = "bitflags"
 version = "1.3.2"
@@ -326,7 +320,6 @@ dependencies = [
  "derive_more",
  "im-rc",
  "lazy_static",
- "num-bigint",
 ]
 
 [[package]]
@@ -382,36 +375,6 @@ dependencies = [
  "libc",
 ]
 
-[[package]]
-name = "num-bigint"
-version = "0.4.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f93ab6289c7b344a8a9f60f88d80aa20032336fe78da341afc91c8a2341fc75f"
-dependencies = [
- "autocfg",
- "num-integer",
- "num-traits",
-]
-
-[[package]]
-name = "num-integer"
-version = "0.1.45"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "225d3389fb3509a24c93f5c29eb6bde2586b98d9f016636dff58d7c6f7569cd9"
-dependencies = [
- "autocfg",
- "num-traits",
-]
-
-[[package]]
-name = "num-traits"
-version = "0.2.15"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd"
-dependencies = [
- "autocfg",
-]
-
 [[package]]
 name = "once_cell"
 version = "1.16.0"
@@ -430,7 +393,6 @@ version = "0.1.0"
 dependencies = [
  "derive_more",
  "kernel",
- "num-bigint",
  "pest",
  "pest_derive",
 ]

Cargo.toml

@@ -12,7 +12,6 @@ clap = { version = "4.0.10", features = ["derive"] }
 colored = "2"
 derive_more = "0.99.17"
 im-rc = "15.1.0"
-num-bigint = "0.4"
 path-absolutize = "3.0.14"
 pest = "2.5"
 pest_derive = "2.5"

kernel/Cargo.toml

@@ -9,7 +9,6 @@ license.workspace = true
 bumpalo.workspace = true
 derive_more.workspace = true
 im-rc.workspace = true
-num-bigint.workspace = true
 
 [dev-dependencies]
 lazy_static = "1.4.0"

kernel/src/calculus/level.rs

+//! A set of useful functions to operate on [`Level`]s.
+
+use Payload::*;
+
+use crate::memory::arena::Arena;
+use crate::memory::level::{Level, Payload};
+
+/// State during computation for level comparison.
+enum State {
+    /// Comparison failed.
+    False,
+
+    /// Comparison succeed.
+    True,
+
+    /// Induction is needed to complete the comparaison.
+    Stuck(usize),
+}
+
+impl State {
+    /// Checks if the comparison succeeded.
+    fn is_true(&self) -> bool {
+        matches!(self, State::True)
+    }
+}
+
+impl<'arena> Level<'arena> {
+    /// Helper function for equality checking, used to substitute `Var(i)` with `Z` and `S(Var(i))`.
+    fn substitute_single(self, var: usize, u: Self, arena: &mut Arena<'arena>) -> Self {
+        match *self {
+            Succ(n) => n.substitute_single(var, u, arena).succ(arena),
+            Max(n, m) => Level::max(n.substitute_single(var, u, arena), m.substitute_single(var, u, arena), arena),
+            IMax(n, m) => Level::imax(n.substitute_single(var, u, arena), m.substitute_single(var, u, arena), arena),
+            Var(n) if n == var => u,
+            _ => self,
+        }
+    }
+
+    /// Substitutes all level variables in `self` according to `univs`.
+    ///
+    /// This function makes no verification that `univs` has an appropriate size, which is way it
+    /// cannot be made public.
+    pub(crate) fn substitute(self, univs: &[Self], arena: &mut Arena<'arena>) -> Self {
+        match *self {
+            Zero => self,
+            Succ(n) => n.substitute(univs, arena).succ(arena),
+            Max(n, m) => Level::max(n.substitute(univs, arena), m.substitute(univs, arena), arena),
+            IMax(n, m) => Level::imax(n.substitute(univs, arena), m.substitute(univs, arena), arena),
+            Var(var) => *univs.get(var).unwrap_or_else(|| unreachable!()),
+        }
+    }
+
+    /// Checks whether `self <= rhs + n`, without applying substitution.
+    ///
+    /// Precisely, it returns:
+    /// - `Stuck(i + 1)` if `Var(i)` needs to be substituted to unstuck the comparison.
+    /// - `True` if `self <= rhs + n`,
+    /// - `False` else.
+    fn geq_no_subst(self, rhs: Self, n: i64) -> State {
+        match (&*self, &*rhs) {
+            (Zero, _) if n >= 0 => State::True,
+
+            (_, _) if self == rhs && n >= 0 => State::True,
+
+            (Succ(l), _) if l.geq_no_subst(rhs, n - 1).is_true() => State::True,
+            (_, Succ(l)) if self.geq_no_subst(*l, n + 1).is_true() => State::True,
+
+            (_, Max(l1, l2))
+                if self.geq_no_subst(*l1, n).is_true() || self.geq_no_subst(*l2, n).is_true() =>
+            {
+                State::True
+            }
+            (Max(l1, l2), _) if l1.geq_no_subst(rhs, n).is_true() && l2.geq_no_subst(rhs, n).is_true() => {
+                State::True
+            }
+
+            (_, IMax(_, v)) | (IMax(_, v), _) if let Var(i) = **v => State::Stuck(i),
+
+            _ => State::False,
+        }
+    }
+
+    /// Checks whether `self <= rhs + n`.
+    ///
+    /// In a case where comparison is stuck because of a variable `Var(i)`, it checks whether the test is correct when `Var(i)`
+    /// is substituted for `0` and `S(Var(i))`.
+    pub fn geq(self, rhs: Self, n: i64, arena: &mut Arena<'arena>) -> bool {
+        match self.geq_no_subst(rhs, n) {
+            State::True => true,
+            State::False => false,
+            State::Stuck(i) => {
+                let zero = Level::zero(arena);
+                let vv = Level::var(i, arena).succ(arena);
+                self.substitute_single(i, zero, arena).geq(rhs.substitute_single(i, zero, arena), n, arena)
+                    && self.substitute_single(i, vv, arena).geq(rhs.substitute_single(i, vv, arena), n, arena)
+            },
+        }
+    }
+
+    /// Checks whether `self = rhs`.
+    ///
+    /// This is a "conversion" equality test, not the equality function used by [`PartialEq`].
+    pub fn is_eq(self, rhs: Self, arena: &mut Arena<'arena>) -> bool {
+        self.geq(rhs, 0, arena) && rhs.geq(self, 0, arena)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::memory::arena::use_arena;
+    use crate::memory::level::builder::raw::*;
+    use crate::memory::level::Level;
+
+    #[test]
+    fn univ_eq() {
+        use_arena(|arena| {
+            let two = arena.build_level_raw(succ(succ(zero())));
+            let one = arena.build_level_raw(succ(zero()));
+            let zero_ = arena.build_level_raw(zero());
+            let var0 = Level::var(0, arena);
+            let var1 = Level::var(1, arena);
+            let succ_var0 = Level::succ(var0, arena);
+            let max1_var0 = Level::max(one, var0, arena);
+            let max0_var0 = Level::max(zero_, var0, arena);
+            let imax_0_var0 = Level::imax(zero_, var0, arena);
+            let max_var0_var1 = Level::max(var0, var1, arena);
+            let max_var1_var0 = Level::max(var1, var0, arena);
+            let max_var1_var1 = Level::max(var1, var1, arena);
+            let succ_max_var0_var1 = Level::succ(max_var0_var1, arena);
+            let max_succ_var0_succ_var1 = arena.build_level_raw(max(succ(var(0)), succ(var(1))));
+
+            assert!(!two.geq_no_subst(succ_var0, 0).is_true());
+            assert!(imax_0_var0.is_eq(var0, arena));
+            assert!(max1_var0.geq(succ_var0, 0, arena));
+            assert!(!zero_.is_eq(one, arena));
+            assert!(!one.is_eq(zero_, arena));
+            assert!(var0.is_eq(max0_var0, arena));
+            assert!(max0_var0.is_eq(var0, arena));
+            assert!(max_var0_var1.is_eq(max_var1_var0, arena));
+            assert!(!max_var1_var1.is_eq(max_var1_var0, arena));
+            assert!(succ_max_var0_var1.is_eq(max_succ_var0_succ_var1, arena));
+            assert!(var0.is_eq(Level::imax(var0, var0, arena), arena));
+            assert!(arena.build_level_raw(imax(succ(zero()), max(zero(), zero()))).is_eq(zero_, arena));
+            assert!(!Level::imax(var0, var1, arena).is_eq(Level::imax(var1, var0, arena), arena));
+
+            assert!(
+                (arena.build_level_raw(max(zero(), imax(zero(), max(succ(zero()), zero())))))
+                    .is_eq(arena.build_level_raw(imax(succ(zero()), imax(succ(zero()), succ(zero())))), arena)
+            )
+        });
+    }
+
+    #[test]
+    fn subst() {
+        use_arena(|arena| {
+            let lvl = Level::imax(
+                Level::succ(Level::zero(arena), arena),
+                arena.build_level_raw(max(succ(zero()), max(var(0), var(1)))),
+                arena,
+            );
+            let subst = vec![arena.build_level_raw(succ(zero())), arena.build_level_raw(zero())];
+            assert_eq!(
+                lvl.substitute(&subst, arena),
+                arena.build_level_raw(imax(zero(), max(succ(zero()), max(succ(zero()), zero()))))
+            )
+        })
+    }
+    #[test]
+    fn single_subst() {
+        use_arena(|arena| {
+            let lvl = arena.build_level_raw(imax(max(succ(zero()), var(0)), var(0)));
+            assert_eq!(
+                lvl.substitute_single(0, Level::zero(arena), arena),
+                arena.build_level_raw(imax(max(succ(zero()), zero()), zero()))
+            )
+        })
+    }
+}

kernel/src/calculus/mod.rs

+//! A collection of computational functions over different types of
+//! [dwellers](crate::memory::arena::Arena)
+
+pub mod level;
+pub mod term;

kernel/src/term/calculus.rs → kernel/src/calculus/term.rs

@@ -5,110 +5,160 @@
 
 use Payload::*;
 
-use super::arena::{Arena, Payload, Term};
+use crate::memory::arena::Arena;
+use crate::memory::declaration::InstantiatedDeclaration;
+use crate::memory::level::Level;
+use crate::memory::term::{Payload, Term};
 
-impl<'arena> Arena<'arena> {
+impl<'arena> Term<'arena> {
     /// Apply one step of β-reduction, using the leftmost-outermost evaluation strategy.
-    pub fn beta_reduction(&mut self, t: Term<'arena>) -> Term<'arena> {
-        match *t {
+    pub fn beta_reduction(self, arena: &mut Arena<'arena>) -> Self {
+        match *self {
             App(t1, t2) => match *t1 {
-                Abs(_, t1) => self.substitute(t1, t2, 1),
+                Abs(_, t1) => t1.substitute(t2, 1, arena),
                 _ => {
-                    let t1_new = self.beta_reduction(t1);
+                    let t1_new = t1.beta_reduction(arena);
                     if t1_new == t1 {
-                        let t2_new = self.beta_reduction(t2);
-                        self.app(t1, t2_new)
+                        let t2_new = t2.beta_reduction(arena);
+                        t1.app(t2_new, arena)
                     } else {
-                        self.app(t1_new, t2)
+                        t1_new.app(t2, arena)
                     }
                 },
             },
             Abs(arg_type, body) => {
-                let body = self.beta_reduction(body);
-                self.abs(arg_type, body)
+                let body = body.beta_reduction(arena);
+                arg_type.abs(body, arena)
             },
             Prod(arg_type, body) => {
-                let body = self.beta_reduction(body);
-                self.prod(arg_type, body)
+                let body = body.beta_reduction(arena);
+                arg_type.prod(body, arena)
             },
-            _ => t,
+            Decl(decl) => decl.get_term(arena),
+            _ => self,
         }
     }
 
-    /// Returns the term `t` where all variables with de Bruijn index larger than `depth` are offset
+    /// Returns the term `self` where all variables with de Bruijn index larger than `depth` are offset
     /// by `offset`.
-    pub(crate) fn shift(&mut self, t: Term<'arena>, offset: usize, depth: usize) -> Term<'arena> {
-        match *t {
-            Var(i, type_) if i > depth.into() => self.var(i + offset.into(), type_),
+    pub(crate) fn shift(self, offset: usize, depth: usize, arena: &mut Arena<'arena>) -> Self {
+        match *self {
+            Var(i, type_) if i > depth.into() => Term::var(i + offset.into(), type_, arena),
             App(t1, t2) => {
-                let t1 = self.shift(t1, offset, depth);
-                let t2 = self.shift(t2, offset, depth);
-                self.app(t1, t2)
+                let t1 = t1.shift(offset, depth, arena);
+                let t2 = t2.shift(offset, depth, arena);
+                t1.app(t2, arena)
             },
             Abs(arg_type, body) => {
-                let arg_type = self.shift(arg_type, offset, depth);
-                let body = self.shift(body, offset, depth + 1);
-                self.abs(arg_type, body)
+                let arg_type = arg_type.shift(offset, depth, arena);
+                let body = body.shift(offset, depth + 1, arena);
+                arg_type.abs(body, arena)
             },
             Prod(arg_type, body) => {
-                let arg_type = self.shift(arg_type, offset, depth);
-                let body = self.shift(body, offset, depth + 1);
-                self.prod(arg_type, body)
+                let arg_type = arg_type.shift(offset, depth, arena);
+                let body = body.shift(offset, depth + 1, arena);
+                arg_type.prod(body, arena)
             },
-            _ => t,
+            _ => self,
         }
     }
 
-    /// Returns the term `t` where all instances of the variable tracked by `depth` are substituted
+    /// Returns the term `self` where all instances of the variable tracked by `depth` are substituted
     /// with `sub`.
-    pub(crate) fn substitute(&mut self, t: Term<'arena>, sub: Term<'arena>, depth: usize) -> Term<'arena> {
-        self.get_subst_or_init(&(t, sub, depth), |arena| match *t {
-            Var(i, _) if i == depth.into() => arena.shift(sub, depth - 1, 0),
-            Var(i, type_) if i > depth.into() => arena.var(i - 1.into(), type_),
+    pub(crate) fn substitute(self, sub: Self, depth: usize, arena: &mut Arena<'arena>) -> Self {
+        arena.get_subst_or_init(&(self, sub, depth), |arena| match *self {
+            Var(i, _) if i == depth.into() => sub.shift(depth - 1, 0, arena),
+            Var(i, type_) if i > depth.into() => Term::var(i - 1.into(), type_, arena),
             App(l, r) => {
-                let l = arena.substitute(l, sub, depth);
-                let r = arena.substitute(r, sub, depth);
-                arena.app(l, r)
+                let l = l.substitute(sub, depth, arena);
+                let r = r.substitute(sub, depth, arena);
+                l.app(r, arena)
             },
             Abs(arg_type, body) => {
-                let arg_type = arena.substitute(arg_type, sub, depth);
-                let body = arena.substitute(body, sub, depth + 1);
-                arena.abs(arg_type, body)
+                let arg_type = arg_type.substitute(sub, depth, arena);
+                let body = body.substitute(sub, depth + 1, arena);
+                arg_type.abs(body, arena)
             },
             Prod(arg_type, body) => {
-                let arg_type = arena.substitute(arg_type, sub, depth);
-                let body = arena.substitute(body, sub, depth + 1);
-                arena.prod(arg_type, body)
+                let arg_type = arg_type.substitute(sub, depth, arena);
+                let body = body.substitute(sub, depth + 1, arena);
+                arg_type.prod(body, arena)
             },
-            _ => t,
+            _ => self,
         })
     }
 
+    /// Substitutes all level variables in `self` according to the correspondence given by
+    /// `univs`.
+    ///
+    /// This function would be safe to use from outside the kernel, but would serve no purpose as
+    /// level variables there can only appear behind a Declaration, which prevents the access to
+    /// the underlying Term.
+    pub(crate) fn substitute_univs(self, univs: &[Level<'arena>], arena: &mut Arena<'arena>) -> Self {
+        match *self {
+            Var(i, ty) => {
+                let ty = ty.substitute_univs(univs, arena);
+                Term::var(i, ty, arena)
+            },
+
+            Sort(level) => {
+                let subst = level.substitute(univs, arena);
+                Term::sort(subst, arena)
+            },
+            App(u1, u2) => {
+                let u1 = u1.substitute_univs(univs, arena);
+                let u2 = u2.substitute_univs(univs, arena);
+                u1.app(u2, arena)
+            },
+            Abs(u1, u2) => {
+                let u1 = u1.substitute_univs(univs, arena);
+                let u2 = u2.substitute_univs(univs, arena);
+                u1.abs(u2, arena)
+            },
+
+            Prod(u1, u2) => {
+                let u1 = u1.substitute_univs(univs, arena);
+                let u2 = u2.substitute_univs(univs, arena);
+                u1.prod(u2, arena)
+            },
+
+            Decl(decl) => {
+                // TODO (#14) this can be slightly optimised in space. Certainly the substitution mapping can be
+                // performed in place while allocating the slice in the arena with store_level_slice. This
+                // function thus has to be made with templates.
+                let params = &*decl.params.iter().map(|level| level.substitute(univs, arena)).collect::<Vec<Level>>();
+                let params = arena.store_level_slice(params);
+                let inst = InstantiatedDeclaration::instantiate(decl.decl, params, arena);
+                Term::decl(inst, arena)
+            },
+        }
+    }
+
     /// Returns the normal form of a term.
     ///
     /// This function is computationally expensive and should only be used for reduce/eval commands, not when type-checking.
-    pub fn normal_form(&mut self, t: Term<'arena>) -> Term<'arena> {
-        let mut temp = t;
-        let mut res = self.beta_reduction(t);
+    pub fn normal_form(self, arena: &mut Arena<'arena>) -> Self {
+        let mut temp = self;
+        let mut res = self.beta_reduction(arena);
 
         while res != temp {
             temp = res;
-            res = self.beta_reduction(res);
+            res = res.beta_reduction(arena);
         }
         res
     }
 
     /// Returns the weak-head normal form of a term.
-    pub fn whnf(&mut self, t: Term<'arena>) -> Term<'arena> {
-        t.get_whnf_or_init(|| match *t {
-            App(t1, t2) => match *self.whnf(t1) {
+    pub fn whnf(self, arena: &mut Arena<'arena>) -> Self {
+        self.get_whnf_or_init(|| match *self {
+            App(t1, t2) => match *t1.whnf(arena) {
                 Abs(_, t1) => {
-                    let subst = self.substitute(t1, t2, 1);
-                    self.whnf(subst)
+                    let subst = t1.substitute(t2, 1, arena);
+                    subst.whnf(arena)
                 },
-                _ => t,
+                _ => self,
             },
-            _ => t,
+            _ => self,
         })
     }
 }
@@ -116,19 +166,22 @@ impl<'arena> Arena<'arena> {
 #[cfg(test)]
 mod tests {
     // /!\ most terms used in these tests are ill-typed; they should not be used elsewhere
-    use super::super::arena::use_arena;
-    use super::super::builders::raw::*;
+    use crate::memory::arena::use_arena;
+    use crate::memory::declaration;
+    use crate::memory::term::builder::raw::*;
 
     #[test]
     fn simple_subst() {
         use_arena(|arena| {
             // λx.(λy.x y) x
-            let term = arena
-                .build_raw(abs(prop(), app(abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))), var(1.into(), prop()))));
+            let term = arena.build_term_raw(abs(
+                prop(),
+                app(abs(prop(), app(var(2.into(), prop()), var(1.into(), prop()))), var(1.into(), prop())),
+            ));
             // λx.x x
-            let reduced = arena.build_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
+            let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
 
-            assert_eq!(arena.beta_reduction(term), reduced);
+            assert_eq!(term.beta_reduction(arena), reduced);
         })
     }
 
@@ -136,7 +189,7 @@ mod tests {
     fn complex_subst() {
         use_arena(|arena| {
             // (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λa.λb.a b)
-            let term = arena.build_raw(app(
+            let term = arena.build_term_raw(app(
                 abs(
                     prop(),
                     abs(
@@ -165,7 +218,7 @@ mod tests {
                 abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
             ));
 
-            let term_step_1 = arena.build_raw(abs(
+            let term_step_1 = arena.build_term_raw(abs(
                 prop(),
                 abs(
                     prop(),
@@ -185,7 +238,7 @@ mod tests {
                 ),
             ));
 
-            let term_step_2 = arena.build_raw(abs(
+            let term_step_2 = arena.build_term_raw(abs(
                 prop(),
                 abs(
                     prop(),
@@ -208,7 +261,7 @@ mod tests {
                 ),
             ));
 
-            let term_step_3 = arena.build_raw(abs(
+            let term_step_3 = arena.build_term_raw(abs(
                 prop(),
                 abs(
                     prop(),
@@ -222,7 +275,7 @@ mod tests {
                 ),
             ));
 
-            let term_step_4 = arena.build_raw(abs(
+            let term_step_4 = arena.build_term_raw(abs(
                 prop(),
                 abs(
                     prop(),
@@ -233,7 +286,7 @@ mod tests {
                 ),
             ));
 
-            let term_step_5 = arena.build_raw(abs(
+            let term_step_5 = arena.build_term_raw(abs(
                 prop(),
                 abs(
                     prop(),
@@ -242,61 +295,118 @@ mod tests {
             ));
 
             let term_step_6 =
-                arena.build_raw(abs(prop(), abs(prop(), app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())))));
+                arena.build_term_raw(abs(prop(), abs(prop(), app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())))));
 
             // λa.λb.b
-            let term_step_7 = arena.build_raw(abs(prop(), abs(prop(), var(1.into(), prop()))));
-
-            assert_eq!(arena.beta_reduction(term), term_step_1);
-            assert_eq!(arena.beta_reduction(term_step_1), term_step_2);
-            assert_eq!(arena.beta_reduction(term_step_2), term_step_3);
-            assert_eq!(arena.beta_reduction(term_step_3), term_step_4);
-            assert_eq!(arena.beta_reduction(term_step_4), term_step_5);
-            assert_eq!(arena.beta_reduction(term_step_5), term_step_6);
-            assert_eq!(arena.beta_reduction(term_step_6), term_step_7);
-            assert_eq!(arena.beta_reduction(term_step_7), term_step_7);
+            let term_step_7 = arena.build_term_raw(abs(prop(), abs(prop(), var(1.into(), prop()))));
+
+            assert_eq!(term.beta_reduction(arena), term_step_1);
+            assert_eq!(term_step_1.beta_reduction(arena), term_step_2);
+            assert_eq!(term_step_2.beta_reduction(arena), term_step_3);
+            assert_eq!(term_step_3.beta_reduction(arena), term_step_4);
+            assert_eq!(term_step_4.beta_reduction(arena), term_step_5);
+            assert_eq!(term_step_5.beta_reduction(arena), term_step_6);
+            assert_eq!(term_step_6.beta_reduction(arena), term_step_7);
+            assert_eq!(term_step_7.beta_reduction(arena), term_step_7);
+        })
+    }
+
+    #[test]
+    fn decl_subst() {
+        use_arena(|arena| {
+            let decl_ = crate::memory::declaration::InstantiatedDeclaration::instantiate(
+                crate::memory::declaration::builder::Builder::Decl(crate::memory::term::builder::Builder::Prop.into(), Vec::new())
+                    .realise(arena)
+                    .unwrap(),
+                &Vec::new(),
+                arena,
+            );
+            let decl = crate::memory::term::Term::decl(decl_, arena);
+            let reduced = arena.build_term_raw(prop());
+
+            assert_eq!(decl.beta_reduction(arena), reduced);
         })
     }
 
     #[test]
     fn shift_prod() {
         use_arena(|arena| {
-            let reduced = arena.build_raw(prod(prop(), var(1.into(), prop())));
-            let term = arena.build_raw(app(abs(prop(), reduced.into()), prop()));
+            let reduced = prod(prop(), var(1.into(), prop()));
+            let term = arena.build_term_raw(app(abs(prop(), reduced), prop()));
 
-            assert_eq!(arena.beta_reduction(term), reduced)
+            let reduced = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
+            assert_eq!(term.beta_reduction(arena), reduced)
         })
     }
 
     #[test]
     fn prod_beta_red() {
         use_arena(|arena| {
-            let term = arena.build_raw(prod(prop(), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop()))));
-            let reduced = arena.build_raw(prod(prop(), var(1.into(), prop())));
+            let term = arena.build_term_raw(prod(prop(), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop()))));
+            let reduced = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
 
-            assert_eq!(arena.beta_reduction(term), reduced);
+            assert_eq!(term.beta_reduction(arena), reduced);
         })
     }
 
     #[test]
     fn app_red_rhs() {
         use_arena(|arena| {
-            let term = arena
-                .build_raw(abs(prop(), app(var(1.into(), prop()), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())))));
-            let reduced = arena.build_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
+            let term = arena.build_term_raw(abs(
+                prop(),
+                app(var(1.into(), prop()), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop()))),
+            ));
+            let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
 
-            assert_eq!(arena.beta_reduction(term), reduced);
+            assert_eq!(term.beta_reduction(arena), reduced);
         })
     }
 
     #[test]
     fn normal_form() {
         use_arena(|arena| {
-            let term = arena
-                .build_raw(app(app(app(abs(prop(), abs(prop(), abs(prop(), var(1.into(), prop())))), prop()), prop()), prop()));
-            let normal_form = arena.build_raw(prop());
+            let term = arena.build_term_raw(app(
+                app(app(abs(prop(), abs(prop(), abs(prop(), var(1.into(), prop())))), prop()), prop()),
+                prop(),
+            ));
+            let normal_form = arena.build_term_raw(prop());
+
+            assert_eq!(term.normal_form(arena), normal_form);
+        })
+    }
+
+    #[test]
+    fn subst_univs() {
+        use crate::memory::level::builder::raw::*;
+
+        use_arena(|arena| {
+            let decl_ = crate::memory::declaration::InstantiatedDeclaration::instantiate(
+                declaration::builder::Builder::Decl(crate::memory::term::builder::Builder::Prop.into(), ["u", "v"].to_vec())
+                    .realise(arena)
+                    .unwrap(),
+                &[arena.build_level_raw(zero()), arena.build_level_raw(zero())],
+                arena,
+            );
+
+            let prop_ = crate::memory::term::Term::decl(decl_, arena);
+
+            assert_eq!(prop_.substitute_univs(&[arena.build_level_raw(zero()), arena.build_level_raw(zero())], arena), prop_);
+
+            let vart = crate::memory::term::builder::raw::var;
+
+            let lvl = max(succ(zero()), succ(zero()));
+            let term = arena.build_term_raw(abs(
+                sort_(lvl),
+                abs(
+                    type_usize(0),
+                    abs(
+                        type_usize(1),
+                        prod(vart(1.into(), type_usize(1)), app(vart(1.into(), type_usize(1)), vart(2.into(), type_usize(0)))),
+                    ),
+                ),
+            ));
 
-            assert_eq!(arena.normal_form(term), normal_form);
+            assert_eq!(term.substitute_univs(&[arena.build_level_raw(zero()), arena.build_level_raw(zero())], arena), term);
         })
     }
 }

kernel/src/error.rs

@@ -2,8 +2,7 @@
 
 use derive_more::{Display, From};
 
-use crate::term::arena::Term;
-use crate::term::builders::DefinitionError;
+use crate::memory::*;
 use crate::type_checker::TypeCheckerError;
 
 /// Type representing kernel errors.
@@ -20,10 +19,15 @@ pub struct Error<'arena> {
 #[derive(Clone, Debug, Display, Eq, PartialEq, From)]
 pub enum ErrorKind<'arena> {
     TypeChecker(TypeCheckerError<'arena>),
-    Definition(DefinitionError<'arena>),
+    Term(term::builder::TermError<'arena>),
+    Level(level::builder::LevelError<'arena>),
+    Declaration(declaration::builder::DeclarationError<'arena>),
 }
 
 impl<'arena> std::error::Error for Error<'arena> {}
 
 pub type Result<'arena, T> = std::result::Result<T, Error<'arena>>;
-pub type ResultTerm<'arena> = Result<'arena, Term<'arena>>;
+pub type ResultTerm<'arena> = Result<'arena, term::Term<'arena>>;
+pub type ResultLevel<'arena> = Result<'arena, level::Level<'arena>>;
+pub type ResultDecl<'arena> = Result<'arena, declaration::Declaration<'arena>>;
+pub type ResultInstantiatedDecl<'arena> = Result<'arena, declaration::InstantiatedDeclaration<'arena>>;

kernel/src/lib.rs

@@ -2,15 +2,17 @@
 
 //! A kernel for the calculus of constructions.
 //!
-//! Terms can be built with functions from the [`term`] module. This module also provides essential
-//! manipulation functions from lambda-calculus, while the [`type_checker`] module provides typed
-//! interactions.
+//! Terms can be built with functions from the [`memory::term`] module. The [`calculus`] module
+//! provides essential manipulation functions from lambda-calculus, while the [`type_checker`]
+//! module provides typed interactions.
 
 #![feature(no_coverage)]
 #![feature(once_cell)]
 #![feature(trait_alias)]
+#![feature(if_let_guard)]
 
+pub mod calculus;
 pub mod error;
 pub mod location;
-pub mod term;
+pub mod memory;
 pub mod type_checker;

kernel/src/memory/arena.rs

+//! A comprehensive memory management unit for terms.
+//!
+//! This module defines the core functions used to manipulate an arena and its dwellers.
+
+use std::collections::{HashMap, HashSet};
+use std::marker::PhantomData;
+
+use bumpalo::Bump;
+
+use super::declaration::Declaration;
+use super::level::Level;
+use super::term::Term;
+
+/// A comprehensive memory management unit for terms.
+///
+/// An arena is a location in memory where a group of terms with several properties is stored. Most
+/// importantly, it ensures that all terms living in the arena are syntactically unique, which
+/// accelerates many algorithms. In particular, this property allows for *memoizing* easily
+/// operations on terms like substitution, shifting, type checking, etc. It also facilitates the
+/// [building of terms](super::term::builder) which are named or use named terms.
+///
+/// While [`Term`] is the most important type, it is not the only one. The arena has a general
+/// concept of *dwellers*, which corresponds to types which have the same, desirable properties as
+/// terms.
+///
+/// This paradigm of memory management is akin to what is usually lectured for Binary Decision
+/// Diagrams (BDD) management. Additionally, it makes use of Rust features to provide a clean
+/// interface: the arena type is invariant over its lifetime argument (usually called `'arena`),
+/// which together with the [`use_arena`] function, enforces strong guarantees on how the arena can
+/// be used, particularly if several of them are used simultaneously.
+///
+/// Early versions of this system are freely inspired by an assignment designed by
+/// [Jacques-Henri Jourdan](<https://jhjourdan.mketjh.fr>).
+pub struct Arena<'arena> {
+    pub(super) alloc: &'arena Bump,
+
+    /// enforces invariances over lifetime parameter
+    _phantom: PhantomData<*mut &'arena ()>,
+
+    // Hashconsing of the various dwellers, at the heart of the uniqueness property
+    // Please note that [`Level`] behave differently because it has an additional *reduced form*
+    // invariant.
+    pub(super) hashcons_terms: HashSet<&'arena super::term::Node<'arena>>,
+    pub(super) hashcons_decls: HashSet<&'arena super::declaration::Node<'arena>>,
+    pub(super) hashcons_levels: HashMap<&'arena super::level::Node<'arena>, super::level::Level<'arena>>,
+
+    named_decls: HashMap<&'arena str, Declaration<'arena>>,
+    named_terms: HashMap<&'arena str, Term<'arena>>,
+
+    /// Hash maps used to speed up certain algorithms. See also `OnceCell`s in [`Term`]
+    pub(super) mem_subst: HashMap<(Term<'arena>, Term<'arena>, usize), Term<'arena>>,
+    // TODO shift hashmap (see #45)
+    // requires the design of an additional is_certainly_closed predicate in terms.
+}
+
+/// This function is the main function that the kernel exports. Most importantly, it is the only
+/// one to provide an entry point for Arena objects, by means of a closure provided by the end
+/// user.
+///
+/// Such an interface is the most elegant way to ensure the one-to-one correspondence between
+/// lifetime parameters and [`Arena`] objects.
+///
+/// To generate the `alloc` object in this function is necessary, as this is the main way to
+/// "create" a lifetime variable which makes sense. That way, `'arena` is valid exactly during
+/// the execution of the function `f`.
+pub fn use_arena<F, T>(f: F) -> T
+where
+    F: for<'arena> FnOnce(&mut Arena<'arena>) -> T,
+{
+    let alloc = Bump::new();
+    let mut arena = Arena::new(&alloc);
+    f(&mut arena)
+}
+
+impl<'arena> Arena<'arena> {
+    /// Allocates a new memory arena. As detailed in the [`use_arena`] function, it is necessary to
+    /// externalise the generation of the [`bumpalo::Bump`] object.
+    fn new(alloc: &'arena Bump) -> Self {
+        Arena {
+            alloc,
+            _phantom: PhantomData,
+
+            hashcons_terms: HashSet::new(),
+            hashcons_decls: HashSet::new(),
+            hashcons_levels: HashMap::new(),
+
+            named_decls: HashMap::new(),
+            named_terms: HashMap::new(),
+
+            mem_subst: HashMap::new(),
+        }
+    }
+
+    /// Stores a slice of levels in the arena.
+    ///
+    /// This is most importantly used by [instantiated
+    /// declarations](`super::declaration::instantiatedDeclaration`).
+    pub(crate) fn store_level_slice(&mut self, slice: &[Level<'arena>]) -> &'arena [Level<'arena>] {
+        self.alloc.alloc_slice_copy(slice)
+    }
+
+    /// Stores a string in the arena.
+    ///
+    /// This is typically done to ensure strings live long enough when manipulating them.
+    pub(crate) fn store_name(&mut self, name: &str) -> &'arena str {
+        self.alloc.alloc_str(name)
+    }
+
+    /// Binds a term to a given name.
+    pub fn bind(&mut self, name: &str, t: Term<'arena>) {
+        let name = self.store_name(name);
+        self.named_terms.insert(name, t);
+    }
+
+    /// Binds a declaration to a given name.
+    pub fn bind_decl(&mut self, name: &str, decl: Declaration<'arena>) {
+        let name = self.store_name(name);
+        self.named_decls.insert(name, decl);
+    }
+
+    /// Retrieves the binding of a given name, if one exists.
+    pub fn get_binding(&self, name: &str) -> Option<Term<'arena>> {
+        self.named_terms.get(name).copied()
+    }
+
+    /// Retrieves the declaration binding of a given name, if one exists.
+    pub fn get_binding_decl(&self, name: &str) -> Option<Declaration<'arena>> {
+        self.named_decls.get(name).copied()
+    }
+}
+
+/// This macro generates two types, $dweller and Node, parametrised by a lifetime. These types are
+/// associated to a set of traits that they are expected to have by living in an arena.
+macro_rules! new_dweller {
+    ($dweller: ident, $header: ident, $payload: ident) => {
+        #[doc = concat!("A ", stringify!($dweller), ".
+
+This type is a dweller of an [arena](crate::memory::arena::Arena). For detailed
+information about the content of this type, please refer to the documentation of its
+[payload](", stringify!($payload), ").
+
+This type is associated, through its lifetime argument, to an [`Arena`], where it
+lives. There, it is guaranteed to be unique, which helps to accelerate a variety of
+algorithms. It is fundamentally a pointer to an internal structure, called a Node,
+which itself contains the [core content](", stringify!($payload), ").
+
+Additionally, the Node contains lazy structures which typically further helps
+accelerating specific algorithms.")]
+        #[derive(Clone, Copy)]
+        pub struct $dweller<'arena>(&'arena Node<'arena>, std::marker::PhantomData<*mut &'arena ()>);
+
+        pub(super) struct Node<'arena> {
+            header: $header<'arena>,
+            payload: $payload<'arena>,
+        }
+
+        impl<'arena> $dweller<'arena> {
+            fn new(node: &'arena Node<'arena>) -> Self {
+                $dweller(node, std::marker::PhantomData)
+            }
+        }
+
+        #[doc = concat!(stringify!($dweller), "s are arguably smart pointers, and as such, can be
+directly dereferenced to their associated payload.
+
+This is done for convenience, as it allows to manipulate the terms relatively seamlessly.
+
+# Example
+
+For a [`Term`](crate::memory::term::Term), it is possible to write:
+```
+# use kernel::memory::arena::use_arena;
+# use kernel::memory::term::Payload::*;
+# use kernel::memory::term::builder::prop;
+# use_arena(|arena| {
+# let t = arena.build(prop()).unwrap();
+match *t {
+    Abs(_, t2) => t2.beta_reduction(arena),
+    App(t1, _) => t1,
+    _ => t,
+}
+# ;})
+```
+Please note that this trait has some limits. For instance, the notations used to match against
+a *pair* of", stringify!($dweller), "s still requires some convolution.")]
+        impl<'arena> std::ops::Deref for $dweller<'arena> {
+            type Target = $payload<'arena>;
+
+            fn deref(&self) -> &Self::Target {
+                &self.0.payload
+            }
+        }
+
+        #[doc = concat!("Debug mode only prints the payload of a ", stringify!($dweller), ".
+
+Apart from enhancing debug readability, this reimplementation is surprisingly necessary: in
+the case of terms for instance, and because they may refer to themselves in the payload, the
+default debug implementation recursively calls itself until the stack overflows.")]
+        impl<'arena> std::fmt::Debug for $dweller<'arena> {
+            fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+                self.0.payload.fmt(f)
+            }
+        }
+
+        #[doc = concat!("Because ", stringify!($dweller), "s are unique in the arena, it is
+sufficient to compare their locations in memory to test equality.")]
+        impl<'arena> PartialEq<Self> for $dweller<'arena> {
+            fn eq(&self, rhs: &Self) -> bool {
+                std::ptr::eq(self.0, rhs.0)
+            }
+        }
+
+        impl<'arena> Eq for $dweller<'arena> {}
+
+        #[doc = concat!("Because ", stringify!($dweller), "s are unique in the arena, it is
+sufficient to compare their locations in memory to test equality. In particular, hash can
+also be computed from the location")]
+        impl<'arena> std::hash::Hash for $dweller<'arena> {
+            fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+                std::ptr::hash(self.0, state)
+            }
+        }
+
+        impl<'arena> PartialEq<Self> for Node<'arena> {
+            fn eq(&self, x: &Self) -> bool {
+                self.payload == x.payload
+            }
+        }
+
+        impl<'arena> Eq for Node<'arena> {}
+
+        /// Nodes are not guaranteed to be unique. Nonetheless, only the payload matters and characterises
+        /// the value. Which means computing the hash for nodes can be restricted to hashing their
+        /// payloads.
+        impl<'arena> std::hash::Hash for Node<'arena> {
+            fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+                self.payload.hash(state);
+            }
+        }
+    };
+}
+
+pub(super) use new_dweller;

kernel/src/memory/declaration/builder.rs

+//! A collection of safe functions to build [`Declaration`]s. and [`InstantiatedDeclaration`]s.
+//!
+//! This module provides two main ways of building these. The first one is via closures: users can
+//! manipulate closures and create bigger ones which, when [built](Arena::build), provide the expected
+//! term.
+//!
+//! The overall syntax remains transparent to the user. This means the user focuses on the
+//! structure of the term they want to build, while the [closures](`BuilderTrait`) internally build an appropriate
+//! logic; namely verifying the correct amount of variables have been supplied or bound.
+
+use derive_more::Display;
+
+use super::{Declaration, InstantiatedDeclaration};
+use crate::error::{Error, Result, ResultDecl, ResultInstantiatedDecl};
+use crate::memory::arena::Arena;
+use crate::memory::level::builder as level;
+use crate::memory::term::builder as term;
+
+#[non_exhaustive]
+#[derive(Clone, Debug, Display, Eq, PartialEq)]
+pub enum DeclarationError<'arena> {
+    #[display(fmt = "expected {_0} universe variables, got {_1}")]
+    IncorrectVariableNumber(usize, usize),
+
+    #[display(fmt = "unknown declaration {_0}")]
+    UnknownDeclaration(&'arena str),
+}
+
+/// The trait of builders producing declarations.
+///
+/// Note that, unlike the other building traits, this one only takes an arena as an argument.
+/// This is because declarations cannot be declared locally (that is, within a context where some
+/// extra local variables are bound by lambda-abstraction).
+pub trait BuilderTrait<'build> = for<'arena> FnOnce(&mut Arena<'arena>) -> ResultDecl<'arena>;
+
+pub trait InstantiatedBuilderTrait<'build> =
+    for<'arena> FnOnce(&mut Arena<'arena>, &level::Environment<'build>) -> ResultInstantiatedDecl<'arena>;
+
+impl<'arena> Arena<'arena> {
+    /// Returns the declaration built from the given closure, provided with an empty context, at
+    /// depth 0.
+    #[inline]
+    pub fn build_declaration<'build, F: BuilderTrait<'build>>(&mut self, f: F) -> ResultDecl<'arena> {
+        f(self)
+    }
+
+    /// Returns the instantiated declaration built from the given closure, provided with an empty
+    /// context, at depth 0.
+    #[inline]
+    pub fn build_instantiated_declaration<'build, F: InstantiatedBuilderTrait<'build>>(
+        &mut self,
+        f: F,
+    ) -> ResultInstantiatedDecl<'arena> {
+        f(self, &level::Environment::new())
+    }
+}
+
+/// Returns a builder creating `term`, where universe variables are described by `vars`.
+pub fn declaration<'build, F: term::BuilderTrait<'build>>(term: F, vars: &[&'build str]) -> impl BuilderTrait<'build> {
+    let len = vars.len();
+    let lvl_env = vars.iter().enumerate().map(|(n, name)| (*name, n)).collect();
+    move |arena| Ok(Declaration::new(term(arena, &term::Environment::new(), &lvl_env, 0.into())?, len))
+}
+
+/// Template of declarations.
+#[derive(Clone, Debug, Display, PartialEq, Eq)]
+pub enum Builder<'build> {
+    #[display(fmt = "{_0}")]
+    Decl(Box<term::Builder<'build>>, Vec<&'build str>),
+}
+
+impl<'build> Builder<'build> {
+    /// Realise a builder into a [`Declaration`]. This internally uses functions described in
+    /// the [builder](`crate::memory::declaration::builder`) module.
+    pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultDecl<'arena> {
+        arena.build_declaration(self.partial_application())
+    }
+
+    fn partial_application(&self) -> impl BuilderTrait<'build> + '_ {
+        |arena| self.realise_in_context(arena)
+    }
+
+    fn realise_in_context<'arena>(&self, arena: &mut Arena<'arena>) -> ResultDecl<'arena> {
+        match self {
+            Builder::Decl(term, vars) => declaration(term.partial_application(), vars.as_slice())(arena),
+        }
+    }
+}
+
+fn try_build_instance<'arena, 'build>(
+    decl: Declaration<'arena>,
+    levels: &'build [level::Builder<'build>],
+    arena: &mut Arena<'arena>,
+    env: &level::Environment<'build>,
+) -> ResultInstantiatedDecl<'arena> {
+    let levels = levels.iter().map(|level_builder| level_builder.realise_in_context(arena, env)).collect::<Result<Vec<_>>>()?;
+
+    if decl.1 == levels.len() {
+        Ok(InstantiatedDeclaration::instantiate(decl, levels.as_slice(), arena))
+    } else {
+        Err(Error {
+            kind: DeclarationError::IncorrectVariableNumber(decl.1, levels.len()).into(),
+        })
+    }
+}
+
+/// Returns a builder creating the declaration built by `decl` instantiated with the universe
+/// levels `levels`.
+///
+/// Please note that this is the only function from the closure API requiring the use of Builders.
+/// This is by choice, as opposed to the other possibility, where `levels` would be a slice over
+/// `Box<dyn level::BuilderTrait>`, which is not interesting performance-wise.
+pub fn instance<'build, F: BuilderTrait<'build>>(
+    decl: F,
+    levels: &'build [level::Builder<'build>],
+) -> impl InstantiatedBuilderTrait<'build> {
+    move |arena, env| try_build_instance(decl(arena)?, levels, arena, env)
+}
+
+/// Returns a builder creating the declaration bound by `name`, instantiated with the universe
+/// levels `levels`.
+pub fn var<'build>(name: &'build str, levels: &'build [level::Builder<'build>]) -> impl InstantiatedBuilderTrait<'build> {
+    move |arena, env| {
+        let decl = arena.get_binding_decl(name).ok_or(Error {
+            kind: DeclarationError::UnknownDeclaration(arena.store_name(name)).into(),
+        })?;
+        try_build_instance(decl, levels, arena, env)
+    }
+}
+
+/// A builder for instantiated declarations.
+///
+/// While there is fundamentally only one way to instantiate a declaration, this builder exposes
+/// two variants: the [first](`InstantiatedBuilder::Instance`) is to be used typically through the
+/// API, in a context where, for instance, the associated declaration is not bound in the arena.
+///
+/// On the other hand, the [second variant](`InstantiatedBuilder::Var`) is typically used by the
+/// parser, as it corresponds to the only possible scenario in a file.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum InstantiatedBuilder<'build> {
+    Instance(Box<Builder<'build>>, Vec<level::Builder<'build>>),
+
+    Var(&'build str, Vec<level::Builder<'build>>),
+}
+
+impl<'arena> std::fmt::Display for InstantiatedBuilder<'arena> {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        use InstantiatedBuilder::*;
+        match self {
+            Instance(decl, params) => {
+                write!(f, "{decl}.{{")?;
+                params.iter().try_for_each(|level| write!(f, "{level}, "))?;
+                write!(f, "}}")
+            },
+            Var(decl, params) => {
+                write!(f, "{decl}.{{")?;
+                params.iter().try_for_each(|level| write!(f, "{level}, "))?;
+                write!(f, "}}")
+            },
+        }
+    }
+}
+impl<'build> InstantiatedBuilder<'build> {
+    /// Realise a builder into an [`InstantiatedDeclaration`]. This internally uses functions described in
+    /// the [builder](`crate::memory::declaration::builder`) module.
+    pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultInstantiatedDecl<'arena> {
+        arena.build_instantiated_declaration(self.partial_application())
+    }
+
+    pub(in crate::memory) fn partial_application(&'build self) -> impl InstantiatedBuilderTrait<'build> {
+        |arena, lvl_env| self.realise_in_context(arena, lvl_env)
+    }
+
+    fn realise_in_context<'arena>(
+        &'build self,
+        arena: &mut Arena<'arena>,
+        lvl_env: &level::Environment<'build>,
+    ) -> ResultInstantiatedDecl<'arena> {
+        use InstantiatedBuilder::*;
+        match self {
+            Instance(decl, levels) => instance(decl.partial_application(), levels)(arena, lvl_env),
+            Var(name, levels) => var(name, levels)(arena, lvl_env),
+        }
+    }
+}

kernel/src/memory/declaration/mod.rs

+//! universe-polymorphic declarations.
+
+use std::cell::OnceCell;
+use std::fmt;
+
+use derive_more::Display;
+
+use super::arena::Arena;
+use super::level::Level;
+use super::term::Term;
+use crate::error::ResultTerm;
+
+pub mod builder;
+
+/// A declaration is a term where some of its constituting universe levels may contain
+/// universe-polymorphic variables.
+///
+/// None of these variables may be "free".
+///
+/// Declarations can be instantiated to create [`InstantiatedDeclaration`]s, which can in turn be
+/// incorporated into [`Term`]s.
+#[derive(Copy, Clone, Debug, Display, Eq, PartialEq, Hash)]
+#[display(fmt = "{_0}")]
+pub struct Declaration<'arena>(pub(crate) Term<'arena>, pub(crate) usize);
+
+super::arena::new_dweller!(InstantiatedDeclaration, Header, Payload);
+
+/// An instantiated declaration.
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+pub struct Payload<'arena> {
+    /// The declaration being instantiated
+    pub decl: Declaration<'arena>,
+
+    /// The parameters used to instantiate it
+    pub params: &'arena [Level<'arena>],
+}
+
+struct Header<'arena> {
+    /// The corresponding term, where levels have been substituted.
+    term: OnceCell<Term<'arena>>,
+}
+
+impl<'arena> fmt::Display for InstantiatedDeclaration<'arena> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self.0.header.term.get() {
+            Some(term) => write!(f, "{term}"),
+            None => {
+                write!(f, "({}).{{", self.0.payload.decl)?;
+
+                let mut iter = self.0.payload.params.iter();
+
+                iter.next().map(|level| write!(f, "{level}")).unwrap_or(Ok(()))?;
+                iter.try_for_each(|level| write!(f, ", {level}"))?;
+
+                write!(f, "}}")
+            },
+        }
+    }
+}
+
+impl<'arena> Declaration<'arena> {
+    pub(crate) fn new(term: Term<'arena>, vars: usize) -> Self {
+        Self(term, vars)
+    }
+}
+
+impl<'arena> InstantiatedDeclaration<'arena> {
+    /// Creates a new instantiated declaration from its base components. It is not verified that
+    /// the provided slice matches in length the number of expected Levels.
+    pub(crate) fn instantiate(decl: Declaration<'arena>, params: &[Level<'arena>], arena: &mut Arena<'arena>) -> Self {
+        let new_node = Node {
+            header: Header {
+                term: OnceCell::new(),
+            },
+            payload: Payload {
+                decl,
+                params: arena.store_level_slice(params),
+            },
+        };
+
+        match arena.hashcons_decls.get(&new_node) {
+            Some(addr) => Self::new(addr),
+            None => {
+                let addr = arena.alloc.alloc(new_node);
+                arena.hashcons_decls.insert(addr);
+                Self::new(addr)
+            },
+        }
+    }
+
+    /// Returns the term linked to a definition in a given environment.
+    pub fn get_term(self, arena: &mut Arena<'arena>) -> Term<'arena> {
+        *self.0.header.term.get_or_init(|| self.0.payload.decl.0.substitute_univs(self.0.payload.params, arena))
+    }
+
+    /// Tries to type the generic underlying declaration. If it works, returns the type
+    /// corresponding to the instantiated declaration, via a universe-variable substitution.
+    pub(crate) fn get_type_or_try_init<F>(self, f: F, arena: &mut Arena<'arena>) -> ResultTerm<'arena>
+    where
+        F: FnOnce(Term<'arena>, &mut Arena<'arena>) -> ResultTerm<'arena>,
+    {
+        let term = self.0.payload.decl.0;
+        term.get_type_or_try_init(|| f(term, arena)).map(|type_| type_.substitute_univs(self.0.payload.params, arena))
+    }
+}

kernel/src/memory/level/builder.rs

+//! A collection of safe functions to build [`Level`]s.
+//!
+//! This module provides two main ways of building terms. The first one is via closures: users can
+//! manipulate closures and create bigger ones which, when [built](Arena::build_level), provide the expected
+//! level.
+//!
+//! The overall syntax remains transparent to the user. This means the user focuses on the
+//! structure of the term they want to build, while the [closures](`BuilderTrait`) internally build an appropriate
+//! logic: converting regular universe variables names into their corresponding variable numbers.
+//!
+//! The other way to proceed is built on top of the latter. Users can also manipulate a sort of
+//! *high-level level* or *template*, described by the public enumeration [`Builder`], and at any
+//! moment, [realise](Builder::realise) it.
+
+use std::collections::HashMap;
+
+use derive_more::Display;
+
+use super::Level;
+use crate::error::{Error, ResultLevel};
+use crate::memory::arena::Arena;
+
+#[non_exhaustive]
+#[derive(Clone, Debug, Display, Eq, PartialEq)]
+pub enum LevelError<'arena> {
+    #[display(fmt = "unknown universe variable {}", _0)]
+    VarNotFound(&'arena str),
+}
+
+/// Local environment used to store correspondence between locally-bound variables and the pair
+/// (depth at which they were bound, their type)
+pub type Environment<'build> = HashMap<&'build str, usize>;
+
+/// The trait of closures which build levels with an adequate logic.
+///
+/// A call with a couple of arguments `(arena, env)` of a closure with this trait should
+/// build a definite level in the [`Arena`] `arena`.
+pub trait BuilderTrait<'build> = for<'arena> FnOnce(&mut Arena<'arena>, &Environment<'build>) -> ResultLevel<'arena>;
+
+impl<'arena> Arena<'arena> {
+    /// Returns the level built from the given closure, provided with a Level environment, which binds names to `usize`s
+    #[inline]
+    pub fn build_level<'build, F: BuilderTrait<'build>>(&mut self, f: F) -> ResultLevel<'arena> {
+        f(self, &Environment::new())
+    }
+}
+
+/// Returns a closure building a universe variable associated to `name`
+#[inline]
+pub const fn var(name: &str) -> impl BuilderTrait<'_> {
+    move |arena, env| {
+        env.get(name).map(|lvl| Level::var(*lvl, arena)).ok_or(Error {
+            kind: LevelError::VarNotFound(arena.store_name(name)).into(),
+        })
+    }
+}
+
+/// Returns a closure building the 0 level.
+#[inline]
+pub const fn zero<'build>() -> impl BuilderTrait<'build> {
+    |arena, _| Ok(Level::zero(arena))
+}
+
+/// Returns a closure building a constant level.
+#[inline]
+pub const fn const_<'build>(n: usize) -> impl BuilderTrait<'build> {
+    move |arena, _| Ok(Level::from(n, arena))
+}
+
+/// Returns a closure building the sum of `u` and a constant `n`.
+#[inline]
+#[no_coverage]
+pub const fn plus<'build, F: BuilderTrait<'build>>(u: F, n: usize) -> impl BuilderTrait<'build> {
+    move |arena, env| Ok(u(arena, env)?.add(n, arena))
+}
+
+/// Returns a closure building the successor of a level built from the given closure `u1`
+#[inline]
+#[no_coverage]
+pub const fn succ<'build, F1: BuilderTrait<'build>>(u1: F1) -> impl BuilderTrait<'build> {
+    |arena, env| Ok(u1(arena, env)?.succ(arena))
+}
+
+/// Returns a closure building the max of two levels built from the given closures `u1` and
+/// `u2`.
+#[inline]
+#[no_coverage]
+pub const fn max<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(u1: F1, u2: F2) -> impl BuilderTrait<'build> {
+    |arena, env| Ok(u1(arena, env)?.max(u2(arena, env)?, arena))
+}
+
+/// Returns a closure building the imax of two levels built from the given closures `u1` and
+/// `u2`.
+#[inline]
+#[no_coverage]
+pub const fn imax<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(u1: F1, u2: F2) -> impl BuilderTrait<'build> {
+    |arena, env| Ok(u1(arena, env)?.imax(u2(arena, env)?, arena))
+}
+
+/// Template of levels.
+///
+/// A [`Builder`] describes a level in a naive but easy to build manner. It strongly resembles the
+/// [`Level`] type, except that the `Var` constructor include a name, as in the syntactic way of
+/// writing levels. Because its purpose is to provide an easy way to build terms, even through the
+/// API, it offers different ways to build some terms, for convenience.
+#[derive(Clone, Debug, Display, PartialEq, Eq)]
+pub enum Builder<'builder> {
+    #[display(fmt = "0")]
+    Zero,
+
+    Const(usize),
+
+    #[display(fmt = "({_0}) + {_1}")]
+    Plus(Box<Builder<'builder>>, usize),
+
+    #[display(fmt = "S({_0})")]
+    Succ(Box<Builder<'builder>>),
+
+    #[display(fmt = "max({_0}, {_1})")]
+    Max(Box<Builder<'builder>>, Box<Builder<'builder>>),
+
+    #[display(fmt = "imax({_0}, {_1})")]
+    IMax(Box<Builder<'builder>>, Box<Builder<'builder>>),
+
+    Var(&'builder str),
+}
+
+impl<'build> Builder<'build> {
+    /// Realise a builder into a [`Level`]. This internally uses functions described in
+    /// the [builder](`crate::memory::level::builder`) module.
+    pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultLevel<'arena> {
+        arena.build_level(self.partial_application())
+    }
+
+    pub(in crate::memory) fn partial_application(&self) -> impl BuilderTrait<'build> + '_ {
+        |arena, env| self.realise_in_context(arena, env)
+    }
+
+    pub(in crate::memory) fn realise_in_context<'arena>(
+        &self,
+        arena: &mut Arena<'arena>,
+        env: &Environment<'build>,
+    ) -> ResultLevel<'arena> {
+        use Builder::*;
+        match *self {
+            Zero => zero()(arena, env),
+            Const(c) => const_(c)(arena, env),
+            Plus(ref u, n) => plus(u.partial_application(), n)(arena, env),
+            Succ(ref l) => succ(l.partial_application())(arena, env),
+            Max(ref l, ref r) => max(l.partial_application(), r.partial_application())(arena, env),
+            IMax(ref l, ref r) => imax(l.partial_application(), r.partial_application())(arena, env),
+            Var(s) => var(s)(arena, env),
+        }
+    }
+}
+
+#[cfg(test)]
+pub(crate) mod raw {
+    use super::*;
+
+    pub trait BuilderTrait = for<'arena> FnOnce(&mut Arena<'arena>) -> Level<'arena>;
+
+    impl<'arena> Arena<'arena> {
+        pub(crate) fn build_level_raw<F: BuilderTrait>(&mut self, f: F) -> Level<'arena> {
+            f(self)
+        }
+    }
+
+    pub const fn var(id: usize) -> impl BuilderTrait {
+        move |arena| Level::var(id, arena)
+    }
+
+    pub const fn zero() -> impl BuilderTrait {
+        |arena| Level::zero(arena)
+    }
+
+    pub const fn succ<F1: BuilderTrait>(u1: F1) -> impl BuilderTrait {
+        |arena| {
+            let u1 = u1(arena);
+            u1.succ(arena)
+        }
+    }
+
+    pub const fn max<F1: BuilderTrait, F2: BuilderTrait>(u1: F1, u2: F2) -> impl BuilderTrait {
+        |arena| {
+            let u1 = u1(arena);
+            let u2 = u2(arena);
+            u1.max(u2, arena)
+        }
+    }
+
+    pub const fn imax<F1: BuilderTrait, F2: BuilderTrait>(u1: F1, u2: F2) -> impl BuilderTrait {
+        |arena| {
+            let u1 = u1(arena);
+            let u2 = u2(arena);
+            u1.imax(u2, arena)
+        }
+    }
+}

kernel/src/memory/level/mod.rs

+//! Universe levels.
+
+use std::cell::OnceCell;
+use std::fmt::{Display, Formatter};
+use std::hash::Hash;
+
+use super::arena::Arena;
+
+super::arena::new_dweller!(Level, Header, Payload);
+
+pub mod builder;
+
+struct Header<'arena> {
+    /// The plus-form of a level
+    plus_form: OnceCell<(Level<'arena>, usize)>,
+}
+
+/// A universe level.
+///
+/// While types in the usual calculus of constructions live in types fully described with integers,
+/// more is needed when manipulating universe-polymorphic descriptions: precisely, the right amount
+/// of formal computation has to be introduced in order to account for universe-polymorphic
+/// variables.
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum Payload<'arena> {
+    /// The zero level (associated to Prop)
+    Zero,
+
+    /// The successor of a level
+    Succ(Level<'arena>),
+
+    /// The maximum of two levels
+    Max(Level<'arena>, Level<'arena>),
+
+    /// The impredicative maximum of two levels
+    IMax(Level<'arena>, Level<'arena>),
+
+    /// A universe-polymorphic variable
+    Var(usize),
+}
+
+impl Display for Level<'_> {
+    fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
+        match self.to_numeral() {
+            Some(n) => write!(f, "{n}"),
+            None => match **self {
+                Zero => unreachable!("Zero is a numeral"),
+                Succ(_) => {
+                    let (u, n) = self.plus();
+                    write!(f, "{u} + {n}")
+                },
+                Max(n, m) => write!(f, "max ({n}) ({m})"),
+                IMax(n, m) => write!(f, "imax ({n}) ({m})"),
+                Var(n) => write!(f, "u{n}"),
+            },
+        }
+    }
+}
+
+use Payload::*;
+
+impl<'arena> Level<'arena> {
+    /// This function is the base low-level function for creating levels.
+    ///
+    /// It enforces the uniqueness property of levels in the arena, as well as the reduced-form
+    /// invariant.
+    fn hashcons(payload: Payload<'arena>, arena: &mut Arena<'arena>) -> Self {
+        let new_node = Node {
+            payload,
+            header: Header {
+                plus_form: OnceCell::new(),
+            },
+        };
+
+        match arena.hashcons_levels.get(&new_node) {
+            Some(level) => *level,
+            None => {
+                // add the unreduced node to the arena
+                let node_unreduced = &*arena.alloc.alloc(new_node);
+                let level_unreduced = Level::new(node_unreduced);
+                arena.hashcons_levels.insert(node_unreduced, level_unreduced);
+
+                // compute its reduced form
+                let reduced = level_unreduced.normalize(arena);
+
+                // supersede the previous correspondence
+                arena.hashcons_levels.insert(node_unreduced, reduced);
+                arena.hashcons_levels.insert(reduced.0, reduced);
+
+                reduced
+            },
+        }
+    }
+
+    /// Returns the 0-level
+    pub(crate) fn zero(arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Zero, arena)
+    }
+
+    /// Returns the successor of a level
+    pub(crate) fn succ(self, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Succ(self), arena)
+    }
+
+    /// Returns the level corresponding to the maximum of two levels
+    pub(crate) fn max(self, right: Self, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Max(self, right), arena)
+    }
+
+    /// Returns the level corresponding to the impredicative maximum of two levels
+    pub(crate) fn imax(self, right: Self, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(IMax(self, right), arena)
+    }
+
+    /// Returns the level associated to a given variable.
+    pub(crate) fn var(id: usize, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Var(id), arena)
+    }
+
+    /// The addition of a level and an integer
+    pub fn add(self, n: usize, arena: &mut Arena<'arena>) -> Self {
+        if n == 0 {
+            self
+        } else {
+            let s = self.add(n - 1, arena);
+            s.succ(arena)
+        }
+    }
+
+    /// Builds a level from an integer
+    pub fn from(n: usize, arena: &mut Arena<'arena>) -> Self {
+        Level::zero(arena).add(n, arena)
+    }
+
+    /// Converts a level to an integer, if possible
+    pub fn to_numeral(self) -> Option<usize> {
+        let (u, n) = self.plus();
+        (*u == Zero).then_some(n)
+    }
+
+    /// Decomposes a level `l` in the best pair `(u, n)` s.t. `l = u + n`
+    pub fn plus(self) -> (Self, usize) {
+        *self.0.header.plus_form.get_or_init(|| match *self {
+            Succ(u) => {
+                let (u, n) = u.plus();
+                (u, n + 1)
+            },
+            _ => (self, 0),
+        })
+    }
+
+    /// Helper function for universe comparison. normalizes imax(es) as follows:
+    ///  - `imax(0, u) = u`
+    ///  - `imax(u, 0) = u`
+    ///  - `imax(u, S(v)) = max(u, S(v))`
+    ///  - `imax(u, imax(v, w)) = max(imax(u, w), imax(v, w))`
+    ///  - `imax(u, max(v, w)) = max(imax(u, v), imax(u, w))`
+    ///
+    /// The function also reduces max. This is further helpful when trying to print the type.
+    ///
+    /// Here, the imax normalization pushes imaxes to all have a `Var(i)` as the second argument. To solve this last case, one needs
+    /// to substitute `Var(i)` with `0` and `S(Var(i))`. This gives us a consistent way to unstuck the geq-checking.
+    fn normalize(self, arena: &mut Arena<'arena>) -> Self {
+        match *self {
+            IMax(u, v) => {
+                if u == v {
+                    u
+                } else {
+                    match &*v {
+                        Zero => v,
+                        Succ(_) => u.max(v, arena),
+                        IMax(_, vw) => Level::max(u.imax(*vw, arena), v, arena),
+                        Max(vv, vw) => Level::max(u.imax(*vv, arena), u.imax(*vw, arena), arena),
+                        _ => self,
+                    }
+                }
+            },
+
+            Max(u, v) => {
+                if u == v {
+                    u
+                } else {
+                    match (&*u, &*v) {
+                        (Zero, _) => v,
+                        (_, Zero) => u,
+                        (Succ(uu), Succ(vv)) => Level::max(*uu, *vv, arena).succ(arena),
+                        _ => self,
+                    }
+                }
+            },
+            _ => self,
+        }
+    }
+}
+
+#[cfg(test)]
+mod pretty_printing {
+
+    use crate::memory::arena::use_arena;
+    use crate::memory::level::builder::raw::*;
+    use crate::memory::level::Level;
+
+    #[test]
+    fn to_num() {
+        use_arena(|arena| {
+            assert_eq!(arena.build_level_raw(max(succ(zero()), zero())).to_numeral(), Some(1));
+            assert_eq!(arena.build_level_raw(max(succ(zero()), succ(var(0)))).to_numeral(), None);
+            assert_eq!(arena.build_level_raw(imax(var(0), zero())).to_numeral(), Some(0));
+            assert_eq!(arena.build_level_raw(imax(zero(), succ(zero()))).to_numeral(), Some(1))
+        })
+    }
+
+    #[test]
+    fn to_plus() {
+        use_arena(|arena| {
+            assert_eq!(arena.build_level_raw(succ(zero())).plus(), (Level::zero(arena), 1));
+        })
+    }
+
+    #[test]
+    fn to_pretty_print() {
+        use_arena(|arena| {
+            assert_eq!(
+                format!("{}", arena.build_level_raw(max(succ(zero()), imax(max(zero(), var(0)), succ(var(0)))))),
+                "max (1) (max (u0) (u0 + 1))"
+            )
+        })
+    }
+
+    #[test]
+    fn normalize() {
+        use_arena(|arena| {
+            let lvl = arena.build_level_raw(imax(zero(), imax(zero(), imax(succ(zero()), var(0)))));
+
+            assert_eq!(format!("{lvl}"), "max (imax (0) (u0)) (max (imax (0) (u0)) (imax (1) (u0)))")
+        })
+    }
+}

kernel/src/memory/mod.rs

+//! Abstracted memory manipulation primitives.
+//!
+//! This module provides a paradigm for building and manipulating [terms](term::Term) in the
+//! calculus of construction, centered around the notion of [arena](`arena::Arena`). Terms also
+//! rely on other structures like [declarations](declaration::Declaration) and [universe
+//! levels](level::Level).
+
+pub mod arena;
+pub mod declaration;
+pub mod level;
+pub mod term;

kernel/src/term/builders.rs → kernel/src/memory/term/builder.rs

-//! Collection of safe functions to build Terms
+//! A collection of safe functions to build [`Term`]s.
 //!
 //! This module provides two main ways of building terms. The first one is via closures: users can
 //! manipulate closures and create bigger ones which, when [built](Arena::build), provide the expected
@@ -16,12 +16,15 @@
 use derive_more::Display;
 use im_rc::hashmap::HashMap as ImHashMap;
 
-use super::arena::{Arena, DeBruijnIndex, Term, UniverseLevel};
+use super::{DeBruijnIndex, Term};
 use crate::error::{Error, ResultTerm};
+use crate::memory::arena::Arena;
+use crate::memory::declaration::builder as declaration;
+use crate::memory::level::builder as level;
 
 #[non_exhaustive]
 #[derive(Clone, Debug, Display, Eq, PartialEq)]
-pub enum DefinitionError<'arena> {
+pub enum TermError<'arena> {
     #[display(fmt = "unknown identifier {}", _0)]
     ConstNotFound(&'arena str),
 }
@@ -32,76 +35,87 @@ pub type Environment<'build, 'arena> = ImHashMap<&'build str, (DeBruijnIndex, Te
 
 /// The trait of closures which build terms with an adequate logic.
 ///
-/// A call with a triplet of arguments `(arena, env, index)` of a closure with this trait should
-/// build a definite term in the [`Arena`] `arena`, knowing the bindings declared in `environment`,
-/// provided that the term is built at a current depth `index`.
+/// A call with a quadruplet of arguments `(arena, env, lvl_env, index)` of a closure with this
+/// trait should build a definite term in the [`Arena`] `arena`, knowing the bindings declared in
+/// `env` and `lvl_env`, provided that the term is built at a current depth `index`.
 ///
-/// Please note that this is just a trait alias, meaning it enforces very little constraints: while
+/// Please note that this is just a trait alias, meaning it enforces few constraints: while
 /// functions in this module returning a closure with this trait are guaranteed to be sound, end
 /// users can also create their own closures satisfying `BuilderTrait`; this should be avoided.
-pub trait BuilderTrait<'build, 'arena> =
-    FnOnce(&mut Arena<'arena>, &Environment<'build, 'arena>, DeBruijnIndex) -> ResultTerm<'arena>;
+pub trait BuilderTrait<'build> = for<'arena> FnOnce(
+    &mut Arena<'arena>,
+    &Environment<'build, 'arena>,
+    &level::Environment<'build>,
+    DeBruijnIndex,
+) -> ResultTerm<'arena>;
 
 impl<'arena> Arena<'arena> {
     /// Returns the term built from the given closure, provided with an empty context, at depth 0.
     #[inline]
-    pub fn build<'build, F: BuilderTrait<'build, 'arena>>(&mut self, f: F) -> ResultTerm<'arena>
-    where
-        'arena: 'build,
-    {
-        f(self, &Environment::new(), 0.into())
+    pub fn build<'build, F: BuilderTrait<'build>>(&mut self, f: F) -> ResultTerm<'arena> {
+        f(self, &Environment::new(), &level::Environment::new(), 0.into())
     }
 }
 
 /// Returns a closure building a variable associated to the name `name`
 #[inline]
-pub const fn var<'build, 'arena>(name: &'build str) -> impl BuilderTrait<'build, 'arena> {
-    move |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
+pub const fn var(name: &str) -> impl BuilderTrait<'_> {
+    move |arena, env, _, depth| {
         env.get(name)
             .map(|(bind_depth, term)| {
                 // This is arguably an eager computation, it could be worth making it lazy,
                 // or at least memoizing it so as to not compute it again
-                let var_type = arena.shift(*term, usize::from(depth - *bind_depth), 0);
-                arena.var(depth - *bind_depth, var_type)
+                let var_type = term.shift(usize::from(depth - *bind_depth), 0, arena);
+                Term::var(depth - *bind_depth, var_type, arena)
             })
             .or_else(|| arena.get_binding(name))
             .ok_or(Error {
-                kind: DefinitionError::ConstNotFound(arena.store_name(name)).into(),
+                kind: TermError::ConstNotFound(arena.store_name(name)).into(),
             })
     }
 }
 
 /// Returns a closure building the Prop term.
 #[inline]
-pub const fn prop<'build, 'arena>() -> impl BuilderTrait<'build, 'arena> {
-    |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.prop())
+pub const fn prop<'build>() -> impl BuilderTrait<'build> {
+    |arena, _, _, _| Ok(Term::prop(arena))
 }
 
 /// Returns a closure building the Type `level` term.
 #[inline]
-pub const fn type_<'build, 'arena>(level: UniverseLevel) -> impl BuilderTrait<'build, 'arena> {
-    move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.type_(level))
+#[no_coverage]
+pub const fn type_<'build, F: level::BuilderTrait<'build>>(level: F) -> impl BuilderTrait<'build> {
+    move |arena, _, lvl_env, _| Ok(Term::sort(level(arena, lvl_env)?.succ(arena), arena))
 }
 
 /// Returns a closure building the Type `level` term (indirection from `usize`).
 #[inline]
-pub const fn type_usize<'build, 'arena>(level: usize) -> impl BuilderTrait<'build, 'arena> {
-    use num_bigint::BigUint;
-    move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.type_(BigUint::from(level).into()))
+pub const fn type_usize<'build>(level: usize) -> impl BuilderTrait<'build> {
+    move |arena, _, _, _| Ok(Term::type_usize(level, arena))
+}
+
+/// Returns a closure building the Sort `level` term.
+#[inline]
+#[no_coverage]
+pub const fn sort<'build, F: level::BuilderTrait<'build>>(level: F) -> impl BuilderTrait<'build> {
+    move |arena, _, lvl_env, _| Ok(Term::sort(level(arena, lvl_env)?, arena))
+}
+
+/// Returns a closure building the Sort `level` term (indirection from `usize`).
+#[inline]
+pub const fn sort_usize<'build>(level: usize) -> impl BuilderTrait<'build> {
+    move |arena, _, _, _| Ok(Term::sort_usize(level, arena))
 }
 
 /// Returns a closure building the application of two terms built from the given closures `u1` and
 /// `u2`.
 #[inline]
 #[no_coverage]
-pub const fn app<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
-    u1: F1,
-    u2: F2,
-) -> impl BuilderTrait<'build, 'arena> {
-    |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
-        let u1 = u1(arena, env, depth)?;
-        let u2 = u2(arena, env, depth)?;
-        Ok(arena.app(u1, u2))
+pub const fn app<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(u1: F1, u2: F2) -> impl BuilderTrait<'build> {
+    |arena, env, lvl_env, depth| {
+        let u1 = u1(arena, env, lvl_env, depth)?;
+        let u2 = u2(arena, env, lvl_env, depth)?;
+        Ok(u1.app(u2, arena))
     }
 }
 
@@ -109,16 +123,16 @@ pub const fn app<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTr
 /// type from `arg_type`.
 #[inline]
 #[no_coverage]
-pub const fn abs<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
+pub const fn abs<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(
     name: &'build str,
     arg_type: F1,
     body: F2,
-) -> impl BuilderTrait<'build, 'arena> {
-    move |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
-        let arg_type = arg_type(arena, env, depth)?;
+) -> impl BuilderTrait<'build> {
+    move |arena, env, lvl_env, depth| {
+        let arg_type = arg_type(arena, env, lvl_env, depth)?;
         let env = env.update(name, (depth, arg_type));
-        let body = body(arena, &env, depth + 1.into())?;
-        Ok(arena.abs(arg_type, body))
+        let body = body(arena, &env, lvl_env, depth + 1.into())?;
+        Ok(arg_type.abs(body, arena))
     }
 }
 
@@ -126,71 +140,89 @@ pub const fn abs<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTr
 /// of the type built from `arg_type`.
 #[inline]
 #[no_coverage]
-pub const fn prod<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
+pub const fn prod<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(
     name: &'build str,
     arg_type: F1,
     body: F2,
-) -> impl BuilderTrait<'build, 'arena> {
-    move |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| {
-        let arg_type = arg_type(arena, env, depth)?;
+) -> impl BuilderTrait<'build> {
+    move |arena, env, lvl_env, depth| {
+        let arg_type = arg_type(arena, env, lvl_env, depth)?;
         let env = env.update(name, (depth, arg_type));
-        let body = body(arena, &env, depth + 1.into())?;
-        Ok(arena.prod(arg_type, body))
+        let body = body(arena, &env, lvl_env, depth + 1.into())?;
+        Ok(arg_type.prod(body, arena))
     }
 }
 
+/// Returns a closure building the term associated to the instantiated declaration `decl`.
+#[inline]
+#[no_coverage]
+pub const fn decl<'build, F: declaration::InstantiatedBuilderTrait<'build>>(decl: F) -> impl BuilderTrait<'build> {
+    move |arena, _, lvl_env, _| Ok(Term::decl(decl(arena, lvl_env)?, arena))
+}
+
 /// Template of terms.
 ///
 /// A Builder describes a term in a naive but easy to build manner. It strongly resembles the
-/// [payload](`crate::term::arena::Payload`) type, except that `Var`, `Abs` and `Prod` constructors
+/// [payload](`crate::memory::term::Payload`) type, except that `Var`, `Abs` and `Prod` constructors
 /// include a name, as in the classic way of writing lambda-terms (i.e. no de Bruijn indices
-/// involved).
+/// involved). Because its purpose is to provide an easy way to build terms, even through the API,
+/// it offers different ways to build some terms, for convenience.
 #[derive(Clone, Debug, Display, PartialEq, Eq)]
-pub enum Builder<'r> {
-    #[display(fmt = "{}", _0)]
-    Var(&'r str),
+pub enum Builder<'build> {
+    #[display(fmt = "{_0}")]
+    Var(&'build str),
 
     #[display(fmt = "Prop")]
     Prop,
 
-    #[display(fmt = "Type {}", _0)]
-    Type(usize),
+    #[display(fmt = "Type {_0}")]
+    Type(Box<level::Builder<'build>>),
 
-    #[display(fmt = "{} {}", _0, _1)]
-    App(Box<Builder<'r>>, Box<Builder<'r>>),
+    #[display(fmt = "Sort {_0}")]
+    Sort(Box<level::Builder<'build>>),
 
-    #[display(fmt = "\u{003BB} {}: {} \u{02192} {}", _0, _1, _2)]
-    Abs(&'r str, Box<Builder<'r>>, Box<Builder<'r>>),
+    #[display(fmt = "{_0} {_1}")]
+    App(Box<Builder<'build>>, Box<Builder<'build>>),
 
-    #[display(fmt = "\u{03A0} {}: {} \u{02192} {}", _0, _1, _2)]
-    Prod(&'r str, Box<Builder<'r>>, Box<Builder<'r>>),
+    #[display(fmt = "\u{003BB} {_0}: {_1} \u{02192} {_2}")]
+    Abs(&'build str, Box<Builder<'build>>, Box<Builder<'build>>),
+
+    #[display(fmt = "\u{03A0} {_0}: {_1} \u{02192} {_2}")]
+    Prod(&'build str, Box<Builder<'build>>, Box<Builder<'build>>),
+
+    Decl(Box<declaration::InstantiatedBuilder<'build>>),
 }
 
 impl<'build> Builder<'build> {
-    /// Build a terms from a [`Builder`]. This internally uses functions described in the
-    /// [builders](`crate::term::builders`) module.
+    /// Realise a builder into a [`Term`]. This internally uses functions described in
+    /// the [builder](`crate::memory::term::builder`) module.
     pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
         arena.build(self.partial_application())
     }
 
-    fn partial_application<'arena>(&self) -> impl BuilderTrait<'build, 'arena> + '_ {
-        |arena: &mut Arena<'arena>, env: &Environment<'build, 'arena>, depth| self.realise_in_context(arena, env, depth)
+    pub(in crate::memory) fn partial_application(&'build self) -> impl BuilderTrait<'build> {
+        |arena, env, lvl_env, depth| self.realise_in_context(arena, env, lvl_env, depth)
     }
 
     fn realise_in_context<'arena>(
-        &self,
+        &'build self,
         arena: &mut Arena<'arena>,
         env: &Environment<'build, 'arena>,
+        lvl_env: &level::Environment<'build>,
         depth: DeBruijnIndex,
     ) -> ResultTerm<'arena> {
         use Builder::*;
-        match *self {
-            Var(s) => var(s)(arena, env, depth),
-            Type(level) => type_usize(level)(arena, env, depth),
-            Prop => prop()(arena, env, depth),
-            App(ref l, ref r) => app(l.partial_application(), r.partial_application())(arena, env, depth),
-            Abs(s, ref arg, ref body) => abs(s, arg.partial_application(), body.partial_application())(arena, env, depth),
-            Prod(s, ref arg, ref body) => prod(s, arg.partial_application(), body.partial_application())(arena, env, depth),
+        match self {
+            Var(s) => var(s)(arena, env, lvl_env, depth),
+            Prop => prop()(arena, env, lvl_env, depth),
+            Type(ref level) => type_(level.partial_application())(arena, env, lvl_env, depth),
+            Sort(ref level) => sort(level.partial_application())(arena, env, lvl_env, depth),
+            App(ref l, ref r) => app(l.partial_application(), r.partial_application())(arena, env, lvl_env, depth),
+            Abs(s, ref arg, ref body) => abs(s, arg.partial_application(), body.partial_application())(arena, env, lvl_env, depth),
+            Prod(s, ref arg, ref body) => {
+                prod(s, arg.partial_application(), body.partial_application())(arena, env, lvl_env, depth)
+            },
+            Decl(ref decl_builder) => decl(decl_builder.partial_application())(arena, env, lvl_env, depth),
         }
     }
 }
@@ -199,56 +231,54 @@ impl<'build> Builder<'build> {
 pub(crate) mod raw {
     use super::*;
 
-    pub trait BuilderTrait<'arena> = FnOnce(&mut Arena<'arena>) -> Term<'arena>;
+    pub trait BuilderTrait = for<'arena> FnOnce(&mut Arena<'arena>) -> Term<'arena>;
 
     impl<'arena> Arena<'arena> {
-        pub(crate) fn build_raw<F: BuilderTrait<'arena>>(&mut self, f: F) -> Term<'arena> {
+        pub(crate) fn build_term_raw<F: BuilderTrait>(&mut self, f: F) -> Term<'arena> {
             f(self)
         }
     }
 
-    impl<'arena> Term<'arena> {
-        pub(crate) const fn into(self) -> impl BuilderTrait<'arena> {
-            move |_: &mut Arena<'arena>| self
+    pub const fn var<F: BuilderTrait>(index: DeBruijnIndex, type_: F) -> impl BuilderTrait {
+        move |arena| {
+            let ty = type_(arena);
+            Term::var(index, ty, arena)
         }
     }
 
-    pub const fn var<'arena, F: BuilderTrait<'arena>>(index: DeBruijnIndex, type_: F) -> impl BuilderTrait<'arena> {
-        move |env: &mut Arena<'arena>| {
-            let ty = type_(env);
-            env.var(index, ty)
-        }
+    pub const fn prop() -> impl BuilderTrait {
+        |arena| Term::prop(arena)
     }
 
-    pub const fn prop<'arena>() -> impl BuilderTrait<'arena> {
-        |env: &mut Arena<'arena>| env.prop()
+    pub const fn type_usize(level: usize) -> impl BuilderTrait {
+        move |arena| Term::type_usize(level, arena)
     }
 
-    pub const fn type_<'arena>(level: UniverseLevel) -> impl BuilderTrait<'arena> {
-        move |env: &mut Arena<'arena>| env.type_(level)
+    pub const fn sort_<F: level::raw::BuilderTrait>(level: F) -> impl BuilderTrait {
+        move |arena| Term::sort(level(arena), arena)
     }
 
-    pub const fn app<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
-        |env: &mut Arena<'arena>| {
-            let u1 = u1(env);
-            let u2 = u2(env);
-            env.app(u1, u2)
+    pub const fn app<F1: BuilderTrait, F2: BuilderTrait>(u1: F1, u2: F2) -> impl BuilderTrait {
+        |arena| {
+            let u1 = u1(arena);
+            let u2 = u2(arena);
+            u1.app(u2, arena)
         }
     }
 
-    pub const fn abs<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
-        |env: &mut Arena<'arena>| {
-            let u1 = u1(env);
-            let u2 = u2(env);
-            env.abs(u1, u2)
+    pub const fn abs<F1: BuilderTrait, F2: BuilderTrait>(u1: F1, u2: F2) -> impl BuilderTrait {
+        |arena| {
+            let u1 = u1(arena);
+            let u2 = u2(arena);
+            u1.abs(u2, arena)
         }
     }
 
-    pub const fn prod<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
-        |env: &mut Arena<'arena>| {
-            let u1 = u1(env);
-            let u2 = u2(env);
-            env.prod(u1, u2)
+    pub const fn prod<F1: BuilderTrait, F2: BuilderTrait>(u1: F1, u2: F2) -> impl BuilderTrait {
+        |arena| {
+            let u1 = u1(arena);
+            let u2 = u2(arena);
+            u1.prod(u2, arena)
         }
     }
 }

kernel/src/memory/term/mod.rs

+//! Terms in the calculus of construction.
+//!
+//! This module defines the core functions used to create and manipulate terms.
+
+use core::fmt;
+use std::cell::OnceCell;
+use std::fmt::Debug;
+
+use derive_more::{Add, Display, From, Into, Sub};
+
+use super::declaration::InstantiatedDeclaration;
+use super::level::Level;
+use crate::error::ResultTerm;
+use crate::memory::arena::Arena;
+
+pub mod builder;
+
+/// An index used to designate bound variables.
+#[derive(Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord, Hash)]
+pub struct DeBruijnIndex(usize);
+
+super::arena::new_dweller!(Term, Header, Payload);
+
+struct Header<'arena> {
+    /// lazy structure to store the weak-head normal form of a term
+    head_normal_form: OnceCell<Term<'arena>>,
+
+    /// lazy structure to store the type of a term
+    type_: OnceCell<Term<'arena>>,
+    // TODO(#45) is_certainly_closed: boolean underapproximation of whether a term is closed. This
+    // may greatly improve performance in shifting, along with a mem_shift hash map.
+}
+
+/// A term.
+///
+/// This enumeration has almost the same shape as the algebraic type of terms in the calculus of
+/// constructions.
+///
+/// One exception is the [variable](`Payload::Var`). Along with its de Bruijn index, the
+/// variable also stores its type, which is unique, and also ensures two variables with a different
+/// type do not share the same term in memory.
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+pub enum Payload<'arena> {
+    /// A variable, with its de Bruijn index and its type
+    //#[display(fmt = "{_0}")]
+    Var(DeBruijnIndex, Term<'arena>),
+
+    /// Sort i, the encoding of Prop and Type i type
+    Sort(Level<'arena>),
+
+    /// The application of two terms
+    //#[display(fmt = "{_0} {_1}")]
+    App(Term<'arena>, Term<'arena>),
+
+    /// The lambda-abstraction of a term: the argument type is on the left, the body on the right.
+    Abs(Term<'arena>, Term<'arena>),
+
+    /// The dependant product of the term on the right over all elements of the type on the left.
+    //#[display(fmt = "\u{03A0} {_0} \u{02192} {_1}")]
+    Prod(Term<'arena>, Term<'arena>),
+
+    /// An instance of a universe-polymorphic declaration
+    Decl(InstantiatedDeclaration<'arena>),
+}
+
+impl<'arena> fmt::Display for Payload<'arena> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match *self {
+            Var(index, _) => write!(f, "{index}"),
+            Sort(level) => match level.to_numeral() {
+                Some(n) => match n {
+                    0 => write!(f, "Prop"),
+                    1 => write!(f, "Type"),
+                    _ => write!(f, "Type {}", n - 1),
+                },
+                None => write!(f, "Sort {level}"),
+            },
+            App(fun, arg) => write!(f, "({fun}) ({arg})"),
+            Abs(argtype, body) => write!(f, "\u{003BB} {argtype} \u{02192} {body}"),
+            Prod(argtype, body) => write!(f, "\u{003A0} {argtype} \u{02192} {body}"),
+            Decl(decl) => write!(f, "{decl}"),
+        }
+    }
+}
+
+impl<'arena> fmt::Display for Term<'arena> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}", self.0.payload)
+    }
+}
+
+use Payload::*;
+
+impl<'arena> Term<'arena> {
+    /// This function is the base low-level function for creating terms.
+    ///
+    /// It enforces the uniqueness property of terms in the arena.
+    fn hashcons(payload: Payload<'arena>, arena: &mut Arena<'arena>) -> Self {
+        // There are concurrent designs here. hashcons could also take a node, which gives
+        // subsequent function some liberty in providing the other objects of the header: WHNF,
+        // type_ (unlikely, because not always desirable), is_certainly_closed.
+        let new_node = Node {
+            payload,
+            header: Header {
+                head_normal_form: OnceCell::new(),
+                type_: OnceCell::new(),
+            },
+        };
+
+        match arena.hashcons_terms.get(&new_node) {
+            Some(addr) => Term::new(addr),
+            None => {
+                let addr = arena.alloc.alloc(new_node);
+                arena.hashcons_terms.insert(addr);
+                Term::new(addr)
+            },
+        }
+    }
+
+    /// Returns a variable term with the given index and type
+    pub(crate) fn var(index: DeBruijnIndex, type_: Term<'arena>, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Var(index, type_), arena)
+    }
+
+    /// Returns the term corresponding to a proposition
+    pub(crate) fn prop(arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Sort(Level::zero(arena)), arena)
+    }
+
+    /// Returns the term associated to the sort of the given level
+    pub(crate) fn sort(level: Level<'arena>, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Sort(level), arena)
+    }
+
+    /// Returns the term corresponding to Type(level), casting level appropriately first
+    pub(crate) fn type_usize(level: usize, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Sort(Level::from(level + 1, arena)), arena)
+    }
+
+    /// Returns the term corresponding to Sort(level), casting level appropriately first
+    pub(crate) fn sort_usize(level: usize, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Sort(Level::from(level, arena)), arena)
+    }
+
+    /// Returns the application of one term to the other
+    pub(crate) fn app(self, arg: Self, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(App(self, arg), arena)
+    }
+
+    /// Returns the lambda-abstraction of the term `body`, with an argument of type `arg_type`.
+    ///
+    /// Please note that no verification is done that occurrences of this variable in `body` have
+    /// the same type.
+    pub(crate) fn abs(self, body: Self, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Abs(self, body), arena)
+    }
+
+    /// Returns the dependant product of the term `body`, over elements of `arg_type`.
+    ///
+    /// Please note that no verification is done that occurrences of this variable in `body` have
+    /// the same type.
+    pub(crate) fn prod(self, body: Self, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Prod(self, body), arena)
+    }
+
+    /// Returns the term associated to the given instantiated declaration.
+    pub(crate) fn decl(decl: InstantiatedDeclaration<'arena>, arena: &mut Arena<'arena>) -> Self {
+        Self::hashcons(Decl(decl), arena)
+    }
+
+    /// Returns the weak head normal form of the term, lazily computing the closure `f`.
+    pub(crate) fn get_whnf_or_init<F>(self, f: F) -> Self
+    where
+        F: FnOnce() -> Self,
+    {
+        *self.0.header.head_normal_form.get_or_init(f)
+    }
+
+    /// Returns the type of the term, lazily computing the closure `f`.
+    pub(crate) fn get_type_or_try_init<F>(self, f: F) -> ResultTerm<'arena>
+    where
+        F: FnOnce() -> ResultTerm<'arena>,
+    {
+        self.0.header.type_.get_or_try_init(f).copied()
+    }
+}
+
+impl<'arena> Arena<'arena> {
+    /// Returns the result of the substitution described by the key, lazily computing the closure `f`.
+    pub(crate) fn get_subst_or_init<F>(&mut self, key: &(Term<'arena>, Term<'arena>, usize), f: F) -> Term<'arena>
+    where
+        F: FnOnce(&mut Self) -> Term<'arena>,
+    {
+        match self.mem_subst.get(key) {
+            Some(res) => *res,
+            None => {
+                let res = f(self);
+                self.mem_subst.insert(*key, res);
+                res
+            },
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::memory::arena::use_arena;
+    use crate::memory::level::builder::raw::{var, *};
+    use crate::memory::term::builder::raw::*;
+
+    #[test]
+    fn display() {
+        use_arena(|arena| {
+            let decl_ = crate::memory::declaration::InstantiatedDeclaration::instantiate(
+                crate::memory::declaration::builder::Builder::Decl(crate::memory::term::builder::Builder::Prop.into(), Vec::new())
+                    .realise(arena)
+                    .unwrap(),
+                &Vec::new(),
+                arena,
+            );
+
+            let prop_ = crate::memory::term::Term::decl(decl_, arena);
+
+            assert_eq!(format!("{}", prop_), "(Prop).{}");
+            let vart = crate::memory::term::builder::raw::var;
+
+            let lvl = max(succ(var(0)), succ(var(1)));
+            let term = arena.build_term_raw(abs(
+                sort_(lvl),
+                abs(
+                    type_usize(0),
+                    abs(
+                        type_usize(1),
+                        prod(vart(1.into(), type_usize(1)), app(vart(1.into(), type_usize(1)), vart(2.into(), type_usize(0)))),
+                    ),
+                ),
+            ));
+
+            assert_eq!(format!("{}", term), "λ Sort max (u0) (u1) + 1 → λ Type → λ Type 1 → Π 1 → (1) (2)")
+        })
+    }
+}

kernel/src/term/arena.rs

-//! A comprehensive memory management unit for terms.
-//!
-//! This module defines the core functions used to manipulate an arena and its terms.
-
-use std::cell::OnceCell;
-use std::collections::{HashMap, HashSet};
-use std::fmt::Debug;
-use std::hash::Hash;
-use std::marker::PhantomData;
-use std::ops::Deref;
-
-use bumpalo::Bump;
-use derive_more::{Add, Display, From, Into, Sub};
-use num_bigint::BigUint;
-
-use crate::error::ResultTerm;
-
-/// An index used to designate bound variables.
-#[derive(Add, Copy, Clone, Debug, Default, Display, PartialEq, Eq, Hash, From, Into, PartialOrd, Ord, Sub)]
-pub struct DeBruijnIndex(usize);
-
-/// A level of universe, used to build terms of the form `Type i`.
-///
-/// In type theory, this corresponds to the construction of universes "à la Russell", the purpose
-/// of which is to give a hierarchy to these types, so as to preserve soundness against paradoxes
-/// akin to Russell's. Universe levels can be arbitrarily large, and, with good faith, they are
-/// represented with *big unsigned integers*, limited only by the memory of the operating computer.
-#[derive(Add, Clone, Debug, Default, Display, PartialEq, Eq, From, Hash, PartialOrd, Ord, Sub)]
-pub struct UniverseLevel(BigUint);
-
-/// A comprehensive memory management unit for terms.
-///
-/// An arena is a location in memory where a group of terms with several properties is stored. Most
-/// importantly, it ensures that all terms living in the arena are syntactically unique, which
-/// accelerates many algorithms. In particular, this property allows for *memoizing* easily
-/// operations on terms like substitution, shifting, type checking, etc. It also facilitates the
-/// [building of terms](super::builders) which are named or use named terms.
-///
-/// This paradigm of memory management is akin to what is usually lectured for Binary Decision
-/// Diagrams (BDD) management. Additionally, it makes use of Rust features to provide a clean
-/// interface: the arena type is invariant over its lifetime argument (usually called `'arena`),
-/// which together with the [`use_arena`] function, enforces strong guarantees on how the arena can
-/// be used, particularly if several of them are used simultaneously.
-///
-/// Early versions of this system are freely inspired by an assignment designed by
-/// [Jacques-Henri Jourdan](<https://jhjourdan.mketjh.fr>).
-pub struct Arena<'arena> {
-    alloc: &'arena Bump,
-
-    // enforces invariances over lifetime parameter
-    _phantom: PhantomData<*mut &'arena ()>,
-
-    // Hashconsing of terms, at the heart of the uniqueness property
-    hashcons: HashSet<&'arena Node<'arena>>,
-    named_terms: HashMap<&'arena str, Term<'arena>>,
-
-    // Hash maps used to speed up certain algorithms. See also `OnceCell`s in [`Term`]
-    mem_subst: HashMap<(Term<'arena>, Term<'arena>, usize), Term<'arena>>,
-    // TODO shift hashmap (see #45)
-    // requires the design of an additional is_certainly_closed predicate in terms.
-}
-
-/// A term of the calculus of constructions.
-///
-/// This type is associated, through its lifetime argument, to an [`Arena`], where it lives. There,
-/// it is guaranteed to be unique, which accelerates many algorithms. It is fundamentally a pointer
-/// to an internal term structure, called a Node, which itself contains the core term, [`Payload`],
-/// which is what can be expected of a term.
-///
-/// Additionally, the Node contains lazy structures which indicate the result of certain
-/// transformation on the term, namely type checking and term reduction. Storing it directly here
-/// is both faster and takes overall less space than storing the result in a separate hash table.
-#[derive(Clone, Copy, Display, Eq)]
-#[display(fmt = "{}", "_0.payload")]
-pub struct Term<'arena>(
-    &'arena Node<'arena>,
-    // This marker ensures invariance over the 'arena lifetime.
-    PhantomData<*mut &'arena ()>,
-);
-
-#[derive(Debug, Eq)]
-struct Node<'arena> {
-    payload: Payload<'arena>,
-
-    // Lazy and aliasing-compatible structures for memoizing
-    head_normal_form: OnceCell<Term<'arena>>,
-    type_: OnceCell<Term<'arena>>,
-    // TODO is_certainly_closed: boolean underapproximation of whether a term is closed.
-    // This may greatly improve performance in shifting, along with a mem_shift hash map.
-}
-
-/// The essence of a term.
-///
-/// This enumeration has the same shape as the algebraic type of terms in the calculus of
-/// constructions.
-///
-/// There is one true exception, which is the variable (Var)[`Payload::Var`]. Along with its de
-/// Bruijn index, the variable also stores its type, which is unique, and also ensures two
-/// variables with a different type do not share the same term in memory.
-#[derive(Clone, Debug, Display, Eq, PartialEq, Hash)]
-pub enum Payload<'arena> {
-    /// A variable, with its de Bruijn index and its type
-    #[display(fmt = "{}", _0)]
-    Var(DeBruijnIndex, Term<'arena>),
-
-    /// The type of propositions
-    #[display(fmt = "Prop")]
-    Prop,
-
-    /// Type i, as described in [`UniverseLevel`]
-    #[display(fmt = "Type {}", _0)]
-    Type(UniverseLevel),
-
-    /// The application of two terms
-    #[display(fmt = "{} {}", _0, _1)]
-    App(Term<'arena>, Term<'arena>),
-
-    /// The lambda-abstraction of a term: the argument type is on the left, the body on the right.
-    #[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
-    Abs(Term<'arena>, Term<'arena>),
-
-    /// The dependant product of the term on the right over all elements of the type on the left.
-    #[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
-    Prod(Term<'arena>, Term<'arena>),
-}
-
-/// This function is the main function that the kernel exports. Most importantly, it is the only
-/// one to provide an entry point for Arena objects, by means of a closure provided by the end
-/// user.
-///
-/// Such an interface is the most elegant way to ensure the one-to-one correspondence between
-/// lifetime parameters and [`Arena`] objects.
-///
-/// To generate the `alloc` object in this function is necessary, as this is the main way to
-/// "create" a lifetime variable which makes sense. That way, `'arena` is valid exactly during
-/// the execution of the function `f`.
-pub fn use_arena<F, T>(f: F) -> T
-where
-    F: for<'arena> FnOnce(&mut Arena<'arena>) -> T,
-{
-    let alloc = Bump::new();
-    let mut arena = Arena::new(&alloc);
-    f(&mut arena)
-}
-
-use Payload::*;
-
-impl<'arena> Arena<'arena> {
-    /// Allocates a new memory arena. As detailed in the [`use_arena`] function, it is necessary to
-    /// externalise the generation of the [`bumpalo::Bump`] object.
-    fn new(alloc: &'arena Bump) -> Self {
-        Arena {
-            alloc,
-            _phantom: PhantomData,
-
-            hashcons: HashSet::new(),
-            named_terms: HashMap::new(),
-
-            mem_subst: HashMap::new(),
-        }
-    }
-
-    /// Stores a string in the arena.
-    ///
-    /// This is typically done to ensure strings live long enough when manipulating them.
-    pub(crate) fn store_name(&mut self, name: &str) -> &'arena str {
-        self.alloc.alloc_str(name)
-    }
-
-    /// Binds a term to a certain name.
-    pub fn bind(&mut self, name: &str, t: Term<'arena>) {
-        let name = self.store_name(name);
-        self.named_terms.insert(name, t);
-    }
-
-    /// Retrieves the binding of a certain name, if one exists.
-    pub fn get_binding(&self, name: &str) -> Option<Term<'arena>> {
-        self.named_terms.get(name).copied()
-    }
-
-    /// This function is the base low-level function for creating terms.
-    ///
-    /// It enforces the uniqueness property of terms in the arena.
-    fn hashcons(&mut self, n: Payload<'arena>) -> Term<'arena> {
-        // There are concurrent designs here. hashcons could also take a node, which gives
-        // subsequent function some liberty in providing the other objects of the header: WHNF,
-        // type_ (unlikely, because not always desirable), is_certainly_closed.
-        let new_node = Node {
-            payload: n,
-            head_normal_form: OnceCell::new(),
-            type_: OnceCell::new(),
-        };
-
-        match self.hashcons.get(&new_node) {
-            Some(addr) => Term(addr, PhantomData),
-            None => {
-                let addr = self.alloc.alloc(new_node);
-                self.hashcons.insert(addr);
-                Term(addr, PhantomData)
-            },
-        }
-    }
-
-    /// Returns a variable term with the given index and type
-    pub(crate) fn var(&mut self, index: DeBruijnIndex, type_: Term<'arena>) -> Term<'arena> {
-        self.hashcons(Var(index, type_))
-    }
-
-    /// Returns the term corresponding to a proposition
-    pub(crate) fn prop(&mut self) -> Term<'arena> {
-        self.hashcons(Prop)
-    }
-
-    /// Returns the term corresponding to Type(level)
-    pub(crate) fn type_(&mut self, level: UniverseLevel) -> Term<'arena> {
-        self.hashcons(Type(level))
-    }
-
-    /// Returns the term corresponding to Type(level), casting level appropriately first
-    pub(crate) fn type_usize(&mut self, level: usize) -> Term<'arena> {
-        self.hashcons(Type(BigUint::from(level).into()))
-    }
-
-    /// Returns the application of one term to the other
-    pub(crate) fn app(&mut self, func: Term<'arena>, arg: Term<'arena>) -> Term<'arena> {
-        self.hashcons(App(func, arg))
-    }
-
-    /// Returns the lambda-abstraction of the term `body`, with an argument of type `arg_type`.
-    ///
-    /// Please note that no verification is done that occurrences of this variable in `body` have
-    /// the same type.
-    pub(crate) fn abs(&mut self, arg_type: Term<'arena>, body: Term<'arena>) -> Term<'arena> {
-        self.hashcons(Abs(arg_type, body))
-    }
-
-    /// Returns the dependant product of the term `body`, over elements of `arg_type`.
-    ///
-    /// Please note that no verification is done that occurrences of this variable in `body` have
-    /// the same type.
-    pub(crate) fn prod(&mut self, arg_type: Term<'arena>, body: Term<'arena>) -> Term<'arena> {
-        self.hashcons(Prod(arg_type, body))
-    }
-
-    /// Returns the result of the substitution described by the key, lazily computing the closure `f`.
-    pub(crate) fn get_subst_or_init<F>(&mut self, key: &(Term<'arena>, Term<'arena>, usize), f: F) -> Term<'arena>
-    where
-        F: FnOnce(&mut Self) -> Term<'arena>,
-    {
-        match self.mem_subst.get(key) {
-            Some(res) => *res,
-            None => {
-                let res = f(self);
-                self.mem_subst.insert(*key, res);
-                res
-            },
-        }
-    }
-}
-
-impl<'arena> Term<'arena> {
-    /// Returns the weak head normal form of the term, lazily computing the closure `f`.
-    pub(crate) fn get_whnf_or_init<F>(self, f: F) -> Term<'arena>
-    where
-        F: FnOnce() -> Term<'arena>,
-    {
-        *self.0.head_normal_form.get_or_init(f)
-    }
-
-    /// Returns the type of the term, lazily computing the closure `f`.
-    pub(crate) fn get_type_or_try_init<F>(self, f: F) -> ResultTerm<'arena>
-    where
-        F: FnOnce() -> ResultTerm<'arena>,
-    {
-        self.0.type_.get_or_try_init(f).copied()
-    }
-}
-
-/// A Term is arguably a smart pointer, and as such, can be directly dereferenced to its associated
-/// payload.
-///
-/// This is done for convenience, as it allows to manipulate the terms relatively seamlessly.
-/// ```
-/// # use kernel::term::arena::{use_arena, Payload::*};
-/// # use kernel::term::builders::prop;
-/// # use_arena(|arena| {
-/// # let t = arena.build(prop()).unwrap();
-/// match *t {
-///     Abs(_, t2) => arena.beta_reduction(t2),
-///     App(t1, _) => t1,
-///     _ => t,
-/// }
-/// # ;})
-/// ```
-/// Please note that this trait has some limits. For instance, the notations used to match against
-/// a *pair* of terms still requires some convolution.
-impl<'arena> Deref for Term<'arena> {
-    type Target = Payload<'arena>;
-
-    fn deref(&self) -> &Self::Target {
-        &self.0.payload
-    }
-}
-
-/// Debug mode only prints the payload of a term.
-///
-/// Apart from enhancing the debug readability, this reimplementation is surprisingly necessary:
-/// because terms may refer to themselves in the payload, the default debug implementation
-/// recursively calls itself and provokes a stack overflow.
-impl<'arena> Debug for Term<'arena> {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        self.0.payload.fmt(f)
-    }
-}
-
-/// Because terms are unique in the arena, it is sufficient to compare their locations in memory to
-/// test equality.
-impl<'arena> PartialEq<Term<'arena>> for Term<'arena> {
-    fn eq(&self, x: &Term<'arena>) -> bool {
-        std::ptr::eq(self.0, x.0)
-    }
-}
-
-/// Because terms are unique in the arena, it is sufficient to compare their locations in memory to
-/// test equality. In particular, hash can also be computed from the location.
-impl<'arena> Hash for Term<'arena> {
-    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
-        std::ptr::hash(self.0, state)
-    }
-}
-
-impl<'arena> PartialEq<Node<'arena>> for Node<'arena> {
-    fn eq(&self, x: &Node<'arena>) -> bool {
-        self.payload == x.payload
-    }
-}
-
-/// Nodes are not guaranteed to be unique. Nonetheless, only the payload matters and characterises
-/// the value. Which means computing the hash for nodes can be restricted to hashing their
-/// payloads.
-impl<'arena> Hash for Node<'arena> {
-    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
-        self.payload.hash(state);
-    }
-}

kernel/src/term/mod.rs

-//! Terms in the Calculus of Construction
-//!
-//! This module provides a paradigm for building and manipulating terms of the calculus of
-//! construction, centered around the notion of [arena](`arena::Arena`).
-
-pub mod arena;
-pub mod builders;
-pub mod calculus;

kernel/tests/and.rs

-use kernel::term::arena::{use_arena, Arena};
-use kernel::term::builders::*;
+use kernel::memory::arena::{use_arena, Arena};
+use kernel::memory::term::builder::*;
 
 fn use_and_arena<F, T>(f: F) -> T
 where
@@ -36,7 +36,7 @@ fn and_true_true() {
         let hypothesis = arena.build(abs("x", var("False"), var("x"))).unwrap();
         let true_ = arena.build(var("True")).unwrap();
 
-        assert!(arena.check(hypothesis, true_).is_ok());
+        assert!(hypothesis.check(true_, arena).is_ok());
         arena.bind("hyp", hypothesis);
 
         let proof = arena
@@ -47,7 +47,7 @@ fn and_true_true() {
             ))
             .unwrap();
 
-        assert!(arena.check(proof, goal).is_ok());
+        assert!(proof.check(goal, arena).is_ok());
     })
 }
 
@@ -101,7 +101,7 @@ fn and_intro() {
             ))
             .unwrap();
 
-        assert!(arena.check(proof, goal).is_ok());
+        assert!(proof.check(goal, arena).is_ok());
     })
 }
 
@@ -154,7 +154,7 @@ fn and_elim_1() {
             ))
             .unwrap();
 
-        assert!(arena.check(proof, goal).is_ok());
+        assert!(proof.check(goal, arena).is_ok());
     })
 }
 
@@ -212,6 +212,6 @@ fn and_elim_2() {
             ))
             .unwrap();
 
-        assert!(arena.check(proof, goal).is_ok());
+        assert!(proof.check(goal, arena).is_ok());
     })
 }