diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 21fc80eff..b95d7cb44 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -62,18 +62,6 @@ static void parse_univ_params(parser & p, buffer & ps) { } } -struct local_scope_if_not_section { - parser & m_p; - local_scope_if_not_section(parser & p):m_p(p) { - if (!in_section(p.env())) - p.push_local_scope(); - } - ~local_scope_if_not_section() { - if (!in_section(m_p.env())) - m_p.pop_local_scope(); - } -}; - static void update_parameters(buffer & ls_buffer, name_set const & found, parser const & p) { unsigned old_sz = ls_buffer.size(); found.for_each([&](name const & n) { @@ -91,9 +79,11 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) buffer ls_buffer; if (p.curr_is_token(g_llevel_curly) && in_section(p.env())) throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos()); - local_scope_if_not_section scope(p); + optional scope1; + if (!in_section(p.env())) + scope1.emplace(p); parse_univ_params(p, ls_buffer); - p.set_type_use_placeholder(false); + parser::param_universe_scope scope2(p); expr type; if (!p.curr_is_token(g_colon)) { buffer ps; @@ -201,24 +191,28 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) { expr type, value; level_param_names ls; { - parser::local_scope scope(p); + parser::local_scope scope1(p); parse_univ_params(p, ls_buffer); - p.set_type_use_placeholder(false); if (!p.curr_is_token(g_colon)) { buffer ps; - auto lenv = p.parse_binders(ps); - p.check_token_next(g_colon, "invalid declaration, ':' expected"); - type = p.parse_scoped_expr(ps, lenv); + optional lenv; + { + parser::param_universe_scope scope2(p); + lenv = p.parse_binders(ps); + p.check_token_next(g_colon, "invalid declaration, ':' expected"); + type = p.parse_scoped_expr(ps, *lenv); + } p.check_token_next(g_assign, "invalid declaration, ':=' expected"); - p.set_type_use_placeholder(true); - value = p.parse_scoped_expr(ps, lenv); + value = p.parse_scoped_expr(ps, *lenv); type = p.pi_abstract(ps, type); value = p.lambda_abstract(ps, value); } else { p.next(); - type = p.parse_expr(); + { + parser::param_universe_scope scope2(p); + type = p.parse_expr(); + } p.check_token_next(g_assign, "invalid declaration, ':=' expected"); - p.set_type_use_placeholder(true); value = p.parse_expr(); } update_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3c4128abd..955dfb3be 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -39,6 +39,23 @@ RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); } // ========================================== +parser::local_scope::local_scope(parser & p): + m_p(p), m_env(p.env()) { + p.push_local_scope(); +} +parser::local_scope::~local_scope() { + m_p.pop_local_scope(); + m_p.m_env = m_env; +} + +parser::param_universe_scope::param_universe_scope(parser & p):m_p(p), m_old(m_p.m_type_use_placeholder) { + m_p.m_type_use_placeholder = false; +} + +parser::param_universe_scope::~param_universe_scope() { + m_p.m_type_use_placeholder = m_old; +} + parser::parser(environment const & env, io_state const & ios, std::istream & strm, char const * strm_name, script_state * ss, bool use_exceptions, @@ -255,12 +272,14 @@ expr parser::mk_app(expr fn, expr arg, pos_info const & p) { } void parser::push_local_scope() { - m_local_level_decls.push(); + if (m_type_use_placeholder) + m_local_level_decls.push(); m_local_decls.push(); } void parser::pop_local_scope() { - m_local_level_decls.pop(); + if (m_type_use_placeholder) + m_local_level_decls.pop(); m_local_decls.pop(); } @@ -530,21 +549,8 @@ void parser::parse_binders_core(buffer & r) { parse_binder_block(r, binder_info()); } else if (curr_is_token(g_lparen)) { next(); - if (curr_is_token(g_infix) || curr_is_token(g_infixl)) { - next(); - m_env = infixl_cmd_core(*this, false); - } else if (curr_is_token(g_infixr)) { - next(); - m_env = infixr_cmd_core(*this, false); - } else if (curr_is_token(g_postfix)) { - next(); - m_env = postfix_cmd_core(*this, false); - } else if (curr_is_token(g_notation)) { - next(); - m_env = notation_cmd_core(*this, false); - } else { + if (!parse_local_notation_decl()) parse_binder_block(r, binder_info()); - } check_token_next(g_rparen, "invalid binder, ')' expected"); } else if (curr_is_token(g_lcurly)) { next(); @@ -570,6 +576,28 @@ local_environment parser::parse_binders(buffer & r) { return local_environment(m_env); } +bool parser::parse_local_notation_decl() { + if (curr_is_token(g_infix) || curr_is_token(g_infixl)) { + next(); + m_env = infixl_cmd_core(*this, false); + return true; + } else if (curr_is_token(g_infixr)) { + next(); + m_env = infixr_cmd_core(*this, false); + return true; + } else if (curr_is_token(g_postfix)) { + next(); + m_env = postfix_cmd_core(*this, false); + return true; + } else if (curr_is_token(g_notation)) { + next(); + m_env = notation_cmd_core(*this, false); + return true; + } else { + return false; + } +} + expr parser::parse_notation(parse_table t, expr * left) { lean_assert(curr() == scanner::token_kind::Keyword); auto p = pos(); @@ -777,11 +805,11 @@ expr parser::parse_expr(unsigned rbp) { } expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp) { - flet let(m_env, lenv.m_env); if (num_params == 0) { return parse_expr(rbp); } else { - local_expr_decls::mk_scope scope(m_local_decls); + local_scope scope(*this); + m_env = lenv; for (unsigned i = 0; i < num_params; i++) add_local(ps[i].m_local); return parse_expr(rbp); @@ -814,7 +842,6 @@ tactic parser::parse_tactic(unsigned /* rbp */) { void parser::parse_command() { lean_assert(curr() == scanner::token_kind::CommandKeyword); - flet save1(m_type_use_placeholder, m_type_use_placeholder); m_last_cmd_pos = pos(); name const & cmd_name = get_token_info().value(); if (auto it = cmds().find(cmd_name)) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 9f5a8706e..2fc4f50b9 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -43,11 +43,7 @@ struct parser_error : public exception { struct interrupt_parser {}; typedef local_decls local_expr_decls; typedef local_decls local_level_decls; -class local_environment { - friend parser; - environment m_env; - local_environment(environment const & env):m_env(env) {} -}; +typedef environment local_environment; class parser { environment m_env; @@ -124,6 +120,12 @@ class parser { void parse_binders_core(buffer & r); expr mk_app(expr fn, expr arg, pos_info const & p); + friend environment section_cmd(parser & p); + friend environment end_scoped_cmd(parser & p); + + void push_local_scope(); + void pop_local_scope(); + public: parser(environment const & env, io_state const & ios, std::istream & strm, char const * str_name, @@ -185,6 +187,8 @@ public: unsigned get_small_nat(); unsigned parse_small_nat(); + bool parse_local_notation_decl(); + level parse_level(unsigned rbp = 0); parameter parse_binder(); @@ -206,9 +210,7 @@ public: tactic parse_tactic(unsigned rbp = 0); - void push_local_scope(); - void pop_local_scope(); - struct local_scope { parser & m_p; local_scope(parser & p):m_p(p) { p.push_local_scope(); } ~local_scope() { m_p.pop_local_scope(); } }; + struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); }; void add_local_level(name const & n, level const & l); void add_local_expr(name const & n, expr const & e, binder_info const & bi = binder_info()); void add_local(expr const & t); @@ -219,17 +221,13 @@ public: /** \brief Return the local parameter named \c n */ optional get_local(name const & n) const; /** - \brief Specify how the method mk_Type behaves. When set_type_use_placeholder(true), then - it returns 'Type.{_}', where '_' is placeholder that instructs the Lean elaborator to - automalically infer a universe level expression for '_'. When set_type_use_placeholder(false), - then it returns 'Type.{l}', where \c l is a fresh universe level parameter. - The new parameter is automatically added to \c m_local_level_decls. - - \remark When the parse is created the flag is set to false. - \remark Before parsing a command, the parser automatically "caches" the current value, and - restores it after the command is parsed (or aborted). + \brief By default, \c mk_Type returns Type.{_} where '_' is a new placeholder. + This scope object allows us to temporarily change this behavior. + In any scope containing this object, \c mk_Type returns Type.{l}, where + \c l is a fresh universe level parameter. + The new parameter is automatically added to \c m_local_level_decls. */ - void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; } + struct param_universe_scope { parser & m_p; bool m_old; param_universe_scope(parser &); ~param_universe_scope(); }; expr mk_Type(); expr elaborate(expr const & e, level_param_names const &);