.gitlab-ci.yml

@@ -28,8 +28,10 @@ format:
 
 lint:
   stage: check
+  variables:
+    RUSTFLAGS: ""
   script:
-    - cargo clippy --all-targets --all-features
+    - cargo clippy --all-targets --all-features --no-deps
 
 build:
   stage: build

.rustfmt.toml

@@ -9,6 +9,7 @@ reorder_impl_items = true
 wrap_comments = true
 
 # Set the width of lines
+chain_width = 90
 comment_width = 132
 max_width = 132
 use_small_heuristics = "Max"

Cargo.lock

@@ -319,7 +319,6 @@ dependencies = [
  "bumpalo",
  "derive_more",
  "im-rc",
- "lazy_static",
 ]
 
 [[package]]

Cargo.toml

@@ -6,17 +6,8 @@ members = [
 ]
 
 [workspace.dependencies]
-atty = "0.2"
-bumpalo = "3.11.1"
 clap = { version = "4.0.10", features = ["derive"] }
-colored = "2"
 derive_more = "0.99.17"
-im-rc = "15.1.0"
-path-absolutize = "3.0.14"
-pest = "2.5"
-pest_derive = "2.5"
-rustyline = "10.0.0"
-rustyline-derive = "0.7.0"
 
 [workspace.package]
 authors = [
@@ -25,7 +16,7 @@ authors = [
     "Vincent Lafeychine",
     "Lucas Tabary-Maujean"
 ]
-description = "A simple proof assistant written in Rust"
 edition = "2021"
-license = "GPL-3.0-or-later"
 version = "0.1.0"
+license = "GPL-3.0-or-later"
+repository = "https://gitlab.crans.org/loutr/proost"

flake.lock

@@ -10,11 +10,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1667210711,
-        "narHash": "sha256-IoErjXZAkzYWHEpQqwu/DeRNJGFdR7X2OGbkhMqMrpw=",
+        "lastModified": 1671489820,
+        "narHash": "sha256-qoei5HDJ8psd1YUPD7DhbHdhLIT9L2nadscp4Qk37uk=",
         "owner": "numtide",
         "repo": "devshell",
-        "rev": "96a9dd12b8a447840cc246e17a47b81a4268bba7",
+        "rev": "5aa3a8039c68b4bf869327446590f4cdf90bb634",
         "type": "github"
       },
       "original": {
@@ -40,11 +40,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1669542132,
-        "narHash": "sha256-DRlg++NJAwPh8io3ExBJdNW7Djs3plVI5jgYQ+iXAZQ=",
+        "lastModified": 1671722432,
+        "narHash": "sha256-ojcZUekIQeOZkHHzR81st7qxX99dB1Eaaq6PU5MNeKc=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "a115bb9bd56831941be3776c8a94005867f316a7",
+        "rev": "652e92b8064949a11bc193b90b74cb727f2a1405",
         "type": "github"
       },
       "original": {
@@ -71,11 +71,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1669775522,
-        "narHash": "sha256-6xxGArBqssX38DdHpDoPcPvB/e79uXyQBwpBcaO/BwY=",
+        "lastModified": 1672062046,
+        "narHash": "sha256-4qEJkmwnAseKSloDdCIcgYFDUxKQgkq8kbMKYmkF2VA=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "3158e47f6b85a288d12948aeb9a048e0ed4434d6",
+        "rev": "33d196f944676bdbd1965f5bf436b8b8d4ea4e5f",
         "type": "github"
       },
       "original": {

kernel/Cargo.toml

 [package]
 name = "kernel"
-edition.workspace = true
-version.workspace = true 
+
 authors.workspace = true
+edition.workspace = true
 license.workspace = true
+repository.workspace = true
+version.workspace = true
 
 [dependencies]
-bumpalo.workspace = true
 derive_more.workspace = true
-im-rc.workspace = true
 
-[dev-dependencies]
-lazy_static = "1.4.0"
+bumpalo = "3.11.1"
+im-rc = "15.1.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};
+use crate::memory::level::Level;
+use crate::memory::level::Payload::{IMax, Max, Succ, Var, Zero};
 
 /// State during computation for level comparison.
 enum State {
@@ -19,8 +18,8 @@ enum State {
 
 impl State {
     /// Checks if the comparison succeeded.
-    fn is_true(&self) -> bool {
-        matches!(self, State::True)
+    const fn is_true(&self) -> bool {
+        matches!(*self, Self::True)
     }
 }
 
@@ -58,23 +57,23 @@ impl<'arena> Level<'arena> {
     /// - `False` else.
     fn geq_no_subst(self, rhs: Self, n: i64) -> State {
         match (&*self, &*rhs) {
-            (Zero, _) if n >= 0 => State::True,
+            (&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,
+            (&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() =>
+            (_, &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() => {
+            (&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),
+            (_, &IMax(_, v)) | (&IMax(_, v), _) if let Var(i) = *v => State::Stuck(i),
 
             _ => State::False,
         }
@@ -84,6 +83,7 @@ impl<'arena> Level<'arena> {
     ///
     /// 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))`.
+    #[inline]
     pub fn geq(self, rhs: Self, n: i64, arena: &mut Arena<'arena>) -> bool {
         match self.geq_no_subst(rhs, n) {
             State::True => true,
@@ -91,7 +91,8 @@ impl<'arena> Level<'arena> {
             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, 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)
             },
         }
@@ -100,6 +101,7 @@ impl<'arena> Level<'arena> {
     /// Checks whether `self = rhs`.
     ///
     /// This is a "conversion" equality test, not the equality function used by [`PartialEq`].
+    #[inline]
     pub fn is_eq(self, rhs: Self, arena: &mut Arena<'arena>) -> bool {
         self.geq(rhs, 0, arena) && rhs.geq(self, 0, arena)
     }
@@ -146,7 +148,7 @@ mod tests {
             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)
-            )
+            );
         });
     }
 
@@ -162,8 +164,8 @@ mod tests {
             assert_eq!(
                 lvl.substitute(&subst, arena),
                 arena.build_level_raw(imax(zero(), max(succ(zero()), max(succ(zero()), zero()))))
-            )
-        })
+            );
+        });
     }
     #[test]
     fn single_subst() {
@@ -172,7 +174,7 @@ mod tests {
             assert_eq!(
                 lvl.substitute_single(0, Level::zero(arena), arena),
                 arena.build_level_raw(imax(max(succ(zero()), zero()), zero()))
-            )
-        })
+            );
+        });
     }
 }

