From 95cfac426da0d0b87aad2eae602796ed70f119ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Aug 2013 18:25:34 -0700 Subject: [PATCH] Add parse_level. Fix bug at environment::is_ge Signed-off-by: Leonardo de Moura --- src/exprlib/printer.h | 4 ++ src/frontend/parser.cpp | 105 ++++++++++++++++++++++++++++++++++++- src/kernel/environment.cpp | 2 +- src/kernel/level.cpp | 4 +- src/kernel/level.h | 1 + src/shell/lean.cpp | 2 + 6 files changed, 113 insertions(+), 5 deletions(-) diff --git a/src/exprlib/printer.h b/src/exprlib/printer.h index 20519fcbf..f71e65ae1 100644 --- a/src/exprlib/printer.h +++ b/src/exprlib/printer.h @@ -18,3 +18,7 @@ std::ostream & operator<<(std::ostream & out, object const & obj); class environment; std::ostream & operator<<(std::ostream & out, environment const & env); } +void print(lean::expr const & a); +void print(lean::expr const & a, lean::context const & c); +void print(lean::context const & c); +void print(lean::environment const & e); diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp index af1a6acbf..c0f15c209 100644 --- a/src/frontend/parser.cpp +++ b/src/frontend/parser.cpp @@ -37,6 +37,15 @@ static name g_mixfixl_kwd("Mixfixl"); static name g_mixfixr_kwd("Mixfixr"); static name g_mixfixc_kwd("Mixfixc"); +// ========================================== +// Support for parsing levels +static name g_max_name("max"); +static name g_cup_name("\u2293"); +static name g_plus_name("+"); +static unsigned g_level_plus_prec = 10; +static unsigned g_level_cup_prec = 5; +// ========================================== + static name g_overload_name(name(name(name(0u), "parser"), "overload")); static expr g_overload = mk_constant(g_overload_name); @@ -89,6 +98,7 @@ struct parser_fn { } bool curr_is_identifier() const { return curr() == scanner::token::Id; } + bool curr_is_int() const { return curr() == scanner::token::IntVal; } bool curr_is_lparen() const { return curr() == scanner::token::LeftParen; } bool curr_is_colon() const { return curr() == scanner::token::Colon; } bool curr_is_comma() const { return curr() == scanner::token::Comma; } @@ -132,6 +142,94 @@ struct parser_fn { throw parser_error("not implemented yet"); } + // ========================================== + // Universe Level parsing + level parse_level_max() { + next(); + buffer lvls; + while (curr_is_identifier() || curr_is_int()) { + lvls.push_back(parse_level()); + } + if (lvls.size() < 2) + throw parser_error("invalid level expression, max must have at least two arguments"); + level r = lvls[0]; + for (unsigned i = 1; i < lvls.size(); i++) + r = max(r, lvls[i]); + return r; + } + + level parse_level_nud_id() { + name id = curr_name(); + if (id == g_max_name) { + return parse_level_max(); + } else { + next(); + return m_frontend.get_uvar(id); + } + } + + level parse_level_nud_int() { + mpz val = curr_num().get_numerator(); + next(); + if (!val.is_unsigned_int()) + throw parser_error("invalid level expression, value does not fit in a machine integer"); + return level() + val.get_unsigned_int(); + } + + level parse_level_nud() { + switch (curr()) { + case scanner::token::Id: return parse_level_nud_id(); + case scanner::token::IntVal: return parse_level_nud_int(); + default: + throw parser_error("invalid level expression"); + } + } + + level parse_level_led_plus(level const & left) { + next(); + level right = parse_level(g_level_plus_prec); + if (!is_lift(right) || !lift_of(right).is_bottom()) + throw parser_error("invalid level expression, right hand side of '+' (aka universe lift operator) must be a numeral"); + return left + lift_offset(right); + } + + level parse_level_led_cup(level const & left) { + next(); + level right = parse_level(g_level_cup_prec); + return max(left, right); + } + + level parse_level_led(level const & left) { + switch (curr()) { + case scanner::token::Id: + if (curr_name() == g_plus_name) return parse_level_led_plus(left); + else if (curr_name() == g_cup_name) return parse_level_led_cup(left); + default: + throw parser_error("invalid level expression"); + } + } + + unsigned curr_level_lbp() { + switch (curr()) { + case scanner::token::Id: { + name const & id = curr_name(); + if (id == g_plus_name) return g_level_plus_prec; + else if (id == g_cup_name) return g_level_cup_prec; + else return 0; + } + default: return 0; + } + } + + level parse_level(unsigned rbp = 0) { + level left = parse_level_nud(); + while (rbp < curr_level_lbp()) { + left = parse_level_led(left); + } + return left; + } + // ========================================== + expr mk_fun(operator_info const & op) { list const & fs = op.get_internal_names(); lean_assert(!is_nil(fs)); @@ -412,8 +510,11 @@ struct parser_fn { expr parse_type() { next(); - // TODO universe - return Type(); + if (curr_is_identifier() || curr_is_int()) { + return mk_type(parse_level()); + } else { + return Type(); + } } expr parse_nud() { diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 42d641239..e1aaa57fd 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -104,7 +104,7 @@ struct environment::imp { /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */ bool is_ge(level const & l1, level const & l2, int k) { if (l1 == l2) - return k == 0; + return k <= 0; switch (kind(l2)) { case level_kind::UVar: switch (kind(l1)) { diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 9c80a278b..7335f22cd 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -143,7 +143,6 @@ level operator+(level const & l, unsigned k) { case level_kind::UVar: return level(l, k); case level_kind::Lift: return level(lift_of(l), safe_add(lift_offset(l), k)); case level_kind::Max: { - std::cout << l << "\n"; buffer new_lvls; for (unsigned i = 0; i < max_size(l); i++) new_lvls.push_back(max_level(l, i) + k); @@ -207,7 +206,7 @@ format pp(level const & l) { if (lift_of(l).is_bottom()) return format(lift_offset(l)); else - return format{pp(lift_of(l)), format(" + "), format(lift_offset(l))}; + return format{pp(lift_of(l)), format("+"), format(lift_offset(l))}; case level_kind::Max: { format r = pp(max_level(l, 0)); for (unsigned i = 1; i < max_size(l); i++) { @@ -226,3 +225,4 @@ level max(std::initializer_list const & l) { return max_core(l.size(), l.begin()); } } +void print(lean::level const & l) { std::cout << l << std::endl; } diff --git a/src/kernel/level.h b/src/kernel/level.h index 4c79df2a4..e37d61c1d 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -67,3 +67,4 @@ inline level const * max_end_levels(level const & l) { return max_begin_levels format pp(level const & l); } +void print(lean::level const & l); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 628348475..3f97e2d8c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -2,8 +2,10 @@ #include #include "version.h" #include "parser.h" +#include "printer.h" using namespace lean; + int main(int argc, char ** argv) { std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n"; frontend f;