From 631e2395a3cf9e6549ea6a8eb0715cc297c05dc4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Aug 2014 18:43:56 -0700 Subject: [PATCH] refactor(frontends/lean/elaborator): add elaborator_env class Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 125 +++++++++++---------- src/frontends/lean/elaborator.h | 29 +++-- src/frontends/lean/parser.cpp | 50 ++++++--- src/frontends/lean/parser.h | 7 +- src/frontends/lean/parser_pos_provider.cpp | 12 +- src/frontends/lean/parser_pos_provider.h | 13 +-- 6 files changed, 135 insertions(+), 101 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index abdf9dc79..3402f3b47 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "frontends/lean/class.h" #include "frontends/lean/tactic_hint.h" #include "frontends/lean/info_manager.h" +#include "frontends/lean/elaborator.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -121,6 +122,12 @@ public: expr operator()(expr const & e) { return apply(e); } }; +elaborator_env::elaborator_env(environment const & env, io_state const & ios, local_decls const & lls, + pos_info_provider const * pp, info_manager * info, bool check_unassigned): + m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) { + m_use_local_instances = get_elaborator_local_instances(ios.get_options()); +} + /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ list get_local_instances(list const & ctx, name const & cls_name) { buffer buffer; @@ -285,9 +292,7 @@ class elaborator { typedef name_map local_tactic_hints; typedef std::unique_ptr type_checker_ptr; - environment m_env; - local_decls m_lls; - io_state m_ios; + elaborator_env & m_env; name_generator m_ngen; type_checker_ptr m_tc[2]; mvar2meta m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants @@ -295,15 +300,11 @@ class elaborator { context m_context; // current local context: a list of local constants context m_full_context; // superset of m_context, it also contains non-contextual locals. - pos_info_provider * m_pos_provider; // optional expression position information used when reporting errors. constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct. local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. // this mapping is populated by the 'by tactic-expr' expression. name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned - bool m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables - bool m_use_local_instances; // if true class-instance resolution will use the local context bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent - info_manager * m_info_manager; std::vector m_pre_info_data; struct scope_ctx { @@ -427,7 +428,7 @@ class elaborator { } optional try_instance(name const & inst) { - auto decl = m_elab.m_env.find(inst); + auto decl = m_elab.env().find(inst); if (!decl) return optional(); expr type = decl->get_type(); @@ -487,7 +488,7 @@ class elaborator { m_tactics = tail(m_tactics); proof_state ps(goals(goal(m_meta, m_meta_type)), substitution(), m_elab.m_ngen.mk_child()); try { - m_tactic_result = tac(m_elab.m_env, m_elab.m_ios, ps); + m_tactic_result = tac(m_elab.env(), m_elab.ios(), ps); if (auto cs = get_next_tactic_result()) return cs; } catch (exception &) {} @@ -511,21 +512,24 @@ class elaborator { } public: - elaborator(environment const & env, local_decls const & lls, list const & ctx, io_state const & ios, name_generator const & ngen, - pos_info_provider * pp, bool check_unassigned, info_manager * info): - m_env(env), m_lls(lls), m_ios(ios), + elaborator(elaborator_env & env, list const & ctx, name_generator const & ngen): + m_env(env), m_ngen(ngen), m_context(m_ngen, m_mvar2meta, ctx), - m_full_context(m_ngen, m_mvar2meta, ctx), - m_pos_provider(pp), - m_info_manager(info) { + m_full_context(m_ngen, m_mvar2meta, ctx) { m_relax_main_opaque = false; - m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false); - m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true); - m_check_unassigned = check_unassigned; - m_use_local_instances = get_elaborator_local_instances(ios.get_options()); + m_tc[0] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), false); + m_tc[1] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), true); } + environment const & env() const { return m_env.m_env; } + io_state const & ios() const { return m_env.m_ios; } + local_decls const & lls() const { return m_env.m_lls; } + bool use_local_instances() const { return m_env.m_use_local_instances; } + info_manager * infom() const { return m_env.m_info_manager; } + pos_info_provider const * pip() const { return m_env.m_pos_provider; } + bool check_unassigned() const { return m_env.m_check_unassigned; } + expr mk_local(name const & n, expr const & t, binder_info const & bi) { return ::lean::mk_local(m_ngen.next(), n, t, bi); } @@ -560,7 +564,7 @@ public: list get_class_instances(expr const & type) { if (is_constant(get_app_fn(type))) { name const & c = const_name(get_app_fn(type)); - return ::lean::get_class_instances(m_env, c); + return ::lean::get_class_instances(env(), c); } else { return list(); } @@ -571,7 +575,7 @@ public: if (!is_constant(f)) return false; name const & cls_name = const_name(f); - return ::lean::is_class(m_env, cls_name) || !empty(get_tactic_hints(m_env, cls_name)); + return ::lean::is_class(env(), cls_name) || !empty(get_tactic_hints(env(), cls_name)); } static expr instantiate_meta(expr const & meta, substitution & subst) { @@ -585,11 +589,11 @@ public: /** \brief Return a 'failed to synthesize placholder' justification for the given metavariable application \c m of the form (?m l_1 ... l_k) */ justification mk_failed_to_synthesize_jst(expr const & m) { - environment env = m_env; + environment _env = env(); return mk_justification(m, [=](formatter const & fmt, substitution const & subst) { substitution tmp(subst); expr new_m = instantiate_meta(m, tmp); - expr new_type = type_checker(env).infer(new_m); + expr new_type = type_checker(_env).infer(new_m); proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare")); return format({format("failed to synthesize placeholder"), line(), ps.pp(fmt)}); }); @@ -608,12 +612,12 @@ public: if (is_class(meta_type)) { name const & cls_name = const_name(get_app_fn(meta_type)); list local_insts; - if (m_use_local_instances) + if (use_local_instances()) local_insts = get_local_instances(ctx, cls_name); list insts = get_class_instances(meta_type); list tacs; if (!s.is_assigned(mvar)) - tacs = get_tactic_hints(m_env, cls_name); + tacs = get_tactic_hints(env(), cls_name); if (empty(local_insts) && empty(insts) && empty(tacs)) return lazy_list(); // nothing to be done bool ignore_failure = false; // we are always strict with placeholders associated with classes @@ -624,7 +628,7 @@ public: // the an empty set of constraints. return lazy_list(constraints()); } else { - list tacs = get_tactic_hints(m_env); + list tacs = get_tactic_hints(env()); bool ignore_failure = !is_strict; return choose(std::make_shared(*this, meta, meta_type, list(), list(), tacs, ctx, full_ctx, j, ignore_failure, m_relax_main_opaque)); @@ -702,13 +706,13 @@ public: } if (!is_pi(f_type)) { // try coercion to function-class - optional c = get_coercion_to_fun(m_env, f_type); + optional c = get_coercion_to_fun(env(), f_type); if (c) { f = mk_app(*c, f, f.get_tag()); f_type = infer_type(f); lean_assert(is_pi(f_type)); } else { - throw_kernel_exception(m_env, f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); + throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); } } lean_assert(is_pi(f_type)); @@ -717,12 +721,12 @@ public: bool has_coercions_from(expr const & a_type) { expr const & a_cls = get_app_fn(whnf(a_type)); - return is_constant(a_cls) && ::lean::has_coercions_from(m_env, const_name(a_cls)); + return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls)); } bool has_coercions_to(expr const & d_type) { expr const & d_cls = get_app_fn(whnf(d_type)); - return is_constant(d_cls) && ::lean::has_coercions_to(m_env, const_name(d_cls)); + return is_constant(d_cls) && ::lean::has_coercions_to(env(), const_name(d_cls)); } expr apply_coercion(expr const & a, expr a_type, expr d_type) { @@ -730,7 +734,7 @@ public: d_type = whnf(d_type); expr const & d_cls = get_app_fn(d_type); if (is_constant(d_cls)) { - if (auto c = get_coercion(m_env, a_type, const_name(d_cls))) + if (auto c = get_coercion(env(), a_type, const_name(d_cls))) return mk_app(*c, a, a.get_tag()); } return a; @@ -883,8 +887,8 @@ public: /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ void save_info_data_core(expr const & e, expr const & r, bool replace) { - if (m_info_manager && m_pos_provider && (is_constant(e) || is_local(e) || is_placeholder(e))) { - if (auto p = m_pos_provider->get_pos_info(e)) { + if (infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) { + if (auto p = pip()->get_pos_info(e)) { type_checker::scope scope(*m_tc[m_relax_main_opaque]); expr t = m_tc[m_relax_main_opaque]->infer(r); if (replace) { @@ -905,13 +909,13 @@ public: } expr visit_constant(expr const & e) { - declaration d = m_env.get(const_name(e)); + declaration d = env().get(const_name(e)); buffer ls; for (level const & l : const_levels(e)) ls.push_back(replace_univ_placeholder(l)); unsigned num_univ_params = length(d.get_univ_params()); if (num_univ_params < ls.size()) - throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" + throw_kernel_exception(env(), sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #" << num_univ_params << " expected, #" << ls.size() << " provided"); // "fill" with meta universe parameters @@ -939,10 +943,10 @@ public: return e; } } - optional c = get_coercion_to_sort(m_env, t); + optional c = get_coercion_to_sort(env(), t); if (c) return mk_app(*c, e, e.get_tag()); - throw_kernel_exception(m_env, e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); + throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); } /** \brief Similar to instantiate_rev, but assumes that subst contains only local constants. @@ -1061,7 +1065,7 @@ public: buffer cs; cs.append(m_constraints); m_constraints.clear(); - return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), true, m_ios.get_options()); + return unify(env(), cs.size(), cs.data(), m_ngen.mk_child(), true, ios().get_options()); } static void collect_metavars(expr const & e, buffer & mvars) { @@ -1078,9 +1082,9 @@ public: lean_assert(is_metavar(mvar)); if (!m_displayed_errors.contains(mlocal_name(mvar))) { m_displayed_errors.insert(mlocal_name(mvar)); - auto out = regular(m_env, m_ios); + auto out = regular(env(), ios()); flycheck_error err(out); - display_error_pos(out, m_pos_provider, mvar); + display_error_pos(out, pip(), mvar); out << " unsolved placeholder, " << msg << "\n" << ps << endl; } } @@ -1112,10 +1116,10 @@ public: optional pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar) { try { - return optional(expr_to_tactic(m_env, pre_tac, m_pos_provider)); + return optional(expr_to_tactic(env(), pre_tac, pip())); } catch (expr_to_tactic_exception & ex) { - auto out = regular(m_env, m_ios); - display_error_pos(out, m_pos_provider, mvar); + auto out = regular(env(), ios()); + display_error_pos(out, pip(), mvar); out << " " << ex.what(); out << pp_indent_expr(out.get_formatter(), pre_tac) << endl << "failed at:" << pp_indent_expr(out.get_formatter(), ex.get_expr()) << endl; @@ -1140,7 +1144,7 @@ public: // make sure ps is a really a proof state for mvar. lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar)); try { - proof_state_seq seq = tac(m_env, m_ios, ps); + proof_state_seq seq = tac(env(), ios(), ps); auto r = seq.pull(); if (!r) { // tactic failed to produce any result @@ -1157,8 +1161,8 @@ public: return true; } } catch (tactic_exception & ex) { - auto out = regular(m_env, m_ios); - display_error_pos(out, m_pos_provider, ex.get_expr()); + auto out = regular(env(), ios()); + display_error_pos(out, pip(), ex.get_expr()); out << " tactic failed: " << ex.what() << "\n"; return false; } @@ -1200,14 +1204,14 @@ public: } void display_unassigned_mvars(expr const & e, substitution const & s) { - if (m_check_unassigned && has_metavar(e)) { + if (check_unassigned() && has_metavar(e)) { substitution tmp_s(s); for_each(e, [&](expr const & e, unsigned) { if (!is_metavar(e)) return has_metavar(e); if (auto it = m_mvar2meta.find(mlocal_name(e))) { expr meta = tmp_s.instantiate(*it); - expr meta_type = tmp_s.instantiate(type_checker(m_env).infer(meta)); + expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta)); goal g(meta, meta_type); display_unsolved_proof_state(e, proof_state(goals(g), substitution(), m_ngen), "don't know how to synthesize it"); @@ -1221,7 +1225,7 @@ public: expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params) { expr r = s.instantiate(e); if (has_univ_metavar(r)) - r = univ_metavars_to_params_fn(m_env, m_lls, s, univ_params, new_params)(r); + r = univ_metavars_to_params_fn(env(), lls(), s, univ_params, new_params)(r); r = solve_unassigned_mvars(s, r); display_unassigned_mvars(r, s); return r; @@ -1235,15 +1239,15 @@ public: } void copy_info_to_manager(substitution s) { - if (!m_info_manager) + if (!infom()) return; for (auto & p : m_pre_info_data) p = type_info_data(p.get_line(), p.get_column(), s.instantiate(p.get_type())); - m_info_manager->append(m_pre_info_data); + infom()->append(m_pre_info_data); } std::tuple operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) { - flet set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(m_env)); + flet set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(env())); expr r = visit(e); if (_ensure_type) r = ensure_type(r); @@ -1259,7 +1263,7 @@ public: lean_assert(!has_local(t)); lean_assert(!has_local(v)); expr r_t = ensure_type(visit(t)); // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent. - flet set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(m_env)); + flet set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(env())); expr r_v = visit(v); expr r_v_type = infer_type(r_v); justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) { @@ -1281,16 +1285,13 @@ public: static name g_tmp_prefix = name::mk_internal_unique_name(); -std::tuple elaborate(environment const & env, local_decls const & lls, list const & ctx, - io_state const & ios, expr const & e, bool relax_main_opaque, - pos_info_provider * pp, bool check_unassigned, bool ensure_type, - info_manager * info) { - return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned, info)(e, ensure_type, relax_main_opaque); +std::tuple elaborate(elaborator_env & env, list const & ctx, expr const & e, + bool relax_main_opaque, bool ensure_type) { + return elaborator(env, ctx, name_generator(g_tmp_prefix))(e, ensure_type, relax_main_opaque); } -std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, - name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp, - info_manager * info) { - return elaborator(env, lls, list(), ios, name_generator(g_tmp_prefix), pp, true, info)(t, v, n, is_opaque); +std::tuple elaborate(elaborator_env & env, name const & n, expr const & t, expr const & v, + bool is_opaque) { + return elaborator(env, list(), name_generator(g_tmp_prefix))(t, v, n, is_opaque); } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 742396d50..fd23d18f6 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -14,11 +14,26 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" namespace lean { -std::tuple elaborate(environment const & env, local_decls const & lls, list const & ctx, - io_state const & ios, expr const & e, bool relax_main_opaque, - pos_info_provider * pp = nullptr, bool check_unassigned = true, - bool ensure_type = false, info_manager * info = nullptr); -std::tuple elaborate(environment const & env, local_decls const & lls, - io_state const & ios, name const & n, expr const & t, expr const & v, - bool is_opaque, pos_info_provider * pp = nullptr, info_manager * info = nullptr); +/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */ +class elaborator_env { + environment m_env; + io_state m_ios; + local_decls m_lls; // local universe levels + pos_info_provider const * m_pos_provider; + info_manager * m_info_manager; + + // configuration + bool m_check_unassigned; + bool m_use_local_instances; + friend class elaborator; +public: + elaborator_env(environment const & env, io_state const & ios, local_decls const & lls, + pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true); +}; + +std::tuple elaborate(elaborator_env & env, list const & ctx, expr const & e, + bool relax_main_opaque, bool ensure_type = false); + +std::tuple elaborate(elaborator_env & env, name const & n, expr const & t, expr const & v, + bool is_opaque); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 12edf73a4..46b577f16 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -86,7 +86,6 @@ parser::parser(environment const & env, io_state const & ios, m_env(env), m_ios(ios), m_ngen(g_tmp_prefix), m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds), - m_pos_table(std::make_shared()), m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr) { m_num_threads = num_threads; @@ -239,7 +238,9 @@ tag parser::get_tag(expr e) { } expr parser::save_pos(expr e, pos_info p) { - m_pos_table->insert(mk_pair(get_tag(e), p)); + auto t = get_tag(e); + if (!m_pos_table.contains(t)) + m_pos_table.insert(t, p); return e; } @@ -302,11 +303,10 @@ expr parser::propagate_levels(expr const & e, levels const & ls) { } pos_info parser::pos_of(expr const & e, pos_info default_pos) { - auto it = m_pos_table->find(get_tag(e)); - if (it == m_pos_table->end()) - return default_pos; + if (auto it = m_pos_table.find(get_tag(e))) + return *it; else - return it->second; + return default_pos; } bool parser::curr_is_token(name const & tk) const { @@ -517,39 +517,54 @@ level parser::parse_level(unsigned rbp) { return left; } +elaborator_env parser::mk_elaborator_env(pos_info_provider const & pp, bool check_unassigned) { + return elaborator_env(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned); +} + +elaborator_env parser::mk_elaborator_env(environment const & env, pos_info_provider const & pp) { + return elaborator_env(env, m_ios, m_local_level_decls, &pp, m_info_manager, true); +} + +elaborator_env parser::mk_elaborator_env(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) { + return elaborator_env(env, m_ios, lls, &pp, m_info_manager, true); +} + std::tuple parser::elaborate_relaxed(expr const & e, list const & ctx) { - parser_pos_provider pp = get_pos_provider(); bool relax = true; bool check_unassigned = false; bool ensure_type = false; - auto r = ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type, - m_info_manager); + parser_pos_provider pp = get_pos_provider(); + elaborator_env env = mk_elaborator_env(pp, check_unassigned); + auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type); m_pre_info_data.clear(); return r; } std::tuple parser::elaborate_type(expr const & e, list const & ctx) { - parser_pos_provider pp = get_pos_provider(); bool relax = false; bool check_unassigned = true; bool ensure_type = true; - auto r = ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type, - m_info_manager); + parser_pos_provider pp = get_pos_provider(); + elaborator_env env = mk_elaborator_env(pp, check_unassigned); + auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type); m_pre_info_data.clear(); return r; } std::tuple parser::elaborate_at(environment const & env, expr const & e) { - parser_pos_provider pp = get_pos_provider(); bool relax = false; - auto r = ::lean::elaborate(env, m_local_level_decls, list(), m_ios, e, relax, &pp, m_info_manager); + parser_pos_provider pp = get_pos_provider(); + elaborator_env eenv = mk_elaborator_env(env, pp); + auto r = ::lean::elaborate(eenv, list(), e, relax); m_pre_info_data.clear(); return r; } -std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) { +std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v, + bool is_opaque) { parser_pos_provider pp = get_pos_provider(); - auto r = ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp, m_info_manager); + elaborator_env eenv = mk_elaborator_env(pp); + auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); m_pre_info_data.clear(); return r; } @@ -557,7 +572,8 @@ std::tuple parser::elaborate_definition(name cons std::tuple parser::elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v, bool is_opaque) { parser_pos_provider pp = get_pos_provider(); - auto r = ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp, m_info_manager); + elaborator_env eenv = mk_elaborator_env(env, lls, pp); + auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); m_pre_info_data.clear(); return r; } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 91086a5ba..3d7317f68 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/definitions_cache.h" #include "frontends/lean/scanner.h" +#include "frontends/lean/elaborator.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/parser_config.h" #include "frontends/lean/parser_pos_provider.h" @@ -75,7 +76,7 @@ class parser { unsigned m_next_tag_idx; bool m_found_errors; bool m_used_sorry; - pos_info_table_ptr m_pos_table; + pos_info_table m_pos_table; // By default, when the parser finds a unknown identifier, it signs an error. // When the following flag is true, it creates a constant. // This flag is when we are trying to parse mutually recursive declarations. @@ -162,6 +163,10 @@ class parser { void save_type_info(expr const & e); void save_pre_info_data(); + elaborator_env mk_elaborator_env(pos_info_provider const & pp, bool check_unassigned = true); + elaborator_env mk_elaborator_env(environment const & env, pos_info_provider const & pp); + elaborator_env mk_elaborator_env(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); + public: parser(environment const & env, io_state const & ios, std::istream & strm, char const * str_name, diff --git a/src/frontends/lean/parser_pos_provider.cpp b/src/frontends/lean/parser_pos_provider.cpp index e2060bb0a..828eb20e5 100644 --- a/src/frontends/lean/parser_pos_provider.cpp +++ b/src/frontends/lean/parser_pos_provider.cpp @@ -9,22 +9,20 @@ Author: Leonardo de Moura #include "frontends/lean/parser_pos_provider.h" namespace lean { -parser_pos_provider::parser_pos_provider(pos_info_table_ptr const & pos_table, - std::string const & strm_name, pos_info const & some_pos): +parser_pos_provider::parser_pos_provider(pos_info_table const & pos_table, + std::string const & strm_name, pos_info const & some_pos): m_pos_table(pos_table), m_strm_name(strm_name), m_pos(some_pos) {} parser_pos_provider::~parser_pos_provider() {} optional parser_pos_provider::get_pos_info(expr const & e) const { - if (!m_pos_table) - return optional(); tag t = e.get_tag(); if (t == nulltag) return optional(); - auto it = m_pos_table->find(t); - if (it == m_pos_table->end()) + if (auto it = m_pos_table.find(t)) + return optional(*it); + else return optional(); - return optional(it->second); } pos_info parser_pos_provider::get_some_pos() const { diff --git a/src/frontends/lean/parser_pos_provider.h b/src/frontends/lean/parser_pos_provider.h index 95c7ff958..3d6a561a7 100644 --- a/src/frontends/lean/parser_pos_provider.h +++ b/src/frontends/lean/parser_pos_provider.h @@ -8,19 +8,18 @@ Author: Leonardo de Moura #include #include #include -#include +#include "util/rb_map.h" #include "kernel/pos_info_provider.h" namespace lean { -typedef std::unordered_map pos_info_table; -typedef std::shared_ptr pos_info_table_ptr; +typedef rb_map pos_info_table; class parser_pos_provider : public pos_info_provider { - pos_info_table_ptr m_pos_table; - std::string m_strm_name; - pos_info m_pos; + pos_info_table m_pos_table; + std::string m_strm_name; + pos_info m_pos; public: - parser_pos_provider(pos_info_table_ptr const & pos_table, std::string const & strm_name, pos_info const & some_pos); + parser_pos_provider(pos_info_table const & pos_table, std::string const & strm_name, pos_info const & some_pos); virtual ~parser_pos_provider(); virtual optional get_pos_info(expr const & e) const; virtual pos_info get_some_pos() const;