From 8aefcc182e4dfd0b6a400520eccce24a58db9cd8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 May 2015 10:47:16 -0700 Subject: [PATCH] feat(frontends/lean/parser): add 'parse_simple_binders' --- src/frontends/lean/parser.cpp | 24 +++++++++++++++--------- src/frontends/lean/parser.h | 28 ++++++++++++++++------------ 2 files changed, 31 insertions(+), 21 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 51cd38985..53a16faf3 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -758,11 +758,15 @@ auto parser::elaborate_definition_at(environment const & env, local_level_decls - '{' : implicit - '{{' or '⦃' : strict implicit - '[' : cast + + If simple_only, then only `(` is considered */ -optional parser::parse_optional_binder_info() { +optional parser::parse_optional_binder_info(bool simple_only) { if (curr_is_token(get_lparen_tk())) { next(); return some(binder_info()); + } else if (simple_only) { + return optional(); } else if (curr_is_token(get_lcurly_tk())) { next(); if (curr_is_token(get_lcurly_tk())) { @@ -788,9 +792,9 @@ optional parser::parse_optional_binder_info() { \see parse_optional_binder_info */ -binder_info parser::parse_binder_info() { +binder_info parser::parse_binder_info(bool simple_only) { auto p = pos(); - if (auto bi = parse_optional_binder_info()) { + if (auto bi = parse_optional_binder_info(simple_only)) { return *bi; } else { throw_invalid_open_binder(p); @@ -843,7 +847,8 @@ expr parser::parse_binder(unsigned rbp) { if (curr_is_identifier()) { return parse_binder_core(binder_info(), rbp); } else { - binder_info bi = parse_binder_info(); + bool simple_only = false; + binder_info bi = parse_binder_info(simple_only); rbp = 0; auto r = parse_binder_core(bi, rbp); parse_close_binder_info(bi); @@ -878,17 +883,17 @@ void parser::parse_binder_block(buffer & r, binder_info const & bi, unsign } void parser::parse_binders_core(buffer & r, buffer * nentries, - bool & last_block_delimited, unsigned rbp) { + bool & last_block_delimited, unsigned rbp, bool simple_only) { while (true) { if (curr_is_identifier()) { parse_binder_block(r, binder_info(), rbp); last_block_delimited = false; } else { - optional bi = parse_optional_binder_info(); + optional bi = parse_optional_binder_info(simple_only); if (bi) { rbp = 0; last_block_delimited = true; - if (!parse_local_notation_decl(nentries)) + if (simple_only || !parse_local_notation_decl(nentries)) parse_binder_block(r, *bi, rbp); parse_close_binder_info(bi); } else { @@ -899,11 +904,12 @@ void parser::parse_binders_core(buffer & r, buffer * nentr } local_environment parser::parse_binders(buffer & r, buffer * nentries, - bool & last_block_delimited, bool allow_empty, unsigned rbp) { + bool & last_block_delimited, bool allow_empty, unsigned rbp, + bool simple_only) { flet save(m_env, m_env); // save environment local_expr_decls::mk_scope scope(m_local_decls); unsigned old_sz = r.size(); - parse_binders_core(r, nentries, last_block_delimited, rbp); + parse_binders_core(r, nentries, last_block_delimited, rbp, simple_only); if (!allow_empty && old_sz == r.size()) throw_invalid_open_binder(pos()); return local_environment(m_env); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 24ac2cce3..bfc5781a8 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -199,9 +199,9 @@ class parser { expr parse_string_expr(); expr parse_binder_core(binder_info const & bi, unsigned rbp); void parse_binder_block(buffer & r, binder_info const & bi, unsigned rbp); - void parse_binders_core(buffer & r, buffer * nentries, bool & last_block_delimited, unsigned rbp); + void parse_binders_core(buffer & r, buffer * nentries, bool & last_block_delimited, unsigned rbp, bool simple_only); local_environment parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited, - bool allow_empty, unsigned rbp); + bool allow_empty, unsigned rbp, bool simple_only); bool parse_local_notation_decl(buffer * entries); pair, expr> parse_id_tk_expr(name const & tk, unsigned rbp); @@ -357,23 +357,27 @@ public: expr parse_binder(unsigned rbp); local_environment parse_binders(buffer & r, bool & last_block_delimited) { - unsigned rbp = 0; bool allow_empty = false; - return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp); + unsigned rbp = 0; bool allow_empty = false; bool simple_only = false; + return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp, simple_only); } local_environment parse_binders(buffer & r, unsigned rbp) { - bool tmp; bool allow_empty = false; - return parse_binders(r, nullptr, tmp, allow_empty, rbp); + bool tmp; bool allow_empty = false; bool simple_only = false; + return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only); + } + void parse_simple_binders(buffer & r, unsigned rbp) { + bool tmp; bool allow_empty = false; bool simple_only = true; + parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only); } local_environment parse_optional_binders(buffer & r) { - bool tmp; bool allow_empty = true; unsigned rbp = 0; - return parse_binders(r, nullptr, tmp, allow_empty, rbp); + bool tmp; bool allow_empty = true; unsigned rbp = 0; bool simple_only = false; + return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only); } local_environment parse_binders(buffer & r, buffer & nentries) { - bool tmp; bool allow_empty = false; unsigned rbp = 0; - return parse_binders(r, &nentries, tmp, allow_empty, rbp); + bool tmp; bool allow_empty = false; unsigned rbp = 0; bool simple_only = false; + return parse_binders(r, &nentries, tmp, allow_empty, rbp, simple_only); } - optional parse_optional_binder_info(); - binder_info parse_binder_info(); + optional parse_optional_binder_info(bool simple_only = false); + binder_info parse_binder_info(bool simple_only = false); void parse_close_binder_info(optional const & bi); void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional(bi)); }