From 9c5ddbc18bef81d66a00d25d9960909532ddbf0a Mon Sep 17 00:00:00 2001
From: loutr <l.ta-ma@proton.me>
Date: Sun, 13 Nov 2022 16:58:37 +0100
Subject: [PATCH] chore(file structure): reorganised the file structure of
arena- or term-related functions
---
kernel/src/command.rs | 3 +-
kernel/src/error.rs | 6 +-
kernel/src/lib.rs | 5 +-
kernel/src/term.rs | 732 ------------------------------------
kernel/src/term/arena.rs | 237 ++++++++++++
kernel/src/term/builders.rs | 167 ++++++++
kernel/src/term/calculus.rs | 356 ++++++++++++++++++
kernel/src/term/mod.rs | 3 +
kernel/src/type_checker.rs | 10 +-
kernel/tests/and.rs | 8 +-
10 files changed, 778 insertions(+), 749 deletions(-)
delete mode 100644 kernel/src/term.rs
create mode 100644 kernel/src/term/arena.rs
create mode 100644 kernel/src/term/builders.rs
create mode 100644 kernel/src/term/calculus.rs
create mode 100644 kernel/src/term/mod.rs
diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 23c71273..7a904d4e 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -1,6 +1,5 @@
use crate::error::Result;
-use crate::term::Arena;
-use crate::term::Term;
+use crate::{Arena, Term};
#[derive(Debug, Eq, PartialEq)]
pub enum Command<'arena> {
diff --git a/kernel/src/error.rs b/kernel/src/error.rs
index 5d3d2adb..055bf348 100644
--- a/kernel/src/error.rs
+++ b/kernel/src/error.rs
@@ -1,7 +1,9 @@
-use crate::term::{DefinitionError, Term};
-use crate::type_checker::TypeCheckerError;
use derive_more::{Display, From};
+use crate::term::arena::Term;
+use crate::term::builders::extern_::DefinitionError;
+use crate::type_checker::TypeCheckerError;
+
/// Type representing kernel errors.
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub struct Error<'arena> {
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index 4457e045..6433072e 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -6,9 +6,10 @@
mod command;
mod error;
mod location;
-pub mod term;
+mod term;
mod type_checker;
pub use self::command::Command;
pub use self::location::{Location, Position};
-pub use self::term::Term;
+pub use self::term::arena::{use_arena, Arena, Term};
+pub use self::term::builders::extern_ as builders;
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
deleted file mode 100644
index 4148c7bc..00000000
--- a/kernel/src/term.rs
+++ /dev/null
@@ -1,732 +0,0 @@
-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 im_rc::hashmap::HashMap as ImHashMap;
-use num_bigint::BigUint;
-
-use crate::error::{Error, ResultTerm};
-
-#[derive(
- Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord, Hash,
-)]
-pub struct DeBruijnIndex(usize);
-
-#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord, Hash)]
-pub struct UniverseLevel(BigUint);
-
-#[non_exhaustive]
-#[derive(Clone, Debug, Display, Eq, PartialEq)]
-pub enum DefinitionError<'arena> {
- #[display(fmt = "unknown identifiant {}", _0)]
- ConstNotFound(&'arena str),
-}
-
-pub struct Arena<'arena> {
- alloc: &'arena Bump,
- _phantom: PhantomData<*mut &'arena ()>,
-
- hashcons: HashSet<&'arena Node<'arena>>,
- named_terms: HashMap<&'arena str, Term<'arena>>,
-
- mem_subst: HashMap<(Term<'arena>, Term<'arena>, DeBruijnIndex), Term<'arena>>,
- // a shift hashmap may also be added when the is_certainly_closed also is
-}
-
-#[derive(Clone, Copy, Display, Eq)]
-#[display(fmt = "{}", "_0.payload")]
-// PhantomData is a marker to ensure invariance over the 'arena lifetime.
-pub struct Term<'arena>(&'arena Node<'arena>, PhantomData<*mut &'arena ()>);
-
-// the rest of the struct is very verbose and useless for debugging
-impl<'arena> Debug for Term<'arena> {
- fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
- self.0.payload.fmt(f)
- }
-}
-
-// no name storage here: meaning consts are known and can be found, but no pretty printing is
-// possible so far.
-#[derive(Debug)]
-struct Node<'arena> {
- payload: Payload<'arena>,
-
- head_normal_form: OnceCell<Term<'arena>>,
- type_: OnceCell<Term<'arena>>,
- //
- // is_certainly_closed: boolean underapproximation of whether a term is closed, which can
- // greatly improve performance in shifting
-}
-
-#[derive(Clone, Debug, Display, Eq, PartialEq, Hash)]
-pub enum Payload<'arena> {
- #[display(fmt = "{}", _0)]
- Var(DeBruijnIndex, Term<'arena>),
-
- #[display(fmt = "Prop")]
- Prop,
-
- #[display(fmt = "Type {}", _0)]
- Type(UniverseLevel),
-
- #[display(fmt = "{} {}", _0, _1)]
- App(Term<'arena>, Term<'arena>),
-
- #[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
- Abs(Term<'arena>, Term<'arena>),
-
- #[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
- Prod(Term<'arena>, Term<'arena>),
-}
-
-use Payload::*;
-
-/// (TODO PRECISE DOCUMENTATION) make use of unicity invariant to speed up equality test
-impl<'arena> PartialEq<Term<'arena>> for Term<'arena> {
- fn eq(&self, x: &Term<'arena>) -> bool {
- std::ptr::eq(self.0, x.0)
- }
-}
-
-/// (TODO PRECISE DOCUMENTATION) make use of unicity invariant to speed up equality test
-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
- }
-}
-
-impl<'arena> Eq for Node<'arena> {}
-
-/// (TODO PRECISE DOCUMENTATION) Only the payload matters and caracterises the value. Changing
-/// OnceCells is *guaranteed* to have no impact on that.
-impl<'arena> Hash for Node<'arena> {
- fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
- self.payload.hash(state);
- }
-}
-
-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 extern_build::Generator as ExternGenerator;
-use intern_build::Generator;
-
-impl<'arena> Arena<'arena> {
- /// (TODO DOC.) Allocate a new memory arena.
- fn new(alloc: &'arena Bump) -> Self {
- Arena {
- alloc,
- _phantom: PhantomData,
-
- hashcons: HashSet::new(),
- named_terms: HashMap::new(),
-
- mem_subst: HashMap::new(),
- }
- }
-
- /// (TODO DOC.) there are concurrent designs here: either hashcons take a Node and functions
- /// which use it immediatly intend to compute the type and/or WHNF of the term, or this is
- /// postponed and computed lazily. This iteration chooses the second approach.
- fn hashcons(&mut self, n: Payload<'arena>) -> Term<'arena> {
- let nn = Node {
- payload: n,
- head_normal_form: OnceCell::new(),
- type_: OnceCell::new(),
- };
- match self.hashcons.get(&nn) {
- Some(addr) => Term(addr, PhantomData),
- None => {
- let addr = self.alloc.alloc(nn);
- self.hashcons.insert(addr);
- Term(addr, PhantomData)
- }
- }
- }
-
- pub(crate) fn var(&mut self, index: DeBruijnIndex, type_: Term<'arena>) -> Term<'arena> {
- self.hashcons(Var(index, type_))
- }
-
- pub(crate) fn prop(&mut self) -> Term<'arena> {
- self.hashcons(Prop)
- }
-
- pub(crate) fn type_(&mut self, level: UniverseLevel) -> Term<'arena> {
- self.hashcons(Type(level))
- }
-
- pub(crate) fn type_usize(&mut self, level: usize) -> Term<'arena> {
- self.hashcons(Type(BigUint::from(level).into()))
- }
-
- pub(crate) fn app(&mut self, u1: Term<'arena>, u2: Term<'arena>) -> Term<'arena> {
- self.hashcons(App(u1, u2))
- }
-
- pub(crate) fn abs(&mut self, arg_type: Term<'arena>, u: Term<'arena>) -> Term<'arena> {
- self.hashcons(Abs(arg_type, u))
- }
-
- pub(crate) fn prod(&mut self, arg_type: Term<'arena>, u: Term<'arena>) -> Term<'arena> {
- self.hashcons(Prod(arg_type, u))
- }
-
- pub(crate) fn build<F: Generator<'arena>>(&mut self, f: F) -> Term<'arena> {
- f(self)
- }
-
- #[inline]
- pub fn build_from_extern<F: ExternGenerator<'arena>>(&mut self, f: F) -> ResultTerm<'arena> {
- f(self, &ImHashMap::new(), 0.into())
- }
-
- pub fn bind(&mut self, name: &'arena str, t: Term<'arena>) {
- self.named_terms.insert(name, t);
- }
-
- /// 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,
- }
- }
-
- 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,
- }
- }
-
- pub(crate) fn substitute(
- &mut self,
- lhs: Term<'arena>,
- rhs: Term<'arena>,
- depth: usize,
- ) -> Term<'arena> {
- match self.mem_subst.get(&(lhs, rhs, depth.into())) {
- Some(res) => *res,
- None => {
- let res = match *lhs {
- Var(i, _) if i == depth.into() => self.shift(rhs, depth - 1, 0),
- Var(i, type_) if i > depth.into() => self.var(i - 1.into(), type_),
- App(l, r) => {
- let l = self.substitute(l, rhs, depth);
- let r = self.substitute(r, rhs, depth);
- self.app(l, r)
- }
- Abs(arg_type, body) => {
- let arg_type = self.substitute(arg_type, rhs, depth);
- let body = self.substitute(body, rhs, depth + 1);
- self.abs(arg_type, body)
- }
- Prod(arg_type, body) => {
- let arg_type = self.substitute(arg_type, rhs, depth);
- let body = self.substitute(body, rhs, depth + 1);
- self.prod(arg_type, body)
- }
- _ => lhs,
- };
- self.mem_subst.insert((lhs, rhs, depth.into()), res);
- res
- }
- }
- }
-
- /// Returns the normal form of a term in a given environment.
- ///
- /// 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 in a given environment.
- pub fn whnf(&mut self, t: Term<'arena>) -> Term<'arena> {
- t.get_whnf_or_init(|| match *t {
- App(t1, t2) => {
- let t1 = self.whnf(t1);
- match *t1 {
- Abs(_, _) => {
- let t = self.app(t1, t2);
- let t = self.beta_reduction(t);
- self.whnf(t)
- }
- _ => t,
- }
- }
- _ => t,
- })
- }
-}
-
-impl<'arena> Term<'arena> {
- pub(crate) fn into(self) -> impl Generator<'arena> {
- move |_: &mut Arena<'arena>| self
- }
-
- 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)
- }
-
- 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()
- }
-}
-
-impl<'arena> Deref for Term<'arena> {
- type Target = Payload<'arena>;
-
- fn deref(&self) -> &Self::Target {
- &self.0.payload
- }
-}
-
-pub(crate) mod intern_build {
- use super::*;
-
- pub(crate) trait Generator<'arena> = FnOnce(&mut Arena<'arena>) -> Term<'arena>;
-
- #[inline]
- pub(crate) fn prop<'arena>() -> impl Generator<'arena> {
- |env: &mut Arena<'arena>| env.prop()
- }
-
- #[inline]
- pub(crate) fn type_<'arena>(level: UniverseLevel) -> impl Generator<'arena> {
- move |env: &mut Arena<'arena>| env.type_(level)
- }
-
- pub(crate) fn var<'arena, F: Generator<'arena>>(
- index: DeBruijnIndex,
- type_: F,
- ) -> impl Generator<'arena> {
- move |env: &mut Arena<'arena>| {
- let ty = type_(env);
- env.var(index, ty)
- }
- }
-
- #[inline]
- pub(crate) fn app<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl Generator<'arena> {
- |env: &mut Arena<'arena>| {
- let u1 = u1(env);
- let u2 = u2(env);
- env.app(u1, u2)
- }
- }
-
- #[inline]
- pub(crate) fn abs<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl Generator<'arena> {
- |env: &mut Arena<'arena>| {
- let u1 = u1(env);
- let u2 = u2(env);
- env.abs(u1, u2)
- }
- }
-
- #[inline]
- pub(crate) fn prod<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl Generator<'arena> {
- |env: &mut Arena<'arena>| {
- let u1 = u1(env);
- let u2 = u2(env);
- env.prod(u1, u2)
- }
- }
-}
-
-/// These functions are available publicly, to the attention of the parser. They manipulate
-/// objects with a type morally equal to (Env -> Term), where Env is a working environment used
-/// in term construction from the parser.
-/// This is done as a way to elengantly keep the logic encapsulated in the kernel, but let the
-/// parser itself explore the term.
-pub mod extern_build {
- use super::*;
-
- pub type Environment<'arena> = ImHashMap<&'arena str, (DeBruijnIndex, Term<'arena>)>;
- pub trait Generator<'arena> =
- FnOnce(&mut Arena<'arena>, &Environment<'arena>, DeBruijnIndex) -> ResultTerm<'arena>;
-
- #[inline]
- pub fn var<'arena>(name: &'arena str) -> impl Generator<'arena> {
- move |arena: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
- env.get(name)
- .map(|(bind_depth, term)| {
- // maybe find a way to make this call efficiently lazy
- let var_type = arena.shift(*term, usize::from(depth - *bind_depth), 0);
- arena.var(depth - *bind_depth, var_type)
- })
- .or_else(|| arena.named_terms.get(name).copied())
- .ok_or(Error {
- kind: DefinitionError::ConstNotFound(name).into(),
- })
- }
- }
-
- #[inline]
- pub fn prop<'arena>() -> impl Generator<'arena> {
- |arena: &mut Arena<'arena>, _: &Environment<'arena>, _| Ok(arena.prop())
- }
-
- #[inline]
- pub fn type_<'arena>(level: UniverseLevel) -> impl Generator<'arena> {
- move |arena: &mut Arena<'arena>, _: &Environment<'arena>, _| Ok(arena.type_(level))
- }
-
- #[inline]
- pub fn app<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
- u1: F1,
- u2: F2,
- ) -> impl Generator<'arena> {
- |arena: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
- let u1 = u1(arena, env, depth)?;
- let u2 = u2(arena, env, depth)?;
- Ok(arena.app(u1, u2))
- }
- }
-
- #[inline]
- pub fn abs<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
- name: &'arena str,
- arg_type: F1,
- body: F2,
- ) -> impl Generator<'arena> {
- move |arena: &mut Arena<'arena>, env: &Environment<'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))
- }
- }
-
- #[inline]
- pub fn prod<'arena, F1: Generator<'arena>, F2: Generator<'arena>>(
- name: &'arena str,
- arg_type: F1,
- body: F2,
- ) -> impl Generator<'arena> {
- move |arena: &mut Arena<'arena>, env: &Environment<'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))
- }
- }
-}
-
-#[cfg(test)]
-mod tests {
- // /!\ most of these tests are on ill-typed terms and should not be used for further testings
- use super::intern_build::*;
- use super::*;
-
- #[test]
- fn simple_subst() {
- use_arena(|arena| {
- // λx.(λy.x y) x
- let term = arena.build(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(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(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(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(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(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(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(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(abs(
- prop(),
- abs(
- prop(),
- app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())),
- ),
- ));
-
- // λa.λb.b
- let term_step_7 = arena.build(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(prod(prop(), var(1.into(), prop())));
- let term = arena.build(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(prod(
- prop(),
- app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
- ));
- let reduced = arena.build(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(abs(
- prop(),
- app(
- var(1.into(), prop()),
- app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
- ),
- ));
- let reduced = arena.build(abs(
- prop(),
- app(var(1.into(), prop()), var(1.into(), prop())),
- ));
-
- assert_eq!(arena.beta_reduction(term), reduced);
- })
- }
-}
diff --git a/kernel/src/term/arena.rs b/kernel/src/term/arena.rs
new file mode 100644
index 00000000..f81c9a6a
--- /dev/null
+++ b/kernel/src/term/arena.rs
@@ -0,0 +1,237 @@
+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 im_rc::hashmap::HashMap as ImHashMap;
+use num_bigint::BigUint;
+
+use crate::error::ResultTerm;
+
+#[derive(
+ Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord, Hash,
+)]
+pub struct DeBruijnIndex(usize);
+
+#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord, Hash)]
+pub struct UniverseLevel(BigUint);
+
+pub struct Arena<'arena> {
+ alloc: &'arena Bump,
+ _phantom: PhantomData<*mut &'arena ()>,
+
+ hashcons: HashSet<&'arena Node<'arena>>,
+ named_terms: HashMap<&'arena str, Term<'arena>>,
+
+ mem_subst: HashMap<(Term<'arena>, Term<'arena>, usize), Term<'arena>>,
+ // a shift hashmap may also be added when the is_certainly_closed also is
+}
+
+#[derive(Clone, Copy, Display, Eq)]
+#[display(fmt = "{}", "_0.payload")]
+// PhantomData is a marker to ensure invariance over the 'arena lifetime.
+pub struct Term<'arena>(&'arena Node<'arena>, PhantomData<*mut &'arena ()>);
+
+// the rest of the struct is very verbose and useless for debugging
+impl<'arena> Debug for Term<'arena> {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+ self.0.payload.fmt(f)
+ }
+}
+
+// no name storage here: meaning consts are known and can be found, but no pretty printing is
+// possible so far.
+#[derive(Debug)]
+struct Node<'arena> {
+ payload: Payload<'arena>,
+
+ head_normal_form: OnceCell<Term<'arena>>,
+ type_: OnceCell<Term<'arena>>,
+ //
+ // is_certainly_closed: boolean underapproximation of whether a term is closed, which can
+ // greatly improve performance in shifting
+}
+
+#[derive(Clone, Debug, Display, Eq, PartialEq, Hash)]
+pub enum Payload<'arena> {
+ #[display(fmt = "{}", _0)]
+ Var(DeBruijnIndex, Term<'arena>),
+
+ #[display(fmt = "Prop")]
+ Prop,
+
+ #[display(fmt = "Type {}", _0)]
+ Type(UniverseLevel),
+
+ #[display(fmt = "{} {}", _0, _1)]
+ App(Term<'arena>, Term<'arena>),
+
+ #[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
+ Abs(Term<'arena>, Term<'arena>),
+
+ #[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
+ Prod(Term<'arena>, Term<'arena>),
+}
+
+/// (TODO PRECISE DOCUMENTATION) make use of unicity invariant to speed up equality test
+impl<'arena> PartialEq<Term<'arena>> for Term<'arena> {
+ fn eq(&self, x: &Term<'arena>) -> bool {
+ std::ptr::eq(self.0, x.0)
+ }
+}
+
+/// (TODO PRECISE DOCUMENTATION) make use of unicity invariant to speed up equality test
+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
+ }
+}
+
+impl<'arena> Eq for Node<'arena> {}
+
+/// (TODO PRECISE DOCUMENTATION) Only the payload matters and caracterises the value. Changing
+/// OnceCells is *guaranteed* to have no impact on that.
+impl<'arena> Hash for Node<'arena> {
+ fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+ self.payload.hash(state);
+ }
+}
+
+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 super::builders::extern_::Builder;
+use Payload::*;
+
+impl<'arena> Arena<'arena> {
+ /// (TODO DOC.) Allocate a new memory arena.
+ fn new(alloc: &'arena Bump) -> Self {
+ Arena {
+ alloc,
+ _phantom: PhantomData,
+
+ hashcons: HashSet::new(),
+ named_terms: HashMap::new(),
+
+ mem_subst: HashMap::new(),
+ }
+ }
+
+ pub fn bind(&mut self, name: &'arena str, t: Term<'arena>) {
+ self.named_terms.insert(name, t);
+ }
+
+ pub fn get_binding(&self, name: &str) -> Option<Term<'arena>> {
+ self.named_terms.get(name).copied()
+ }
+
+ /// (TODO DOC.) there are concurrent designs here: either hashcons take a Node and functions
+ /// which use it immediatly intend to compute the type and/or WHNF of the term, or this is
+ /// postponed and computed lazily. This iteration chooses the second approach.
+ fn hashcons(&mut self, n: Payload<'arena>) -> Term<'arena> {
+ let nn = Node {
+ payload: n,
+ head_normal_form: OnceCell::new(),
+ type_: OnceCell::new(),
+ };
+ match self.hashcons.get(&nn) {
+ Some(addr) => Term(addr, PhantomData),
+ None => {
+ let addr = self.alloc.alloc(nn);
+ self.hashcons.insert(addr);
+ Term(addr, PhantomData)
+ }
+ }
+ }
+
+ pub(crate) fn var(&mut self, index: DeBruijnIndex, type_: Term<'arena>) -> Term<'arena> {
+ self.hashcons(Var(index, type_))
+ }
+
+ pub(crate) fn prop(&mut self) -> Term<'arena> {
+ self.hashcons(Prop)
+ }
+
+ pub(crate) fn type_(&mut self, level: UniverseLevel) -> Term<'arena> {
+ self.hashcons(Type(level))
+ }
+
+ pub(crate) fn type_usize(&mut self, level: usize) -> Term<'arena> {
+ self.hashcons(Type(BigUint::from(level).into()))
+ }
+
+ pub(crate) fn app(&mut self, u1: Term<'arena>, u2: Term<'arena>) -> Term<'arena> {
+ self.hashcons(App(u1, u2))
+ }
+
+ pub(crate) fn abs(&mut self, arg_type: Term<'arena>, u: Term<'arena>) -> Term<'arena> {
+ self.hashcons(Abs(arg_type, u))
+ }
+
+ pub(crate) fn prod(&mut self, arg_type: Term<'arena>, u: Term<'arena>) -> Term<'arena> {
+ self.hashcons(Prod(arg_type, u))
+ }
+
+ #[inline]
+ pub fn build_from_extern<F: Builder<'arena>>(&mut self, f: F) -> ResultTerm<'arena> {
+ f(self, &ImHashMap::new(), 0.into())
+ }
+
+ 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> {
+ 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)
+ }
+
+ 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()
+ }
+}
+
+impl<'arena> Deref for Term<'arena> {
+ type Target = Payload<'arena>;
+
+ fn deref(&self) -> &Self::Target {
+ &self.0.payload
+ }
+}
diff --git a/kernel/src/term/builders.rs b/kernel/src/term/builders.rs
new file mode 100644
index 00000000..e6c42ee9
--- /dev/null
+++ b/kernel/src/term/builders.rs
@@ -0,0 +1,167 @@
+use super::arena::{Arena, DeBruijnIndex, Term, UniverseLevel};
+
+#[cfg(test)]
+pub(crate) mod intern {
+ use super::*;
+
+ impl<'arena> Arena<'arena> {
+ pub(crate) fn build<F: Builder<'arena>>(&mut self, f: F) -> Term<'arena> {
+ f(self)
+ }
+ }
+
+ impl<'arena> Term<'arena> {
+ pub(crate) fn into(self) -> impl Builder<'arena> {
+ move |_: &mut Arena<'arena>| self
+ }
+ }
+
+ pub(crate) trait Builder<'arena> = FnOnce(&mut Arena<'arena>) -> Term<'arena>;
+
+ #[inline]
+ pub(crate) fn prop<'arena>() -> impl Builder<'arena> {
+ |env: &mut Arena<'arena>| env.prop()
+ }
+
+ #[inline]
+ pub(crate) fn type_<'arena>(level: UniverseLevel) -> impl Builder<'arena> {
+ move |env: &mut Arena<'arena>| env.type_(level)
+ }
+
+ #[inline]
+ pub(crate) fn var<'arena, F: Builder<'arena>>(
+ index: DeBruijnIndex,
+ type_: F,
+ ) -> impl Builder<'arena> {
+ move |env: &mut Arena<'arena>| {
+ let ty = type_(env);
+ env.var(index, ty)
+ }
+ }
+
+ #[inline]
+ pub(crate) fn app<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Builder<'arena> {
+ |env: &mut Arena<'arena>| {
+ let u1 = u1(env);
+ let u2 = u2(env);
+ env.app(u1, u2)
+ }
+ }
+
+ #[inline]
+ pub(crate) fn abs<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Builder<'arena> {
+ |env: &mut Arena<'arena>| {
+ let u1 = u1(env);
+ let u2 = u2(env);
+ env.abs(u1, u2)
+ }
+ }
+
+ #[inline]
+ pub(crate) fn prod<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Builder<'arena> {
+ |env: &mut Arena<'arena>| {
+ let u1 = u1(env);
+ let u2 = u2(env);
+ env.prod(u1, u2)
+ }
+ }
+}
+
+/// These functions are available publicly, to the attention of the parser. They manipulate
+/// objects with a type morally equal to (Env -> Term), where Env is a working environment used
+/// in term construction from the parser.
+/// This is done as a way to elengantly keep the logic encapsulated in the kernel, but let the
+/// parser itself explore the term.
+pub mod extern_ {
+ use derive_more::Display;
+ use im_rc::hashmap::HashMap as ImHashMap;
+
+ use super::*;
+ use crate::error::{Error, ResultTerm};
+
+ #[non_exhaustive]
+ #[derive(Clone, Debug, Display, Eq, PartialEq)]
+ pub enum DefinitionError<'arena> {
+ #[display(fmt = "unknown identifiant {}", _0)]
+ ConstNotFound(&'arena str),
+ }
+
+ pub type Environment<'arena> = ImHashMap<&'arena str, (DeBruijnIndex, Term<'arena>)>;
+ pub trait Builder<'arena> =
+ FnOnce(&mut Arena<'arena>, &Environment<'arena>, DeBruijnIndex) -> ResultTerm<'arena>;
+
+ #[inline]
+ pub fn var<'arena>(name: &'arena str) -> impl Builder<'arena> {
+ move |arena: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
+ env.get(name)
+ .map(|(bind_depth, term)| {
+ // maybe find a way to make this call efficiently lazy
+ 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(name).into(),
+ })
+ }
+ }
+
+ #[inline]
+ pub fn prop<'arena>() -> impl Builder<'arena> {
+ |arena: &mut Arena<'arena>, _: &Environment<'arena>, _| Ok(arena.prop())
+ }
+
+ #[inline]
+ pub fn type_<'arena>(level: UniverseLevel) -> impl Builder<'arena> {
+ move |arena: &mut Arena<'arena>, _: &Environment<'arena>, _| Ok(arena.type_(level))
+ }
+
+ #[inline]
+ pub fn app<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
+ u1: F1,
+ u2: F2,
+ ) -> impl Builder<'arena> {
+ |arena: &mut Arena<'arena>, env: &Environment<'arena>, depth| {
+ let u1 = u1(arena, env, depth)?;
+ let u2 = u2(arena, env, depth)?;
+ Ok(arena.app(u1, u2))
+ }
+ }
+
+ #[inline]
+ pub fn abs<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
+ name: &'arena str,
+ arg_type: F1,
+ body: F2,
+ ) -> impl Builder<'arena> {
+ move |arena: &mut Arena<'arena>, env: &Environment<'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))
+ }
+ }
+
+ #[inline]
+ pub fn prod<'arena, F1: Builder<'arena>, F2: Builder<'arena>>(
+ name: &'arena str,
+ arg_type: F1,
+ body: F2,
+ ) -> impl Builder<'arena> {
+ move |arena: &mut Arena<'arena>, env: &Environment<'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))
+ }
+ }
+}
diff --git a/kernel/src/term/calculus.rs b/kernel/src/term/calculus.rs
new file mode 100644
index 00000000..06b820cc
--- /dev/null
+++ b/kernel/src/term/calculus.rs
@@ -0,0 +1,356 @@
+use super::arena::{Arena, Payload, Term};
+use Payload::*;
+
+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,
+ }
+ }
+
+ 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,
+ }
+ }
+
+ pub(crate) fn substitute(
+ &mut self,
+ lhs: Term<'arena>,
+ rhs: Term<'arena>,
+ depth: usize,
+ ) -> Term<'arena> {
+ self.get_subst_or_init(&(lhs, rhs, depth), |arena| match *lhs {
+ Var(i, _) if i == depth.into() => arena.shift(rhs, depth - 1, 0),
+ Var(i, type_) if i > depth.into() => arena.var(i - 1.into(), type_),
+ App(l, r) => {
+ let l = arena.substitute(l, rhs, depth);
+ let r = arena.substitute(r, rhs, depth);
+ arena.app(l, r)
+ }
+ Abs(arg_type, body) => {
+ let arg_type = arena.substitute(arg_type, rhs, depth);
+ let body = arena.substitute(body, rhs, depth + 1);
+ arena.abs(arg_type, body)
+ }
+ Prod(arg_type, body) => {
+ let arg_type = arena.substitute(arg_type, rhs, depth);
+ let body = arena.substitute(body, rhs, depth + 1);
+ arena.prod(arg_type, body)
+ }
+ _ => lhs,
+ })
+ }
+
+ /// Returns the normal form of a term in a given environment.
+ ///
+ /// 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 in a given environment.
+ pub fn whnf(&mut self, t: Term<'arena>) -> Term<'arena> {
+ t.get_whnf_or_init(|| match *t {
+ App(t1, t2) => {
+ let t1 = self.whnf(t1);
+ match *t1 {
+ Abs(_, _) => {
+ let t = self.app(t1, t2);
+ let t = self.beta_reduction(t);
+ self.whnf(t)
+ }
+ _ => t,
+ }
+ }
+ _ => t,
+ })
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ // /!\ most of these tests are on ill-typed terms and should not be used for further testings
+ use super::super::arena::use_arena;
+ use super::super::builders::intern::*;
+
+ #[test]
+ fn simple_subst() {
+ use_arena(|arena| {
+ // λx.(λy.x y) x
+ let term = arena.build(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(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(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(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(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(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(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(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(abs(
+ prop(),
+ abs(
+ prop(),
+ app(abs(prop(), var(2.into(), prop())), var(2.into(), prop())),
+ ),
+ ));
+
+ // λa.λb.b
+ let term_step_7 = arena.build(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(prod(prop(), var(1.into(), prop())));
+ let term = arena.build(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(prod(
+ prop(),
+ app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
+ ));
+ let reduced = arena.build(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(abs(
+ prop(),
+ app(
+ var(1.into(), prop()),
+ app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())),
+ ),
+ ));
+ let reduced = arena.build(abs(
+ prop(),
+ app(var(1.into(), prop()), var(1.into(), prop())),
+ ));
+
+ assert_eq!(arena.beta_reduction(term), reduced);
+ })
+ }
+}
diff --git a/kernel/src/term/mod.rs b/kernel/src/term/mod.rs
new file mode 100644
index 00000000..1bfae37f
--- /dev/null
+++ b/kernel/src/term/mod.rs
@@ -0,0 +1,3 @@
+pub mod arena;
+pub mod builders;
+pub mod calculus;
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 65048a60..9e26ebbc 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -4,7 +4,7 @@ use derive_more::Display;
use num_bigint::BigUint;
use crate::error::{Error, Result, ResultTerm};
-use crate::term::{Arena, Payload, Term};
+use crate::term::arena::{Arena, Payload, Term};
use Payload::*;
#[derive(Clone, Debug, Display, Eq, PartialEq)]
@@ -174,10 +174,10 @@ impl<'arena> Arena<'arena> {
#[cfg(test)]
mod tests {
use super::*;
- use crate::term::intern_build::*;
- use crate::term::use_arena;
+ use crate::term::builders::intern::*;
+ use crate::use_arena;
- fn id<'arena>() -> impl Generator<'arena> {
+ fn id<'arena>() -> impl Builder<'arena> {
abs(prop(), var(1.into(), prop()))
}
@@ -297,7 +297,7 @@ mod tests {
// this test uses more intricate terms. In order to preserve some readibility,
// switching to extern_build, which is clearer.
fn typed_reduction_app_2() {
- use crate::term::extern_build::*;
+ use crate::term::builders::extern_::*;
use_arena(|arena| {
// (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λf.λg.f g)
let term = arena
diff --git a/kernel/tests/and.rs b/kernel/tests/and.rs
index d323aee2..e7630382 100644
--- a/kernel/tests/and.rs
+++ b/kernel/tests/and.rs
@@ -1,10 +1,6 @@
-#![feature(box_syntax)]
-
+use kernel::builders::*;
use kernel::Command::*;
-
-use kernel::term::extern_build::*;
-use kernel::term::use_arena;
-use kernel::term::Arena;
+use kernel::{use_arena, Arena};
fn use_and_arena<F, T>(f: F) -> T
where
--
GitLab