kernel/src/calculus/term.rs

@@ -3,20 +3,22 @@
 //! This module consists of internal utility functions used by the type checker, and correspond to
 //! usual functions over lambda-terms. These functions interact appropriately with a given arena.
 
-use Payload::*;
-
 use crate::memory::arena::Arena;
 use crate::memory::declaration::InstantiatedDeclaration;
 use crate::memory::level::Level;
-use crate::memory::term::{Payload, Term};
+use crate::memory::term::Payload::{Abs, App, Decl, Prod, Sort, Var};
+use crate::memory::term::Term;
 
 impl<'arena> Term<'arena> {
     /// Apply one step of β-reduction, using the leftmost-outermost evaluation strategy.
+    #[inline]
+    #[must_use]
     pub fn beta_reduction(self, arena: &mut Arena<'arena>) -> Self {
         match *self {
-            App(t1, t2) => match *t1 {
-                Abs(_, t1) => t1.substitute(t2, 1, arena),
-                _ => {
+            App(t1, t2) => {
+                if let Abs(_, t1) = *t1 {
+                    t1.substitute(t2, 1, arena)
+                } else {
                     let t1_new = t1.beta_reduction(arena);
                     if t1_new == t1 {
                         let t2_new = t2.beta_reduction(arena);
@@ -24,7 +26,7 @@ impl<'arena> Term<'arena> {
                     } else {
                         t1_new.app(t2, arena)
                     }
-                },
+                }
             },
             Abs(arg_type, body) => {
                 let body = body.beta_reduction(arena);
@@ -137,6 +139,8 @@ impl<'arena> Term<'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.
+    #[inline]
+    #[must_use]
     pub fn normal_form(self, arena: &mut Arena<'arena>) -> Self {
         let mut temp = self;
         let mut res = self.beta_reduction(arena);
@@ -149,6 +153,8 @@ impl<'arena> Term<'arena> {
     }
 
     /// Returns the weak-head normal form of a term.
+    #[inline]
+    #[must_use]
     pub fn whnf(self, arena: &mut Arena<'arena>) -> Self {
         self.get_whnf_or_init(|| match *self {
             App(t1, t2) => match *t1.whnf(arena) {
@@ -182,7 +188,7 @@ mod tests {
             let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
 
             assert_eq!(term.beta_reduction(arena), reduced);
-        })
+        });
     }
 
     #[test]
@@ -308,7 +314,7 @@ mod tests {
             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]
@@ -325,7 +331,7 @@ mod tests {
             let reduced = arena.build_term_raw(prop());
 
             assert_eq!(decl.beta_reduction(arena), reduced);
-        })
+        });
     }
 
     #[test]
@@ -335,8 +341,8 @@ mod tests {
             let term = arena.build_term_raw(app(abs(prop(), reduced), prop()));
 
             let reduced = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
-            assert_eq!(term.beta_reduction(arena), reduced)
-        })
+            assert_eq!(term.beta_reduction(arena), reduced);
+        });
     }
 
     #[test]
@@ -346,7 +352,7 @@ mod tests {
             let reduced = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
 
             assert_eq!(term.beta_reduction(arena), reduced);
-        })
+        });
     }
 
     #[test]
@@ -359,7 +365,7 @@ mod tests {
             let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
 
             assert_eq!(term.beta_reduction(arena), reduced);
-        })
+        });
     }
 
     #[test]
@@ -372,7 +378,7 @@ mod tests {
             let normal_form = arena.build_term_raw(prop());
 
             assert_eq!(term.normal_form(arena), normal_form);
-        })
+        });
     }
 
     #[test]
@@ -407,6 +413,6 @@ mod tests {
             ));
 
             assert_eq!(term.substitute_univs(&[arena.build_level_raw(zero()), arena.build_level_raw(zero())], arena), term);
-        })
+        });
     }
 }

kernel/src/error.rs

@@ -2,14 +2,14 @@
 
 use derive_more::{Display, From};
 
-use crate::memory::*;
+use crate::memory::{declaration, level, term};
 use crate::type_checker::TypeCheckerError;
 
 /// Type representing kernel errors.
 #[derive(Clone, Debug, Display, Eq, PartialEq)]
 pub struct Error<'arena> {
     /// The kind of form error that occurred.
-    pub kind: ErrorKind<'arena>,
+    pub kind: Kind<'arena>,
     // This struct might contains more fields in the future (waiting for #15)
 }
 
@@ -17,7 +17,7 @@ pub struct Error<'arena> {
 /// the errors are respectively defined.
 #[non_exhaustive]
 #[derive(Clone, Debug, Display, Eq, PartialEq, From)]
