From 7f01eb14c1a23f06329343ef9fd013393ccd351f Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 15 Mar 2019 21:43:39 -0400 Subject: [PATCH] [ #7 ] First step towards universe levels --- samples/basics/syntacic-sugar.out | 4 ++-- src/ast.rs | 10 ++++---- src/check/expr.rs | 40 +++++++++++++++++++++---------- src/check/read_back.rs | 4 ++-- src/check/tests.rs | 4 ++-- src/eval.rs | 2 +- src/grammar.pest | 3 ++- src/parser.rs | 14 +++++++++-- src/pretty.rs | 15 +++++++++--- 9 files changed, 65 insertions(+), 31 deletions(-) diff --git a/samples/basics/syntacic-sugar.out b/samples/basics/syntacic-sugar.out index 2e3f2d9..8097d37 100644 --- a/samples/basics/syntacic-sugar.out +++ b/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); diff --git a/src/ast.rs b/src/ast.rs index 5301d34..9fb36ad 100644 --- a/src/ast.rs +++ b/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, Closure), /// Canonical form: sigma type (type for dependent pair). @@ -229,7 +229,7 @@ pub enum GenericTelescope { /// 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 }; diff --git a/src/check/expr.rs b/src/check/expr.rs index 5e123f0..fcc99c1 100644 --- a/src/check/expr.rs +++ b/src/check/expr.rs @@ -14,7 +14,8 @@ pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM { 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,7 +49,8 @@ pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM { 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())?; @@ -56,7 +58,8 @@ pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM { 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 { /// `checkT` in Mini-TT.
/// 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 { 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 { +pub fn check_sum_type(index: u32, tcs: TCS, constructors: Branch, _level: u32) -> TCM { 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 { check_type(index, tcs_borrow!(tcs), first.clone())?; let TCS { gamma, context } = tcs; diff --git a/src/check/read_back.rs b/src/check/read_back.rs index afd49e4..f01c534 100644 --- a/src/check/read_back.rs +++ b/src/check/read_back.rs @@ -23,7 +23,7 @@ pub enum NormalExpression { Pair(Box, Box), Unit, One, - Type, + Type(u32), Pi(Box, u32, Box), Sigma(Box, u32, Box), Constructor(String, Box), @@ -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)) diff --git a/src/check/tests.rs b/src/check/tests.rs index 2b4334e..8be2e10 100644 --- a/src/check/tests.rs +++ b/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(); diff --git a/src/eval.rs b/src/eval.rs index 015d7bd..e6bea82 100644 --- a/src/eval.rs +++ b/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)) diff --git a/src/grammar.pest b/src/grammar.pest index 8b25fd2..1666f10 100644 --- a/src/grammar.pest +++ b/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 = { "_" } diff --git a/src/parser.rs b/src/parser.rs index c169281..07b8f38 100644 --- a/src/parser.rs +++ b/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;"); diff --git a/src/pretty.rs b/src/pretty.rs index c4c60b2..1bd3589 100644 --- a/src/pretty.rs +++ b/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)?;