From 5ff3504d71d4389cc1c61bcf6ff249fb50db186a Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Sun, 13 Nov 2022 10:08:45 +0100
Subject: [PATCH] Fix:todo
---
kernel/src/declaration.rs | 28 ++++++++++++----------------
kernel/src/error.rs | 8 ++++++--
kernel/src/universe.rs | 13 +++++++------
3 files changed, 25 insertions(+), 24 deletions(-)
diff --git a/kernel/src/declaration.rs b/kernel/src/declaration.rs
index 8b300f5d..a5ade92d 100644
--- a/kernel/src/declaration.rs
+++ b/kernel/src/declaration.rs
@@ -1,5 +1,6 @@
use crate::term::Term;
use crate::universe::UniverseLevel;
+use crate::KernelError;
/// Declarations constructed through commands. A declaration describes a constant in the environment, whether it's a definition with
/// a corresponding term, or an axiom with only a type.
@@ -24,29 +25,24 @@ impl Declaration {
}
}
- pub fn get_type(&self, vec: &[UniverseLevel]) -> Term {
+ /// Returns the type linked to a definition in a given environment.
+ pub fn get_type(&self, vec: &[UniverseLevel]) -> Result<Term,KernelError> {
if self.univ_vars != vec.len() {
- //TODO wrap in a Result monad
- panic!(
- "wrong type of universe arguments, expected {}, found {}",
- self.univ_vars,
- vec.len()
- )
+ Err(KernelError::WrongNumberOfUniverseArguments(self.univ_vars,
+ vec.len()))
} else {
- self.ty.substitute_univs(vec)
+ Ok(self.ty.substitute_univs(vec))
}
}
- pub fn get_term(&self, vec: &[UniverseLevel]) -> Option<Term> {
+ /// Returns the term linked to a definition in a given environment.
+ /// Since the declaration might be an axiom, it might not have an associated term to reduce to, hence the Option.
+ pub fn get_term(&self, vec: &[UniverseLevel]) -> Result<Option<Term>,KernelError> {
if self.univ_vars != vec.len() {
- //TODO wrap in a Result monad
- panic!(
- "wrong type of universe arguments, expected {}, found {}",
- self.univ_vars,
- vec.len()
- )
+ Err(KernelError::WrongNumberOfUniverseArguments(self.univ_vars,
+ vec.len()))
} else {
- self.clone().term.map(|x| x.substitute_univs(vec))
+ Ok(self.clone().term.map(|x| x.substitute_univs(vec)))
}
}
}
diff --git a/kernel/src/error.rs b/kernel/src/error.rs
index 50c2def1..f81eb026 100644
--- a/kernel/src/error.rs
+++ b/kernel/src/error.rs
@@ -28,7 +28,7 @@ impl Loc {
#[derive(Clone, Debug, Display, PartialEq, Eq)]
pub enum KernelError {
// cannot parse command
- #[display(fmt = "cannot parse: {}", _1)]
+ #[display(fmt = "Cannot parse: {}", _1)]
CannotParse(Loc, String),
// s is already defined
@@ -65,6 +65,10 @@ pub enum KernelError {
NotAFunction(Term, Term, Term),
/// Expected ty1, found ty2
- #[display(fmt = "expected {}, found {}", _0, _1)]
+ #[display(fmt = "Expected {}, found {}", _0, _1)]
TypeMismatch(Term, Term),
+
+ #[display(fmt = "Wrong number of universe arguments, expected {}, found {}", _0, _1)]
+ WrongNumberOfUniverseArguments(usize, usize),
+
}
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index 631a6d49..3b59fff5 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -16,10 +16,6 @@ pub enum UniverseLevel {
Var(usize),
}
-//Each declaration in the global context has a number corresponding to its number of universe parameters.
-//things to worry about : how to check conversion between universe polymorphic types ? only check universe_eq between them ? might be incomplete.
-// TODO extend universe checking.
-
impl Add<usize> for UniverseLevel {
type Output = Self;
@@ -97,6 +93,7 @@ impl UniverseLevel {
}
}
+ /// Is used to find the number of universe in a declaration.
pub fn univ_vars(self) -> usize {
match self {
Zero => 0,
@@ -107,6 +104,7 @@ impl UniverseLevel {
}
}
+ /// Helper function for equality checking, used to substitute Var(i) with Z and S(Var(i)).
fn substitute_single(self, var: usize, u: UniverseLevel) -> UniverseLevel {
match self {
Zero => Zero,
@@ -129,6 +127,7 @@ impl UniverseLevel {
}
}
+ /// General universe substitution, given a vector of universe levels, it substitutes each Var(i) with the i-th element of the vector.
pub fn substitute(self, univs: &[UniverseLevel]) -> Self {
match self {
Zero => Zero,
@@ -166,8 +165,6 @@ impl UniverseLevel {
}
// 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)).
// returns:
// - (true,0) if u1 <= u2 + n,
// - (false,0) if !(u1 <= u2 + n),
@@ -191,6 +188,10 @@ impl UniverseLevel {
}
}
+
+ /// 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)).
fn geq(&self, u2: &UniverseLevel, n: i64) -> bool {
match self.geq_no_subst(u2, n) {
(true, _) => true,
--
GitLab