From e600cb3af3d005f43f11e01cd9664f077e083eb5 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Thu, 10 Nov 2022 14:10:42 +0100
Subject: [PATCH] chore : tests
---
kernel/src/universe.rs | 40 ++++++++++++++++++++++++++++++++--------
1 file changed, 32 insertions(+), 8 deletions(-)
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index 40d3bf99..31b0e916 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -86,10 +86,10 @@ impl UniverseLevel {
Some(n) => n.to_string(),
None => match self {
Zero => unreachable!("Zero is a numeral"),
- Succ(_) => match self.plus() {
- (u, 0) => u.pretty_print(),
- (u, n) => format!("{} + {}", u.pretty_print(), n),
- },
+ Succ(_) => {
+ let (u, n) = self.plus();
+ format!("{} + {}", u.pretty_print(), n)
+ },
Max(box n, box m) => format!("max ({}) ({})", n.pretty_print(), m.pretty_print()),
IMax(box n, box m) => format!("imax ({}) ({})", n.pretty_print(), m.pretty_print()),
Var(n) => format!("u{}", n),
@@ -181,6 +181,29 @@ impl UniverseLevel {
mod tests {
use crate::universe::UniverseLevel::*;
+
+ mod pretty_printing {
+ use crate::universe::UniverseLevel::*;
+
+ #[test]
+ fn to_num() {
+ assert_eq!(Max(box Succ(box Zero), box Zero).to_numeral(),Some(1));
+ assert_eq!(Max(box Succ(box Zero), box Succ(box Var(0))).to_numeral(),None);
+ assert_eq!(IMax(box Var(0),box Zero).to_numeral(),Some(0));
+ assert_eq!(IMax(box Zero,box Succ(box Zero)).to_numeral(),Some(1))
+ }
+
+ #[test]
+ fn to_plus() {
+ assert_eq!(Succ(box Zero).plus(),(Zero,1));
+ }
+
+ #[test]
+ fn to_pretty_print() {
+ assert_eq!(Max(box Succ(box Zero), box IMax(box Max(box Zero, box Var(0)), box Succ(box Var(0)))).pretty_print(), "max (1) (imax (max (0) (u0)) (u0 + 1))");
+ }
+ }
+
#[test]
fn univ_eq() {
assert!(&Zero.is_eq(&Default::default()));
@@ -192,23 +215,24 @@ mod tests {
assert!(!&Max(box Var(1), box Var(1)).is_eq(&Max(box Var(0), box Var(1))));
assert!(&Succ(box Max(box Var(1), box Var(0)))
.is_eq(&Max(box Succ(box Var(0)), box Succ(box Var(1)))));
- }
+ assert!(&Max(box Zero, box IMax(box Zero, box Succ(box Zero))).is_eq(&IMax(box Succ(box Zero), box Max(box Zero, box Zero))));
+ }
#[test]
fn univ_vars_count() {
assert_eq!(
- Max(box Succ(box Zero), box Max(box Var(0), box Var(1))).univ_vars(),
+ IMax(box Zero,box Max(box Succ(box Zero), box Max(box Var(0), box Var(1)))).univ_vars(),
2
)
}
#[test]
fn subst() {
- let lvl = Max(box Succ(box Zero), box Max(box Var(0), box Var(1)));
+ let lvl = IMax(box Zero, box Max(box Succ(box Zero), box Max(box Var(0), box Var(1))));
let subst = vec![Succ(box Zero), Zero];
assert_eq!(
lvl.substitute(&subst),
- Max(box Succ(box Zero), box Max(box Succ(box Zero), box Zero))
+ IMax(box Zero, box Max(box Succ(box Zero), box Max(box Succ(box Zero), box Zero)))
)
}
}
--
GitLab