From edeae776da311be0c951806158eb8f49caeef034 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 May 2019 11:23:35 -0700 Subject: [PATCH] chore(library/module): `module::add` for declarations is not needed anymore --- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/decl_cmds.cpp | 2 +- src/frontends/lean/definition_cmds.cpp | 5 ++--- src/frontends/lean/inductive_cmds.cpp | 3 +-- src/frontends/lean/lean_elaborator.cpp | 2 +- src/frontends/lean/parser.cpp | 1 - src/frontends/lean/structure_cmd.cpp | 9 ++++----- src/library/aux_definition.cpp | 3 +-- src/library/compiler/eager_lambda_lifting.cpp | 2 +- src/library/compiler/llnf_code.cpp | 1 - src/library/compiler/specialize.cpp | 5 ++--- src/library/compiler/util.cpp | 5 ++--- src/library/constructions/brec_on.cpp | 5 ++--- src/library/constructions/cases_on.cpp | 3 +-- src/library/constructions/no_confusion.cpp | 5 ++--- src/library/constructions/projection.cpp | 3 +-- src/library/constructions/rec_on.cpp | 6 ++---- src/library/derive_attribute.cpp | 5 ++--- src/library/equations_compiler/unbounded_rec.cpp | 3 +-- src/library/equations_compiler/util.cpp | 3 +-- src/library/module.h | 3 --- 21 files changed, 28 insertions(+), 48 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 01edd6ce73..c79c83ff90 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -336,7 +336,7 @@ static environment help_cmd(parser & p) { } static environment init_quot_cmd(parser & p) { - return module::add(p.env(), mk_quot_decl()); + return p.env().add(mk_quot_decl()); } /* diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 573c00be14..45d43df43f 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -100,7 +100,7 @@ static environment declare_var(parser & p, environment env, expr new_type = Pi(new_params, type); bool is_unsafe = meta.m_modifiers.m_is_unsafe; - env = module::add(env, mk_axiom(full_n, ls, new_type, is_unsafe)); + env = env.add(mk_axiom(full_n, ls, new_type, is_unsafe)); if (!ns.is_anonymous()) { if (meta.m_modifiers.m_is_protected) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 1789bfc145..8116bc1971 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/private.h" #include "library/protected.h" -#include "library/module.h" #include "library/aux_definition.h" #include "library/scope_pos_info_provider.h" #include "library/replace_visitor.h" @@ -211,7 +210,7 @@ declare_definition(environment const & env, decl_cmd_kind kind, buffer con default: throw exception("unknown command declaration"); } - new_env = module::add(new_env, def); + new_env = new_env.add(def); if (meta.m_modifiers.m_is_protected) new_env = add_protected(new_env, c_real_name); @@ -478,7 +477,7 @@ static void check_example(environment const & decl_env, options const & opts, bool is_unsafe = modifiers.m_is_unsafe; auto new_env = elab.env(); declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_unsafe); - new_env = module::add(new_env, def); + new_env = new_env.add(def); } catch (throwable & ex) { message_builder error_msg(tc, decl_env, get_global_ios(), pos_provider.get_file_name(), pos_provider.get_some_pos(), diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 3e7166f6d1..21d4544f51 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -25,7 +25,6 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/reducible.h" #include "library/class.h" #include "library/trace.h" -#include "library/module.h" #include "library/type_context.h" #include "library/constants.h" #include "library/tactic/tactic_evaluator.h" @@ -721,7 +720,7 @@ public: } ind_types.push_back(inductive_type(local_name_p(r.m_inds[i]), Pi(r.m_params, local_type_p(r.m_inds[i])), constructors(cnstrs))); } - m_env = module::add(m_env, mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_unsafe)); + m_env = m_env.add(mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_unsafe)); bool has_eq = has_eq_decls(m_env); bool has_heq = has_heq_decls(m_env); diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 4daf797a88..f07f0bead2 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -395,7 +395,7 @@ static void elaborate_command(parser & p, expr const & cmd) { elab_structure_cmd(p, cmd); return; } else if (*cmd_name == "initQuot") { - p.set_env(module::add(p.env(), mk_quot_decl())); + p.set_env(p.env().add(mk_quot_decl())); return; } else if (*cmd_name == "variables") { elab_variables_cmd(p, cmd); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8fc2a703ef..ab5116f476 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -33,7 +33,6 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/placeholder.h" #include "library/deep_copy.h" -#include "library/module.h" #include "library/explicit.h" #include "library/num.h" #include "library/string.h" diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 4c7ec94369..90a85ee390 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -24,7 +24,6 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/locals.h" #include "library/reducible.h" -#include "library/module.h" #include "library/aliases.h" #include "library/annotation.h" #include "library/explicit.h" @@ -1068,7 +1067,7 @@ struct structure_cmd_fn { constructor cnstr(m_mk, intro_type); inductive_type S(m_name, structure_type, constructors(cnstr)); declaration decl = mk_inductive_decl(lnames, nat(m_params.size()), inductive_types(S), is_unsafe); - m_env = module::add(m_env, decl); + m_env = m_env.add(decl); name rec_name = mk_rec_name(m_name); m_env = add_namespace(m_env, m_name); m_env = add_protected(m_env, rec_name); @@ -1143,7 +1142,7 @@ struct structure_cmd_fn { names decl_lvls = to_names(used_univs); declaration new_decl = mk_definition_inferring_unsafe(m_env, decl_name, decl_lvls, decl_type, decl_value, reducibility_hints::mk_abbreviation()); - m_env = module::add(m_env, new_decl); + m_env = m_env.add(new_decl); m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true); } } @@ -1155,7 +1154,7 @@ struct structure_cmd_fn { declaration new_decl = mk_definition_inferring_unsafe(m_env, n, rec_on_decl.get_lparams(), rec_on_decl.get_type(), rec_on_decl.get_value(), reducibility_hints::mk_abbreviation()); - m_env = module::add(m_env, new_decl); + m_env = m_env.add(new_decl); m_env = set_reducible(m_env, n, reducible_status::Reducible, true); add_alias(n); } @@ -1247,7 +1246,7 @@ struct structure_cmd_fn { name coercion_name = coercion_names[i]; declaration coercion_decl = mk_definition_inferring_unsafe(m_env, coercion_name, lnames, coercion_type, coercion_value); - m_env = module::add(m_env, coercion_decl); + m_env = m_env.add(coercion_decl); add_alias(coercion_name); m_env = compile(m_env, m_p.get_options(), coercion_name); if (!m_private_parents[i]) { diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index afd4317888..8bc6ad79de 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "library/locals.h" #include "library/placeholder.h" -#include "library/module.h" #include "library/trace.h" #include "library/aux_definition.h" #include "library/replace_visitor_with_tc.h" @@ -167,7 +166,7 @@ struct mk_aux_definition_fn : public closure_helper { } else { d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, *is_unsafe); } - environment new_env = module::add(env, d); + environment new_env = env.add(d); buffer ls; get_level_closure(ls); buffer ps; diff --git a/src/library/compiler/eager_lambda_lifting.cpp b/src/library/compiler/eager_lambda_lifting.cpp index 857cdce2b6..51f0437d5f 100644 --- a/src/library/compiler/eager_lambda_lifting.cpp +++ b/src/library/compiler/eager_lambda_lifting.cpp @@ -150,7 +150,7 @@ class eager_lambda_lifting_fn { other definitions that use `n`. We used a similar hack at `specialize.cpp`. */ declaration aux_ax = mk_axiom(n, names(), type, true /* meta */); - m_st.env() = module::add(env(), aux_ax, false); + m_st.env() = env().add(aux_ax, false); m_new_decls.push_back(comp_decl(n, code)); return mk_app(mk_constant(n), fvars); } diff --git a/src/library/compiler/llnf_code.cpp b/src/library/compiler/llnf_code.cpp index 71a8f3ec84..cfd0d51827 100644 --- a/src/library/compiler/llnf_code.cpp +++ b/src/library/compiler/llnf_code.cpp @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "runtime/sstream.h" -#include "library/module.h" #include "library/compiler/util.h" #include "library/compiler/init_attribute.h" diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index 40f1edbffe..b147cdf9f4 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -10,13 +10,12 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/abstract.h" #include "library/class.h" +#include "library/trace.h" #include "library/module.h" #include "library/attribute_manager.h" #include "library/compiler/util.h" #include "library/compiler/csimp.h" -#include "library/trace.h" - namespace lean { bool has_specialize_attribute(environment const & env, name const & n) { if (has_attribute(env, "specialize", n)) @@ -946,7 +945,7 @@ class specialize_fn { { expr type = cheap_beta_reduce(type_checker(m_st).infer(code)); declaration aux_ax = mk_axiom(n, names(), type, true /* meta */); - m_st.env() = module::add(env(), aux_ax, false); + m_st.env() = env().add(aux_ax, false); } code = eta_expand_specialization(code); // lean_trace(name("compiler", "spec_info"), tout() << "STEP 2 " << n << "\n" << code << "\n";); diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index 0583f42a73..bb66de4ec0 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include "library/aux_recursors.h" #include "library/replace_visitor.h" #include "library/constants.h" -#include "library/module.h" #include "library/trace.h" #include "library/compiler/lambda_lifting.h" #include "library/compiler/eager_lambda_lifting.h" @@ -504,7 +503,7 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) { environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v) { declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), true); - return module::add(env, aux_decl, false); + return env.add(aux_decl, false); } bool is_stage2_decl(environment const & env, name const & n) { @@ -514,7 +513,7 @@ bool is_stage2_decl(environment const & env, name const & n) { environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v) { declaration aux_decl = mk_definition(mk_cstage2_name(n), names(), t, v, reducibility_hints::mk_opaque(), true); - return module::add(env, aux_decl, false); + return env.add(aux_decl, false); } /* @[export lean.get_num_lit_core] diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 6374a555c8..004da58d1d 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "kernel/inductive.h" #include "library/protected.h" #include "library/reducible.h" -#include "library/module.h" #include "library/bin_app.h" #include "library/suffixes.h" #include "library/util.h" @@ -142,7 +141,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow declaration new_d = mk_definition_inferring_unsafe(env, below_name, blvls, below_type, below_value, reducibility_hints::mk_abbreviation()); - environment new_env = module::add(env, new_d); + environment new_env = env.add(new_d); new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true); return add_protected(new_env, below_name); } @@ -343,7 +342,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) declaration new_d = mk_definition_inferring_unsafe(env, brec_on_name, blps, brec_on_type, brec_on_value, reducibility_hints::mk_abbreviation()); - environment new_env = module::add(env, new_d); + environment new_env = env.add(new_d); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, brec_on_name); return add_protected(new_env, brec_on_name); diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index e8fe012093..dad8a10699 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/inductive.h" -#include "library/module.h" #include "library/suffixes.h" #include "library/protected.h" #include "library/reducible.h" @@ -182,7 +181,7 @@ environment mk_cases_on(environment const & env, name const & n) { expr cases_on_value = lctx.mk_lambda(cases_on_params, mk_app(rec_cnst, rec_args)); declaration new_d = mk_definition_inferring_unsafe(env, cases_on_name, rec_info.get_lparams(), cases_on_type, cases_on_value, reducibility_hints::mk_abbreviation()); - environment new_env = module::add(env, new_d); + environment new_env = env.add(new_d); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, cases_on_name); return add_protected(new_env, cases_on_name); diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index cce434667c..98fde16105 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/type_checker.h" #include "library/protected.h" -#include "library/module.h" #include "library/util.h" #include "library/suffixes.h" #include "library/reducible.h" @@ -121,7 +120,7 @@ static optional mk_no_confusion_type(environment const & env, name expr no_confusion_type_value = lctx.mk_lambda(args, mk_app(cases_on1, outer_cases_on_args)); declaration new_d = mk_definition_inferring_unsafe(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, reducibility_hints::mk_abbreviation()); - environment new_env = module::add(env, new_d); + environment new_env = env.add(new_d); new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true); return some(add_protected(new_env, no_confusion_type_name)); } @@ -231,7 +230,7 @@ environment mk_no_confusion(environment const & env, name const & n) { expr no_confusion_val = lctx.mk_lambda(args, eq_rec); declaration new_d = mk_definition_inferring_unsafe(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, reducibility_hints::mk_abbreviation()); - new_env = module::add(new_env, new_d); + new_env = new_env.add(new_d); new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible, true); new_env = add_no_confusion(new_env, no_confusion_name); return add_protected(new_env, no_confusion_name); diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 69c8dca89d..fee7accd2f 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "library/reducible.h" #include "library/projection.h" -#include "library/module.h" #include "library/util.h" #include "library/class.h" #include "library/constructions/projection.h" @@ -100,7 +99,7 @@ environment mk_projections(environment const & env, name const & n, buffer proj_val = lctx.mk_lambda(proj_args, proj_val); declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val, reducibility_hints::mk_abbreviation()); - new_env = module::add(new_env, new_d); + new_env = new_env.add(new_d); new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true); new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index 83cf7792cd..e6c6bbdc2c 100644 --- a/src/library/constructions/rec_on.cpp +++ b/src/library/constructions/rec_on.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/inductive.h" -#include "library/module.h" #include "library/reducible.h" #include "library/protected.h" #include "library/suffixes.h" @@ -55,9 +54,8 @@ environment mk_rec_on(environment const & env, name const & n) { expr rec = mk_constant(rec_info.get_name(), ls); expr rec_on_val = lctx.mk_lambda(new_locals, mk_app(rec, locals)); - environment new_env = module::add(env, - mk_definition_inferring_unsafe(env, rec_on_name, rec_info.get_lparams(), - rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation())); + environment new_env = env.add(mk_definition_inferring_unsafe(env, rec_on_name, rec_info.get_lparams(), + rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation())); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, rec_on_name); return add_protected(new_env, rec_on_name); diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index 96bb4c6b7f..a023ac52b9 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/app_builder.h" #include "library/class.h" -#include "library/module.h" #include "library/protected.h" #include "library/sorry.h" #include "library/compiler/compiler.h" @@ -125,8 +124,8 @@ static environment derive(environment env, options const & opts, name const & n, tgt = ctx.mk_pi(params, tgt); auto inst2 = ctx.mk_lambda(params, inst.value()); auto new_n = n + const_name(cls); - env = module::add(env, mk_definition(env, new_n, d.get_lparams(), - ctx.instantiate_mvars(tgt), inst2, d.is_unsafe())); + env = env.add(mk_definition(env, new_n, d.get_lparams(), + ctx.instantiate_mvars(tgt), inst2, d.is_unsafe())); env = add_instance(env, new_n, LEAN_DEFAULT_PRIORITY, true); env = add_protected(env, new_n); env = compile(env, opts, new_n); diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp index 248d267cb3..41aa434336 100644 --- a/src/library/equations_compiler/unbounded_rec.cpp +++ b/src/library/equations_compiler/unbounded_rec.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/trace.h" #include "library/aux_definition.h" -#include "library/module.h" #include "library/compiler/compiler.h" #include "library/equations_compiler/util.h" #include "library/equations_compiler/elim_match.h" @@ -173,7 +172,7 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab, fn_actual_names = tail(fn_actual_names); } - env = module::add(env, mk_mutual_definitions(definition_vals(new_defs))); + env = env.add(mk_mutual_definitions(definition_vals(new_defs))); /* 4. Create result and add private/alias info */ buffer result_fns; diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index cf656701bf..35cdac546a 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "library/scope_pos_info_provider.h" #include "library/util.h" -#include "library/module.h" #include "library/aliases.h" #include "library/trace.h" #include "library/app_builder.h" @@ -524,7 +523,7 @@ environment mk_smart_unfolding_definition(environment const & env, options const helper_value = locals.mk_lambda(helper_value); try { declaration def = mk_definition(env, mk_smart_unfolding_name_for(n), info.get_lparams(), info.get_type(), helper_value, true); - return module::add(env, def); + return env.add(def); } catch (exception & ex) { throw nested_exception("failed to generate helper declaration for smart unfolding, type error", std::current_exception()); } diff --git a/src/library/module.h b/src/library/module.h index bb5fbc11b3..cdd02fa9bc 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -59,9 +59,6 @@ namespace module { */ environment add(environment const & env, modification * modif); environment add_and_perform(environment const & env, modification * modif); - -/** \brief Add the given declaration to the environment, and mark it to be exported. */ -environment add(environment const & env, declaration const & d, bool check = true); } void initialize_module(); void finalize_module();