From 90af3fd845cad7e0ab8378c492d22df72ed36ca2 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Tue, 1 Nov 2022 16:00:05 +0100
Subject: [PATCH] Fix : tests
---
kernel/src/term.rs | 12 ----------
kernel/src/type_checker.rs | 15 -------------
parser/src/parser.rs | 46 +++++++++++++++++++-------------------
3 files changed, 23 insertions(+), 50 deletions(-)
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index 86417519..e1f45521 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -350,16 +350,4 @@ mod tests {
.is_ok())
}
-
- #[test]
- fn poly_univ_id(){
- let id_ty = Prod(box Type(UniverseLevel::Var(0)),box Prod(box Var(1.into()),box Var(2.into())));
- let id_te = Abs(box Type(UniverseLevel::Var(0)),box Abs(box Var(1.into()),box Var(1.into())));
- let id_zero = Abs(box Type(0.into()),box Abs(box Var(1.into()),box Var(1.into())));
- assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
- let env = Environment::new()
- .insert("id".into(), id_te.clone().into(), id_ty.clone())
- .unwrap();
- assert!(Const("id".into(),vec![0.into()]).is_def_eq(&id_zero, &env).is_ok())
- }
}
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index b1a7eac1..33602bbd 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -425,19 +425,4 @@ mod tests {
assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
}
- #[test]
- fn prod_var() {
- let ty = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
- let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
- assert!(t.check(&ty, &Environment::new()).is_ok())
- }
-
- #[test]
- fn univ_reduc() {
- let ty = App(
- box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
- box Prod(box Prop, box Var(1.into())),
- );
- assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
- }
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 2196eb24..1289044c 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -266,7 +266,7 @@ mod tests {
#[test]
fn successful_var() {
- assert_eq!(parse_line("check A"), Ok(GetType(Const("A".to_string()))));
+ assert_eq!(parse_line("check A"), Ok(GetType(Const("A".to_string(),Vec::new()))));
assert_eq!(
parse_line("check fun A:Prop => A"),
Ok(GetType(Abs(box Prop, box Var(1.into()))))
@@ -294,22 +294,22 @@ mod tests {
assert_eq!(
parse_line("check A B C"),
Ok(GetType(App(
- box App(box Const("A".to_string()), box Const("B".to_string())),
- box Const("C".to_string())
+ box App(box Const("A".to_string(),Vec::new()), box Const("B".to_string(),Vec::new())),
+ box Const("C".to_string(),Vec::new())
)))
);
assert_eq!(
parse_line("check (A B) C"),
Ok(GetType(App(
- box App(box Const("A".to_string()), box Const("B".to_string())),
- box Const("C".to_string())
+ box App(box Const("A".to_string(),Vec::new()), box Const("B".to_string(),Vec::new())),
+ box Const("C".to_string(),Vec::new())
)))
);
assert_eq!(
parse_line("check A (B C)"),
Ok(GetType(App(
- box Const("A".to_string()),
- box App(box Const("B".to_string()), box Const("C".to_string()))
+ box Const("A".to_string(),Vec::new()),
+ box App(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
)))
)
}
@@ -319,22 +319,22 @@ mod tests {
assert_eq!(
parse_line("check A -> B -> C"),
Ok(GetType(Prod(
- box Const("A".to_string()),
- box Prod(box Const("B".to_string()), box Const("C".to_string()))
+ box Const("A".to_string(),Vec::new()),
+ box Prod(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
)))
);
assert_eq!(
parse_line("check A -> (B -> C)"),
Ok(GetType(Prod(
- box Const("A".to_string()),
- box Prod(box Const("B".to_string()), box Const("C".to_string()))
+ box Const("A".to_string(),Vec::new()),
+ box Prod(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
)))
);
assert_eq!(
parse_line("check (A -> B) -> C"),
Ok(GetType(Prod(
- box Prod(box Const("A".to_string()), box Const("B".to_string())),
- box Const("C".to_string())
+ box Prod(box Const("A".to_string(),Vec::new()), box Const("B".to_string(),Vec::new())),
+ box Const("C".to_string(),Vec::new())
)))
)
}
@@ -344,15 +344,15 @@ mod tests {
assert_eq!(
parse_line("check (x:A) -> (y:B) -> x"),
Ok(GetType(Prod(
- box Const("A".to_string()),
- box Prod(box Const("B".to_string()), box Var(2.into()))
+ box Const("A".to_string(),Vec::new()),
+ box Prod(box Const("B".to_string(),Vec::new()), box Var(2.into()))
)))
);
assert_eq!(
parse_line("check (x:A) -> ((y:B) -> x)"),
Ok(GetType(Prod(
- box Const("A".to_string()),
- box Prod(box Const("B".to_string()), box Var(2.into()))
+ box Const("A".to_string(),Vec::new()),
+ box Prod(box Const("B".to_string(),Vec::new()), box Var(2.into()))
)))
)
}
@@ -476,8 +476,8 @@ mod tests {
assert_eq!(
parse_line("check (((A))) -> (((B -> C)))"),
Ok(GetType(Prod(
- box Const("A".to_string()),
- box Prod(box Const("B".to_string()), box Const("C".to_string()))
+ box Const("A".to_string(),Vec::new()),
+ box Prod(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
)))
)
}
@@ -487,8 +487,8 @@ mod tests {
assert_eq!(
parse_line("check (((x:A))) -> ((((y:B) -> x)))"),
Ok(GetType(Prod(
- box Const("A".to_string()),
- box Prod(box Const("B".to_string()), box Var(2.into()))
+ box Const("A".to_string(),Vec::new()),
+ box Prod(box Const("B".to_string(),Vec::new()), box Var(2.into()))
)))
)
}
@@ -498,8 +498,8 @@ mod tests {
assert_eq!(
parse_line("check ((((((A))) (((B C))))))"),
Ok(GetType(App(
- box Const("A".to_string()),
- box App(box Const("B".to_string()), box Const("C".to_string()))
+ box Const("A".to_string(),Vec::new()),
+ box App(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
)))
)
}
--
GitLab