[ #7 ] First step towards universe levels

samples/basics/syntacic-sugar.out

@@ -1,6 +1,6 @@
 Parse successful.
-let a: Type = 1;
-let b: Type = 1;
+let a: Type0 = 1;
+let b: Type0 = 1;
 let f: Π _: a. b = λ x. x;
 let p: Σ _: a. b = (0, 0);
 const infer_my_type = (1, 1);

src/ast.rs

@@ -10,13 +10,13 @@ pub enum Expression {
     Unit,
     /// `1`
     One,
-    /// `U`
-    Type,
+    /// `Type`
+    Type(u32),
     /// Empty file
     Void,
     /// `bla`
     Var(String),
-    /// `sum { Bla x }`
+    /// `Sum { Bla x }`
     Sum(Branch),
     /// `split { Bla x => y }`
     Split(Branch),
@@ -99,7 +99,7 @@ pub enum Value {
     /// Canonical form: unit type.
     One,
     /// Canonical form: type universe.
-    Type,
+    Type(u32),
     /// Canonical form: pi type (type for dependent functions).
     Pi(Box<Self>, Closure),
     /// Canonical form: sigma type (type for dependent pair).
@@ -229,7 +229,7 @@ pub enum GenericTelescope<Value: Clone> {
     /// recursive declaration as an `Expression` (which is a member of `Declaration`) here.
     ///
     /// The problem is quite complicated and can be reproduced by checking out 0.1.5 revision and
-    /// type-check this code:
+    /// type-check this code (`Type` was `U` and `Sum` was `sum` at that time):
     ///
     /// ```ignore
     /// rec nat : U = sum { Zero 1 | Suc nat };

src/check/expr.rs

@@ -14,7 +14,8 @@ pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM<Value> {
     use crate::ast::Expression::*;
     match expression {
         Unit => Ok(Value::One),
-        Type | Void | One => Ok(Value::Type),
+        Type(level) => Ok(Value::Type(level + 1)),
+        Void | One => Ok(Value::Type(0)),
         Var(name) => tcs
             .gamma
             .get(&name)
@@ -48,15 +49,17 @@ pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM<Value> {
             for (_name, branch) in branches.into_iter() {
                 check_type(index, tcs_borrow!(tcs), *branch)?;
             }
-            Ok(Value::Type)
+            // Do we need to find the highest level of each branch?
+            Ok(Value::Type(0))
         }
         Pi((pattern, input), output) | Sigma((pattern, input), output) => {
             let tcs = check_type(index, tcs, *input.clone())?;
             let input_type = input.eval(tcs.context());
             let generated = generate_value(index);
             let gamma = update_gamma(tcs.gamma, &pattern, input_type, generated)?;
             check_type(index + 1, TCS::new(gamma, tcs.context), *output)?;
-            Ok(Value::Type)
+            // Does this need to depend on the level of the return type?
+            Ok(Value::Type(0))
         }
         Application(function, argument) => match *function {
             Lambda(pattern, Some(parameter_type), return_value) => {
@@ -83,15 +86,18 @@ pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM<Value> {
 
 /// `checkT` in Mini-TT.<br/>
 /// Check if an expression is a well-typed type expression.
+///
+/// TODO: return the level
 pub fn check_type(index: u32, tcs: TCS, expression: Expression) -> TCM<TCS> {
     use crate::ast::Expression::*;
     match expression {
-        Sum(constructors) => check_sum_type(index, tcs, constructors),
+        Sum(constructors) => check_sum_type(index, tcs, constructors, 0),
         Pi((pattern, first), second) | Sigma((pattern, first), second) => {
-            check_telescoped(index, tcs, pattern, *first, *second)
+            check_telescoped(index, tcs, pattern, *first, *second, 0)
         }
-        Type | Void | One => Ok(tcs),
-        expression => check(index, tcs, expression, Value::Type),
+        Type(_level) => Ok(tcs),
+        Void | One => Ok(tcs),
+        expression => check(index, tcs, expression, Value::Type(0)),
     }
 }
 
@@ -101,7 +107,14 @@ pub fn check(index: u32, tcs: TCS, expression: Expression, value: Value) -> TCM<
     use crate::ast::Expression as E;
     use crate::ast::Value as V;
     match (expression, value) {
-        (E::Unit, V::One) | (E::Type, V::Type) | (E::One, V::Type) => Ok(tcs),
+        (E::Unit, V::One) | (E::One, V::Type(0)) => Ok(tcs),
+        (E::Type(low), V::Type(high)) => {
+            if high > low {
+                Ok(tcs)
+            } else {
+                Err(TCE::TypeMismatch(V::Type(low + 1), V::Type(high)))
+            }
+        }
         // There's nothing left to check.
         (E::Void, _) => Ok(tcs),
         (E::Lambda(pattern, _, body), V::Pi(signature, closure)) => {
@@ -134,10 +147,10 @@ pub fn check(index: u32, tcs: TCS, expression: Expression, value: Value) -> TCM<
             let constructor_type = reduce_to_value(constructor, *constructors.environment);
             check(index, tcs, *body, constructor_type)
         }
-        (E::Sum(constructors), V::Type) => check_sum_type(index, tcs, constructors),
-        (E::Sigma((pattern, first), second), V::Type)
-        | (E::Pi((pattern, first), second), V::Type) => {
-            check_telescoped(index, tcs, pattern, *first, *second)
+        (E::Sum(constructors), V::Type(level)) => check_sum_type(index, tcs, constructors, level),
+        (E::Sigma((pattern, first), second), V::Type(level))
+        | (E::Pi((pattern, first), second), V::Type(level)) => {
+            check_telescoped(index, tcs, pattern, *first, *second, level)
         }
         (E::Declaration(declaration, rest), rest_type) => {
             let tcs = check_declaration(index, tcs, *declaration)?;
@@ -191,7 +204,7 @@ pub fn check_fallback(index: u32, tcs: TCS, body: Expression, signature: Value)
 }
 
 /// To reuse code that checks if a sum type is well-typed between `check_type` and `check`
-pub fn check_sum_type(index: u32, tcs: TCS, constructors: Branch) -> TCM<TCS> {
+pub fn check_sum_type(index: u32, tcs: TCS, constructors: Branch, _level: u32) -> TCM<TCS> {
     for constructor in constructors.values().cloned() {
         check_type(index, tcs_borrow!(tcs), *constructor)?;
     }
@@ -205,6 +218,7 @@ pub fn check_telescoped(
     pattern: Pattern,
     first: Expression,
     second: Expression,
+    _level: u32,
 ) -> TCM<TCS> {
     check_type(index, tcs_borrow!(tcs), first.clone())?;
     let TCS { gamma, context } = tcs;

src/check/read_back.rs

@@ -23,7 +23,7 @@ pub enum NormalExpression {
     Pair(Box<Self>, Box<Self>),
     Unit,
     One,
-    Type,
+    Type(u32),
     Pi(Box<Self>, u32, Box<Self>),
     Sigma(Box<Self>, u32, Box<Self>),
     Constructor(String, Box<Self>),
@@ -79,7 +79,7 @@ impl ReadBack for Value {
             }
             Value::Unit => Unit,
             Value::One => One,
-            Value::Type => Type,
+            Value::Type(level) => Type(level),
             Value::Pi(input, output) => {
                 let output = output
                     .instantiate(generate_value(index))

src/check/tests.rs

@@ -6,14 +6,14 @@ fn simple_check() {
     check_declaration_main(Declaration::simple(
         Pattern::Unit,
         vec![],
-        Expression::Type,
+        Expression::Type(0),
         Expression::One,
     ))
     .unwrap();
     let error_message = check_declaration_main(Declaration::simple(
         Pattern::Unit,
         vec![],
-        Expression::Type,
+        Expression::Type(0),
         Expression::Unit,
     ))
     .unwrap_err();

src/eval.rs

@@ -163,7 +163,7 @@ impl Expression {
         match self {
             E::Unit => V::Unit,
             E::One => V::One,
-            E::Type => V::Type,
+            E::Type(level) => V::Type(level),
             E::Var(name) => context
                 .resolve(&name)
                 .map_err(|err| eprintln!("{}", err))

src/grammar.pest

@@ -43,7 +43,8 @@ single_arrow = _{ "->" | "\u{2192}" }
 let_or_rec = { "let" | "rec" }
 one = { "1" }
 unit = { "0" }
-universe = { "Type" }
+level = { ASCII_DIGIT* }
+universe = ${ "Type" ~ level }
 void = { EOI }
 meta_var = { "_" }
 

src/parser.rs

@@ -247,7 +247,7 @@ pub fn const_declaration_to_expression(the_rule: Tok) -> Expression {
 pub fn atom_to_expression(rules: Tok) -> Expression {
     let the_rule: Tok = rules.into_inner().next().unwrap();
     match the_rule.as_rule() {
-        Rule::universe => Expression::Type,
+        Rule::universe => universe_to_expression(the_rule),
         Rule::constructor => constructor_to_expression(the_rule),
         Rule::variable => variable_to_expression(the_rule),
         Rule::split => Expression::Split(choices_to_tree_map(the_rule)),
@@ -381,6 +381,16 @@ pub fn constructor_to_expression(the_rule: Tok) -> Expression {
     Expression::Constructor(constructor, Box::new(argument))
 }
 
+/// ```ignore
+/// level = { ASCII_DIGIT* }
+/// universe = @{ "Type" ~ level }
+/// ```
+pub fn universe_to_expression(the_rule: Tok) -> Expression {
+    let mut inner: Tik = the_rule.into_inner();
+    let level = inner.next().unwrap().as_str();
+    Expression::Type(level.parse().unwrap_or(0))
+}
+
 /// ```ignore
 /// constructor_name = @{ ASCII_ALPHA_UPPER ~ identifier? }
 /// constructor = { constructor_name ~ expression }
@@ -451,7 +461,7 @@ mod tests {
 
     #[test]
     fn simple_parse() {
-        successful_test_case("let unit_one : 1 = 0;\nlet type_one : Type = unit_one;");
+        successful_test_case("let unit_one : 1 = 0;\nlet type_one : Type0 = unit_one;");
         successful_test_case("let application : k = f e;");
         successful_test_case("let pair_first_second : k = ((x, y).1).2;");
         successful_test_case("let sigma_type : \\Sigma x : x_type . y = x, y;");

src/pretty.rs

@@ -23,7 +23,10 @@ impl Display for Value {
                 f.write_str("\u{03A0} ")?;
                 output.fmt_with_type(f, Some(&**input))
             }
-            Value::Type => f.write_str("Type"),
+            Value::Type(level) => {
+                f.write_str("Type")?;
+                level.fmt(f)
+            }
             Value::Sigma(first, second) => {
                 f.write_str("\u{03A3} ")?;
                 second.fmt_with_type(f, Some(&**first))
@@ -104,7 +107,10 @@ impl Display for Expression {
                 f.write_str(". ")?;
                 output.fmt(f)
             }
-            Expression::Type => f.write_str("Type"),
+            Expression::Type(level) => {
+                f.write_str("Type")?;
+                level.fmt(f)
+            }
             Expression::Sigma((pattern, first), second) => {
                 f.write_str("\u{03A3} ")?;
                 pattern.fmt(f)?;
@@ -304,7 +310,10 @@ impl Display for NormalExpression {
                 f.write_str(". ")?;
                 output.fmt(f)
             }
-            Expression::Type => f.write_str("Type"),
+            Expression::Type(level) => {
+                f.write_str("Type")?;
+                level.fmt(f)
+            }
             Expression::Sigma(first, index, second) => {
                 f.write_str("\u{03A3} <")?;
                 index.fmt(f)?;