diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3a1d7c059b..c19230b241 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -483,7 +483,7 @@ expr parser::mk_app(std::initializer_list const & args, pos_info const & p parser_scope parser::mk_parser_scope(optional const & opts) { return parser_scope(opts, m_level_variables, m_variables, m_include_vars, - m_undef_ids.size(), m_next_inst_idx, m_has_params, + m_next_inst_idx, m_has_params, m_local_level_decls, m_local_decls); } @@ -512,7 +512,6 @@ void parser::pop_local_scope() { lean_assert(m_parser_scope_stack); auto s = head(m_parser_scope_stack); restore_parser_scope(s); - m_undef_ids.shrink(s.m_num_undef_ids); m_parser_scope_stack = tail(m_parser_scope_stack); } @@ -1813,8 +1812,6 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only) if (!r) { if (m_id_behavior == id_behavior::AssumeLocalIfUndef) { expr local = mk_local(id, save_pos(mk_expr_placeholder(), p)); - if (!resolve_only) - m_undef_ids.push_back(local); r = save_pos(local, p); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 41edf4b387..46205ebf7f 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -74,8 +74,6 @@ class parser : public abstract_parser { // curr command token name m_cmd_token; - buffer m_undef_ids; - // profiling bool m_profile; @@ -458,11 +456,6 @@ public: struct error_if_undef_scope : public flet { error_if_undef_scope(parser & p); }; struct all_id_local_scope : public flet { all_id_local_scope(parser & p); }; - /** \brief Return the size of the stack of undefined local constants */ - unsigned get_num_undef_ids() const { return m_undef_ids.size(); } - /** \brief Return the i-th undefined local constants */ - expr const & get_undef_id(unsigned i) const { return m_undef_ids[i]; } - private: pair elaborate(name const & decl_name, metavar_context & mctx, local_context_adapter const & adapter, expr const & e, bool check_unassigned = true); diff --git a/src/frontends/lean/parser_state.cpp b/src/frontends/lean/parser_state.cpp index 32ea715d18..6508ccb0c6 100644 --- a/src/frontends/lean/parser_state.cpp +++ b/src/frontends/lean/parser_state.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "library/class.h" #include "library/deep_copy.h" +#include "library/quote.h" #include "frontends/lean/parser_state.h" #include "frontends/lean/tokens.h" @@ -108,14 +109,34 @@ name parser_state::mk_anonymous_inst_name() { return n; } -optional parser_state::get_pos_info(expr const & /* e */) const { - /* TODO(Leo): */ - return optional(); +optional parser_state::get_pos_info(expr const & e) const { + tag t = e.get_tag(); + if (t == nulltag) + return optional(); + if (auto it = m_pos_table.find(t)) + return optional(*it); + else + return optional(); +} + +token const * parser_state::get_last_cmd_tk() const { + unsigned i = m_tv_cmd_idx; + while (true) { + token const & tk = get_token(i); + if (tk.kind() == token_kind::CommandKeyword && + tk.get_token_info().token() != get_end_tk()) { + return &tk; + } + if (i == 0) return nullptr; + i--; + } } pos_info parser_state::get_some_pos() const { - /* TODO(Leo): */ - return pos_info(0, 0); + if (token const * tk = get_last_cmd_tk()) + return tk->get_pos(); + else + return get_token(0).get_pos(); } expr parser_state::save_pos(expr e, pos_info p) { @@ -149,16 +170,24 @@ expr parser_state::rec_save_pos(expr const & e, pos_info p) { expr parser_state::copy_with_new_pos(expr const & e, pos_info p) { switch (e.kind()) { case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta: - case expr_kind::Local: case expr_kind::Var: + case expr_kind::Var: case expr_kind::Local: return save_pos(copy(e), p); case expr_kind::App: return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p), copy_with_new_pos(app_arg(e), p)), p); - case expr_kind::Lambda: case expr_kind::Pi: - return save_pos(update_binding(e, - copy_with_new_pos(binding_domain(e), p), - copy_with_new_pos(binding_body(e), p)), + case expr_kind::Lambda: + return save_pos(::lean::mk_lambda(binding_name(e), + copy_with_new_pos(binding_domain(e), p), + copy_with_new_pos(binding_body(e), p), + binding_info(e)), + + p); + case expr_kind::Pi: + return save_pos(::lean::mk_pi(binding_name(e), + copy_with_new_pos(binding_domain(e), p), + copy_with_new_pos(binding_body(e), p), + binding_info(e)), p); case expr_kind::Let: return save_pos(::lean::mk_let(let_name(e), @@ -166,12 +195,16 @@ expr parser_state::copy_with_new_pos(expr const & e, pos_info p) { copy_with_new_pos(let_value(e), p), copy_with_new_pos(let_body(e), p)), p); - case expr_kind::Macro: { - buffer args; - for (unsigned i = 0; i < macro_num_args(e); i++) - args.push_back(copy_with_new_pos(macro_arg(e, i), p)); - return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p); - }} + case expr_kind::Macro: + if (is_quote(e)) { + return save_pos(mk_quote_core(copy_with_new_pos(get_quote_expr(e), p)), p); + } else { + buffer args; + for (unsigned i = 0; i < macro_num_args(e); i++) + args.push_back(copy_with_new_pos(macro_arg(e, i), p)); + return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p); + } + } lean_unreachable(); // LCOV_EXCL_LINE } @@ -254,4 +287,60 @@ name parser_state::check_atomic_decl_id_next(char const * msg) { return id; } +expr parser_state::mk_app(expr fn, expr arg, pos_info const & p) { + return save_pos(::lean::mk_app(fn, arg), p); +} + +expr parser_state::mk_app(expr fn, buffer const & args, pos_info const & p) { + expr r = fn; + for (expr const & arg : args) { + r = mk_app(r, arg, p); + } + return r; +} + +expr parser_state::mk_app(std::initializer_list const & args, pos_info const & p) { + lean_assert(args.size() >= 2); + auto it = args.begin(); + expr r = *it; + it++; + for (; it != args.end(); it++) + r = mk_app(r, *it, p); + return r; +} + +parser_state::scope parser_state::mk_scope(optional const & opts) { + return scope(opts, m_context->m_level_variables, m_context->m_variables, m_context->m_include_vars, + m_next_inst_idx, m_has_params, m_context->m_local_level_decls, m_context->m_local_decls); +} + +void parser_state::restore_scope(scope const & s) { + ensure_exclusive_context(); + if (s.m_options) { + m_context->m_ios.set_options(*s.m_options); + } + m_context->m_local_level_decls = s.m_local_level_decls; + m_context->m_local_decls = s.m_local_decls; + m_context->m_level_variables = s.m_level_variables; + m_context->m_variables = s.m_variables; + m_context->m_include_vars = s.m_include_vars; + m_has_params = s.m_has_params; + m_next_inst_idx = s.m_next_inst_idx; +} + +void parser_state::push_local_scope(bool save_options) { + ensure_exclusive_context(); + optional opts; + if (save_options) + opts = m_context->m_ios.get_options(); + m_context->m_scope_stack = cons(mk_scope(opts), m_context->m_scope_stack); +} + +void parser_state::pop_local_scope() { + lean_assert(m_context->m_scope_stack); + ensure_exclusive_context(); + auto s = head(m_context->m_scope_stack); + restore_scope(s); + m_context->m_scope_stack = tail(m_context->m_scope_stack); +} } diff --git a/src/frontends/lean/parser_state.h b/src/frontends/lean/parser_state.h index 7c0501a3aa..a03fdfa711 100644 --- a/src/frontends/lean/parser_state.h +++ b/src/frontends/lean/parser_state.h @@ -73,16 +73,15 @@ public: name_set m_level_variables; name_set m_variables; name_set m_include_vars; - unsigned m_num_undef_ids; unsigned m_next_inst_idx; bool m_has_params; local_level_decls m_local_level_decls; local_expr_decls m_local_decls; scope(optional const & o, name_set const & lvs, name_set const & vs, name_set const & ivs, - unsigned num_undef_ids, unsigned next_inst_idx, bool has_params, + unsigned next_inst_idx, bool has_params, local_level_decls const & lld, local_expr_decls const & led): m_options(o), m_level_variables(lvs), m_variables(vs), m_include_vars(ivs), - m_num_undef_ids(num_undef_ids), m_next_inst_idx(next_inst_idx), m_has_params(has_params), + m_next_inst_idx(next_inst_idx), m_has_params(has_params), m_local_level_decls(lld), m_local_decls(led) {} }; @@ -106,7 +105,6 @@ public: name_set m_include_vars; // subset of m_local_decls that is marked as include scope_stack m_scope_stack; scope_stack m_quote_stack; - list m_undef_ids; /* Tasks that need to be successful (no exception) for parsing to succeed. */ list m_required_successes; context(environment const & env, io_state const & ios):m_env(env), m_ios(ios) {} @@ -228,6 +226,8 @@ private: void ensure_exclusive_context(); + token const * get_last_cmd_tk() const; + public: parser_state(environment const & env, io_state const & ios, header_ptr const & h, bool use_exceptions = false, std::shared_ptr const & s = {}); @@ -236,6 +236,7 @@ public: environment const & env() const { return m_context->m_env; } std::vector const & get_token_vector() const { return m_header->m_token_vector; } + token const & get_token(unsigned i) const { return m_header->m_token_vector[i]; } token const & curr_token() const { return get_token_vector()[m_tv_curr_idx]; } token_kind curr() const { return curr_token().kind(); } @@ -296,12 +297,15 @@ public: /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */ name check_constant_next(char const * msg); - void check_break_at_pos(break_at_pos_exception::token_context ctxt = break_at_pos_exception::token_context::none); /** \brief Throw \c break_at_pos_exception with empty token and given context if \c m_break_at_pos is before current position. */ void check_break_before(break_at_pos_exception::token_context ctxt = break_at_pos_exception::token_context::none); + expr mk_app(expr fn, expr arg, pos_info const & p); + expr mk_app(expr fn, buffer const & args, pos_info const & p); + expr mk_app(std::initializer_list const & args, pos_info const & p); + name mk_anonymous_inst_name(); bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); } @@ -467,8 +471,6 @@ public: struct error_if_undef_scope : public flet { error_if_undef_scope(parser_state & p); }; struct all_id_local_scope : public flet { all_id_local_scope(parser_state & p); }; - list get_undef_ids() const { return m_context->m_undef_ids; } - private: pair elaborate(name const & decl_name, metavar_context & mctx, local_context_adapter const & adapter, expr const & e, bool check_unassigned = true);