kernel/src/command.rs

@@ -7,6 +7,8 @@ pub enum Command {
     CheckType(Term, Term),
 
     GetType(Term),
+
+    Eval(Term),
 }
 
 impl Command {
@@ -15,37 +17,41 @@ 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),
 
+            // This is only a temporary workaround. Once metavariables will be part of the system,
+            // there won't be any issue with checking/infering with a term with non-unified metavariables
+            Command::GetType(Term::Const(s, vec)) if vec.is_empty() => {
+                env.get_type_free_univ(&s).map(Some)
+            }
+
             Command::GetType(t) => t.infer(env).map(Some),
+
+            Command::Eval(t) => Ok(Some(t.normal_form(env)?)),
         }
     }
 }
 
 #[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_def("x".to_string(), Term::r#type(0.into()), Term::PROP)
             .unwrap()
             .clone()
     }
 
     #[test]
     fn failed_untyped_define() {
-        let cmd = Command::Define("x".to_string(), None, Term::Prop);
+        let cmd = Command::Define("x".to_string(), None, Term::PROP);
         let mut env = simple_env();
 
         assert!(cmd.process(&mut env).is_err());
@@ -54,29 +60,21 @@ mod tests {
 
     #[test]
     fn successful_untyped_define() {
-        let cmd = Command::Define("y".to_string(), None, Term::Prop);
+        let cmd = Command::Define("y".to_string(), None, 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_def("y".to_string(), Term::PROP, Term::r#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::r#type(1.into())), Term::PROP);
         let mut env = simple_env();
 
         assert!(cmd.process(&mut env).is_err());
@@ -85,29 +83,21 @@ 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::r#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_def("y".to_string(), Term::PROP, Term::r#type(0.into()))
                 .unwrap())
         );
     }
 
     #[test]
     fn failed_checktype() {
-        let cmd = Command::CheckType(Term::Prop, Term::Prop);
+        let cmd = Command::CheckType(Term::PROP, Term::PROP);
         let mut env = simple_env();
 
         assert!(cmd.process(&mut env).is_err());
@@ -116,7 +106,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::r#type(0.into()));
         let mut env = simple_env();
 
         assert!(cmd.process(&mut env).is_ok());
@@ -125,7 +115,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());
@@ -134,7 +124,7 @@ mod tests {
 
     #[test]
     fn successful_gettype() {
-        let cmd = Command::GetType(Term::Prop);
+        let cmd = Command::GetType(Term::PROP);
         let mut env = simple_env();
 
         assert!(cmd.process(&mut env).is_ok());

kernel/src/declaration.rs

+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.
+/// 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 ty are counted.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Declaration {
+    ty: Term,
+    term: Option<Term>,
+    univ_vars: usize,
+}
+
+impl Declaration {
+    pub fn make(term: Option<Term>, ty: Term) -> Declaration {
+        Declaration {
+            ty: ty.clone(),
+            term,
+            univ_vars: ty.univ_vars(),
+        }
+    }
+
+    /// 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() {
+            Err(KernelError::WrongNumberOfUniverseArguments(
+                self.univ_vars,
+                vec.len(),
+            ))
+        } else {
+            Ok(self.ty.substitute_univs(vec))
+        }
+    }
+
+    /// Returns the type linked to a definition in a given environment.
+    pub fn get_type_free_univ(&self) -> Term {
+        self.ty.clone()
+    }
+
+    /// 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() {
+            Err(KernelError::WrongNumberOfUniverseArguments(
+                self.univ_vars,
+                vec.len(),
+            ))
+        } else {
+            Ok(self.clone().term.map(|x| x.substitute_univs(vec)))
+        }
+    }
+}

kernel/src/environment.rs

+use crate::declaration::Declaration;
 use crate::error::KernelError;
 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, Debug, Eq, PartialEq, From)]
-pub struct Environment(HashMap<String, (Term, Term)>);
+#[derive(Clone, Default, Debug, From, PartialEq, Eq)]
+pub struct Environment(HashMap<String, Declaration>);
 
 impl Environment {
     /// Creates an empty environment.
@@ -13,23 +15,46 @@ 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((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) -> Option<Term> {
-        self.0.get(s).map(|(t, _)| t.clone())
+    pub fn get_term(&self, s: &String, vec: &[UniverseLevel]) -> Result<Option<Term>, KernelError> {
+        match self.0.get(s) {
+            Some(decl) => Ok(decl.get_term(vec)?),
+            None => Err(KernelError::ConstNotFound(s.clone())),
+        }
     }
 
     /// 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]) -> Result<Term, KernelError> {
+        match self.0.get(s) {
+            Some(decl) => Ok(decl.get_type(vec)?),
+            None => Err(KernelError::ConstNotFound(s.clone())),
+        }
+    }
+
+    /// Returns the type linked to a definition in a given environment.
+    pub fn get_type_free_univ(&self, s: &String) -> Result<Term, KernelError> {
+        match self.0.get(s) {
+            Some(decl) => Ok(decl.get_type_free_univ()),
+            None => Err(KernelError::ConstNotFound(s.clone())),
+        }
     }
 }

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,13 @@ 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),
 }

kernel/src/lib.rs

@@ -4,15 +4,19 @@
 #![feature(box_syntax)]
 
 mod command;
+mod declaration;
 mod environment;
 mod error;
 mod term;
 mod type_checker;
+mod universe;
 
 pub use derive_more;
 pub use num_bigint;
 
 pub use command::Command;
+pub use declaration::Declaration;
 pub use environment::Environment;
 pub use error::{KernelError, Loc};
 pub use term::Term;
+pub use universe::UniverseLevel;

kernel/src/term.rs

 use crate::environment::Environment;
+use crate::universe::UniverseLevel;
+use crate::KernelError;
 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)]
     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),
-
-    #[display(fmt = "Prop")]
-    Prop,
+    Const(String, Vec<UniverseLevel>),
 
-    #[display(fmt = "Type {}", _0)]
-    Type(UniverseLevel),
+    #[display(fmt = "Sort {}", _0)]
+    Sort(UniverseLevel),
 
     #[display(fmt = "{} {}", _0, _1)]
     App(Box<Term>, Box<Term>),
 
-    #[display(fmt = "\u{003BB} {} \u{02192} {}", _0, _1)]
+    #[display(fmt = "\u{003BB} ({}) \u{02192} {}", _0, _1)]
     Abs(Box<Term>, Box<Term>),
 
