From 8b20ac8090549dc6574b366f078e192beceefe61 Mon Sep 17 00:00:00 2001
From: belazy <aarthuur01@gmail.com>
Date: Sat, 24 Dec 2022 15:24:21 +0100
Subject: [PATCH] =?UTF-8?q?Resolve=20"Add=20Universe=20Polymorphism"=20?=
=?UTF-8?q?=E2=9C=A8=EF=B8=8F=20Closes=20#28=20=F0=9F=90=94=EF=B8=8F?=
=?UTF-8?q?=F0=9F=91=8D=EF=B8=8F=20Approved-by:=20belazy=20<aarthuur01@gma?=
=?UTF-8?q?il.com>=20Approved-by:=20aalbert=20<augustin.albert@bleu-azure.?=
=?UTF-8?q?fr>=20Approved-by:=20v-lafeychine=20<vincent.lafeychine@proton.?=
=?UTF-8?q?me>=20Approved-by:=20loutr=20<loutr@crans.org>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* fix(proost): added Define command back (need to distinguish between the two in order to bind and reuse correctly later
* chore(kernel, calculus/level): adapt documentation to new type
* chore(level): Add specific enum to handle comparison state
* chore(kernel): c-o-v-e-r-a-g-e
* chore(parser): remove TODO
* chore(parser): more coverage
* fix(kernel): trailing comma when printing `InstantiatedDeclaration`s
* fix(kernel): chiale + aboie, coverage
* chore(kernel): mention #14
* chore(kernel): yet another test
* chore(kernel): always more coverage
* chore(parser): add issue nb to todo
* fix(kernel): avoid reentrant entry bug when infering type of decls with 0 universe arguments
* fix(parser): revert comit, wtf clippy ?
* chore(parser): remove unused branch
* chore(kernel): another test
* Apply 1 suggestion(s) to 1 file(s)
* fix(kernel): remove dangerous function
* chore(kernel): always more coverage
* feat(parser): remove `Define` command
* fix(kernel): interface checking for decls
* Apply 1 suggestion(s) to 1 file(s)
* chore(kernel): add coverage
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* chore(kernel): coverage
* Apply 1 suggestion(s) to 1 file(s)
* fix(kernel): over-agressive normalization
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* fix(parser): avoid spacing befor univ decls/vars
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* fix(proost): check existing identifiers for al definitions
* Apply 1 suggestion(s) to 1 file(s)
* feat(parser): add `DeclarationCheckType`
* chore(kernel): remove unused test
* fix(proost): type-check terms before `Eval`uating
* docs: update
* fix: further adjustments to parser
* chore: formatting + some adjustments for kernel tests
* fix(parser, proost): modify command generation for declarations
* chore(parser): add tests todo
* chore(parser): tests on sort parsing
* fix(parser): tests
* feat(parser): parse universe bindings
* feat(parser): parse universe declarations in define_type
* fix(level): comments
* chore: remove biging as a dependency
* chore(kernel): remove todo
* chore(kernel): remove unused file
* chore(kernel): more tests
* chore(kernel): documentation of `level_builder.rs`
* feat(kernel): tests coverage
* fix(kernel): tests
* feat(kernel/term/builder): add binding to (instantiated) declaration builders
* feat(kernel): add builders for declaration
* chore(kernel): refactor builder file hierarchy and simplify these files
* fix(proost): some import errors
* feat(parser): add parsing for univ parameters of definitions
* chore(kernel): add todo
* fix: remove lifetime dependency on LevelEnvironment
* feat : add inference for declarations.
* feat(parser): add new parsing rules for levels
* feat(parser): new syntax for universe polymorphism
* feat(kernel): add type-checking for Decls
* feat: incorporate LevelBuilder in TermBuilder
* fix(kernel): refactor impl organisation: unload most of arena's
* WOOOHOOOO
* fix(kernel, level): fix incorrect assignment in hashcons function
* fix(kernel): more errors
* feat(kernel): fixed some errors
* feat(kernel): finish rudimentary bases for modifying parser and type checker
* feat(kernel): further work on Levels
* WIP feat(kernel): modify declaration.rs structure
* fix(kernel): removing Dweller struct, using a macro instead
* fix(kernel): refactor file structure to add new core types. first attempt for levels.
* feat(kernel): add generic Dweller type
* WIP fix(kernel): refactor file structure to add new core types
* um
* feat:something
* AH
* first commit
---
Cargo.lock | 38 --
Cargo.toml | 1 -
kernel/Cargo.toml | 1 -
kernel/src/calculus/level.rs | 178 +++++++++
kernel/src/calculus/mod.rs | 5 +
kernel/src/calculus/term.rs | 412 ++++++++++++++++++++
kernel/src/error.rs | 12 +-
kernel/src/lib.rs | 10 +-
kernel/src/memory/arena.rs | 243 ++++++++++++
kernel/src/memory/declaration/builder.rs | 185 +++++++++
kernel/src/memory/declaration/mod.rs | 105 ++++++
kernel/src/memory/level/builder.rs | 199 ++++++++++
kernel/src/memory/level/mod.rs | 238 ++++++++++++
kernel/src/memory/mod.rs | 11 +
kernel/src/memory/term/builder.rs | 284 ++++++++++++++
kernel/src/memory/term/mod.rs | 242 ++++++++++++
kernel/src/term/arena.rs | 345 -----------------
kernel/src/term/builders.rs | 254 -------------
kernel/src/term/calculus.rs | 302 ---------------
kernel/src/term/mod.rs | 8 -
kernel/src/type_checker.rs | 462 +++++++++++++----------
kernel/tests/and.rs | 14 +-
parser/Cargo.toml | 1 -
parser/src/command.rs | 26 +-
parser/src/parser.rs | 235 ++++++++++--
parser/src/term.pest | 36 +-
proost/src/evaluator.rs | 56 ++-
proost/src/main.rs | 2 +-
28 files changed, 2671 insertions(+), 1234 deletions(-)
create mode 100644 kernel/src/calculus/level.rs
create mode 100644 kernel/src/calculus/mod.rs
create mode 100644 kernel/src/calculus/term.rs
create mode 100644 kernel/src/memory/arena.rs
create mode 100644 kernel/src/memory/declaration/builder.rs
create mode 100644 kernel/src/memory/declaration/mod.rs
create mode 100644 kernel/src/memory/level/builder.rs
create mode 100644 kernel/src/memory/level/mod.rs
create mode 100644 kernel/src/memory/mod.rs
create mode 100644 kernel/src/memory/term/builder.rs
create mode 100644 kernel/src/memory/term/mod.rs
delete mode 100644 kernel/src/term/arena.rs
delete mode 100644 kernel/src/term/builders.rs
delete mode 100644 kernel/src/term/calculus.rs
delete mode 100644 kernel/src/term/mod.rs
diff --git a/Cargo.lock b/Cargo.lock
index de4781df..bb6450bb 100644
--- a/Cargo.lock
+++ b/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",
]
diff --git a/Cargo.toml b/Cargo.toml
index 4cf76d27..b1013a65 100644
--- a/Cargo.toml
+++ b/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"
diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml
index 95c167d4..f67b0a78 100644
--- a/kernel/Cargo.toml
+++ b/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"
diff --git a/kernel/src/calculus/level.rs b/kernel/src/calculus/level.rs
new file mode 100644
index 00000000..561664d8
--- /dev/null
+++ b/kernel/src/calculus/level.rs
@@ -0,0 +1,178 @@
+//! 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()))
+ )
+ })
+ }
+}
diff --git a/kernel/src/calculus/mod.rs b/kernel/src/calculus/mod.rs
new file mode 100644
index 00000000..850844f0
--- /dev/null
+++ b/kernel/src/calculus/mod.rs
@@ -0,0 +1,5 @@
+//! A collection of computational functions over different types of
+//! [dwellers](crate::memory::arena::Arena)
+
+pub mod level;
+pub mod term;
diff --git a/kernel/src/calculus/term.rs b/kernel/src/calculus/term.rs
new file mode 100644
index 00000000..e1d5325e
--- /dev/null
+++ b/kernel/src/calculus/term.rs
@@ -0,0 +1,412 @@
+//! A set of lambda-calculus quasi-primitives.
+//!
+//! 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};
+
+impl<'arena> Term<'arena> {
+ /// Apply one step of β-reduction, using the leftmost-outermost evaluation strategy.
+ pub fn beta_reduction(self, arena: &mut Arena<'arena>) -> Self {
+ match *self {
+ App(t1, t2) => match *t1 {
+ Abs(_, t1) => t1.substitute(t2, 1, arena),
+ _ => {
+ let t1_new = t1.beta_reduction(arena);
+ if t1_new == t1 {
+ let t2_new = t2.beta_reduction(arena);
+ t1.app(t2_new, arena)
+ } else {
+ t1_new.app(t2, arena)
+ }
+ },
+ },
+ Abs(arg_type, body) => {
+ let body = body.beta_reduction(arena);
+ arg_type.abs(body, arena)
+ },
+ Prod(arg_type, body) => {
+ let body = body.beta_reduction(arena);
+ arg_type.prod(body, arena)
+ },
+ Decl(decl) => decl.get_term(arena),
+ _ => self,
+ }
+ }
+
+ /// Returns the term `self` where all variables with de Bruijn index larger than `depth` are offset
+ /// by `offset`.
+ 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 = t1.shift(offset, depth, arena);
+ let t2 = t2.shift(offset, depth, arena);
+ t1.app(t2, arena)
+ },
+ 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 = arg_type.shift(offset, depth, arena);
+ let body = body.shift(offset, depth + 1, arena);
+ arg_type.prod(body, arena)
+ },
+ _ => self,
+ }
+ }
+
+ /// Returns the term `self` where all instances of the variable tracked by `depth` are substituted
+ /// with `sub`.
+ 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 = l.substitute(sub, depth, arena);
+ let r = r.substitute(sub, depth, arena);
+ l.app(r, 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 = arg_type.substitute(sub, depth, arena);
+ let body = body.substitute(sub, depth + 1, arena);
+ arg_type.prod(body, arena)
+ },
+ _ => 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(self, arena: &mut Arena<'arena>) -> Self {
+ let mut temp = self;
+ let mut res = self.beta_reduction(arena);
+
+ while res != temp {
+ temp = res;
+ res = res.beta_reduction(arena);
+ }
+ res
+ }
+
+ /// Returns the weak-head normal form of a term.
+ 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 = t1.substitute(t2, 1, arena);
+ subst.whnf(arena)
+ },
+ _ => self,
+ },
+ _ => self,
+ })
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ // /!\ most terms used in these tests are ill-typed; they should not be used elsewhere
+ 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_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_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
+
+ assert_eq!(term.beta_reduction(arena), reduced);
+ })
+ }
+
+ #[test]
+ 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_term_raw(app(
+ abs(
+ prop(),
+ abs(
+ prop(),
+ abs(
+ prop(),
+ app(
+ app(
+ app(
+ var(3.into(), prop()),
+ abs(
+ prop(),
+ abs(
+ prop(),
+ app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop()))),
+ ),
+ ),
+ ),
+ abs(prop(), var(2.into(), prop())),
+ ),
+ abs(prop(), var(1.into(), prop())),
+ ),
+ ),
+ ),
+ ),
+ abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
+ ));
+
+ let term_step_1 = arena.build_term_raw(abs(
+ prop(),
+ abs(
+ prop(),
+ app(
+ app(
+ app(
+ abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
+ abs(
+ prop(),
+ abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop())))),
+ ),
+ ),
+ abs(prop(), var(2.into(), prop())),
+ ),
+ abs(prop(), var(1.into(), prop())),
+ ),
+ ),
+ ));
+
+ let term_step_2 = arena.build_term_raw(abs(
+ prop(),
+ abs(
+ prop(),
+ app(
+ app(
+ abs(
+ prop(),
+ app(
+ abs(
+ prop(),
+ abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(5.into(), prop())))),
+ ),
+ var(1.into(), prop()),
+ ),
+ ),
+ abs(prop(), var(2.into(), prop())),
+ ),
+ abs(prop(), var(1.into(), prop())),
+ ),
+ ),
+ ));
+
+ let term_step_3 = arena.build_term_raw(abs(
+ prop(),
+ abs(
+ prop(),
+ app(
+ app(
+ abs(prop(), abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop()))))),
+ abs(prop(), var(2.into(), prop())),
+ ),
+ abs(prop(), var(1.into(), prop())),
+ ),
+ ),
+ ));
+
+ let term_step_4 = arena.build_term_raw(abs(
+ prop(),
+ abs(
+ prop(),
+ app(
+ abs(prop(), app(var(1.into(), prop()), app(abs(prop(), var(3.into(), prop())), var(3.into(), prop())))),
+ abs(prop(), var(1.into(), prop())),
+ ),
+ ),
+ ));
+
+ let term_step_5 = arena.build_term_raw(abs(
+ prop(),
+ abs(
+ prop(),
+ app(abs(prop(), var(1.into(), prop())), app(abs(prop(), var(2.into(), prop())), var(2.into(), prop()))),
+ ),
+ ));
+
+ let term_step_6 =
+ 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_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 = prod(prop(), var(1.into(), prop()));
+ 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)
+ })
+ }
+
+ #[test]
+ fn prod_beta_red() {
+ use_arena(|arena| {
+ 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!(term.beta_reduction(arena), reduced);
+ })
+ }
+
+ #[test]
+ fn app_red_rhs() {
+ use_arena(|arena| {
+ 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!(term.beta_reduction(arena), reduced);
+ })
+ }
+
+ #[test]
+ fn normal_form() {
+ use_arena(|arena| {
+ 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!(term.substitute_univs(&[arena.build_level_raw(zero()), arena.build_level_raw(zero())], arena), term);
+ })
+ }
+}
diff --git a/kernel/src/error.rs b/kernel/src/error.rs
index 5713f329..bf063b57 100644
--- a/kernel/src/error.rs
+++ b/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>>;
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index fae36aaa..b795a4b3 100644
--- a/kernel/src/lib.rs
+++ b/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;
diff --git a/kernel/src/memory/arena.rs b/kernel/src/memory/arena.rs
new file mode 100644
index 00000000..35f762e2
--- /dev/null
+++ b/kernel/src/memory/arena.rs
@@ -0,0 +1,243 @@
+//! 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;
diff --git a/kernel/src/memory/declaration/builder.rs b/kernel/src/memory/declaration/builder.rs
new file mode 100644
index 00000000..00b4b719
--- /dev/null
+++ b/kernel/src/memory/declaration/builder.rs
@@ -0,0 +1,185 @@
+//! 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),
+ }
+ }
+}
diff --git a/kernel/src/memory/declaration/mod.rs b/kernel/src/memory/declaration/mod.rs
new file mode 100644
index 00000000..a2ef8888
--- /dev/null
+++ b/kernel/src/memory/declaration/mod.rs
@@ -0,0 +1,105 @@
+//! 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))
+ }
+}
diff --git a/kernel/src/memory/level/builder.rs b/kernel/src/memory/level/builder.rs
new file mode 100644
index 00000000..eb702a2e
--- /dev/null
+++ b/kernel/src/memory/level/builder.rs
@@ -0,0 +1,199 @@
+//! 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)
+ }
+ }
+}
diff --git a/kernel/src/memory/level/mod.rs b/kernel/src/memory/level/mod.rs
new file mode 100644
index 00000000..fdfb7418
--- /dev/null
+++ b/kernel/src/memory/level/mod.rs
@@ -0,0 +1,238 @@
+//! 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)))")
+ })
+ }
+}
diff --git a/kernel/src/memory/mod.rs b/kernel/src/memory/mod.rs
new file mode 100644
index 00000000..8cf67bcb
--- /dev/null
+++ b/kernel/src/memory/mod.rs
@@ -0,0 +1,11 @@
+//! 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;
diff --git a/kernel/src/memory/term/builder.rs b/kernel/src/memory/term/builder.rs
new file mode 100644
index 00000000..3cb24e68
--- /dev/null
+++ b/kernel/src/memory/term/builder.rs
@@ -0,0 +1,284 @@
+//! 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
+//! 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: converting regular terms into de Bruijn-compatible ones, assigning types to variables,
+//! etc.
+//!
+//! The other way to proceed is built on top of the latter. Users can also manipulate a sort of
+//! *high-level term* or *template*, described by the public enumeration [`Builder`], and at any
+//! moment, [realise](Builder::realise) it.
+
+use derive_more::Display;
+use im_rc::hashmap::HashMap as ImHashMap;
+
+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 TermError<'arena> {
+ #[display(fmt = "unknown identifier {}", _0)]
+ ConstNotFound(&'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, 'arena> = ImHashMap<&'build str, (DeBruijnIndex, Term<'arena>)>;
+
+/// The trait of closures which build terms with an adequate logic.
+///
+/// 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 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> = 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>>(&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(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 = 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: TermError::ConstNotFound(arena.store_name(name)).into(),
+ })
+ }
+}
+
+/// Returns a closure building the Prop term.
+#[inline]
+pub const fn prop<'build>() -> impl BuilderTrait<'build> {
+ |arena, _, _, _| Ok(Term::prop(arena))
+}
+
+/// Returns a closure building the Type `level` term.
+#[inline]
+#[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>(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, 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))
+ }
+}
+
+/// Returns a closure building the lambda-abstraction with a body built from `body` and an argument
+/// type from `arg_type`.
+#[inline]
+#[no_coverage]
+pub const fn abs<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(
+ name: &'build str,
+ arg_type: F1,
+ body: F2,
+) -> 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, lvl_env, depth + 1.into())?;
+ Ok(arg_type.abs(body, arena))
+ }
+}
+
+/// Returns a closure building the dependant product of a term built from `body` over all elements
+/// of the type built from `arg_type`.
+#[inline]
+#[no_coverage]
+pub const fn prod<'build, F1: BuilderTrait<'build>, F2: BuilderTrait<'build>>(
+ name: &'build str,
+ arg_type: F1,
+ body: F2,
+) -> 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, 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::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). 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<'build> {
+ #[display(fmt = "{_0}")]
+ Var(&'build str),
+
+ #[display(fmt = "Prop")]
+ Prop,
+
+ #[display(fmt = "Type {_0}")]
+ Type(Box<level::Builder<'build>>),
+
+ #[display(fmt = "Sort {_0}")]
+ Sort(Box<level::Builder<'build>>),
+
+ #[display(fmt = "{_0} {_1}")]
+ App(Box<Builder<'build>>, Box<Builder<'build>>),
+
+ #[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> {
+ /// 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())
+ }
+
+ 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>(
+ &'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, 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),
+ }
+ }
+}
+
+#[cfg(test)]
+pub(crate) mod raw {
+ use super::*;
+
+ pub trait BuilderTrait = for<'arena> FnOnce(&mut Arena<'arena>) -> Term<'arena>;
+
+ impl<'arena> Arena<'arena> {
+ pub(crate) fn build_term_raw<F: BuilderTrait>(&mut self, f: F) -> Term<'arena> {
+ f(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 prop() -> impl BuilderTrait {
+ |arena| Term::prop(arena)
+ }
+
+ pub const fn type_usize(level: usize) -> impl BuilderTrait {
+ move |arena| Term::type_usize(level, arena)
+ }
+
+ pub const fn sort_<F: level::raw::BuilderTrait>(level: F) -> impl BuilderTrait {
+ move |arena| Term::sort(level(arena), arena)
+ }
+
+ 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<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<F1: BuilderTrait, F2: BuilderTrait>(u1: F1, u2: F2) -> impl BuilderTrait {
+ |arena| {
+ let u1 = u1(arena);
+ let u2 = u2(arena);
+ u1.prod(u2, arena)
+ }
+ }
+}
diff --git a/kernel/src/memory/term/mod.rs b/kernel/src/memory/term/mod.rs
new file mode 100644
index 00000000..a9a5780d
--- /dev/null
+++ b/kernel/src/memory/term/mod.rs
@@ -0,0 +1,242 @@
+//! 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)")
+ })
+ }
+}
diff --git a/kernel/src/term/arena.rs b/kernel/src/term/arena.rs
deleted file mode 100644
index 620eaed7..00000000
--- a/kernel/src/term/arena.rs
+++ /dev/null
@@ -1,345 +0,0 @@
-//! 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);
- }
-}
diff --git a/kernel/src/term/builders.rs b/kernel/src/term/builders.rs
deleted file mode 100644
index ffa91ff5..00000000
--- a/kernel/src/term/builders.rs
+++ /dev/null
@@ -1,254 +0,0 @@
-//! Collection of safe functions to build Terms
-//!
-//! 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
-//! 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: converting regular terms into de Bruijn-compatible ones, assigning types to variables,
-//! etc.
-//!
-//! The other way to proceed is built on top of the latter. Users can also manipulate a sort of
-//! *high-level term* or *template*, described by the public enumeration [`Builder`], and at any
-//! moment, [realise](Builder::realise) it.
-
-use derive_more::Display;
-use im_rc::hashmap::HashMap as ImHashMap;
-
-use super::arena::{Arena, DeBruijnIndex, Term, UniverseLevel};
-use crate::error::{Error, ResultTerm};
-
-#[non_exhaustive]
-#[derive(Clone, Debug, Display, Eq, PartialEq)]
-pub enum DefinitionError<'arena> {
- #[display(fmt = "unknown identifier {}", _0)]
- ConstNotFound(&'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, 'arena> = ImHashMap<&'build str, (DeBruijnIndex, Term<'arena>)>;
-
-/// 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`.
-///
-/// Please note that this is just a trait alias, meaning it enforces very little 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>;
-
-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())
- }
-}
-
-/// 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| {
- 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)
- })
- .or_else(|| arena.get_binding(name))
- .ok_or(Error {
- kind: DefinitionError::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())
-}
-
-/// 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))
-}
-
-/// 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()))
-}
-
-/// 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))
- }
-}
-
-/// Returns a closure building the lambda-abstraction with a body built from `body` and an argument
-/// type from `arg_type`.
-#[inline]
-#[no_coverage]
-pub const fn abs<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
- 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)?;
- let env = env.update(name, (depth, arg_type));
- let body = body(arena, &env, depth + 1.into())?;
- Ok(arena.abs(arg_type, body))
- }
-}
-
-/// Returns a closure building the dependant product of a term built from `body` over all elements
-/// of the type built from `arg_type`.
-#[inline]
-#[no_coverage]
-pub const fn prod<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTrait<'build, 'arena>>(
- 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)?;
- let env = env.update(name, (depth, arg_type));
- let body = body(arena, &env, depth + 1.into())?;
- Ok(arena.prod(arg_type, body))
- }
-}
-
-/// 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
-/// include a name, as in the classic way of writing lambda-terms (i.e. no de Bruijn indices
-/// involved).
-#[derive(Clone, Debug, Display, PartialEq, Eq)]
-pub enum Builder<'r> {
- #[display(fmt = "{}", _0)]
- Var(&'r str),
-
- #[display(fmt = "Prop")]
- Prop,
-
- #[display(fmt = "Type {}", _0)]
- Type(usize),
-
- #[display(fmt = "{} {}", _0, _1)]
- App(Box<Builder<'r>>, Box<Builder<'r>>),
-
- #[display(fmt = "\u{003BB} {}: {} \u{02192} {}", _0, _1, _2)]
- Abs(&'r str, Box<Builder<'r>>, Box<Builder<'r>>),
-
- #[display(fmt = "\u{03A0} {}: {} \u{02192} {}", _0, _1, _2)]
- Prod(&'r str, Box<Builder<'r>>, Box<Builder<'r>>),
-}
-
-impl<'build> Builder<'build> {
- /// Build a terms from a [`Builder`]. This internally uses functions described in the
- /// [builders](`crate::term::builders`) 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)
- }
-
- fn realise_in_context<'arena>(
- &self,
- arena: &mut Arena<'arena>,
- env: &Environment<'build, 'arena>,
- 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),
- }
- }
-}
-
-#[cfg(test)]
-pub(crate) mod raw {
- use super::*;
-
- pub trait BuilderTrait<'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> {
- f(self)
- }
- }
-
- impl<'arena> Term<'arena> {
- pub(crate) const fn into(self) -> impl BuilderTrait<'arena> {
- move |_: &mut Arena<'arena>| self
- }
- }
-
- 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<'arena>() -> impl BuilderTrait<'arena> {
- |env: &mut Arena<'arena>| env.prop()
- }
-
- pub const fn type_<'arena>(level: UniverseLevel) -> impl BuilderTrait<'arena> {
- move |env: &mut Arena<'arena>| env.type_(level)
- }
-
- 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 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 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)
- }
- }
-}
diff --git a/kernel/src/term/calculus.rs b/kernel/src/term/calculus.rs
deleted file mode 100644
index da57c2fb..00000000
--- a/kernel/src/term/calculus.rs
+++ /dev/null
@@ -1,302 +0,0 @@
-//! A set of lambda-calculus quasi-primitives.
-//!
-//! 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 super::arena::{Arena, Payload, Term};
-
-impl<'arena> Arena<'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 {
- App(t1, t2) => match *t1 {
- Abs(_, t1) => self.substitute(t1, t2, 1),
- _ => {
- let t1_new = self.beta_reduction(t1);
- if t1_new == t1 {
- let t2_new = self.beta_reduction(t2);
- self.app(t1, t2_new)
- } else {
- self.app(t1_new, t2)
- }
- },
- },
- Abs(arg_type, body) => {
- let body = self.beta_reduction(body);
- self.abs(arg_type, body)
- },
- Prod(arg_type, body) => {
- let body = self.beta_reduction(body);
- self.prod(arg_type, body)
- },
- _ => t,
- }
- }
-
- /// Returns the term `t` 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_),
- App(t1, t2) => {
- let t1 = self.shift(t1, offset, depth);
- let t2 = self.shift(t2, offset, depth);
- self.app(t1, t2)
- },
- 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)
- },
- 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)
- },
- _ => t,
- }
- }
-
- /// Returns the term `t` 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_),
- App(l, r) => {
- let l = arena.substitute(l, sub, depth);
- let r = arena.substitute(r, sub, depth);
- arena.app(l, r)
- },
- 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)
- },
- 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)
- },
- _ => t,
- })
- }
-
- /// 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);
-
- while res != temp {
- temp = res;
- res = self.beta_reduction(res);
- }
- 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) {
- Abs(_, t1) => {
- let subst = self.substitute(t1, t2, 1);
- self.whnf(subst)
- },
- _ => t,
- },
- _ => t,
- })
- }
-}
-
-#[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::*;
-
- #[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()))));
- // λx.x x
- let reduced = arena.build_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
-
- assert_eq!(arena.beta_reduction(term), reduced);
- })
- }
-
- #[test]
- 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(
- abs(
- prop(),
- abs(
- prop(),
- abs(
- prop(),
- app(
- app(
- app(
- var(3.into(), prop()),
- abs(
- prop(),
- abs(
- prop(),
- app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop()))),
- ),
- ),
- ),
- abs(prop(), var(2.into(), prop())),
- ),
- abs(prop(), var(1.into(), prop())),
- ),
- ),
- ),
- ),
- abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
- ));
-
- let term_step_1 = arena.build_raw(abs(
- prop(),
- abs(
- prop(),
- app(
- app(
- app(
- abs(prop(), abs(prop(), app(var(2.into(), prop()), var(1.into(), prop())))),
- abs(
- prop(),
- abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop())))),
- ),
- ),
- abs(prop(), var(2.into(), prop())),
- ),
- abs(prop(), var(1.into(), prop())),
- ),
- ),
- ));
-
- let term_step_2 = arena.build_raw(abs(
- prop(),
- abs(
- prop(),
- app(
- app(
- abs(
- prop(),
- app(
- abs(
- prop(),
- abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(5.into(), prop())))),
- ),
- var(1.into(), prop()),
- ),
- ),
- abs(prop(), var(2.into(), prop())),
- ),
- abs(prop(), var(1.into(), prop())),
- ),
- ),
- ));
-
- let term_step_3 = arena.build_raw(abs(
- prop(),
- abs(
- prop(),
- app(
- app(
- abs(prop(), abs(prop(), app(var(1.into(), prop()), app(var(2.into(), prop()), var(4.into(), prop()))))),
- abs(prop(), var(2.into(), prop())),
- ),
- abs(prop(), var(1.into(), prop())),
- ),
- ),
- ));
-
- let term_step_4 = arena.build_raw(abs(
- prop(),
- abs(
- prop(),
- app(
- abs(prop(), app(var(1.into(), prop()), app(abs(prop(), var(3.into(), prop())), var(3.into(), prop())))),
- abs(prop(), var(1.into(), prop())),
- ),
- ),
- ));
-
- let term_step_5 = arena.build_raw(abs(
- prop(),
- abs(
- prop(),
- app(abs(prop(), var(1.into(), prop())), app(abs(prop(), var(2.into(), prop())), var(2.into(), prop()))),
- ),
- ));
-
- let term_step_6 =
- arena.build_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);
- })
- }
-
- #[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()));
-
- assert_eq!(arena.beta_reduction(term), 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())));
-
- assert_eq!(arena.beta_reduction(term), 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()))));
-
- assert_eq!(arena.beta_reduction(term), 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());
-
- assert_eq!(arena.normal_form(term), normal_form);
- })
- }
-}
diff --git a/kernel/src/term/mod.rs b/kernel/src/term/mod.rs
deleted file mode 100644
index 42fe9d28..00000000
--- a/kernel/src/term/mod.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-//! 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;
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index fbadb941..2ef2b54f 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -2,14 +2,13 @@
//!
//! The logical core of the kernel.
-use std::cmp::max;
-
use derive_more::Display;
-use num_bigint::BigUint;
use Payload::*;
use crate::error::{Error, Result, ResultTerm};
-use crate::term::arena::{Arena, Payload, Term};
+use crate::memory::arena::Arena;
+use crate::memory::declaration::Declaration;
+use crate::memory::term::{Payload, Term};
#[derive(Clone, Debug, Display, Eq, PartialEq)]
#[display(fmt = "{}: {}", _0, _1)]
@@ -19,117 +18,112 @@ pub struct TypedTerm<'arena>(Term<'arena>, Term<'arena>);
#[non_exhaustive]
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum TypeCheckerError<'arena> {
- /// `t` is not a universe
- #[display(fmt = "{} is not a universe", _0)]
+ #[display(fmt = "{_0} is not a universe")]
NotUniverse(Term<'arena>),
- /// `t1` and `t2` are not definitionally equal
- #[display(fmt = "{} and {} are not definitionally equal", _0, _1)]
+ #[display(fmt = "{_0} and {_1} are not definitionally equal")]
NotDefEq(Term<'arena>, Term<'arena>),
- /// function `f` expected a `t`, received `x: t`'
- #[display(fmt = "function {} expects a term of type {}, received {}", _0, _1, _2)]
+ #[display(fmt = "function {_0} expects a term of type {_1}, received {_2}")]
WrongArgumentType(Term<'arena>, Term<'arena>, TypedTerm<'arena>),
- /// `t1` of type `ty` is not a function so cannot be applied to `t2`
- #[display(fmt = "{} is not a function, it cannot be applied to {}", _0, _1)]
+ #[display(fmt = "{_0} is not a function, it cannot be applied to {_1}")]
NotAFunction(TypedTerm<'arena>, Term<'arena>),
- /// Expected `ty1`, found `ty2`
- #[display(fmt = "expected {}, got {}", _0, _1)]
+ #[display(fmt = "expected {_0}, got {_1}")]
TypeMismatch(Term<'arena>, Term<'arena>),
}
-impl<'arena> Arena<'arena> {
+impl<'arena> Term<'arena> {
/// Conversion function, checks whether two terms are definitionally equal.
///
/// The conversion is untyped, meaning that it should **only** be called during type-checking
- /// when the two `Term`s are already known to be of the same type and in the same context.
- fn conversion(&mut self, lhs: Term<'arena>, rhs: Term<'arena>) -> bool {
- if lhs == rhs {
+ /// when the two [`Term`]s are already known to be of the same type and in the same context.
+ fn conversion(self, rhs: Self, arena: &mut Arena<'arena>) -> bool {
+ if self == rhs {
return true;
}
- let lhs = self.whnf(lhs);
- let rhs = self.whnf(rhs);
+ let lhs = self.whnf(arena);
+ let rhs = rhs.whnf(arena);
if lhs == rhs {
return true;
}
match (&*lhs, &*rhs) {
- // For universe conversion (Prop/Type), the equality of conversion is syntactical over the whnfs, as such,
- // they live in the same place in memory. This means we don't need to check for these cases here.
- // /!\ Once we have universe polymorphism, this won't be the case anymore and these cases will need to be added
- // again.
+ (Sort(l1), Sort(l2)) => l1.is_eq(*l2, arena),
+
(Var(i, _), Var(j, _)) => i == j,
- (&Prod(t1, u1), &Prod(t2, u2)) => self.conversion(t1, t2) && self.conversion(u1, u2),
+ (&Prod(t1, u1), &Prod(t2, u2)) => t1.conversion(t2, arena) && u1.conversion(u2, arena),
// Since we assume that both values already have the same type,
// checking conversion over the argument type is useless.
// However, this doesn't mean we can simply remove the arg type
// from the type constructor in the enum, it is needed to quote back to terms.
- (&Abs(_, t), &Abs(_, u)) => self.conversion(t, u),
+ (&Abs(_, t), &Abs(_, u)) => t.conversion(u, arena),
+
+ (&App(t1, u1), &App(t2, u2)) => t1.conversion(t2, arena) && u1.conversion(u2, arena),
- (&App(t1, u1), &App(t2, u2)) => self.conversion(t1, t2) && self.conversion(u1, u2),
+ // We do not automatically unfold definitions during normalisation because of how costly it is.
+ // Instead, when the same declaration is met on both terms, they're also equal in memory.
+ // Otherwise, either one of them is not a decl, or they are two different decls. In both case, we unfold decls to check
+ // equality.
+ (&Decl(decl), _) => decl.get_term(arena).conversion(rhs, arena),
+
+ (_, &Decl(decl)) => decl.get_term(arena).conversion(lhs, arena),
_ => false,
}
}
/// Checks whether two terms are definitionally equal.
- pub fn is_def_eq(&mut self, lhs: Term<'arena>, rhs: Term<'arena>) -> Result<'arena, ()> {
- self.conversion(lhs, rhs).then_some(()).ok_or(Error {
- kind: TypeCheckerError::NotDefEq(lhs, rhs).into(),
+ 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(),
})
}
/// Computes the universe in which `(x: A) -> B` lives when `A: lhs` and `B: rhs`.
- fn imax(&mut self, lhs: Term<'arena>, rhs: Term<'arena>) -> ResultTerm<'arena> {
- match *rhs {
- // Because Prop is impredicative, if B : Prop, then (x : A) -> B : Prop
- Prop => Ok(self.prop()),
-
- Type(ref i) => match *lhs {
- Prop => Ok(self.type_(i.clone())),
-
- // else if u1 = Type(i) and u2 = Type(j), then (x : A) -> B : Type(max(i,j))
- Type(ref j) => Ok(self.type_(max(i, j).clone())),
-
+ fn imax(self, rhs: Self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
+ match *self {
+ Sort(l1) => match *rhs {
+ Sort(l2) => {
+ let lvl = l1.imax(l2, arena);
+ Ok(Term::sort(lvl, arena))
+ },
_ => Err(Error {
- kind: TypeCheckerError::NotUniverse(lhs).into(),
+ kind: TypeCheckerError::NotUniverse(rhs).into(),
}),
},
-
_ => Err(Error {
- kind: TypeCheckerError::NotUniverse(rhs).into(),
+ kind: TypeCheckerError::NotUniverse(self).into(),
}),
}
}
- /// Infers the type of the term `t`, living in arena `self`.
- pub fn infer(&mut self, t: Term<'arena>) -> ResultTerm<'arena> {
- t.get_type_or_try_init(|| match *t {
- Prop => Ok(self.type_usize(0)),
- Type(ref i) => Ok(self.type_(i.clone() + BigUint::from(1_u64).into())),
+ /// Infers the type of the term `t`, living in arena `arena`.
+ pub fn infer_raw(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
+ match *self {
+ Sort(lvl) => Ok(Term::sort(lvl.succ(arena), arena)),
Var(_, type_) => Ok(type_),
Prod(t, u) => {
- let univ_t = self.infer(t)?;
- let univ_u = self.infer(u)?;
+ let univ_t = t.infer(arena)?;
+ let univ_u = u.infer(arena)?;
- let univ_t = self.whnf(univ_t);
- let univ_u = self.whnf(univ_u);
- self.imax(univ_t, univ_u)
+ let univ_t = univ_t.whnf(arena);
+ let univ_u = univ_u.whnf(arena);
+ univ_t.imax(univ_u, arena)
},
Abs(t, u) => {
- let type_t = self.infer(t)?;
+ let type_t = t.infer(arena)?;
match *type_t {
- Type(_) | Prop => {
- let type_u = self.infer(u)?;
- Ok(self.prod(t, type_u))
+ Sort(_) => {
+ let type_u = u.infer(arena)?;
+ Ok(t.prod(type_u, arena))
},
_ => Err(Error {
kind: TypeCheckerError::NotUniverse(type_t).into(),
@@ -138,14 +132,14 @@ impl<'arena> Arena<'arena> {
},
App(t, u) => {
- let type_t = self.infer(t)?;
- let type_t = self.whnf(type_t);
+ let type_t = t.infer(arena)?;
+ let type_t = type_t.whnf(arena);
match *type_t {
Prod(arg_type, cls) => {
- let type_u = self.infer(u)?;
+ let type_u = u.infer(arena)?;
- if self.conversion(type_u, arg_type) {
- Ok(self.substitute(cls, u, 1))
+ if type_u.conversion(arg_type, arena) {
+ Ok(cls.substitute(u, 1, arena))
} else {
Err(Error {
kind: TypeCheckerError::WrongArgumentType(t, arg_type, TypedTerm(u, type_u)).into(),
@@ -158,70 +152,129 @@ impl<'arena> Arena<'arena> {
}),
}
},
- })
+
+ Decl(decl) => decl.get_type_or_try_init(Term::infer_raw, arena),
+ }
+ }
+
+ /// Infers the type of the term `t`, living in arena `arena`, checks for memoization.
+ 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 `self` is of type `ty`.
- pub fn check(&mut self, t: Term<'arena>, ty: Term<'arena>) -> Result<'arena, ()> {
- let tty = self.infer(t)?;
+ /// Checks whether the term `t` living in `arena` is of type `ty`.
+ pub fn check(self, ty: Self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
+ let tty = self.infer(arena)?;
- self.conversion(tty, ty).then_some(()).ok_or(Error {
+ tty.conversion(ty, arena).then_some(()).ok_or(Error {
kind: TypeCheckerError::TypeMismatch(tty, ty).into(),
})
}
}
+impl<'arena> Declaration<'arena> {
+ /// Infer the type of a declaration.
+ ///
+ /// 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.
+ pub fn infer(self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
+ self.0.infer(arena)?;
+ Ok(())
+ }
+
+ pub fn check(self, ty: Self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
+ self.0.check(ty.0, arena)
+ }
+}
+
#[cfg(test)]
mod tests {
use super::*;
- use crate::term::arena::use_arena;
- use crate::term::builders::raw::*;
+ use crate::memory::arena::use_arena;
+ use crate::memory::term::builder::raw::*;
- fn id<'arena>() -> impl BuilderTrait<'arena> {
+ fn id() -> impl BuilderTrait {
abs(prop(), var(1.into(), prop()))
}
#[test]
fn def_eq_1() {
use_arena(|arena| {
- let id = arena.build_raw(id());
- let term = arena.build_raw(app(abs(prop(), id.into()), id.into()));
- let normal_form = arena.build_raw(abs(prop(), var(1.into(), prop())));
+ 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())
+ })
+ }
+
+ #[test]
+ fn conv_decl() {
+ 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 prop = arena.build_term_raw(prop());
+
+ assert!(decl.is_def_eq(prop, arena).is_ok());
+ assert!(prop.is_def_eq(decl, arena).is_ok());
+ })
+ }
+
+ #[test]
+ fn infer_decl() {
+ //use std::env;
+ //env::set_var("RUST_BACKTRACE", "1");
+ 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 term = crate::memory::term::Term::decl(decl_, arena);
+ let ty = arena.build_term_raw(type_usize(0));
- assert!(arena.is_def_eq(term, normal_form).is_ok())
+ assert!(term.check(ty, arena).is_ok());
})
}
#[test]
fn def_eq_2() {
use_arena(|arena| {
- let id = arena.build_raw(id());
- let term = arena.build_raw(app(abs(prop(), abs(prop(), var(2.into(), prop()))), id.into()));
- let normal_form = arena.build_raw(abs(prop(), id.into()));
+ 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!(arena.is_def_eq(term, normal_form).is_ok())
+ assert!(term.is_def_eq(normal_form, arena).is_ok())
})
}
#[test]
fn def_eq_self() {
use_arena(|arena| {
- let id = arena.build_raw(id());
// λa.a (λx.x) (λx.x)
- let term = arena.build_raw(abs(prop(), app(app(var(2.into(), prop()), id.into()), id.into())));
+ let term = arena.build_term_raw(abs(prop(), app(app(var(2.into(), prop()), id()), id())));
- assert!(arena.is_def_eq(term, term).is_ok());
+ assert!(term.is_def_eq(term, arena).is_ok());
})
}
#[test]
fn failed_def_equal() {
use_arena(|arena| {
- let term_lhs = arena.prop();
- let term_rhs = arena.type_usize(0);
+ let term_lhs = Term::prop(arena);
+ let term_rhs = Term::type_usize(0, arena);
assert_eq!(
- arena.is_def_eq(term_lhs, term_rhs),
+ term_lhs.is_def_eq(term_rhs, arena),
Err(Error {
kind: TypeCheckerError::NotDefEq(term_lhs, term_rhs).into()
})
@@ -232,13 +285,11 @@ mod tests {
#[test]
fn failed_prod_binder_conversion() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
-
- let term_lhs = arena.build_raw(prod(prop(), prop()));
- let term_rhs = arena.build_raw(prod(type_0.into(), prop()));
+ let term_lhs = arena.build_term_raw(prod(prop(), prop()));
+ let term_rhs = arena.build_term_raw(prod(type_usize(0), prop()));
assert_eq!(
- arena.is_def_eq(term_lhs, term_rhs),
+ term_lhs.is_def_eq(term_rhs, arena),
Err(Error {
kind: TypeCheckerError::NotDefEq(term_lhs, term_rhs).into()
})
@@ -249,13 +300,11 @@ mod tests {
#[test]
fn failed_app_head_conversion() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
- let term_lhs = arena.build_raw(abs(type_0.into(), abs(type_0.into(), app(var(1.into(), prop()), prop()))));
-
- let term_rhs = arena.build_raw(abs(type_0.into(), abs(type_0.into(), app(var(2.into(), prop()), prop()))));
+ let term_lhs = arena.build_term_raw(abs(type_usize(0), abs(type_usize(0), app(var(1.into(), prop()), prop()))));
+ let term_rhs = arena.build_term_raw(abs(type_usize(0), abs(type_usize(0), app(var(2.into(), prop()), prop()))));
assert_eq!(
- arena.is_def_eq(term_lhs, term_rhs),
+ term_lhs.is_def_eq(term_rhs, arena),
Err(Error {
kind: TypeCheckerError::NotDefEq(term_lhs, term_rhs).into()
})
@@ -266,15 +315,15 @@ mod tests {
#[test]
fn typed_reduction_app_1() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
- let term = arena.build_raw(app(abs(type_0.into(), var(1.into(), type_0.into())), prop()));
+ let type_0 = Term::type_usize(0, arena);
+ let term = arena.build_term_raw(app(abs(type_usize(0), var(1.into(), type_usize(0))), prop()));
- let reduced = arena.build_raw(prop());
- assert!(arena.is_def_eq(term, reduced).is_ok());
+ let reduced = arena.build_term_raw(prop());
+ assert!(term.is_def_eq(reduced, arena).is_ok());
- let term_type = arena.infer(term).unwrap();
+ let term_type = term.infer(arena).unwrap();
assert_eq!(term_type, type_0);
- assert!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
@@ -282,7 +331,7 @@ mod tests {
// this test uses more intricate terms. In order to preserve some readability,
// switching to extern_build, which is clearer.
fn typed_reduction_app_2() {
- use crate::term::builders::*;
+ use crate::memory::term::builder::*;
use_arena(|arena| {
// (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λf.λg.f g)
let term = arena
@@ -350,42 +399,40 @@ mod tests {
// λa: P. λb: P. b
let reduced = arena.build(abs("_", prop(), abs("x", prop(), var("x")))).unwrap();
- assert!(arena.is_def_eq(term, reduced).is_ok());
+ assert!(term.is_def_eq(reduced, arena).is_ok());
- let term_type = arena.infer(term).unwrap();
+ 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!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
#[test]
fn typed_reduction_universe() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
- let type_1 = arena.type_usize(1);
+ let type_0 = Term::type_usize(0, arena);
+ let type_1 = Term::type_usize(1, arena);
- let term = arena.build_raw(app(abs(prop(), type_0.into()), prod(prop(), var(1.into(), prop()))));
+ let term = arena.build_term_raw(app(abs(prop(), type_usize(0)), prod(prop(), var(1.into(), prop()))));
- assert!(arena.is_def_eq(term, type_0).is_ok());
+ assert!(term.is_def_eq(type_0, arena).is_ok());
- let term_type = arena.infer(term).unwrap();
+ let term_type = term.infer(arena).unwrap();
assert_eq!(term_type, type_1);
- assert!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
#[test]
fn escape_from_prop() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
- let type_1 = arena.type_usize(1);
- let term = arena.build_raw(abs(prop(), prod(var(1.into(), prop()), type_0.into())));
+ let term = arena.build_term_raw(abs(prop(), prod(var(1.into(), prop()), type_usize(0))));
- let term_type = arena.infer(term).unwrap();
- let expected_type = arena.build_raw(prod(prop(), type_1.into()));
+ 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!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
@@ -394,7 +441,7 @@ mod tests {
use_arena(|arena| {
// λ(x: P -> P).(λ(y: P).x y) x
// λP -> P.(λP.2 1) 1
- let term = arena.build_raw(abs(
+ let term = arena.build_term_raw(abs(
prod(prop(), prop()),
app(
abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop()))),
@@ -403,68 +450,66 @@ mod tests {
));
// λ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!(arena.is_def_eq(term, reduced).is_ok())
+ assert!(term.is_def_eq(reduced, arena).is_ok())
})
}
#[test]
fn typed_prod_1() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
- let term = arena.build_raw(prod(prop(), prop()));
- let term_type = arena.infer(term).unwrap();
+ let type_0 = Term::type_usize(0, arena);
+ let term = arena.build_term_raw(prod(prop(), prop()));
+ let term_type = term.infer(arena).unwrap();
assert_eq!(term_type, type_0);
- assert!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
#[test]
fn typed_prod_2() {
use_arena(|arena| {
- let term = arena.build_raw(prod(prop(), var(1.into(), prop())));
- let term_type = arena.infer(term).unwrap();
+ let term = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
+ let term_type = term.infer(arena).unwrap();
- assert_eq!(term_type, arena.prop());
- assert!(arena.check(term, term_type).is_ok());
+ assert_eq!(term_type, Term::prop(arena));
+ assert!(term.check(term_type, arena).is_ok());
})
}
#[test]
fn typed_prod_3() {
use_arena(|arena| {
- let term = arena.build_raw(abs(prop(), abs(var(1.into(), prop()), var(1.into(), var(2.into(), prop())))));
- let term_type = arena.infer(term).unwrap();
- let expected_type = arena.build_raw(prod(prop(), prod(var(1.into(), prop()), var(2.into(), prop()))));
+ let term = arena.build_term_raw(abs(prop(), abs(var(1.into(), prop()), var(1.into(), var(2.into(), prop())))));
+ let term_type = term.infer(arena).unwrap();
+ let expected_type = arena.build_term_raw(prod(prop(), prod(var(1.into(), prop()), var(2.into(), prop()))));
assert_eq!(term_type, expected_type);
- assert!(arena.check(term, term_type).is_ok());
+ assert!(term.check(term_type, arena).is_ok());
})
}
#[test]
fn typed_polymorphism() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
+ let identity = arena
+ .build_term_raw(abs(type_usize(0), abs(var(1.into(), type_usize(0)), var(1.into(), var(2.into(), type_usize(0))))));
- let identity =
- arena.build_raw(abs(type_0.into(), abs(var(1.into(), type_0.into()), var(1.into(), var(2.into(), type_0.into())))));
-
- let identity_type = arena.infer(identity).unwrap();
+ let identity_type = identity.infer(arena).unwrap();
let expected_type =
- arena.build_raw(prod(type_0.into(), prod(var(1.into(), type_0.into()), var(2.into(), type_0.into()))));
+ arena.build_term_raw(prod(type_usize(0), prod(var(1.into(), type_usize(0)), var(2.into(), type_usize(0)))));
assert_eq!(identity_type, expected_type);
- assert!(arena.check(identity, identity_type).is_ok());
+ assert!(identity.check(identity_type, arena).is_ok());
})
}
#[test]
fn typed_polymorphism_2() {
use_arena(|arena| {
- let term = arena.build_raw(abs(
+ let term = arena.build_term_raw(abs(
prop(),
abs(
prop(),
@@ -474,32 +519,35 @@ mod tests {
),
),
));
- let term_type = arena.infer(term).unwrap();
+ let term_type = term.infer(arena).unwrap();
- assert_eq!(term_type, arena.build_raw(prod(prop(), prod(prop(), prod(prod(prop(), prod(prop(), prop())), prop())))));
- assert!(arena.check(term, term_type).is_ok());
+ assert_eq!(
+ term_type,
+ arena.build_term_raw(prod(prop(), prod(prop(), prod(prod(prop(), prod(prop(), prop())), prop()))))
+ );
+ assert!(term.check(term_type, arena).is_ok());
})
}
#[test]
fn type_hierarchy_prop() {
use_arena(|arena| {
- let term = arena.prop();
- let term_type = arena.infer(term).unwrap();
+ let term = Term::prop(arena);
+ let term_type = term.infer(arena).unwrap();
- assert_eq!(term_type, arena.type_usize(0));
- assert!(arena.check(term, term_type).is_ok());
+ assert_eq!(term_type, Term::type_usize(0, arena));
+ assert!(term.check(term_type, arena).is_ok());
})
}
#[test]
fn type_hierarchy_type() {
use_arena(|arena| {
- let term = arena.type_usize(0);
- let term_type = arena.infer(term).unwrap();
+ let term = Term::type_usize(0, arena);
+ let term_type = term.infer(arena).unwrap();
- assert_eq!(term_type, arena.type_usize(1));
- assert!(arena.check(term, term_type).is_ok());
+ assert_eq!(term_type, Term::type_usize(1, arena));
+ assert!(term.check(term_type, arena).is_ok());
})
}
@@ -509,12 +557,16 @@ mod tests {
#[test]
fn not_function_abs() {
use_arena(|arena| {
- let term = arena.build_raw(abs(app(prop(), prop()), prop()));
+ let term = arena.build_term_raw(abs(app(prop(), prop()), prop()));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into()
})
);
})
@@ -523,12 +575,16 @@ mod tests {
#[test]
fn not_function_prod_1() {
use_arena(|arena| {
- let term = arena.build_raw(prod(prop(), app(prop(), prop())));
+ let term = arena.build_term_raw(prod(prop(), app(prop(), prop())));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into()
})
);
})
@@ -537,12 +593,16 @@ mod tests {
#[test]
fn not_function_prod_2() {
use_arena(|arena| {
- let term = arena.build_raw(prod(app(prop(), prop()), prop()));
+ let term = arena.build_term_raw(prod(app(prop(), prop()), prop()));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into()
})
);
})
@@ -551,12 +611,16 @@ mod tests {
#[test]
fn not_function_app_1() {
use_arena(|arena| {
- let term = arena.build_raw(app(prop(), prop()));
+ let term = arena.build_term_raw(app(prop(), prop()));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into()
})
);
})
@@ -565,12 +629,16 @@ mod tests {
#[test]
fn not_function_app_2() {
use_arena(|arena| {
- let term = arena.build_raw(app(app(prop(), prop()), prop()));
+ let term = arena.build_term_raw(app(app(prop(), prop()), prop()));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into()
})
);
})
@@ -579,12 +647,16 @@ mod tests {
#[test]
fn not_function_app_3() {
use_arena(|arena| {
- let term = arena.build_raw(app(abs(prop(), prop()), app(prop(), prop())));
+ let term = arena.build_term_raw(app(abs(prop(), prop()), app(prop(), prop())));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into()
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into()
})
);
})
@@ -595,7 +667,7 @@ mod tests {
use_arena(|arena| {
// λ(x: P -> P).(λ(y: P).x y) x
// λP -> P.(λP.2 1) 1
- let term = arena.build_raw(abs(
+ let term = arena.build_term_raw(abs(
prod(prop(), prop()),
app(
abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop()))),
@@ -604,12 +676,15 @@ mod tests {
));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
kind: TypeCheckerError::WrongArgumentType(
- arena.build_raw(abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop())))),
- arena.prop(),
- TypedTerm(arena.build_raw(var(1.into(), prod(prop(), prop()))), arena.build_raw(prod(prop(), prop())))
+ arena.build_term_raw(abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop())))),
+ Term::prop(arena),
+ TypedTerm(
+ arena.build_term_raw(var(1.into(), prod(prop(), prop()))),
+ arena.build_term_raw(prod(prop(), prop()))
+ )
)
.into()
})
@@ -620,15 +695,15 @@ mod tests {
#[test]
fn not_universe_abs() {
use_arena(|arena| {
- let term = arena.build_raw(abs(
+ let term = arena.build_term_raw(abs(
prop(),
abs(var(1.into(), prop()), abs(var(1.into(), var(2.into(), prop())), var(1.into(), var(2.into(), prop())))),
));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotUniverse(arena.build_raw(var(2.into(), prop()))).into()
+ kind: TypeCheckerError::NotUniverse(arena.build_term_raw(var(2.into(), prop()))).into()
})
);
})
@@ -637,12 +712,12 @@ mod tests {
#[test]
fn not_universe_prod_1() {
use_arena(|arena| {
- let term = arena.build_raw(prod(id(), prop()));
+ let term = arena.build_term_raw(prod(id(), prop()));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotUniverse(arena.build_raw(prod(prop(), prop()))).into()
+ kind: TypeCheckerError::NotUniverse(arena.build_term_raw(prod(prop(), prop()))).into()
})
);
})
@@ -651,13 +726,14 @@ mod tests {
#[test]
fn not_universe_prod_2() {
use_arena(|arena| {
- let term = arena.build_raw(prod(prop(), abs(prop(), prop())));
+ let term = arena.build_term_raw(prod(prop(), abs(prop(), prop())));
+ let prop = Term::prop(arena);
+ let type_ = Term::type_usize(0, arena);
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
- kind: TypeCheckerError::NotUniverse(arena.build_raw(prod(prop(), type_(BigUint::from(0_u64).into()))))
- .into()
+ kind: TypeCheckerError::NotUniverse(prop.prod(type_, arena)).into()
})
);
})
@@ -666,13 +742,17 @@ mod tests {
#[test]
fn check_fail_1() {
use_arena(|arena| {
- let term = arena.build_raw(app(prop(), prop()));
- let expected_type = arena.prop();
+ let term = arena.build_term_raw(app(prop(), prop()));
+ let expected_type = Term::prop(arena);
assert_eq!(
- arena.check(term, expected_type),
+ term.check(expected_type, arena),
Err(Error {
- kind: TypeCheckerError::NotAFunction(TypedTerm(arena.prop(), arena.type_usize(0)), arena.prop()).into(),
+ kind: TypeCheckerError::NotAFunction(
+ TypedTerm(Term::prop(arena), Term::type_usize(0, arena)),
+ Term::prop(arena)
+ )
+ .into(),
})
);
})
@@ -681,11 +761,11 @@ mod tests {
#[test]
fn check_fail_2() {
use_arena(|arena| {
- let prop = arena.prop();
+ let prop = Term::prop(arena);
assert_eq!(
- arena.check(prop, prop),
+ prop.check(prop, arena),
Err(Error {
- kind: TypeCheckerError::TypeMismatch(arena.type_usize(0), prop).into(),
+ kind: TypeCheckerError::TypeMismatch(Term::type_usize(0, arena), prop).into(),
})
);
})
diff --git a/kernel/tests/and.rs b/kernel/tests/and.rs
index c5013a39..ac4b8394 100644
--- a/kernel/tests/and.rs
+++ b/kernel/tests/and.rs
@@ -1,5 +1,5 @@
-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());
})
}
diff --git a/parser/Cargo.toml b/parser/Cargo.toml
index 02b56ba1..d8817526 100644
--- a/parser/Cargo.toml
+++ b/parser/Cargo.toml
@@ -9,6 +9,5 @@ license.workspace = true
kernel.path = "../kernel"
derive_more.workspace = true
-num-bigint.workspace = true
pest.workspace = true
pest_derive.workspace = true
diff --git a/parser/src/command.rs b/parser/src/command.rs
index 2daa4448..3f3c1fc1 100644
--- a/parser/src/command.rs
+++ b/parser/src/command.rs
@@ -4,15 +4,19 @@
use core::fmt;
-use kernel::term::builders::Builder;
+use kernel::memory::declaration::builder as declaration;
+use kernel::memory::term::builder::Builder;
/// The type of commands that can be received by the kernel.
#[derive(Debug, Eq, PartialEq)]
pub enum Command<'build> {
- /// Define a new term and optionally check that it's type match the given one.
+ /// Define the given term
Define(&'build str, Option<Builder<'build>>, Builder<'build>),
- /// Infer the type of a term and check that it match the given one.
+ /// Define the given declaration
+ Declaration(&'build str, Option<declaration::Builder<'build>>, declaration::Builder<'build>),
+
+ /// Infer the type of a term and check that it matches the given one.
CheckType(Builder<'build>, Builder<'build>),
/// Infer the type of a term.
@@ -33,22 +37,26 @@ impl<'build> fmt::Display for Command<'build> {
use Command::*;
match self {
- Define(name, None, t) => write!(f, "def {} := {}", name, t),
+ Define(name, None, t) => write!(f, "def {name} := {t}"),
+
+ Define(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
+
+ Declaration(name, None, t) => write!(f, "def {name} := {t}"),
- Define(name, Some(ty), t) => write!(f, "def {}: {} := {}", name, ty, t),
+ Declaration(name, Some(ty), t) => write!(f, "def {name}: {ty} := {t}"),
- CheckType(t, ty) => write!(f, "check {}: {}", t, ty),
+ CheckType(t, ty) => write!(f, "check {t}: {ty}"),
- GetType(t) => write!(f, "check {}", t),
+ GetType(t) => write!(f, "check {t}"),
- Eval(t) => write!(f, "eval {}", t),
+ Eval(t) => write!(f, "eval {t}"),
Import(files) => {
write!(f, "imports")?;
files.iter().try_for_each(|file| write!(f, " {file}"))
},
- Search(name) => write!(f, "search {}", name),
+ Search(name) => write!(f, "search {name}"),
}
}
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 8084d02e..a997617f 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -1,11 +1,13 @@
use kernel::location::Location;
-use kernel::term::builders::Builder;
+use kernel::memory::declaration::builder as declaration;
+use kernel::memory::level::builder as level;
+use kernel::memory::term::builder as term;
use pest::error::LineColLocation;
use pest::iterators::Pair;
use pest::{Parser, Span};
use crate::command::Command;
-use crate::error::{Error, ErrorKind};
+use crate::error;
#[derive(Parser)]
#[grammar = "term.pest"]
@@ -18,9 +20,52 @@ fn convert_span(span: Span) -> Location {
((x1, y1), (x2, y2)).into()
}
+/// build universe level from errorless pest's output
+fn parse_level(pair: Pair<Rule>) -> level::Builder {
+ use level::Builder::*;
+
+ // location to be used in a future version
+ let _loc = convert_span(pair.as_span());
+
+ match pair.as_rule() {
+ Rule::Num => {
+ let n = pair.into_inner().as_str().parse().unwrap();
+ Const(n)
+ },
+
+ Rule::Max => {
+ let mut iter = pair.into_inner();
+ let univ1 = parse_level(iter.next().unwrap());
+ let univ2 = parse_level(iter.next().unwrap());
+ Max(box univ1, box univ2)
+ },
+
+ Rule::IMax => {
+ let mut iter = pair.into_inner();
+ let univ1 = parse_level(iter.next().unwrap());
+ let univ2 = parse_level(iter.next().unwrap());
+ IMax(box univ1, box univ2)
+ },
+
+ Rule::Plus => {
+ let mut iter = pair.into_inner();
+ let univ = parse_level(iter.next().unwrap());
+ let n = iter.map(|x| x.as_str().parse::<usize>().unwrap()).sum();
+ Plus(box univ, n)
+ },
+
+ Rule::string => {
+ let name = pair.as_str();
+ Var(name)
+ },
+
+ univ => unreachable!("unexpected universe level: {univ:?}"),
+ }
+}
+
/// Returns a kernel term builder from pest output
-fn parse_term(pair: Pair<Rule>) -> Builder {
- use Builder::*;
+fn parse_term(pair: Pair<Rule>) -> term::Builder {
+ use term::Builder::*;
// location to be used in a future version
let _loc = convert_span(pair.as_span());
@@ -30,12 +75,33 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
Rule::Var => Var(pair.into_inner().as_str()),
- Rule::Type => Type(pair.into_inner().fold(0, |_, x| x.as_str().parse::<usize>().unwrap())),
+ Rule::VarDecl => {
+ let mut iter = pair.into_inner();
+ let name = iter.next().unwrap().as_str();
+ let levels = iter.next().unwrap().into_inner().map(parse_level).collect();
+ Decl(box declaration::InstantiatedBuilder::Var(name, levels))
+ },
+
+ Rule::Type => {
+ if let Some(next) = pair.into_inner().next_back() {
+ Type(box parse_level(next))
+ } else {
+ Type(box level::Builder::Const(0))
+ }
+ },
+
+ Rule::Sort => {
+ if let Some(next) = pair.into_inner().next_back() {
+ Sort(box parse_level(next))
+ } else {
+ Sort(box level::Builder::Const(0))
+ }
+ },
Rule::App => {
let mut iter = pair.into_inner().map(parse_term);
let t = iter.next().unwrap();
- iter.fold(t, |acc, x| App(Box::new(acc), Box::new(x)))
+ iter.fold(t, |acc, x| App(box acc, box x))
},
Rule::Abs => {
@@ -43,11 +109,11 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
let body = parse_term(iter.next_back().unwrap());
iter.flat_map(|pair| {
let mut pair = pair.into_inner();
- let type_ = Box::new(parse_term(pair.next_back().unwrap()));
+ let type_ = box parse_term(pair.next_back().unwrap());
pair.map(move |var| (var.as_str(), type_.clone()))
})
.rev()
- .fold(body, |acc, (var, type_)| Abs(var, type_, Box::new(acc)))
+ .fold(body, |acc, (var, type_)| Abs(var, type_, box acc))
},
Rule::dProd => {
@@ -55,25 +121,25 @@ fn parse_term(pair: Pair<Rule>) -> Builder {
let body = parse_term(iter.next_back().unwrap());
iter.flat_map(|pair| {
let mut pair = pair.into_inner();
- let type_ = Box::new(parse_term(pair.next_back().unwrap()));
+ let type_ = box parse_term(pair.next_back().unwrap());
pair.map(move |var| (var.as_str(), type_.clone()))
})
.rev()
- .fold(body, |acc, (var, type_)| Prod(var, type_, Box::new(acc)))
+ .fold(body, |acc, (var, type_)| Prod(var, type_, box acc))
},
Rule::Prod => {
let mut iter = pair.into_inner();
let ret = parse_term(iter.next_back().unwrap());
- iter.map(parse_term).rev().fold(ret, |acc, argtype| Prod("_", Box::new(argtype), Box::new(acc)))
+ iter.map(parse_term).rev().fold(ret, |acc, argtype| Prod("_", box argtype, box acc))
},
- term => unreachable!("Unexpected term: {:?}", term),
+ term => unreachable!("unexpected term: {term:?}"),
}
}
/// build commands from errorless pest's output
-fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
+fn parse_expr(pair: Pair<Rule>) -> Command {
// location to be used in a future version
let _loc = convert_span(pair.as_span());
@@ -93,17 +159,42 @@ fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
Rule::Define => {
let mut iter = pair.into_inner();
- let s: &'build str = iter.next().unwrap().as_str();
+ let s = iter.next().unwrap().as_str();
let term = parse_term(iter.next().unwrap());
Command::Define(s, None, term)
},
Rule::DefineCheckType => {
let mut iter = pair.into_inner();
- let s: &'build str = iter.next().unwrap().as_str();
- let t = parse_term(iter.next().unwrap());
+ let s = iter.next().unwrap().as_str();
+ let ty = parse_term(iter.next().unwrap());
let term = parse_term(iter.next().unwrap());
- Command::Define(s, Some(t), term)
+
+ Command::Define(s, Some(ty), term)
+ },
+
+ Rule::Declaration => {
+ let mut iter = pair.into_inner();
+ let mut string_decl = iter.next().unwrap().into_inner();
+ let s = string_decl.next().unwrap().as_str();
+ let vars: Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+ let body = iter.next().map(parse_term).unwrap();
+
+ Command::Declaration(s, None, declaration::Builder::Decl(box body, vars))
+ },
+
+ Rule::DeclarationCheckType => {
+ let mut iter = pair.into_inner();
+ let mut string_decl = iter.next().unwrap().into_inner();
+ let s = string_decl.next().unwrap().as_str();
+ let vars: Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+
+ let ty = parse_term(iter.next().unwrap());
+ let decl = iter.next().map(parse_term).unwrap();
+
+ let ty = declaration::Builder::Decl(box ty, vars.clone());
+ let decl = declaration::Builder::Decl(box decl, vars);
+ Command::Declaration(s, Some(ty), decl)
},
Rule::Eval => {
@@ -126,12 +217,14 @@ fn parse_expr<'build>(pair: Pair<'build, Rule>) -> Command<'build> {
}
/// convert pest error to kernel error
-fn convert_error(err: pest::error::Error<Rule>) -> Error {
+fn convert_error(err: pest::error::Error<Rule>) -> error::Error {
// renaming error messages
let err = err.renamed_rules(|rule| match *rule {
Rule::string | Rule::Var => "variable".to_owned(),
- Rule::number => "universe level".to_owned(),
+ Rule::number => "number".to_owned(),
Rule::Define => "def var := term".to_owned(),
+ Rule::Declaration => "def decl.{ vars, ... } := term".to_owned(),
+ Rule::DeclarationCheckType => "def decl.{ vars, ... } : term := term".to_owned(),
Rule::CheckType => "check term : term".to_owned(),
Rule::GetType => "check term".to_owned(),
Rule::DefineCheckType => "def var : term := term".to_owned(),
@@ -141,11 +234,19 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
Rule::App => "application".to_owned(),
Rule::Prop => "Prop".to_owned(),
Rule::Type => "Type".to_owned(),
+ Rule::Sort => "Sort".to_owned(),
Rule::Eval => "eval term".to_owned(),
Rule::filename => "path_to_file".to_owned(),
Rule::ImportFile => "import path_to_file".to_owned(),
Rule::Search => "search var".to_owned(),
- _ => unreachable!("low level rules cannot appear in error messages"),
+ Rule::Max => "max".to_owned(),
+ Rule::Plus => "plus".to_owned(),
+ Rule::IMax => "imax".to_owned(),
+ Rule::arg_univ => "universe argument".to_owned(),
+ Rule::univ_decl => "universe declaration".to_owned(),
+ _ => {
+ unreachable!("low level rules cannot appear in error messages")
+ },
});
// extracting the location from the pest output
@@ -183,8 +284,8 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
for _ in 0..4 {
chars.next();
}
- Error {
- kind: ErrorKind::CannotParse(chars.as_str().to_string()),
+ error::Error {
+ kind: error::ErrorKind::CannotParse(chars.as_str().to_string()),
location: loc,
}
}
@@ -192,30 +293,32 @@ fn convert_error(err: pest::error::Error<Rule>) -> Error {
/// Parse a text input and try to convert it into a command.
///
/// if unsuccessful, a box containing the first error that was encountered is returned.
-pub fn parse_line(line: &str) -> crate::error::Result<Command> {
+pub fn parse_line(line: &str) -> error::Result<Command> {
CommandParser::parse(Rule::command, line).map_err(convert_error).map(|mut pairs| parse_expr(pairs.next().unwrap()))
}
/// Parse a text input and try to convert it into a vector of commands.
///
/// if unsuccessful, a box containing the first error that was encountered is returned.
-pub fn parse_file(file: &str) -> crate::error::Result<Vec<Command>> {
+pub fn parse_file(file: &str) -> error::Result<Vec<Command>> {
CommandParser::parse(Rule::file, file).map_err(convert_error).map(|pairs| pairs.into_iter().map(parse_expr).collect())
}
#[cfg(test)]
mod tests {
- use kernel::term::builders::*;
- use Builder::*;
+
+ use error::{Error, ErrorKind};
+ use kernel::memory::term::builder as term;
+ use term::Builder::*;
use super::Command::*;
use super::*;
/// Error messages
- const COMMAND_ERR: &str = "expected def var := term, def var : term := term, check term : term, check term, eval term, import path_to_file, or search var";
- const TERM_ERR: &str = "expected variable, abstraction, dependent product, application, product, Prop, or Type";
- const SIMPLE_TERM_ERR: &str = "expected variable, abstraction, Prop, or Type";
- const UNIVERSE_ERR: &str = "expected universe level, variable, abstraction, Prop, or Type";
+ const COMMAND_ERR: &str = "expected def var := term, def var : term := term, def decl.{ vars, ... } := term, def decl.{ vars, ... } : term := term, check term : term, check term, eval term, import path_to_file, or search var";
+ const TERM_ERR: &str = "expected variable, abstraction, dependent product, application, product, Prop, Type, or Sort";
+ const SIMPLE_TERM_ERR: &str = "expected variable, abstraction, Prop, Type, Sort, or universe argument";
+ const UNIVERSE_ERR: &str = "expected number, variable, abstraction, Prop, Type, Sort, plus, max, or imax";
#[test]
fn failure_universe_level() {
@@ -230,7 +333,25 @@ mod tests {
#[test]
fn successful_define_with_type_annotation() {
- assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(0)), Prop)));
+ assert_eq!(parse_line("def x : Type := Prop"), Ok(Define("x", Some(Type(box level::Builder::Const(0))), Prop)));
+ }
+
+ #[test]
+ fn successful_declare_with_type_annotation() {
+ assert_eq!(
+ parse_line("def x.{u} : Type u := foo.{u}"),
+ Ok(Declaration(
+ "x",
+ Some(declaration::Builder::Decl(box Type(box level::Builder::Var("u")), ["u"].to_vec())),
+ declaration::Builder::Decl(
+ box kernel::memory::term::builder::Builder::Decl(box declaration::InstantiatedBuilder::Var(
+ "foo",
+ [level::Builder::Var("u")].to_vec()
+ )),
+ ["u"].to_vec()
+ )
+ ))
+ );
}
#[test]
@@ -254,9 +375,14 @@ mod tests {
assert_eq!(parse_line("def x := Prop"), Ok(Define("x", None, Prop)));
}
+ #[test]
+ fn successful_declare() {
+ assert_eq!(parse_line("def x.{} := Prop"), Ok(Declaration("x", None, declaration::Builder::Decl(box Prop, Vec::new()))));
+ }
+
#[test]
fn successful_checktype() {
- assert_eq!(parse_line("check Prop : Type"), Ok(CheckType(Prop, Type(0))));
+ assert_eq!(parse_line("check Prop : Type"), Ok(CheckType(Prop, Type(box level::Builder::Const(0)))));
}
#[test]
@@ -264,6 +390,11 @@ mod tests {
assert_eq!(parse_line("check Prop"), Ok(GetType(Prop)));
}
+ #[test]
+ fn successful_gettype_sort() {
+ assert_eq!(parse_line("check Sort"), Ok(GetType(Sort(box level::Builder::Const(0)))));
+ }
+
#[test]
fn successful_var() {
assert_eq!(parse_line("check fun A: Prop => A"), Ok(GetType(Abs("A", Box::new(Prop), Box::new(Var("A"))))));
@@ -271,9 +402,25 @@ mod tests {
#[test]
fn successful_type() {
- assert_eq!(parse_line("check Type"), Ok(GetType(Type(0))));
- assert_eq!(parse_line("check Type 0"), Ok(GetType(Type(0))));
- assert_eq!(parse_line("check Type 1"), Ok(GetType(Type(1))));
+ assert_eq!(parse_line("check Type"), Ok(GetType(Type(box level::Builder::Const(0)))));
+ assert_eq!(parse_line("check Type 0"), Ok(GetType(Type(box level::Builder::Const(0)))));
+ assert_eq!(parse_line("check Type 1"), Ok(GetType(Type(box level::Builder::Const(1)))));
+ }
+
+ #[test]
+ fn successful_sort() {
+ assert_eq!(parse_line("check Sort"), Ok(GetType(Sort(box level::Builder::Const(0)))));
+ assert_eq!(parse_line("check Sort 0"), Ok(GetType(Sort(box level::Builder::Const(0)))));
+ assert_eq!(parse_line("check Sort 1"), Ok(GetType(Sort(box level::Builder::Const(1)))));
+ assert_eq!(parse_line("check Sort (0 + 1)"), Ok(GetType(Sort(box level::Builder::Plus(box level::Builder::Const(0), 1)))));
+ assert_eq!(
+ parse_line("check Sort max 0 0"),
+ Ok(GetType(Sort(box level::Builder::Max(box level::Builder::Const(0), box level::Builder::Const(0)))))
+ );
+ assert_eq!(
+ parse_line("check Sort imax 0 0"),
+ Ok(GetType(Sort(box level::Builder::IMax(box level::Builder::Const(0), box level::Builder::Const(0)))))
+ );
}
#[test]
@@ -296,7 +443,11 @@ mod tests {
#[test]
fn successful_dprod() {
- let res = Ok(GetType(Prod("x", Box::new(Type(0)), Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))))));
+ let res = Ok(GetType(Prod(
+ "x",
+ Box::new(Type(box level::Builder::Const(0))),
+ Box::new(Prod("y", Box::new(Type(box level::Builder::Const(1))), Box::new(Var("x")))),
+ )));
assert_eq!(parse_line("check (x:Type) -> (y:Type 1) -> x"), res);
assert_eq!(parse_line("check (x:Type) -> ((y:Type 1) -> x)"), res);
}
@@ -383,13 +534,21 @@ mod tests {
#[test]
fn parenthesis_in_prod() {
- let res = Prod("_", Box::new(Type(0)), Box::new(Prod("_", Box::new(Type(1)), Box::new(Type(2)))));
+ let res = Prod(
+ "_",
+ Box::new(Type(box level::Builder::Const(0))),
+ Box::new(Prod("_", Box::new(Type(box level::Builder::Const(1))), Box::new(Type(box level::Builder::Const(2))))),
+ );
assert_eq!(parse_line("check (((Type))) -> (((Type 1 -> Type 2)))"), Ok(GetType(res)));
}
#[test]
fn parenthesis_in_dprod() {
- let res = Prod("x", Box::new(Type(0)), Box::new(Prod("y", Box::new(Type(1)), Box::new(Var("x")))));
+ let res = Prod(
+ "x",
+ Box::new(Type(box level::Builder::Const(0))),
+ Box::new(Prod("y", Box::new(Type(box level::Builder::Const(1))), Box::new(Var("x")))),
+ );
assert_eq!(parse_line("check (((x:Type))) -> ((((y:Type 1) -> x)))"), Ok(GetType(res)));
}
diff --git a/parser/src/term.pest b/parser/src/term.pest
index fc78bc41..c0250907 100644
--- a/parser/src/term.pest
+++ b/parser/src/term.pest
@@ -3,14 +3,16 @@ COMMENT = _{ "//" ~ (!"\n" ~ ANY)* }
number = @{ ASCII_DIGIT+ }
filename = @{ ( ASCII_ALPHANUMERIC | PUNCTUATION )+ }
string = @{ !keywords ~ ASCII_ALPHA ~ ( "_" | ASCII_ALPHANUMERIC )* }
-keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" ) ~ !ASCII_ALPHANUMERIC }
+keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" | "Sort" ) ~ !ASCII_ALPHANUMERIC }
eoi = _{ !ANY }
-Term = _{ Abs | dProd | Prod | App | Var | Prop | Type | "(" ~ Term ~ ")" }
-term_prod = _{ App | Abs | dProd | Var | Prop | Type | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
-term_app = _{ Abs | Var | Prop | Type | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" }
-term_dprod = _{ App | Abs | Prod | dProd | Var | Prop | Type | "(" ~ term_dprod ~ ")" }
-term_abs = _{ App | Abs | Prod | dProd | Var | Prop | Type | "(" ~ term_abs ~ ")" }
+
+
+Term = _{ Abs | dProd | Prod | App | VarDecl | Var | Prop | Type | Sort | "(" ~ Term ~ ")" }
+term_prod = _{ App | Abs | dProd | VarDecl | Var | Prop | Type | Sort | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
+term_app = _{ Abs | VarDecl | Var | Prop | Type | Sort | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" }
+term_dprod = _{ App | Abs | Prod | dProd | VarDecl | Var | Prop | Type | Sort | "(" ~ term_dprod ~ ")" }
+term_abs = _{ App | Abs | Prod | dProd | VarDecl | Var | Prop | Type | Sort | "(" ~ term_abs ~ ")" }
Abs = { ( "fun" ~ ( arg_abs_par ~ ( "," ~ arg_abs_par )* ) ~ "=>" ~ Term ) }
arg_abs_par = _{ arg_abs | "(" ~ arg_abs_par ~ ")" }
@@ -22,19 +24,33 @@ arg_dprod = { string+ ~ ":" ~ term_dprod }
App = { term_app ~ term_app+ }
Prod = { term_prod ~ ( "->" ~ term_prod )+ }
-
Prop = { "Prop" }
-Type = { "Type(" ~ number ~ ")" | "Type" ~ number? }
+
+Type = { "Type" ~ univ? }
+Sort = { "Sort" ~ univ? }
+univ = _{ Plus | Max | IMax | Num | string | "(" ~ univ ~ ")" }
+univ_plus = _{ Max | IMax | Num | string | "(" ~ univ ~ ")" }
+Num = { number }
+Plus = { univ_plus ~ ( "+" ~ number )+ }
+Max = { ( "max" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "max" ~ univ ~ univ ) }
+IMax = { ( "imax" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "imax" ~ univ ~ univ ) }
+
Var = { string }
+VarDecl = ${ string ~ arg_univ }
+stringDecl = ${ string ~ univ_decl }
+
+arg_univ = {".{" ~ (univ ~ ("," ~ univ)* )? ~ "}"}
+univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"}
-Command = _{ Define | CheckType | GetType | DefineCheckType | Eval | ImportFile | Search}
+Command = _{ Define | Declaration | DeclarationCheckType | CheckType | GetType | DefineCheckType | Eval | ImportFile | Search}
Define = { "def" ~ string ~ ":=" ~ Term }
DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term }
+Declaration = { "def" ~ stringDecl ~ ":=" ~ Term }
+DeclarationCheckType = { "def" ~ stringDecl ~ ":" ~ Term ~ ":=" ~ Term }
CheckType = { "check" ~ Term ~ ":" ~ Term }
GetType = { "check" ~ Term }
Eval = { "eval" ~ Term }
ImportFile = { "import" ~ filename* }
Search = { "search" ~ string }
-
command = _{SOI ~ Command ~ eoi }
file = _{ SOI ~ Command* ~ eoi }
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index eba1b916..89a00c19 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -5,7 +5,8 @@ use std::path::PathBuf;
use colored::Colorize;
use derive_more::Display;
use kernel::location::Location;
-use kernel::term::arena::{Arena, Term};
+use kernel::memory::arena::Arena;
+use kernel::memory::term::Term;
use parser::command::Command;
use parser::{parse_file, parse_line};
use path_absolutize::Absolutize;
@@ -131,50 +132,65 @@ impl<'arena> Evaluator {
.map(|_| None)
}
- fn process<'build>(
+ fn process(
&mut self,
arena: &mut Arena<'arena>,
- command: &Command<'build>,
+ command: &Command,
importing: &mut Vec<PathBuf>,
) -> Result<'arena, Option<Term<'arena>>> {
match command {
- Command::Define(s, None, term) => {
- let term = term.realise(arena)?;
- if arena.get_binding(s).is_none() {
- arena.infer(term)?;
- arena.bind(s, term);
- Ok(None)
- } else {
- Err(Toplevel(Error {
+ Command::Define(s, ty, term) => {
+ if arena.get_binding(s).is_some() {
+ return Err(Toplevel(Error {
kind: ErrorKind::BoundVariable(s.to_string()),
location: Location::default(), // TODO (see #38)
- }))
+ }));
}
- },
-
- Command::Define(s, Some(t), term) => {
let term = term.realise(arena)?;
- let t = t.realise(arena)?;
- arena.check(term, t)?;
+ match ty {
+ None => {
+ term.infer(arena)?;
+ },
+ Some(ty) => term.check(ty.realise(arena)?, arena)?,
+ }
arena.bind(s, term);
Ok(None)
},
+ Command::Declaration(s, ty, decl) => {
+ if arena.get_binding_decl(s).is_some() {
+ return Err(Toplevel(Error {
+ kind: ErrorKind::BoundVariable(s.to_string()),
+ location: Location::default(), // TODO (see #38)
+ }));
+ }
+ let decl = decl.realise(arena)?;
+ match ty {
+ None => {
+ decl.infer(arena)?;
+ },
+ Some(ty) => decl.check(ty.realise(arena)?, arena)?,
+ }
+ arena.bind_decl(s, decl);
+ Ok(None)
+ },
+
Command::CheckType(t1, t2) => {
let t1 = t1.realise(arena)?;
let t2 = t2.realise(arena)?;
- arena.check(t1, t2)?;
+ t1.check(t2, arena)?;
Ok(None)
},
Command::GetType(t) => {
let t = t.realise(arena)?;
- Ok(arena.infer(t).map(Some)?)
+ Ok(t.infer(arena).map(Some)?)
},
Command::Eval(t) => {
let t = t.realise(arena)?;
- Ok(Some(arena.normal_form(t)))
+ let _ = t.infer(arena)?;
+ Ok(Some(t.normal_form(arena)))
},
Command::Search(s) => Ok(arena.get_binding(s)), // TODO (see #49)
diff --git a/proost/src/main.rs b/proost/src/main.rs
index 08d25afb..cd141e10 100644
--- a/proost/src/main.rs
+++ b/proost/src/main.rs
@@ -53,7 +53,7 @@ fn main() -> Result<'static, ()> {
rl.bind_sequence(KeyEvent::from('\t'), EventHandler::Conditional(Box::new(TabEventHandler)));
rl.bind_sequence(KeyEvent(KeyCode::Enter, Modifiers::ALT), EventHandler::Simple(Cmd::Newline));
- kernel::term::arena::use_arena(|arena| {
+ kernel::memory::arena::use_arena(|arena| {
let current_path = current_dir()?;
let mut evaluator = Evaluator::new(current_path, args.verbose);
--
GitLab