From 0a766e977b49838c05ff92f9224add5b64edf5cf Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Tue, 1 Nov 2022 15:41:33 +0100
Subject: [PATCH] Chore : fix rebase
---
kernel/src/command.rs | 36 ++++++++----------------------------
kernel/src/declaration.rs | 2 +-
kernel/src/environment.rs | 4 ++--
kernel/src/term.rs | 22 +++++-----------------
kernel/src/type_checker.rs | 22 +++++++++-------------
kernel/src/universe.rs | 10 ++++++++--
parser/src/parser.rs | 20 +++++---------------
7 files changed, 38 insertions(+), 78 deletions(-)
diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 14788a47..c97df9eb 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -30,15 +30,11 @@ impl Command {
#[cfg(test)]
mod tests {
- use crate::{num_bigint::BigUint, Command, Environment, Term};
+ use crate::{Command, Environment, Term};
fn simple_env() -> Environment {
Environment::new()
- .insert(
- "x".to_string(),
- Term::Type(BigUint::from(0_u64).into()),
- Term::Prop,
- )
+ .insert("x".to_string(), Term::Type(0.into()), Term::Prop)
.unwrap()
.clone()
}
@@ -61,22 +57,14 @@ mod tests {
assert_eq!(
env,
*(simple_env()
- .insert(
- "y".to_string(),
- Term::Prop,
- Term::Type(BigUint::from(0_u64).into())
- )
+ .insert("y".to_string(), Term::Prop, Term::Type(0.into()))
.unwrap())
);
}
#[test]
fn failed_typed_define() {
- let cmd = Command::Define(
- "y".to_string(),
- Some(Term::Type(BigUint::from(1_u64).into())),
- Term::Prop,
- );
+ let cmd = Command::Define("y".to_string(), Some(Term::Type(1.into())), Term::Prop);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
@@ -85,22 +73,14 @@ mod tests {
#[test]
fn successful_typed_define() {
- let cmd = Command::Define(
- "y".to_string(),
- Some(Term::Type(BigUint::from(0_u64).into())),
- Term::Prop,
- );
+ let cmd = Command::Define("y".to_string(), Some(Term::Type(0.into())), Term::Prop);
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
assert_eq!(
env,
*(simple_env()
- .insert(
- "y".to_string(),
- Term::Prop,
- Term::Type(BigUint::from(0_u64).into())
- )
+ .insert("y".to_string(), Term::Prop, Term::Type(0.into()))
.unwrap())
);
}
@@ -116,7 +96,7 @@ mod tests {
#[test]
fn successful_checktype() {
- let cmd = Command::CheckType(Term::Prop, Term::Type(BigUint::from(0_u64).into()));
+ let cmd = Command::CheckType(Term::Prop, Term::Type(0.into()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_ok());
@@ -125,7 +105,7 @@ mod tests {
#[test]
fn failed_gettype() {
- let cmd = Command::GetType(Term::Const("y".to_string()));
+ let cmd = Command::GetType(Term::Const("y".to_string(), Vec::new()));
let mut env = simple_env();
assert!(cmd.process(&mut env).is_err());
diff --git a/kernel/src/declaration.rs b/kernel/src/declaration.rs
index cda8a22a..8b300f5d 100644
--- a/kernel/src/declaration.rs
+++ b/kernel/src/declaration.rs
@@ -8,7 +8,7 @@ use crate::universe::UniverseLevel;
/// Additionally, ty and term *should* in theory always have the same number of universe variables, and as such, only a single method is needed.
/// However, additional checks to ensure this invariant will have to be put in place. For now, when constructing declarations, only the number of
/// universes in ty are counted.
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Declaration {
ty: Term,
term: Option<Term>,
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index 93118e94..65922e70 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -7,7 +7,7 @@ use derive_more::From;
use std::collections::{hash_map, HashMap};
/// Global Environment, contains the term and type of every definitions, denoted by their strings.
-#[derive(Clone, Default, Debug, From)]
+#[derive(Clone, Default, Debug, From, PartialEq, Eq)]
pub struct Environment(HashMap<String, Declaration>);
impl Environment {
@@ -19,7 +19,7 @@ impl Environment {
/// Creates a new environment binding s with (t1,t2)
pub fn insert(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
if let hash_map::Entry::Vacant(e) = self.0.entry(s.clone()) {
- e.insert(Declaration::make(t1, t2));
+ e.insert(Declaration::make(Some(t1), t2));
Ok(self)
} else {
Err(KernelError::AlreadyDefined(s))
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index efa321a0..d9882178 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -343,22 +343,10 @@ mod tests {
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())
- }
-
-
- #[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())
+ let mut binding = Environment::new();
+ let env = binding.insert("id".into(), id_te, id_ty).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 7c113025..043060dc 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -376,12 +376,12 @@ mod tests {
fn env_test() {
let id_prop = 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())));
- let mut env = Environment::new();
- env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
+ let mut binding = Environment::new();
+ let env = binding.insert("foo".into(), id_prop.clone(), Prop).unwrap();
- assert!(t.check(&Const("foo".into(), Vec::new()), &env).is_ok());
+ assert!(t.check(&Const("foo".into(), Vec::new()), env).is_ok());
assert!(id_prop
- .is_def_eq(&Const("foo".into(), Vec::new()), &env)
+ .is_def_eq(&Const("foo".into(), Vec::new()), env)
.is_ok());
}
@@ -400,10 +400,10 @@ mod tests {
#[test]
fn infer_const() {
let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
- let mut env = Environment::new();
- env.insert("foo".into(), id_prop, Prop).unwrap();
+ let mut binding = Environment::new();
+ let env = binding.insert("foo".into(), id_prop, Prop).unwrap();
- assert!(Const("foo".into(), Vec::new()).infer(&env).is_ok());
+ assert!(Const("foo".into(), Vec::new()).infer(env).is_ok());
assert!(Const("foo".into(), Vec::new())
.infer(&Environment::new())
.is_err());
@@ -419,13 +419,9 @@ mod tests {
#[test]
fn univ_reduc() {
let ty = App(
- box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
+ box Abs(box Prop, box Type(0.into())),
box Prod(box Prop, box Var(1.into())),
);
- assert!(ty.conversion(
- &Type(BigUint::from(0_u64).into()),
- &Environment::new(),
- 0.into()
- ))
+ assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
}
}
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index b22df581..d9660953 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -96,13 +96,19 @@ mod tests {
#[test]
fn univ_vars_count() {
- assert_eq!(Max(box Succ(box Zero), box Max(box Var(0), box Var(1))).univ_vars(), 2)
+ assert_eq!(
+ 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 subst = vec![Succ(box Zero), Zero];
- assert_eq!(lvl.substitute(&subst), Max(box Succ(box Zero), box Max(box Succ(box Zero), box Zero)))
+ assert_eq!(
+ lvl.substitute(&subst),
+ Max(box Succ(box Zero), box Max(box Succ(box Zero), box Zero))
+ )
}
}
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index ca6ebf0c..2196eb24 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -1,4 +1,3 @@
-use kernel::num_bigint::BigUint;
use kernel::{Command, KernelError, Loc, Term};
use pest::error::{Error, LineColLocation};
use pest::iterators::Pair;
@@ -15,16 +14,6 @@ fn convert_span(span: Span) -> Loc {
let (x2, y2) = span.end_pos().line_col();
Loc::new(x1, y1, x2, y2)
}
-fn build_term_from_expr(
- pair: Pair<Rule>,
- known_vars: &mut VecDeque<String>,
- //defined_vars: issue #18 TODO use a hash map of known variables
-) -> Result<Term, Box<Error<Rule>>> {
- match pair.as_rule() {
- Rule::Prop => Ok(Term::Prop),
- Rule::Type => Ok(Term::Type(
- pair.into_inner().as_str().parse::<usize>().unwrap().into(),
- )),
/// build terms from errorless pest's output
fn build_term_from_expr(pair: Pair<Rule>, known_vars: &mut VecDeque<String>) -> Term {
@@ -32,14 +21,15 @@ fn build_term_from_expr(pair: Pair<Rule>, known_vars: &mut VecDeque<String>) ->
let _loc = convert_span(pair.as_span());
match pair.as_rule() {
Rule::Prop => Term::Prop,
- Rule::Type => Term::Type(pair.into_inner().fold(BigUint::from(0_u64).into(), |_, x| {
- x.as_str().parse::<BigUint>().unwrap().into()
- })),
+ Rule::Type => Term::Type(
+ pair.into_inner()
+ .fold(0.into(), |_, x| x.as_str().parse::<usize>().unwrap().into()),
+ ),
Rule::Var => {
let name = pair.into_inner().as_str().to_string();
match known_vars.iter().position(|x| *x == name) {
Some(i) => Term::Var((i + 1).into()),
- None => Term::Const(name),
+ None => Term::Const(name, Vec::new()),
}
}
Rule::App => {
--
GitLab