-pub enum ErrorKind<'arena> {
+pub enum Kind<'arena> {
     TypeChecker(TypeCheckerError<'arena>),
     Term(term::builder::TermError<'arena>),
     Level(level::builder::LevelError<'arena>),
@@ -26,7 +26,7 @@ pub enum ErrorKind<'arena> {
 
 impl<'arena> std::error::Error for Error<'arena> {}
 
-pub type Result<'arena, T> = std::result::Result<T, Error<'arena>>;
+pub type Result<'arena, T> = core::result::Result<T, Error<'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>>;

kernel/src/lib.rs

@@ -10,6 +10,52 @@
 #![feature(once_cell)]
 #![feature(trait_alias)]
 #![feature(if_let_guard)]
+#![deny(
+    clippy::complexity,
+    clippy::correctness,
+    clippy::nursery,
+    clippy::pedantic,
+    clippy::perf,
+    clippy::restriction,
+    clippy::style,
+    clippy::suspicious
+)]
+#![allow(
+    clippy::blanket_clippy_restriction_lints,
+    clippy::else_if_without_else,
+    clippy::exhaustive_enums,
+    clippy::exhaustive_structs,
+    clippy::implicit_return,
+    clippy::match_same_arms,
+    clippy::match_wildcard_for_single_variants,
+    clippy::missing_trait_methods,
+    clippy::mod_module_files,
+    clippy::panic_in_result_fn,
+    clippy::pattern_type_mismatch,
+    clippy::separated_literal_suffix,
+    clippy::shadow_reuse,
+    clippy::shadow_unrelated,
+    clippy::unreachable,
+    clippy::wildcard_enum_match_arm
+)]
+#![warn(
+    clippy::arithmetic_side_effects,
+    clippy::integer_arithmetic,
+    clippy::missing_errors_doc,
+    clippy::missing_docs_in_private_items
+)]
+#![cfg_attr(
+    test,
+    allow(
+        clippy::assertions_on_result_states,
+        clippy::enum_glob_use,
+        clippy::indexing_slicing,
+        clippy::non_ascii_literal,
+        clippy::too_many_lines,
+        clippy::unwrap_used,
+        clippy::wildcard_imports,
+    )
+)]
 
 pub mod calculus;
 pub mod error;

kernel/src/location.rs

@@ -6,7 +6,7 @@ use derive_more::{Constructor, Display, From};
 
 /// Line and column position.
 #[derive(Clone, Constructor, Debug, Default, Display, Eq, PartialEq, From, Ord, PartialOrd)]
-#[display(fmt = "{}:{}", line, column)]
+#[display(fmt = "{line}:{column}")]
 pub struct Position {
     pub line: usize,
     pub column: usize,
@@ -14,7 +14,7 @@ pub struct Position {
 
 /// Span of position.
 #[derive(Clone, Constructor, Debug, Default, Display, Eq, PartialEq, From, Ord, PartialOrd)]
-#[display(fmt = "{}-{}", start, end)]
+#[display(fmt = "{start}-{end}")]
 pub struct Location {
     #[from(forward)]
     pub start: Position,

kernel/src/memory/arena.rs

@@ -2,8 +2,8 @@
 //!
 //! This module defines the core functions used to manipulate an arena and its dwellers.
 
+use core::marker::PhantomData;
 use std::collections::{HashMap, HashSet};
-use std::marker::PhantomData;
 
 use bumpalo::Bump;
 
@@ -63,6 +63,8 @@ pub struct Arena<'arena> {
 /// 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`.
+#[allow(clippy::module_name_repetitions)]
+#[inline]
 pub fn use_arena<F, T>(f: F) -> T
 where
     F: for<'arena> FnOnce(&mut Arena<'arena>) -> T,
@@ -107,23 +109,29 @@ impl<'arena> Arena<'arena> {
     }
 
     /// Binds a term to a given name.
+    #[inline]
     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.
+    #[inline]
     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.
+    #[inline]
+    #[must_use]
     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.
+    #[inline]
+    #[must_use]
     pub fn get_binding_decl(&self, name: &str) -> Option<Declaration<'arena>> {
         self.named_decls.get(name).copied()
     }
@@ -147,7 +155,7 @@ 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 struct $dweller<'arena>(&'arena Node<'arena>, core::marker::PhantomData<*mut &'arena ()>);
 
         pub(super) struct Node<'arena> {
             header: $header<'arena>,
