diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 1f03d7c73f..0e4d67efe9 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -11,8 +11,7 @@ parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp type_util.cpp elaborator_exception.cpp local_ref_info.cpp obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp parse_with_options_tactic.cpp opt_cmd.cpp prenum.cpp -parse_with_attributes_tactic.cpp print_cmd.cpp +parse_with_attributes_tactic.cpp print_cmd.cpp elaborator_context.cpp # LEGACY old_elaborator.cpp -old_elaborator_context.cpp ) diff --git a/src/frontends/lean/old_elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp similarity index 81% rename from src/frontends/lean/old_elaborator_context.cpp rename to src/frontends/lean/elaborator_context.cpp index 8274353809..7f76844a2c 100644 --- a/src/frontends/lean/old_elaborator_context.cpp +++ b/src/frontends/lean/elaborator_context.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "util/sexpr/option_declarations.h" #include "frontends/lean/parser.h" -#include "frontends/lean/old_elaborator_context.h" +#include "frontends/lean/elaborator_context.h" #include "frontends/lean/opt_cmd.h" #ifndef LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS @@ -43,19 +43,19 @@ bool get_elaborator_coercions(options const & opts) { // ========================================== -old_elaborator_context::old_elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls, - pos_info_provider const * pp, info_manager * info, bool check_unassigned): +elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_level_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) { set_options(ios.get_options()); } -old_elaborator_context::old_elaborator_context(old_elaborator_context const & ctx, options const & o): +elaborator_context::elaborator_context(elaborator_context const & ctx, options const & o): m_env(ctx.m_env), m_ios(ctx.m_ios), m_lls(ctx.m_lls), m_pos_provider(ctx.m_pos_provider), m_info_manager(ctx.m_info_manager), m_check_unassigned(ctx.m_check_unassigned) { set_options(o); } -void old_elaborator_context::set_options(options const & opts) { +void elaborator_context::set_options(options const & opts) { m_options = opts; m_flycheck_goals = get_elaborator_flycheck_goals(opts); m_lift_coercions = get_elaborator_lift_coercions(opts); @@ -74,7 +74,7 @@ void old_elaborator_context::set_options(options const & opts) { } } -bool old_elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) const { +bool elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) const { if (m_show_goal_at) { line = m_show_goal_line; col = m_show_goal_col; @@ -84,11 +84,11 @@ bool old_elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) c } } -void old_elaborator_context::reset_show_goal_at() { +void elaborator_context::reset_show_goal_at() { m_show_goal_at = false; } -bool old_elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) const { +bool elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) const { if (m_show_hole_at) { line = m_show_hole_line; col = m_show_hole_col; @@ -98,11 +98,11 @@ bool old_elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) c } } -void old_elaborator_context::reset_show_hole_at() { +void elaborator_context::reset_show_hole_at() { m_show_hole_at = false; } -void initialize_old_elaborator_context() { +void initialize_elaborator_context() { g_elaborator_flycheck_goals = new name{"elaborator", "flycheck_goals"}; g_elaborator_lift_coercions = new name{"elaborator", "lift_coercions"}; g_elaborator_coercions = new name{"elaborator", "coercions"}; @@ -115,7 +115,7 @@ void initialize_old_elaborator_context() { register_bool_option(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS, "(elaborator) if true, the elaborator will automatically introduce coercions"); } -void finalize_old_elaborator_context() { +void finalize_elaborator_context() { delete g_elaborator_flycheck_goals; delete g_elaborator_lift_coercions; delete g_elaborator_coercions; diff --git a/src/frontends/lean/old_elaborator_context.h b/src/frontends/lean/elaborator_context.h similarity index 53% rename from src/frontends/lean/old_elaborator_context.h rename to src/frontends/lean/elaborator_context.h index c9b2cf7c51..1649cdef70 100644 --- a/src/frontends/lean/old_elaborator_context.h +++ b/src/frontends/lean/elaborator_context.h @@ -7,13 +7,18 @@ Author: Leonardo de Moura #pragma once #include "kernel/environment.h" #include "library/io_state.h" -#include "frontends/lean/local_decls.h" #include "frontends/lean/local_level_decls.h" #include "frontends/lean/info_manager.h" namespace lean { -/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */ -class old_elaborator_context { +/** \brief Context for the elaborator. + + \remark It contains all the information that is "scope-indenpendent". + So, it does not contain the local context because it is context dependent. */ +class elaborator_context { + friend class old_elaborator; // TODO(Leo): remove this line when done + friend class elaborator; + environment m_env; io_state m_ios; local_level_decls m_lls; // local universe levels @@ -25,15 +30,14 @@ class old_elaborator_context { bool m_flycheck_goals; bool m_lift_coercions; bool m_coercions; - friend class old_elaborator; - bool m_show_goal_at; - unsigned m_show_goal_line; - unsigned m_show_goal_col; + bool m_show_goal_at; + unsigned m_show_goal_line; + unsigned m_show_goal_col; - bool m_show_hole_at; - unsigned m_show_hole_line; - unsigned m_show_hole_col; + bool m_show_hole_at; + unsigned m_show_hole_line; + unsigned m_show_hole_col; void set_options(options const & opts); @@ -44,11 +48,11 @@ class old_elaborator_context { bool has_show_hole_at(unsigned & line, unsigned & col) const; void reset_show_hole_at(); public: - old_elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls, - pos_info_provider const * pp = nullptr, info_manager * info = nullptr, - bool check_unassigned = true); - old_elaborator_context(old_elaborator_context const & ctx, options const & o); + elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls, + pos_info_provider const * pp = nullptr, info_manager * info = nullptr, + bool check_unassigned = true); + elaborator_context(elaborator_context const & ctx, options const & o); }; -void initialize_old_elaborator_context(); -void finalize_old_elaborator_context(); +void initialize_elaborator_context(); +void finalize_elaborator_context(); } diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 53360646c0..f58539b5a3 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "frontends/lean/tokens.h" -#include "frontends/lean/old_elaborator_context.h" +#include "frontends/lean/elaborator_context.h" #include "frontends/lean/old_elaborator.h" #include "frontends/lean/parser.h" #include "frontends/lean/info_annotation.h" @@ -43,7 +43,7 @@ void initialize_frontend_lean_module() { initialize_builtin_cmds(); initialize_builtin_exprs(); initialize_builtin_tactics(); - initialize_old_elaborator_context(); + initialize_elaborator_context(); initialize_old_elaborator(); initialize_scanner(); initialize_parser(); @@ -84,7 +84,7 @@ void finalize_frontend_lean_module() { finalize_parser(); finalize_scanner(); finalize_old_elaborator(); - finalize_old_elaborator_context(); + finalize_elaborator_context(); finalize_builtin_tactics(); finalize_builtin_exprs(); finalize_builtin_cmds(); diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index b611bffcbb..5855546eda 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -173,7 +173,7 @@ struct old_elaborator::choice_expr_elaborator : public choice_iterator { } }; -old_elaborator::old_elaborator(old_elaborator_context & ctx, bool nice_mvar_names): +old_elaborator::old_elaborator(elaborator_context & ctx, bool nice_mvar_names): m_ctx(ctx), m_context(), m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) { @@ -1881,7 +1881,7 @@ optional old_elaborator::pre_tactic_to_tactic(expr const & pre_tac) { return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, use_tactic_hints, subst, report_unassigned); } else { - old_elaborator_context aux_ctx(m_ctx, o); + elaborator_context aux_ctx(m_ctx, o); old_elaborator aux_elaborator(aux_ctx); return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, use_tactic_hints, subst, report_unassigned); @@ -2446,12 +2446,12 @@ elaborate_result old_elaborator::elaborate_nested(list const & ctx, option static name * g_tmp_prefix = nullptr; -std::tuple elaborate(old_elaborator_context & env, list const & ctx, expr const & e, +std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, bool ensure_type, bool nice_mvar_names) { return old_elaborator(env, nice_mvar_names)(ctx, e, ensure_type); } -std::tuple elaborate(old_elaborator_context & env, name const & n, expr const & t, +std::tuple elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v) { return old_elaborator(env)(t, v, n); } diff --git a/src/frontends/lean/old_elaborator.h b/src/frontends/lean/old_elaborator.h index 85d3144fc2..7134312abe 100644 --- a/src/frontends/lean/old_elaborator.h +++ b/src/frontends/lean/old_elaborator.h @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" #include "library/tactic/elaborate.h" #include "library/old_type_checker.h" -#include "frontends/lean/old_elaborator_context.h" +#include "frontends/lean/elaborator_context.h" #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/util.h" #include "frontends/lean/obtain_expr.h" @@ -29,7 +29,7 @@ class old_elaborator : public coercion_info_manager { typedef name_map local_tactic_hints; typedef rb_map, expr_quick_cmp> cache; typedef std::vector> to_check_sorts; - old_elaborator_context & m_ctx; + elaborator_context & m_ctx; old_type_checker_ptr m_tc; old_type_checker_ptr m_coercion_from_tc; old_type_checker_ptr m_coercion_to_tc; @@ -191,15 +191,15 @@ class old_elaborator : public coercion_info_manager { void show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr); public: - old_elaborator(old_elaborator_context & ctx, bool nice_mvar_names = false); + old_elaborator(elaborator_context & ctx, bool nice_mvar_names = false); std::tuple operator()(list const & ctx, expr const & e, bool _ensure_type); std::tuple operator()(expr const & t, expr const & v, name const & n); }; -std::tuple elaborate(old_elaborator_context & env, list const & ctx, expr const & e, +std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, bool ensure_type = false, bool nice_mvar_names = false); -std::tuple elaborate(old_elaborator_context & env, name const & n, expr const & t, expr const & v); +std::tuple elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v); void initialize_old_elaborator(); void finalize_old_elaborator(); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 91deea3554..68b5e4214c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -863,17 +863,17 @@ level parser::parse_level(unsigned rbp) { return left; } -old_elaborator_context parser::mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned) { - return old_elaborator_context(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned); +elaborator_context parser::mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned) { + return elaborator_context(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned); } -old_elaborator_context parser::mk_elaborator_context(environment const & env, pos_info_provider const & pp) { - return old_elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true); +elaborator_context parser::mk_elaborator_context(environment const & env, pos_info_provider const & pp) { + return elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true); } -old_elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, +elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) { - return old_elaborator_context(env, m_ios, lls, &pp, m_info_manager, true); + return elaborator_context(env, m_ios, lls, &pp, m_info_manager, true); } std::tuple parser::old_elaborate_relaxed(expr const & e, list const & ctx) { @@ -881,7 +881,7 @@ std::tuple parser::old_elaborate_relaxed(expr const & e bool ensure_type = false; bool nice_mvar_names = true; parser_pos_provider pp = get_pos_provider(); - old_elaborator_context env = mk_elaborator_context(pp, check_unassigned); + elaborator_context env = mk_elaborator_context(pp, check_unassigned); auto r = ::lean::elaborate(env, ctx, e, ensure_type, nice_mvar_names); m_pre_info_manager.clear(); return r; @@ -891,7 +891,7 @@ std::tuple parser::old_elaborate(expr const & e, list parser::old_elaborate_type(expr const & e, l bool check_unassigned = true; bool ensure_type = true; parser_pos_provider pp = get_pos_provider(); - old_elaborator_context env = mk_elaborator_context(pp, check_unassigned); + elaborator_context env = mk_elaborator_context(pp, check_unassigned); auto r = ::lean::elaborate(env, ctx, e, ensure_type); if (clear_pre_info) m_pre_info_manager.clear(); @@ -910,7 +910,7 @@ std::tuple parser::old_elaborate_type(expr const & e, l std::tuple parser::old_elaborate_at(environment const & env, expr const & e) { parser_pos_provider pp = get_pos_provider(); - old_elaborator_context eenv = mk_elaborator_context(env, pp); + elaborator_context eenv = mk_elaborator_context(env, pp); auto r = ::lean::elaborate(eenv, list(), e); m_pre_info_manager.clear(); return r; @@ -919,7 +919,7 @@ std::tuple parser::old_elaborate_at(environment const & auto parser::old_elaborate_definition(name const & n, expr const & t, expr const & v) -> std::tuple { parser_pos_provider pp = get_pos_provider(); - old_elaborator_context eenv = mk_elaborator_context(pp); + elaborator_context eenv = mk_elaborator_context(pp); auto r = ::lean::elaborate(eenv, n, t, v); m_pre_info_manager.clear(); return r; @@ -929,7 +929,7 @@ auto parser::old_elaborate_definition_at(environment const & env, local_level_de name const & n, expr const & t, expr const & v) -> std::tuple { parser_pos_provider pp = get_pos_provider(); - old_elaborator_context eenv = mk_elaborator_context(env, lls, pp); + elaborator_context eenv = mk_elaborator_context(env, lls, pp); auto r = ::lean::elaborate(eenv, n, t, v); m_pre_info_manager.clear(); return r; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 871e8eb98a..f6172334b2 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -19,7 +19,7 @@ Author: Leonardo de Moura #include "library/definition_cache.h" #include "library/declaration_index.h" #include "frontends/lean/scanner.h" -#include "frontends/lean/old_elaborator_context.h" +#include "frontends/lean/elaborator_context.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/local_level_decls.h" #include "frontends/lean/parser_config.h" @@ -233,9 +233,10 @@ class parser { void commit_info(unsigned line, unsigned col); void commit_info() { commit_info(m_scanner.get_line(), m_scanner.get_pos()); } - old_elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true); - old_elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp); - old_elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); + elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true); + elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp); + elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, + pos_info_provider const & pp); bool m_in_backtick; // true if parser `expr` notation expr parse_backtick_expr_core();