From 843253355bf80ccaaa0074770c5b40b8d0acb151 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Aug 2013 10:50:14 -0700 Subject: [PATCH] Improve parser Signed-off-by: Leonardo de Moura --- src/frontend/frontend.cpp | 2 + src/frontend/frontend.h | 1 + src/frontend/parser.cpp | 145 +++++++++++++++++++++++++++++++--- src/frontend/parser.h | 4 +- src/tests/frontend/parser.cpp | 5 ++ 5 files changed, 143 insertions(+), 14 deletions(-) diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index 8e53cf97f..ddc945f81 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -151,6 +151,7 @@ struct frontend::imp { m_env.add_neutral_object(new notation_declaration(new_op, n)); } + void add_infix(name const & opn, unsigned p, name const & n) { add_op(infix(opn, p), n, true); } void add_infixl(name const & opn, unsigned p, name const & n) { add_op(infixl(opn, p), n, true); } void add_infixr(name const & opn, unsigned p, name const & n) { add_op(infixr(opn, p), n, true); } void add_prefix(name const & opn, unsigned p, name const & n) { add_op(prefix(opn, p), n, false); } @@ -210,6 +211,7 @@ frontend::object_iterator frontend::end_objects() const { return m_imp->m_env.en frontend::object_iterator frontend::begin_local_objects() const { return m_imp->m_env.begin_local_objects(); } frontend::object_iterator frontend::end_local_objects() const { return m_imp->m_env.end_local_objects(); } +void frontend::add_infix(name const & opn, unsigned p, name const & n) { m_imp->add_infix(opn, p, n); } void frontend::add_infixl(name const & opn, unsigned p, name const & n) { m_imp->add_infixl(opn, p, n); } void frontend::add_infixr(name const & opn, unsigned p, name const & n) { m_imp->add_infixr(opn, p, n); } void frontend::add_prefix(name const & opn, unsigned p, name const & n) { m_imp->add_prefix(opn, p, n); } diff --git a/src/frontend/frontend.h b/src/frontend/frontend.h index 72f4f4b81..c307145aa 100644 --- a/src/frontend/frontend.h +++ b/src/frontend/frontend.h @@ -68,6 +68,7 @@ public: // ======================================= // Notation + void add_infix(name const & opn, unsigned precedence, name const & n); void add_infixl(name const & opn, unsigned precedence, name const & n); void add_infixr(name const & opn, unsigned precedence, name const & n); void add_prefix(name const & opn, unsigned precedence, name const & n); diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp index a1b9012ed..3d79895d4 100644 --- a/src/frontend/parser.cpp +++ b/src/frontend/parser.cpp @@ -9,6 +9,10 @@ Author: Leonardo de Moura #include "scanner.h" #include "scoped_map.h" #include "exception.h" +#include "normalize.h" +#include "type_check.h" +#include "builtin_notation.h" +#include "pp.h" #include "builtin.h" #include "arith.h" @@ -20,6 +24,8 @@ static name g_axiom_kwd("Axiom"); static name g_universe_kwd("Universe"); static name g_eval_kwd("Eval"); static name g_show_kwd("Show"); +static name g_check_kwd("Check"); +static name g_env_kwd("Environment"); static name g_infix_kwd("Infix"); static name g_infixl_kwd("Infixl"); static name g_infixr_kwd("Infixr"); @@ -32,7 +38,7 @@ static name g_mixfixc_kwd("Mixfixc"); static name g_overload_name(name(name(name(0u), "parser"), "overload")); static expr g_overload = mk_constant(g_overload_name); -static list g_command_keywords = {g_definition_kwd, g_variable_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd, g_show_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_prefix_kwd, g_postfix_kwd, g_mixfixl_kwd, g_mixfixr_kwd, g_mixfixc_kwd}; +static list g_command_keywords = {g_definition_kwd, g_variable_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd, g_show_kwd, g_check_kwd, g_env_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_prefix_kwd, g_postfix_kwd, g_mixfixl_kwd, g_mixfixr_kwd, g_mixfixc_kwd}; /** \brief Functional object for parsing */ struct parser_fn { @@ -40,6 +46,8 @@ struct parser_fn { typedef std::unordered_map builtins; frontend m_frontend; scanner m_scanner; + formatter m_formatter; + std::ostream * m_out; std::ostream * m_err; scanner::token m_curr; bool m_use_exceptions; @@ -60,6 +68,7 @@ struct parser_fn { next(); } name const & curr_name() const { return m_scanner.get_name_val(); } + mpq const & curr_num() const { return m_scanner.get_num_val(); } void check_next(scanner::token t, char const * msg) { if (curr() == t) @@ -74,6 +83,8 @@ struct parser_fn { name check_identifier_next(char const * msg) { check_identifier(msg); name r = curr_name(); next(); return r; } void check_colon_next(char const * msg) { check_next(scanner::token::Colon, msg); } void check_rparen_next(char const * msg) { check_next(scanner::token::RightParen, msg); } + void check_name(name const & op, char const * msg) { if(!curr_is_identifier() || curr_name() != op) throw parser_error(msg); } + void check_name_next(name const & op, char const * msg) { check_name(op, msg); next(); } void init_builtins() { m_builtins["Bool"] = Bool; @@ -84,9 +95,11 @@ struct parser_fn { m_builtins["Int"] = Int; } - parser_fn(frontend & fe, std::istream & in, std::ostream * err, bool use_exceptions): + parser_fn(frontend & fe, std::istream & in, std::ostream * out, std::ostream * err, bool use_exceptions): m_frontend(fe), m_scanner(in), + m_formatter(mk_pp_formatter(fe)), + m_out(out), m_err(err), m_use_exceptions(use_exceptions) { m_found_errors = false; @@ -134,16 +147,50 @@ struct parser_fn { return mk_app(mk_fun(op), left, right); } + void check_op_part(name const & op_part) { + check_name_next(op_part, "invalid expression, identifier expected"); + } + + void parse_mixfix_args(list const & ops, unsigned prec, buffer & args) { + auto it = ops.begin(); + ++it; + while (it != ops.end()) { + check_op_part(*it); + args.push_back(parse_expr(prec)); + ++it; + } + } + expr parse_mixfixl(operator_info const & op) { - not_implemented_yet(); + buffer args; + args.push_back(mk_fun(op)); + args.push_back(parse_expr(op.get_precedence())); + parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); + return mk_app(args.size(), args.data()); } expr parse_mixfixr(expr const & left, operator_info const & op) { - not_implemented_yet(); + buffer args; + args.push_back(mk_fun(op)); + args.push_back(left); + parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); + return mk_app(args.size(), args.data()); } expr parse_mixfixc(operator_info const & op) { - not_implemented_yet(); + buffer args; + args.push_back(mk_fun(op)); + args.push_back(parse_expr(op.get_precedence())); + list const & ops = op.get_op_name_parts(); + auto it = ops.begin(); + ++it; + while (true) { + check_op_part(*it); + ++it; + if (it == ops.end()) + return mk_app(args.size(), args.data()); + args.push_back(parse_expr(op.get_precedence())); + } } expr get_name_ref(name const & id) { @@ -208,6 +255,12 @@ struct parser_fn { } } + expr parse_eq(expr const & left) { + next(); + expr right = parse_expr(g_eq_precedence); + return mk_eq(left, right); + } + expr parse_lparen() { next(); expr r = parse_expr(); @@ -261,6 +314,7 @@ struct parser_fn { expr parse_led(expr const & left) { switch (curr()) { case scanner::token::Id: return parse_led_id(left); + case scanner::token::Eq: return parse_eq(left); case scanner::token::LeftParen: return mk_app(left, parse_lparen()); case scanner::token::IntVal: return mk_app(left, parse_int()); case scanner::token::DecimalVal: return mk_app(left, parse_decimal()); @@ -285,6 +339,7 @@ struct parser_fn { return 1; } } + case scanner::token::Eq : return g_eq_precedence; case scanner::token::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal: case scanner::token::StringVal: case scanner::token::Type: return 1; @@ -334,19 +389,80 @@ struct parser_fn { } void parse_eval() { - // TODO + next(); + expr v = elaborate(parse_expr()); + expr r = normalize(v, m_frontend); + (*m_out) << m_formatter(r) << std::endl; } void parse_show() { - // TODO + next(); + expr v = elaborate(parse_expr()); + (*m_out) << m_formatter(v) << std::endl; + } + + void parse_check() { + next(); + expr v = elaborate(parse_expr()); + expr t = infer_type(v, m_frontend); + (*m_out) << m_formatter(t) << std::endl; + } + + void parse_env() { + next(); + (*m_out) << m_frontend << std::endl; + } + + unsigned parse_precision() { + if (curr() == scanner::token::IntVal) { + mpz pval = curr_num().get_numerator(); + if (!pval.is_unsigned_int()) + throw parser_error("invalid operator definition, precedence does not fit in a machine integer"); + unsigned r = pval.get_unsigned_int(); + next(); + return r; + } else { + return 0; + } + } + + name parse_op_id() { + return check_identifier_next("invalid operator definition, identifier expected"); } void parse_op(fixity fx) { - // TODO + next(); + unsigned prec = parse_precision(); + name op_id = parse_op_id(); + name id = parse_op_id(); + switch (fx) { + case fixity::Prefix: m_frontend.add_prefix(op_id, prec, id); break; + case fixity::Postfix: m_frontend.add_postfix(op_id, prec, id); break; + case fixity::Infix: m_frontend.add_infix(op_id, prec, id); break; + case fixity::Infixl: m_frontend.add_infixl(op_id, prec, id); break; + case fixity::Infixr: m_frontend.add_infixr(op_id, prec, id); break; + default: lean_unreachable(); break; + } } void parse_mixfix_op(fixity fx) { - // TODO + next(); + unsigned prec = parse_precision(); + buffer parts; + parts.push_back(parse_op_id()); + parts.push_back(parse_op_id()); + name id = parse_op_id(); + while (curr_is_identifier()) { + parts.push_back(id); + id = curr_name(); + next(); + } + switch (fx) { + case fixity::Mixfixl: m_frontend.add_mixfixl(parts.size(), parts.data(), prec, id); break; + case fixity::Mixfixr: m_frontend.add_mixfixr(parts.size(), parts.data(), prec, id); break; + case fixity::Mixfixc: m_frontend.add_mixfixc(parts.size(), parts.data(), prec, id); break; + default: lean_unreachable(); break; + } } void parse_command() { @@ -357,6 +473,8 @@ struct parser_fn { else if (cmd_id == g_axiom_kwd) parse_axiom(); else if (cmd_id == g_eval_kwd) parse_eval(); else if (cmd_id == g_show_kwd) parse_show(); + else if (cmd_id == g_check_kwd) parse_check(); + else if (cmd_id == g_env_kwd) parse_env(); else if (cmd_id == g_infix_kwd) parse_op(fixity::Infix); else if (cmd_id == g_infixl_kwd) parse_op(fixity::Infixl); else if (cmd_id == g_infixr_kwd) parse_op(fixity::Infixr); @@ -383,6 +501,7 @@ struct parser_fn { try { switch (curr()) { case scanner::token::CommandId: parse_command(); break; + case scanner::token::Period: next(); break; case scanner::token::Eof: return !m_found_errors; default: throw parser_error("Command expected"); @@ -407,17 +526,17 @@ struct parser_fn { expr parse_expr_main() { try { - return parse_expr(); + return elaborate(parse_expr()); } catch (parser_error & ex) { throw parser_exception(ex.what(), m_scanner.get_line(), m_scanner.get_pos()); } } }; -bool parse_commands(frontend & fe, std::istream & in, std::ostream & err, bool use_exceptions) { - return parser_fn(fe, in, &err, use_exceptions).parse_commands(); +bool parse_commands(frontend & fe, std::istream & in, std::ostream & out, std::ostream & err, bool use_exceptions) { + return parser_fn(fe, in, &out, &err, use_exceptions).parse_commands(); } expr parse_expr(frontend const & fe, std::istream & in) { - return parser_fn(const_cast(fe), in, nullptr, true).parse_expr_main(); + return parser_fn(const_cast(fe), in, nullptr, nullptr, true).parse_expr_main(); } } diff --git a/src/frontend/parser.h b/src/frontend/parser.h index f50016f1d..c5d769f24 100644 --- a/src/frontend/parser.h +++ b/src/frontend/parser.h @@ -9,6 +9,8 @@ Author: Leonardo de Moura #include "frontend.h" namespace lean { -bool parse_commands(frontend & fe, std::istream & in, std::ostream & err = std::cerr, bool use_exceptions = false); +bool parse_commands(frontend & fe, std::istream & in, + std::ostream & out = std::cout, std::ostream & err = std::cerr, + bool use_exceptions = false); expr parse_expr(frontend const & fe, std::istream & in); } diff --git a/src/tests/frontend/parser.cpp b/src/tests/frontend/parser.cpp index 02d7ea615..039e53e5e 100644 --- a/src/tests/frontend/parser.cpp +++ b/src/tests/frontend/parser.cpp @@ -30,6 +30,10 @@ static void parse(frontend & fe, char const * str) { static void tst1() { frontend fe; parse(fe, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x"); + parse(fe, "Eval true && true"); + parse(fe, "Show true && false Eval true && false"); + parse(fe, "Infixl 35 & and Show true & false & false Eval true & false"); + parse(fe, "Mixfixc 100 if then fi implies Show if true then false fi"); } static void check(frontend const & fe, char const * str, expr const & expected) { @@ -56,6 +60,7 @@ static void tst2() { check(fe, "x ∨ y ∨ x ∧ z ⇒ x ∧ y", Implies(Or(x, Or(y, And(x, z))), And(x, y))); check(fe, "x⇒y⇒z⇒x", Implies(x, Implies(y, Implies(z, x)))); check(fe, "x=>y=>z=>x", Implies(x, Implies(y, Implies(z, x)))); + check(fe, "x=>(y=>z)=>x", Implies(x, Implies(Implies(y, z), x))); } int main() {