-    #[display(fmt = "\u{03A0} {} \u{02192} {}", _0, _1)]
+    #[display(fmt = "\u{03A0} ({}) \u{02192} {}", _0, _1)]
     Prod(Box<Term>, Box<Term>),
 }
 
 use Term::*;
 
 impl Term {
+    pub const PROP: Term = Sort(UniverseLevel::Zero);
+
+    pub fn r#type(u: UniverseLevel) -> Term {
+        Sort(u + 1)
+    }
+
     /// Apply one step of β-reduction, using leftmost outermost evaluation strategy.
-    pub fn beta_reduction(&self, env: &Environment) -> Term {
+    pub fn beta_reduction(&self, env: &Environment) -> Result<Term, KernelError> {
+        //if self.is_eliminator() {
+        //    return self.compute()
+        //}
         match self {
-            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) {
-                Some(t) => t,
-                None => unreachable!(),
+            App(box Abs(_, box t1), box t2) => Ok(t1.substitute(t2, 1)),
+            App(box t1, box t2) => Ok(App(box t1.beta_reduction(env)?, box t2.clone())),
+            Abs(x, box t) => Ok(Abs(x.clone(), box t.beta_reduction(env)?)),
+            Const(s, vec) => match env.get_term(s, vec)? {
+                Some(t) => Ok(t),
+                None => Ok(self.clone()),
             },
-            _ => self.clone(),
+            _ => Ok(self.clone()),
         }
     }
 
@@ -75,55 +82,100 @@ impl Term {
 
     /// Returns the normal form of a term in a given environment.
     ///
-    /// This function is computationally expensive and should only be used for Reduce/Eval commands, not when type-checking.
-    pub fn normal_form(self, env: &Environment) -> Term {
-        let mut res = self.beta_reduction(env);
+    /// This function is computationally expensive and should only be used for Reduce/Eval commands, not when Sort-checking.
+    pub fn normal_form(self, env: &Environment) -> Result<Term, KernelError> {
+        let mut res = self.beta_reduction(env)?;
         let mut temp = self;
 
         while res != temp {
             temp = res.clone();
-            res = res.beta_reduction(env)
+            res = res.beta_reduction(env)?
         }
-        res
+        Ok(res)
     }
 
     /// Returns the weak-head normal form of a term in a given environment.
-    pub fn whnf(&self, env: &Environment) -> Term {
+    pub fn whnf(&self, env: &Environment) -> Result<Term, KernelError> {
         match self {
-            App(box t, t2) => match t.whnf(env) {
-                whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env).whnf(env),
-                _ => self.clone(),
+            App(box t, t2) => match t.whnf(env)? {
+                whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env)?.whnf(env),
+                _ => Ok(self.clone()),
             },
-            Const(s) => match env.get_term(s) {
-                Some(t) => t,
-                None => unreachable!(),
+            Const(s, vec) => match env.get_term(s, vec)? {
+                Some(t) => Ok(t),
+                None => Ok(self.clone()),
             },
-            _ => self.clone(),
+            _ => Ok(self.clone()),
+        }
+    }
+
+    pub fn univ_vars(&self) -> usize {
+        match self {
+            Var(_) => 0,
+            Const(..) => 0,
+            Sort(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(),
+            Sort(u) => Sort(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)),
+        }
+    }
+
+    /*fn is_eliminator(&self) -> bool {
+        match self {
+                App(
+                    box App(
+                        box App(
+                            box App(
+                                box Const(rec,_var),
+                                _motive
+                            ),
+                            _p_zero
+                        ),
+                        _p_succ
+                    ),
+                _n) if rec == "Nat_rec" => true,
+            _ => false
+        }
+    }*/
 }
 
 #[cfg(test)]
 mod tests {
-    // /!\ most of these tests are on ill-typed terms and should not be used for further testings
+    // /!\ most of these tests are on ill-Sortd terms and should not be used for further testings
     use super::Term::*;
     use crate::term::Environment;
+    use crate::universe::UniverseLevel;
 
     #[test]
     fn simple_subst() {
         // λx.(λy.x y) x
         let term = Abs(
-            box Prop,
+            box Sort(0.into()),
             box App(
-                box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+                box Abs(
+                    box Sort(0.into()),
+                    box App(box Var(2.into()), box Var(1.into())),
+                ),
                 box Var(1.into()),
             ),
         );
 
         // λx.x x
-        let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
+        let reduced = Abs(
+            box Sort(0.into()),
+            box App(box Var(1.into()), box Var(1.into())),
+        );
 
-        assert_eq!(term.beta_reduction(&Environment::new()), reduced);
+        assert_eq!(term.beta_reduction(&Environment::new()).unwrap(), reduced);
     }
 
     #[test]
@@ -131,19 +183,19 @@ mod tests {
         // (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λa.λb.a b)
         let term = App(
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box Abs(
-                    box Prop,
+                    box Sort(0.into()),
                     box Abs(
-                        box Prop,
+                        box Sort(0.into()),
                         box App(
                             box App(
                                 box App(
                                     box Var(3.into()),
                                     box Abs(
-                                        box Prop,
+                                        box Sort(0.into()),
                                         box Abs(
-                                            box Prop,
+                                            box Sort(0.into()),
                                             box App(
                                                 box Var(1.into()),
                                                 box App(box Var(2.into()), box Var(4.into())),
@@ -151,34 +203,40 @@ mod tests {
                                         ),
                                     ),
                                 ),
-                                box Abs(box Prop, box Var(2.into())),
+                                box Abs(box Sort(0.into()), box Var(2.into())),
                             ),
-                            box Abs(box Prop, box Var(1.into())),
+                            box Abs(box Sort(0.into()), box Var(1.into())),
                         ),
                     ),
                 ),
             ),
             box Abs(
-                box Prop,
-                box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+                box Sort(0.into()),
+                box Abs(
+                    box Sort(0.into()),
+                    box App(box Var(2.into()), box Var(1.into())),
+                ),
             ),
         );
 
         let term_step_1 = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box App(
                     box App(
                         box App(
                             box Abs(
-                                box Prop,
-                                box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+                                box Sort(0.into()),
+                                box Abs(
+                                    box Sort(0.into()),
+                                    box App(box Var(2.into()), box Var(1.into())),
+                                ),
                             ),
                             box Abs(
-                                box Prop,
+                                box Sort(0.into()),
                                 box Abs(
-                                    box Prop,
+                                    box Sort(0.into()),
                                     box App(
                                         box Var(1.into()),
                                         box App(box Var(2.into()), box Var(4.into())),
@@ -186,26 +244,26 @@ mod tests {
                                 ),
                             ),
                         ),
-                        box Abs(box Prop, box Var(2.into())),
+                        box Abs(box Sort(0.into()), box Var(2.into())),
                     ),
-                    box Abs(box Prop, box Var(1.into())),
+                    box Abs(box Sort(0.into()), box Var(1.into())),
                 ),
             ),
         );
 
         let term_step_2 = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box App(
                     box App(
                         box Abs(
-                            box Prop,
+                            box Sort(0.into()),
                             box App(
                                 box Abs(
-                                    box Prop,
+                                    box Sort(0.into()),
                                     box Abs(
-                                        box Prop,
+                                        box Sort(0.into()),
                                         box App(
                                             box Var(1.into()),
                                             box App(box Var(2.into()), box Var(5.into())),
@@ -215,101 +273,147 @@ mod tests {
                                 box Var(1.into()),
                             ),
                         ),
-                        box Abs(box Prop, box Var(2.into())),
+                        box Abs(box Sort(0.into()), box Var(2.into())),
                     ),
-                    box Abs(box Prop, box Var(1.into())),
+                    box Abs(box Sort(0.into()), box Var(1.into())),
                 ),
             ),
         );
 
         let term_step_3 = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box App(
                     box App(
                         box Abs(
-                            box Prop,
+                            box Sort(0.into()),
                             box Abs(
-                                box Prop,
+                                box Sort(0.into()),
                                 box App(
                                     box Var(1.into()),
                                     box App(box Var(2.into()), box Var(4.into())),
                                 ),
                             ),
                         ),
-                        box Abs(box Prop, box Var(2.into())),
+                        box Abs(box Sort(0.into()), box Var(2.into())),
                     ),
-                    box Abs(box Prop, box Var(1.into())),
+                    box Abs(box Sort(0.into()), box Var(1.into())),
                 ),
             ),
         );
 
         let term_step_4 = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box App(
                     box Abs(
-                        box Prop,
+                        box Sort(0.into()),
                         box App(
                             box Var(1.into()),
-                            box App(box Abs(box Prop, box Var(3.into())), box Var(3.into())),
+                            box App(
+                                box Abs(box Sort(0.into()), box Var(3.into())),
+                                box Var(3.into()),
+                            ),
                         ),
                     ),
-                    box Abs(box Prop, box Var(1.into())),
+                    box Abs(box Sort(0.into()), box Var(1.into())),
                 ),
             ),
         );
 
         let term_step_5 = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box App(
-                    box Abs(box Prop, box Var(1.into())),
-                    box App(box Abs(box Prop, box Var(2.into())), box Var(2.into())),
+                    box Abs(box Sort(0.into()), box Var(1.into())),
+                    box App(
+                        box Abs(box Sort(0.into()), box Var(2.into())),
+                        box Var(2.into()),
+                    ),
                 ),
             ),
         );
 
         let term_step_6 = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
-                box App(box Abs(box Prop, box Var(2.into())), box Var(2.into())),
+                box Sort(0.into()),
+                box App(
+                    box Abs(box Sort(0.into()), box Var(2.into())),
+                    box Var(2.into()),
+                ),
             ),
         );
 
         // λa.λb.b