@@ -155,8 +163,8 @@ accelerating specific algorithms.")]
         }
 
         impl<'arena> $dweller<'arena> {
-            fn new(node: &'arena Node<'arena>) -> Self {
-                $dweller(node, std::marker::PhantomData)
+            const fn new(node: &'arena Node<'arena>) -> Self {
+                $dweller(node, core::marker::PhantomData)
             }
         }
 
@@ -183,9 +191,10 @@ match *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> {
+        impl<'arena> core::ops::Deref for $dweller<'arena> {
             type Target = $payload<'arena>;
 
+            #[inline]
             fn deref(&self) -> &Self::Target {
                 &self.0.payload
             }
@@ -196,8 +205,9 @@ a *pair* of", stringify!($dweller), "s still requires some convolution.")]
 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 {
+        impl<'arena> core::fmt::Debug for $dweller<'arena> {
+            #[inline]
+            fn fmt(&self, f: &mut core::fmt::Formatter) -> core::fmt::Result {
                 self.0.payload.fmt(f)
             }
         }
@@ -205,8 +215,9 @@ default debug implementation recursively calls itself until the stack overflows.
         #[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> {
+            #[inline]
             fn eq(&self, rhs: &Self) -> bool {
-                std::ptr::eq(self.0, rhs.0)
+                core::ptr::eq(self.0, rhs.0)
             }
         }
 
@@ -215,9 +226,10 @@ sufficient to compare their locations in memory to test equality.")]
         #[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> core::hash::Hash for $dweller<'arena> {
+            #[inline]
+            fn hash<H: core::hash::Hasher>(&self, state: &mut H) {
+                core::ptr::hash(self.0, state)
             }
         }
 
@@ -232,8 +244,8 @@ also be computed from the location")]
         /// 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) {
+        impl<'arena> core::hash::Hash for Node<'arena> {
+            fn hash<H: core::hash::Hasher>(&self, state: &mut H) {
                 self.payload.hash(state);
             }
         }

kernel/src/memory/declaration/builder.rs

@@ -31,6 +31,7 @@ pub enum DeclarationError<'arena> {
 /// 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).
+#[allow(clippy::module_name_repetitions)]
 pub trait BuilderTrait<'build> = for<'arena> FnOnce(&mut Arena<'arena>) -> ResultDecl<'arena>;
 
 pub trait InstantiatedBuilderTrait<'build> =
@@ -56,6 +57,7 @@ impl<'arena> Arena<'arena> {
 }
 
 /// Returns a builder creating `term`, where universe variables are described by `vars`.
+#[inline]
 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();
@@ -72,6 +74,7 @@ pub enum Builder<'build> {
 impl<'build> Builder<'build> {
     /// Realise a builder into a [`Declaration`]. This internally uses functions described in
     /// the [builder](`crate::memory::declaration::builder`) module.
+    #[inline]
     pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultDecl<'arena> {
         arena.build_declaration(self.partial_application())
     }
@@ -81,8 +84,8 @@ impl<'build> Builder<'build> {
     }
 
     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),
+        match *self {
+            Builder::Decl(ref term, ref vars) => declaration(term.partial_application(), vars.as_slice())(arena),
         }
     }
 }
@@ -93,7 +96,10 @@ fn try_build_instance<'arena, '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<_>>>()?;
+    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))
@@ -110,6 +116,7 @@ fn try_build_instance<'arena, 'build>(
 /// 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.
+#[inline]
 pub fn instance<'build, F: BuilderTrait<'build>>(
     decl: F,
     levels: &'build [level::Builder<'build>],
@@ -119,6 +126,8 @@ pub fn instance<'build, F: BuilderTrait<'build>>(
 
 /// Returns a builder creating the declaration bound by `name`, instantiated with the universe
 /// levels `levels`.
+#[inline]
+#[must_use]
 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 {
@@ -136,6 +145,7 @@ pub fn var<'build>(name: &'build str, levels: &'build [level::Builder<'build>])
 ///
 /// 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.
+#[allow(clippy::module_name_repetitions)]
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum InstantiatedBuilder<'build> {
     Instance(Box<Builder<'build>>, Vec<level::Builder<'build>>),
@@ -143,16 +153,16 @@ pub enum InstantiatedBuilder<'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) => {
+impl<'arena> core::fmt::Display for InstantiatedBuilder<'arena> {
+    #[inline]
+    fn fmt(&self, f: &mut core::fmt::Formatter) -> core::fmt::Result {
+        match *self {
+            InstantiatedBuilder::Instance(ref decl, ref params) => {
                 write!(f, "{decl}.{{")?;
                 params.iter().try_for_each(|level| write!(f, "{level}, "))?;
                 write!(f, "}}")
             },
-            Var(decl, params) => {
+            InstantiatedBuilder::Var(decl, ref params) => {
                 write!(f, "{decl}.{{")?;
                 params.iter().try_for_each(|level| write!(f, "{level}, "))?;
                 write!(f, "}}")
@@ -163,6 +173,7 @@ impl<'arena> std::fmt::Display for InstantiatedBuilder<'arena> {
 impl<'build> InstantiatedBuilder<'build> {
     /// Realise a builder into an [`InstantiatedDeclaration`]. This internally uses functions described in
     /// the [builder](`crate::memory::declaration::builder`) module.
+    #[inline]
     pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultInstantiatedDecl<'arena> {
         arena.build_instantiated_declaration(self.partial_application())
     }
@@ -176,10 +187,9 @@ impl<'build> InstantiatedBuilder<'build> {
         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),
+        match *self {
+            InstantiatedBuilder::Instance(ref decl, ref levels) => instance(decl.partial_application(), levels)(arena, lvl_env),
+            InstantiatedBuilder::Var(name, ref levels) => var(name, levels)(arena, lvl_env),
         }
     }
 }

kernel/src/memory/declaration/mod.rs

 //! universe-polymorphic declarations.
 
+use core::fmt;
 use std::cell::OnceCell;
-use std::fmt;
 
 use derive_more::Display;
 
@@ -29,10 +29,10 @@ super::arena::new_dweller!(InstantiatedDeclaration, Header, Payload);
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Payload<'arena> {
     /// The declaration being instantiated
-    pub decl: Declaration<'arena>,
+    pub(crate) decl: Declaration<'arena>,
 
     /// The parameters used to instantiate it
-    pub params: &'arena [Level<'arena>],
+    pub(crate) params: &'arena [Level<'arena>],
 }
 
 struct Header<'arena> {
@@ -41,25 +41,25 @@ struct Header<'arena> {
 }
 
 impl<'arena> fmt::Display for InstantiatedDeclaration<'arena> {
+    #[inline]
     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)?;
+        if let Some(term) = self.0.header.term.get() {
+            write!(f, "{term}")
+        } else {
+            write!(f, "({}).{{", self.0.payload.decl)?;
 
-                let mut iter = self.0.payload.params.iter();
+            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}"))?;
+            iter.next().map_or(Ok(()), |level| write!(f, "{level}"))?;
+            iter.try_for_each(|level| write!(f, ", {level}"))?;
 
-                write!(f, "}}")
-            },
+            write!(f, "}}")
         }
     }
 }
 
 impl<'arena> Declaration<'arena> {
-    pub(crate) fn new(term: Term<'arena>, vars: usize) -> Self {
+    pub(crate) const fn new(term: Term<'arena>, vars: usize) -> Self {
         Self(term, vars)
     }
 }
@@ -78,19 +78,23 @@ impl<'arena> InstantiatedDeclaration<'arena> {
             },
         };
 
