Resolve "Add axioms"

Closes #70 (closed)

kernel/src/calculus/term.rs

@@ -3,8 +3,8 @@
 //! 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 crate::memory::arena::Arena;
 use crate::axiom;
+use crate::memory::arena::Arena;
 use crate::memory::declaration::InstantiatedDeclaration;
 use crate::memory::level::Level;
 use crate::memory::term::Payload::{Abs, App, Axiom, Decl, Prod, Sort, Var};
@@ -28,7 +28,6 @@ impl<'arena> Term<'arena> {
         if let Some(red) = self.reduce_recursor(arena) {
             return red;
         };
-        // TODO beta-reduce recursors
         match *self {
             App(t1, t2) => {
                 if let Abs(_, t1) = *t1.unfold(arena) {
@@ -196,13 +195,13 @@ impl<'arena> Term<'arena> {
         // Be aware that this function will not be automatically formatted, because of the
         // experimental status of let-chains, as well as that of if-let conditions in pattern matching.
         if let App(f, n) = *self && let App(f, motive_succ) = *f &&
-           let App(f, motive_0) = *f && let App(f, motive) = *f && let Axiom(axiom::Axiom::NatRec,lvl) = *f {
+           let App(f, motive_0) = *f && let App(f, motive) = *f && let Axiom(axiom::Axiom::NatRec, lvl) = *f {
             match *n.whnf(arena) {
-                Axiom(axiom::Axiom::Zero,_) => Some(motive_0),
-                App(f, n) if let Axiom(axiom::Axiom::Succ,_) = *f => {
+                Axiom(axiom::Axiom::Zero, _) => Some(motive_0),
+                App(f, n) if let Axiom(axiom::Axiom::Succ, _) = *f => {
                     let new_rec = Term::app(
                         Term::app(
-                            Term::app(Term::app(Term::axiom(axiom::Axiom::NatRec,lvl, arena), motive, arena), motive_0, arena),
+                            Term::app(Term::app(Term::axiom(axiom::Axiom::NatRec, lvl, arena), motive, arena), motive_0, arena),
                             motive_succ,
                             arena,
                         ),
@@ -463,6 +462,7 @@ mod tests {
 
     #[test]
     fn subst_univs() {
+        use crate::axiom::Axiom;
         use crate::memory::level::builder::raw::*;
 
         use_arena(|arena| {
@@ -495,6 +495,40 @@ mod tests {
             ));
 
             assert_eq!(term.substitute_univs(&[arena.build_level_raw(zero()), arena.build_level_raw(zero())], arena), term);
+
+            let nat = Term::axiom(Axiom::Nat, &[], arena);
+            assert_eq!(nat.substitute_univs(&[arena.build_level_raw(zero()), arena.build_level_raw(zero())], arena), nat);
+        });
+    }
+
+    #[test]
+    fn reduce_nat() {
+        use crate::axiom::Axiom;
+        use crate::memory::level::Level;
+        use_arena(|arena| {
+            let lvl_one = Level::succ(Level::zero(arena), arena);
+            let nat = Term::axiom(Axiom::Nat, &[], arena);
+            let zero = Term::axiom(Axiom::Zero, &[], arena);
+            let one = Term::app(Term::axiom(Axiom::Succ, &[], arena), zero, arena);
+            let to_zero = Term::app(
+                Term::app(
+                    Term::app(
+                        Term::axiom(Axiom::NatRec, arena.store_level_slice(&[lvl_one]), arena),
+                        Term::abs(nat, nat, arena),
+                        arena,
+                    ),
+                    zero,
+                    arena,
+                ),
+                Term::abs(nat, Term::abs(nat, zero, arena), arena),
+                arena,
+            );
+            let zero_to_zero = Term::app(to_zero, zero, arena);
+            let one_to_zero = Term::app(to_zero, one, arena);
+            let nat_to_zero = Term::app(to_zero, nat, arena);
+            assert_eq!(zero_to_zero.normal_form(arena), zero);
+            assert_eq!(one_to_zero.normal_form(arena), zero);
+            assert_eq!(nat_to_zero.whnf(arena), nat_to_zero);
         });
     }
 }