From b349acd98c6aafd1c2a5261c4ce5b6e408f0f4f7 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Tue, 1 Nov 2022 16:06:27 +0100
Subject: [PATCH] chore : fix rebase
---
kernel/src/environment.rs | 3 +-
kernel/src/term.rs | 24 +++++++---
kernel/src/type_checker.rs | 1 -
parser/src/parser.rs | 96 ++++++++++++++++++++++----------------
4 files changed, 73 insertions(+), 51 deletions(-)
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index 65922e70..5096eacd 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -1,6 +1,5 @@
-use crate::error::KernelError;
-use crate::term::Term;
use crate::declaration::Declaration;
+use crate::error::KernelError;
use crate::term::Term;
use crate::universe::UniverseLevel;
use derive_more::From;
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index e1f45521..6c8e7186 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -333,15 +333,26 @@ mod tests {
let mut env = Environment::new();
env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
- assert_eq!(Const("foo".into()).beta_reduction(&env), id_prop);
+ assert_eq!(
+ Const("foo".into(), Vec::new()).beta_reduction(&env),
+ id_prop
+ );
}
-
#[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())));
+ 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 mut binding = Environment::new();
let env = binding.insert("id".into(), id_te, id_ty).unwrap();
@@ -349,5 +360,4 @@ mod tests {
.is_def_eq(&id_zero, env)
.is_ok())
}
-
}
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 33602bbd..043060dc 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -424,5 +424,4 @@ mod tests {
);
assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
}
-
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 1289044c..b59d8d58 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -235,11 +235,7 @@ mod tests {
fn successful_definechecktype() {
assert_eq!(
parse_line("def x : Type := Prop"),
- Ok(Define(
- "x".to_string(),
- Some(Type(BigUint::from(0_u64).into())),
- Prop
- ))
+ Ok(Define("x".to_string(), Some(Type(0.into())), Prop))
)
}
@@ -255,7 +251,7 @@ mod tests {
fn successful_checktype() {
assert_eq!(
parse_line("check Prop : Type"),
- Ok(CheckType(Prop, Type(BigUint::from(0_u64).into())))
+ Ok(CheckType(Prop, Type(0.into())))
)
}
@@ -266,7 +262,10 @@ mod tests {
#[test]
fn successful_var() {
- assert_eq!(parse_line("check A"), Ok(GetType(Const("A".to_string(),Vec::new()))));
+ 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()))))
@@ -275,18 +274,9 @@ mod tests {
#[test]
fn successful_type() {
- assert_eq!(
- parse_line("check Type"),
- Ok(GetType(Type(BigUint::from(0_u64).into())))
- );
- assert_eq!(
- parse_line("check Type 0"),
- Ok(GetType(Type(BigUint::from(0_u64).into())))
- );
- assert_eq!(
- parse_line("check Type 1"),
- Ok(GetType(Type(BigUint::from(1_u64).into())))
- )
+ assert_eq!(parse_line("check Type"), Ok(GetType(Type(0.into()))));
+ assert_eq!(parse_line("check Type 0"), Ok(GetType(Type(0.into()))));
+ assert_eq!(parse_line("check Type 1"), Ok(GetType(Type(1.into()))))
}
#[test]
@@ -294,22 +284,31 @@ mod tests {
assert_eq!(
parse_line("check A B C"),
Ok(GetType(App(
- box App(box Const("A".to_string(),Vec::new()), box Const("B".to_string(),Vec::new())),
- box Const("C".to_string(),Vec::new())
+ 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(),Vec::new()), box Const("B".to_string(),Vec::new())),
- box Const("C".to_string(),Vec::new())
+ 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(),Vec::new()),
- box App(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
+ 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 +318,31 @@ mod tests {
assert_eq!(
parse_line("check A -> B -> C"),
Ok(GetType(Prod(
- box Const("A".to_string(),Vec::new()),
- box Prod(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
+ 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(),Vec::new()),
- box Prod(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
+ 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(),Vec::new()), box Const("B".to_string(),Vec::new())),
- box Const("C".to_string(),Vec::new())
+ 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 +352,15 @@ mod tests {
assert_eq!(
parse_line("check (x:A) -> (y:B) -> x"),
Ok(GetType(Prod(
- box Const("A".to_string(),Vec::new()),
- box Prod(box Const("B".to_string(),Vec::new()), 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(),Vec::new()),
- box Prod(box Const("B".to_string(),Vec::new()), 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 +484,11 @@ mod tests {
assert_eq!(
parse_line("check (((A))) -> (((B -> C)))"),
Ok(GetType(Prod(
- box Const("A".to_string(),Vec::new()),
- box Prod(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
+ 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 +498,8 @@ mod tests {
assert_eq!(
parse_line("check (((x:A))) -> ((((y:B) -> x)))"),
Ok(GetType(Prod(
- box Const("A".to_string(),Vec::new()),
- box Prod(box Const("B".to_string(),Vec::new()), 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 +509,11 @@ mod tests {
assert_eq!(
parse_line("check ((((((A))) (((B C))))))"),
Ok(GetType(App(
- box Const("A".to_string(),Vec::new()),
- box App(box Const("B".to_string(),Vec::new()), box Const("C".to_string(),Vec::new()))
+ box Const("A".to_string(), Vec::new()),
+ box App(
+ box Const("B".to_string(), Vec::new()),
+ box Const("C".to_string(), Vec::new())
+ )
)))
)
}
--
GitLab