From eefaad73df58d0ded161f71626b98896d2ec724f Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Wed, 9 Nov 2022 17:16:39 +0100
Subject: [PATCH] chore(environment) : refactor
---
kernel/src/command.rs | 10 +++++-----
kernel/src/environment.rs | 16 +++++++++++++---
kernel/src/term.rs | 4 ++--
kernel/src/type_checker.rs | 4 ++--
4 files changed, 22 insertions(+), 12 deletions(-)
diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 39402a2d..570ee1e9 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -17,11 +17,11 @@ impl Command {
match self {
Command::Define(s, None, term) => term
.infer(env)
- .and_then(|t| env.insert(s, term, t).map(|_| None)),
+ .and_then(|t| env.insert_def(s, term, t).map(|_| None)),
Command::Define(s, Some(t), term) => term
.check(&t, env)
- .and_then(|_| env.insert(s, term, t).map(|_| None)),
+ .and_then(|_| env.insert_def(s, term, t).map(|_| None)),
Command::CheckType(t1, t2) => t1.check(&t2, env).map(|_| None),
@@ -38,7 +38,7 @@ mod tests {
fn simple_env() -> Environment {
Environment::new()
- .insert("x".to_string(), Term::r#type(0.into()), Term::PROP)
+ .insert_def("x".to_string(), Term::r#type(0.into()), Term::PROP)
.unwrap()
.clone()
}
@@ -61,7 +61,7 @@ mod tests {
assert_eq!(
env,
*(simple_env()
- .insert("y".to_string(), Term::PROP, Term::r#type(0.into()))
+ .insert_def("y".to_string(), Term::PROP, Term::r#type(0.into()))
.unwrap())
);
}
@@ -84,7 +84,7 @@ mod tests {
assert_eq!(
env,
*(simple_env()
- .insert("y".to_string(), Term::PROP, Term::r#type(0.into()))
+ .insert_def("y".to_string(), Term::PROP, Term::r#type(0.into()))
.unwrap())
);
}
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index 5096eacd..cd6e264e 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -15,16 +15,26 @@ impl Environment {
Self::default()
}
- /// Creates a new environment binding s with (t1,t2)
- pub fn insert(&mut self, s: String, t1: Term, t2: Term) -> 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(Declaration::make(Some(t1), t2));
+ e.insert(decl);
Ok(self)
} else {
Err(KernelError::AlreadyDefined(s))
}
}
+ /// Creates a new environment binding s with t1 : t2
+ pub fn insert_def(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
+ self.insert(s, Declaration::make(Some(t1), t2))
+ }
+
+ /// Creates a new environment binding s with an axiom of type ty
+ 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> {
self.0.get(s).and_then(|decl| decl.get_term(vec))
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index 03c332b1..e42e6933 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -383,7 +383,7 @@ mod tests {
box Prod(box Var(1.into()), box Var(1.into())),
);
let mut env = Environment::new();
- env.insert("foo".into(), id_prop.clone(), Sort(0.into()))
+ env.insert_def("foo".into(), id_prop.clone(), Sort(0.into()))
.unwrap();
assert_eq!(
@@ -408,7 +408,7 @@ mod tests {
);
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();
+ let env = binding.insert_def("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 fbe9b3d5..904ba830 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -412,7 +412,7 @@ mod tests {
);
let mut binding = Environment::new();
let env = binding
- .insert("foo".into(), id_prop.clone(), Sort(0.into()))
+ .insert_def("foo".into(), id_prop.clone(), Sort(0.into()))
.unwrap();
assert!(t.check(&Const("foo".into(), Vec::new()), env).is_ok());
@@ -443,7 +443,7 @@ mod tests {
);
let mut binding = Environment::new();
let env = binding
- .insert("foo".into(), id_prop, Sort(0.into()))
+ .insert_def("foo".into(), id_prop, Sort(0.into()))
.unwrap();
assert!(Const("foo".into(), Vec::new()).infer(env).is_ok());
--
GitLab