-        let term_step_7 = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
+        let term_step_7 = Abs(
+            box Sort(0.into()),
+            box Abs(box Sort(0.into()), box Var(1.into())),
+        );
 
         let env = Environment::new();
 
-        assert_eq!(term.beta_reduction(&env), term_step_1);
-        assert_eq!(term_step_1.beta_reduction(&env), term_step_2);
-        assert_eq!(term_step_2.beta_reduction(&env), term_step_3);
-        assert_eq!(term_step_3.beta_reduction(&env), term_step_4);
-        assert_eq!(term_step_4.beta_reduction(&env), term_step_5);
-        assert_eq!(term_step_5.beta_reduction(&env), term_step_6);
-        assert_eq!(term_step_6.beta_reduction(&env), term_step_7);
-        assert_eq!(term_step_7.beta_reduction(&env), term_step_7);
+        assert_eq!(term.beta_reduction(&env).unwrap(), term_step_1);
+        assert_eq!(term_step_1.beta_reduction(&env).unwrap(), term_step_2);
+        assert_eq!(term_step_2.beta_reduction(&env).unwrap(), term_step_3);
+        assert_eq!(term_step_3.beta_reduction(&env).unwrap(), term_step_4);
+        assert_eq!(term_step_4.beta_reduction(&env).unwrap(), term_step_5);
+        assert_eq!(term_step_5.beta_reduction(&env).unwrap(), term_step_6);
+        assert_eq!(term_step_6.beta_reduction(&env).unwrap(), term_step_7);
+        assert_eq!(term_step_7.beta_reduction(&env).unwrap(), term_step_7);
     }
 
     #[test]
     fn shift_prod() {
         let t1 = Prod(box Var(1.into()), box Var(1.into()));
-        let t2 = App(box Abs(box Prop, box t1.clone()), box Prop);
+        let t2 = App(
+            box Abs(box Sort(0.into()), box t1.clone()),
+            box Sort(0.into()),
+        );
 
-        assert_eq!(t2.beta_reduction(&Environment::new()), t1)
+        assert_eq!(t2.beta_reduction(&Environment::new()).unwrap(), t1)
     }
 
     #[test]
     fn beta_red_const() {
-        let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+        let id_prop = Prod(
+            box Sort(0.into()),
+            box Prod(box Var(1.into()), box Var(1.into())),
+        );
         let mut env = Environment::new();
-        env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
+        env.insert_def("foo".into(), id_prop.clone(), Sort(0.into()))
+            .unwrap();
+
+        assert_eq!(
+            Const("foo".into(), Vec::new())
+                .beta_reduction(&env)
+                .unwrap(),
+            id_prop
+        );
+    }
 
