diff --git a/kernel/src/declaration.rs b/kernel/src/declaration.rs
index 81feeddaf152dd6655ec51854008abd22676b620..ae64e75261e57ae72f8842e5a0e445b1ac63fdb6 100644
--- a/kernel/src/declaration.rs
+++ b/kernel/src/declaration.rs
@@ -1,20 +1,50 @@
use crate::term::Term;
+use crate::universe::UniverseLevel;
-
-/// Declarations constructed through commands. A declaration describes a constant in the environment, whether it's a definition with
+/// 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.
+/// 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)]
+/// 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)]
pub struct Declaration {
- ty : Term,
- term : Option<Term>,
- univ_vars : usize
+ ty: Term,
+ term: Option<Term>,
+ univ_vars: usize,
}
impl Declaration {
-
-}
\ No newline at end of file
+ pub fn make(term: Option<Term>, ty: Term) -> Declaration {
+ Declaration {
+ ty: ty.clone(),
+ term,
+ univ_vars: ty.univ_vars(),
+ }
+ }
+
+ pub fn get_type(&self, vec: &[UniverseLevel]) -> Term {
+ if self.univ_vars != vec.len() {
+ panic!(
+ "wrong type of universe arguments, expected {}, found {}",
+ self.univ_vars,
+ vec.len()
+ )
+ } else {
+ self.ty.substitute_univs(vec)
+ }
+ }
+
+ pub fn get_term(&self, vec: &[UniverseLevel]) -> Option<Term> {
+ if self.univ_vars != vec.len() {
+ panic!(
+ "wrong type of universe arguments, expected {}, found {}",
+ self.univ_vars,
+ vec.len()
+ )
+ } else {
+ self.clone().term.map(|x| x.substitute_univs(vec))
+ }
+ }
+}
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index 01721aca033df6aa75fbd1ad9049ad599f6b0024..93118e9456712f0da17faa09336a31ae265d39f1 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -1,11 +1,13 @@
use crate::error::KernelError;
use crate::term::Term;
use crate::declaration::Declaration;
+use crate::term::Term;
+use crate::universe::UniverseLevel;
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, From)]
+#[derive(Clone, Default, Debug, From)]
pub struct Environment(HashMap<String, Declaration>);
impl Environment {
@@ -25,12 +27,12 @@ impl Environment {
}
/// Returns the term linked to a definition in a given environment.
- pub fn get_term(&self, s: &String) -> Option<Term> {
- self.0.get(s).map(|(t, _)| t.clone())
+ pub fn get_term(&self, s: &String, vec: &[UniverseLevel]) -> Option<Term> {
+ self.0.get(s).and_then(|decl| decl.get_term(vec))
}
/// Returns the type linked to a definition in a given environment.
- pub fn get_type(&self, s: &String) -> Option<Term> {
- self.0.get(s).map(|(_, t)| t.clone())
+ pub fn get_type(&self, s: &String, vec: &[UniverseLevel]) -> Option<Term> {
+ self.0.get(s).map(|decl| decl.get_type(vec))
}
}
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index d3642508b65403f12893aa24a14d9982d048e283..59a7d9f01df6c2cc17db258fb881677d78fae0cd 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -4,12 +4,12 @@
#![feature(box_syntax)]
mod command;
+mod declaration;
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 4abd86860d0c36ec2afb7ae3463b1e894e519b45..bba9d85284c1fe51187a3ae102c44c71339bae40 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -12,8 +12,11 @@ pub enum Term {
#[display(fmt = "{}", _0)]
Var(DeBruijnIndex),
+ /// Constants can be universe polymorphic. As such, it is important to know what universes
+ /// they're assigned to. The vector serves to represent the universes by which the variables
+ /// present in the constant need to be substituted for.
#[display(fmt = "{}", _0)]
- Const(String),
+ Const(String, Vec<UniverseLevel>),
#[display(fmt = "Prop")]
Prop,
@@ -40,9 +43,9 @@ impl Term {
App(box Abs(_, box t1), box t2) => t1.substitute(t2, 1),
App(box t1, box t2) => App(box t1.beta_reduction(env), box t2.clone()),
Abs(x, box t) => Abs(x.clone(), box t.beta_reduction(env)),
- Const(s) => match env.get_term(s) {
+ Const(s, vec) => match env.get_term(s, vec) {
Some(t) => t,
- None => unreachable!(),
+ None => self.clone(),
},
_ => self.clone(),
}
@@ -91,13 +94,35 @@ impl Term {
whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env).whnf(env),
_ => self.clone(),
},
- Const(s) => match env.get_term(s) {
+ Const(s, vec) => match env.get_term(s, vec) {
Some(t) => t,
- None => unreachable!(),
+ None => self.clone(),
},
_ => self.clone(),
}
}
+
+ pub fn univ_vars(&self) -> usize {
+ match self {
+ Var(_) => 0,
+ Const(..) => 0,
+ Prop => 0,
+ Type(u) => u.clone().univ_vars(),
+ App(t1, t2) | Abs(t1, t2) | Prod(t1, t2) => t1.univ_vars().max(t2.univ_vars()),
+ }
+ }
+
+ pub fn substitute_univs(&self, vec: &[UniverseLevel]) -> Term {
+ match self {
+ Var(_) => self.clone(),
+ Const(..) => self.clone(),
+ Prop => self.clone(),
+ Type(u) => Type(u.clone().substitute(vec)),
+ App(t1, t2) => App(box t1.substitute_univs(vec), box t2.substitute_univs(vec)),
+ Abs(t1, t2) => Abs(box t1.substitute_univs(vec), box t2.substitute_univs(vec)),
+ Prod(t1, t2) => Prod(box t1.substitute_univs(vec), box t2.substitute_univs(vec)),
+ }
+ }
}
#[cfg(test)]
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 611840a8f18eca941841902e1f270b49f85d8987..7c1130257f4b03bd5eb4618792ebe85ac8d3a67e 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -114,7 +114,7 @@ impl Term {
Type(i) => Ok(Type(i.clone() + 1)),
Var(i) => Ok(ctx.types[ctx.lvl - *i].clone()),
- Const(s) => match env.get_type(s) {
+ Const(s, vec) => match env.get_type(s, vec) {
Some(ty) => Ok(ty),
None => Err(KernelError::ConstNotFound(s.clone())),
},
@@ -342,7 +342,7 @@ mod tests {
assert!(t.infer(&Environment::new()).is_err());
let wf_prod = Prod(box Prop, box Prop);
- println!("{:?}",wf_prod.infer(&Environment::new()));
+ 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()));
@@ -379,8 +379,10 @@ mod tests {
let mut env = Environment::new();
env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
- assert!(t.check(&Const("foo".into()), &env).is_ok());
- assert!(id_prop.is_def_eq(&Const("foo".into()), &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_ok());
}
#[test]
@@ -401,8 +403,10 @@ mod tests {
let mut env = Environment::new();
env.insert("foo".into(), id_prop, Prop).unwrap();
- assert!(Const("foo".into()).infer(&env).is_ok());
- assert!(Const("foo".into()).infer(&Environment::new()).is_err());
+ assert!(Const("foo".into(), Vec::new()).infer(&env).is_ok());
+ assert!(Const("foo".into(), Vec::new())
+ .infer(&Environment::new())
+ .is_err());
}
#[test]
diff --git a/kernel/src/universe.rs b/kernel/src/universe.rs
index 4ffa5a1b23a2550f68756c8e19bdc989d17630ce..2def2419097456b6168ca1b5e61c39a645f3b381 100644
--- a/kernel/src/universe.rs
+++ b/kernel/src/universe.rs
@@ -41,16 +41,23 @@ impl From<usize> for UniverseLevel {
use UniverseLevel::*;
impl UniverseLevel {
- /*fn substitute(self, u: &UniverseLevel, lvl : usize) -> Self {
+ pub fn univ_vars(self) -> usize {
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
+ Zero => 0,
+ Succ(n) => n.univ_vars(),
+ Max(n, m) => n.univ_vars().max(m.univ_vars()),
+ Var(n) => n + 1,
}
- }*/
+ }
+
+ pub fn substitute(self, univs: &[UniverseLevel]) -> Self {
+ match self {
+ Zero => Zero,
+ Succ(v) => Succ(box v.substitute(univs)),
+ Max(u1, u2) => Max(box u1.substitute(univs), box u2.substitute(univs)),
+ Var(var) => univs[var].clone(),
+ }
+ }
fn geq(&self, u2: &UniverseLevel, n: i64) -> bool {
match (self, u2) {
@@ -60,7 +67,7 @@ impl UniverseLevel {
(_, 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
+ _ => false,
}
}
@@ -75,7 +82,7 @@ mod tests {
#[test]
fn univ_eq() {
- assert!(format!("{}",Max(box Zero, box Zero)) == "max (Zero) (Zero)");
+ 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));
@@ -83,6 +90,7 @@ mod tests {
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)))));
+ assert!(&Succ(box Max(box Var(1), box Var(0)))
+ .is_eq(&Max(box Succ(box Var(0)), box Succ(box Var(1)))));
}
}