-        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)
-            },
+        if let Some(addr) = arena.hashcons_decls.get(&new_node) {
+            Self::new(addr)
+        } else {
+            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.
+    #[inline]
     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))
+        *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
@@ -100,6 +104,7 @@ impl<'arena> InstantiatedDeclaration<'arena> {
         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))
+        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

@@ -23,7 +23,7 @@ use crate::memory::arena::Arena;
 #[non_exhaustive]
 #[derive(Clone, Debug, Display, Eq, PartialEq)]
 pub enum LevelError<'arena> {
-    #[display(fmt = "unknown universe variable {}", _0)]
+    #[display(fmt = "unknown universe variable {_0}")]
     VarNotFound(&'arena str),
 }
 
@@ -35,6 +35,7 @@ pub type Environment<'build> = HashMap<&'build str, usize>;
 ///
 /// A call with a couple of arguments `(arena, env)` of a closure with this trait should
 /// build a definite level in the [`Arena`] `arena`.
+#[allow(clippy::module_name_repetitions)]
 pub trait BuilderTrait<'build> = for<'arena> FnOnce(&mut Arena<'arena>, &Environment<'build>) -> ResultLevel<'arena>;
 
 impl<'arena> Arena<'arena> {
@@ -47,6 +48,7 @@ impl<'arena> Arena<'arena> {
 
 /// Returns a closure building a universe variable associated to `name`
 #[inline]
+#[must_use]
 pub const fn var(name: &str) -> impl BuilderTrait<'_> {
     move |arena, env| {
         env.get(name).map(|lvl| Level::var(*lvl, arena)).ok_or(Error {
@@ -57,12 +59,14 @@ pub const fn var(name: &str) -> impl BuilderTrait<'_> {
 
 /// Returns a closure building the 0 level.
 #[inline]
+#[must_use]
 pub const fn zero<'build>() -> impl BuilderTrait<'build> {
     |arena, _| Ok(Level::zero(arena))
 }
 
 /// Returns a closure building a constant level.
 #[inline]
+#[must_use]
 pub const fn const_<'build>(n: usize) -> impl BuilderTrait<'build> {
     move |arena, _| Ok(Level::from(n, arena))
 }
@@ -128,6 +132,7 @@ pub enum Builder<'builder> {
 impl<'build> Builder<'build> {
     /// Realise a builder into a [`Level`]. This internally uses functions described in
     /// the [builder](`crate::memory::level::builder`) module.
+    #[inline]
     pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultLevel<'arena> {
         arena.build_level(self.partial_application())
     }
@@ -141,15 +146,14 @@ impl<'build> Builder<'build> {
         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),
+            Builder::Zero => zero()(arena, env),
+            Builder::Const(c) => const_(c)(arena, env),
+            Builder::Plus(ref u, n) => plus(u.partial_application(), n)(arena, env),
+            Builder::Succ(ref l) => succ(l.partial_application())(arena, env),
+            Builder::Max(ref l, ref r) => max(l.partial_application(), r.partial_application())(arena, env),
+            Builder::IMax(ref l, ref r) => imax(l.partial_application(), r.partial_application())(arena, env),
+            Builder::Var(s) => var(s)(arena, env),
         }
     }
 }

kernel/src/memory/level/mod.rs

 //! Universe levels.
 
+use core::fmt::{Display, Formatter};
+use core::hash::Hash;
 use std::cell::OnceCell;
-use std::fmt::{Display, Formatter};
-use std::hash::Hash;
 
 use super::arena::Arena;
 
@@ -40,7 +40,8 @@ pub enum Payload<'arena> {
 }
 
 impl Display for Level<'_> {
-    fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
+    #[inline]
+    fn fmt(&self, f: &mut Formatter) -> core::fmt::Result {
         match self.to_numeral() {
             Some(n) => write!(f, "{n}"),
             None => match **self {
@@ -57,7 +58,7 @@ impl Display for Level<'_> {
     }
 }
 
-use Payload::*;
+use Payload::{IMax, Max, Succ, Var, Zero};
 
 impl<'arena> Level<'arena> {
     /// This function is the base low-level function for creating levels.
@@ -72,23 +73,22 @@ impl<'arena> Level<'arena> {
             },
         };
 
-        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);
+        if let Some(level) = arena.hashcons_levels.get(&new_node) {
+            *level
+        } else {
+            // 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);
+            // 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);
+            // supersede the previous correspondence
+            arena.hashcons_levels.insert(node_unreduced, reduced);
+            arena.hashcons_levels.insert(reduced.0, reduced);
 
-                reduced
-            },
+            reduced
         }
     }
 
@@ -118,6 +118,8 @@ impl<'arena> Level<'arena> {
     }
 
     /// The addition of a level and an integer
