From bccc3df1aa79ee6957b46c4867350fadfcb85961 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jun 2014 16:52:20 -0700 Subject: [PATCH] chore(frontends/lean): reduce code duplication Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 62 +++---------- src/frontends/lean/parser.cpp | 147 +++++++++++++++++++------------ src/frontends/lean/parser.h | 4 + 3 files changed, 109 insertions(+), 104 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index ada9e3722..0a27008c9 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -18,12 +18,7 @@ Author: Leonardo de Moura namespace lean { static name g_llevel_curly(".{"); -static name g_lcurly("{"); static name g_rcurly("}"); -static name g_ldcurly("⦃"); -static name g_rdcurly("⦄"); -static name g_lbracket("["); -static name g_rbracket("]"); static name g_colon(":"); static name g_assign(":="); static name g_private("[private]"); @@ -45,44 +40,6 @@ environment universe_cmd(parser & p) { return env; } -binder_info parse_open_binder_info(parser & p) { - if (p.curr_is_token(g_lcurly)) { - check_in_section(p); - p.next(); - if (p.curr_is_token(g_lcurly)) { - p.next(); - return mk_strict_implicit_binder_info(); - } else { - return mk_implicit_binder_info(); - } - } else if (p.curr_is_token(g_lbracket)) { - check_in_section(p); - p.next(); - return mk_cast_binder_info(); - } else if (p.curr_is_token(g_ldcurly)) { - check_in_section(p); - p.next(); - return mk_strict_implicit_binder_info(); - } else { - return binder_info(); - } -} - -void parse_close_binder_info(parser & p, binder_info const & bi) { - if (bi.is_implicit()) { - p.check_token_next(g_rcurly, "invalid declaration, '}' expected"); - } else if (bi.is_cast()) { - p.check_token_next(g_rbracket, "invalid declaration, ']' expected"); - } else if (bi.is_strict_implicit()) { - if (p.curr_is_token(g_lcurly)) { - p.next(); - p.check_token_next(g_rdcurly, "invalid declaration, '}' expected"); - } else { - p.check_token_next(g_rdcurly, "invalid declaration, '⦄' expected"); - } - } -} - bool parse_univ_params(parser & p, buffer & ps) { if (p.curr_is_token(g_llevel_curly)) { p.next(); @@ -111,7 +68,9 @@ void update_univ_parameters(buffer & ls_buffer, name_set const & found, pa static environment declare_var(parser & p, environment env, name const & n, level_param_names const & ls, expr const & type, - bool is_axiom, binder_info const & bi, pos_info const & pos) { + bool is_axiom, optional const & _bi, pos_info const & pos) { + binder_info bi; + if (_bi) bi = *_bi; if (in_section(p.env())) { p.add_local(p.save_pos(mk_local(n, type, bi), pos)); return env; @@ -128,9 +87,16 @@ static environment declare_var(parser & p, environment env, } } +optional parse_binder_info(parser & p) { + optional bi = p.parse_optional_binder_info(); + if (bi) + check_in_section(p); + return bi; +} + environment variable_cmd_core(parser & p, bool is_axiom) { auto pos = p.pos(); - binder_info bi = parse_open_binder_info(p); + optional bi = parse_binder_info(p); name n = p.check_id_next("invalid declaration, identifier expected"); check_atomic(n); buffer ls_buffer; @@ -152,7 +118,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) { p.next(); type = p.parse_expr(); } - parse_close_binder_info(p, bi); + p.parse_close_binder_info(bi); level_param_names ls; if (in_section(p.env())) { ls = to_level_param_names(collect_univ_params(type)); @@ -308,7 +274,7 @@ environment theorem_cmd(parser & p) { static environment variables_cmd(parser & p) { auto pos = p.pos(); buffer ids; - binder_info bi = parse_open_binder_info(p); + optional bi = parse_binder_info(p); while (!p.curr_is_token(g_colon)) { name id = p.check_id_next("invalid parameters declaration, identifier expected"); check_atomic(id); @@ -320,7 +286,7 @@ static environment variables_cmd(parser & p) { scope1.emplace(p); parser::param_universe_scope scope2(p); expr type = p.parse_expr(); - parse_close_binder_info(p, bi); + p.parse_close_binder_info(bi); level_param_names ls = to_level_param_names(collect_univ_params(type)); type = p.elaborate(type); environment env = p.env(); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index caf60c3ec..599005585 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -538,6 +538,82 @@ std::pair parser::elaborate(name const & n, expr const & t, expr con return ::lean::elaborate(m_env, m_ios, n, t, v, m_hints, &pp); } +[[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) { + throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos); +} + +/** + \brief Return an optional binder_info object based on the current token + - '(' : default + - '{' : implicit + - '{{' or '⦃' : strict implicit + - '[' : cast +*/ +optional parser::parse_optional_binder_info() { + if (curr_is_token(g_lparen)) { + next(); + return some(binder_info()); + } else if (curr_is_token(g_lcurly)) { + next(); + if (curr_is_token(g_lcurly)) { + next(); + return some(mk_strict_implicit_binder_info()); + } else { + return some(mk_implicit_binder_info()); + } + } else if (curr_is_token(g_lbracket)) { + next(); + return some(mk_cast_binder_info()); + } else if (curr_is_token(g_ldcurly)) { + next(); + return some(mk_strict_implicit_binder_info()); + } else { + return optional(); + } +} + +/** + \brief Return binder_info object based on the current token, it fails if the current token + is not '(', '{', '{{', '⦃', or '[' + + \see parse_optional_binder_info +*/ +binder_info parser::parse_binder_info() { + auto p = pos(); + if (auto bi = parse_optional_binder_info()) { + return *bi; + } else { + throw_invalid_open_binder(p); + } +} + +/** + \brief Consume the next token based on the value of \c bi + - none : do not consume anything + - default : consume ')' + - implicit : consume '}' + - strict implicit : consume '}}' or '⦄' + - cast : consume ']' +*/ +void parser::parse_close_binder_info(optional const & bi) { + if (!bi) { + return; + } else if (bi->is_implicit()) { + check_token_next(g_rcurly, "invalid declaration, '}' expected"); + } else if (bi->is_cast()) { + check_token_next(g_rbracket, "invalid declaration, ']' expected"); + } else if (bi->is_strict_implicit()) { + if (curr_is_token(g_rcurly)) { + next(); + check_token_next(g_rcurly, "invalid declaration, '}' expected"); + } else { + check_token_next(g_rdcurly, "invalid declaration, '⦄' expected"); + } + } else { + check_token_next(g_rparen, "invalid declaration, ')' expected"); + } +} + /** \brief Parse ID ':' expr, where the expression represents the type of the identifier. */ expr parser::parse_binder_core(binder_info const & bi) { auto p = pos(); @@ -558,36 +634,11 @@ expr parser::parse_binder_core(binder_info const & bi) { expr parser::parse_binder() { if (curr_is_identifier()) { return parse_binder_core(binder_info()); - } else if (curr_is_token(g_lparen)) { - next(); - auto p = parse_binder_core(binder_info()); - check_token_next(g_rparen, "invalid binder, ')' expected"); - return p; - } else if (curr_is_token(g_lcurly)) { - next(); - if (curr_is_token(g_lcurly)) { - next(); - auto p = parse_binder_core(mk_strict_implicit_binder_info()); - check_token_next(g_rcurly, "invalid binder, '}' expected"); - check_token_next(g_rcurly, "invalid binder, '}' expected"); - return p; - } else { - auto p = parse_binder_core(mk_implicit_binder_info()); - check_token_next(g_rcurly, "invalid binder, '}' expected"); - return p; - } - } else if (curr_is_token(g_lbracket)) { - next(); - auto p = parse_binder_core(mk_cast_binder_info()); - check_token_next(g_rbracket, "invalid binder, ']' expected"); - return p; - } else if (curr_is_token(g_ldcurly)) { - next(); - auto p = parse_binder_core(mk_strict_implicit_binder_info()); - check_token_next(g_rdcurly, "invalid binder, '⦄' expected"); - return p; } else { - throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos()); + binder_info bi = parse_binder_info(); + auto r = parse_binder_core(bi); + parse_close_binder_info(bi); + return r; } } @@ -614,36 +665,20 @@ void parser::parse_binder_block(buffer & r, binder_info const & bi) { } void parser::parse_binders_core(buffer & r) { - if (curr_is_identifier()) { - parse_binder_block(r, binder_info()); - } else if (curr_is_token(g_lparen)) { - next(); - if (!parse_local_notation_decl()) + while (true) { + if (curr_is_identifier()) { parse_binder_block(r, binder_info()); - check_token_next(g_rparen, "invalid binder, ')' expected"); - } else if (curr_is_token(g_lcurly)) { - next(); - if (curr_is_token(g_lcurly)) { - next(); - parse_binder_block(r, mk_strict_implicit_binder_info()); - check_token_next(g_rcurly, "invalid binder, '}' expected"); - check_token_next(g_rcurly, "invalid binder, '}' expected"); } else { - parse_binder_block(r, mk_implicit_binder_info()); - check_token_next(g_rcurly, "invalid binder, '}' expected"); + optional bi = parse_optional_binder_info(); + if (bi) { + if (!parse_local_notation_decl()) + parse_binder_block(r, *bi); + parse_close_binder_info(bi); + } else { + return; + } } - } else if (curr_is_token(g_lbracket)) { - next(); - parse_binder_block(r, mk_cast_binder_info()); - check_token_next(g_rbracket, "invalid binder, ']' expected"); - } else if (curr_is_token(g_ldcurly)) { - next(); - parse_binder_block(r, mk_strict_implicit_binder_info()); - check_token_next(g_rdcurly, "invalid binder, '⦄' expected"); - } else { - return; } - parse_binders_core(r); } local_environment parser::parse_binders(buffer & r) { @@ -652,7 +687,7 @@ local_environment parser::parse_binders(buffer & r) { unsigned old_sz = r.size(); parse_binders_core(r); if (old_sz == r.size()) - throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos()); + 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 960636da1..931f1f2f7 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -205,6 +205,10 @@ public: expr parse_binder(); local_environment parse_binders(buffer & r); + optional parse_optional_binder_info(); + binder_info parse_binder_info(); + void parse_close_binder_info(optional const & bi); + void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional(bi)); } /** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */ expr id_to_expr(name const & id, pos_info const & p);