From 6f551f0be7b14a9b7229649d2ce71fa314595c7e Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Tue, 1 Nov 2022 10:10:56 +0100
Subject: [PATCH] feat: everything
---
kernel/src/declaration.rs | 20 +++++++
kernel/src/environment.rs | 7 +--
kernel/src/lib.rs | 2 +
kernel/src/term.rs | 5 +-
kernel/src/type_checker.rs | 35 +++++-------
kernel/src/universe.rs | 106 ++++++++++++++++++++++++-------------
6 files changed, 110 insertions(+), 65 deletions(-)
create mode 100644 kernel/src/declaration.rs
diff --git a/kernel/src/declaration.rs b/kernel/src/declaration.rs
new file mode 100644
index 00000000..81feedda
--- /dev/null
+++ b/kernel/src/declaration.rs
@@ -0,0 +1,20 @@
+use crate::term::Term;
+
+
+/// 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.
+/// univ_vars corresponds to the number of universe variables bound to the declaration.
+/// No universe variable can be "free" in a term, meaning that for all Var(i) in ty or term, i<univ_vars.
+/// 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 term are counted. Since ty has to be infered, or at least checked against the infered type before being added, it has to have <= universes than term.
+#[derive(Clone)]
+pub struct Declaration {
+ ty : Term,
+ term : Option<Term>,
+ univ_vars : usize
+}
+
+impl Declaration {
+
+}
\ No newline at end of file
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index a83244ac..01721aca 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -1,11 +1,12 @@
use crate::error::KernelError;
use crate::term::Term;
+use crate::declaration::Declaration;
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, Eq, PartialEq, From)]
-pub struct Environment(HashMap<String, (Term, Term)>);
+#[derive(Clone, Default, From)]
+pub struct Environment(HashMap<String, Declaration>);
impl Environment {
/// Creates an empty environment.
@@ -16,7 +17,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((t1, t2));
+ e.insert(Declaration::make(t1, t2));
Ok(self)
} else {
Err(KernelError::AlreadyDefined(s))
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index 331f2a82..d3642508 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -8,6 +8,8 @@ mod environment;
mod error;
mod term;
mod type_checker;
+mod universe;
+mod declaration;
pub use derive_more;
pub use num_bigint;
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index a840deaa..4abd8686 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -1,15 +1,12 @@
use crate::environment::Environment;
+use crate::universe::UniverseLevel;
use derive_more::{Add, Display, From, Into, Sub};
-use num_bigint::BigUint;
#[derive(
Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord,
)]
pub struct DeBruijnIndex(usize);
-#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord)]
-pub struct UniverseLevel(BigUint);
-
#[derive(Clone, Debug, Display, Eq, PartialEq)]
pub enum Term {
#[display(fmt = "{}", _0)]
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index ca4c8cb5..611840a8 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -1,8 +1,7 @@
use crate::environment::Environment;
use crate::error::KernelError;
use crate::term::{DeBruijnIndex, Term};
-use num_bigint::BigUint;
-use std::cmp::max;
+use crate::universe::UniverseLevel;
use std::ops::Index;
use Term::*;
@@ -47,7 +46,7 @@ impl Term {
/// The conversion is untyped, meaning that it should **only** be called during type-checking when the two `Term`s are already known to be of the same type and in the same context.
fn conversion(&self, rhs: &Term, env: &Environment, lvl: DeBruijnIndex) -> bool {
match (self.whnf(env), rhs.whnf(env)) {
- (Type(i), Type(j)) => i == j,
+ (Type(i), Type(j)) => i.is_eq(&j),
(Prop, Prop) => true,
@@ -100,7 +99,7 @@ impl Term {
Prop => Ok(Type(i.clone())),
// else if u1 = Type(i) and u2 = Type(j), then (x : A) -> B : Type(max(i,j))
- Type(j) => Ok(Type(max(i.clone(), j.clone()))),
+ Type(j) => Ok(Type(UniverseLevel::Max(box i.clone(), box j.clone()))),
_ => Err(KernelError::NotUniverse(self.clone())),
},
@@ -111,8 +110,8 @@ impl Term {
fn _infer(&self, env: &Environment, ctx: &mut Context) -> Result<Term, KernelError> {
match self {
- Prop => Ok(Type(BigUint::from(0_u64).into())),
- Type(i) => Ok(Type(i.clone() + BigUint::from(1_u64).into())),
+ Prop => Ok(Type(UniverseLevel::Zero)),
+ Type(i) => Ok(Type(i.clone() + 1)),
Var(i) => Ok(ctx.types[ctx.lvl - *i].clone()),
Const(s) => match env.get_type(s) {
@@ -199,16 +198,13 @@ mod tests {
#[test]
fn simple() {
- let t1 = App(
- box Abs(box Type(BigUint::from(0_u64).into()), box Var(1.into())),
- box Prop,
- );
+ let t1 = App(box Abs(box Type(0.into()), box Var(1.into())), box Prop);
let t2 = Prop;
assert!(t1.conversion(&t2, &Environment::new(), 0.into()));
let ty = t1.infer(&Environment::new());
- assert_eq!(ty, Ok(Type(BigUint::from(0_u64).into())));
+ assert_eq!(ty, Ok(Type(0.into())));
}
#[test]
@@ -317,7 +313,7 @@ mod tests {
#[test]
fn polymorphism() {
let id = Abs(
- box Type(BigUint::from(0_u64).into()),
+ box Type(0.into()),
box Abs(box Var(1.into()), box Var(1.into())),
);
@@ -326,8 +322,8 @@ mod tests {
#[test]
fn type_type() {
- assert!(Type(BigUint::from(0_u64).into())
- .check(&Type(BigUint::from(1_u64).into()), &Environment::new())
+ assert!(Type(0.into())
+ .check(&Type(1.into()), &Environment::new())
.is_ok());
}
@@ -346,18 +342,15 @@ mod tests {
assert!(t.infer(&Environment::new()).is_err());
let wf_prod = Prod(box Prop, box Prop);
- assert!(wf_prod
- .check(&Type(BigUint::from(0_u64).into()), &Environment::new())
- .is_ok());
+ println!("{:?}",wf_prod.infer(&Environment::new()));
+ assert!(wf_prod.check(&Type(0.into()), &Environment::new()).is_ok());
let wf_prod = Prod(box Prop, box Var(1.into()));
assert!(wf_prod.check(&Prop, &Environment::new()).is_ok());
// Type0 -> (A : Prop) ->
let wf_prod = Prod(box Prop, box Prop);
- assert!(wf_prod
- .check(&Type(BigUint::from(0_u64).into()), &Environment::new())
- .is_ok());
+ assert!(wf_prod.check(&Type(0.into()), &Environment::new()).is_ok());
}
#[test]
@@ -398,7 +391,7 @@ mod tests {
#[test]
fn not_def_eq() {
assert!(Prop
- .is_def_eq(&Type(BigUint::from(0_u64).into()), &Environment::new())
+ .is_def_eq(&Type(0.into()), &Environment::new())
.is_err());
}
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index 85ce34ff..4ffa5a1b 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -1,56 +1,88 @@
-use derive_more::{Display};
+use std::ops::Add;
+
+use derive_more::Display;
#[derive(Clone, Debug, Default, Display, PartialEq, Eq)]
pub enum UniverseLevel {
#[default]
- UnivZero,
- UnivSucc(Box<UniverseLevel>),
- #[display(fmt = "max {} {}", _0, _1)]
- UnivMax(Box<UniverseLevel>,Box<UniverseLevel>),
- UnivVar(usize)
+ Zero,
+ Succ(Box<UniverseLevel>),
+ #[display(fmt = "max ({}) ({})", _0, _1)]
+ Max(Box<UniverseLevel>, Box<UniverseLevel>),
+ Var(usize),
}
-use UniverseLevel::*;
-impl UniverseLevel {
- fn normalize(self) -> Self {
- match self {
- UnivMax(box UnivSucc(u1),box UnivSucc(u2)) => UnivSucc(box UnivMax(u1,u2)),
- UnivMax(box u1,box UnivZero) | UnivMax(box UnivZero, box u1) => u1,
- UnivMax(u1, u2) if u1.clone().normalize() == u2.clone().normalize() => u1.clone().normalize(),
- _ => self
- }
- }
-
- fn shift(self, n : usize) -> Self{
- match self {
- UnivZero => self,
- UnivSucc(u) => UnivSucc(box u.shift(n)),
- UnivMax(u1,u2) => UnivMax(box u1.shift(n), box u2.shift(n)),
- UnivVar(k) if k>n => UnivVar(k-1),
- _ => self
+//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;
+
+ fn add(self, n: usize) -> Self {
+ if n == 0 {
+ self
+ } else {
+ Succ(box self.add(n - 1))
}
}
+}
- fn substitute(self,n : usize) -> Self {
-
+impl From<usize> for UniverseLevel {
+ fn from(n: usize) -> Self {
+ if n == 0 {
+ Zero
+ } else {
+ Succ(box (n - 1).into())
+ }
}
+}
- fn geq(self, u2 : UniverseLevel,n : u64) -> bool {
- match (self,u2) {
- (UnivZero,_) if n >=0 => true,
- (_,_) if self == u2 && n>=0 => true,
- (UnivSucc(l),_) if l.geq(u2,n-1) => true,
- (_,UnivSucc(box l)) if self.geq(l,n+1) => true,
- (_,UnivMax(box l1, box l2)) if self.geq(l1,n) || self.geq(l2,n) => true,
- (UnivMax(box l1, box l2),_) if l1.geq(u2,n) && l2.geq(u2,n) => true
+use UniverseLevel::*;
+impl UniverseLevel {
+ /*fn substitute(self, u: &UniverseLevel, lvl : usize) -> Self {
+ match self {
+ UnivZero => UnivZero,
+ UnivSucc(v) => UnivSucc(box v.substitute(u),lvl),
+ UnivMax(u1, u2) => UnivMax(box u1.substitute(u,lvl), box u2.substitute(u,lvl)),
+ UnivVar(var) if var == lvl => u.clone(),
+ UnivVar(var) if var>lvl => UnivVar(var - 1),
+ _ => self
+ }
+ }*/
+ fn geq(&self, u2: &UniverseLevel, n: i64) -> bool {
+ match (self, u2) {
+ (Zero, _) if n >= 0 => true,
+ (_, _) if self == u2 && n >= 0 => true,
+ (Succ(l), _) if l.geq(u2, n - 1) => true,
+ (_, Succ(box l)) if self.geq(l, n + 1) => true,
+ (_, Max(box l1, box l2)) if self.geq(l1, n) || self.geq(l2, n) => true,
+ (Max(box l1, box l2), _) if l1.geq(u2, n) && l2.geq(u2, n) => true,
+ _ => false
}
}
-
- pub fn is_eq(self,u2 : UniverseLevel) -> bool {
- self.geq(u2,0) && u2.geq(self,0)
+ pub fn is_eq(&self, u2: &UniverseLevel) -> bool {
+ self.geq(u2, 0) && u2.geq(self, 0)
}
+}
+#[cfg(test)]
+mod tests {
+ use crate::universe::UniverseLevel::*;
+
+ #[test]
+ fn univ_eq() {
+ assert!(format!("{}",Max(box Zero, box Zero)) == "max (Zero) (Zero)");
+ assert!(&Zero.is_eq(&Default::default()));
+ assert!(!&Zero.is_eq(&Succ(box Zero)));
+ assert!(!&Succ(box Zero).is_eq(&Zero));
+ assert!(&Var(0).is_eq(&Max(box Zero, box Var(0))));
+ assert!(&Max(box Zero, box Var(0)).is_eq(&Var(0)));
+ assert!(&Max(box Var(1), box Var(0)).is_eq(&Max(box Var(0), box Var(1))));
+ assert!(!&Max(box Var(1), box Var(1)).is_eq(&Max(box Var(0), box Var(1))));
+ assert!(&Succ(box Max(box Var(1), box Var(0))).is_eq(&Max(box Succ(box Var(0)), box Succ(box Var(1)))));
+ }
}
--
GitLab