diff --git a/kernel/src/calculus/term.rs b/kernel/src/calculus/term.rs
index 14698eda19699c24c419a5d42d437e8212fdad4c..d23443807bbf3113dc67f1cd5ddbcc445ed16416 100644
--- a/kernel/src/calculus/term.rs
+++ b/kernel/src/calculus/term.rs
@@ -10,119 +10,119 @@ use crate::memory::declaration::InstantiatedDeclaration;
use crate::memory::level::Level;
use crate::memory::term::{Payload, Term};
-impl<'arena> Arena<'arena> {
+impl<'arena> Term<'arena> {
/// Apply one step of β-reduction, using the leftmost-outermost evaluation strategy.
- pub fn beta_reduction(&mut self, t: Term<'arena>) -> Term<'arena> {
- match *t {
+ pub fn beta_reduction(self, arena: &mut Arena<'arena>) -> Self {
+ match *self {
App(t1, t2) => match *t1 {
- Abs(_, t1) => self.substitute(t1, t2, 1),
+ Abs(_, t1) => t1.substitute(t2, 1, arena),
_ => {
- let t1_new = self.beta_reduction(t1);
+ let t1_new = t1.beta_reduction(arena);
if t1_new == t1 {
- let t2_new = self.beta_reduction(t2);
- self.app(t1, t2_new)
+ let t2_new = t2.beta_reduction(arena);
+ t1.app(t2_new, arena)
} else {
- self.app(t1_new, t2)
+ t1_new.app(t2, arena)
}
},
},
Abs(arg_type, body) => {
- let body = self.beta_reduction(body);
- self.abs(arg_type, body)
+ let body = body.beta_reduction(arena);
+ arg_type.abs(body, arena)
},
Prod(arg_type, body) => {
- let body = self.beta_reduction(body);
- self.prod(arg_type, body)
+ let body = body.beta_reduction(arena);
+ arg_type.prod(body, arena)
},
- _ => t,
+ _ => self,
}
}
/// 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_),
+ pub(crate) fn shift(self, offset: usize, depth: usize, arena: &mut Arena<'arena>) -> Self {
+ match *self {
+ Var(i, type_) if i > depth.into() => Term::var(i + offset.into(), type_, arena),
App(t1, t2) => {
- let t1 = self.shift(t1, offset, depth);
- let t2 = self.shift(t2, offset, depth);
- self.app(t1, t2)
+ let t1 = t1.shift(offset, depth, arena);
+ let t2 = t2.shift(offset, depth, arena);
+ t1.app(t2, arena)
},
Abs(arg_type, body) => {
- let arg_type = self.shift(arg_type, offset, depth);
- let body = self.shift(body, offset, depth + 1);
- self.abs(arg_type, body)
+ let arg_type = arg_type.shift(offset, depth, arena);
+ let body = body.shift(offset, depth + 1, arena);
+ arg_type.abs(body, arena)
},
Prod(arg_type, body) => {
- let arg_type = self.shift(arg_type, offset, depth);
- let body = self.shift(body, offset, depth + 1);
- self.prod(arg_type, body)
+ let arg_type = arg_type.shift(offset, depth, arena);
+ let body = body.shift(offset, depth + 1, arena);
+ arg_type.prod(body, arena)
},
- _ => t,
+ _ => self,
}
}
/// Returns the term `t` where all instances of the variable tracked by `depth` are substituted
/// with `sub`.
- pub(crate) fn substitute(&mut self, t: Term<'arena>, sub: Term<'arena>, depth: usize) -> Term<'arena> {
- self.get_subst_or_init(&(t, sub, depth), |arena| match *t {
- Var(i, _) if i == depth.into() => arena.shift(sub, depth - 1, 0),
- Var(i, type_) if i > depth.into() => arena.var(i - 1.into(), type_),
+ pub(crate) fn substitute(self, sub: Self, depth: usize, arena: &mut Arena<'arena>) -> Self {
+ arena.get_subst_or_init(&(self, sub, depth), |arena| match *self {
+ Var(i, _) if i == depth.into() => sub.shift(depth - 1, 0, arena),
+ Var(i, type_) if i > depth.into() => Term::var(i - 1.into(), type_, arena),
App(l, r) => {
- let l = arena.substitute(l, sub, depth);
- let r = arena.substitute(r, sub, depth);
- arena.app(l, r)
+ let l = l.substitute(sub, depth, arena);
+ let r = r.substitute(sub, depth, arena);
+ l.app(r, arena)
},
Abs(arg_type, body) => {
- let arg_type = arena.substitute(arg_type, sub, depth);
- let body = arena.substitute(body, sub, depth + 1);
- arena.abs(arg_type, body)
+ let arg_type = arg_type.substitute(sub, depth, arena);
+ let body = body.substitute(sub, depth + 1, arena);
+ arg_type.abs(body, arena)
},
Prod(arg_type, body) => {
- let arg_type = arena.substitute(arg_type, sub, depth);
- let body = arena.substitute(body, sub, depth + 1);
- arena.prod(arg_type, body)
+ let arg_type = arg_type.substitute(sub, depth, arena);
+ let body = body.substitute(sub, depth + 1, arena);
+ arg_type.prod(body, arena)
},
- _ => t,
+ _ => self,
})
}
/// TODO(docs)
- pub(crate) fn substitute_univs(&mut self, t: Term<'arena>, univs: &[Level<'arena>]) -> Term<'arena> {
- match *t {
+ pub(crate) fn substitute_univs(self, univs: &[Level<'arena>], arena: &mut Arena<'arena>) -> Self {
+ match *self {
Var(i, ty) => {
- let ty = self.substitute_univs(ty, univs);
- self.var(i, ty)
+ let ty = ty.substitute_univs(univs, arena);
+ Term::var(i, ty, arena)
},
Sort(level) => {
- let subst = level.substitute(univs, self);
- self.sort(subst)
+ let subst = level.substitute(univs, arena);
+ Term::sort(subst, arena)
},
App(u1, u2) => {
- let u1 = self.substitute_univs(u1, univs);
- let u2 = self.substitute_univs(u2, univs);
- self.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 = self.substitute_univs(u1, univs);
- let u2 = self.substitute_univs(u2, univs);
- self.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 = self.substitute_univs(u1, univs);
- let u2 = self.substitute_univs(u2, univs);
- self.prod(u1, u2)
+ let u1 = u1.substitute_univs(univs, arena);
+ let u2 = u2.substitute_univs(univs, arena);
+ u1.prod(u2, arena)
},
Decl(decl) => {
// TODO this can be slightly optimised. Certainly the substitute mapping can be
// performed in place while allocating the slice with store_level_slice. This
// function thus has to be made with templates.
- let params = &*decl.params.into_iter().map(|level| level.substitute(univs, self)).collect::<Vec<Level>>();
- let params = self.store_level_slice(params);
- let inst = InstantiatedDeclaration::instantiate((*decl).decl, params, self);
- self.decl(inst)
+ let params = &*decl.params.into_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)
},
}
}
@@ -130,28 +130,28 @@ impl<'arena> Arena<'arena> {
/// Returns the normal form of a term.
///
/// This function is computationally expensive and should only be used for reduce/eval commands, not when type-checking.
- pub fn normal_form(&mut self, t: Term<'arena>) -> Term<'arena> {
- let mut temp = t;
- let mut res = self.beta_reduction(t);
+ pub fn normal_form(self, arena: &mut Arena<'arena>) -> Self {
+ let mut temp = self;
+ let mut res = self.beta_reduction(arena);
while res != temp {
temp = res;
- res = self.beta_reduction(res);
+ res = res.beta_reduction(arena);
}
res
}
/// Returns the weak-head normal form of a term.
- pub fn whnf(&mut self, t: Term<'arena>) -> Term<'arena> {
- t.get_whnf_or_init(|| match *t {
- App(t1, t2) => match *self.whnf(t1) {
+ pub fn whnf(self, arena: &mut Arena<'arena>) -> Self {
+ self.get_whnf_or_init(|| match *self {
+ App(t1, t2) => match *t1.whnf(arena) {
Abs(_, t1) => {
- let subst = self.substitute(t1, t2, 1);
- self.whnf(subst)
+ let subst = t1.substitute(t2, 1, arena);
+ subst.whnf(arena)
},
- _ => t,
+ _ => self,
},
- _ => t,
+ _ => self,
})
}
}
@@ -171,7 +171,7 @@ mod tests {
// λx.x x
let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
- assert_eq!(arena.beta_reduction(term), reduced);
+ assert_eq!(term.beta_reduction(arena), reduced);
})
}
@@ -290,14 +290,14 @@ mod tests {
// λa.λb.b
let term_step_7 = arena.build_term_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);
+ 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);
})
}
@@ -307,7 +307,7 @@ mod tests {
let reduced = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
let term = arena.build_term_raw(app(abs(prop(), reduced.into()), prop()));
- assert_eq!(arena.beta_reduction(term), reduced)
+ assert_eq!(term.beta_reduction(arena), reduced)
})
}
@@ -317,7 +317,7 @@ mod tests {
let term = arena.build_term_raw(prod(prop(), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop()))));
let reduced = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
- assert_eq!(arena.beta_reduction(term), reduced);
+ assert_eq!(term.beta_reduction(arena), reduced);
})
}
@@ -328,7 +328,7 @@ mod tests {
.build_term_raw(abs(prop(), app(var(1.into(), prop()), app(abs(prop(), var(1.into(), prop())), var(1.into(), prop())))));
let reduced = arena.build_term_raw(abs(prop(), app(var(1.into(), prop()), var(1.into(), prop()))));
- assert_eq!(arena.beta_reduction(term), reduced);
+ assert_eq!(term.beta_reduction(arena), reduced);
})
}
@@ -339,7 +339,7 @@ mod tests {
.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!(arena.normal_form(term), normal_form);
+ assert_eq!(term.normal_form(arena), normal_form);
})
}
}
diff --git a/kernel/src/memory/builders.rs b/kernel/src/memory/builders.rs
index 27ff0fda98f5264f9d031536b9f3954766db76ec..e45f7570b7db6846e44001cc30a21059d377055d 100644
--- a/kernel/src/memory/builders.rs
+++ b/kernel/src/memory/builders.rs
@@ -64,8 +64,8 @@ pub const fn var<'build, 'arena>(name: &'build str) -> impl BuilderTrait<'build,
.map(|(bind_depth, term)| {
// This is arguably an eager computation, it could be worth making it lazy,
// or at least memoizing it so as to not compute it again
- let var_type = arena.shift(*term, usize::from(depth - *bind_depth), 0);
- arena.var(depth - *bind_depth, var_type)
+ let var_type = term.shift(usize::from(depth - *bind_depth), 0, arena);
+ Term::var(depth - *bind_depth, var_type, arena)
})
.or_else(|| arena.get_binding(name))
.ok_or(Error {
@@ -77,36 +77,28 @@ pub const fn var<'build, 'arena>(name: &'build str) -> impl BuilderTrait<'build,
/// 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())
+ |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(Term::prop(arena))
}
-/// Returns a closure building the Type `level` term.
-#[inline]
-pub const fn type_<'build, 'arena>(level: Level<'arena>) -> 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`).
+/// Returns a closure building the Type `i` term, where `i` is an integer
#[inline]
pub const fn type_usize<'build, 'arena>(level: usize) -> impl BuilderTrait<'build, 'arena> {
move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| {
- let lvl = Level::from(level, arena);
- Ok(arena.type_(lvl))
+ Ok(Term::type_usize(level, arena))
}
}
-/// Returns a closure building the Type `level` term.
+/// Returns a closure building the Sort `level` term.
#[inline]
pub const fn sort<'build, 'arena>(level: Level<'arena>) -> impl BuilderTrait<'build, 'arena> {
- move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(arena.sort(level))
+ move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| Ok(Term::sort(level, arena))
}
-/// Returns a closure building the Type `level` term (indirection from `usize`).
+/// Returns a closure building the Sort `level` term (indirection from `usize`).
#[inline]
pub const fn sort_usize<'build, 'arena>(level: usize) -> impl BuilderTrait<'build, 'arena> {
move |arena: &mut Arena<'arena>, _: &Environment<'build, 'arena>, _| {
- let lvl = Level::from(level, arena);
- Ok(arena.sort(lvl))
+ Ok(Term::sort_usize(level, arena))
}
}
@@ -121,7 +113,7 @@ pub const fn app<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTr
|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))
+ Ok(u1.app(u2, arena))
}
}
@@ -138,7 +130,7 @@ pub const fn abs<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderTr
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))
+ Ok(arg_type.abs(body, arena))
}
}
@@ -155,7 +147,7 @@ pub const fn prod<'build, 'arena, F1: BuilderTrait<'build, 'arena>, F2: BuilderT
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))
+ Ok(arg_type.prod(body, arena))
}
}
@@ -231,41 +223,41 @@ pub(crate) mod raw {
}
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)
+ move |arena: &mut Arena<'arena>| {
+ let ty = type_(arena);
+ Term::var(index, ty, arena)
}
}
pub const fn prop<'arena>() -> impl BuilderTrait<'arena> {
- |env: &mut Arena<'arena>| env.prop()
+ |arena: &mut Arena<'arena>| Term::prop(arena)
}
- pub const fn type_<'arena>(level: Level<'arena>) -> impl BuilderTrait<'arena> {
- move |env: &mut Arena<'arena>| env.type_(level)
+ pub const fn sort_<'arena>(level: Level<'arena>) -> impl BuilderTrait<'arena> {
+ move |arena: &mut Arena<'arena>| Term::sort(level, arena)
}
pub const fn app<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
- |env: &mut Arena<'arena>| {
- let u1 = u1(env);
- let u2 = u2(env);
- env.app(u1, u2)
+ |arena: &mut Arena<'arena>| {
+ let u1 = u1(arena);
+ let u2 = u2(arena);
+ u1.app(u1, arena)
}
}
pub const fn abs<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
- |env: &mut Arena<'arena>| {
- let u1 = u1(env);
- let u2 = u2(env);
- env.abs(u1, u2)
+ |arena: &mut Arena<'arena>| {
+ let u1 = u1(arena);
+ let u2 = u2(arena);
+ u1.abs(u2, arena)
}
}
pub const fn prod<'arena, F1: BuilderTrait<'arena>, F2: BuilderTrait<'arena>>(u1: F1, u2: F2) -> impl BuilderTrait<'arena> {
- |env: &mut Arena<'arena>| {
- let u1 = u1(env);
- let u2 = u2(env);
- env.prod(u1, u2)
+ |arena: &mut Arena<'arena>| {
+ let u1 = u1(arena);
+ let u2 = u2(arena);
+ u1.prod(u2, arena)
}
}
}
diff --git a/kernel/src/memory/term.rs b/kernel/src/memory/term.rs
index 0277c820b7ce440feced831256f1f70a67a194d5..25cca8f90baaf1a5f3b07900dcaf9910c5afe58e 100644
--- a/kernel/src/memory/term.rs
+++ b/kernel/src/memory/term.rs
@@ -10,6 +10,7 @@ use derive_more::{Add, Display, From, Into, Sub};
use super::declaration::InstantiatedDeclaration;
use super::level::Level;
+use crate::memory::arena::Arena;
use crate::error::ResultTerm;
/// An index used to designate bound variables.
@@ -86,92 +87,101 @@ impl<'arena> fmt::Display for Term<'arena> {
use Payload::*;
-// TODO make this a Term-impl. This will impact most files from the project, but should not be so
-// hard.
-impl<'arena> super::arena::Arena<'arena> {
+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_term(&mut self, n: Payload<'arena>) -> Term<'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: n,
+ payload,
header: Header {
head_normal_form: OnceCell::new(),
type_: OnceCell::new(),
},
};
- match self.hashcons_terms.get(&new_node) {
+ match arena.hashcons_terms.get(&new_node) {
Some(addr) => Term::new(addr),
None => {
- let addr = self.alloc.alloc(new_node);
- self.hashcons_terms.insert(addr);
+ 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(&mut self, index: DeBruijnIndex, type_: Term<'arena>) -> Term<'arena> {
- self.hashcons_term(Var(index, 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(&mut self) -> Term<'arena> {
- let zero = Level::zero(self);
- self.hashcons_term(Sort(zero))
- }
-
- pub(crate) fn type_(&mut self, level: Level<'arena>) -> Term<'arena> {
- let succ = level.succ(self);
- self.hashcons_term(Sort(succ))
+ pub(crate) fn prop(arena: &mut Arena<'arena>) -> Self {
+ Self::hashcons(Sort(Level::zero(arena)), arena)
}
- pub(crate) fn sort(&mut self, level: Level<'arena>) -> Term<'arena> {
- self.hashcons_term(Sort(level))
+ /// 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(&mut self, level: usize) -> Term<'arena> {
- let level = Level::from(level + 1, self);
- self.hashcons_term(Sort(level))
+ 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 Type(level), casting level appropriately first
- pub(crate) fn sort_usize(&mut self, level: usize) -> Term<'arena> {
- let level = Level::from(level, self);
- self.hashcons_term(Sort(level))
+ /// 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(&mut self, func: Term<'arena>, arg: Term<'arena>) -> Term<'arena> {
- self.hashcons_term(App(func, arg))
+ 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(&mut self, arg_type: Term<'arena>, body: Term<'arena>) -> Term<'arena> {
- self.hashcons_term(Abs(arg_type, body))
+ 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(&mut self, arg_type: Term<'arena>, body: Term<'arena>) -> Term<'arena> {
- self.hashcons_term(Prod(arg_type, body))
+ pub(crate) fn prod(self, body: Self, arena: &mut Arena<'arena>) -> Self {
+ Self::hashcons(Prod(self, body), arena)
}
- /// TODO(doc)
- pub(crate) fn decl(&mut self, decl: InstantiatedDeclaration<'arena>) -> Term<'arena> {
- self.hashcons_term(Decl(decl))
+ /// 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
@@ -187,21 +197,3 @@ impl<'arena> super::arena::Arena<'arena> {
}
}
}
-
-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.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()
- }
-}
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index df6c755a9bc74c714dfa3b91fc66d0de5394aeb2..5c2ae1fa7f45010a135ca3b7599f79a47b027305 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -38,18 +38,18 @@ pub enum TypeCheckerError<'arena> {
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 {
+ 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;
@@ -62,69 +62,69 @@ impl<'arena> Arena<'arena> {
// again.
(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)) => self.conversion(t1, t2) && self.conversion(u1, u2),
+ (&App(t1, u1), &App(t2, u2)) => t1.conversion(t2, arena) && u1.conversion(u2, 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 *lhs {
+ fn imax(self, rhs: Self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
+ match *self {
Sort(l1) => match *rhs {
Sort(l2) => {
- let lvl = l1.imax(l2, self);
- Ok(self.sort(lvl))
+ let lvl = l1.imax(l2, arena);
+ Ok(Term::sort(lvl, arena))
},
_ => Err(Error {
kind: TypeCheckerError::NotUniverse(rhs).into(),
}),
},
_ => Err(Error {
- kind: TypeCheckerError::NotUniverse(lhs).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 {
+ /// Infers the type of the term `t`, living in arena `arena`.
+ pub fn infer(self, arena: &mut Arena<'arena>) -> ResultTerm<'arena> {
+ self.get_type_or_try_init(|| match *self {
Sort(lvl) => {
- let lvl = lvl.succ(self);
- Ok(self.sort(lvl))
+ let lvl = lvl.succ(arena);
+ Ok(Term::sort(lvl, 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 {
Sort(_) => {
- let type_u = self.infer(u)?;
- Ok(self.prod(t, type_u))
+ let type_u = u.infer(arena)?;
+ Ok(t.prod(type_u, arena))
},
_ => Err(Error {
kind: TypeCheckerError::NotUniverse(type_t).into(),
@@ -133,14 +133,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,11 +158,11 @@ impl<'arena> Arena<'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(),
})
}
@@ -185,7 +185,7 @@ mod tests {
let term = arena.build_term_raw(app(abs(prop(), id.into()), id.into()));
let normal_form = arena.build_term_raw(abs(prop(), var(1.into(), prop())));
- assert!(arena.is_def_eq(term, normal_form).is_ok())
+ assert!(term.is_def_eq(normal_form, arena).is_ok())
})
}
@@ -196,7 +196,7 @@ mod tests {
let term = arena.build_term_raw(app(abs(prop(), abs(prop(), var(2.into(), prop()))), id.into()));
let normal_form = arena.build_term_raw(abs(prop(), id.into()));
- assert!(arena.is_def_eq(term, normal_form).is_ok())
+ assert!(term.is_def_eq(normal_form, arena).is_ok())
})
}
@@ -207,18 +207,18 @@ mod tests {
// λa.a (λx.x) (λx.x)
let term = arena.build_term_raw(abs(prop(), app(app(var(2.into(), prop()), id.into()), id.into())));
- 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()
})
@@ -229,13 +229,13 @@ mod tests {
#[test]
fn failed_prod_binder_conversion() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
+ let type_0 = Term::type_usize(0, arena);
let term_lhs = arena.build_term_raw(prod(prop(), prop()));
let term_rhs = arena.build_term_raw(prod(type_0.into(), 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()
})
@@ -246,13 +246,13 @@ mod tests {
#[test]
fn failed_app_head_conversion() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
+ let type_0 = Term::type_usize(0, arena);
let term_lhs = arena.build_term_raw(abs(type_0.into(), abs(type_0.into(), app(var(1.into(), prop()), prop()))));
let term_rhs = arena.build_term_raw(abs(type_0.into(), abs(type_0.into(), 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()
})
@@ -263,15 +263,15 @@ mod tests {
#[test]
fn typed_reduction_app_1() {
use_arena(|arena| {
- let type_0 = arena.type_usize(0);
+ let type_0 = Term::type_usize(0, arena);
let term = arena.build_term_raw(app(abs(type_0.into(), var(1.into(), type_0.into())), prop()));
let reduced = arena.build_term_raw(prop());
- 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();
assert_eq!(term_type, type_0);
- assert!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
@@ -347,42 +347,42 @@ 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_term_raw(app(abs(prop(), type_0.into()), 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 type_0 = Term::type_usize(0, arena);
+ let type_1 = Term::type_usize(1, arena);
let term = arena.build_term_raw(abs(prop(), prod(var(1.into(), prop()), type_0.into())));
- let term_type = arena.infer(term).unwrap();
+ let term_type = term.infer(arena).unwrap();
let expected_type = arena.build_term_raw(prod(prop(), type_1.into()));
assert_eq!(term_type, expected_type);
- assert!(arena.check(term, term_type).is_ok())
+ assert!(term.check(term_type, arena).is_ok())
})
}
@@ -402,19 +402,19 @@ mod tests {
// λx.x x
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 type_0 = Term::type_usize(0, arena);
let term = arena.build_term_raw(prod(prop(), prop()));
- 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())
})
}
@@ -422,10 +422,10 @@ mod tests {
fn typed_prod_2() {
use_arena(|arena| {
let term = arena.build_term_raw(prod(prop(), var(1.into(), prop())));
- let term_type = arena.infer(term).unwrap();
+ 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());
})
}
@@ -433,28 +433,28 @@ mod tests {
fn typed_prod_3() {
use_arena(|arena| {
let term = arena.build_term_raw(abs(prop(), abs(var(1.into(), prop()), var(1.into(), var(2.into(), prop())))));
- let term_type = arena.infer(term).unwrap();
+ 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 type_0 = Term::type_usize(0, arena);
let identity =
arena.build_term_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_term_raw(prod(type_0.into(), prod(var(1.into(), type_0.into()), var(2.into(), type_0.into()))));
assert_eq!(identity_type, expected_type);
- assert!(arena.check(identity, identity_type).is_ok());
+ assert!(identity.check(identity_type, arena).is_ok());
})
}
@@ -471,32 +471,32 @@ mod tests {
),
),
));
- let term_type = arena.infer(term).unwrap();
+ let term_type = term.infer(arena).unwrap();
assert_eq!(term_type, arena.build_term_raw(prod(prop(), prod(prop(), prod(prod(prop(), prod(prop(), prop())), prop())))));
- assert!(arena.check(term, term_type).is_ok());
+ 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,9 +509,9 @@ mod tests {
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,9 +523,9 @@ mod tests {
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,9 +537,9 @@ mod tests {
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,9 +551,9 @@ mod tests {
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,9 +565,9 @@ mod tests {
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,9 +579,9 @@ mod tests {
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()
})
);
})
@@ -601,11 +601,11 @@ mod tests {
));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
kind: TypeCheckerError::WrongArgumentType(
arena.build_term_raw(abs(prop(), app(var(2.into(), prod(prop(), prop())), var(1.into(), prop())))),
- arena.prop(),
+ Term::prop(arena),
TypedTerm(arena.build_term_raw(var(1.into(), prod(prop(), prop()))), arena.build_term_raw(prod(prop(), prop())))
)
.into()
@@ -623,7 +623,7 @@ mod tests {
));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
kind: TypeCheckerError::NotUniverse(arena.build_term_raw(var(2.into(), prop()))).into()
})
@@ -637,7 +637,7 @@ mod tests {
let term = arena.build_term_raw(prod(id(), prop()));
assert_eq!(
- arena.infer(term),
+ term.infer(arena),
Err(Error {
kind: TypeCheckerError::NotUniverse(arena.build_term_raw(prod(prop(), prop()))).into()
})
@@ -650,12 +650,12 @@ mod tests {
use_arena(|arena| {
let term = arena.build_term_raw(prod(prop(), abs(prop(), prop())));
- let prop = arena.prop();
- let type_ = arena.type_usize(0);
+ 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.prod(prop, type_)).into()
+ kind: TypeCheckerError::NotUniverse(prop.prod(type_, arena)).into()
})
);
})
@@ -665,12 +665,12 @@ mod tests {
fn check_fail_1() {
use_arena(|arena| {
let term = arena.build_term_raw(app(prop(), prop()));
- let expected_type = arena.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(),
})
);
})
@@ -679,11 +679,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(),
})
);
})