-        assert_eq!(Const("foo".into()).beta_reduction(&env), id_prop);
+    #[test]
+    fn poly_univ_id() {
+        let id_ty = Prod(
+            box Sort(UniverseLevel::Var(0)),
+            box Prod(box Var(1.into()), box Var(2.into())),
+        );
+        let id_te = Abs(
+            box Sort(UniverseLevel::Var(0)),
+            box Abs(box Var(1.into()), box Var(1.into())),
+        );
+        let id_zero = Abs(
+            box Sort(0.into()),
+            box Abs(box Var(1.into()), box Var(1.into())),
+        );
+        assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
+        let mut binding = Environment::new();
+        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())
     }
 }

kernel/src/type_checker.rs

 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::*;
 
@@ -45,19 +44,24 @@ impl Term {
     /// Conversion function, checks whether two terms are definitionally equal.
     ///
     /// 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,
+    fn conversion(
+        &self,
+        rhs: &Term,
+        env: &Environment,
+        lvl: DeBruijnIndex,
+    ) -> Result<bool, KernelError> {
+        match (self.whnf(env)?, rhs.whnf(env)?) {
+            (lhs, rhs) if lhs == rhs => Ok(true),
 
-            (Prop, Prop) => true,
+            (Sort(i), Sort(j)) => Ok(i.is_eq(&j)),
 
-            (Var(i), Var(j)) => i == j,
+            (Var(i), Var(j)) => Ok(i == j),
 
             (Prod(t1, u1), Prod(box t2, u2)) => {
                 let u1 = u1.substitute(&Var(lvl), lvl.into());
                 let u2 = u2.substitute(&Var(lvl), lvl.into());
 
-                t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl + 1.into())
+                Ok(t1.conversion(&t2, env, lvl)? && u1.conversion(&u2, env, lvl + 1.into())?)
             }
 
             // Since we assume that both vals already have the same type,
@@ -72,59 +76,45 @@ impl Term {
             }
 
             (App(box t1, box u1), App(box t2, box u2)) => {
-                t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl)
+                Ok(t1.conversion(&t2, env, lvl)? && u1.conversion(&u2, env, lvl)?)
             }
 
             (app @ App(box Abs(_, _), box _), u) | (u, app @ App(box Abs(_, _), box _)) => {
-                app.beta_reduction(env).conversion(&u, env, lvl)
+                app.beta_reduction(env)?.conversion(&u, env, lvl)
             }
 
-            _ => false,
+            _ => Ok(false),
         }
     }
 
     /// Checks whether two terms are definitionally equal.
     pub fn is_def_eq(&self, rhs: &Term, env: &Environment) -> Result<(), KernelError> {
-        self.conversion(rhs, env, 1.into())
+        self.conversion(rhs, env, 1.into())?
             .then_some(())
             .ok_or_else(|| KernelError::NotDefEq(self.clone(), rhs.clone()))
     }
 
     /// Computes universe the universe in which `(x : A) -> B` lives when `A : u1` and `B : u2`.
     fn imax(&self, rhs: &Term) -> Result<Term, KernelError> {
-        match rhs {
-            // Because Prop is impredicative, if B : Prop, then (x : A) -> b : Prop
-            Prop => Ok(Prop),
-
-            Type(ref i) => match self {
-                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()))),
-
-                _ => Err(KernelError::NotUniverse(self.clone())),
-            },
-
+        match (self, rhs) {
+            (Sort(u), Sort(v)) => Ok(Sort(UniverseLevel::IMax(box u.clone(), box v.clone()))),
+            (Sort(_), _) => Err(KernelError::NotUniverse(rhs.clone())),
             _ => Err(KernelError::NotUniverse(rhs.clone())),
         }
     }
 
     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())),
+            Sort(i) => Ok(Sort(i.clone() + 1)),
             Var(i) => Ok(ctx.types[ctx.lvl - *i].clone()),
 
