From f830bf54c222467080b8b5d26ffd220d9216bd0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 May 2015 14:32:36 -0700 Subject: [PATCH] refactor(*): clarify name_generator ownership --- src/frontends/lean/calc_proof_elaborator.cpp | 14 ++++++----- src/frontends/lean/coercion_elaborator.cpp | 2 +- src/frontends/lean/elaborator.cpp | 22 ++++++++--------- src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/server.cpp | 7 +++--- src/kernel/constraint.h | 2 +- src/kernel/environment.h | 2 +- src/kernel/expr.h | 2 -- src/kernel/type_checker.cpp | 12 +++++----- src/kernel/type_checker.h | 6 ++--- src/library/class.cpp | 2 +- src/library/inductive_unifier_plugin.cpp | 6 ++--- src/library/kernel_bindings.cpp | 10 ++++---- src/library/reducible.cpp | 16 ++++++------- src/library/reducible.h | 4 ++-- src/library/tactic/class_instance_synth.cpp | 4 ++-- src/library/tactic/elaborate.h | 2 +- src/library/unifier.cpp | 25 ++++++++++---------- src/library/unifier.h | 4 ++-- src/library/unifier_plugin.cpp | 10 ++++---- src/library/unifier_plugin.h | 2 +- src/tests/library/unifier.cpp | 3 +-- 22 files changed, 80 insertions(+), 79 deletions(-) diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index d6cb8bde7..81346ed16 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -123,11 +123,10 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, info_manager * im, update_type_info_fn const & fn) { justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & _s, - name_generator const & _ngen) { + name_generator && ngen) { local_context ctx = _ctx; expr e = _e; substitution s = _s; - name_generator ngen(_ngen); type_checker_ptr tc(mk_type_checker(env, ngen.mk_child())); constraint_seq new_cs = cs; expr e_type = tc->infer(e, new_cs); @@ -169,7 +168,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, unifier_config new_cfg(cfg); new_cfg.m_discard = false; new_cfg.m_kind = conservative ? unifier_kind::Conservative : unifier_kind::Liberal; - unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg); + unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen.mk_child(), substitution(), new_cfg); auto p = seq.pull(); lean_assert(p); substitution new_s = p->first.first; @@ -218,8 +217,10 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, // 4. subst (eq.symm pr) (eq.refl lhs) if (symm) { constraint_seq subst_cs = symm_cs; - if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) { - try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {} + if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, + meta_type, subst_cs, g)) { + try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } + catch (exception&) {} } } } @@ -240,7 +241,8 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, constraint_seq symm_cs = new_cs; auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g); if (symm) { - try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } catch (exception &) {} + try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } + catch (exception &) {} } // We use the exception for the first alternative as the error message diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp index 1c8ec63e0..5f6401ea4 100644 --- a/src/frontends/lean/coercion_elaborator.cpp +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -62,7 +62,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) { auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s, - name_generator const & /* ngen */) { + name_generator && /* ngen */) { expr new_a_type; justification new_a_type_jst; if (is_meta(a_type)) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b122febca..c277ecebf 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -80,13 +80,13 @@ public: } }; -type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator const & ngen) { - return std::unique_ptr(new type_checker(env, ngen, +type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator && ngen) { + return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new coercion_from_converter(env)))); } -type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator const & ngen) { - return std::unique_ptr(new type_checker(env, ngen, +type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator && ngen) { + return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new coercion_to_converter(env)))); } @@ -141,7 +141,7 @@ struct elaborator::choice_expr_elaborator : public choice_iterator { } }; -elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names): +elaborator::elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names): m_ctx(ctx), m_ngen(ngen), m_context(), @@ -334,7 +334,7 @@ expr elaborator::visit_choice(expr const & e, optional const & t, constrai local_context ctx = m_context; local_context full_ctx = m_full_context; auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */, - name_generator const & /* ngen */) { + name_generator && /* ngen */) { return choose(std::make_shared(*this, ctx, full_ctx, meta, type, e)); }; auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main) { @@ -471,7 +471,7 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) { return pp_function_expected(fmt, substitution(subst).instantiate(f)); }); - auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator const &) { + auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator &&) { flet save1(m_context, ctx); flet save2(m_full_context, full_ctx); list choices = map2(coes, [&](expr const & coe) { @@ -1112,13 +1112,13 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) { io_state const & _ios = ios(); justification j = mk_failed_to_synthesize_jst(_env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, - name_generator const & ngen) { + name_generator && ngen) { substitution new_s = s; expr new_eqns = new_s.instantiate_all(eqns); new_eqns = solve_unassigned_mvars(new_s, new_eqns); if (display_unassigned_mvars(new_eqns, new_s)) return lazy_list(); - type_checker_ptr tc = mk_type_checker(_env, ngen); + type_checker_ptr tc = mk_type_checker(_env, std::move(ngen)); new_eqns = assign_equation_lhs_metas(*tc, new_eqns); expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type); justification j = mk_justification("equation compilation", some_expr(eqns)); @@ -1687,9 +1687,9 @@ optional elaborator::get_pre_tactic_for(expr const & mvar) { optional elaborator::pre_tactic_to_tactic(expr const & pre_tac) { try { - auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional const & expected_type, + auto fn = [=](goal const & g, name_generator && ngen, expr const & e, optional const & expected_type, substitution const & subst, bool report_unassigned) { - elaborator aux_elaborator(m_ctx, ngen); + elaborator aux_elaborator(m_ctx, std::move(ngen)); // Disable tactic hints when processing expressions nested in tactics. // We must do it otherwise, it is easy to make the system loop. bool use_tactic_hints = false; diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index c510ce9d4..811196187 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -181,7 +181,7 @@ class elaborator : public coercion_info_manager { expr const & goal, bool first, constraint_seq & cs, expr const & src); expr visit_obtain_expr(expr const & e, constraint_seq & cs); public: - elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false); + elaborator(elaborator_context & ctx, name_generator && ngen, 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); }; diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index d04b71514..e0bb98300 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -774,8 +774,8 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type } } -static std::unique_ptr mk_find_goal_type_checker(environment const & env, name_generator const & ngen) { - return mk_opaque_type_checker(env, ngen); +static std::unique_ptr mk_find_goal_type_checker(environment const & env, name_generator && ngen) { + return mk_opaque_type_checker(env, std::move(ngen)); } static name * g_tmp_prefix = nullptr; @@ -794,8 +794,7 @@ void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string m_out << std::endl; environment const & env = env_opts->first; options const & opts = env_opts->second; - name_generator ngen(*g_tmp_prefix); - std::unique_ptr tc = mk_find_goal_type_checker(env, ngen); + std::unique_ptr tc = mk_find_goal_type_checker(env, name_generator(*g_tmp_prefix)); if (auto meta = m_file->infom().get_meta_at(line_num, col_num)) { if (is_meta(*meta)) { if (auto type = m_file->infom().get_type_at(line_num, col_num)) { diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index e6fc68e03..5bb77fa6d 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -57,7 +57,7 @@ typedef list constraints; One application of choice constraints is overloaded notation. */ -typedef std::function(expr const &, expr const &, substitution const &, name_generator const &)> choice_fn; +typedef std::function(expr const &, expr const &, substitution const &, name_generator &&)> choice_fn; struct constraint_cell; class constraint { diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 904118c1a..a970cad06 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -224,7 +224,7 @@ class name_generator; Only the type_checker class can create certified declarations. */ class certified_declaration { - friend certified_declaration check(environment const & env, declaration const & d, name_generator const & g); + friend certified_declaration check(environment const & env, declaration const & d, name_generator && g); environment_id m_id; declaration m_declaration; certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {} diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 63d86b924..4a6f9907d 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -483,8 +483,6 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const /** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */ expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag); -expr mk_local_for(expr const & b, name_generator const & ngen, tag g = nulltag); - bool enable_expr_caching(bool f); /** \brief Helper class for temporarily enabling/disabling expression caching */ struct scoped_expr_caching { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 432be973d..e60ceb2d6 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -416,13 +416,13 @@ bool type_checker::is_opaque(expr const & c) const { return true; } -type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize): +type_checker::type_checker(environment const & env, name_generator && g, std::unique_ptr && conv, bool memoize): m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this), m_memoize(memoize), m_params(nullptr) { } -type_checker::type_checker(environment const & env, name_generator const & g, bool memoize): - type_checker(env, g, std::unique_ptr(new default_converter(env, memoize)), memoize) {} +type_checker::type_checker(environment const & env, name_generator && g, bool memoize): + type_checker(env, std::move(g), std::unique_ptr(new default_converter(env, memoize)), memoize) {} static name * g_tmp_prefix = nullptr; @@ -472,18 +472,18 @@ static void check_duplicated_params(environment const & env, declaration const & } } -certified_declaration check(environment const & env, declaration const & d, name_generator const & g) { +certified_declaration check(environment const & env, declaration const & d, name_generator && g) { if (d.is_definition()) check_no_mlocal(env, d.get_name(), d.get_value(), false); check_no_mlocal(env, d.get_name(), d.get_type(), true); check_name(env, d.get_name()); check_duplicated_params(env, d); bool memoize = true; - type_checker checker1(env, g, std::unique_ptr(new default_converter(env, memoize))); + type_checker checker1(env, g.mk_child(), std::unique_ptr(new default_converter(env, memoize))); expr sort = checker1.check(d.get_type(), d.get_univ_params()).first; checker1.ensure_sort(sort, d.get_type()); if (d.is_definition()) { - type_checker checker2(env, g, std::unique_ptr(new default_converter(env, memoize))); + type_checker checker2(env, g.mk_child(), std::unique_ptr(new default_converter(env, memoize))); expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first; if (!checker2.is_def_eq(val_type, d.get_type()).first) { throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 138bdf307..d183a84eb 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -123,8 +123,8 @@ public: memoize: if true, then inferred types are memoized/cached */ - type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize = true); - type_checker(environment const & env, name_generator const & g, bool memoize = true); + type_checker(environment const & env, name_generator && g, std::unique_ptr && conv, bool memoize = true); + type_checker(environment const & env, name_generator && g, bool memoize = true); type_checker(environment const & env); ~type_checker(); @@ -235,7 +235,7 @@ void check_no_metavar(environment const & env, name const & n, expr const & e, b \brief Type check the given declaration, and return a certified declaration if it is type correct. Throw an exception if the declaration is type incorrect. */ -certified_declaration check(environment const & env, declaration const & d, name_generator const & g); +certified_declaration check(environment const & env, declaration const & d, name_generator && g); certified_declaration check(environment const & env, declaration const & d); /** diff --git a/src/library/class.cpp b/src/library/class.cpp index 719a2662b..74f464453 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -187,7 +187,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior declaration d = env.get(n); expr type = d.get_type(); name_generator ngen(*g_tmp_prefix); - auto tc = mk_type_checker(env, ngen); + auto tc = mk_type_checker(env, ngen.mk_child()); while (true) { type = tc->whnf(type).first; if (!is_pi(type)) diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp index 63d715376..1aa92eb65 100644 --- a/src/library/inductive_unifier_plugin.cpp +++ b/src/library/inductive_unifier_plugin.cpp @@ -43,7 +43,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...) to the different constructors of decl. */ - lazy_list add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl, + lazy_list add_elim_meta_cnstrs(type_checker & tc, name_generator & ngen, inductive::inductive_decl const & decl, expr const & elim, buffer & args, expr const & t, justification const & j, constraint_seq cs) const { lean_assert(is_constant(elim)); @@ -87,7 +87,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { return to_lazy(to_list(alts.begin(), alts.end())); } - lazy_list process_elim_meta_core(type_checker & tc, name_generator const & ngen, + lazy_list process_elim_meta_core(type_checker & tc, name_generator & ngen, expr const & lhs, expr const & rhs, justification const & j) const { lean_assert(inductive::is_elim_meta_app(tc, lhs)); auto dcs = tc.is_def_eq_types(lhs, rhs, j); @@ -111,7 +111,7 @@ public: \brief Try to solve constraint of the form (elim ... (?m ...)) =?= t, by assigning (?m ...) to the introduction rules associated with the eliminator \c elim. */ - virtual lazy_list solve(type_checker & tc, constraint const & c, name_generator const & ngen) const { + virtual lazy_list solve(type_checker & tc, constraint const & c, name_generator && ngen) const { if (!is_eq_cnstr(c)) return lazy_list(); expr const & lhs = cnstr_lhs_expr(c); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 52709cd8c..e7a127648 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1766,7 +1766,8 @@ static int mk_type_checker(lua_State * L) { if (nargs == 1) { return push_type_checker_ref(L, std::make_shared(to_environment(L, 1))); } else { - return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2))); + return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), + to_name_generator(L, 2).mk_child())); } } static int type_checker_whnf(lua_State * L) { return push_ecs(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); } @@ -1802,7 +1803,7 @@ static int mk_type_checker_with_hints(lua_State * L) { if (nargs == 1) { return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix))); } else { - return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2))); + return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2).mk_child())); } } @@ -1824,7 +1825,8 @@ static int type_check(lua_State * L) { if (nargs == 2) { return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2))); } else { - return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3))); + return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), + to_name_generator(L, 3).mk_child())); } } @@ -1835,7 +1837,7 @@ static int add_declaration(lua_State * L) { if (nargs == 2) { d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2))); } else { - d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3)); + d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3).mk_child()); } return push_environment(L, module::add(to_environment(L, 1), *d)); } diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 7f4f6ae3f..24cb23b7b 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -134,17 +134,17 @@ bool unfold_semireducible_converter::is_opaque(declaration const & d) const { return default_converter::is_opaque(d); } -std::unique_ptr mk_type_checker(environment const & env, name_generator const & ngen, +std::unique_ptr mk_type_checker(environment const & env, name_generator && ngen, reducible_behavior rb, bool memoize) { switch (rb) { case UnfoldReducible: - return std::unique_ptr(new type_checker(env, ngen, + return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new unfold_reducible_converter(env, memoize)))); case UnfoldQuasireducible: - return std::unique_ptr(new type_checker(env, ngen, + return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new unfold_quasireducible_converter(env, memoize)))); case UnfoldSemireducible: - return std::unique_ptr(new type_checker(env, ngen, + return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new unfold_semireducible_converter(env, memoize)))); } lean_unreachable(); @@ -160,8 +160,8 @@ public: virtual bool is_opaque(declaration const &) const { return true; } }; -std::unique_ptr mk_opaque_type_checker(environment const & env, name_generator const & ngen) { - return std::unique_ptr(new type_checker(env, ngen, +std::unique_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen) { + return std::unique_ptr(new type_checker(env, std::move(ngen), std::unique_ptr(new opaque_converter(env)))); } @@ -174,7 +174,7 @@ static int mk_opaque_type_checker(lua_State * L) { type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), name_generator())); return push_type_checker_ref(L, r); } else { - type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), to_name_generator(L, 2))); + type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), to_name_generator(L, 2).mk_child())); return push_type_checker_ref(L, r); } } @@ -188,7 +188,7 @@ static int mk_reducible_checker_core(lua_State * L, reducible_behavior rb) { type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), rb)); return push_type_checker_ref(L, r); } else { - type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), rb)); + type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2).mk_child(), rb)); return push_type_checker_ref(L, r); } } diff --git a/src/library/reducible.h b/src/library/reducible.h index 9c72b612b..499809ddd 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -63,13 +63,13 @@ public: enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireducible }; /** \brief Create a type checker that takes the "reducibility" hints into account. */ -std::unique_ptr mk_type_checker(environment const & env, name_generator const & ngen, +std::unique_ptr mk_type_checker(environment const & env, name_generator && ngen, reducible_behavior r = UnfoldSemireducible, bool memoize = true); std::unique_ptr mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible); /** \brief Create a type checker that treats all definitions as opaque. */ -std::unique_ptr mk_opaque_type_checker(environment const & env, name_generator const & ngen); +std::unique_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen); void initialize_reducible(); void finalize_reducible(); diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index 2c651d83b..209330af7 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -328,7 +328,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, - name_generator const & ngen) { + name_generator && ngen) { environment const & env = C->env(); auto cls_name_it = is_ext_class(C->tc(), meta_type); if (!cls_name_it) { @@ -368,7 +368,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr return lazy_list(constraints()); }; - unify_result_seq seq1 = unify(env, 1, &c, ngen, substitution(), new_cfg); + unify_result_seq seq1 = unify(env, 1, &c, std::move(ngen), substitution(), new_cfg); unify_result_seq seq2 = filter(seq1, [=](pair const & p) { substitution new_s = p.first; expr result = new_s.instantiate(new_meta); diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index 7ffe85d32..8a09461d0 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -25,7 +25,7 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat 3- postponed constraints */ typedef std::tuple elaborate_result; -typedef std::function const &, substitution const &, bool)> elaborate_fn; /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 970243cd8..ade676e8f 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -432,7 +432,7 @@ struct unifier_fn { optional m_conflict; //!< if different from none, then there is a conflict. unifier_fn(environment const & env, unsigned num_cs, constraint const * cs, - name_generator const & ngen, substitution const & s, + name_generator && ngen, substitution const & s, unifier_config const & cfg): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), m_config(cfg), m_num_steps(0) { @@ -2326,17 +2326,17 @@ unify_result_seq unify(std::shared_ptr u) { } } -unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, +unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator && ngen, substitution const & s, unifier_config const & cfg) { - return unify(std::make_shared(env, num_cs, cs, ngen, s, cfg)); + return unify(std::make_shared(env, num_cs, cs, std::move(ngen), s, cfg)); } -unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, +unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator && ngen, substitution const & s, unifier_config const & cfg) { substitution new_s = s; expr _lhs = new_s.instantiate(lhs); expr _rhs = new_s.instantiate(rhs); - auto u = std::make_shared(env, 0, nullptr, ngen, new_s, cfg); + auto u = std::make_shared(env, 0, nullptr, std::move(ngen), new_s, cfg); constraint_seq cs; if (!u->m_tc->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) { return unify_result_seq(); @@ -2411,7 +2411,7 @@ static constraints to_constraints(lua_State * L, int idx) { static unifier_plugin to_unifier_plugin(lua_State * L, int idx) { luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun luaref f(L, idx); - return unifier_plugin([=](constraint const & c, name_generator const & ngen) { + return unifier_plugin([=](constraint const & c, name_generator && ngen) { lua_State * L = f.get_state(); f.push(); push_constraint(L, c); @@ -2465,21 +2465,22 @@ static int unify(lua_State * L) { environment const & env = to_environment(L, 1); if (is_expr(L, 2)) { if (nargs == 6) - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child(), to_substitution(L, 5), unifier_config(to_options(L, 6))); else if (nargs == 5) - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5)); + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child(), to_substitution(L, 5)); else - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4)); + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child()); } else { buffer cs; to_constraint_buffer(L, 2, cs); if (nargs == 5) - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4), unifier_config(to_options(L, 5))); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child(), to_substitution(L, 4), + unifier_config(to_options(L, 5))); else if (nargs == 4) - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4)); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child(), to_substitution(L, 4)); else - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3)); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child()); } return push_unify_result_seq_it(L, r); } diff --git a/src/library/unifier.h b/src/library/unifier.h index 1730daeee..09172a727 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -74,9 +74,9 @@ struct unifier_config { /** \brief The unification procedures produce a lazy list of pair substitution + constraints that could not be solved. */ typedef lazy_list> unify_result_seq; -unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, +unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator && ngen, substitution const & s = substitution(), unifier_config const & c = unifier_config()); -unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, +unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator && ngen, substitution const & s = substitution(), unifier_config const & c = unifier_config()); /** diff --git a/src/library/unifier_plugin.cpp b/src/library/unifier_plugin.cpp index 846541207..b9dcf3050 100644 --- a/src/library/unifier_plugin.cpp +++ b/src/library/unifier_plugin.cpp @@ -22,16 +22,16 @@ public: class append_unifier_plugin_cell : public binary_unifier_plugin_cell { public: append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {} - virtual lazy_list solve(type_checker & tc, constraint const & c, name_generator const & ngen) const { - return append(m_p1->solve(tc, c, ngen), m_p2->solve(tc, c, ngen)); + virtual lazy_list solve(type_checker & tc, constraint const & c, name_generator && ngen) const { + return append(m_p1->solve(tc, c, ngen.mk_child()), m_p2->solve(tc, c, ngen.mk_child())); } }; class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell { public: orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {} - virtual lazy_list solve(type_checker & tc, constraint const & c, name_generator const & ngen) const { - return orelse(m_p1->solve(tc, c, ngen), m_p2->solve(tc, c, ngen)); + virtual lazy_list solve(type_checker & tc, constraint const & c, name_generator && ngen) const { + return orelse(m_p1->solve(tc, c, ngen.mk_child()), m_p2->solve(tc, c, ngen.mk_child())); } }; @@ -46,7 +46,7 @@ unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2) { static unifier_plugin noop_unifier_plugin() { class noop_unifier_plugin_cell : public unifier_plugin_cell { public: - virtual lazy_list solve(type_checker &, constraint const &, name_generator const &) const { + virtual lazy_list solve(type_checker &, constraint const &, name_generator &&) const { return lazy_list(); } virtual bool delay_constraint(type_checker &, constraint const &) const { return false; } diff --git a/src/library/unifier_plugin.h b/src/library/unifier_plugin.h index 484552b3d..3c2adccbe 100644 --- a/src/library/unifier_plugin.h +++ b/src/library/unifier_plugin.h @@ -23,7 +23,7 @@ namespace lean { class unifier_plugin_cell { public: virtual ~unifier_plugin_cell() {} - virtual lazy_list solve(type_checker &, constraint const &, name_generator const &) const = 0; + virtual lazy_list solve(type_checker &, constraint const &, name_generator &&) const = 0; virtual bool delay_constraint(type_checker &, constraint const &) const = 0; }; diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp index 96c65ee87..dad089ad4 100644 --- a/src/tests/library/unifier.cpp +++ b/src/tests/library/unifier.cpp @@ -14,7 +14,6 @@ using namespace lean; static void tst1() { environment env; - name_generator ngen("foo"); expr Type = mk_Type(); expr A = Local("A", Type); expr f = Local("f", A >> (A >> A)); @@ -23,7 +22,7 @@ static void tst1() { expr m = mk_metavar("m", A); expr t1 = mk_app(f, m, m); expr t2 = mk_app(f, a, b); - auto r = unify(env, t1, t2, ngen); + auto r = unify(env, t1, t2, name_generator("foo")); lean_assert(!r.pull()); }