diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3402f3b47..251069c8b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -122,8 +122,8 @@ 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): +elaborator_context::elaborator_context(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()); } @@ -292,19 +292,19 @@ class elaborator { typedef name_map local_tactic_hints; typedef std::unique_ptr type_checker_ptr; - 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 + elaborator_context & 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 // representing the context where ?m was created. - 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. + 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. - 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. + 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_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent + name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned + bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent std::vector m_pre_info_data; struct scope_ctx { @@ -512,7 +512,7 @@ class elaborator { } public: - elaborator(elaborator_env & env, list const & ctx, name_generator const & ngen): + elaborator(elaborator_context & env, list const & ctx, name_generator const & ngen): m_env(env), m_ngen(ngen), m_context(m_ngen, m_mvar2meta, ctx), @@ -1285,12 +1285,12 @@ public: static name g_tmp_prefix = name::mk_internal_unique_name(); -std::tuple elaborate(elaborator_env & env, list const & ctx, expr const & e, +std::tuple elaborate(elaborator_context & 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(elaborator_env & 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, 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 fd23d18f6..f0b71480b 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -15,7 +15,7 @@ Author: Leonardo de Moura namespace lean { /** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */ -class elaborator_env { +class elaborator_context { environment m_env; io_state m_ios; local_decls m_lls; // local universe levels @@ -27,13 +27,13 @@ class elaborator_env { 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); + elaborator_context(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, +std::tuple elaborate(elaborator_context & 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, +std::tuple elaborate(elaborator_context & 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 46b577f16..f03c114dc 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -517,16 +517,16 @@ 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_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); } -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_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); } -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); +elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) { + return elaborator_context(env, m_ios, lls, &pp, m_info_manager, true); } std::tuple parser::elaborate_relaxed(expr const & e, list const & ctx) { @@ -534,7 +534,7 @@ std::tuple parser::elaborate_relaxed(expr const & e, li bool check_unassigned = false; bool ensure_type = false; parser_pos_provider pp = get_pos_provider(); - elaborator_env env = mk_elaborator_env(pp, check_unassigned); + elaborator_context env = mk_elaborator_context(pp, check_unassigned); auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type); m_pre_info_data.clear(); return r; @@ -545,7 +545,7 @@ std::tuple parser::elaborate_type(expr const & e, list< bool check_unassigned = true; bool ensure_type = true; parser_pos_provider pp = get_pos_provider(); - elaborator_env env = mk_elaborator_env(pp, check_unassigned); + elaborator_context env = mk_elaborator_context(pp, check_unassigned); auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type); m_pre_info_data.clear(); return r; @@ -554,7 +554,7 @@ std::tuple parser::elaborate_type(expr const & e, list< std::tuple parser::elaborate_at(environment const & env, expr const & e) { bool relax = false; parser_pos_provider pp = get_pos_provider(); - elaborator_env eenv = mk_elaborator_env(env, pp); + elaborator_context eenv = mk_elaborator_context(env, pp); auto r = ::lean::elaborate(eenv, list(), e, relax); m_pre_info_data.clear(); return r; @@ -563,7 +563,7 @@ std::tuple parser::elaborate_at(environment const & env std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) { parser_pos_provider pp = get_pos_provider(); - elaborator_env eenv = mk_elaborator_env(pp); + elaborator_context eenv = mk_elaborator_context(pp); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); m_pre_info_data.clear(); return r; @@ -572,7 +572,7 @@ 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(); - elaborator_env eenv = mk_elaborator_env(env, lls, pp); + elaborator_context eenv = mk_elaborator_context(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 3d7317f68..bd8cb4277 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -163,9 +163,9 @@ 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); + 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); public: parser(environment const & env, io_state const & ios,