+    #[inline]
+    #[must_use]
     pub fn add(self, n: usize, arena: &mut Arena<'arena>) -> Self {
         if n == 0 {
             self
@@ -128,17 +130,23 @@ impl<'arena> Level<'arena> {
     }
 
     /// Builds a level from an integer
+    #[inline]
+    #[must_use]
     pub fn from(n: usize, arena: &mut Arena<'arena>) -> Self {
         Level::zero(arena).add(n, arena)
     }
 
     /// Converts a level to an integer, if possible
+    #[inline]
+    #[must_use]
     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`
+    #[inline]
+    #[must_use]
     pub fn plus(self) -> (Self, usize) {
         *self.0.header.plus_form.get_or_init(|| match *self {
             Succ(u) => {
@@ -166,11 +174,11 @@ impl<'arena> Level<'arena> {
                 if u == v {
                     u
                 } else {
-                    match &*v {
+                    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),
+                        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,
                     }
                 }
@@ -206,15 +214,15 @@ mod pretty_printing {
             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))
-        })
+            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]
@@ -223,8 +231,8 @@ mod pretty_printing {
             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]
@@ -232,7 +240,7 @@ mod pretty_printing {
         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)))")
-        })
+            assert_eq!(format!("{lvl}"), "max (imax (0) (u0)) (max (imax (0) (u0)) (imax (1) (u0)))");
+        });
     }
 }

kernel/src/memory/term/builder.rs

@@ -25,7 +25,7 @@ use crate::memory::level::builder as level;
 #[non_exhaustive]
 #[derive(Clone, Debug, Display, Eq, PartialEq)]
 pub enum TermError<'arena> {
-    #[display(fmt = "unknown identifier {}", _0)]
+    #[display(fmt = "unknown identifier {_0}")]
     ConstNotFound(&'arena str),
 }
 
@@ -42,6 +42,7 @@ pub type Environment<'build, 'arena> = ImHashMap<&'build str, (DeBruijnIndex, Te
 /// 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.
+#[allow(clippy::module_name_repetitions)]
 pub trait BuilderTrait<'build> = for<'arena> FnOnce(
     &mut Arena<'arena>,
     &Environment<'build, 'arena>,
@@ -59,6 +60,7 @@ impl<'arena> Arena<'arena> {
 
 /// Returns a closure building a variable associated to the name `name`
 #[inline]
+#[must_use]
 pub const fn var(name: &str) -> impl BuilderTrait<'_> {
     move |arena, env, _, depth| {
         env.get(name)
@@ -77,6 +79,7 @@ pub const fn var(name: &str) -> impl BuilderTrait<'_> {
 
 /// Returns a closure building the Prop term.
 #[inline]
+#[must_use]
 pub const fn prop<'build>() -> impl BuilderTrait<'build> {
     |arena, _, _, _| Ok(Term::prop(arena))
 }
@@ -90,6 +93,7 @@ pub const fn type_<'build, F: level::BuilderTrait<'build>>(level: F) -> impl Bui
 
 /// Returns a closure building the Type `level` term (indirection from `usize`).
 #[inline]
+#[must_use]
 pub const fn type_usize<'build>(level: usize) -> impl BuilderTrait<'build> {
     move |arena, _, _, _| Ok(Term::type_usize(level, arena))
 }
@@ -103,6 +107,7 @@ pub const fn sort<'build, F: level::BuilderTrait<'build>>(level: F) -> impl Buil
 
 /// Returns a closure building the Sort `level` term (indirection from `usize`).
 #[inline]
+#[must_use]
 pub const fn sort_usize<'build>(level: usize) -> impl BuilderTrait<'build> {
     move |arena, _, _, _| Ok(Term::sort_usize(level, arena))
 }
@@ -196,6 +201,7 @@ pub enum Builder<'build> {
 impl<'build> Builder<'build> {
     /// Realise a builder into a [`Term`]. This internally uses functions described in
     /// the [builder](`crate::memory::term::builder`) module.
+    #[inline]
     pub fn realise<'arena>(&self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
         arena.build(self.partial_application())
     }
@@ -211,18 +217,19 @@ impl<'build> Builder<'build> {
         lvl_env: &level::Environment<'build>,
         depth: DeBruijnIndex,
     ) -> ResultTerm<'arena> {
-        use Builder::*;
-        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) => {
+        match *self {
+            Builder::Var(s) => var(s)(arena, env, lvl_env, depth),
+            Builder::Prop => prop()(arena, env, lvl_env, depth),
+            Builder::Type(ref level) => type_(level.partial_application())(arena, env, lvl_env, depth),
+            Builder::Sort(ref level) => sort(level.partial_application())(arena, env, lvl_env, depth),
+            Builder::App(ref l, ref r) => app(l.partial_application(), r.partial_application())(arena, env, lvl_env, depth),
+            Builder::Abs(s, ref arg, ref body) => {
+                abs(s, arg.partial_application(), body.partial_application())(arena, env, lvl_env, depth)
+            },
+            Builder::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),
+            Builder::Decl(ref decl_builder) => decl(decl_builder.partial_application())(arena, env, lvl_env, depth),
         }
     }
 }

kernel/src/memory/term/mod.rs

@@ -3,8 +3,8 @@
 //! This module defines the core functions used to create and manipulate terms.
 
 use core::fmt;
+use core::fmt::Debug;
 use std::cell::OnceCell;
-use std::fmt::Debug;
 
 use derive_more::{Add, Display, From, Into, Sub};
 
@@ -64,6 +64,7 @@ pub enum Payload<'arena> {
 }
 
 impl<'arena> fmt::Display for Payload<'arena> {
+    #[inline]
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match *self {
             Var(index, _) => write!(f, "{index}"),
@@ -84,12 +85,13 @@ impl<'arena> fmt::Display for Payload<'arena> {
 }
 
 impl<'arena> fmt::Display for Term<'arena> {
+    #[inline]
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         write!(f, "{}", self.0.payload)
     }
 }
 
-use Payload::*;
+use Payload::{Abs, App, Decl, Prod, Sort, Var};
 
 impl<'arena> Term<'arena> {
     /// This function is the base low-level function for creating terms.
@@ -107,13 +109,12 @@ impl<'arena> Term<'arena> {
             },
         };
 
-        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)
-            },
+        if let Some(addr) = arena.hashcons_terms.get(&new_node) {
+            Term::new(addr)
+        } else {
+            let addr = arena.alloc.alloc(new_node);
+            arena.hashcons_terms.insert(addr);
+            Term::new(addr)
         }
     }
 
@@ -191,13 +192,12 @@ impl<'arena> Arena<'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
-            },
+        if let Some(res) = self.mem_subst.get(key) {
+            *res
+        } else {
+            let res = f(self);
+            self.mem_subst.insert(*key, res);
+            res
         }
     }
 }
@@ -221,7 +221,7 @@ mod tests {
 
             let prop_ = crate::memory::term::Term::decl(decl_, arena);
 
-            assert_eq!(format!("{}", prop_), "(Prop).{}");
+            assert_eq!(prop_.to_string(), "(Prop).{}");
             let vart = crate::memory::term::builder::raw::var;
 
             let lvl = max(succ(var(0)), succ(var(1)));
@@ -236,7 +236,7 @@ mod tests {
                 ),
             ));
 
-            assert_eq!(format!("{}", term), "λ Sort max (u0) (u1) + 1 → λ Type → λ Type 1 → Π 1 → (1) (2)")
-        })
+            assert_eq!(term.to_string(), "λ Sort max (u0) (u1) + 1 → λ Type → λ Type 1 → Π 1 → (1) (2)");
+        });
     }
 }

kernel/src/type_checker.rs

@@ -3,18 +3,19 @@
 //! The logical core of the kernel.
 
 use derive_more::Display;
-use Payload::*;
 
 use crate::error::{Error, Result, ResultTerm};
 use crate::memory::arena::Arena;
 use crate::memory::declaration::Declaration;
-use crate::memory::term::{Payload, Term};
+use crate::memory::term::Payload::{Abs, App, Decl, Prod, Sort, Var};
+use crate::memory::term::Term;
 
 #[derive(Clone, Debug, Display, Eq, PartialEq)]
-#[display(fmt = "{}: {}", _0, _1)]
+#[display(fmt = "{_0}: {_1}")]
 pub struct TypedTerm<'arena>(Term<'arena>, Term<'arena>);
 
 /// Errors that can occur, at runtime, during type checking.
+#[allow(clippy::module_name_repetitions)]
 #[non_exhaustive]
 #[derive(Clone, Debug, Display, Eq, PartialEq)]
 pub enum TypeCheckerError<'arena> {
@@ -52,9 +53,9 @@ impl<'arena> Term<'arena> {
         }
 
         match (&*lhs, &*rhs) {
-            (Sort(l1), Sort(l2)) => l1.is_eq(*l2, arena),
+            (&Sort(l1), &Sort(l2)) => l1.is_eq(l2, arena),
 
-            (Var(i, _), Var(j, _)) => i == j,
+            (&Var(i, _), &Var(j, _)) => i == j,
 
             (&Prod(t1, u1), &Prod(t2, u2)) => t1.conversion(t2, arena) && u1.conversion(u2, arena),
 
@@ -79,6 +80,7 @@ impl<'arena> Term<'arena> {
     }
 
     /// Checks whether two terms are definitionally equal.
+    #[inline]
     pub fn is_def_eq(self, rhs: Self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
         self.conversion(rhs, arena).then_some(()).ok_or(Error {
             kind: TypeCheckerError::NotDefEq(self, rhs).into(),
@@ -104,6 +106,7 @@ impl<'arena> Term<'arena> {
     }
 
     /// Infers the type of the term `t`, living in arena `arena`.
+    #[inline]
     pub fn infer_raw(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
         match *self {
             Sort(lvl) => Ok(Term::sort(lvl.succ(arena), arena)),
@@ -158,11 +161,13 @@ impl<'arena> Term<'arena> {
     }
 
     /// Infers the type of the term `t`, living in arena `arena`, checks for memoization.
+    #[inline]
     pub fn infer(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
         self.get_type_or_try_init(|| self.infer_raw(arena))
     }
 
     /// Checks whether the term `t` living in `arena` is of type `ty`.
+    #[inline]
     pub fn check(self, ty: Self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
         let tty = self.infer(arena)?;
 
@@ -178,11 +183,13 @@ impl<'arena> Declaration<'arena> {
     /// Because it is not allowed to access the underlying term of a declaration, this function
     /// does not return anything, and only serves as a way to ensure the declaration is
     /// well-formed.
+    #[inline]
     pub fn infer(self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
         self.0.infer(arena)?;
         Ok(())
     }
 
+    #[inline]
     pub fn check(self, ty: Self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
         self.0.check(ty.0, arena)
     }
@@ -204,8 +211,8 @@ mod tests {
             let term = arena.build_term_raw(app(abs(prop(), id()), id()));
             let normal_form = arena.build_term_raw(abs(prop(), var(1.into(), prop())));
 
-            assert!(term.is_def_eq(normal_form, arena).is_ok())
-        })
+            assert!(term.is_def_eq(normal_form, arena).is_ok());
+        });
     }
 
     #[test]
@@ -224,7 +231,7 @@ mod tests {
 
             assert!(decl.is_def_eq(prop, arena).is_ok());
             assert!(prop.is_def_eq(decl, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -244,7 +251,7 @@ mod tests {
             let ty = arena.build_term_raw(type_usize(0));
 
             assert!(term.check(ty, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -253,8 +260,8 @@ mod tests {
             let term = arena.build_term_raw(app(abs(prop(), abs(prop(), var(2.into(), prop()))), id()));
             let normal_form = arena.build_term_raw(abs(prop(), id()));
 
-            assert!(term.is_def_eq(normal_form, arena).is_ok())
-        })
+            assert!(term.is_def_eq(normal_form, arena).is_ok());
+        });
     }
 
     #[test]
@@ -264,7 +271,7 @@ mod tests {
             let term = arena.build_term_raw(abs(prop(), app(app(var(2.into(), prop()), id()), id())));
 
             assert!(term.is_def_eq(term, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -279,7 +286,7 @@ mod tests {
                     kind: TypeCheckerError::NotDefEq(term_lhs, term_rhs).into()
                 })
             );
-        })
+        });
     }
 
     #[test]
@@ -294,7 +301,7 @@ mod tests {
                     kind: TypeCheckerError::NotDefEq(term_lhs, term_rhs).into()
                 })
             );
-        })
+        });
     }
 
     #[test]
@@ -309,7 +316,7 @@ mod tests {
                     kind: TypeCheckerError::NotDefEq(term_lhs, term_rhs).into()
                 })
             );
-        })
+        });
     }
 
     #[test]
@@ -323,8 +330,8 @@ mod tests {
 
             let term_type = term.infer(arena).unwrap();
             assert_eq!(term_type, type_0);
-            assert!(term.check(term_type, arena).is_ok())
-        })
+            assert!(term.check(term_type, arena).is_ok());
+        });
     }
 
     #[test]
@@ -404,8 +411,8 @@ mod tests {
             let term_type = term.infer(arena).unwrap();
             let expected_type = arena.build(prod("_", prop(), prod("_", prop(), prop()))).unwrap();
             assert_eq!(term_type, expected_type);
-            assert!(term.check(term_type, arena).is_ok())
-        })
+            assert!(term.check(term_type, arena).is_ok());
+        });
     }
 
     #[test]
@@ -420,8 +427,8 @@ mod tests {
 
             let term_type = term.infer(arena).unwrap();
             assert_eq!(term_type, type_1);
-            assert!(term.check(term_type, arena).is_ok())
-        })
+            assert!(term.check(term_type, arena).is_ok());
+        });
     }
 
     #[test]
@@ -432,8 +439,8 @@ mod tests {
             let term_type = term.infer(arena).unwrap();
             let expected_type = arena.build_term_raw(prod(prop(), type_usize(1)));
             assert_eq!(term_type, expected_type);
-            assert!(term.check(term_type, arena).is_ok())
-        })
+            assert!(term.check(term_type, arena).is_ok());
+        });
     }
 
     #[test]
@@ -452,8 +459,8 @@ mod tests {
             // λx.x x
             let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
 
-            assert!(term.is_def_eq(reduced, arena).is_ok())
-        })
+            assert!(term.is_def_eq(reduced, arena).is_ok());
+        });
     }
 
     #[test]
@@ -464,8 +471,8 @@ mod tests {
             let term_type = term.infer(arena).unwrap();
 
             assert_eq!(term_type, type_0);
-            assert!(term.check(term_type, arena).is_ok())
-        })
+            assert!(term.check(term_type, arena).is_ok());
+        });
     }
 
     #[test]
@@ -476,7 +483,7 @@ mod tests {
 
             assert_eq!(term_type, Term::prop(arena));
             assert!(term.check(term_type, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -488,7 +495,7 @@ mod tests {
 
             assert_eq!(term_type, expected_type);
             assert!(term.check(term_type, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -503,7 +510,7 @@ mod tests {
 
             assert_eq!(identity_type, expected_type);
             assert!(identity.check(identity_type, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -526,7 +533,7 @@ mod tests {
                 arena.build_term_raw(prod(prop(), prod(prop(), prod(prod(prop(), prod(prop(), prop())), prop()))))
             );
             assert!(term.check(term_type, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -537,7 +544,7 @@ mod tests {
 
             assert_eq!(term_type, Term::type_usize(0, arena));
             assert!(term.check(term_type, arena).is_ok());
-        })
+        });
     }
 
     #[test]
@@ -548,7 +555,7 @@ mod tests {
 
             assert_eq!(term_type, Term::type_usize(1, arena));
             assert!(term.check(term_type, arena).is_ok());
-        })
+        });
     }
 
     mod failed_type_inference {
@@ -569,7 +576,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -587,7 +594,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -605,7 +612,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -623,7 +630,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -641,7 +648,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -659,7 +666,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -689,7 +696,7 @@ mod tests {
                         .into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -706,7 +713,7 @@ mod tests {
                         kind: TypeCheckerError::NotUniverse(arena.build_term_raw(var(2.into(), prop()))).into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -720,7 +727,7 @@ mod tests {
                         kind: TypeCheckerError::NotUniverse(arena.build_term_raw(prod(prop(), prop()))).into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -736,7 +743,7 @@ mod tests {
                         kind: TypeCheckerError::NotUniverse(prop.prod(type_, arena)).into()
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -755,7 +762,7 @@ mod tests {
                         .into(),
                     })
                 );
-            })
+            });
         }
 
         #[test]
@@ -768,7 +775,7 @@ mod tests {
                         kind: TypeCheckerError::TypeMismatch(Term::type_usize(0, arena), prop).into(),
                     })
                 );
-            })
+            });
         }
     }
 }

parser/Cargo.toml

 [package]
 name = "parser"
-edition.workspace = true
-version.workspace = true
+
 authors.workspace = true
+edition.workspace = true
 license.workspace = true
+repository.workspace = true
+version.workspace = true
 
 [dependencies]
 kernel.path = "../kernel"
 
 derive_more.workspace = true
-pest.workspace = true
-pest_derive.workspace = true
+
+pest = "2.5"
+pest_derive = "2.5"