-            Const(s) => match env.get_type(s) {
-                Some(ty) => Ok(ty),
-                None => Err(KernelError::ConstNotFound(s.clone())),
-            },
+            Const(s, vec) => env.get_type(s, vec),
 
             Prod(box t, u) => {
                 let univ_t = t._infer(env, ctx)?;
                 let univ_u = u._infer(env, ctx.clone().bind(t))?;
 
-                univ_t.normal_form(env).imax(&univ_u.normal_form(env))
+                univ_t.normal_form(env)?.imax(&univ_u.normal_form(env)?)
             }
 
             Abs(box t, u) => {
@@ -138,7 +128,7 @@ impl Term {
                     let typ_rhs = u._infer(env, ctx)?;
 
                     typ_lhs
-                        .conversion(&typ_rhs, env, ctx.types.len().into())
+                        .conversion(&typ_rhs, env, ctx.types.len().into())?
                         .then_some(*cls)
                         .ok_or_else(|| {
                             KernelError::WrongArgumentType(t.clone(), typ_lhs, u.clone(), typ_rhs)
@@ -160,7 +150,7 @@ impl Term {
         let ctx = &mut Context::new();
         let tty = self._infer(env, ctx)?;
 
-        tty.conversion(ty, env, ctx.types.len().into())
+        tty.conversion(ty, env, ctx.types.len().into())?
             .then_some(())
             .ok_or_else(|| KernelError::TypeMismatch(tty, ty.clone()))
     }
@@ -171,44 +161,50 @@ mod tests {
     use crate::type_checker::*;
 
     fn id(l: usize) -> Box<Term> {
-        box Abs(box Prop, box Var(l.into()))
+        box Abs(box Sort(0.into()), box Var(l.into()))
     }
 
     #[test]
     fn var_subst_1() {
         // (λ P. λP. 1) (λP.1)
         let t = App(
-            box Abs(box Prop, box Abs(box Prop, box Var(1.into()))),
+            box Abs(
+                box Sort(0.into()),
+                box Abs(box Sort(0.into()), box Var(1.into())),
+            ),
             id(1),
         );
 
-        let nf = Abs(box Prop, box Var(1.into()));
-        assert_eq!(t.normal_form(&Environment::new()), nf)
+        let nf = Abs(box Sort(0.into()), box Var(1.into()));
+        assert_eq!(t.normal_form(&Environment::new()).unwrap(), nf)
     }
 
     #[test]
     fn var_subst_2() {
         let t = App(
-            box Abs(box Prop, box Abs(box Prop, box Var(2.into()))),
+            box Abs(
+                box Sort(0.into()),
+                box Abs(box Sort(0.into()), box Var(2.into())),
+            ),
             id(1),
         );
 
-        let nf = Abs(box Prop, id(1));
-        assert_eq!(t.normal_form(&Environment::new()), nf)
+        let nf = Abs(box Sort(0.into()), id(1));
+        assert_eq!(t.normal_form(&Environment::new()).unwrap(), nf)
     }
 
     #[test]
     fn simple() {
         let t1 = App(
-            box Abs(box Type(BigUint::from(0_u64).into()), box Var(1.into())),
-            box Prop,
+            box Abs(box Sort(1.into()), box Var(1.into())),
+            box Sort(0.into()),
         );
 
-        let t2 = Prop;
-        assert!(t1.conversion(&t2, &Environment::new(), 0.into()));
+        let t2 = Sort(0.into());
+        assert!(t1.conversion(&t2, &Environment::new(), 0.into()).unwrap());
 
         let ty = t1.infer(&Environment::new());
-        assert_eq!(ty, Ok(Type(BigUint::from(0_u64).into())));
+        assert_eq!(ty, Ok(Sort(1.into())));
     }
 
     #[test]
@@ -216,15 +212,21 @@ mod tests {
         // λ (x : P -> P).(λ (y :P).x y) x
         //λ P -> P.(λ P.2 1) 1
         let term = Abs(
-            box Prod(box Prop, box Prop),
+            box Prod(box Sort(0.into()), box Sort(0.into())),
             box App(
-                box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+                box Abs(
+                    box Sort(0.into()),
+                    box App(box Var(2.into()), box Var(1.into())),
+                ),
                 box Var(1.into()),
             ),
         );
 
         // λx.x x
-        let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
+        let reduced = Abs(
+            box Sort(0.into()),
+            box App(box Var(1.into()), box Var(1.into())),
+        );
         assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
         assert!(term.infer(&Environment::new()).is_err());
     }
@@ -239,34 +241,40 @@ mod tests {
                     // (P → P) → ((P → P) → P)
                     box Prod(
                         // P -> P
-                        box Prod(box Prop, box Prop),
+                        box Prod(box Sort(0.into()), box Sort(0.into())),
                         // (P -> P) -> P
-                        box Prod(box Prod(box Prop, box Prop), box Prop),
+                        box Prod(
+                            box Prod(box Sort(0.into()), box Sort(0.into())),
+                            box Sort(0.into()),
+                        ),
                     ),
                     // (P → P) → ((P → P) → P)
                     box Prod(
                         // P -> P
-                        box Prod(box Prop, box Prop),
+                        box Prod(box Sort(0.into()), box Sort(0.into())),
                         // (P -> P) -> P
-                        box Prod(box Prod(box Prop, box Prop), box Prop),
+                        box Prod(
+                            box Prod(box Sort(0.into()), box Sort(0.into())),
+                            box Sort(0.into()),
+                        ),
                     ),
                 ),
                 box Abs(
                     // b : P
-                    box Prop,
+                    box Sort(0.into()),
                     box Abs(
                         // c : P
-                        box Prop,
+                        box Sort(0.into()),
                         box App(
                             box App(
                                 box App(
                                     box Var(3.into()),
                                     box Abs(
                                         // d : P -> P
-                                        box Prod(box Prop, box Prop),
+                                        box Prod(box Sort(0.into()), box Sort(0.into())),
                                         box Abs(
                                             // e : P -> P
-                                            box Prod(box Prop, box Prop),
+                                            box Prod(box Sort(0.into()), box Sort(0.into())),
                                             box App(
                                                 box Var(1.into()),
                                                 box App(box Var(2.into()), box Var(4.into())),
@@ -275,10 +283,10 @@ mod tests {
                                     ),
                                 ),
                                 // _ : P
-                                box Abs(box Prop, box Var(2.into())),
+                                box Abs(box Sort(0.into()), box Var(2.into())),
                             ),
                             //d : P
-                            box Abs(box Prop, box Var(1.into())),
+                            box Abs(box Sort(0.into()), box Var(1.into())),
                         ),
                     ),
                 ),
@@ -286,19 +294,25 @@ mod tests {
             box Abs(
                 //a : (P -> P) -> (P -> P) -> P
                 box Prod(
-                    box Prod(box Prop, box Prop),
-                    box Prod(box Prod(box Prop, box Prop), box Prop),
+                    box Prod(box Sort(0.into()), box Sort(0.into())),
+                    box Prod(
+                        box Prod(box Sort(0.into()), box Sort(0.into())),
+                        box Sort(0.into()),
+                    ),
                 ),
                 box Abs(
                     //b : P -> P
-                    box Prod(box Prop, box Prop),
+                    box Prod(box Sort(0.into()), box Sort(0.into())),
                     box App(box Var(2.into()), box Var(1.into())),
                 ),
             ),
         );
 
         // λa : P.λb : P .b
-        let reduced = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
+        let reduced = Abs(
+            box Sort(0.into()),
+            box Abs(box Sort(0.into()), box Var(1.into())),
+        );
         assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
         assert!(term.infer(&Environment::new()).is_ok())
     }
@@ -307,9 +321,12 @@ mod tests {
     #[test]
     fn nf_test() {
         //λa.a (λx.x) (λx.x)
-        let reduced = Abs(box Prop, box App(box App(box Var(2.into()), id(1)), id(1)));
+        let reduced = Abs(
+            box Sort(0.into()),
+            box App(box App(box Var(2.into()), id(1)), id(1)),
+        );
 
-        let nff = reduced.clone().normal_form(&Environment::new());
+        let nff = reduced.clone().normal_form(&Environment::new()).unwrap();
         assert_eq!(reduced, nff);
         assert!(reduced.is_def_eq(&nff, &Environment::new()).is_ok());
     }
@@ -317,7 +334,7 @@ mod tests {
     #[test]
     fn polymorphism() {
         let id = Abs(
-            box Type(BigUint::from(0_u64).into()),
+            box Sort(0.into()),
             box Abs(box Var(1.into()), box Var(1.into())),
         );
 
@@ -326,48 +343,54 @@ mod tests {
 
     #[test]
     fn type_type() {
-        assert!(Type(BigUint::from(0_u64).into())
-            .check(&Type(BigUint::from(1_u64).into()), &Environment::new())
+        assert!(Sort(0.into())
+            .check(&Sort(1.into()), &Environment::new())
             .is_ok());
     }
 
     #[test]
     fn not_function() {
-        let t = App(box Prop, box Prop);
+        let t = App(box Sort(0.into()), box Sort(0.into()));
         assert!(t.infer(&Environment::new()).is_err())
     }
 
     #[test]
     fn not_type_prod() {
-        let t = Prod(box Abs(box Prop, box Var(1.into())), box Prop);
+        let t = Prod(
+            box Abs(box Sort(0.into()), box Var(1.into())),
+            box Sort(0.into()),
+        );
         assert!(t.infer(&Environment::new()).is_err());
 
-        let t = Prod(box Prop, box Abs(box Prop, box Prop));
+        let t = Prod(
+            box Sort(0.into()),
+            box Abs(box Sort(0.into()), box Sort(0.into())),
+        );
         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());
+        let wf_prod = Prod(box Sort(0.into()), box Sort(0.into()));
+        println!("{:?}", wf_prod.infer(&Environment::new()));
+        assert!(wf_prod.check(&Sort(1.into()), &Environment::new()).is_ok());
 
-        let wf_prod = Prod(box Prop, box Var(1.into()));
-        assert!(wf_prod.check(&Prop, &Environment::new()).is_ok());
+        let wf_prod = Prod(box Sort(0.into()), box Var(1.into()));
+        assert!(wf_prod.check(&Sort(0.into()), &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());
+        // Sort0 -> (A : Sort(0.into())) ->
+        let wf_prod = Prod(box Sort(0.into()), box Sort(0.into()));
+        assert!(wf_prod.check(&Sort(1.into()), &Environment::new()).is_ok());
     }
 
     #[test]
     fn poly_test2() {
         let t = Abs(
-            box Prop,
+            box Sort(0.into()),
             box Abs(
-                box Prop,
+                box Sort(0.into()),
                 box Abs(
-                    box Prod(box Prop, box Prod(box Prop, box Prop)),
+                    box Prod(
+                        box Sort(0.into()),
+                        box Prod(box Sort(0.into()), box Sort(0.into())),
+                    ),
                     box App(
                         box App(box Var(1.into()), box Var(3.into())),
                         box Var(2.into()),
@@ -381,54 +404,77 @@ mod tests {
 
     #[test]
     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();
-
-        assert!(t.check(&Const("foo".into()), &env).is_ok());
-        assert!(id_prop.is_def_eq(&Const("foo".into()), &env).is_ok());
+        let id_prop = Prod(
+            box Sort(0.into()),
+            box Prod(box Var(1.into()), box Var(2.into())),
+        );
+        let t = Abs(
+            box Sort(0.into()),
+            box Abs(box Var(1.into()), box Var(1.into())),
+        );
+        let mut binding = Environment::new();
+        let env = binding
+            .insert_def("foo".into(), id_prop.clone(), Sort(0.into()))
+            .unwrap();
+
+        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]
     fn check_bad() {
-        assert!(Prop.check(&Prop, &Environment::new()).is_err());
+        assert!(Sort(0.into())
+            .check(&Sort(0.into()), &Environment::new())
+            .is_err());
     }
 
     #[test]
     fn not_def_eq() {
-        assert!(Prop
-            .is_def_eq(&Type(BigUint::from(0_u64).into()), &Environment::new())
+        assert!(Sort(0.into())
+            .is_def_eq(&Sort(1.into()), &Environment::new())
             .is_err());
     }
 
     #[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();
-
-        assert!(Const("foo".into()).infer(&env).is_ok());
-        assert!(Const("foo".into()).infer(&Environment::new()).is_err());
+        let id_prop = Prod(
+            box Sort(0.into()),
+            box Prod(box Var(1.into()), box Var(1.into())),
+        );
+        let mut binding = Environment::new();
+        let env = binding
+            .insert_def("foo".into(), id_prop, Sort(0.into()))
+            .unwrap();
+
+        assert!(Const("foo".into(), Vec::new()).infer(env).is_ok());
+        assert!(Const("foo".into(), Vec::new())
+            .infer(&Environment::new())
+            .is_err());
     }
 
     #[test]
     fn prod_var() {
-        let ty = 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 ty = Prod(
+            box Sort(0.into()),
+            box Prod(box Var(1.into()), box Var(2.into())),
+        );
+        let t = Abs(
+            box Sort(0.into()),
+            box Abs(box Var(1.into()), box Var(1.into())),
+        );
         assert!(t.check(&ty, &Environment::new()).is_ok())
     }
 
     #[test]
     fn univ_reduc() {
         let ty = App(
-            box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
-            box Prod(box Prop, box Var(1.into())),
+            box Abs(box Sort(0.into()), box Sort(0.into())),
+            box Prod(box Sort(0.into()), box Var(1.into())),
         );
-        assert!(ty.conversion(
-            &Type(BigUint::from(0_u64).into()),
-            &Environment::new(),
-            0.into()
-        ))
+        assert!(ty
+            .conversion(&Sort(0.into()), &Environment::new(), 0.into())
+            .unwrap())
     }
 }

kernel/src/universe.rs

+use std::fmt::Display;
+use std::fmt::Formatter;
+use std::ops::Add;
+
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub enum UniverseLevel {
+    #[default]
+    Zero,
+
+    Succ(Box<UniverseLevel>),
+
+    Max(Box<UniverseLevel>, Box<UniverseLevel>),
+
+    IMax(Box<UniverseLevel>, Box<UniverseLevel>),
+
+    Var(usize),
+}
+
+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))
+        }
+    }
+}
+
+impl From<usize> for UniverseLevel {
+    fn from(n: usize) -> Self {
+        if n == 0 {
+            Zero
+        } else {
+            Succ(box (n - 1).into())
+        }
+    }
+}
+
+impl Display for UniverseLevel {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.pretty_print())
+    }
+}
+
+use UniverseLevel::*;
+
+impl UniverseLevel {
+    /// Helper function for pretty printing, if universe doesn't contain any variable then it gets printed as a decimal number.
+    fn to_numeral(&self) -> Option<usize> {
+        match self {
+            Zero => Some(0),
+            Succ(box u) => u.to_numeral().map(|n| n + 1),
+            Max(box n, box m) => n
+                .to_numeral()
+                .and_then(|n| m.to_numeral().map(|m| n.max(m))),
+            IMax(box n, box m) => m.to_numeral().and_then(|m| {
+                if m == 0 {
+                    0.into()
+                } else {
+                    n.to_numeral().map(|n| m.max(n))
+                }
+            }),
+            _ => None,
+        }
+    }
+
+    /// Helper function for pretty printing, if universe is of the form Succ(Succ(...(Succ(u))...)) then it gets printed as u+n.
+    fn plus(&self) -> (UniverseLevel, usize) {
+        match self {
+            Succ(box u) => {
+                let (u, n) = u.plus();
+                (u, n + 1)
+            }
+            _ => (self.clone(), 0),
+        }
+    }
+    /// Pretty prints universe levels, used to impl Display for UniverseLevel.
+    fn pretty_print(&self) -> String {
+        match self.to_numeral() {
+            Some(n) => n.to_string(),
+            None => match self {
+                Zero => unreachable!("Zero is a numeral"),
+                Succ(_) => {
+                    let (u, n) = self.plus();
+                    format!("{} + {}", u.pretty_print(), n)
+                }
+                Max(box n, box m) => format!("max ({}) ({})", n.pretty_print(), m.pretty_print()),
+                IMax(box _, box Zero) => "Zero".into(),
+                IMax(box n, box m @ Succ(_)) => {
+                    format!("max ({}) ({})", n.pretty_print(), m.pretty_print())
+                }
+                IMax(box n, box m) => format!("imax ({}) ({})", n.pretty_print(), m.pretty_print()),
+                Var(n) => format!("u{}", n),
+            },
+        }
+    }
+
+    /// Is used to find the number of universe in a declaration.
+    pub fn univ_vars(self) -> usize {
+        match self {
+            Zero => 0,
+            Succ(n) => n.univ_vars(),
+            Max(n, m) => n.univ_vars().max(m.univ_vars()),
+            IMax(n, m) => n.univ_vars().max(m.univ_vars()),
+            Var(n) => n + 1,
+        }
+    }
+
+    /// 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,
+            Succ(n) => Succ(box n.substitute_single(var, u)),
+            Max(n, m) => Max(
+                box n.substitute_single(var, u.clone()),
+                box m.substitute_single(var, u),
+            ),
+            IMax(n, m) => IMax(
+                box n.substitute_single(var, u.clone()),
+                box m.substitute_single(var, u),
+            ),
+            Var(n) => {
+                if n == var {
+                    u
+                } else {
+                    Var(n)
+                }
+            }
+        }
+    }
+
+    /// 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,
+            Succ(v) => Succ(box v.substitute(univs)),
+            Max(u1, u2) => Max(box u1.substitute(univs), box u2.substitute(univs)),
+            IMax(u1, u2) => IMax(box u1.substitute(univs), box u2.substitute(univs)),
+            Var(var) => univs[var].clone(),
+        }
+    }
+
+    /// Helper function for universe comparison. normalizes imax(es) as follows:
+    /// imax(0, u) = u
+    /// imax(u, 0) = u
+    /// imax(u, S(v)) = max(u, S(v))
+    /// imax(u, imax(v, w)) = max(imax(u, w), imax(v, w))
+    /// imax(u, max(v, w)) = max(imax(u, v), imax(u, w))
+    ///
+    /// Here, the imax normalization pushes imaxes to all have a Var(i) as the second argument. To solve this last case, one needs to substitute
+    /// Var(i) with 0 and S(Var(i)). This gives us a consistent way to unstuck the geq-checking.
+    fn normalize(&self) -> Self {
+        match self {
+            IMax(box Zero, box u) => u.clone(),
+            IMax(_, box Zero) => Zero,
+            IMax(box u, box Succ(v)) => Max(box u.normalize(), box Succ(v.clone())).normalize(),
+            IMax(box u, box IMax(box v, box w)) => Max(
+                box IMax(box u.clone(), box w.clone()).normalize(),
+                box IMax(box v.clone(), box w.clone()).normalize(),
+            ),
+            IMax(box u, box Max(box v, box w)) => Max(
+                box IMax(box u.clone(), box v.clone()).normalize(),
+                box IMax(box u.clone(), box w.clone()).normalize(),
+            ),
+            _ => self.clone(),
+        }
+    }
+
+    // checks whether u1 <= u2 + n
+    // returns:
+    // -   (true,0) if u1 <= u2 + n,
+    // -   (false,0) if !(u1 <= u2 + n),
+    // -   (false,i+1) if Var(i) needs to be substituted to unstuck the comparison.
+    fn geq_no_subst(&self, u2: &UniverseLevel, n: i64) -> (bool, usize) {
+        match (self.normalize(), u2.normalize()) {
+            (Zero, _) if n >= 0 => (true, 0),
+            (_, _) if *self == *u2 && n >= 0 => (true, 0),
+            (Succ(l), _) if l.geq_no_subst(u2, n - 1).0 => (true, 0),
+            (_, Succ(box l)) if self.geq_no_subst(&l, n + 1).0 => (true, 0),
+            (_, Max(box l1, box l2))
+                if self.geq_no_subst(&l1, n).0 || self.geq_no_subst(&l2, n).0 =>
+            {
+                (true, 0)
+            }
+            (Max(box l1, box l2), _) if l1.geq_no_subst(u2, n).0 && l2.geq_no_subst(u2, n).0 => {
+                (true, 0)
+            }
+            (_, IMax(_, box Var(i))) | (IMax(_, box Var(i)), _) => (false, i + 1),
+            _ => (false, 0),
+        }
+    }
+
+    /// 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,
+            (false, 0) => false,
+            (false, i) => {
+                self.clone()
+                    .substitute_single(i - 1, Zero)
+                    .geq(&u2.clone().substitute_single(i - 1, Zero), n)
+                    && self
+                        .clone()
+                        .substitute_single(i - 1, Succ(box Var(i - 1)))
+                        .geq(
+                            &u2.clone().substitute_single(i - 1, Succ(box Var(i - 1))),
+                            n,
+                        )
+            }
+        }
+    }
+
+    pub fn is_eq(&self, u2: &UniverseLevel) -> bool {
+        self.geq(u2, 0) && u2.geq(self, 0)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::universe::UniverseLevel::*;
+
+    mod pretty_printing {
+        use crate::universe::UniverseLevel::*;
+
+        #[test]
+        fn to_num() {
+            assert_eq!(Max(box Succ(box Zero), box Zero).to_numeral(), Some(1));
+            assert_eq!(
+                Max(box Succ(box Zero), box Succ(box Var(0))).to_numeral(),
+                None
+            );
+            assert_eq!(IMax(box Var(0), box Zero).to_numeral(), Some(0));
+            assert_eq!(IMax(box Zero, box Succ(box Zero)).to_numeral(), Some(1))
+        }
+
+        #[test]
+        fn to_plus() {
+            assert_eq!(Succ(box Zero).plus(), (Zero, 1));
+        }
+
+        #[test]
+        fn to_pretty_print() {
+            assert_eq!(
+                Max(
+                    box Succ(box Zero),
+                    box IMax(box Max(box Zero, box Var(0)), box Succ(box Var(0)))
+                )
+                .pretty_print(),
+                "max (1) (imax (max (0) (u0)) (u0 + 1))"
+            );
+        }
+    }
+
+    #[test]
+    fn univ_eq() {
+        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)))));
+        assert!(&Max(
+            box Zero,
+            box IMax(box Zero, box Max(box Succ(box Zero), box Zero))
+        )
+        .is_eq(&IMax(
+            box Succ(box Zero),
+            box IMax(box Succ(box Zero), box Succ(box Zero))
+        )));
+        assert!(&Var(0).is_eq(&IMax(box Var(0), box Var(0))));
+        assert!(&IMax(box Succ(box Zero), box Max(box Zero, box Zero)).is_eq(&Zero));
+        assert!(!&IMax(box Var(0), box Var(1)).is_eq(&IMax(box Var(1), box Var(0))))
+    }
+
+    #[test]
+    fn univ_vars_count() {
+        assert_eq!(
+            IMax(
+                box Zero,
+                box Max(box Succ(box Zero), box Max(box Var(0), box Var(1)))
+            )
+            .univ_vars(),
+            2
+        )
+    }
+
+    #[test]
+    fn subst() {
+        let lvl = IMax(
+            box Zero,
+            box 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),
+            IMax(
+                box Zero,
+                box Max(box Succ(box Zero), box Max(box Succ(box Zero), box Zero))
+            )
+        )
+    }
+
+    #[test]
+    fn single_subst() {
+        let lvl = IMax(box Max(box Succ(box Zero), box Var(0)), box Var(0));
+        assert_eq!(
+            lvl.substitute_single(0, Zero),
+            IMax(box Max(box Succ(box Zero), box Zero), box Zero)
+        )
+    }
+}

