From 5e69a1616e2fbaab0008256d9c4e5613a63b2612 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Sun, 13 Nov 2022 09:48:25 +0100
Subject: [PATCH] chore: add coverage
---
kernel/src/environment.rs | 3 +-
kernel/src/universe.rs | 154 ++++++++++++++++++++++++++------------
parser/src/parser.rs | 6 +-
3 files changed, 110 insertions(+), 53 deletions(-)
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index cd6e264e..dfb6573c 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -15,7 +15,7 @@ impl Environment {
Self::default()
}
- pub fn insert(&mut self, s: String, decl : Declaration) -> Result<&Self, KernelError> {
+ pub fn insert(&mut self, s: String, decl: Declaration) -> Result<&Self, KernelError> {
if let hash_map::Entry::Vacant(e) = self.0.entry(s.clone()) {
e.insert(decl);
Ok(self)
@@ -33,7 +33,6 @@ impl Environment {
pub fn insert_axiom(&mut self, s: String, ty: Term) -> Result<&Self, KernelError> {
self.insert(s, Declaration::make(None, ty))
}
-
/// Returns the term linked to a definition in a given environment.
pub fn get_term(&self, s: &String, vec: &[UniverseLevel]) -> Option<Term> {
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index 51f4345e..631a6d49 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -87,9 +87,9 @@ impl UniverseLevel {
None => match self {
Zero => unreachable!("Zero is a numeral"),
Succ(_) => {
- let (u, n) = self.plus();
- format!("{} + {}", u.pretty_print(), n)
- },
+ 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),
@@ -107,17 +107,28 @@ impl UniverseLevel {
}
}
- fn substitute_single(self, var : usize, u : UniverseLevel) -> UniverseLevel {
+ fn substitute_single(self, var: usize, u: UniverseLevel) -> UniverseLevel {
match self {
Zero => Zero,
- Succ(n) => Succ(box n.substitute_single(var, u.clone())),
- Max(n, m) => Max(box n.substitute_single(var, u.clone()), box m.substitute_single(var, u)),
- IMax(n, m) => IMax(box n.substitute_single(var, u.clone()), box m.substitute_single(var, u)),
- Var(n) => if n == var { u } else { Var(n) },
+ Succ(n) => Succ(box n.substitute_single(var, u)),
+ Max(n, m) => Max(
+ box n.substitute_single(var, u.clone()),
+ box m.substitute_single(var, u),
+ ),
+ IMax(n, m) => IMax(
+ box n.substitute_single(var, u.clone()),
+ box m.substitute_single(var, u),
+ ),
+ Var(n) => {
+ if n == var {
+ u
+ } else {
+ Var(n)
+ }
+ }
}
}
-
pub fn substitute(self, univs: &[UniverseLevel]) -> Self {
match self {
Zero => Zero,
@@ -134,27 +145,26 @@ impl UniverseLevel {
/// 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))
- ///
- /// 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
+ ///
+ /// 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) -> Self {
match self {
IMax(box Zero, box u) => u.clone(),
- IMax(_ , box Zero) => Zero,
+ IMax(_, box Zero) => Zero,
IMax(box u, box Succ(v)) => Max(box u.normalize(), box Succ(v.clone())).normalize(),
- IMax(box u, box IMax(box v, box w)) => {
- Max(box IMax(box u.clone(), box w.clone()).normalize(),
- box IMax(box v.clone(), box w.clone()).normalize())
- }
- IMax(box u, box Max(box v, box w)) => {
- Max(box IMax(box u.clone(), box v.clone()).normalize(),
- box IMax(box u.clone(), box w.clone()).normalize())
- }
+ IMax(box u, box IMax(box v, box w)) => Max(
+ box IMax(box u.clone(), box w.clone()).normalize(),
+ box IMax(box v.clone(), box w.clone()).normalize(),
+ ),
+ IMax(box u, box Max(box v, box w)) => Max(
+ box IMax(box u.clone(), box v.clone()).normalize(),
+ box IMax(box u.clone(), box w.clone()).normalize(),
+ ),
_ => self.clone(),
}
}
-
// checks whether u1 <= u2 + 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)).
@@ -162,26 +172,40 @@ impl UniverseLevel {
// - (true,0) if u1 <= u2 + n,
// - (false,0) if !(u1 <= u2 + n),
// - (false,i+1) if Var(i) needs to be substituted to unstuck the comparison.
- fn geq_no_subst(&self, u2: &UniverseLevel, n: i64) -> (bool,usize) {
+ fn geq_no_subst(&self, u2: &UniverseLevel, n: i64) -> (bool, usize) {
match (self.normalize(), u2.normalize()) {
- (Zero, _) if n >= 0 => (true,0),
- (_, _) if *self == *u2 && n >= 0 => (true,0),
- (Succ(l), _) if l.geq_no_subst(u2, n - 1).0 => (true,0),
- (_, Succ(box l)) if self.geq_no_subst(&l, n + 1).0 => (true,0),
- (_, Max(box l1, box l2)) if self.geq_no_subst(&l1, n).0 || self.geq_no_subst(&l2, n).0 => (true,0),
- (Max(box l1, box l2), _) if l1.geq_no_subst(u2, n).0 && l2.geq_no_subst(u2, n).0 => (true,0),
- (_,IMax(_, box Var(i))) | (IMax(_, box Var(i)),_) => (false,i+1),
- _ => (false,0),
+ (Zero, _) if n >= 0 => (true, 0),
+ (_, _) if *self == *u2 && n >= 0 => (true, 0),
+ (Succ(l), _) if l.geq_no_subst(u2, n - 1).0 => (true, 0),
+ (_, Succ(box l)) if self.geq_no_subst(&l, n + 1).0 => (true, 0),
+ (_, Max(box l1, box l2))
+ if self.geq_no_subst(&l1, n).0 || self.geq_no_subst(&l2, n).0 =>
+ {
+ (true, 0)
+ }
+ (Max(box l1, box l2), _) if l1.geq_no_subst(u2, n).0 && l2.geq_no_subst(u2, n).0 => {
+ (true, 0)
+ }
+ (_, IMax(_, box Var(i))) | (IMax(_, box Var(i)), _) => (false, i + 1),
+ _ => (false, 0),
}
}
fn geq(&self, u2: &UniverseLevel, n: i64) -> bool {
match self.geq_no_subst(u2, n) {
- (true,_) => true,
- (false,0) => false,
- (false,i) => {
- self.clone().substitute_single(i-1,Zero).geq(&u2.clone().substitute_single(i-1,Zero), n) &&
- self.clone().substitute_single(i-1,Succ(box Var(i-1))).geq(&u2.clone().substitute_single(i-1,Succ(box Var(i-1))), n)
+ (true, _) => true,
+ (false, 0) => false,
+ (false, i) => {
+ self.clone()
+ .substitute_single(i - 1, Zero)
+ .geq(&u2.clone().substitute_single(i - 1, Zero), n)
+ && self
+ .clone()
+ .substitute_single(i - 1, Succ(box Var(i - 1)))
+ .geq(
+ &u2.clone().substitute_single(i - 1, Succ(box Var(i - 1))),
+ n,
+ )
}
}
}
@@ -195,26 +219,35 @@ 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))
+ 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));
+ 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))");
+ 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))"
+ );
}
}
@@ -229,26 +262,53 @@ 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 Max(box Succ(box Zero), box Zero))).is_eq(&IMax(box Succ(box Zero), box IMax(box Succ(box Zero), box Succ(box Zero)))));
+ assert!(&Max(
+ box Zero,
+ box IMax(box Zero, box Max(box Succ(box Zero), box Zero))
+ )
+ .is_eq(&IMax(
+ box Succ(box Zero),
+ box IMax(box Succ(box Zero), box Succ(box Zero))
+ )));
assert!(&Var(0).is_eq(&IMax(box Var(0), box Var(0))));
+ assert!(&IMax(box Succ(box Zero), box Max(box Zero, box Zero)).is_eq(&Zero));
+ assert!(!&IMax(box Var(0), box Var(1)).is_eq(&IMax(box Var(1), box Var(0))))
}
-
#[test]
fn univ_vars_count() {
assert_eq!(
- IMax(box Zero,box 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 = IMax(box Zero, box 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),
- IMax(box Zero, box 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))
+ )
+ )
+ }
+
+ #[test]
+ fn single_subst() {
+ let lvl = IMax(box Max(box Succ(box Zero), box Var(0)), box Var(0));
+ assert_eq!(
+ lvl.substitute_single(0, Zero),
+ IMax(box Max(box Succ(box Zero), box Zero), box Zero)
)
}
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 39f825e8..90273ffc 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -58,7 +58,7 @@ fn convert_span(span: Span) -> Loc {
fn build_univ_map_from_expr(pair: Pair<Rule>) -> HashMap<String, usize> {
let iter = pair.into_inner();
let mut map = HashMap::new();
- for (i,pair) in iter.enumerate() {
+ for (i, pair) in iter.enumerate() {
let str = pair.as_str();
if map.insert(str.to_string(), i).is_some() {
panic!("Duplicate universe variable {}", str);
@@ -209,9 +209,7 @@ fn build_command_from_expr(pair: Pair<Rule>) -> Command {
next.clone().map(|x| x.as_rule()),
None | Some(Rule::univ_decl)
) {
- let univs = next
- .map(build_univ_map_from_expr )
- .unwrap_or_default();
+ let univs = next.map(build_univ_map_from_expr).unwrap_or_default();
build_term_from_expr(iter.next().unwrap(), &mut VecDeque::new(), &univs)
} else {
build_term_from_expr(next.unwrap(), &mut VecDeque::new(), &HashMap::new())
--
GitLab