parser/src/term.pest

 WHITESPACE = _{ WHITE_SPACE }
 COMMENT = _{ "//" ~ (!"\n" ~ ANY)* }
+eoi = _{ !ANY }
+keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" | "Sort" ) ~ !ASCII_ALPHANUMERIC }
 number = @{ ASCII_DIGIT+ }
 string = @{ !keywords ~ ASCII_ALPHA ~ ( "_" | ASCII_ALPHANUMERIC )* }
-keywords = @{ ( "fun" | "def" | "check" | "Prop" | "Type" ) ~ !ASCII_ALPHANUMERIC }
-eoi = _{ !ANY }
 
-Term = _{ Abs | dProd | Prod | App | Var | Prop | Type | "(" ~ Term ~ ")" }
-term_prod = _{ App | Abs | dProd | Var | Prop | Type | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
-term_app = _{ Abs | Var | Prop | Type | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" } 
-term_dprod = _{ App | Abs | Prod | dProd | Var | Prop | Type | "(" ~ term_dprod ~ ")" }
-term_abs = _{ App | Abs | Prod | dProd | Var | Prop | Type | "(" ~ term_abs ~ ")" }
+Term = _{ Abs | dProd | Prod | App | Var | Prop | Type | Sort | "(" ~ Term ~ ")" }
+term_prod = _{ App | Abs | dProd | Var | Prop | Type | Sort | "(" ~ Prod ~ ")" | "(" ~ term_prod ~ ")" }
+term_app = _{ Abs | Var | Prop | Type | Sort | "(" ~ App ~ ")" | "(" ~ Prod ~ ")" | "(" ~ dProd ~ ")" | "(" ~ term_app ~ ")" } 
+term_dprod = _{ App | Abs | Prod | dProd | Var | Prop | Type | Sort | "(" ~ term_dprod ~ ")" }
+term_abs = _{ App | Abs | Prod | dProd | Var | Prop | Type | Sort | "(" ~ term_abs ~ ")" }
 
 Abs = { ( "fun" ~ ( arg_abs_par ~ ( "," ~ arg_abs_par )* ) ~ "=>" ~ Term ) }
 arg_abs_par = _{ arg_abs | "(" ~ arg_abs_par ~ ")" }
@@ -21,14 +21,25 @@ arg_dprod = { string+ ~ ":" ~ term_dprod }
 
 App = { term_app ~ term_app+ }
 Prod = { term_prod ~ ( "->" ~ term_prod )+ }
-
 Prop = { "Prop" }
-Type = { "Type(" ~ number ~ ")" | "Type" ~ number? }
-Var = { string }
 
-Command = _{ Define | CheckType | GetType | DefineCheckType }
-Define = { "def" ~ string ~ ":=" ~ Term }
-DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term }
+Type = { "Type" ~ univ? }
+Sort = { "Sort" ~ univ? }
+univ = _{ Plus | Max | Num | string | "(" ~ univ ~ ")" }
+univ_plus = _{ Max | Num | string | "(" ~ univ ~ ")" }
+Num = { number }
+Plus = { univ_plus ~ ( "+" ~ number )+ }
+Max = { ( "max" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "max" ~ univ ~ univ ) }
+
+Var = { string ~ arg_univ? }
+arg_univ = {".{" ~ (univ ~ ("," ~ univ)*)? ~ "}"}
+
+univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"}
+
+Command = _{ Eval | Define | CheckType | GetType | DefineCheckType }
+Eval = { "eval" ~ Term }
+Define = { "def" ~ string ~ univ_decl? ~ ":=" ~ Term }
+DefineCheckType = { "def" ~ string ~ univ_decl? ~ ":" ~ Term ~ ":=" ~ Term }
 CheckType = { "check" ~ Term ~ ":" ~ Term }
 GetType = { "check" ~ Term }