diff --git a/src/api/type_checker.cpp b/src/api/type_checker.cpp index af309fdde..e3ad692e4 100644 --- a/src/api/type_checker.cpp +++ b/src/api/type_checker.cpp @@ -12,7 +12,7 @@ using namespace lean; // NOLINT lean_bool lean_type_checker_mk(lean_env e, lean_type_checker * r, lean_exception * ex) { LEAN_TRY; check_nonnull(e); - *r = of_type_checker(new type_checker(to_env_ref(e), name_generator())); + *r = of_type_checker(new type_checker(to_env_ref(e))); LEAN_CATCH; } diff --git a/src/compiler/eta_expansion.cpp b/src/compiler/eta_expansion.cpp index 7b92b7884..6d2f5caf6 100644 --- a/src/compiler/eta_expansion.cpp +++ b/src/compiler/eta_expansion.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" @@ -69,13 +70,13 @@ class eta_expand_fn : public replace_visitor { virtual expr visit_binding(expr const & b) { expr new_domain = visit(binding_domain(b)); - expr l = mk_local(m_tc.mk_fresh_name(), new_domain); + expr l = mk_local(mk_fresh_name(), new_domain); expr new_body = abstract_local(visit(instantiate(binding_body(b), l)), l); return update_binding(b, new_domain, new_body); } public: - eta_expand_fn(environment const & env):m_env(env), m_tc(env, name_generator()) {} + eta_expand_fn(environment const & env):m_env(env), m_tc(env) {} }; expr eta_expand(environment const & env, expr const & e) { diff --git a/src/compiler/preprocess_rec.cpp b/src/compiler/preprocess_rec.cpp index 502fe7147..832f10717 100644 --- a/src/compiler/preprocess_rec.cpp +++ b/src/compiler/preprocess_rec.cpp @@ -18,7 +18,7 @@ void pp(lean::environment const & env, lean::expr const & e); namespace lean { static expr expand_aux_recursors(environment const & env, expr const & e) { - auto tc = mk_type_checker(env, name_generator(), [=](name const & n) { + auto tc = mk_type_checker(env, [=](name const & n) { return !is_aux_recursor(env, n) && !is_user_defined_recursor(env, n); }); constraint_seq cs; diff --git a/src/compiler/simp_pr1_rec.cpp b/src/compiler/simp_pr1_rec.cpp index a49ef57be..ef4ba1399 100644 --- a/src/compiler/simp_pr1_rec.cpp +++ b/src/compiler/simp_pr1_rec.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" @@ -16,7 +17,6 @@ Author: Leonardo de Moura namespace lean { class simp_pr1_rec_fn : public replace_visitor { environment m_env; - name_generator m_ngen; type_checker m_tc; struct failed {}; @@ -92,7 +92,7 @@ class simp_pr1_rec_fn : public replace_visitor { // (lambda ctx, prod c1 c2), and replace it with (lambda ctx, c1) expr typeformer = rec_args[i]; buffer typeformer_ctx; - expr typeformer_body = fun_to_telescope(m_ngen, typeformer, typeformer_ctx, optional()); + expr typeformer_body = fun_to_telescope(typeformer, typeformer_ctx, optional()); buffer typeformer_body_args; expr typeformer_body_fn = get_app_args(typeformer_body, typeformer_body_args); @@ -107,7 +107,7 @@ class simp_pr1_rec_fn : public replace_visitor { buffer const & minor_is_rec_arg = is_rec_arg[j]; expr minor = rec_args[i]; buffer minor_ctx; - expr minor_body = fun_to_telescope(m_ngen, minor, minor_ctx, optional()); + expr minor_body = fun_to_telescope(minor, minor_ctx, optional()); if (minor_is_rec_arg.size() != minor_ctx.size()) { return none_expr(); } @@ -159,13 +159,13 @@ class simp_pr1_rec_fn : public replace_visitor { virtual expr visit_binding(expr const & b) { expr new_domain = visit(binding_domain(b)); - expr l = mk_local(m_ngen.next(), new_domain); + expr l = mk_local(mk_fresh_name(), new_domain); expr new_body = abstract_local(visit(instantiate(binding_body(b), l)), l); return update_binding(b, new_domain, new_body); } public: - simp_pr1_rec_fn(environment const & env):m_env(env), m_tc(env, m_ngen.mk_child()) {} + simp_pr1_rec_fn(environment const & env):m_env(env), m_tc(env) {} }; expr simp_pr1_rec(environment const & env, expr const & e) { diff --git a/src/compiler/util.cpp b/src/compiler/util.cpp index 860145dcd..a52fb1b57 100644 --- a/src/compiler/util.cpp +++ b/src/compiler/util.cpp @@ -26,14 +26,13 @@ static bool is_typeformer_app(buffer const & typeformer_names, expr const void get_rec_args(environment const & env, name const & n, buffer> & r) { lean_assert(inductive::is_inductive_decl(env, n)); type_checker tc(env); - name_generator ngen; declaration ind_decl = env.get(n); declaration rec_decl = env.get(inductive::get_elim_name(n)); unsigned nparams = *inductive::get_num_params(env, n); unsigned nminors = *inductive::get_num_minor_premises(env, n); unsigned ntypeformers = *inductive::get_num_type_formers(env, n); buffer rec_args; - to_telescope(ngen, rec_decl.get_type(), rec_args); + to_telescope(rec_decl.get_type(), rec_args); buffer typeformer_names; for (unsigned i = nparams; i < nparams + ntypeformers; i++) { typeformer_names.push_back(mlocal_name(rec_args[i])); @@ -46,7 +45,7 @@ void get_rec_args(environment const & env, name const & n, buffer> buffer & bv = r.back(); expr minor_type = mlocal_type(rec_args[i]); buffer minor_args; - to_telescope(ngen, minor_type, minor_args); + to_telescope(minor_type, minor_args); for (expr & minor_arg : minor_args) { buffer minor_arg_args; expr minor_arg_type = to_telescope(tc, mlocal_type(minor_arg), minor_arg_args); @@ -57,7 +56,6 @@ void get_rec_args(environment const & env, name const & n, buffer> bool is_recursive_rec_app(environment const & env, expr const & e) { buffer args; - name_generator ngen; expr const & f = get_app_args(e, args); if (!is_constant(f)) return false; @@ -73,7 +71,7 @@ bool is_recursive_rec_app(environment const & env, expr const & e) { buffer const & minor_is_rec_arg = is_rec_arg[j]; expr minor = args[i]; buffer minor_ctx; - expr minor_body = fun_to_telescope(ngen, minor, minor_ctx, optional()); + expr minor_body = fun_to_telescope(minor, minor_ctx, optional()); unsigned sz = std::min(minor_is_rec_arg.size(), minor_ctx.size()); if (find(minor_body, [&](expr const & e, unsigned) { if (!is_local(e)) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 90ed28c1a..63d14c470 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -117,7 +117,7 @@ environment check_cmd(parser & p) { expr e; level_param_names ls; std::tie(e, ls) = parse_local_expr(p); e = expand_abbreviations(p.env(), e); - auto tc = mk_type_checker(p.env(), p.mk_ngen()); + auto tc = mk_type_checker(p.env()); expr type = tc->check(e, ls).first; auto reg = p.regular_stream(); formatter fmt = reg.get_formatter(); @@ -145,7 +145,7 @@ environment eval_cmd(parser & p) { std::tie(e, ls) = parse_local_expr(p); expr r; if (whnf) { - auto tc = mk_type_checker(p.env(), p.mk_ngen()); + auto tc = mk_type_checker(p.env()); r = tc->whnf(e).first; } else { type_checker tc(p.env()); @@ -446,11 +446,11 @@ static environment telescope_eq_cmd(parser & p) { std::tie(e, ls) = parse_local_expr(p); buffer t; while (is_pi(e)) { - expr local = mk_local(p.mk_fresh_name(), binding_name(e), binding_domain(e), binder_info()); + expr local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binder_info()); t.push_back(local); e = instantiate(binding_body(e), local); } - auto tc = mk_type_checker(p.env(), p.mk_ngen()); + auto tc = mk_type_checker(p.env()); buffer eqs; mk_telescopic_eq(*tc, t, eqs); for (expr const & eq : eqs) { @@ -757,7 +757,7 @@ static environment simplify_cmd(parser & p) { if (!r.has_proof()) { p.regular_stream() << "(refl): " << r.get_new() << endl; } else { - auto tc = mk_type_checker(p.env(), p.mk_ngen()); + auto tc = mk_type_checker(p.env()); expr pf_type = tc->check(r.get_proof(), ls).first; diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index 4b549e4ad..3597feb9c 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -41,19 +41,19 @@ bool get_elaborator_calc_assistant(options const & o) { return o.get_bool(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT); } -static optional> mk_op(environment const & env, local_context & ctx, name_generator & ngen, type_checker_ptr & tc, +static optional> mk_op(environment const & env, local_context & ctx, type_checker_ptr & tc, name const & op, unsigned nunivs, unsigned nargs, std::initializer_list const & explicit_args, constraint_seq & cs, tag g) { levels lvls; for (unsigned i = 0; i < nunivs; i++) - lvls = levels(mk_meta_univ(ngen.next()), lvls); + lvls = levels(mk_meta_univ(mk_fresh_name()), lvls); expr c = mk_constant(op, lvls); expr op_type = instantiate_type_univ_params(env.get(op), lvls); buffer args; for (unsigned i = 0; i < nargs; i++) { if (!is_pi(op_type)) return optional>(); - expr arg = ctx.mk_meta(ngen, some_expr(binding_domain(op_type)), g); + expr arg = ctx.mk_meta(some_expr(binding_domain(op_type)), g); args.push_back(arg); op_type = instantiate(binding_body(op_type), arg); } @@ -71,20 +71,20 @@ static optional> mk_op(environment const & env, local_context & return some(mk_pair(r, op_type)); } -static optional> apply_symmetry(environment const & env, local_context & ctx, name_generator & ngen, type_checker_ptr & tc, +static optional> apply_symmetry(environment const & env, local_context & ctx, type_checker_ptr & tc, expr const & e, expr const & e_type, constraint_seq & cs, tag g) { buffer args; expr const & op = get_app_args(e_type, args); if (is_constant(op)) { if (auto info = get_symm_extra_info(env, const_name(op))) { - return mk_op(env, ctx, ngen, tc, info->m_name, + return mk_op(env, ctx, tc, info->m_name, info->m_num_univs, info->m_num_args-1, {e}, cs, g); } } return optional>(); } -static optional> apply_subst(environment const & env, local_context & ctx, name_generator & ngen, +static optional> apply_subst(environment const & env, local_context & ctx, type_checker_ptr & tc, expr const & e, expr const & e_type, expr const & pred, constraint_seq & cs, tag g) { buffer pred_args; @@ -97,9 +97,9 @@ static optional> apply_subst(environment const & env, local_con if (is_constant(op) && args.size() >= 2) { if (auto sinfo = get_subst_extra_info(env, const_name(op))) { if (auto rinfo = get_refl_extra_info(env, const_name(op))) { - if (auto refl_pair = mk_op(env, ctx, ngen, tc, rinfo->m_name, rinfo->m_num_univs, + if (auto refl_pair = mk_op(env, ctx, tc, rinfo->m_name, rinfo->m_num_univs, rinfo->m_num_args-1, { pred_args[npargs-2] }, cs, g)) { - return mk_op(env, ctx, ngen, tc, sinfo->m_name, sinfo->m_num_univs, + return mk_op(env, ctx, tc, sinfo->m_name, sinfo->m_num_univs, sinfo->m_num_args-2, {e, refl_pair->first}, cs, g); } } @@ -110,8 +110,8 @@ static optional> apply_subst(environment const & env, local_con // Return true if \c e is convertible to a term of the form (h ...). // If the result is true, update \c e and \c cs. -bool try_normalize_to_head(environment const & env, name_generator && ngen, name const & h, expr & e, constraint_seq & cs) { - type_checker_ptr tc = mk_type_checker(env, std::move(ngen), [=](name const & n) { return n == h; }); +bool try_normalize_to_head(environment const & env, name const & h, expr & e, constraint_seq & cs) { + type_checker_ptr tc = mk_type_checker(env, [=](name const & n) { return n == h; }); constraint_seq new_cs; expr new_e = tc->whnf(e, new_cs); expr const & fn = get_app_fn(new_e); @@ -136,13 +136,12 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, constraint_seq const & cs, unifier_config const & cfg, 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 && ngen) { + auto choice_fn = [=](expr const & meta, expr const & _meta_type, substitution const & _s) { local_context ctx = _ctx; expr e = _e; substitution s = _s; expr meta_type = _meta_type; - type_checker_ptr tc = mk_type_checker(env, ngen.mk_child()); + type_checker_ptr tc = mk_type_checker(env); constraint_seq new_cs = cs; expr e_type = tc->infer(e, new_cs); e_type = s.instantiate(e_type); @@ -160,7 +159,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, break; } } - expr imp_arg = ctx.mk_meta(ngen, some_expr(binding_domain(e_type)), g); + expr imp_arg = ctx.mk_meta(some_expr(binding_domain(e_type)), g); e = mk_app(e, imp_arg, g); e_type = instantiate(binding_body(e_type), imp_arg); } @@ -173,9 +172,9 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, expr const & e_type_fn = get_app_fn(e_type); if (is_constant(meta_type_fn) && (!is_constant(e_type_fn) || const_name(e_type_fn) != const_name(meta_type_fn))) { // try to make sure meta_type and e_type have the same head symbol - if (!try_normalize_to_head(env, ngen.mk_child(), const_name(meta_type_fn), e_type, new_cs) && + if (!try_normalize_to_head(env, const_name(meta_type_fn), e_type, new_cs) && is_constant(e_type_fn)) { - try_normalize_to_head(env, ngen.mk_child(), const_name(e_type_fn), meta_type, new_cs); + try_normalize_to_head(env, const_name(e_type_fn), meta_type, new_cs); } } @@ -192,7 +191,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.mk_child(), substitution(), new_cfg); + unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), substitution(), new_cfg); auto p = seq.pull(); lean_assert(p); substitution new_s = p->first.first; @@ -232,21 +231,21 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, // 2. eq.symm pr constraint_seq symm_cs = new_cs; - auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g); + auto symm = apply_symmetry(env, ctx, tc, e, e_type, symm_cs, g); if (symm) { try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } catch (exception &) {} } // 3. subst pr (eq.refl lhs) constraint_seq subst_cs = new_cs; - if (auto subst = apply_subst(env, ctx, ngen, tc, e, e_type, meta_type, subst_cs, g)) { + if (auto subst = apply_subst(env, ctx, tc, e, e_type, meta_type, subst_cs, g)) { try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {} } // 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, + if (auto subst = apply_subst(env, ctx, tc, symm->first, symm->second, meta_type, subst_cs, g)) { try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {} @@ -268,7 +267,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, // 2. eq.symm pr constraint_seq symm_cs = new_cs; - auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g); + auto symm = apply_symmetry(env, ctx, tc, e, e_type, symm_cs, g); if (symm) { try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } catch (exception &) {} diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp index 4577669f4..e6c19bf23 100644 --- a/src/frontends/lean/coercion_elaborator.cpp +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/metavar.h" #include "kernel/constraint.h" @@ -36,7 +37,7 @@ list get_coercions_from_to(type_checker & from_tc, type_checker & to_tc, return list(); // failed if (!from_tc.is_def_eq(binding_domain(whnf_from_type), binding_domain(whnf_to_type), justification(), new_cs)) return list(); // failed, the domains must be definitionally equal - expr x = mk_local(from_tc.mk_fresh_name(), "x", binding_domain(whnf_from_type), binder_info()); + expr x = mk_local(mk_fresh_name(), "x", binding_domain(whnf_from_type), binder_info()); expr A = instantiate(binding_body(whnf_from_type), x); expr B = instantiate(binding_body(whnf_to_type), x); list coe = get_coercions_from_to(from_tc, to_tc, A, B, new_cs, lift_coe); @@ -44,7 +45,7 @@ list get_coercions_from_to(type_checker & from_tc, type_checker & to_tc, cs += new_cs; // Remark: each coercion c in coe is a function from A to B // We create a new list: (fun (f : D -> A) (x : D), c (f x)) - expr f = mk_local(from_tc.mk_fresh_name(), "f", whnf_from_type, binder_info()); + expr f = mk_local(mk_fresh_name(), "f", whnf_from_type, binder_info()); expr fx = mk_app(f, x); return map(coe, [&](expr const & c) { return Fun(f, Fun(x, mk_app(c, fx))); }); } else { @@ -95,8 +96,7 @@ bool is_pi_meta(expr const & e) { constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coercion_info_manager & infom, expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor, bool lift_coe) { - auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s, - name_generator && /* ngen */) { + auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s) { expr new_a_type; justification new_a_type_jst; if (is_meta(a_type)) { @@ -128,7 +128,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc expr dom_to = binding_domain(it_to); if (!from_tc.is_def_eq(dom_from, dom_to, justification(), cs)) return lazy_list(); - expr local = mk_local(from_tc.mk_fresh_name(), binding_name(it_from), dom_from, binder_info()); + expr local = mk_local(mk_fresh_name(), binding_name(it_from), dom_from, binder_info()); locals.push_back(local); it_from = instantiate(binding_body(it_from), local); it_to = instantiate(binding_body(it_to), local); @@ -137,7 +137,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc get_coercions_from(from_tc.env(), it_from, alts); expr fn_a; if (!locals.empty()) - fn_a = mk_local(from_tc.mk_fresh_name(), "f", new_a_type, binder_info()); + fn_a = mk_local(mk_fresh_name(), "f", new_a_type, binder_info()); buffer choices; buffer coes; // first alternative: no coercion diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 4cf8f0456..349ee0310 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include "util/fresh_name.h" #include "util/sstream.h" #include "util/timeit.h" #include "kernel/type_checker.h" @@ -139,7 +140,7 @@ static environment declare_var(parser & p, environment env, if (p.get_local(n)) throw parser_error(sstream() << "invalid parameter/variable declaration, '" << n << "' has already been declared", pos); - name u = p.mk_fresh_name(); + name u = mk_fresh_name(); expr l = p.save_pos(mk_local(u, n, type, bi), pos); if (k == variable_kind::Parameter) p.add_parameter(n, l); @@ -661,7 +662,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { try { t = p.parse_expr(); p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected"); - expr fn = mk_local(p.mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info()); + expr fn = mk_local(mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info()); if (p.curr_is_token(get_end_tk())) { p.next(); // empty match-with diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a49c89ccd..2f3b9fdb2 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -108,16 +108,16 @@ static bool save_error(pos_info_provider const * pip, expr const & e) { return g_elaborator_reported_errors->save(pip, e); } -type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator && ngen) { +type_checker_ptr mk_coercion_from_type_checker(environment const & env) { auto irred_pred = mk_irreducible_pred(env); - return mk_type_checker(env, std::move(ngen), [=](name const & n) { + return mk_type_checker(env, [=](name const & n) { return has_coercions_from(env, n) || irred_pred(n); }); } -type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator && ngen) { +type_checker_ptr mk_coercion_to_type_checker(environment const & env) { auto irred_pred = mk_irreducible_pred(env); - return mk_type_checker(env, std::move(ngen), [=](name const & n) { + return mk_type_checker(env, [=](name const & n) { return has_coercions_to(env, n) || irred_pred(n); }); } @@ -176,9 +176,8 @@ struct elaborator::choice_expr_elaborator : public choice_iterator { } }; -elaborator::elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names): +elaborator::elaborator(elaborator_context & ctx, bool nice_mvar_names): m_ctx(ctx), - m_ngen(ngen), m_context(), m_full_context(), m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) { @@ -186,14 +185,14 @@ elaborator::elaborator(elaborator_context & ctx, name_generator && ngen, bool ni m_use_tactic_hints = true; m_no_info = false; m_in_equation_lhs = false; - m_tc = mk_type_checker(ctx.m_env, m_ngen.mk_child()); - m_coercion_from_tc = mk_coercion_from_type_checker(ctx.m_env, m_ngen.mk_child()); - m_coercion_to_tc = mk_coercion_to_type_checker(ctx.m_env, m_ngen.mk_child()); + m_tc = mk_type_checker(ctx.m_env); + m_coercion_from_tc = mk_coercion_from_type_checker(ctx.m_env); + m_coercion_to_tc = mk_coercion_to_type_checker(ctx.m_env); m_nice_mvar_names = nice_mvar_names; } expr elaborator::mk_local(name const & n, expr const & t, binder_info const & bi) { - return ::lean::mk_local(m_ngen.next(), n, t, bi); + return ::lean::mk_local(mk_fresh_name(), n, t, bi); } void elaborator::register_meta(expr const & meta) { @@ -312,7 +311,7 @@ void elaborator::instantiate_info(substitution s) { expr meta = s.instantiate(*m_to_show_hole); expr meta_type = s.instantiate(type_checker(env()).infer(meta).first); goal g(meta, meta_type); - proof_state ps(goals(g), s, m_ngen, constraints()); + proof_state ps(goals(g), s, constraints()); auto out = regular(env(), ios()); print_lean_info_header(out.get_stream()); out << ps.pp(env(), ios()) << endl; @@ -340,13 +339,13 @@ expr elaborator::mk_placeholder_meta(optional const & suffix, optional const & suffix, optional const & t, constraint_seq & cs) { lean_assert(is_choice(e)); // Possible optimization: try to lookahead and discard some of the alternatives. - expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); + expr m = m_full_context.mk_meta(t, e.get_tag()); register_meta(m); local_context ctx = m_context; local_context full_ctx = m_full_context; bool in_equation_lhs = m_in_equation_lhs; - auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */, - name_generator && /* ngen */) { + auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */) { return choose(std::make_shared(*this, ctx, full_ctx, in_equation_lhs, meta, type, e)); }; auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main, bool) { @@ -427,7 +425,7 @@ expr elaborator::visit_choice(expr const & e, optional const & t, constrai expr elaborator::visit_by(expr const & e, optional const & t, constraint_seq & cs) { lean_assert(is_by(e)); expr tac = visit(get_by_arg(e), cs); - expr m = m_context.mk_meta(m_ngen, t, e.get_tag()); + expr m = m_context.mk_meta(t, e.get_tag()); register_meta(m); m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac); return m; @@ -436,7 +434,7 @@ expr elaborator::visit_by(expr const & e, optional const & t, constraint_s expr elaborator::visit_by_plus(expr const & e, optional const & t, constraint_seq & cs) { lean_assert(is_by_plus(e)); expr tac = visit(get_by_plus_arg(e), cs); - expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); + expr m = m_full_context.mk_meta(t, e.get_tag()); register_meta(m); m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac); return m; @@ -448,7 +446,7 @@ expr elaborator::visit_calc_proof(expr const & e, optional const & t, cons if (infom()) im = &m_pre_info_data; pair ecs = visit(get_annotation_arg(e)); - expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); + expr m = m_full_context.mk_meta(t, e.get_tag()); register_meta(m); auto fn = [=](expr const & t) { save_type_data(get_annotation_arg(e), t); }; constraint c = mk_calc_proof_cnstr(env(), ios().get_options(), @@ -536,7 +534,7 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst, bool) { return pp_function_expected(fmt, substitution(subst).instantiate(f)); }); - auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator &&) { + auto choice_fn = [=](expr const & meta, expr const &, substitution const &) { flet save1(m_context, ctx); flet save2(m_full_context, full_ctx); list choices = map2(coes, [&](expr const & coe) { @@ -548,7 +546,7 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { }); return choose(std::make_shared(*this, f, choices, coes, false)); }; - f = m_full_context.mk_meta(m_ngen, none_expr(), f.get_tag()); + f = m_full_context.mk_meta(none_expr(), f.get_tag()); register_meta(f); cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j); lean_assert(is_meta(f)); @@ -653,7 +651,7 @@ pair elaborator::apply_coercion(expr const & a, expr a_typ pair elaborator::mk_delayed_coercion( expr const & a, expr const & a_type, expr const & expected_type, justification const & j) { - expr m = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag()); + expr m = m_full_context.mk_meta(some_expr(expected_type), a.get_tag()); register_meta(m); constraint c = mk_coercion_cnstr(*m_coercion_from_tc, *m_coercion_to_tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), m_ctx.m_lift_coercions); @@ -808,7 +806,7 @@ expr elaborator::visit_placeholder(expr const & e, constraint_seq & cs) { level elaborator::replace_univ_placeholder(level const & l) { auto fn = [&](level const & l) { if (is_placeholder(l)) - return some_level(mk_meta_univ(m_ngen.next())); + return some_level(mk_meta_univ(mk_fresh_name())); else return none_level(); }; @@ -857,7 +855,7 @@ expr elaborator::visit_constant(expr const & e) { << " expected, #" << ls.size() << " provided"); // "fill" with meta universe parameters for (unsigned i = ls.size(); i < num_univ_params; i++) - ls.push_back(mk_meta_univ(m_ngen.next())); + ls.push_back(mk_meta_univ(mk_fresh_name())); lean_assert(num_univ_params == ls.size()); return update_constant(e, to_list(ls.begin(), ls.end())); } @@ -999,9 +997,9 @@ bool elaborator::is_sorry(expr const & e) const { } expr elaborator::visit_sorry(expr const & e) { - level u = mk_meta_univ(m_ngen.next()); + level u = mk_meta_univ(mk_fresh_name()); expr t = mk_sort(u); - expr m = m_full_context.mk_meta(m_ngen, some_expr(t), e.get_tag()); + expr m = m_full_context.mk_meta(some_expr(t), e.get_tag()); return mk_app(update_constant(e, to_list(u)), m, e.get_tag()); } @@ -1174,8 +1172,7 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) { new_eqs.push_back(eq); } else { buffer locals; - name_generator ngen = tc.mk_ngen(); - eq = fun_to_telescope(ngen, eq, locals, optional()); + eq = fun_to_telescope(eq, locals, optional()); if (is_equation(eq)) { name x("x"); lean_assert(num_fns <= locals.size()); @@ -1189,7 +1186,7 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) { } else if (r.first == Accessible) { expr const & meta = r.second; expr meta_type = tc.infer(meta).first; - expr new_local = mk_local(tc.mk_fresh_name(), x.append_after(idx), meta_type, binder_info()); + expr new_local = mk_local(mk_fresh_name(), x.append_after(idx), meta_type, binder_info()); for (expr & local : locals) local = update_mlocal(local, replace_meta(mlocal_type(local), meta, new_local)); eq = replace_meta(eq, meta, new_local); @@ -1234,8 +1231,7 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) { environment const & _env = env(); 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 && ngen) { + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s) { substitution new_s = s; expr new_eqns = new_s.instantiate_all(eqns); bool reject_type_is_meta = false; @@ -1243,7 +1239,7 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) { if (display_unassigned_mvars(new_eqns, new_s)) { return lazy_list(); } - type_checker_ptr tc = mk_type_checker(_env, std::move(ngen)); + type_checker_ptr tc = mk_type_checker(_env); 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)); @@ -1285,7 +1281,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { expr new_eq; constraint_seq new_cs; buffer fns_locals; - fun_to_telescope(m_ngen, eq, fns_locals, optional()); + fun_to_telescope(eq, fns_locals, optional()); list locals = to_list(fns_locals.begin() + num_fns, fns_locals.end()); if (first_eq) { // Replace first num_fns domains of eq with the ones in first_eq. @@ -1330,7 +1326,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { lean_assert(first_eq && is_lambda(*first_eq)); expr type = binding_domain(*first_eq); - expr m = m_full_context.mk_meta(m_ngen, some_expr(type), eqns.get_tag()); + expr m = m_full_context.mk_meta(some_expr(type), eqns.get_tag()); register_meta(m); constraint c = mk_equations_cnstr(m, new_eqns); /* We use stack policy for processing MaxDelayed constraints */ @@ -1432,7 +1428,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) { expr new_S_type = whnf(infer_type(new_S, cs), cs); tag S_tag = S.get_tag(); while (is_pi(new_S_type)) { - expr m = m_full_context.mk_meta(m_ngen, some_expr(binding_domain(new_S_type)), S_tag); + expr m = m_full_context.mk_meta(some_expr(binding_domain(new_S_type)), S_tag); register_meta(m); new_S_args.push_back(m); new_S = mk_app(new_S, m, S_tag); @@ -1502,7 +1498,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) { throw_elaborator_exception(sstream() << "invalid structure instance, field '" << n << "' is missing", e); } - v = m_full_context.mk_meta(m_ngen, some_expr(d_type), result_tag); + v = m_full_context.mk_meta(some_expr(d_type), result_tag); register_meta(v); } } @@ -1582,7 +1578,7 @@ expr elaborator::process_obtain_expr(list const & s_list, list const & s_list, listensure_type(A, cs)); levels ls(A_lvl); bool is_strict = true; @@ -1702,15 +1698,14 @@ expr elaborator::visit_checkpoint_expr(expr const & e, constraint_seq & cs) { expr arg = get_annotation_arg(e); expr m; if (is_by(arg)) - m = m_context.mk_meta(m_ngen, none_expr(), e.get_tag()); + m = m_context.mk_meta(none_expr(), e.get_tag()); else - m = m_full_context.mk_meta(m_ngen, none_expr(), e.get_tag()); + m = m_full_context.mk_meta(none_expr(), e.get_tag()); register_meta(m); local_context ctx = m_context; local_context full_ctx = m_full_context; bool in_equation_lhs = m_in_equation_lhs; - auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */, - name_generator && /* ngen */) { + auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */) { flet set1(m_context, ctx); flet set2(m_full_context, full_ctx); flet set3(m_in_equation_lhs, in_equation_lhs); @@ -1884,7 +1879,7 @@ expr elaborator::visit(expr const & e, constraint_seq & cs) { unify_result_seq elaborator::solve(constraint_seq const & cs) { buffer tmp; cs.linearize(tmp); - return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), substitution(), m_unifier_config); + return unify(env(), tmp.size(), tmp.data(), substitution(), m_unifier_config); } void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg, expr const & pos) { @@ -1915,18 +1910,18 @@ 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, options const & o, name_generator && ngen, expr const & e, optional const & expected_type, + auto fn = [=](goal const & g, options const & o, expr const & e, optional const & expected_type, substitution const & subst, bool report_unassigned) { // 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; if (o == m_ctx.m_options) { - elaborator aux_elaborator(m_ctx, std::move(ngen)); + elaborator aux_elaborator(m_ctx); return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, use_tactic_hints, subst, report_unassigned); } else { elaborator_context aux_ctx(m_ctx, o); - elaborator aux_elaborator(aux_ctx, std::move(ngen)); + elaborator aux_elaborator(aux_ctx); return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, use_tactic_hints, subst, report_unassigned); } @@ -2074,11 +2069,10 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac); goal g = head(gs); expr mvar = g.get_mvar(); - name_generator ngen = ps.get_ngen(); - proof_state focus_ps(ps, goals(g), ngen.mk_child()); + proof_state focus_ps(ps, goals(g)); if (!try_using_begin_end(subst, mvar, focus_ps, ptac)) return false; - ps = proof_state(ps, tail(gs), subst, ngen); + ps = proof_state(ps, tail(gs), subst); } else { show_goal(ps, start_expr, end_expr, ptac); expr new_ptac = subst.instantiate_all(ptac); @@ -2155,7 +2149,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set throw_elaborator_exception("failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) " "(solution: provide type explicitly)", mvar); } - proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child()); + proof_state ps = to_proof_state(*meta, type, subst); if (auto pre_tac = get_pre_tactic_for(mvar)) { if (is_begin_end_annotation(*pre_tac)) { try_using_begin_end(subst, mvar, ps, *pre_tac); @@ -2262,7 +2256,7 @@ bool elaborator::display_unassigned_mvars(expr const & e, substitution const & s expr meta = tmp_s.instantiate(*it); expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first); goal g(meta, meta_type); - proof_state ps(goals(g), s, m_ngen, constraints()); + proof_state ps(goals(g), s, constraints()); display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder"); r = true; } @@ -2467,7 +2461,7 @@ elaborate_result elaborator::elaborate_nested(list const & ctx, optional tmp; cs.linearize(tmp); - auto p = unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), subst, m_unifier_config).pull(); + auto p = unify(env(), tmp.size(), tmp.data(), subst, m_unifier_config).pull(); lean_assert(p); substitution new_subst = p->first.first; constraints rcs = p->first.second; @@ -2489,12 +2483,12 @@ static name * g_tmp_prefix = nullptr; std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, bool ensure_type, bool nice_mvar_names) { - return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type); + return elaborator(env, nice_mvar_names)(ctx, e, ensure_type); } std::tuple elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v) { - return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n); + return elaborator(env)(t, v, n); } void initialize_elaborator() { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index c0e69f939..df36e6d58 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -31,7 +31,6 @@ class elaborator : public coercion_info_manager { typedef rb_map, expr_quick_cmp> cache; typedef std::vector> to_check_sorts; elaborator_context & m_ctx; - name_generator m_ngen; type_checker_ptr m_tc; type_checker_ptr m_coercion_from_tc; type_checker_ptr m_coercion_to_tc; @@ -196,7 +195,7 @@ class elaborator : public coercion_info_manager { void show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr); public: - elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names = false); + 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); }; diff --git a/src/frontends/lean/find_cmd.cpp b/src/frontends/lean/find_cmd.cpp index a98f8e2d2..9757dd94f 100644 --- a/src/frontends/lean/find_cmd.cpp +++ b/src/frontends/lean/find_cmd.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/fresh_name.h" #include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "library/unifier.h" @@ -52,11 +53,10 @@ bool get_find_expensive(options const & opts) { bool match_pattern(type_checker & tc, expr const & pattern, declaration const & d, unsigned max_steps, bool cheap) { - name_generator ngen = tc.mk_ngen(); - buffer ls; + buffer ls; unsigned num_ls = d.get_num_univ_params(); for (unsigned i = 0; i < num_ls; i++) - ls.push_back(mk_meta_univ(ngen.next())); + ls.push_back(mk_meta_univ(mk_fresh_name())); expr dt = instantiate_type_univ_params(d, to_list(ls.begin(), ls.end())); unsigned num_e = get_expect_num_args(tc, pattern); @@ -65,7 +65,7 @@ bool match_pattern(type_checker & tc, expr const & pattern, declaration const & return false; for (unsigned i = 0; i < num_d - num_e; i++) { dt = tc.whnf(dt).first; - expr local = mk_local(ngen.next(), binding_domain(dt)); + expr local = mk_local(mk_fresh_name(), binding_domain(dt)); dt = instantiate(binding_body(dt), local); } try { @@ -73,7 +73,7 @@ bool match_pattern(type_checker & tc, expr const & pattern, declaration const & cfg.m_max_steps = max_steps; cfg.m_kind = cheap ? unifier_kind::Cheap : unifier_kind::Liberal; cfg.m_ignore_context_check = true; - auto r = unify(tc.env(), pattern, dt, tc.mk_ngen(), substitution(), cfg); + auto r = unify(tc.env(), pattern, dt, substitution(), cfg); return static_cast(r.pull()); } catch (exception&) { return false; @@ -107,7 +107,7 @@ environment find_cmd(parser & p) { buffer pos_names, neg_names; parse_filters(p, pos_names, neg_names); environment env = p.env(); - auto tc = mk_opaque_type_checker(env, p.mk_ngen()); + auto tc = mk_opaque_type_checker(env); flycheck_information info(p.regular_stream()); if (info.enabled()) { p.display_information_pos(p.cmd_pos()); diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 3d435f10b..2c1d1b22e 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "util/name_map.h" +#include "util/fresh_name.h" #include "util/sexpr/option_declarations.h" #include "kernel/replace_fn.h" #include "kernel/type_checker.h" @@ -175,7 +176,7 @@ struct inductive_cmd_fn { m_u = mk_global_univ(u_name); m_infer_result_universe = false; m_namespace = get_namespace(m_env); - m_tc = mk_type_checker(m_env, m_p.mk_ngen()); + m_tc = mk_type_checker(m_env); } [[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); } @@ -276,7 +277,7 @@ struct inductive_cmd_fn { /** \brief Create a local constant based on the given binding */ expr mk_local_for(expr const & b) { - return mk_local(m_p.mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b), b.get_tag()); + return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b), b.get_tag()); } /** \brief Set explicit datatype parameters as local constants in m_params */ @@ -492,7 +493,7 @@ struct inductive_cmd_fn { throw_error("invalid universe polymorphic inductive declaration, the resultant universe is not Prop (i.e., 0), but it may " "be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')"); } - expr local = mk_local(m_p.mk_fresh_name(), n, type, binder_info(), type.get_tag()); + expr local = mk_local(mk_fresh_name(), n, type, binder_info(), type.get_tag()); r.push_back(local); map.insert(n, local); } @@ -538,7 +539,7 @@ struct inductive_cmd_fn { for (inductive_decl const & decl : decls) { for (intro_rule const & rule : inductive_decl_intros(decl)) { expr type = fix_intro_rule_type(intro_rule_type(rule), ind_to_local); - expr local = mk_local(m_p.mk_fresh_name(), intro_rule_name(rule), type, binder_info()); + expr local = mk_local(mk_fresh_name(), intro_rule_name(rule), type, binder_info()); r.push_back(local); } } diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp index 7b88c462e..9a6f0b204 100644 --- a/src/frontends/lean/info_tactic.cpp +++ b/src/frontends/lean/info_tactic.cpp @@ -36,7 +36,7 @@ tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) { // create dummy variable just to communicate position to the elaborator expr dummy = mk_sort(mk_level_zero(), e.get_tag()); scoped_info_tactic_proof_state scope(ps); - fn(goal(), ios.get_options(), name_generator("dummy"), dummy, none_expr(), substitution(), false); + fn(goal(), ios.get_options(), dummy, none_expr(), substitution(), false); return ps; }); } diff --git a/src/frontends/lean/nested_declaration.cpp b/src/frontends/lean/nested_declaration.cpp index 6c38931df..cacfa0bf9 100644 --- a/src/frontends/lean/nested_declaration.cpp +++ b/src/frontends/lean/nested_declaration.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/find_fn.h" #include "kernel/instantiate.h" @@ -183,7 +184,7 @@ public: expr visit_binding(expr const & b) { expr new_domain = visit(binding_domain(b)); - expr l = mk_local(m_tc.mk_fresh_name(), new_domain); + expr l = mk_local(mk_fresh_name(), new_domain); expr new_body = abstract(visit(instantiate(binding_body(b), l)), l); return update_binding(b, new_domain, new_body); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9dbd13879..9667039a8 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -129,7 +129,7 @@ parser::parser(environment const & env, io_state const & ios, bool use_exceptions, unsigned num_threads, snapshot const * s, snapshot_vector * sv, info_manager * im, keep_theorem_mode tmode): - m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix), + m_env(env), m_ios(ios), m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name, s ? s->m_line : 1), m_base_dir(base_dir), @@ -145,7 +145,6 @@ parser::parser(environment const & env, io_state const & ios, m_has_params = false; m_keep_theorem_mode = tmode; if (s) { - m_ngen = s->m_ngen; m_local_level_decls = s->m_lds; m_local_decls = s->m_eds; m_level_variables = s->m_lvars; @@ -2281,7 +2280,7 @@ void parser::save_snapshot() { if (!m_snapshot_vector) return; if (m_snapshot_vector->empty() || static_cast(m_snapshot_vector->back().m_line) != m_scanner.get_line()) - m_snapshot_vector->push_back(snapshot(m_env, m_ngen, m_local_level_decls, m_local_decls, + m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_level_variables, m_variables, m_include_vars, m_ios.get_options(), m_parser_scope_stack, m_scanner.get_line())); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 191e42514..eb2e25e42 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "util/flet.h" #include "util/name_map.h" #include "util/exception.h" -#include "util/name_generator.h" #include "kernel/environment.h" #include "kernel/expr_maps.h" #include "library/io_state.h" @@ -63,7 +62,6 @@ typedef list parser_scope_stack; /** \brief Snapshot of the state of the Lean parser */ struct snapshot { environment m_env; - name_generator m_ngen; local_level_decls m_lds; local_expr_decls m_eds; name_set m_lvars; // subset of m_lds that is tagged as level variable @@ -74,10 +72,10 @@ struct snapshot { unsigned m_line; snapshot():m_line(0) {} snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {} - snapshot(environment const & env, name_generator const & ngen, local_level_decls const & lds, + snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, name_set const & lvars, name_set const & vars, name_set const & includes, options const & opts, parser_scope_stack const & pss, unsigned line): - m_env(env), m_ngen(ngen), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes), + m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes), m_options(opts), m_parser_scope_stack(pss), m_line(line) {} }; @@ -90,7 +88,6 @@ enum class undef_id_behavior { Error, AssumeConstant, AssumeLocal }; class parser { environment m_env; io_state m_ios; - name_generator m_ngen; bool m_verbose; bool m_use_exceptions; bool m_show_errors; @@ -307,9 +304,6 @@ public: options get_options() const { return m_ios.get_options(); } template void set_option(name const & n, T const & v) { m_ios.set_option(n, v); } - name mk_fresh_name() { return m_ngen.next(); } - name_generator mk_ngen() { return m_ngen.mk_child(); } - /** \brief Return the current position information */ pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); } expr save_pos(expr e, pos_info p); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 3237e2908..e40caf4ce 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include #include #include "util/flet.h" +#include "util/fresh_name.h" #include "kernel/replace_fn.h" #include "kernel/free_vars.h" #include "kernel/abstract.h" @@ -623,14 +624,13 @@ bool pretty_fn::has_implicit_args(expr const & f) { // there are no implicit arguments. return false; } - name_generator ngen(*g_tmp_prefix); try { expr type = m_tc.whnf(m_tc.infer(f).first).first; while (is_pi(type)) { binder_info bi = binding_info(type); if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit()) return true; - expr local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type)); + expr local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type)); type = m_tc.whnf(instantiate(binding_body(type), local)).first; } return false; diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index a8d2f03d7..552f53705 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -745,12 +745,11 @@ void consume_pos_neg_strs(std::string const & filters, buffer & pos } bool match_type(type_checker & tc, expr const & meta, expr const & expected_type, declaration const & d) { - name_generator ngen = tc.mk_ngen(); goal g(meta, expected_type); buffer ls; unsigned num_ls = d.get_num_univ_params(); for (unsigned i = 0; i < num_ls; i++) - ls.push_back(mk_meta_univ(ngen.next())); + ls.push_back(mk_meta_univ(mk_fresh_name())); expr dt = instantiate_type_univ_params(d, to_list(ls.begin(), ls.end())); unsigned num_e = get_expect_num_args(tc, expected_type); unsigned num_d = get_expect_num_args(tc, dt); @@ -758,7 +757,7 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type return false; for (unsigned i = 0; i < num_d - num_e; i++) { dt = tc.whnf(dt).first; - expr meta = g.mk_meta(ngen.next(), binding_domain(dt)); + expr meta = g.mk_meta(mk_fresh_name(), binding_domain(dt)); dt = instantiate(binding_body(dt), meta); } // Remark: we ignore declarations where the resultant type is of the form @@ -771,15 +770,15 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type unifier_config cfg; cfg.m_max_steps = LEAN_FINDG_MAX_STEPS; cfg.m_kind = unifier_kind::Cheap; - auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), substitution(), cfg); + auto r = unify(tc.env(), dt, expected_type, substitution(), cfg); return static_cast(r.pull()); } catch (exception&) { return false; } } -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 std::unique_ptr mk_find_goal_type_checker(environment const & env) { + return mk_opaque_type_checker(env); } static name * g_tmp_prefix = nullptr; @@ -798,7 +797,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; - std::unique_ptr tc = mk_find_goal_type_checker(env, name_generator(*g_tmp_prefix)); + std::unique_ptr tc = mk_find_goal_type_checker(env); 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/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index df9e91f98..37c0f803e 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include #include #include "util/sstream.h" +#include "util/fresh_name.h" #include "util/sexpr/option_declarations.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" @@ -87,7 +88,6 @@ struct structure_cmd_fn { parser & m_p; environment m_env; - name_generator m_ngen; type_checker_ptr m_tc; name m_namespace; name m_name; @@ -113,8 +113,8 @@ struct structure_cmd_fn { bool m_gen_eta; bool m_gen_proj_mk; - structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) { - m_tc = mk_type_checker(m_env, m_p.mk_ngen()); + structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_namespace(get_namespace(m_env)) { + m_tc = mk_type_checker(m_env); m_infer_result_universe = false; m_gen_eta = get_structure_eta_thm(p.get_options()); m_gen_proj_mk = get_structure_proj_mk_thm(p.get_options()); @@ -298,7 +298,7 @@ struct structure_cmd_fn { buffer tmp_locals; tmp_locals.append(m_params); for (expr const & parent : m_parents) - tmp_locals.push_back(mk_local(m_ngen.next(), parent)); + tmp_locals.push_back(mk_local(mk_fresh_name(), parent)); collected_locals dep_set; for (expr const & v : include_vars) { @@ -440,7 +440,7 @@ struct structure_cmd_fn { bool use_exceptions = true; bool discard = true; unifier_config cfg(use_exceptions, discard); - unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), substitution(), cfg); + unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), substitution(), cfg); auto p = rseq.pull(); lean_assert(p); substitution subst = p->first.first; @@ -810,7 +810,7 @@ struct structure_cmd_fn { binder_info bi; if (m_modifiers.is_class()) bi = mk_inst_implicit_binder_info(); - expr st = mk_local(m_ngen.next(), "s", st_type, bi); + expr st = mk_local(mk_fresh_name(), "s", st_type, bi); expr coercion_type = infer_implicit(Pi(m_params, Pi(st, parent)), m_params.size(), true);; expr coercion_value = parent_intro; for (unsigned idx : fmap) { @@ -846,7 +846,7 @@ struct structure_cmd_fn { level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end()); levels st_ls = param_names_to_levels(lnames); expr st_type = mk_app(mk_constant(m_name, st_ls), m_params); - expr st = mk_local(m_ngen.next(), "s", st_type, binder_info()); + expr st = mk_local(mk_fresh_name(), "s", st_type, binder_info()); expr lhs = mk_app(mk_constant(m_mk, st_ls), m_params); for (expr const & field : m_fields) { expr proj = mk_app(mk_app(mk_constant(m_name + mlocal_name(field), st_ls), m_params), st); diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 5bb77fa6d..cc53df8de 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include "util/lazy_list.h" #include "util/list.h" -#include "util/name_generator.h" #include "util/sequence.h" #include "kernel/level.h" @@ -57,7 +56,7 @@ typedef list constraints; One application of choice constraints is overloaded notation. */ -typedef std::function(expr const &, expr const &, substitution const &, name_generator &&)> choice_fn; +typedef std::function(expr const &, expr const &, substitution const &)> choice_fn; struct constraint_cell; class constraint { diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 99dcc24fe..642d1ef45 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -20,8 +20,6 @@ pair converter::is_def_eq(expr const & t, expr const & s, return is_def_eq(t, s, c, *g_no_delayed_jst); } -name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); } - pair converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); } extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); } diff --git a/src/kernel/converter.h b/src/kernel/converter.h index d05520b28..9497d90b7 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -13,7 +13,6 @@ class type_checker; class converter { protected: - name mk_fresh_name(type_checker & tc); pair infer_type(type_checker & tc, expr const & e); extension_context & get_extension(type_checker & tc); public: diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index a24a8aefa..7a78400d6 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/interrupt.h" #include "util/flet.h" +#include "util/fresh_name.h" #include "kernel/default_converter.h" #include "kernel/instantiate.h" #include "kernel/free_vars.h" @@ -248,7 +249,7 @@ bool default_converter::is_def_eq_binding(expr t, expr s, constraint_seq & cs) { // local is used inside t or s if (!var_s_type) var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data()); - subst.push_back(mk_local(mk_fresh_name(*m_tc), binding_name(s), *var_s_type, binding_info(s))); + subst.push_back(mk_local(mk_fresh_name(), binding_name(s), *var_s_type, binding_info(s))); } else { subst.push_back(*g_dont_care); // don't care } @@ -332,8 +333,7 @@ bool default_converter::try_eta_expansion_core(expr const & t, expr const & s, c if (is_pi(s_type)) { // do nothing ... s_type is already a Pi } else if (auto m = m_tc->is_stuck(s_type)) { - name_generator ngen = m_tc->mk_ngen(); - expr r = mk_pi_for(ngen, *m); + expr r = mk_pi_for(*m); justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) { return pp_function_expected(fmt, substitution(subst).instantiate(s)); }); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index af9962910..a1c0041c4 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -230,7 +230,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 && g, + friend certified_declaration check(environment const & env, declaration const & d, name_predicate const & opaque_hints); environment_id m_id; declaration m_declaration; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index a92e9b698..a7ecbf513 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -20,7 +20,6 @@ Author: Leonardo de Moura #include "util/optional.h" #include "util/serializer.h" #include "util/sexpr/format.h" -#include "util/name_generator.h" #include "kernel/level.h" #include "kernel/formatter.h" #include "kernel/extension_context.h" diff --git a/src/kernel/extension_context.h b/src/kernel/extension_context.h index 05a118ded..1cf52e094 100644 --- a/src/kernel/extension_context.h +++ b/src/kernel/extension_context.h @@ -18,8 +18,7 @@ class delayed_justification; 1) the environment being used. 2) the weak head normal form of an expression. 3) the type of an expression. - 4) a new fresh name. - 5) registration of a new constraint. + 4) registration of a new constraint. */ class extension_context { public: @@ -29,7 +28,6 @@ public: virtual pair is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) = 0; virtual pair check_type(expr const & e, bool infer_only) = 0; virtual optional is_stuck(expr const & e) = 0; - virtual name mk_fresh_name() = 0; expr check_type(expr const & e, constraint_seq & cs, bool infer_only); expr whnf(expr const & e, constraint_seq & cs); pair infer(expr const & e); diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index a19147666..7f2c6c0d0 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "util/name_generator.h" #include "util/sstream.h" #include "util/list_fn.h" #include "util/rb_map.h" +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/kernel_exception.h" #include "kernel/instantiate.h" @@ -266,7 +266,6 @@ struct add_inductive_fn { bool m_is_not_zero; unsigned m_decls_sz; // length(m_decls) list m_levels; // m_level_names ==> m_levels - name_generator m_ngen; type_checker_ptr m_tc; level m_elim_level; // extra universe level for eliminator. @@ -292,7 +291,7 @@ struct add_inductive_fn { unsigned num_params, list const & decls): m_env(env), m_level_names(level_params), m_num_params(num_params), m_decls(decls), - m_ngen(*g_tmp_prefix), m_tc(new type_checker(m_env)) { + m_tc(new type_checker(m_env)) { m_is_not_zero = false; m_decls_sz = length(m_decls); m_levels = param_names_to_levels(level_params); @@ -311,9 +310,6 @@ struct add_inductive_fn { expr whnf(expr const & e) { return tc().whnf(e).first; } expr ensure_type(expr const & e) { return tc().ensure_type(e).first; } - /** \brief Return a fresh name. */ - name mk_fresh_name() { return m_ngen.next(); } - /** \brief Create a local constant for the given binding. */ expr mk_local_for(expr const & b) { return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b)); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 8ce63591b..a61cdb866 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/flet.h" #include "util/sstream.h" #include "util/scoped_map.h" +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/default_converter.h" #include "kernel/expr_maps.h" @@ -40,34 +41,34 @@ unsigned get_arity(expr type) { return r; } -expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t) { - expr new_type = replace_range(t, mk_sort(mk_meta_univ(ngen.next()))); - name n = ngen.next(); +expr mk_aux_type_metavar_for(expr const & t) { + expr new_type = replace_range(t, mk_sort(mk_meta_univ(mk_fresh_name()))); + name n = mk_fresh_name(); return mk_metavar(n, new_type); } -expr mk_aux_metavar_for(name_generator & ngen, expr const & t) { +expr mk_aux_metavar_for(expr const & t) { unsigned num = get_arity(t); - expr r = mk_app_vars(mk_aux_type_metavar_for(ngen, t), num); + expr r = mk_app_vars(mk_aux_type_metavar_for(t), num); expr new_type = replace_range(t, r); - name n = ngen.next(); + name n = mk_fresh_name(); return mk_metavar(n, new_type); } -expr mk_pi_for(name_generator & ngen, expr const & meta) { +expr mk_pi_for(expr const & meta) { lean_assert(is_meta(meta)); buffer margs; expr const & m = get_app_args(meta, margs); expr const & mtype = mlocal_type(m); - expr maux1 = mk_aux_type_metavar_for(ngen, mtype); + expr maux1 = mk_aux_type_metavar_for(mtype); expr dontcare; - expr tmp_pi = mk_pi(ngen.next(), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context + expr tmp_pi = mk_pi(mk_fresh_name(), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context - expr maux2 = mk_aux_type_metavar_for(ngen, mtype2); + expr maux2 = mk_aux_type_metavar_for(mtype2); expr A = mk_app(maux1, margs); margs.push_back(Var(0)); expr B = mk_app(maux2, margs); - return mk_pi(ngen.next(), A, B); + return mk_pi(mk_fresh_name(), A, B); } optional type_checker::expand_macro(expr const & m) { @@ -80,7 +81,7 @@ optional type_checker::expand_macro(expr const & m) { It also returns the fresh local constant. */ pair type_checker::open_binding_body(expr const & e) { - expr local = mk_local(m_gen.next(), binding_name(e), binding_domain(e), binding_info(e)); + expr local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); return mk_pair(instantiate(binding_body(e), local), local); } @@ -104,7 +105,7 @@ pair type_checker::ensure_sort_core(expr e, expr const & s if (is_sort(ecs.first)) { return ecs; } else if (is_meta(ecs.first)) { - expr r = mk_sort(mk_meta_univ(m_gen.next())); + expr r = mk_sort(mk_meta_univ(mk_fresh_name())); justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) { return pp_type_expected(fmt, substitution(subst).instantiate(s)); @@ -123,7 +124,7 @@ pair type_checker::ensure_pi_core(expr e, expr const & s) if (is_pi(ecs.first)) { return ecs; } else if (auto m = is_stuck(ecs.first)) { - expr r = mk_pi_for(m_gen, *m); + expr r = mk_pi_for(*m); justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) { return pp_function_expected(fmt, substitution(subst).instantiate(s)); }); @@ -207,7 +208,7 @@ pair type_checker::infer_lambda(expr const & _e, bool infe es.push_back(e); ds.push_back(binding_domain(e)); expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); - expr l = mk_local(m_gen.next(), binding_name(e), d, binding_info(e)); + expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e)); ls.push_back(l); if (!infer_only) { pair dtcs = infer_type_core(d, infer_only); @@ -239,7 +240,7 @@ pair type_checker::infer_pi(expr const & _e, bool infer_on cs = cs + scs.second + dtcs.second; expr t1 = scs.first; us.push_back(sort_level(t1)); - expr l = mk_local(m_gen.next(), binding_name(e), d, binding_info(e)); + expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e)); ls.push_back(l); e = binding_body(e); } @@ -420,18 +421,13 @@ bool type_checker::is_opaque(expr const & c) const { return true; } -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), +type_checker::type_checker(environment const & env, std::unique_ptr && conv, bool memoize): + m_env(env), m_conv(std::move(conv)), m_tc_ctx(*this), m_memoize(memoize), m_params(nullptr) { } -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; - -type_checker::type_checker(environment const & env): - type_checker(env, name_generator(*g_tmp_prefix), std::unique_ptr(new default_converter(env)), true) {} +type_checker::type_checker(environment const & env, bool memoize): + type_checker(env, std::unique_ptr(new default_converter(env, memoize)), memoize) {} type_checker::~type_checker() {} @@ -472,13 +468,13 @@ static void check_duplicated_params(environment const & env, declaration const & } } -certified_declaration check(environment const & env, declaration const & d, name_generator && g, name_predicate const & pred) { +certified_declaration check(environment const & env, declaration const & d, name_predicate const & pred) { 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); - type_checker checker(env, g.mk_child(), std::unique_ptr(new hint_converter(env, pred))); + type_checker checker(env, std::unique_ptr(new hint_converter(env, pred))); expr sort = checker.check(d.get_type(), d.get_univ_params()).first; checker.ensure_sort(sort, d.get_type()); if (d.is_definition()) { @@ -492,23 +488,13 @@ certified_declaration check(environment const & env, declaration const & d, name return certified_declaration(env.get_id(), d); } -certified_declaration check(environment const & env, declaration const & d, name_generator && g) { - return check(env, d, std::move(g), [](name const &) { return false; }); -} - -certified_declaration check(environment const & env, declaration const & d, name_predicate const & pred) { - return check(env, d, name_generator(*g_tmp_prefix), pred); -} - certified_declaration check(environment const & env, declaration const & d) { - return check(env, d, name_generator(*g_tmp_prefix)); + return check(env, d, [](name const &) { return false; }); } void initialize_type_checker() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); } void finalize_type_checker() { - delete g_tmp_prefix; } } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 73a9c934c..5870c8cf4 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -9,8 +9,8 @@ Author: Leonardo de Moura #include #include #include "util/flet.h" -#include "util/name_generator.h" #include "util/name_set.h" +#include "util/fresh_name.h" #include "kernel/environment.h" #include "kernel/constraint.h" #include "kernel/justification.h" @@ -38,7 +38,7 @@ expr replace_range(expr const & type, expr const & new_range); Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u} where \c u is a new universe metavariable. */ -expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t); +expr mk_aux_type_metavar_for(expr const & t); /** \brief Given a type \c t of the form @@ -49,7 +49,7 @@ expr mk_aux_type_metavar_for(name_generator & ngen, expr const & t); Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u} where \c u is a new universe metavariable. */ -expr mk_aux_metavar_for(name_generator & ngen, expr const & t); +expr mk_aux_metavar_for(expr const & t); /** \brief Given a meta (?m t_1 ... t_n) where ?m has type @@ -58,7 +58,7 @@ expr mk_aux_metavar_for(name_generator & ngen, expr const & t); Pi (x : ?m1 t_1 ... t_n), (?m2 t_1 ... t_n x) where ?m1 and ?m2 are fresh metavariables */ -expr mk_pi_for(name_generator & ngen, expr const & meta); +expr mk_pi_for(expr const & meta); /** \brief Lean Type Checker. It can also be used to infer types, check whether a @@ -82,12 +82,10 @@ class type_checker { virtual pair check_type(expr const & e, bool infer_only) { return m_tc.infer_type_core(e, infer_only); } - virtual name mk_fresh_name() { return m_tc.m_gen.next(); } virtual optional is_stuck(expr const & e) { return m_tc.is_stuck(e); } }; environment m_env; - name_generator m_gen; std::unique_ptr m_conv; // In the type checker cache, we must take into account binder information. // Examples: @@ -123,14 +121,11 @@ public: memoize: if true, then inferred types are memoized/cached */ - 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(environment const & env, std::unique_ptr && conv, bool memoize = true); + type_checker(environment const & env, bool memoize = true); ~type_checker(); environment const & env() const { return m_env; } - name_generator mk_ngen() { return m_gen.mk_child(); } - name mk_fresh_name() { return m_gen.next(); } /** \brief Return the type of \c t. @@ -241,9 +236,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 && g); certified_declaration check(environment const & env, declaration const & d); -certified_declaration check(environment const & env, declaration const & d, name_generator && g, name_predicate const & opaque_hints); certified_declaration check(environment const & env, declaration const & d, name_predicate const & opaque_hints); /** diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 224e68a3e..9001cae8f 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -7,7 +7,6 @@ Author: Leonardo de Moura #include #include #include "util/rb_map.h" -#include "util/name_generator.h" #include "util/sstream.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index c69bfbc8a..3995c98ab 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -38,9 +38,7 @@ Author: Leonardo de Moura namespace lean { namespace blast { -static name * g_prefix = nullptr; static name * g_ref_prefix = nullptr; -static name * g_tmp_prefix = nullptr; static expr * g_dummy_type = nullptr; // dummy type for href/mref class imp_extension_manager { @@ -83,13 +81,11 @@ class blastenv { These messages are reported to the user only if none of the strategies have worked. We dump the content of the diagnostic channel into an blast_exception. */ io_state m_buffer_ios; - name_generator m_ngen; unsigned m_next_uref_idx{0}; unsigned m_next_mref_idx{0}; unsigned m_next_href_idx{0}; unsigned m_next_choice_idx{0}; unsigned m_next_split_idx{0}; - tmp_local_generator m_tmp_local_generator; list m_initial_context; // for setting type_context local instances name_set m_lemma_hints; name_set m_unfold_hints; @@ -132,7 +128,7 @@ class blastenv { std::vector m_stack; public: tctx(blastenv & benv): - type_context(benv.m_env, benv.m_ios.get_options(), benv.m_tmp_local_generator), + type_context(benv.m_env, benv.m_ios.get_options()), m_benv(benv) {} virtual bool is_extra_opaque(name const & n) const override { @@ -611,7 +607,7 @@ class blastenv { public: blastenv(environment const & env, io_state const & ios, list const & ls, list const & ds): m_env(env), m_ios(ios), m_buffer_ios(ios), - m_ngen(*g_prefix), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)), + m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)), m_not_reducible_pred(mk_not_reducible_pred(env)), m_class_pred(mk_class_pred(env)), m_instance_pred(mk_instance_pred(env)), @@ -695,10 +691,10 @@ public: } expr mk_fresh_local(expr const & type, binder_info const & bi) { - return m_tmp_local_generator.mk_tmp_local(type, bi); + return m_tctx.mk_tmp_local(type, bi); } bool is_fresh_local(expr const & e) const { - return m_tmp_local_generator.is_tmp_local(e); + return m_tctx.is_tmp_local(e); } expr whnf(expr const & e) { return m_tctx.whnf(e); } expr relaxed_whnf(expr const & e) { return m_tctx.relaxed_whnf(e); } @@ -1295,8 +1291,8 @@ scope_debug::~scope_debug() {} and blast meta-variables are stored in the blast state */ class tmp_tctx : public tmp_type_context { public: - tmp_tctx(environment const & env, options const & o, tmp_local_generator & gen): - tmp_type_context(env, o, gen) {} + tmp_tctx(environment const & env, options const & o): + tmp_type_context(env, o) {} /** \brief Return the type of a local constant (local or not). \remark This method allows the customer to store the type of local constants @@ -1329,7 +1325,7 @@ public: tmp_type_context * blastenv::mk_tmp_type_context() { tmp_type_context * r; if (m_tmp_ctx_pool.empty()) { - r = new tmp_tctx(m_env, m_ios.get_options(), m_tmp_local_generator); + r = new tmp_tctx(m_env, m_ios.get_options()); // Design decision: in the blast tactic, we only consider the instances that were // available in initial goal provided to the blast tactic. // So, we only need to setup the local instances when we create a new (temporary) type context. @@ -1398,16 +1394,12 @@ void initialize_blast() { register_trace_class_alias(name({"simplifier", "failure"}), "blast_detailed"); register_trace_class_alias(name({"cc", "merge"}), "blast_detailed"); - blast::g_prefix = new name(name::mk_internal_unique_name()); - blast::g_tmp_prefix = new name(name::mk_internal_unique_name()); blast::g_ref_prefix = new name(name::mk_internal_unique_name()); blast::g_imp_extension_manager = new blast::imp_extension_manager(); blast::g_dummy_type = new expr(mk_constant(*blast::g_ref_prefix)); } void finalize_blast() { delete blast::g_imp_extension_manager; - delete blast::g_prefix; - delete blast::g_tmp_prefix; delete blast::g_ref_prefix; delete blast::g_dummy_type; } diff --git a/src/library/class.cpp b/src/library/class.cpp index 3e5ed184e..806594be2 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/lbool.h" #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/instantiate.h" #include "library/scoped_ext.h" #include "library/kernel_serializer.h" @@ -248,25 +249,23 @@ bool is_class(environment const & env, name const & c) { return s.m_instances.contains(c); } -type_checker_ptr mk_class_type_checker(environment const & env, name_generator && ngen, bool conservative) { +type_checker_ptr mk_class_type_checker(environment const & env, bool conservative) { auto pred = conservative ? mk_not_reducible_pred(env) : mk_irreducible_pred(env); class_state s = class_ext::get_state(env); - return mk_type_checker(env, std::move(ngen), [=](name const & n) { + return mk_type_checker(env, [=](name const & n) { return s.m_instances.contains(n) || pred(n); }); } -static name * g_tmp_prefix = nullptr; environment add_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) { declaration d = env.get(n); expr type = d.get_type(); - name_generator ngen(*g_tmp_prefix); - auto tc = mk_class_type_checker(env, ngen.mk_child(), false); + auto tc = mk_class_type_checker(env, false); while (true) { type = tc->whnf(type).first; if (!is_pi(type)) break; - type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type))); + type = instantiate(binding_body(type), mk_local(mk_fresh_name(), binding_domain(type))); } name c = get_class_name(env, get_app_fn(type)); check_is_class(env, c); @@ -303,7 +302,7 @@ static pair get_source_target(environment const & env, type_checker } environment add_trans_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) { - type_checker_ptr tc = mk_type_checker(env, name_generator()); + type_checker_ptr tc = mk_type_checker(env); pair src_tgt = get_source_target(env, *tc, n); class_state const & s = class_ext::get_state(env); tc_multigraph g = s.m_mgraph; @@ -437,7 +436,7 @@ static lbool is_quick_ext_class(type_checker const & tc, expr const & type, name static optional is_full_ext_class(type_checker & tc, expr type) { type = tc.whnf(type).first; if (is_pi(type)) { - return is_full_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type)))); + return is_full_ext_class(tc, instantiate(binding_body(type), mk_local(mk_fresh_name(), binding_domain(type)))); } else { expr f = get_app_fn(type); if (!is_constant(f)) @@ -472,7 +471,6 @@ list get_local_instances(type_checker & tc, list const & ctx, name c } void initialize_class() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); g_source = new name("_source"); g_class_name = new name("class"); g_key = new std::string("class"); @@ -512,6 +510,5 @@ void finalize_class() { delete g_key; delete g_class_name; delete g_source; - delete g_tmp_prefix; } } diff --git a/src/library/class.h b/src/library/class.h index 9cb4b7152..d99b3d3ef 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/util.h" namespace lean { /** \brief Create type checker that treats classes as opaque constants */ -type_checker_ptr mk_class_type_checker(environment const & env, name_generator && ngen, bool conservative); +type_checker_ptr mk_class_type_checker(environment const & env, bool conservative); /** \brief Add a new 'class' to the environment (if it is not already declared) */ environment add_class(environment const & env, name const & n, name const & ns, bool persistent); /** \brief Add a new 'class instance' to the environment with default priority. */ diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index f9be1461f..1a6c6a45e 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/lbool.h" #include "util/interrupt.h" +#include "util/fresh_name.h" #include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "kernel/metavar.h" @@ -34,7 +35,6 @@ namespace lean { [[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); } static name * g_class_force_new = nullptr; -static name * g_prefix = nullptr; bool get_class_force_new(options const & o) { return o.get_bool(*g_class_force_new, false); @@ -130,7 +130,7 @@ public: static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, local_context const & _ctx, expr const & m, bool is_strict, bool use_local_instances, pos_info_provider const * pip) { justification j = mk_failed_to_synthesize_jst(env, m); - auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator &&) { + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s) { local_context ctx; if (use_local_instances) ctx = _ctx.instantiate(substitution(s)); @@ -170,10 +170,9 @@ static constraint mk_class_instance_root_cnstr(environment const & env, io_state */ pair mk_new_class_instance_elaborator( environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, optional const & suffix, bool use_local_instances, + optional const & suffix, bool use_local_instances, bool is_strict, optional const & type, tag g, pos_info_provider const * pip) { - name_generator ngen(prefix); - expr m = ctx.mk_meta(ngen, suffix, type, g); + expr m = ctx.mk_meta(suffix, type, g); constraint c = mk_class_instance_root_cnstr(env, ios, ctx, m, is_strict, use_local_instances, pip); return mk_pair(m, c); @@ -203,7 +202,6 @@ optional mk_subsingleton_instance(environment const & env, options const & } void initialize_class_instance_resolution() { - g_prefix = new name(name::mk_internal_unique_name()); g_class_force_new = new name{"class", "force_new"}; register_bool_option(*g_class_force_new, false, @@ -211,7 +209,6 @@ void initialize_class_instance_resolution() { } void finalize_class_instance_resolution() { - delete g_prefix; delete g_class_force_new; } @@ -233,7 +230,6 @@ static bool get_class_trace_instances(options const & o) { /** \brief Context for handling class-instance metavariable choice constraint */ struct class_instance_context { io_state m_ios; - name_generator m_ngen; type_checker_ptr m_tc; expr m_main_meta; bool m_use_local_instances; @@ -244,16 +240,15 @@ struct class_instance_context { char const * m_fname; optional m_pos; class_instance_context(environment const & env, io_state const & ios, - name const & prefix, bool use_local_instances): + bool use_local_instances): m_ios(ios), - m_ngen(prefix), m_use_local_instances(use_local_instances) { m_fname = nullptr; m_trace_instances = get_class_trace_instances(ios.get_options()); m_max_depth = get_class_instance_max_depth(ios.get_options()); m_conservative = true; // We removed the option class.conservative m_trans_instances = get_class_trans_instances(ios.get_options()); - m_tc = mk_class_type_checker(env, m_ngen.mk_child(), m_conservative); + m_tc = mk_class_type_checker(env, m_conservative); options opts = m_ios.get_options(); opts = opts.update_if_undef(get_pp_purify_metavars_name(), false); opts = opts.update_if_undef(get_pp_implicit_name(), true); @@ -349,7 +344,6 @@ struct class_instance_elaborator : public choice_iterator { optional try_instance(expr const & inst, expr const & inst_type, bool use_globals) { type_checker & tc = m_C->tc(); - name_generator & ngen = m_C->m_ngen; tag g = inst.get_tag(); try { flet scope(m_ctx, m_ctx); @@ -359,7 +353,7 @@ struct class_instance_elaborator : public choice_iterator { meta_type = tc.whnf(meta_type).first; if (!is_pi(meta_type)) break; - expr local = mk_local(ngen.next(), binding_name(meta_type), + expr local = mk_local(mk_fresh_name(), binding_name(meta_type), binding_domain(meta_type), binding_info(meta_type)); m_ctx.add_local(local); locals.push_back(local); @@ -379,7 +373,7 @@ struct class_instance_elaborator : public choice_iterator { arg = ac.first; cs.push_back(ac.second); } else { - arg = m_ctx.mk_meta(m_C->m_ngen, some_expr(binding_domain(type)), g); + arg = m_ctx.mk_meta(some_expr(binding_domain(type)), g); } r = mk_app(r, arg, g); type = instantiate(binding_body(type), arg); @@ -396,11 +390,10 @@ struct class_instance_elaborator : public choice_iterator { optional try_instance(name const & inst, bool use_globals) { environment const & env = m_C->env(); if (auto decl = env.find(inst)) { - name_generator & ngen = m_C->m_ngen; buffer ls_buffer; unsigned num_univ_ps = decl->get_num_univ_params(); for (unsigned i = 0; i < num_univ_ps; i++) - ls_buffer.push_back(mk_meta_univ(ngen.next())); + ls_buffer.push_back(mk_meta_univ(mk_fresh_name())); levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); expr inst_cnst = copy_tag(m_meta, mk_constant(inst, ls)); expr inst_type = instantiate_type_univ_params(*decl, ls); @@ -444,7 +437,7 @@ static constraint mk_class_instance_cnstr(std::shared_ptrenv(); justification j = mk_failed_to_synthesize_jst(env, m); - auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &, name_generator const &) { + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &) { if (auto cls_name_it = is_ext_class(C->tc(), meta_type)) { name cls_name = *cls_name_it; list const & ctx_lst = ctx.get_data(); @@ -472,7 +465,7 @@ static constraint mk_class_instance_cnstr(std::shared_ptr mk_class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, optional const & type, tag g, unsigned depth, bool use_globals) { - expr m = ctx.mk_meta(C->m_ngen, type, g); + expr m = ctx.mk_meta(type, g); constraint c = mk_class_instance_cnstr(C, ctx, m, depth, use_globals); return mk_pair(m, c); } @@ -482,8 +475,7 @@ static constraint mk_class_instance_root_cnstr(std::shared_ptrenv(); justification j = mk_failed_to_synthesize_jst(env, m); - auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, - name_generator && ngen) { + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s) { environment const & env = C->env(); auto cls_name_it = is_ext_class(C->tc(), meta_type); if (!cls_name_it) { @@ -524,7 +516,7 @@ static constraint mk_class_instance_root_cnstr(std::shared_ptr(constraints()); }; - unify_result_seq seq1 = unify(env, 1, &c, std::move(ngen), substitution(), new_cfg); + unify_result_seq seq1 = unify(env, 1, &c, substitution(), new_cfg); unify_result_seq seq2 = filter(seq1, [=](pair const & p) { substitution new_s = p.first; expr result = new_s.instantiate(new_meta); @@ -559,11 +551,11 @@ static constraint mk_class_instance_root_cnstr(std::shared_ptr mk_old_class_instance_elaborator( environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, optional const & suffix, bool use_local_instances, + optional const & suffix, bool use_local_instances, bool is_strict, optional const & type, tag g, unifier_config const & cfg, pos_info_provider const * pip) { - auto C = std::make_shared(env, ios, prefix, use_local_instances); - expr m = ctx.mk_meta(C->m_ngen, suffix, type, g); + auto C = std::make_shared(env, ios, use_local_instances); + expr m = ctx.mk_meta(suffix, type, g); C->set_main_meta(m); if (pip) C->set_pos(pip->get_file_name(), pip->get_pos_info(m)); @@ -573,15 +565,15 @@ pair mk_old_class_instance_elaborator( pair mk_class_instance_elaborator( environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, optional const & suffix, bool use_local_instances, + optional const & suffix, bool use_local_instances, bool is_strict, optional const & type, tag g, pos_info_provider const * pip) { if (is_standard(env) || get_class_force_new(ios.get_options())) { - return mk_new_class_instance_elaborator(env, ios, ctx, prefix, suffix, use_local_instances, + return mk_new_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances, is_strict, type, g, pip); } else { unifier_config cfg(ios.get_options(), true /* use exceptions */, true /* discard */); - return mk_old_class_instance_elaborator(env, ios, ctx, prefix, suffix, use_local_instances, + return mk_old_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances, is_strict, type, g, cfg, pip); } } diff --git a/src/library/class_instance_resolution.h b/src/library/class_instance_resolution.h index 0bc035f97..84d55aa37 100644 --- a/src/library/class_instance_resolution.h +++ b/src/library/class_instance_resolution.h @@ -34,7 +34,7 @@ optional mk_class_instance(environment const & env, list const & ctx */ pair mk_class_instance_elaborator( environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, optional const & suffix, bool use_local_instances, + optional const & suffix, bool use_local_instances, bool is_strict, optional const & type, tag g, pos_info_provider const * pip); optional mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances); diff --git a/src/library/composition_manager.cpp b/src/library/composition_manager.cpp index 43062b0b0..ab7b59efe 100644 --- a/src/library/composition_manager.cpp +++ b/src/library/composition_manager.cpp @@ -57,7 +57,7 @@ struct elim_proj_mk : public replace_visitor { } elim_proj_mk(environment const & env): - m_env(env), m_tc(mk_opaque_type_checker(env, name_generator())) {} + m_env(env), m_tc(mk_opaque_type_checker(env)) {} }; // Return true iff d is a declaration of the form (mk ... ) @@ -99,8 +99,7 @@ pair compose(environment const & env, type_checker & tc, name levels f_ls = param_names_to_levels(f_decl.get_univ_params()); expr f_type = instantiate_type_univ_params(f_decl, f_ls); buffer f_domain; - name_generator ngen = tc.mk_ngen(); - expr f_codomain = to_telescope(ngen, f_type, f_domain); + expr f_codomain = to_telescope(f_type, f_domain); buffer B_args; expr const & B = get_app_args(f_codomain, B_args); if (!is_constant(B)) diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 66e40d7c2..52662afa3 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -44,7 +45,6 @@ static environment mk_below(environment const & env, name const & n, bool ibelow return env; inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n); type_checker tc(env); - name_generator ngen; unsigned nparams = std::get<1>(decls); declaration ind_decl = env.get(n); declaration rec_decl = env.get(inductive::get_elim_name(n)); @@ -82,7 +82,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow } Type_result = mk_sort(rlvl); buffer ref_args; - to_telescope(ngen, ref_type, ref_args); + to_telescope(ref_type, ref_args); if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1) throw_corrupted(n); @@ -108,7 +108,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow // add type formers for (unsigned i = nparams; i < nparams + ntypeformers; i++) { buffer targs; - to_telescope(ngen, mlocal_type(args[i]), targs); + to_telescope(mlocal_type(args[i]), targs); rec = mk_app(rec, Fun(targs, Type_result)); } // add minor premises @@ -116,7 +116,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow expr minor = ref_args[i]; expr minor_type = mlocal_type(minor); buffer minor_args; - minor_type = to_telescope(ngen, minor_type, minor_args); + minor_type = to_telescope(minor_type, minor_args); buffer prod_pairs; for (expr & minor_arg : minor_args) { buffer minor_arg_args; @@ -168,7 +168,6 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) return env; inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n); type_checker tc(env); - name_generator ngen; unsigned nparams = std::get<1>(decls); declaration ind_decl = env.get(n); declaration rec_decl = env.get(inductive::get_elim_name(n)); @@ -211,7 +210,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) ref_type = rec_decl.get_type(); } buffer ref_args; - to_telescope(ngen, ref_type, ref_args); + to_telescope(ref_type, ref_args); if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1) throw_corrupted(n); @@ -257,12 +256,12 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) { expr const & C = ref_args[i]; buffer F_args; - to_telescope(ngen, mlocal_type(C), F_args); + to_telescope(mlocal_type(C), F_args); expr F_result = mk_app(C, F_args); expr F_below = mk_app(belows[j], F_args); - F_args.push_back(mk_local(ngen.next(), "f", F_below, binder_info())); + F_args.push_back(mk_local(mk_fresh_name(), "f", F_below, binder_info())); expr F_type = Pi(F_args, F_result); - expr F = mk_local(ngen.next(), F_name.append_after(j+1), F_type, binder_info()); + expr F = mk_local(mk_fresh_name(), F_name.append_after(j+1), F_type, binder_info()); Fs.push_back(F); args.push_back(F); } @@ -278,7 +277,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) { expr const & C = ref_args[i]; buffer C_args; - to_telescope(ngen, mlocal_type(C), C_args); + to_telescope(mlocal_type(C), C_args); expr C_t = mk_app(C, C_args); expr below_t = mk_app(belows[j], C_args); expr prod = mk_prod(tc, C_t, below_t, ind); @@ -289,7 +288,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) expr minor = ref_args[i]; expr minor_type = mlocal_type(minor); buffer minor_args; - minor_type = to_telescope(ngen, minor_type, minor_args); + minor_type = to_telescope(minor_type, minor_args); buffer pairs; for (expr & minor_arg : minor_args) { buffer minor_arg_args; diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 858eb1c34..5e2837ea1 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -60,7 +61,6 @@ environment mk_cases_on(environment const & env, name const & n) { if (!decls) throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' is not an inductive datatype"); name cases_on_name(n, "cases_on"); - name_generator ngen; name rec_name = inductive::get_elim_name(n); declaration rec_decl = env.get(rec_name); declaration ind_decl = env.get(n); @@ -72,7 +72,7 @@ environment mk_cases_on(environment const & env, name const & n) { buffer rec_params; expr rec_type = rec_decl.get_type(); while (is_pi(rec_type)) { - expr local = mk_local(ngen.next(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type)); + expr local = mk_local(mk_fresh_name(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type)); rec_type = instantiate(binding_body(rec_type), local); rec_params.push_back(local); } @@ -143,7 +143,7 @@ environment mk_cases_on(environment const & env, name const & n) { buffer minor_params; expr minor_type = mlocal_type(minor); while (is_pi(minor_type)) { - expr local = mk_local(ngen.next(), binding_name(minor_type), binding_domain(minor_type), + expr local = mk_local(mk_fresh_name(), binding_name(minor_type), binding_domain(minor_type), binding_info(minor_type)); expr curr_type = mlocal_type(local); while (is_pi(curr_type)) diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index c3ca09ec4..1c7d65f8e 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "util/list_fn.h" +#include "util/fresh_name.h" #include "kernel/expr.h" #include "kernel/type_checker.h" #include "kernel/abstract.h" @@ -324,7 +325,6 @@ class equation_compiler_fn { environment const & env() const { return m_tc.env(); } io_state const & ios() const { return m_ios; } io_state_stream out() const { return regular(env(), ios()); } - name mk_fresh_name() { return m_tc.mk_fresh_name(); } expr whnf(expr const & e) { return m_tc.whnf(e).first; } expr infer_type(expr const & e) { return m_tc.infer(e).first; } bool is_def_eq(expr const & e1, expr const & e2) { return m_tc.is_def_eq(e1, e2).first; } @@ -337,13 +337,11 @@ class equation_compiler_fn { } expr to_telescope(expr const & e, buffer & tele) { - name_generator ngen = m_tc.mk_ngen(); - return ::lean::to_telescope(ngen, e, tele, optional()); + return ::lean::to_telescope(e, tele, optional()); } expr fun_to_telescope(expr const & e, buffer & tele) { - name_generator ngen = m_tc.mk_ngen(); - return ::lean::fun_to_telescope(ngen, e, tele, optional()); + return ::lean::fun_to_telescope(e, tele, optional()); } // Similar to to_telescope, but uses normalization @@ -1213,7 +1211,7 @@ class equation_compiler_fn { if (!check_rhs(binding_domain(e), arg)) { return false; } else { - expr l = mk_local(m_main.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); + expr l = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); return check_rhs(instantiate(binding_body(e), l), arg); } } @@ -1401,7 +1399,7 @@ class equation_compiler_fn { return mk_app(new_fn, new_args, e.get_tag()); } case expr_kind::Lambda: { - expr local = mk_local(m_main.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); + expr local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); expr body = instantiate(binding_body(e), local); expr new_body; if (is_below_type(binding_domain(e))) @@ -1412,7 +1410,7 @@ class equation_compiler_fn { } case expr_kind::Pi: { expr new_domain = elim(binding_domain(e), b); - expr local = mk_local(m_main.mk_fresh_name(), binding_name(e), new_domain, binding_info(e)); + expr local = mk_local(mk_fresh_name(), binding_name(e), new_domain, binding_info(e)); expr new_body = elim(instantiate(binding_body(e), local), b); return copy_tag(e, Pi(local, new_body)); }} diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index 2f353fbd7..a4fcc7d66 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -29,7 +30,6 @@ optional mk_no_confusion_type(environment const & env, name const & throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' is not an inductive datatype"); if (is_inductive_predicate(env, n)) return optional(); // type is a proposition - name_generator ngen; bool impredicative = env.impredicative(); unsigned nparams = std::get<1>(*decls); declaration ind_decl = env.get(n); @@ -48,7 +48,7 @@ optional mk_no_confusion_type(environment const & env, name const & return optional(); // type does not have only a restricted eliminator // All inductive datatype parameters and indices are arguments buffer args; - ind_type = to_telescope(ngen, ind_type, args, some(mk_implicit_binder_info())); + ind_type = to_telescope(ind_type, args, some(mk_implicit_binder_info())); if (!is_sort(ind_type) || args.size() < nparams) throw_corrupted(n); lean_assert(!(env.impredicative() && is_zero(sort_level(ind_type)))); @@ -56,11 +56,11 @@ optional mk_no_confusion_type(environment const & env, name const & // Create inductive datatype expr I = mk_app(mk_constant(n, ilvls), args); // Add (P : Type) - expr P = mk_local(ngen.next(), "P", mk_sort(plvl), binder_info()); + expr P = mk_local(mk_fresh_name(), "P", mk_sort(plvl), binder_info()); args.push_back(P); // add v1 and v2 elements of the inductive type - expr v1 = mk_local(ngen.next(), "v1", I, binder_info()); - expr v2 = mk_local(ngen.next(), "v2", I, binder_info()); + expr v1 = mk_local(mk_fresh_name(), "v1", I, binder_info()); + expr v2 = mk_local(mk_fresh_name(), "v2", I, binder_info()); args.push_back(v1); args.push_back(v2); expr R = mk_sort(rlvl); @@ -119,7 +119,7 @@ optional mk_no_confusion_type(environment const & env, name const & } else { h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs); } - rtype_hyp.push_back(mk_local(ngen.next(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info())); + rtype_hyp.push_back(mk_local(mk_fresh_name(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info())); } } else { // we use telescope equality (with casts) when proof irrelevance is not available @@ -153,7 +153,6 @@ environment mk_no_confusion(environment const & env, name const & n) { bool impredicative = env.impredicative(); inductive::inductive_decls decls = *inductive::is_inductive_decl(new_env, n); unsigned nparams = std::get<1>(decls); - name_generator ngen; declaration ind_decl = env.get(n); declaration no_confusion_type_decl = new_env.get(name{n, "no_confusion_type"}); declaration cases_decl = new_env.get(name(n, "cases_on")); @@ -164,7 +163,7 @@ environment mk_no_confusion(environment const & env, name const & n) { expr no_confusion_type_type = instantiate_type_univ_params(no_confusion_type_decl, ls); buffer args; expr type = no_confusion_type_type; - type = to_telescope(ngen, type, args, some(mk_implicit_binder_info())); + type = to_telescope(type, args, some(mk_implicit_binder_info())); lean_assert(args.size() >= nparams + 3); unsigned nindices = args.size() - nparams - 3; // 3 is for P v1 v2 expr range = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), args); @@ -178,7 +177,7 @@ environment mk_no_confusion(environment const & env, name const & n) { } level v_lvl = sort_level(tc.ensure_type(v_type).first); expr eq_v = mk_app(mk_constant(get_eq_name(), to_list(v_lvl)), v_type); - expr H12 = mk_local(ngen.next(), "H12", mk_app(eq_v, v1, v2), binder_info()); + expr H12 = mk_local(mk_fresh_name(), "H12", mk_app(eq_v, v1, v2), binder_info()); lean_assert(impredicative != inductive::has_dep_elim(env, get_eq_name())); args.push_back(H12); name no_confusion_name{n, "no_confusion"}; @@ -191,7 +190,7 @@ environment mk_no_confusion(environment const & env, name const & n) { // ) // H11 is for creating the generalization - expr H11 = mk_local(ngen.next(), "H11", mk_app(eq_v, v1, v1), binder_info()); + expr H11 = mk_local(mk_fresh_name(), "H11", mk_app(eq_v, v1, v1), binder_info()); // Create the type former (fun Indices v1, no_confusion_type Params Indices P v1 v1) buffer type_former_args; for (unsigned i = nparams; i < nparams + nindices; i++) @@ -254,8 +253,8 @@ environment mk_no_confusion(environment const & env, name const & n) { expr eq_rec = mk_app(mk_constant(get_eq_rec_name(), {eq_rec_l1, v_lvl}), v_type, v1); // create eq_rec type_former // (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) - expr a = mk_local(ngen.next(), "a", v_type, binder_info()); - expr H1a = mk_local(ngen.next(), "H1a", mk_app(eq_v, v1, a), binder_info()); + expr a = mk_local(mk_fresh_name(), "a", v_type, binder_info()); + expr H1a = mk_local(mk_fresh_name(), "H1a", mk_app(eq_v, v1, a), binder_info()); // reusing no_confusion_type_args... we just replace the last argument with a no_confusion_type_args.pop_back(); no_confusion_type_args.push_back(a); diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 055c83fbb..6f56e381d 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/fresh_name.h" #include "util/sstream.h" #include "kernel/abstract.h" #include "kernel/type_checker.h" @@ -186,7 +187,6 @@ environment mk_projections(environment const & env, name const & n, buffer // proj_i A (c : C A) : B_i[A, (proj_1 A n), ..., (proj_{i-1} A n)] // C.rec A (fun (x : C A), B_i[A, ...]) (fun (x_1 ... x_n), x_i) c auto p = get_nparam_intro_rule(env, n); - name_generator ngen; unsigned nparams = p.first; inductive::intro_rule intro = p.second; expr intro_type = inductive::intro_rule_type(intro); @@ -201,17 +201,17 @@ environment mk_projections(environment const & env, name const & n, buffer for (unsigned i = 0; i < nparams; i++) { if (!is_pi(intro_type)) throw_ill_formed(n); - expr param = mk_local(ngen.next(), binding_name(intro_type), binding_domain(intro_type), binder_info()); + expr param = mk_local(mk_fresh_name(), binding_name(intro_type), binding_domain(intro_type), binder_info()); intro_type = instantiate(binding_body(intro_type), param); params.push_back(param); } expr C_A = mk_app(mk_constant(n, lvls), params); binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : binder_info(); - expr c = mk_local(ngen.next(), name("c"), C_A, c_bi); + expr c = mk_local(mk_fresh_name(), name("c"), C_A, c_bi); buffer intro_type_args; // arguments that are not parameters expr it = intro_type; while (is_pi(it)) { - expr local = mk_local(ngen.next(), binding_name(it), binding_domain(it), binding_info(it)); + expr local = mk_local(mk_fresh_name(), binding_name(it), binding_domain(it), binding_info(it)); intro_type_args.push_back(local); it = instantiate(binding_body(it), local); } diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index 83966e2e8..7cf1f1f32 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -22,13 +23,12 @@ environment mk_rec_on(environment const & env, name const & n) { if (!inductive::is_inductive_decl(env, n)) throw exception(sstream() << "error in 'rec_on' generation, '" << n << "' is not an inductive datatype"); name rec_on_name(n, "rec_on"); - name_generator ngen; declaration rec_decl = env.get(inductive::get_elim_name(n)); buffer locals; expr rec_type = rec_decl.get_type(); while (is_pi(rec_type)) { - expr local = mk_local(ngen.next(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type)); + expr local = mk_local(mk_fresh_name(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type)); rec_type = instantiate(binding_body(rec_type), local); locals.push_back(local); } diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp index 24b301fed..775a2fa9d 100644 --- a/src/library/inductive_unifier_plugin.cpp +++ b/src/library/inductive_unifier_plugin.cpp @@ -45,7 +45,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, 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)); @@ -74,7 +74,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { expr hint = intro_fn; expr intro_type = tc.whnf(inductive::intro_rule_type(intro), cs_intro); while (is_pi(intro_type)) { - expr new_arg = mk_app(mk_aux_metavar_for(ngen, mtype), margs); + expr new_arg = mk_app(mk_aux_metavar_for(mtype), margs); hint = mk_app(hint, new_arg); intro_type = tc.whnf(instantiate(binding_body(intro_type), new_arg), cs_intro); } @@ -90,8 +90,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 & ngen, - expr const & lhs, expr const & rhs, justification const & j) const { + lazy_list process_elim_meta_core(type_checker & tc, 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); if (!dcs.first) @@ -106,7 +105,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { auto decls = *inductive::is_inductive_decl(env, it_name); for (auto const & d : std::get<2>(decls)) { if (inductive::inductive_decl_name(d) == it_name) - return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, cs); + return add_elim_meta_cnstrs(tc, d, elim, args, rhs, j, cs); } lean_unreachable(); // LCOV_EXCL_LINE } @@ -116,16 +115,16 @@ 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 && ngen) const { + virtual lazy_list solve(type_checker & tc, constraint const & c) const { if (!is_eq_cnstr(c)) return lazy_list(); expr const & lhs = cnstr_lhs_expr(c); expr const & rhs = cnstr_rhs_expr(c); justification const & j = c.get_justification(); if (inductive::is_elim_meta_app(tc, lhs)) - return process_elim_meta_core(tc, ngen, lhs, rhs, j); + return process_elim_meta_core(tc, lhs, rhs, j); else if (inductive::is_elim_meta_app(tc, rhs)) - return process_elim_meta_core(tc, ngen, rhs, lhs, j); + return process_elim_meta_core(tc, rhs, lhs, j); else return lazy_list(); } diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 369c2f765..3a470f778 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/metavar.h" @@ -75,28 +76,28 @@ expr local_context::apply_context(expr const & f, tag g) const { return apply_context_core(f, m_ctx, g); } -expr local_context::mk_type_metavar(name_generator & ngen, tag g) const { - name n = ngen.next(); - expr s = mk_sort(mk_meta_univ(ngen.next()), g); +expr local_context::mk_type_metavar(tag g) const { + name n = mk_fresh_name(); + expr s = mk_sort(mk_meta_univ(mk_fresh_name()), g); expr t = pi_abstract_context(s, g); return ::lean::mk_metavar(n, t, g); } -expr local_context::mk_type_meta(name_generator & ngen, tag g) const { - return apply_context(mk_type_metavar(ngen, g), g); +expr local_context::mk_type_meta(tag g) const { + return apply_context(mk_type_metavar(g), g); } -expr local_context::mk_metavar(name_generator & ngen, optional const & suffix, optional const & type, tag g) const { - name n = ngen.next(); +expr local_context::mk_metavar(optional const & suffix, optional const & type, tag g) const { + name n = mk_fresh_name(); if (suffix) n = n + *suffix; - expr r_type = type ? *type : mk_type_meta(ngen, g); + expr r_type = type ? *type : mk_type_meta(g); expr t = pi_abstract_context(r_type, g); return ::lean::mk_metavar(n, t, g); } -expr local_context::mk_meta(name_generator & ngen, optional const & suffix, optional const & type, tag g) const { - expr mvar = mk_metavar(ngen, suffix, type, g); +expr local_context::mk_meta(optional const & suffix, optional const & type, tag g) const { + expr mvar = mk_metavar(suffix, type, g); expr meta = apply_context(mvar, g); return meta; } diff --git a/src/library/local_context.h b/src/library/local_context.h index c5f88368d..7b3c5ab83 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -44,7 +44,7 @@ public: (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), where \c ?u is a fresh universe metavariable. */ - expr mk_type_metavar(name_generator & ngen, tag g) const; + expr mk_type_metavar(tag g) const; /** \brief Assuming \c m_ctx is [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], @@ -54,7 +54,7 @@ public: \remark The type of the resulting expression is Type.{?u} */ - expr mk_type_meta(name_generator & ngen, tag g) const; + expr mk_type_meta(tag g) const; /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], @@ -68,7 +68,7 @@ public: \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name. */ - expr mk_metavar(name_generator & ngen, optional const & suffix, optional const & type, tag g) const; + expr mk_metavar(optional const & suffix, optional const & type, tag g) const; /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], @@ -79,9 +79,9 @@ public: \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name. */ - expr mk_meta(name_generator & ngen, optional const & suffix, optional const & type, tag g) const; - expr mk_meta(name_generator & ngen, optional const & type, tag g) const { - return mk_meta(ngen, optional(), type, g); + expr mk_meta(optional const & suffix, optional const & type, tag g) const; + expr mk_meta(optional const & type, tag g) const { + return mk_meta(optional(), type, g); } /** \brief Return context as a list */ diff --git a/src/library/match.cpp b/src/library/match.cpp index 2e937725c..2312f92b9 100644 --- a/src/library/match.cpp +++ b/src/library/match.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" @@ -20,7 +21,6 @@ class match_fn : public match_context { optional * m_esubst; unsigned m_lsubst_sz; optional * m_lsubst; - name_generator m_ngen; name_map * m_name_subst; match_plugin const * m_plugin; buffer> m_stack; @@ -96,7 +96,7 @@ class match_fn : public match_context { virtual void assign(level const & p, level const & t) { return _assign(p, t); } virtual optional get_subst(expr const & x) const { return _get_subst(x); } virtual optional get_subst(level const & x) const { return _get_subst(x); } - virtual name mk_name() { return m_ngen.next(); } + virtual name mk_name() { return mk_fresh_name(); } bool args_are_distinct_locals(buffer const & args) { for (auto it = args.begin(); it != args.end(); it++) { @@ -131,7 +131,7 @@ class match_fn : public match_context { expr t_d = instantiate_rev(binding_domain(t), ls.size(), ls.data()); if (!_match(p_d, t_d)) return false; - expr l = mk_local(m_ngen.next(), binding_name(t), t_d, binding_info(t)); + expr l = mk_local(mk_fresh_name(), binding_name(t), t_d, binding_info(t)); ls.push_back(l); p = binding_body(p); t = binding_body(t); @@ -363,11 +363,10 @@ class match_fn : public match_context { public: match_fn(unsigned lsubst_sz, optional * lsubst, unsigned esubst_sz, optional * esubst, - name_generator const & ngen, name_map * name_subst, match_plugin const * plugin, bool * assigned): m_esubst_sz(esubst_sz), m_esubst(esubst), m_lsubst_sz(lsubst_sz), m_lsubst(lsubst), - m_ngen(ngen), m_name_subst(name_subst), m_plugin(plugin), + m_name_subst(name_subst), m_plugin(plugin), m_assigned(assigned) {} virtual bool match(expr const & p, expr const & t) { return _match(p, t); } @@ -376,21 +375,17 @@ public: bool match(expr const & p, expr const & t, unsigned lsubst_sz, optional * lsubst, unsigned esubst_sz, optional * esubst, - name const * prefix, name_map * name_subst, match_plugin const * plugin, bool * assigned) { + name_map * name_subst, match_plugin const * plugin, bool * assigned) { lean_assert(closed(t)); lean_assert(closed(p)); - if (prefix) - return match_fn(lsubst_sz, lsubst, esubst_sz, esubst, name_generator(*prefix), - name_subst, plugin, assigned).match(p, t); - else - return match_fn(lsubst_sz, lsubst, esubst_sz, esubst, - name_generator(), name_subst, plugin, assigned).match(p, t); + return match_fn(lsubst_sz, lsubst, esubst_sz, esubst, + name_subst, plugin, assigned).match(p, t); } bool match(expr const & p, expr const & t, buffer> & lsubst, buffer> & esubst, - name const * prefix, name_map * name_subst, match_plugin const * plugin, bool * assigned) { + name_map * name_subst, match_plugin const * plugin, bool * assigned) { return match(p, t, lsubst.size(), lsubst.data(), esubst.size(), esubst.data(), - prefix, name_subst, plugin, assigned); + name_subst, plugin, assigned); } bool whnf_match_plugin::on_failure(expr const & p, expr const & t, match_context & ctx) const { diff --git a/src/library/match.h b/src/library/match.h index 22d96f21f..bd94d1eea 100644 --- a/src/library/match.h +++ b/src/library/match.h @@ -90,8 +90,6 @@ public: \pre \c esubst and \c lsubst must be big enough to store the substitution. That is, their size should be > than the index of any special metavariable occuring in p. - If prefix is provided, then it is used for creating unique names. - If name_subst is different from nullptr, then the procedure stores in name_subst a mapping for binder names. It maps the binder names used in the pattern \c p into the binder names used in \c t. @@ -101,12 +99,12 @@ public: If \c assigned is provided, then it is set to true if \c esubst or \c lsubst is updated. */ bool match(expr const & p, expr const & t, buffer> & lsubst, buffer> & esubst, - name const * prefix = nullptr, name_map * name_subst = nullptr, match_plugin const * plugin = nullptr, + name_map * name_subst = nullptr, match_plugin const * plugin = nullptr, bool * assigned = nullptr); bool match(expr const & p, expr const & t, unsigned lsubst_sz, optional * lsubst, unsigned esubst_sz, optional * esubst, - name const * prefix = nullptr, name_map * name_subst = nullptr, + name_map * name_subst = nullptr, match_plugin const * plugin = nullptr, bool * assigned = nullptr); void initialize_match(); diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 528efa623..9f79dbf03 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/interrupt.h" -#include "util/name_generator.h" +#include "util/fresh_name.h" #include "kernel/replace_fn.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" @@ -265,7 +265,6 @@ class normalize_fn { // So, we use m_full_tc for this kind of operation. It is an unconstrained type checker. // See issue #801 type_checker m_full_tc; - name_generator m_ngen; std::function m_pred; // NOLINT bool m_save_cnstrs; constraint_seq m_cnstrs; @@ -276,7 +275,7 @@ class normalize_fn { expr normalize_binding(expr const & e) { expr d = normalize(binding_domain(e)); - expr l = mk_local(m_ngen.next(), binding_name(e), d, binding_info(e)); + expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e)); expr b = abstract(normalize(instantiate(binding_body(e), l)), l); return update_binding(e, d, b); } @@ -408,7 +407,7 @@ class normalize_fn { public: normalize_fn(type_checker & tc, bool save, bool eta, bool nested_prop = true): - m_tc(tc), m_full_tc(tc.env()), m_ngen(m_tc.mk_ngen()), + m_tc(tc), m_full_tc(tc.env()), m_pred([](expr const &) { return true; }), m_save_cnstrs(save), m_use_eta(eta), m_eval_nested_prop(nested_prop) { if (!is_standard(env())) @@ -416,7 +415,7 @@ public: } normalize_fn(type_checker & tc, std::function const & fn, bool eta, bool nested_prop = true): // NOLINT - m_tc(tc), m_full_tc(tc.env()), m_ngen(m_tc.mk_ngen()), + m_tc(tc), m_full_tc(tc.env()), m_pred(fn), m_save_cnstrs(true), m_use_eta(eta), m_eval_nested_prop(nested_prop) { if (!is_standard(env())) m_eval_nested_prop = true; diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 82413f18d..c09d30b19 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -62,12 +62,9 @@ struct reducible_config { template class scoped_ext; typedef scoped_ext reducible_ext; -static name * g_tmp_prefix = nullptr; - void initialize_reducible() { g_class_name = new name("reducible"); g_key = new std::string("REDU"); - g_tmp_prefix = new name(name::mk_internal_unique_name()); reducible_ext::initialize(); register_attribute("reducible", "reducible", @@ -104,7 +101,6 @@ void initialize_reducible() { void finalize_reducible() { reducible_ext::finalize(); - delete g_tmp_prefix; delete g_key; delete g_class_name; } @@ -157,23 +153,19 @@ name_predicate mk_irreducible_pred(environment const & env) { }; } -type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, reducible_behavior rb) { +type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb) { switch (rb) { case UnfoldReducible: - return mk_type_checker(env, std::move(ngen), mk_not_reducible_pred(env)); + return mk_type_checker(env, mk_not_reducible_pred(env)); case UnfoldQuasireducible: - return mk_type_checker(env, std::move(ngen), mk_not_quasireducible_pred(env)); + return mk_type_checker(env, mk_not_quasireducible_pred(env)); case UnfoldSemireducible: - return mk_type_checker(env, std::move(ngen), mk_irreducible_pred(env)); + return mk_type_checker(env, mk_irreducible_pred(env)); } lean_unreachable(); } -type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb) { - return mk_type_checker(env, name_generator(*g_tmp_prefix), rb); -} - -type_checker_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen) { - return mk_type_checker(env, std::move(ngen), [](name const &) { return true; }); +type_checker_ptr mk_opaque_type_checker(environment const & env) { + return mk_type_checker(env, [](name const &) { return true; }); } } diff --git a/src/library/reducible.h b/src/library/reducible.h index 5d186f893..d68d16fc5 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -40,12 +40,10 @@ name_predicate mk_irreducible_pred(environment const & env); enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireducible }; /** \brief Create a type checker that takes the "reducibility" hints into account. */ -type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, - reducible_behavior r = UnfoldSemireducible); type_checker_ptr mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible); /** \brief Create a type checker that treats all definitions as opaque. */ -type_checker_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen); +type_checker_ptr mk_opaque_type_checker(environment const & env); void initialize_reducible(); void finalize_reducible(); diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index e6c72e0b2..72d9e81f4 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -77,8 +77,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const return proof_state_seq(); } bool class_inst = get_apply_class_instance(ios.get_options()); - name_generator ngen = s.get_ngen(); - std::shared_ptr tc(mk_type_checker(env, ngen.mk_child())); + std::shared_ptr tc(mk_type_checker(env)); goal g = head(gs); goals tail_gs = tail(gs); expr t = g.get_type(); @@ -116,13 +115,13 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const bool use_local_insts = true; bool is_strict = false; auto mc = mk_class_instance_elaborator( - env, ios, ctx, ngen.next(), optional(), + env, ios, ctx, optional(), use_local_insts, is_strict, some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), nullptr); meta = mc.first; cs.push_back(mc.second); } else { - meta = g.mk_meta(ngen.next(), head_beta_reduce(binding_domain(e_t))); + meta = g.mk_meta(mk_fresh_name(), head_beta_reduce(binding_domain(e_t))); } e = mk_app(e, meta); e_t = instantiate(binding_body(e_t), meta); @@ -141,12 +140,11 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const return proof_state_seq(); } dcs.second.linearize(cs); - unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), s.get_subst(), cfg); + unify_result_seq rseq = unify(env, cs.size(), cs.data(), s.get_subst(), cfg); list meta_lst = to_list(metas.begin(), metas.end()); return map2(rseq, [=](pair const & p) -> proof_state { substitution const & subst = p.first; constraints const & postponed = p.second; - name_generator new_ngen(ngen); substitution new_subst = subst; expr new_e = new_subst.instantiate_all(e); assign(new_subst, g, new_e); @@ -171,7 +169,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const } } } - return proof_state(s, new_gs, new_subst, new_ngen, postponed); + return proof_state(s, new_gs, new_subst, postponed); }); } @@ -201,15 +199,14 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kin return proof_state_seq(); } goal const & g = head(gs); - name_generator ngen = s.get_ngen(); expr new_e; substitution new_subst; constraints cs_; try { - auto ecs = elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), s.get_subst(), false); + auto ecs = elab(g, ios.get_options(), e, none_expr(), s.get_subst(), false); std::tie(new_e, new_subst, cs_) = ecs; buffer cs; to_buffer(cs_, cs); to_buffer(s.get_postponed(), cs); - proof_state new_s(s, new_subst, ngen, constraints()); + proof_state new_s(s, new_subst, constraints()); return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k); } catch (exception &) { if (s.report_failure()) diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp index 129f0bc3b..a2d228663 100644 --- a/src/library/tactic/assert_tactic.cpp +++ b/src/library/tactic/assert_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "library/constants.h" #include "library/tactic/tactic.h" @@ -28,21 +29,20 @@ tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) { goals const & gs = new_s.get_goals(); goal const & g = head(gs); - name_generator ngen = new_s.get_ngen(); - expr new_meta1 = g.mk_meta(ngen.next(), *new_e); + expr new_meta1 = g.mk_meta(mk_fresh_name(), *new_e); goal new_goal1(new_meta1, *new_e); - expr new_local = mk_local(ngen.next(), id, *new_e, binder_info()); + expr new_local = mk_local(mk_fresh_name(), id, *new_e, binder_info()); buffer hyps; g.get_hyps(hyps); hyps.push_back(new_local); - expr new_mvar2 = mk_metavar(ngen.next(), Pi(hyps, g.get_type())); + expr new_mvar2 = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type())); hyps.pop_back(); expr new_meta2_core = mk_app(new_mvar2, hyps); expr new_meta2 = mk_app(new_meta2_core, new_local); goal new_goal2(new_meta2, g.get_type()); substitution new_subst = new_s.get_subst(); assign(new_subst, g, mk_app(new_meta2_core, new_meta1)); - return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst, ngen)); + return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst)); } return none_proof_state(); }); diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index fa49d24b6..c9b0fb370 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/lazy_list_fn.h" +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/error_msgs.h" #include "library/constants.h" @@ -28,9 +29,8 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) { if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) { goals const & gs = new_s.get_goals(); goal const & g = head(gs); - name_generator ngen = new_s.get_ngen(); substitution subst = new_s.get_subst(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); constraint_seq cs; if (tc->is_def_eq(t, *new_e, justification(), cs)) { if (cs) { @@ -38,23 +38,22 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) { buffer cs_buf; cs.linearize(cs_buf); to_buffer(new_s.get_postponed(), cs_buf); - unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), ngen.mk_child(), subst, cfg); + unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), subst, cfg); return map2(rseq, [=](pair const & p) -> proof_state { substitution const & subst = p.first; constraints const & postponed = p.second; - name_generator new_ngen(ngen); substitution new_subst = subst; expr final_e = new_subst.instantiate_all(*new_e); - expr M = g.mk_meta(new_ngen.next(), final_e); + expr M = g.mk_meta(mk_fresh_name(), final_e); goal new_g(M, final_e); assign(new_subst, g, M); - return proof_state(new_s, cons(new_g, tail(gs)), new_subst, new_ngen, postponed); + return proof_state(new_s, cons(new_g, tail(gs)), new_subst, postponed); }); } - expr M = g.mk_meta(ngen.next(), *new_e); + expr M = g.mk_meta(mk_fresh_name(), *new_e); goal new_g(M, *new_e); assign(subst, g, M); - return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen)); + return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst)); } else { throw_tactic_exception_if_enabled(new_s, [=](formatter const & fmt) { format r = format("invalid 'change' tactic, the given type"); diff --git a/src/library/tactic/check_expr_tactic.cpp b/src/library/tactic/check_expr_tactic.cpp index a0adca6db..24d8d9573 100644 --- a/src/library/tactic/check_expr_tactic.cpp +++ b/src/library/tactic/check_expr_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/fresh_name.h" #include "library/constants.h" #include "library/reducible.h" #include "library/flycheck.h" @@ -20,9 +21,8 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e, return none_proof_state(); } goal const & g = head(gs); - name_generator ngen = s.get_ngen(); - expr new_e = std::get<0>(elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), s.get_subst(), false)); - auto tc = mk_type_checker(env, ngen.mk_child()); + expr new_e = std::get<0>(elab(g, ios.get_options(), e, none_expr(), s.get_subst(), false)); + auto tc = mk_type_checker(env); expr new_t = tc->infer(new_e).first; auto out = regular(env, ios); flycheck_information info(out); diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index 6ef34dbeb..a4df2289c 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "library/constants.h" #include "kernel/abstract.h" #include "library/locals.h" @@ -37,13 +38,12 @@ tactic clear_tactic(name const & n) { << "' depends on '" << n << "'"); return none_proof_state(); } - name_generator ngen = s.get_ngen(); expr new_type = g.get_type(); - expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); substitution new_subst = s.get_subst(); assign(new_subst, g, new_meta); - proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen); + proof_state new_s(s, goals(new_g, tail_gs), new_subst); return some_proof_state(new_s); } else { throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, goal does not have a hypothesis " diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp index 14da37b91..8eda7de72 100644 --- a/src/library/tactic/congruence_tactic.cpp +++ b/src/library/tactic/congruence_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "library/util.h" @@ -118,9 +119,9 @@ optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios } expr conclusion = mk_eq(tc, mk_app(fn, conclusion_lhs), mk_app(fn, conclusion_rhs)); expr mvar_type = Pi(hyps, conclusion); - expr mvar = mk_metavar(tc.mk_fresh_name(), mvar_type); + expr mvar = mk_metavar(mk_fresh_name(), mvar_type); expr meta = mk_app(mvar, hyps); - proof_state ps = to_proof_state(meta, conclusion, tc.mk_ngen()).update_report_failure(false); + proof_state ps = to_proof_state(meta, conclusion).update_report_failure(false); for (unsigned i = 0; i < eqs.size(); i++) { goal const & g = head(ps.get_goals()); optional const & eq = eqs[i]; @@ -151,7 +152,7 @@ optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios expr new_eq = mk_local(get_unused_name(name(h, eqidx), hyps), mk_eq(tc, new_rhs, new_lhs)); eqidx++; expr new_eq_pr = mk_subsingleton_elim(tc, *spr, new_rhs, new_lhs); - expr aux_mvar = mk_metavar(tc.mk_fresh_name(), Pi(hyps, g.get_type())); + expr aux_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type())); expr aux_meta_core = mk_app(aux_mvar, hyps); goal aux_g(mk_app(aux_meta_core, new_eq), g.get_type()); substitution new_subst = ps.get_subst(); @@ -194,8 +195,7 @@ tactic congruence_tactic() { goal const & g = head(gs); expr t = g.get_type(); substitution subst = s.get_subst(); - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); constraint_seq cs; t = tc->whnf(t, cs); expr lhs, rhs; @@ -229,7 +229,7 @@ tactic congruence_tactic() { optional fn_pr; if (!tc->is_def_eq(lhs_fn, rhs_fn, justification(), cs)) { expr new_type = mk_eq(*tc, lhs_fn, rhs_fn); - expr new_meta = g.mk_meta(ngen.next(), new_type); + expr new_meta = g.mk_meta(mk_fresh_name(), new_type); new_goals.push_back(goal(new_meta, new_type)); fn_pr = new_meta; } @@ -260,7 +260,7 @@ tactic congruence_tactic() { pr = mk_app(pr, mk_refl(*tc, lhs_args[i])); } else { expr new_type = mk_eq(*tc, lhs_args[i], rhs_args[i]); - expr new_meta = g.mk_meta(ngen.next(), new_type); + expr new_meta = g.mk_meta(mk_fresh_name(), new_type); new_goals.push_back(goal(new_meta, new_type)); pr = mk_app(pr, mk_symm(*tc, new_meta)); } @@ -274,7 +274,7 @@ tactic congruence_tactic() { } assign(subst, g, pr); - proof_state new_ps(s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), subst, ngen); + proof_state new_ps(s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), subst); if (solve_constraints(env, ios, new_ps, cs)) return some_proof_state(new_ps); return none_proof_state(); diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp index a9a4d60e0..ed35ec7d4 100644 --- a/src/library/tactic/constructor_tactic.cpp +++ b/src/library/tactic/constructor_tactic.cpp @@ -31,8 +31,7 @@ tactic constructor_tactic(elaborate_fn const & elab, optional _i, opti return proof_state_seq(); } constraint_seq cs; - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); goal const & g = head(gs); expr t = tc->whnf(g.get_type(), cs); buffer I_args; @@ -59,7 +58,7 @@ tactic constructor_tactic(elaborate_fn const & elab, optional _i, opti unsigned num_params = *inductive::get_num_params(env, const_name(I)); if (I_args.size() < num_params) return proof_state_seq(); - proof_state new_s(s, ngen); + proof_state new_s(s); C = mk_app(C, num_params, I_args.data()); expr C_type = tc->whnf(tc->infer(C, cs), cs); bool report_unassigned = true; diff --git a/src/library/tactic/contradiction_tactic.cpp b/src/library/tactic/contradiction_tactic.cpp index 024405bf8..1ae70abe5 100644 --- a/src/library/tactic/contradiction_tactic.cpp +++ b/src/library/tactic/contradiction_tactic.cpp @@ -23,9 +23,8 @@ tactic contradiction_tactic() { goal const & g = head(gs); expr const & t = g.get_type(); substitution subst = s.get_subst(); - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); - auto conserv_tc = mk_type_checker(env, ngen.mk_child(), UnfoldReducible); + auto tc = mk_type_checker(env); + auto conserv_tc = mk_type_checker(env, UnfoldReducible); buffer hyps; g.get_hyps(hyps); for (expr const & h : hyps) { @@ -34,7 +33,7 @@ tactic contradiction_tactic() { expr lhs, rhs, arg; if (is_false(env, h_type)) { assign(subst, g, mk_false_rec(*tc, h, t)); - return some_proof_state(proof_state(s, tail(gs), subst, ngen)); + return some_proof_state(proof_state(s, tail(gs), subst)); } else if (is_not(env, h_type, arg)) { optional h_pos; for (expr const & h_prime : hyps) { @@ -46,7 +45,7 @@ tactic contradiction_tactic() { } if (h_pos) { assign(subst, g, mk_absurd(*tc, t, *h_pos, h)); - return some_proof_state(proof_state(s, tail(gs), subst, ngen)); + return some_proof_state(proof_state(s, tail(gs), subst)); } } else if (is_eq(h_type, lhs, rhs)) { lhs = tc->whnf(lhs).first; @@ -67,7 +66,7 @@ tactic contradiction_tactic() { if (auto r = lift_down_if_hott(*tc, V)) { check_term(*tc, *r); assign(subst, g, *r); - return some_proof_state(proof_state(s, tail(gs), subst, ngen)); + return some_proof_state(proof_state(s, tail(gs), subst)); } } } catch (kernel_exception & ex) { diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 3b0d69b4a..35e8fae42 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -17,13 +17,12 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat buffer cs_buffer; cs.linearize(cs_buffer); to_buffer(ps.get_postponed(), cs_buffer); - name_generator ngen = ps.get_ngen(); substitution subst = ps.get_subst(); - unify_result_seq rseq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen.mk_child(), subst, cfg); + unify_result_seq rseq = unify(env, cs_buffer.size(), cs_buffer.data(), subst, cfg); if (auto p = rseq.pull()) { substitution new_subst = p->first.first; constraints new_postponed = p->first.second; - ps = proof_state(ps, ps.get_goals(), new_subst, ngen, new_postponed); + ps = proof_state(ps, ps.get_goals(), new_subst, new_postponed); return true; } else { return false; @@ -34,7 +33,6 @@ optional elaborate_with_respect_to(environment const & env, io_state const proof_state & s, expr const & e, optional const & _expected_type, bool report_unassigned, bool enforce_type_during_elaboration, bool conservative) { - name_generator ngen = s.get_ngen(); substitution subst = s.get_subst(); goals const & gs = s.get_goals(); optional expected_type = _expected_type; @@ -45,19 +43,19 @@ optional elaborate_with_respect_to(environment const & env, io_state const optional elab_expected_type; if (enforce_type_during_elaboration) elab_expected_type = expected_type; - auto esc = elab(head(gs), ios.get_options(), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned); + auto esc = elab(head(gs), ios.get_options(), e, elab_expected_type, subst, report_unassigned); expr new_e; substitution new_subst; constraints cs_; std::tie(new_e, new_subst, cs_) = esc; buffer cs; to_buffer(cs_, cs); if (cs.empty() && (!expected_type || enforce_type_during_elaboration)) { // easy case: no constraints to be solved - s = proof_state(s, new_subst, ngen); + s = proof_state(s, new_subst); return some_expr(new_e); } else { to_buffer(s.get_postponed(), cs); if (expected_type) { - auto tc = mk_type_checker(env, ngen.mk_child(), conservative ? UnfoldReducible : UnfoldSemireducible); + auto tc = mk_type_checker(env, conservative ? UnfoldReducible : UnfoldSemireducible); auto e_t_cs = tc->infer(new_e); expr t = *expected_type; e_t_cs.second.linearize(cs); @@ -77,12 +75,12 @@ optional elaborate_with_respect_to(environment const & env, io_state const d_cs.second.linearize(cs); } unifier_config cfg(ios.get_options()); - unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), new_subst, cfg); + unify_result_seq rseq = unify(env, cs.size(), cs.data(), new_subst, cfg); if (auto p = rseq.pull()) { substitution new_subst = p->first.first; constraints new_postponed = p->first.second; new_e = new_subst.instantiate(new_e); - s = proof_state(s, gs, new_subst, ngen, new_postponed); + s = proof_state(s, gs, new_subst, new_postponed); return some_expr(new_e); } else { return none_expr(); diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index d47b06f25..d1b35ef74 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/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 67e2a56c0..316664569 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -63,8 +63,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type assign(subst, g, *new_e); if (allow_metavars) { buffer new_goals; - name_generator ngen = new_s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); for_each(*new_e, [&](expr const & m, unsigned) { if (!has_expr_metavar(m)) return false; @@ -75,7 +74,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type return !is_metavar(m) && !is_local(m); }); goals new_gs = to_list(new_goals.begin(), new_goals.end(), tail(gs)); - return some(proof_state(new_s, new_gs, subst, ngen)); + return some(proof_state(new_s, new_gs, subst)); } else { return some(proof_state(new_s, tail(gs), subst)); } @@ -99,7 +98,7 @@ static tactic assumption_tactic_core(bool conservative) { goal g = head(gs); buffer hs; g.get_hyps(hs); - auto elab = [](goal const &, options const &, name_generator const &, expr const & H, + auto elab = [](goal const &, options const &, expr const & H, optional const &, substitution const & s, bool) -> elaborate_result { return elaborate_result(H, s, constraints()); }; diff --git a/src/library/tactic/exfalso_tactic.cpp b/src/library/tactic/exfalso_tactic.cpp index f192183f2..786bebd03 100644 --- a/src/library/tactic/exfalso_tactic.cpp +++ b/src/library/tactic/exfalso_tactic.cpp @@ -23,13 +23,12 @@ tactic exfalso_tactic() { goal const & g = head(gs); expr const & t = g.get_type(); substitution subst = s.get_subst(); - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); expr false_expr = mk_false(env); - expr new_meta = g.mk_meta(ngen.next(), false_expr); + expr new_meta = g.mk_meta(mk_fresh_name(), false_expr); goal new_goal(new_meta, false_expr); assign(subst, g, mk_false_rec(*tc, new_meta, t)); - return some(proof_state(s, goals(new_goal, tail(gs)), subst, ngen)); + return some(proof_state(s, goals(new_goal, tail(gs)), subst)); }; return tactic01(fn); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 0e7cdd081..2c2fc796a 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -226,9 +226,8 @@ tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_in throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); if (num_ls < num_ps) { buffer extra_ls; - name_generator ngen = tc.mk_ngen(); for (unsigned i = num_ls; i < num_ps; i++) - extra_ls.push_back(mk_meta_univ(ngen.next())); + extra_ls.push_back(mk_meta_univ(mk_fresh_name())); ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); } v = instantiate_univ_params(v, ps, ls); @@ -237,14 +236,6 @@ tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_in } } -static name * g_tmp_prefix = nullptr; -LEAN_THREAD_VALUE(unsigned, g_expr_tac_id, 0); -static name_generator next_name_generator() { - unsigned r = g_expr_tac_id; - g_expr_tac_id++; - return name_generator(name(*g_tmp_prefix, r)); -} - unsigned get_unsigned(type_checker & tc, expr const & e, expr const & ref) { optional k = to_num(e); if (!k) @@ -295,7 +286,7 @@ public: tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { bool memoize = false; - type_checker tc(env, next_name_generator(), std::unique_ptr(new tac_builtin_opaque_converter(env)), memoize); + type_checker tc(env, std::unique_ptr(new tac_builtin_opaque_converter(env)), memoize); return expr_to_tactic(tc, fn, e, p); } @@ -368,8 +359,6 @@ bool is_by_plus(expr const & e) { return is_annotation(e, *g_by_plus_name); } expr const & get_by_plus_arg(expr const & e) { lean_assert(is_by_plus(e)); return get_annotation_arg(e); } void initialize_expr_to_tactic() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_by_name = new name("by"); register_annotation(*g_by_name); @@ -473,6 +462,5 @@ void finalize_expr_to_tactic() { delete g_tactic_opcode; delete g_by_name; delete g_by_plus_name; - delete g_tmp_prefix; } } diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index 2a2e3e11c..777db9327 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -24,11 +24,10 @@ optional generalize_core(environment const & env, io_state const & bool intro) { proof_state new_s = s; if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) { - name_generator ngen = new_s.get_ngen(); substitution subst = new_s.get_subst(); goals const & gs = new_s.get_goals(); goal const & g = head(gs); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); auto e_t_cs = tc->infer(*new_e); if (e_t_cs.second) { throw_tactic_exception_if_enabled(s, sstream() << "invalid '" << tac_name << "' tactic, unification constraints " @@ -49,17 +48,17 @@ optional generalize_core(environment const & env, io_state const & if (intro) { buffer hyps; g.get_hyps(hyps); - expr new_h = mk_local(ngen.next(), get_unused_name(x, hyps), e_t, binder_info()); + expr new_h = mk_local(mk_fresh_name(), get_unused_name(x, hyps), e_t, binder_info()); new_t = instantiate(abstract(t, *new_e), new_h); to_check = Pi(new_h, new_t); - new_m = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t))); + new_m = mk_metavar(mk_fresh_name(), Pi(hyps, Pi(new_h, new_t))); new_m = mk_app(new_m, hyps); new_val = mk_app(new_m, *new_e); new_m = mk_app(new_m, new_h); } else { new_t = mk_pi(n, e_t, abstract(t, *new_e)); to_check = new_t; - new_m = g.mk_meta(ngen.next(), new_t); + new_m = g.mk_meta(mk_fresh_name(), new_t); new_val = mk_app(new_m, *new_e); } try { @@ -76,7 +75,7 @@ optional generalize_core(environment const & env, io_state const & } assign(subst, g, new_val); goal new_g(new_m, new_t); - return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen)); + return some(proof_state(new_s, goals(new_g, tail(gs)), subst)); } return none_proof_state(); } diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 995f4b820..3001989ef 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -26,7 +26,6 @@ class induction_tac { name m_h_name; optional m_rec_name; list m_ids; - name_generator m_ngen; substitution m_subst; bool m_throw_ex; bool m_standard; @@ -67,7 +66,7 @@ class induction_tac { bool is_strict = false; local_context ctx = g.to_local_context(); auto mc = mk_class_instance_elaborator( - m_env, m_ios, ctx, m_ngen.next(), optional(), + m_env, m_ios, ctx, optional(), use_local_insts, is_strict, some_expr(type), m_ref.get_tag(), nullptr); m_cs += mc.second; @@ -171,7 +170,7 @@ class induction_tac { } else { arg_name = binding_name(new_type); } - expr new_h = mk_local(m_ngen.next(), get_unused_name(arg_name, new_goal_hyps), + expr new_h = mk_local(mk_fresh_name(), get_unused_name(arg_name, new_goal_hyps), arg_type, binder_info()); minor_args.push_back(new_h); new_goal_hyps.push_back(new_h); @@ -186,14 +185,15 @@ class induction_tac { throw_ill_formed_recursor(rec_info); } expr dep_type = binding_domain(new_type); - expr new_dep = mk_local(m_ngen.next(), get_unused_name(binding_name(new_type), new_goal_hyps), + expr new_dep = mk_local(mk_fresh_name(), + get_unused_name(binding_name(new_type), new_goal_hyps), dep_type, binder_info()); new_deps.push_back(new_dep); new_goal_hyps.push_back(new_dep); new_type = instantiate(binding_body(new_type), new_dep); } } - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_goal_hyps, new_type)), new_goal_hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_goal_hyps, new_type)), new_goal_hyps); goal new_g(new_meta, new_type); new_goals.push_back(new_g); rec_arg = Fun(minor_args, Fun(new_deps, new_meta)); @@ -270,7 +270,7 @@ class induction_tac { buffer & new_hyps = non_deps; new_hyps.push_back(h); expr new_type = Pi(deps, g.get_type()); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps); goal new_g(new_meta, new_type); expr val = mk_app(new_meta, deps); assign(g, val); @@ -281,17 +281,15 @@ class induction_tac { } public: - induction_tac(environment const & env, io_state const & ios, name_generator const & ngen, + induction_tac(environment const & env, io_state const & ios, type_checker & tc, substitution const & subst, name const & h_name, optional const & rec_name, list const & ids, bool throw_ex, expr const & ref): m_env(env), m_ios(ios), m_tc(tc), m_h_name(h_name), m_rec_name(rec_name), m_ids(ids), - m_ngen(ngen), m_subst(subst), m_throw_ex(throw_ex), m_ref(ref) { + m_subst(subst), m_throw_ex(throw_ex), m_ref(ref) { m_standard = is_standard(env); } - name_generator const & get_ngen() const { return m_ngen; } - substitution const & get_subst() const { return m_subst; } constraint_seq get_new_constraints() const { return m_cs; } @@ -302,11 +300,11 @@ public: if (m_rec_name) { recursor_info info = get_recursor_info(m_env, *m_rec_name); name tname = info.get_type_name(); - type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { return n == tname; }); + type_checker_ptr aux_tc = mk_type_checker(m_env, [=](name const & n) { return n == tname; }); return aux_tc->whnf(H_type).first; } else { has_recursors_pred pred(m_env); - type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), pred); + type_checker_ptr aux_tc = mk_type_checker(m_env, pred); return aux_tc->whnf(H_type).first; } } @@ -369,11 +367,10 @@ tactic induction_tactic(name const & H, optional rec, list const & i } goal g = head(gs); goals tail_gs = tail(gs); - name_generator ngen = ps.get_ngen(); - std::unique_ptr tc = mk_type_checker(env, ngen.mk_child()); - induction_tac tac(env, ios, ngen, *tc, ps.get_subst(), H, rec, ids, ps.report_failure(), ref); + std::unique_ptr tc = mk_type_checker(env); + induction_tac tac(env, ios, *tc, ps.get_subst(), H, rec, ids, ps.report_failure(), ref); if (auto res = tac.execute(g)) { - proof_state new_s(ps, append(*res, tail_gs), tac.get_subst(), tac.get_ngen()); + proof_state new_s(ps, append(*res, tail_gs), tac.get_subst()); if (solve_constraints(env, ios, new_s, tac.get_new_constraints())) return some_proof_state(new_s); else diff --git a/src/library/tactic/injection_tactic.cpp b/src/library/tactic/injection_tactic.cpp index a7e7c5c00..6a5137e59 100644 --- a/src/library/tactic/injection_tactic.cpp +++ b/src/library/tactic/injection_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/inductive/inductive.h" @@ -49,8 +50,7 @@ tactic intros_num_tactic(unsigned num, list _ns) { if (empty(gs)) return proof_state_seq(); goal const & g = head(gs); - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); expr t = g.get_type(); expr m = g.get_meta(); @@ -68,16 +68,16 @@ tactic intros_num_tactic(unsigned num, list _ns) { expr H = mk_local(mk_name(binding_name(t)), binding_domain(t)); t = instantiate(binding_body(t), H); m = mk_app(m, H); - proof_state new_s(s, cons(goal(m, t), tail(gs)), ngen); + proof_state new_s(s, cons(goal(m, t), tail(gs))); return intros_num_tactic(num-1, ns)(env, ios, new_s); }; auto discard_hyp = [&]() { - expr new_meta = g.mk_meta(ngen.next(), binding_body(t)); + expr new_meta = g.mk_meta(mk_fresh_name(), binding_body(t)); goal new_goal(new_meta, binding_body(t)); substitution new_subst = s.get_subst(); assign(new_subst, g, mk_lambda(binding_name(t), binding_domain(t), new_meta)); - proof_state new_s(s, cons(new_goal, tail(gs)), new_subst, ngen); + proof_state new_s(s, cons(new_goal, tail(gs)), new_subst); return intros_num_tactic(num-1, ns)(env, ios, new_s); }; @@ -101,11 +101,11 @@ tactic intros_num_tactic(unsigned num, list _ns) { return discard_hyp(); } else if (is_injection_target(*tc, lhs, rhs)) { // apply injection recursively - name Hname = ngen.next(); + name Hname = mk_fresh_name(); expr H = mk_local(Hname, binding_domain(t)); t = binding_body(t); m = mk_app(m, H); - proof_state new_s(s, cons(goal(m, t), tail(gs)), ngen); + proof_state new_s(s, cons(goal(m, t), tail(gs))); return then(injection_tactic_core(H, num-1, ns, false), clear_tactic(Hname))(env, ios, new_s); } else { @@ -119,15 +119,15 @@ tactic intros_num_tactic(unsigned num, list _ns) { // since types A and B are definitionally equal, we convert to homogeneous expr new_eq = mk_eq(*tc, lhs, rhs); expr new_type = mk_pi(binding_name(t), new_eq, binding_body(t)); - expr new_meta = g.mk_meta(ngen.next(), new_type); + expr new_meta = g.mk_meta(mk_fresh_name(), new_type); goal new_goal(new_meta, new_type); - expr H = mk_local(ngen.next(), binding_domain(t)); + expr H = mk_local(mk_fresh_name(), binding_domain(t)); levels heq_lvl = const_levels(get_app_fn(Htype)); expr arg = mk_app(mk_constant(get_eq_of_heq_name(), heq_lvl), A, lhs, rhs, H); expr V = Fun(H, mk_app(new_meta, arg)); substitution new_subst = s.get_subst(); assign(new_subst, g, V); - proof_state new_s(s, cons(new_goal, tail(gs)), new_subst, ngen); + proof_state new_s(s, cons(new_goal, tail(gs)), new_subst); return intros_num_tactic(num, ns)(env, ios, new_s); } else { return keep_hyp(); @@ -149,8 +149,7 @@ tactic injection_tactic_core(expr const & e, unsigned num, list const & id } expr t = head(gs).get_type(); constraint_seq cs; - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); expr e_type = tc->whnf(tc->infer(e, cs), cs); expr lhs, rhs; if (!is_eq(e_type, lhs, rhs)) { @@ -193,13 +192,13 @@ tactic injection_tactic_core(expr const & e, unsigned num, list const & id level t_lvl = sort_level(tc->ensure_type(t, cs)); expr N = mk_constant(name(const_name(I), "no_confusion"), cons(t_lvl, const_levels(I))); N = mk_app(mk_app(N, I_args), t, lhs, rhs, e); - proof_state new_s(s, ngen); + proof_state new_s(s); if (is_standard(env)) { tactic tac = then(take(apply_tactic_core(N, cs), 1), intros_num_tactic(num + num_new_eqs, ids)); return tac(env, ios, new_s); } else { - level n_lvl = mk_meta_univ(tc->mk_fresh_name()); + level n_lvl = mk_meta_univ(mk_fresh_name()); expr lift_down = mk_app(mk_constant(get_lift_down_name(), {t_lvl, n_lvl}), t); tactic tac = then(take(apply_tactic_core(lift_down), 1), then(take(apply_tactic_core(N, cs), 1), diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp index 508be684a..8021ed43f 100644 --- a/src/library/tactic/intros_tactic.cpp +++ b/src/library/tactic/intros_tactic.cpp @@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/constants.h" +#include "util/fresh_name.h" #include "kernel/instantiate.h" +#include "library/constants.h" #include "library/reducible.h" #include "library/tactic/intros_tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -20,8 +21,7 @@ static tactic intro_intros_tactic(list _ns, bool is_intros) { return optional(); } goal const & g = head(gs); - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); expr t = g.get_type(); expr m = g.get_meta(); bool gen_names = is_intros && empty(ns); @@ -50,13 +50,13 @@ static tactic intro_intros_tactic(list _ns, bool is_intros) { } else { new_name = get_unused_name(binding_name(t), m); } - expr new_local = mk_local(ngen.next(), new_name, binding_domain(t), binding_info(t)); + expr new_local = mk_local(mk_fresh_name(), new_name, binding_domain(t), binding_info(t)); t = instantiate(binding_body(t), new_local); m = mk_app(m, new_local); first = false; } goal new_g(m, t); - return some(proof_state(s, goals(new_g, tail(gs)), ngen)); + return some(proof_state(s, goals(new_g, tail(gs)))); } catch (exception &) { return optional(); } diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index def28e2bb..8f7a1f419 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" @@ -25,9 +26,9 @@ Author: Leonardo de Moura namespace lean { namespace inversion { result::result(list const & gs, list> const & args, list const & imps, - list const & rs, name_generator const & ngen, substitution const & subst): + list const & rs, substitution const & subst): m_goals(gs), m_args(args), m_implementation_lists(imps), - m_renames(rs), m_ngen(ngen), m_subst(subst) { + m_renames(rs), m_subst(subst) { lean_assert_eq(length(m_goals), length(m_args)); lean_assert_eq(length(m_goals), length(m_implementation_lists)); lean_assert_eq(length(m_goals), length(m_renames)); @@ -64,7 +65,7 @@ optional apply_eq_rec_eq(type_checker & tc, io_state const & ios, list m_ids; - name_generator m_ngen; substitution m_subst; bool m_dep_elim; @@ -269,12 +269,12 @@ class inversion_tac { pair p = mk_eq(lhs, rhs); expr new_eq = p.first; expr new_refl = p.second; - eqs.push_back(mk_local(m_ngen.next(), g.get_unused_name(eq_prefix, eq_idx), new_eq, binder_info())); + eqs.push_back(mk_local(mk_fresh_name(), g.get_unused_name(eq_prefix, eq_idx), new_eq, binder_info())); refls.push_back(new_refl); }; for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) { expr t_type = binding_domain(d); - expr t = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); + expr t = mk_local(mk_fresh_name(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); expr const & index = I_args[i]; add_eq(index, t); h_new_type = mk_app(h_new_type, t); @@ -282,12 +282,12 @@ class inversion_tac { ts.push_back(t); d = instantiate(binding_body(d), t); } - expr h_new = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h)); + expr h_new = mk_local(mk_fresh_name(), h_new_name, h_new_type, local_info(h)); if (m_dep_elim) add_eq(h, h_new); hyps.push_back(h_new); expr new_type = Pi(eqs, g.get_type()); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); expr val = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), refls); @@ -300,7 +300,7 @@ class inversion_tac { buffer refls; for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) { expr t_type = binding_domain(d); - expr t = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); + expr t = mk_local(mk_fresh_name(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); h_new_type = mk_app(h_new_type, t); ss.push_back(I_args[i]); refls.push_back(mk_refl(m_tc, I_args[i])); @@ -308,7 +308,7 @@ class inversion_tac { ts.push_back(t); d = instantiate(binding_body(d), t); } - expr h_new = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h)); + expr h_new = mk_local(mk_fresh_name(), h_new_name, h_new_type, local_info(h)); ts.push_back(h_new); ss.push_back(h); refls.push_back(mk_refl(m_tc, h)); @@ -317,7 +317,7 @@ class inversion_tac { mk_telescopic_eq(m_tc, ss, ts, eqs); ts.pop_back(); expr new_type = Pi(eqs, g.get_type()); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); expr val = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), refls); @@ -341,7 +341,7 @@ class inversion_tac { buffer & new_hyps = non_deps; new_hyps.push_back(h); expr new_type = Pi(deps, g.get_type()); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps); goal new_g(new_meta, new_type); expr val = mk_app(new_meta, deps); assign(g, val); @@ -421,7 +421,7 @@ class inversion_tac { buffer new_imps; for (unsigned i = 0; i < m_nminors; i++) { expr new_type = binding_domain(cases_on_type); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps); goal new_g(new_meta, new_type); new_goals.push_back(new_g); cases_on = mk_app(cases_on, new_meta); @@ -482,14 +482,14 @@ class inversion_tac { } else { new_h_name = binding_name(g_type); } - expr new_h = mk_local(m_ngen.next(), get_unused_name(new_h_name, new_hyps), type, binder_info()); + expr new_h = mk_local(mk_fresh_name(), get_unused_name(new_h_name, new_hyps), type, binder_info()); curr_new_args.push_back(new_h); new_hyps.push_back(new_h); g_type = instantiate(binding_body(g_type), new_h); } new_args.push_back(to_list(curr_new_args)); g_type = head_beta_reduce(g_type); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, g_type)), new_hyps); goal new_g(new_meta, g_type); new_gs.push_back(new_g); expr val = Fun(nargs, new_hyps.end() - nargs, new_meta); @@ -564,13 +564,13 @@ class inversion_tac { expr const & reduced_lhs = lhs_args[3]; expr new_eq = ::lean::mk_eq(m_tc, reduced_lhs, rhs); expr new_type = update_binding(type, new_eq, binding_body(type)); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); // create assignment for g expr A = infer_type(lhs); level lvl = sort_level(m_tc.ensure_type(A).first); // old_eq : eq.rec A s C a s p = b - expr old_eq = mk_local(m_ngen.next(), binding_name(type), eq, binder_info()); + expr old_eq = mk_local(mk_fresh_name(), binding_name(type), eq, binder_info()); // aux_eq : a = eq.rec A s C a s p expr trans_eq = mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, reduced_lhs, lhs, rhs, *aux_eq, old_eq}); // trans_eq : a = b @@ -597,14 +597,14 @@ class inversion_tac { buffer hyps; g.get_hyps(hyps); expr new_eq = mk_app(mk_constant(get_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3]); - expr new_hyp = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), new_eq, binder_info()); + expr new_hyp = mk_local(mk_fresh_name(), g.get_unused_name(binding_name(type)), new_eq, binder_info()); expr new_type = instantiate(binding_body(type), new_hyp); hyps.push_back(new_hyp); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); expr new_meta = mk_app(new_mvar, hyps); goal new_g(new_meta, new_type); hyps.pop_back(); - expr H = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); + expr H = mk_local(mk_fresh_name(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); expr to_eq = mk_app(mk_constant(get_eq_of_heq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H); expr val = Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq)); assign(g, val); @@ -629,10 +629,10 @@ class inversion_tac { lean_assert(const_name(get_app_fn(eq)) == get_eq_name()); buffer hyps; g.get_hyps(hyps); - expr new_hyp = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); + expr new_hyp = mk_local(mk_fresh_name(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); expr new_type = instantiate(binding_body(type), new_hyp); hyps.push_back(new_hyp); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); expr val = Fun(new_hyp, new_meta); assign(g, val); @@ -732,7 +732,7 @@ class inversion_tac { // deletion transition: t == t hyps.pop_back(); // remove t == t equality expr new_type = g.get_type(); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); assign(g, new_meta); return unify_eqs(new_g, neqs-1); @@ -763,7 +763,7 @@ class inversion_tac { expr new_type = binding_domain(whnf(infer_type(no_confusion))); if (m_proof_irrel || !depends_on(g_type, hyps.back())) hyps.pop_back(); // remove processed equality - expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); expr new_meta = mk_app(new_mvar, hyps); goal new_g(new_meta, new_type); expr val = lift_down(mk_app(no_confusion, new_meta)); @@ -807,7 +807,7 @@ class inversion_tac { // eq.rec is not necessary buffer & new_hyps = non_deps; expr new_type = g_type; - expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); assign(g, new_meta); @@ -843,7 +843,7 @@ class inversion_tac { } buffer new_deps; for (unsigned i = 0; i < deps.size(); i++) { - expr new_hyp = mk_local(m_ngen.next(), binding_name(new_type), binding_domain(new_type), + expr new_hyp = mk_local(mk_fresh_name(), binding_name(new_type), binding_domain(new_type), binding_info(new_type)); new_hyps.push_back(new_hyp); new_deps.push_back(new_hyp); @@ -852,7 +852,7 @@ class inversion_tac { replace(m_imps, deps, new_deps); lean_assert(deps.size() == new_deps.size()); store_renames(deps, new_deps); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); expr eq_rec_minor = mk_app(new_mvar, non_deps); @@ -867,7 +867,7 @@ class inversion_tac { hyps.pop_back(); // remove processed equality if (!depends_on(g_type, Heq)) { expr new_type = mk_arrow(symm_eq, g_type); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); expr new_meta = mk_app(new_mvar, hyps); goal new_g(new_meta, new_type); expr Heq_inv = mk_symm(m_tc, Heq); @@ -879,7 +879,7 @@ class inversion_tac { expr new_Heq = update_mlocal(Heq, symm_eq); expr new_Heq_inv = mk_symm(m_tc, new_Heq); expr new_type = Pi(new_Heq, instantiate(abstract_local(g_type, Heq), new_Heq_inv)); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); expr new_meta = mk_app(new_mvar, hyps); goal new_g(new_meta, new_type); // Then, we have @@ -938,12 +938,12 @@ class inversion_tac { expr g_type = g.get_type(); for (expr const & d : deps) { expr type = binding_domain(g_type); - expr new_d = mk_local(m_ngen.next(), get_unused_name(local_pp_name(d), new_hyps), type, local_info(d)); + expr new_d = mk_local(mk_fresh_name(), get_unused_name(local_pp_name(d), new_hyps), type, local_info(d)); rs.insert(mlocal_name(d), mlocal_name(new_d)); new_hyps.push_back(new_d); g_type = instantiate(binding_body(g_type), new_d); } - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, g_type)), new_hyps); goal new_g(new_meta, g_type); unsigned ndeps = deps.size(); expr val = Fun(ndeps, new_hyps.end() - ndeps, new_meta); @@ -973,7 +973,7 @@ class inversion_tac { return g; // other hypotheses or result type depend on h } expr new_type = g.get_type(); - expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); assign(g, new_meta); return new_g; @@ -1022,17 +1022,17 @@ class inversion_tac { } public: - inversion_tac(environment const & env, io_state const & ios, name_generator const & ngen, + inversion_tac(environment const & env, io_state const & ios, type_checker & tc, substitution const & subst, list const & ids, bool throw_tactic_ex, bool clear_elim): m_env(env), m_ios(ios), m_tc(tc), m_ids(ids), - m_ngen(ngen), m_subst(subst), m_throw_tactic_exception(throw_tactic_ex), + m_subst(subst), m_throw_tactic_exception(throw_tactic_ex), m_clear_elim(clear_elim) { m_proof_irrel = m_env.prop_proof_irrel(); } inversion_tac(environment const & env, io_state const & ios, type_checker & tc, bool clear_elim): - inversion_tac(env, ios, tc.mk_ngen(), tc, substitution(), list(), false, clear_elim) {} + inversion_tac(env, ios, tc, substitution(), list(), false, clear_elim) {} typedef inversion::result result; @@ -1053,7 +1053,7 @@ public: auto gs_rs_pair = intro_deps(gs3, deps); list gs4 = gs_rs_pair.first; list rs = gs_rs_pair.second; - return optional(result(gs4, args, new_imps, rs, m_ngen, m_subst)); + return optional(result(gs4, args, new_imps, rs, m_subst)); } else { goal g1 = generalize_indices(g, h, h_type); auto gs_imps_pair = apply_cases_on(g1, imps, false); @@ -1066,7 +1066,7 @@ public: list rs; std::tie(gs4, args, new_imps, rs) = unify_eqs(gs3, args, new_imps); gs4 = clear_hypothesis(gs4, rs, mlocal_name(h), h_type); - return optional(result(gs4, args, new_imps, rs, m_ngen, m_subst)); + return optional(result(gs4, args, new_imps, rs, m_subst)); } } catch (inversion_exception & ex) { return optional(); @@ -1099,12 +1099,11 @@ tactic inversion_tactic(name const & n, list const & ids) { return none_proof_state(); goal g = head(gs); goals tail_gs = tail(gs); - name_generator ngen = ps.get_ngen(); - std::unique_ptr tc = mk_type_checker(env, ngen.mk_child()); + std::unique_ptr tc = mk_type_checker(env); bool clear_elim = true; - inversion_tac tac(env, ios, ngen, *tc, ps.get_subst(), ids, ps.report_failure(), clear_elim); + inversion_tac tac(env, ios, *tc, ps.get_subst(), ids, ps.report_failure(), clear_elim); if (auto res = tac.execute(g, n, implementation_list())) { - proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst, res->m_ngen); + proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst); return some_proof_state(new_s); } else { return none_proof_state(); diff --git a/src/library/tactic/inversion_tactic.h b/src/library/tactic/inversion_tactic.h index 9939dabff..1a086de9e 100644 --- a/src/library/tactic/inversion_tactic.h +++ b/src/library/tactic/inversion_tactic.h @@ -50,10 +50,9 @@ struct result { // invariant: length(m_goals) == length(m_args); // invariant: length(m_goals) == length(m_implementation_lists); // invariant: length(m_goals) == length(m_renames); - name_generator m_ngen; substitution m_subst; result(list const & gs, list> const & args, list const & imps, - list const & rs, name_generator const & ngen, substitution const & subst); + list const & rs, substitution const & subst); }; optional apply(environment const & env, io_state const & ios, type_checker & tc, diff --git a/src/library/tactic/note_tactic.cpp b/src/library/tactic/note_tactic.cpp index 550426a07..a1f9e0e88 100644 --- a/src/library/tactic/note_tactic.cpp +++ b/src/library/tactic/note_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "library/constants.h" #include "library/reducible.h" @@ -27,26 +28,25 @@ tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) { return none_proof_state(); } goal const & g = head(gs); - name_generator ngen = s.get_ngen(); bool report_unassigned = true; - elaborate_result esc = elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned); + elaborate_result esc = elab(g, ios.get_options(), e, none_expr(), new_s.get_subst(), report_unassigned); expr new_e; substitution new_subst; constraints cs; std::tie(new_e, new_subst, cs) = esc; if (cs) throw_tactic_exception_if_enabled(s, "invalid 'note' tactic, fail to resolve generated constraints"); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); expr new_e_type = tc->infer(new_e).first; - expr new_local = mk_local(ngen.next(), id, new_e_type, binder_info()); + expr new_local = mk_local(mk_fresh_name(), id, new_e_type, binder_info()); buffer hyps; g.get_hyps(hyps); hyps.push_back(new_local); - expr new_mvar = mk_metavar(ngen.next(), Pi(hyps, g.get_type())); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type())); hyps.pop_back(); expr new_meta_core = mk_app(new_mvar, hyps); expr new_meta = mk_app(new_meta_core, new_local); goal new_goal(new_meta, g.get_type()); assign(new_subst, g, mk_app(new_meta_core, new_e)); - return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst, ngen)); + return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst)); }); } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 265a470ae..dcd8ada38 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -29,9 +29,9 @@ bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); } -proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen, +proof_state::proof_state(goals const & gs, substitution const & s, constraints const & postponed, bool report_failure): - m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), + m_goals(gs), m_subst(s), m_postponed(postponed), m_report_failure(report_failure) { if (std::any_of(gs.begin(), gs.end(), [&](goal const & g) { return s.is_assigned(g.get_mvar()); })) { @@ -80,12 +80,12 @@ goals map_goals(proof_state const & s, std::function(goal const & }); } -proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen) { - return proof_state(goals(goal(meta, type)), subst, ngen, constraints()); +proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst) { + return proof_state(goals(goal(meta, type)), subst, constraints()); } -proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) { - return to_proof_state(meta, type, substitution(), ngen); +proof_state to_proof_state(expr const & meta, expr const & type) { + return to_proof_state(meta, type, substitution()); } proof_state apply_substitution(proof_state const & s) { diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 788d655bb..328be8639 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -18,45 +18,37 @@ typedef list goals; class proof_state { goals m_goals; substitution m_subst; - name_generator m_ngen; constraints m_postponed; bool m_report_failure; format pp_core(std::function const & mk_fmt, options const & opts) const; public: - proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed, + proof_state(goals const & gs, substitution const & s, constraints const & postponed, bool report_failure = true); - proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen, + proof_state(proof_state const & s, goals const & gs, substitution const & subst, constraints const & postponed): - proof_state(gs, subst, ngen, postponed, s.report_failure()) {} - proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen): - proof_state(gs, subst, ngen, s.m_postponed, s.report_failure()) {} + proof_state(gs, subst, postponed, s.report_failure()) {} proof_state(proof_state const & s, goals const & gs, substitution const & subst): - proof_state(s, gs, subst, s.m_ngen) {} - proof_state(proof_state const & s, goals const & gs, name_generator const & ngen): - proof_state(s, gs, s.m_subst, ngen) {} + proof_state(gs, subst, s.m_postponed, s.report_failure()) {} proof_state(proof_state const & s, goals const & gs): proof_state(s, gs, s.m_subst) {} - proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen, + proof_state(proof_state const & s, substitution const & subst, constraints const & postponed): - proof_state(s.m_goals, subst, ngen, postponed, s.report_failure()) {} - proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed): - proof_state(s, s.m_goals, s.m_subst, ngen, postponed) {} - proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen): - proof_state(s, s.m_goals, subst, ngen, s.m_postponed) {} - proof_state(proof_state const & s, name_generator const & ngen): - proof_state(s, ngen, s.m_postponed) {} + proof_state(s.m_goals, subst, postponed, s.report_failure()) {} + proof_state(proof_state const & s, constraints const & postponed): + proof_state(s, s.m_goals, s.m_subst, postponed) {} proof_state(proof_state const & s, substitution const & subst): - proof_state(s, subst, s.m_ngen) {} + proof_state(s, s.m_goals, subst, s.m_postponed) {} + proof_state(proof_state const & s): + proof_state(s, s.m_postponed) {} proof_state update_report_failure(bool f) const { - return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, f); + return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_postponed, f); } goals const & get_goals() const { return m_goals; } substitution const & get_subst() const { return m_subst; } - name_generator const & get_ngen() const { return m_ngen; } constraints const & get_postponed() const { return m_postponed; } bool report_failure() const { return m_report_failure; } @@ -78,8 +70,8 @@ proof_state apply_substitution(proof_state const & s); inline optional some_proof_state(proof_state const & s) { return some(s); } inline optional none_proof_state() { return optional (); } -proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen); -proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen); +proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst); +proof_state to_proof_state(expr const & meta, expr const & type); goals map_goals(proof_state const & s, std::function(goal const & g)> f); diff --git a/src/library/tactic/replace_tactic.cpp b/src/library/tactic/replace_tactic.cpp index 9589c2171..7adcbb095 100644 --- a/src/library/tactic/replace_tactic.cpp +++ b/src/library/tactic/replace_tactic.cpp @@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Robert Y. Lewis */ - -#include "library/tactic/replace_tactic.h" +#include "util/fresh_name.h" #include "util/lazy_list_fn.h" #include "kernel/error_msgs.h" +#include "kernel/instantiate.h" #include "library/constants.h" #include "library/reducible.h" #include "library/unifier.h" +#include "library/tactic/replace_tactic.h" #include "library/tactic/expr_to_tactic.h" -#include "kernel/instantiate.h" namespace lean { @@ -61,9 +61,8 @@ tactic mk_replace_tactic(elaborate_fn const & elab, expr const & e) { if (new_t1 && new_t2) { goals const & gs = new_s.get_goals(); goal const & g = head(gs); - name_generator ngen = new_s.get_ngen(); substitution subst = new_s.get_subst(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); constraint_seq cs; if (tc->is_def_eq(*new_t1, *new_t2, justification(), cs)) { auto nocc = loc.includes_goal(); @@ -79,22 +78,21 @@ tactic mk_replace_tactic(elaborate_fn const & elab, expr const & e) { buffer cs_buf; cs.linearize(cs_buf); to_buffer(new_s.get_postponed(), cs_buf); - unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), ngen.mk_child(), subst, cfg); + unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), subst, cfg); return map2(rseq, [=](pair const & p) -> proof_state { substitution const & subst = p.first; constraints const & postponed = p.second; - name_generator new_ngen(ngen); substitution new_subst = subst; - expr M = g.mk_meta(new_ngen.next(), new_goal); + expr M = g.mk_meta(mk_fresh_name(), new_goal); goal new_g(M, new_goal); assign(new_subst, g, M); - return proof_state(new_s, cons(new_g, tail(gs)), new_subst, new_ngen, postponed); + return proof_state(new_s, cons(new_g, tail(gs)), new_subst, postponed); }); } - expr M = g.mk_meta(ngen.next(), new_goal); + expr M = g.mk_meta(mk_fresh_name(), new_goal); goal new_g(M, new_goal); assign(subst, g, M); - return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen)); + return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst)); } else { throw_tactic_exception_if_enabled(new_s, [=](formatter const & fmt) { format r = format("invalid 'replace' tactic, the new type"); diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index a6cf0bd35..e8ae846c1 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "library/constants.h" #include "library/locals.h" @@ -31,13 +32,12 @@ tactic revert_tactic(name const & n) { << "' depends on '" << local_pp_name(h) << "'"); return none_proof_state(); // other hypotheses depend on h } - name_generator ngen = s.get_ngen(); expr new_type = Pi(h, g.get_type()); - expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps); + expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); goal new_g(new_meta, new_type); substitution new_subst = s.get_subst(); assign(new_subst, g, mk_app(new_meta, h)); - proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen); + proof_state new_s(s, goals(new_g, tail_gs), new_subst); return some_proof_state(new_s); } else { throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, unknown hypothesis '" << n << "'"); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 101d48e6d..e3b81772b 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -430,7 +430,7 @@ expr mk_xrewrite_tactic_expr(buffer const & elems) { \remark It stores the solution for goal \c g into \c s. */ -optional move_after(name_generator & ngen, goal const & g, name const & h, buffer const & hs, substitution & s) { +optional move_after(goal const & g, name const & h, buffer const & hs, substitution & s) { if (hs.empty()) return optional(g); // nothing to be done buffer hyps; @@ -452,7 +452,7 @@ optional move_after(name_generator & ngen, goal const & g, name const & h, new_hyps.append(to_move); new_hyps.append(hyps.size() - i - 1, hyps.begin() + i + 1); expr new_type = g.get_type(); - expr new_mvar = mk_metavar(ngen.next(), Pi(new_hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); assign(s, g, new_meta); @@ -569,7 +569,6 @@ class rewrite_fn { io_state m_ios; elaborate_fn m_elab; proof_state m_ps; - name_generator m_ngen; type_checker_ptr m_tc; type_checker_ptr m_matcher_tc; type_checker_ptr m_relaxed_tc; // reduce_to and check_trivial @@ -609,7 +608,7 @@ class rewrite_fn { } expr mk_meta(expr const & type) { - return m_g.mk_meta(m_ngen.next(), type); + return m_g.mk_meta(mk_fresh_name(), type); } class rewriter_converter : public projection_converter { @@ -645,17 +644,17 @@ class rewrite_fn { // TODO(Leo): should we add add an option that will not try to fold recursive applications if (to_unfold) { lean_assert(occs); - auto new_e = unfold_rec(m_env, m_ngen.mk_child(), force_unfold, e, to_unfold, *occs); + auto new_e = unfold_rec(m_env, force_unfold, e, to_unfold, *occs); if (!new_e) return none_expr(); - type_checker_ptr tc(new type_checker(m_env, m_ngen.mk_child(), + type_checker_ptr tc(new type_checker(m_env, std::unique_ptr(new rewriter_converter(m_env, list(), unfolded)))); expr r = normalize(*tc, *new_e, cs, use_eta); if (cs) // FAIL if generated constraints return none_expr(); return some_expr(r); } else { - type_checker_ptr tc(new type_checker(m_env, m_ngen.mk_child(), + type_checker_ptr tc(new type_checker(m_env, std::unique_ptr(new rewriter_converter(m_env, to_unfold, unfolded)))); expr r = normalize(*tc, e, cs, use_eta); @@ -667,7 +666,7 @@ class rewrite_fn { // Replace goal with definitionally equal one void replace_goal(expr const & new_type) { - expr M = m_g.mk_meta(m_ngen.next(), new_type); + expr M = m_g.mk_meta(mk_fresh_name(), new_type); goal new_g(M, new_type); assign(m_subst, m_g, M); update_goal(new_g); @@ -703,7 +702,7 @@ class rewrite_fn { } } expr new_type = m_g.get_type(); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); assign(m_subst, m_g, new_meta); @@ -748,7 +747,7 @@ class rewrite_fn { optional> elaborate_core(expr const & e, bool fail_if_cnstrs) { expr new_expr; substitution new_subst; constraints cs; - std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ios.get_options(), m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false); + std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ios.get_options(), e, none_expr(), m_ps.get_subst(), false); if (fail_if_cnstrs && cs) return optional>(); m_ps = proof_state(m_ps, new_subst); @@ -849,7 +848,7 @@ class rewrite_fn { cs_seq.linearize(cs); unifier_config cfg; cfg.m_discard = true; - unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_subst, cfg); + unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_subst, cfg); if (auto p = rseq.pull()) { substitution new_subst = p->first.first; new_e = new_subst.instantiate_all(new_e); @@ -1042,7 +1041,7 @@ class rewrite_fn { pair mk_class_instance_elaborator(expr const & type) { bool use_local_instances = true; bool is_strict = false; - return ::lean::mk_class_instance_elaborator(m_env, m_ios, m_ctx, m_ngen.next(), optional(), + return ::lean::mk_class_instance_elaborator(m_env, m_ios, m_ctx, optional(), use_local_instances, is_strict, some_expr(type), m_expr_loc.get_tag(), nullptr); } @@ -1251,7 +1250,7 @@ class rewrite_fn { unifier_config cfg; cfg.m_kind = unifier_kind::Liberal; cfg.m_discard = true; - unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_subst, cfg); + unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_subst, cfg); if (auto p = rseq.pull()) { substitution new_subst = p->first.first; rule = new_subst.instantiate_all(rule); @@ -1320,7 +1319,7 @@ class rewrite_fn { r = compare_head(pattern, t); } else { bool assigned = false; - r = match(pattern, t, m_lsubst, m_esubst, nullptr, nullptr, &m_mplugin, &assigned); + r = match(pattern, t, m_lsubst, m_esubst, nullptr, &m_mplugin, &assigned); if (assigned) reset_subst(); } @@ -1341,7 +1340,7 @@ class rewrite_fn { for (auto const & p : hyps) { used_hyp_names.push_back(mlocal_name(p)); } - if (auto new_g = ::lean::move_after(m_ngen, m_g, mlocal_name(hyp), used_hyp_names, m_subst)) { + if (auto new_g = ::lean::move_after(m_g, mlocal_name(hyp), used_hyp_names, m_subst)) { m_g = *new_g; return true; } else { @@ -1413,7 +1412,7 @@ class rewrite_fn { } } expr new_type = m_g.get_type(); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); + expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); expr V = mk_app(new_mvar, args); @@ -1446,7 +1445,7 @@ class rewrite_fn { expr A = m_relaxed_tc->infer(a).first; level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).first); level l2 = sort_level(m_relaxed_tc->ensure_type(A).first); - expr M = m_g.mk_meta(m_ngen.next(), Pb); + expr M = m_g.mk_meta(mk_fresh_name(), Pb); expr H; if (has_dep_elim) { expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, b, mk_var(0)); @@ -1555,7 +1554,7 @@ class rewrite_fn { } // Process the given rewrite element/step. This method destructively update - // m_g, m_subst, m_ngen. It returns true if it succeeded and false otherwise. + // m_g, m_subst, It returns true if it succeeded and false otherwise. bool process_step(expr const & elem) { clear_trace(); if (is_rewrite_unfold_step(elem)) { @@ -1582,10 +1581,10 @@ class rewrite_fn { type_checker_ptr mk_matcher_tc(bool full) { if (get_rewriter_syntactic(m_ios.get_options())) { // use an everything opaque converter - return mk_opaque_type_checker(m_env, m_ngen.mk_child()); + return mk_opaque_type_checker(m_env); } else { auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env); - return mk_simple_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { + return mk_simple_type_checker(m_env, [=](name const & n) { // Remark: the condition !is_num_leaf_constant(n) is a little bit hackish. // It is here to allow us to match terms such as (@zero nat nat_has_zero) with nat.zero. // The idea is to treat zero and has_zero.zero as reducible terms and unfold them here. @@ -1596,7 +1595,7 @@ class rewrite_fn { type_checker_ptr mk_tc(bool full) { auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_quasireducible_pred(m_env); - return mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { + return mk_type_checker(m_env, [=](name const & n) { return aux_pred(n) && !is_numeral_const_name(n); }); } @@ -1606,7 +1605,7 @@ class rewrite_fn { if (ex) saved_ex.reset(static_cast(ex->clone())); if (m_ps.report_failure()) { - proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen); + proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst); if (!m_use_trace || !m_trace_initialized) { throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, [=](formatter const & fmt) { @@ -1649,10 +1648,10 @@ class rewrite_fn { public: rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps, bool full, bool keyed): - m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()), + m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_tc(mk_tc(full)), m_matcher_tc(mk_matcher_tc(full)), - m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child())), + m_relaxed_tc(mk_type_checker(m_env)), m_mplugin(m_ios, *m_matcher_tc) { m_keyed = keyed; m_ps = apply_substitution(m_ps); @@ -1681,7 +1680,7 @@ public: } goals new_gs = cons(m_g, tail(m_ps.get_goals())); - proof_state new_ps(m_ps, new_gs, m_subst, m_ngen); + proof_state new_ps(m_ps, new_gs, m_subst); return proof_state_seq(new_ps); } }; diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index 2dbeef716..b242c0b28 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/fresh_name.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" @@ -46,8 +47,7 @@ optional subst(environment const & env, name const & h_name, bool s expr lhs, rhs; if (!is_eq(mlocal_type(h), lhs, rhs)) return none_proof_state(); - name_generator ngen = s.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); if (symm) std::swap(lhs, rhs); if (!is_local(lhs)) @@ -75,7 +75,7 @@ optional subst(environment const & env, name const & h_name, bool s if (symm) { motive = Fun(lhs, Fun(h, type)); } else { - expr Heq = mk_local(ngen.next(), local_pp_name(h), mk_eq(*tc, rhs, lhs), binder_info()); + expr Heq = mk_local(mk_fresh_name(), local_pp_name(h), mk_eq(*tc, rhs, lhs), binder_info()); motive = Fun(lhs, Fun(Heq, type)); } } else { @@ -90,14 +90,14 @@ optional subst(environment const & env, name const & h_name, bool s for (expr const & d : deps) { if (!is_pi(new_goal_type)) return none_proof_state(); - expr new_h = mk_local(ngen.next(), local_pp_name(d), binding_domain(new_goal_type), binder_info()); + expr new_h = mk_local(mk_fresh_name(), local_pp_name(d), binding_domain(new_goal_type), binder_info()); new_hyps.push_back(new_h); intros_hyps.push_back(new_h); new_goal_type = instantiate(binding_body(new_goal_type), new_h); } // create new goal - expr new_metavar = mk_metavar(ngen.next(), Pi(new_hyps, new_goal_type)); + expr new_metavar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_goal_type)); expr new_meta_core = mk_app(new_metavar, non_deps); expr new_meta = mk_app(new_meta_core, intros_hyps); goal new_g(new_meta, new_goal_type); @@ -135,7 +135,7 @@ optional subst(environment const & env, name const & h_name, bool s expr new_val = mk_app(eqrec, deps); assign(new_subst, g, new_val); lean_assert(new_subst.is_assigned(g.get_mvar())); - proof_state new_s(s, goals(new_g, tail(gs)), new_subst, ngen); + proof_state new_s(s, goals(new_g, tail(gs)), new_subst); return some_proof_state(new_s); } diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/tactic/unfold_rec.cpp index a39ee964a..0c5a4cbb9 100644 --- a/src/library/tactic/unfold_rec.cpp +++ b/src/library/tactic/unfold_rec.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" @@ -21,8 +22,6 @@ namespace lean { // Auxiliary visitor the implements the common parts for unfold_rec_fn and fold_rec_fn class replace_visitor_aux : public replace_visitor { protected: - virtual name mk_fresh_name() = 0; - expr visit_app_default(expr const & e, expr const & fn, buffer & args) { bool modified = false; for (expr & arg : args) { @@ -47,7 +46,6 @@ protected: class unfold_rec_fn : public replace_visitor_aux { environment const & m_env; - name_generator m_ngen; bool m_force_unfold; type_checker_ptr m_tc; type_checker_ptr m_norm_decl_tc; @@ -55,8 +53,6 @@ class unfold_rec_fn : public replace_visitor_aux { occurrence m_occs; unsigned m_occ_idx; - virtual name mk_fresh_name() { return m_ngen.next(); } - static void throw_ill_formed() { throw exception("ill-formed expression"); } @@ -185,7 +181,7 @@ class unfold_rec_fn : public replace_visitor_aux { throw_ill_formed(); expr fn_body = instantiate_value_univ_params(decl, const_levels(fn)); while (is_lambda(fn_body)) { - expr local = mk_local(m_ngen.next(), binding_domain(fn_body)); + expr local = mk_local(mk_fresh_name(), binding_domain(fn_body)); locals.push_back(local); fn_body = instantiate(binding_body(fn_body), local); } @@ -217,8 +213,6 @@ class unfold_rec_fn : public replace_visitor_aux { lean_assert(std::all_of(rec_arg_pos.begin(), rec_arg_pos.end(), [&](unsigned pos) { return pos < args.size(); })); } - virtual name mk_fresh_name() { return m_tc->mk_fresh_name(); } - expr fold_rec(expr const & e, buffer const & args) { if (args.size() != m_major_idx + 1 + m_rec_arg_pos.size()) throw fold_failed(); @@ -382,13 +376,12 @@ class unfold_rec_fn : public replace_visitor_aux { } public: - unfold_rec_fn(environment const & env, name_generator && ngen, bool force_unfold, list const & to_unfold, + unfold_rec_fn(environment const & env, bool force_unfold, list const & to_unfold, occurrence const & occs): m_env(env), - m_ngen(ngen), m_force_unfold(force_unfold), - m_tc(mk_type_checker(m_env, m_ngen.mk_child(), [](name const &) { return false; })), - m_norm_decl_tc(mk_type_checker(m_env, m_ngen.mk_child(), [&](name const & n) { return !is_rec_building_part(n); })), + m_tc(mk_type_checker(m_env, [](name const &) { return false; })), + m_norm_decl_tc(mk_type_checker(m_env, [&](name const & n) { return !is_rec_building_part(n); })), m_to_unfold(to_unfold), m_occs(occs), m_occ_idx(0) @@ -400,11 +393,11 @@ public: } }; -optional unfold_rec(environment const & env, name_generator && ngen, bool force_unfold, expr const & e, list const & to_unfold, +optional unfold_rec(environment const & env, bool force_unfold, expr const & e, list const & to_unfold, occurrence const & occs) { lean_assert(std::all_of(to_unfold.begin(), to_unfold.end(), [&](name const & n) { return env.get(n).is_definition(); })); try { - expr r = unfold_rec_fn(env, std::move(ngen), force_unfold, to_unfold, occs)(e); + expr r = unfold_rec_fn(env, force_unfold, to_unfold, occs)(e); if (r == e) return none_expr(); return some_expr(r); diff --git a/src/library/tactic/unfold_rec.h b/src/library/tactic/unfold_rec.h index f4c6067e3..074ab5fbd 100644 --- a/src/library/tactic/unfold_rec.h +++ b/src/library/tactic/unfold_rec.h @@ -9,6 +9,6 @@ Author: Leonardo de Moura #include "library/tactic/location.h" namespace lean { -optional unfold_rec(environment const & env, name_generator && ngen, bool force_unfold, expr const & e, +optional unfold_rec(environment const & env, bool force_unfold, expr const & e, list const & to_unfold, occurrence const & occs); } diff --git a/src/library/tactic/whnf_tactic.cpp b/src/library/tactic/whnf_tactic.cpp index d0c78ff8d..d5bc87fb9 100644 --- a/src/library/tactic/whnf_tactic.cpp +++ b/src/library/tactic/whnf_tactic.cpp @@ -16,14 +16,13 @@ tactic whnf_tactic() { goals const & gs = ps.get_goals(); if (empty(gs)) return none_proof_state(); - name_generator ngen = ps.get_ngen(); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_type_checker(env); goal g = head(gs); goals tail_gs = tail(gs); expr type = g.get_type(); auto t_cs = tc->whnf(type); goals new_gs(goal(g.get_meta(), t_cs.first), tail_gs); - proof_state new_ps(ps, new_gs, ngen); + proof_state new_ps(ps, new_gs); if (solve_constraints(env, ios, new_ps, t_cs.second)) { return some_proof_state(new_ps); } else { diff --git a/src/library/tmp_type_context.cpp b/src/library/tmp_type_context.cpp index 92bd46bb2..fdfca87a5 100644 --- a/src/library/tmp_type_context.cpp +++ b/src/library/tmp_type_context.cpp @@ -21,12 +21,6 @@ tmp_type_context::tmp_type_context(environment const & env, options const & o, r init(env, b); } -tmp_type_context::tmp_type_context(environment const & env, options const & o, tmp_local_generator & gen, - reducible_behavior b): - type_context(env, o, gen) { - init(env, b); -} - tmp_type_context::~tmp_type_context() { } diff --git a/src/library/tmp_type_context.h b/src/library/tmp_type_context.h index b04289d69..aff334213 100644 --- a/src/library/tmp_type_context.h +++ b/src/library/tmp_type_context.h @@ -44,8 +44,6 @@ class tmp_type_context : public type_context { void init(environment const & env, reducible_behavior b); public: tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible); - tmp_type_context(environment const & env, options const & o, - tmp_local_generator & gen, reducible_behavior b = UnfoldReducible); virtual ~tmp_type_context(); /** \brief Reset the state: backtracking stack, indices and assignment. */ diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 0b7ebb16e..91aa09b02 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -46,32 +46,6 @@ bool get_class_trans_instances(options const & o) { return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES); } -tmp_local_generator::tmp_local_generator(): - m_next_local_idx(0) {} - -name tmp_local_generator::mk_fresh_name() { - unsigned idx = m_next_local_idx; - m_next_local_idx++; - return name(*g_tmp_prefix, idx); -} - -expr tmp_local_generator::mk_tmp_local(expr const & type, binder_info const & bi) { - name n = mk_fresh_name(); - return lean::mk_local(n, n, type, bi); -} - -expr tmp_local_generator::mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) { - name n = mk_fresh_name(); - return lean::mk_local(n, pp_n, type, bi); -} - -bool tmp_local_generator::is_tmp_local(expr const & e) const { - if (!is_local(e)) - return false; - name const & n = mlocal_name(e); - return !n.is_atomic() && n.get_prefix() == *g_tmp_prefix; -} - struct type_context::ext_ctx : public extension_context { type_context & m_owner; @@ -91,22 +65,14 @@ struct type_context::ext_ctx : public extension_context { return mk_pair(m_owner.infer(e), constraint_seq()); } - virtual name mk_fresh_name() { - return m_owner.m_ngen.next(); - } - virtual optional is_stuck(expr const &) { return none_expr(); } }; -type_context::type_context(environment const & env, options const & o, tmp_local_generator * gen, - bool gen_owner, bool multiple_instances): +type_context::type_context(environment const & env, options const & o, bool multiple_instances): m_env(env), - m_ngen(*g_internal_prefix), m_ext_ctx(new ext_ctx(*this)), - m_local_gen(gen), - m_local_gen_owner(gen_owner), m_proj_info(get_projection_info_map(env)) { m_pip = nullptr; m_ci_multiple_instances = multiple_instances; @@ -120,8 +86,6 @@ type_context::type_context(environment const & env, options const & o, tmp_local } type_context::~type_context() { - if (m_local_gen_owner) - delete m_local_gen; } void type_context::push() { @@ -134,12 +98,29 @@ void type_context::pop() { m_infer_cache.pop(); } +expr type_context::mk_tmp_local(expr const & type, binder_info const & bi) { + name n = mk_tagged_fresh_name(*g_tmp_prefix); + return lean::mk_local(n, n, type, bi); +} + +expr type_context::mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi) { + name n = mk_tagged_fresh_name(*g_tmp_prefix); + return lean::mk_local(n, pp_name, type, bi); +} + +bool type_context::is_tmp_local(expr const & e) const { + if (!is_local(e)) + return false; + name const & n = mlocal_name(e); + return is_tagged_by(n, *g_tmp_prefix); +} + expr type_context::mk_internal_local(name const & n, expr const & type, binder_info const & bi) { - return mk_local(m_ngen.next(), n, type, bi); + return mk_local(mk_tagged_fresh_name(*g_internal_prefix), n, type, bi); } expr type_context::mk_internal_local(expr const & type, binder_info const & bi) { - name n = m_ngen.next(); + name n = mk_tagged_fresh_name(*g_internal_prefix); return mk_local(n, n, type, bi); } @@ -147,7 +128,7 @@ bool type_context::is_internal_local(expr const & e) const { if (!is_local(e)) return false; name const & n = mlocal_name(e); - return !n.is_atomic() && n.get_prefix() == m_ngen.prefix(); + return is_tagged_by(n, *g_internal_prefix); } void type_context::set_local_instances(list const & insts) { diff --git a/src/library/type_context.h b/src/library/type_context.h index 421b98865..f78700ae7 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/fresh_name.h" #include "util/scoped_map.h" #include "kernel/environment.h" #include "library/io_state.h" @@ -18,35 +19,9 @@ namespace lean { unsigned get_class_instance_max_depth(options const & o); bool get_class_trans_instances(options const & o); -/** \brief Many procedures need to create temporary local constants. - So, in the type_context class we provide this capability. - It is just a convenience, and allows many procedures to have a simpler - interface. Example: no need to take a type_context AND a name_generator. - However, in some procedures (e.g., simplifier) use multiple type_context - objects, and they want to make sure the local constants created by them - are distinct. So, we can accomplish that by providing the same - tmp_local_generator to different type_context objects. */ -class tmp_local_generator { - unsigned m_next_local_idx; - name mk_fresh_name(); -public: - tmp_local_generator(); - virtual ~tmp_local_generator() {} +/** \brief Type inference, normalization and definitional equality. + It is similar to the kernel type checker but it also supports unification variables. - /** \brief Create a temporary local constant */ - virtual expr mk_tmp_local(expr const & type, binder_info const & bi); - - /** \brief Create a temporary local constant using the given pretty print name. - The pretty printing name has not semantic significance. */ - virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi); - - /** \brief Return true if \c e was created using \c mk_tmp_local */ - virtual bool is_tmp_local(expr const & e) const; -}; - -/** \brief Light-weight type inference, normalization and definitional equality. - It is simpler and more efficient version of the kernel type checker. - It does not generate unification constraints. Unification problems are eagerly solved. However, only higher-order patterns are supported. @@ -82,7 +57,7 @@ public: These simultaneous unification problem cannot be solved. - In the elaborator, we address the issues above by making sure that + In the Lean 0.2 elaborator, we addressed the issues above by making sure that only *closed terms* (terms not containing local constants) can be assigned to metavariables. So a metavariable that occurs in a context records the parameters it depends on. For example, we @@ -103,7 +78,7 @@ public: Which has the solution ?m := fun x, x - The solution used in the elaborator is correct, but it may produce performance problems + The solution used in the Lean 0.2 elaborator is correct, but it may produce performance problems for procedures that have to create many meta-variables and the context is not small. For example, if the context contains N declarations, then the type of each meta-variable created will have N-nested Pi's. @@ -136,10 +111,7 @@ class type_context { struct ext_ctx; friend struct ext_ctx; environment m_env; - name_generator m_ngen; std::unique_ptr m_ext_ctx; - tmp_local_generator * m_local_gen; - bool m_local_gen_owner; // postponed universe constraints std::vector> m_postponed; name_map m_proj_info; @@ -330,14 +302,8 @@ class type_context { bool mk_nested_instance(expr const & m, expr const & m_type); optional mk_class_instance_core(expr const & type); void cache_ci_result(expr const & type, optional const & inst); - type_context(environment const & env, options const & o, tmp_local_generator * gen, - bool gen_owner, bool multiple_instances); public: - type_context(environment const & env, options const & o, bool multiple_instances = false): - type_context(env, o, new tmp_local_generator(), true, multiple_instances) {} - type_context(environment const & env, options const & o, tmp_local_generator & gen, - bool multiple_instances = false): - type_context(env, o, &gen, false, multiple_instances) {} + type_context(environment const & env, options const & o, bool multiple_instances = false); virtual ~type_context(); void set_local_instances(list const & insts); @@ -358,15 +324,11 @@ public: bool is_internal_local(expr const & e) const; /** \brief Create a temporary local constant */ - expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()) { - return m_local_gen->mk_tmp_local(type, bi); - } + expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()); /** \brief Create a temporary local constant using the given pretty print name. The pretty printing name has not semantic significance. */ - expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { - return m_local_gen->mk_tmp_local(pp_name, type, bi); - } + expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */ expr mk_tmp_local_from_binding(expr const & b) { @@ -374,9 +336,7 @@ public: } /** \brief Return true if \c e was created using \c mk_tmp_local */ - bool is_tmp_local(expr const & e) const { - return m_local_gen->is_tmp_local(e); - } + bool is_tmp_local(expr const & e) const; /** \brief Return true if \c l represents a universe unification variable. \remark This is supposed to be a subset of is_meta(l). diff --git a/src/library/type_util.cpp b/src/library/type_util.cpp index 9d1f5195a..852c2e9ff 100644 --- a/src/library/type_util.cpp +++ b/src/library/type_util.cpp @@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/fresh_name.h" #include "kernel/instantiate.h" #include "library/type_util.h" namespace lean { unsigned get_expect_num_args(type_checker & tc, expr e) { - name_generator ngen = tc.mk_ngen(); unsigned r = 0; while (true) { e = tc.whnf(e).first; if (!is_pi(e)) return r; // TODO(Leo): try to avoid the following instantiate. - expr local = mk_local(ngen.next(), binding_name(e), binding_domain(e), binding_info(e)); + expr local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); e = instantiate(binding_body(e), local); r++; } diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp index 668bb514c..df64ceba5 100644 --- a/src/library/unfold_macros.cpp +++ b/src/library/unfold_macros.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/interrupt.h" +#include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/find_fn.h" #include "kernel/expr_maps.h" @@ -56,7 +57,7 @@ class unfold_untrusted_macros_fn { buffer ls; while (e.kind() == k) { expr d = visit(instantiate_rev(binding_domain(e), ls.size(), ls.data())); - expr l = mk_local(m_tc.mk_fresh_name(), binding_name(e), d, binding_info(e)); + expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e)); ls.push_back(l); es.push_back(e); e = binding_body(e); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index dd0887772..2d571ab88 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/lbool.h" #include "util/flet.h" +#include "util/fresh_name.h" #include "util/sexpr/option_declarations.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" @@ -339,7 +340,6 @@ struct unifier_fn { typedef rb_map, expr_quick_cmp> expr_map; typedef std::shared_ptr type_checker_ptr; environment m_env; - name_generator m_ngen; substitution m_subst; constraints m_postponed; // constraints that will not be solved owned_map m_owned_map; // mapping from metavariable name m to constraint idx @@ -448,26 +448,26 @@ 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 && ngen, substitution const & s, + substitution const & s, unifier_config const & cfg): - m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), + m_env(env), m_subst(s), m_plugin(get_unifier_plugin(env)), m_config(cfg), m_num_steps(0) { switch (m_config.m_kind) { case unifier_kind::Cheap: - m_tc = mk_opaque_type_checker(env, m_ngen.mk_child()); + m_tc = mk_opaque_type_checker(env); m_flex_rigid_tc = m_tc; break; case unifier_kind::VeryConservative: - m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldReducible); + m_tc = mk_type_checker(env, UnfoldReducible); m_flex_rigid_tc = m_tc; break; case unifier_kind::Conservative: - m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldQuasireducible); + m_tc = mk_type_checker(env, UnfoldQuasireducible); m_flex_rigid_tc = m_tc; break; case unifier_kind::Liberal: - m_tc = mk_type_checker(env, m_ngen.mk_child()); - m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldQuasireducible); + m_tc = mk_type_checker(env); + m_flex_rigid_tc = mk_type_checker(env, UnfoldQuasireducible); break; default: lean_unreachable(); @@ -512,7 +512,7 @@ struct unifier_fn { void reset_conflict() { m_conflict = optional(); lean_assert(!in_conflict()); } expr mk_local_for(expr const & b) { - return mk_local(m_ngen.next(), binding_name(b), binding_domain(b), binding_info(b)); + return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b)); } /** @@ -1560,7 +1560,7 @@ struct unifier_fn { optional mk_i; unsigned i = 0; while (is_pi(mk_type)) { - expr new_mvar = mk_app(mk_aux_metavar_for(m_ngen, mvar_type), meta_args); + expr new_mvar = mk_app(mk_aux_metavar_for(mvar_type), meta_args); mk = mk_app(mk, new_mvar); if (info->m_i == i) mk_i = new_mvar; @@ -1579,7 +1579,7 @@ struct unifier_fn { bool process_plugin_constraint(constraint const & c) { lean_assert(!is_choice_cnstr(c)); - lazy_list alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child()); + lazy_list alts = m_plugin->solve(*m_tc, c); alts = append(alts, process_const_const_cnstr(c)); return process_lazy_constraints(alts, c.get_justification()); } @@ -1605,7 +1605,7 @@ struct unifier_fn { return false; } auto m_type_jst = m_subst.instantiate_metavars(m_type); - lazy_list alts = fn(m, m_type_jst.first, m_subst, m_ngen.mk_child()); + lazy_list alts = fn(m, m_type_jst.first, m_subst); return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second)); } @@ -1991,7 +1991,7 @@ struct unifier_fn { if (is_local(margs[i]) && local_occurs_once(margs[i], margs)) { n = mlocal_name(margs[i]); } else { - n = u.m_ngen.next(); + n = mk_fresh_name(); } expr local = mk_local(n, binding_name(it), d, binding_info(it)); locals.push_back(local); @@ -2030,13 +2030,13 @@ struct unifier_fn { // std::cout << "type: " << type << "\n"; if (context_check(type, locals)) { - expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, type)); + expr maux = mk_metavar(mk_fresh_name(), Pi(locals, type)); // std::cout << " >> " << maux << " : " << mlocal_type(maux) << "\n"; cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs; return mk_app(maux, locals); } else { - expr maux_type = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next())))); - expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals))); + expr maux_type = mk_metavar(mk_fresh_name(), Pi(locals, mk_sort(mk_meta_univ(mk_fresh_name())))); + expr maux = mk_metavar(mk_fresh_name(), Pi(locals, mk_app(maux_type, locals))); cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs; return mk_app(maux, locals); } @@ -2127,7 +2127,7 @@ struct unifier_fn { expr rhs_A = binding_domain(rhs); expr A_type = tc().infer(rhs_A, cs); expr A = mk_imitation_arg(rhs_A, A_type, locals, cs); - expr local = mk_local(u.m_ngen.next(), binding_name(rhs), A, binding_info(rhs)); + expr local = mk_local(mk_fresh_name(), binding_name(rhs), A, binding_info(rhs)); locals.push_back(local); margs.push_back(local); expr rhs_B = instantiate(binding_body(rhs), local); @@ -2371,7 +2371,7 @@ struct unifier_fn { if (optional lhs_type = infer(lhs, cs)) { expr new_type = Pi(shared_locals, *lhs_type); if (!has_local(new_type)) { - expr new_mvar = mk_metavar(m_ngen.next(), new_type); + expr new_mvar = mk_metavar(mk_fresh_name(), new_type); expr new_val = mk_app(new_mvar, shared_locals); justification const & j = c.get_justification(); return @@ -2460,7 +2460,7 @@ struct unifier_fn { if (found_lhs) { // rhs is of the form max(rest, lhs) // Solution is lhs := max(rest, ?u) where ?u is fresh metavariable - r = mk_meta_univ(m_ngen.next()); + r = mk_meta_univ(mk_fresh_name()); rest.push_back(r); unsigned i = rest.size(); while (i > 0) { @@ -2824,17 +2824,17 @@ unify_result_seq unify(std::shared_ptr u) { } } -unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator && ngen, +unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, substitution const & s, unifier_config const & cfg) { - return unify(std::make_shared(env, num_cs, cs, std::move(ngen), s, cfg)); + return unify(std::make_shared(env, num_cs, cs, s, cfg)); } -unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator && ngen, +unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, 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, std::move(ngen), new_s, cfg); + auto u = std::make_shared(env, 0, nullptr, 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(); diff --git a/src/library/unifier.h b/src/library/unifier.h index 2079a5b75..89eccfdd5 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include #include "util/lazy_list.h" -#include "util/name_generator.h" #include "util/sexpr/options.h" #include "kernel/constraint.h" #include "kernel/environment.h" @@ -18,7 +17,7 @@ namespace lean { unsigned get_unifier_max_steps(options const & opts); bool is_simple_meta(expr const & e); -expr mk_aux_metavar_for(name_generator & ngen, expr const & t); +expr mk_aux_metavar_for(expr const & t); enum class unify_status { Solved, Failed, Unsupported }; /** @@ -72,9 +71,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 && ngen, +unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, 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 && ngen, +unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, 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 b9dcf3050..7b76d44a2 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 && ngen) const { - return append(m_p1->solve(tc, c, ngen.mk_child()), m_p2->solve(tc, c, ngen.mk_child())); + virtual lazy_list solve(type_checker & tc, constraint const & c) const { + return append(m_p1->solve(tc, c), m_p2->solve(tc, c)); } }; 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 && ngen) const { - return orelse(m_p1->solve(tc, c, ngen.mk_child()), m_p2->solve(tc, c, ngen.mk_child())); + virtual lazy_list solve(type_checker & tc, constraint const & c) const { + return orelse(m_p1->solve(tc, c), m_p2->solve(tc, c)); } }; @@ -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 { + virtual lazy_list solve(type_checker &, constraint const &) 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 3c2adccbe..5e64c8829 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 = 0; + virtual lazy_list solve(type_checker &, constraint const &) const = 0; virtual bool delay_constraint(type_checker &, constraint const &) const = 0; }; diff --git a/src/library/util.cpp b/src/library/util.cpp index d7c72dc06..4f82c0ba0 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -163,7 +163,6 @@ bool is_recursive_datatype(environment const & env, name const & n) { bool is_reflexive_datatype(type_checker & tc, name const & n) { environment const & env = tc.env(); - name_generator ngen = tc.mk_ngen(); optional decls = inductive::is_inductive_decl(env, n); if (!decls) return false; @@ -175,7 +174,7 @@ bool is_reflexive_datatype(type_checker & tc, name const & n) { if (is_pi(arg) && find(arg, [&](expr const & e, unsigned) { return is_constant(e) && const_name(e) == n; })) { return true; } - expr local = mk_local(ngen.next(), binding_domain(type)); + expr local = mk_local(mk_fresh_name(), binding_domain(type)); type = instantiate(binding_body(type), local); } } @@ -236,27 +235,27 @@ expr instantiate_univ_param (expr const & e, name const & p, level const & l) { return instantiate_univ_params(e, to_list(p), to_list(l)); } -expr to_telescope(bool pi, name_generator & ngen, expr e, buffer & telescope, +expr to_telescope(bool pi, expr e, buffer & telescope, optional const & binfo) { while ((pi && is_pi(e)) || (!pi && is_lambda(e))) { expr local; if (binfo) - local = mk_local(ngen.next(), binding_name(e), binding_domain(e), *binfo); + local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), *binfo); else - local = mk_local(ngen.next(), binding_name(e), binding_domain(e), binding_info(e)); + local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); telescope.push_back(local); e = instantiate(binding_body(e), local); } return e; } -expr to_telescope(name_generator & ngen, expr const & type, buffer & telescope, optional const & binfo) { - return to_telescope(true, ngen, type, telescope, binfo); +expr to_telescope(expr const & type, buffer & telescope, optional const & binfo) { + return to_telescope(true, type, telescope, binfo); } -expr fun_to_telescope(name_generator & ngen, expr const & e, buffer & telescope, +expr fun_to_telescope(expr const & e, buffer & telescope, optional const & binfo) { - return to_telescope(false, ngen, e, telescope, binfo); + return to_telescope(false, e, telescope, binfo); } expr to_telescope(type_checker & tc, expr type, buffer & telescope, optional const & binfo, @@ -266,9 +265,9 @@ expr to_telescope(type_checker & tc, expr type, buffer & telescope, option type = new_type; expr local; if (binfo) - local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), *binfo); + local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), *binfo); else - local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type)); + local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type)); telescope.push_back(local); type = instantiate(binding_body(type), local); new_type = tc.whnf(type, cs); @@ -759,7 +758,7 @@ void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer co } t_aux.back().push_back(t_i); } - expr eq = mk_local(tc.mk_fresh_name(), e_name.append_after(i+1), mk_eq(tc, t_i, s_i), binder_info()); + expr eq = mk_local(mk_fresh_name(), e_name.append_after(i+1), mk_eq(tc, t_i, s_i), binder_info()); eqs.push_back(eq); } } @@ -772,7 +771,7 @@ void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer & expr ty = mlocal_type(t[i]); ty = abstract_locals(ty, i, t.data()); ty = instantiate_rev(ty, i, s.data()); - expr local = mk_local(tc.mk_fresh_name(), local_pp_name(t[i]).append_after("'"), ty, local_info(t[i])); + expr local = mk_local(mk_fresh_name(), local_pp_name(t[i]).append_after("'"), ty, local_info(t[i])); s.push_back(local); } return mk_telescopic_eq(tc, t, s, eqs); @@ -1014,14 +1013,14 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const & }); } -type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) { - return std::unique_ptr(new type_checker(env, std::move(ngen), - std::unique_ptr(new hint_converter(env, pred)))); +type_checker_ptr mk_type_checker(environment const & env, name_predicate const & pred) { + return std::unique_ptr(new type_checker(env, + std::unique_ptr(new hint_converter(env, pred)))); } -type_checker_ptr mk_simple_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) { - return std::unique_ptr(new type_checker(env, std::move(ngen), - std::unique_ptr(new hint_converter(env, pred)))); +type_checker_ptr mk_simple_type_checker(environment const & env, name_predicate const & pred) { + return std::unique_ptr(new type_checker(env, + std::unique_ptr(new hint_converter(env, pred)))); } bool is_internal_name(name const & n) { diff --git a/src/library/util.h b/src/library/util.h index 3bc0d4c5e..8b9cac788 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -87,7 +87,7 @@ optional is_constructor_app_ext(environment const & env, expr const & e); binder_info, otherwise the procedure uses the one attached in the domain. The procedure returns the "body" of type. */ -expr to_telescope(name_generator & ngen, expr const & type, buffer & telescope, +expr to_telescope(expr const & type, buffer & telescope, optional const & binfo = optional()); /** \brief Similar to previous procedure, but puts \c type in whnf */ expr to_telescope(type_checker & tc, expr type, buffer & telescope, @@ -105,7 +105,7 @@ expr to_telescope(type_checker & tc, expr type, buffer & telescope, option binder_info, otherwise the procedure uses the one attached to the arguments. The procedure returns the "body" of function. */ -expr fun_to_telescope(name_generator & ngen, expr const & e, buffer & telescope, optional const & binfo); +expr fun_to_telescope(expr const & e, buffer & telescope, optional const & binfo); /** \brief Return the universe where inductive datatype resides \pre \c ind_type is of the form Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl} @@ -266,10 +266,10 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e /** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true. Projections are reduced using the projection converter */ -type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred); +type_checker_ptr mk_type_checker(environment const & env, name_predicate const & pred); /** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true. No special support for projections is used */ -type_checker_ptr mk_simple_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred); +type_checker_ptr mk_simple_type_checker(environment const & env, name_predicate const & pred); /** \brief Generate the format object for hyps |- conclusion. The given substitution is applied to all elements. diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index f0692c469..16c2e2450 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -19,7 +19,7 @@ Author: Leonardo de Moura using namespace lean; static environment add_decl(environment const & env, declaration const & d) { - auto cd = check(env, d, name_generator("test")); + auto cd = check(env, d); return env.add(cd); } @@ -72,12 +72,12 @@ static void tst1() { expr Prop = mk_Prop(); expr c = mk_local("c", Prop); expr id = Const("id"); - type_checker checker(env3, name_generator("tmp")); + type_checker checker(env3); lean_assert(checker.check(mk_app(id, Prop)).first == Prop >> Prop); lean_assert(checker.whnf(mk_app(id, Prop, c)).first == c); lean_assert(checker.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))).first == c); - type_checker checker2(env2, name_generator("tmp")); + type_checker checker2(env2); lean_assert(checker2.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))).first == mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))); } @@ -99,7 +99,7 @@ static void tst2() { env = add_decl(env, mk_definition("id", level_param_names(), Pi(A, A >> A), Fun({A, a}, a))); - type_checker checker(env, name_generator("tmp")); + type_checker checker(env); expr f96 = Const(name(base, 96)); expr f97 = Const(name(base, 97)); expr f98 = Const(name(base, 98)); @@ -152,7 +152,7 @@ static void tst3() { expr proj1 = Const("proj1"); expr a = Const("a"); expr b = Const("b"); - type_checker checker(env, name_generator("tmp")); + type_checker checker(env); lean_assert_eq(checker.whnf(mk_app(proj1, mk_app(proj1, mk_app(mk, mk_app(id, A, mk_app(mk, a, b)), b)))).first, a); } diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp index dad089ad4..0d6cb02df 100644 --- a/src/tests/library/unifier.cpp +++ b/src/tests/library/unifier.cpp @@ -22,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, name_generator("foo")); + auto r = unify(env, t1, t2); lean_assert(!r.pull()); } diff --git a/src/tests/shared/shared.cpp b/src/tests/shared/shared.cpp index c301106a1..022fa9bd4 100644 --- a/src/tests/shared/shared.cpp +++ b/src/tests/shared/shared.cpp @@ -34,7 +34,7 @@ int main() { env = add_decl(env, mk_definition("id", level_param_names(), Pi(A, A >> A), Fun({A, a}, a))); - type_checker checker(env, name_generator("tmp")); + type_checker checker(env); expr f96 = Const(name(base, 96)); expr f97 = Const(name(base, 97)); expr f98 = Const(name(base, 98)); diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp index 7391dd980..f9cb387b4 100644 --- a/src/tests/util/name.cpp +++ b/src/tests/util/name.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include "util/test.h" #include "util/name.h" -#include "util/name_generator.h" #include "util/name_set.h" #include "util/init_module.h" using namespace lean; @@ -120,31 +119,6 @@ static void tst8() { std::cout << u1 << " " << u2 << "\n"; } -static void tst9() { - name_generator g("a"); - lean_assert(g.prefix() == "a"); - name n0 = g.next(); - name n1 = g.next(); - name a0(name("a"), 0u); - name a1(name("a"), 1u); - lean_assert(n0 == a0); - lean_assert(n1 == a1); -} - -static void tst10() { - name_generator g1("a"); - name_generator g2("b"); - name a0 = g1.next(); - name b0 = g2.next(); - lean_assert_eq(a0, name(name("a"), 0u)); - lean_assert_eq(b0, name(name("b"), 0u)); - swap(g1, g2); - name a1 = g2.next(); - name b1 = g1.next(); - lean_assert_eq(a1, name(name("a"), 1u)); - lean_assert_eq(b1, name(name("b"), 1u)); -} - static void tst11() { name n1("a"); name n2("b"); @@ -163,15 +137,6 @@ static void tst12() { lean_assert(mk_unique(s, name("foo")) == name(name("foo"), 2)); } -static void tst13() { - name_generator g1("a"); - name_generator c1 = g1.mk_child(); - name_generator c2 = g1.mk_child(); - lean_assert(c1.next() != c2.next()); - std::cout << c1.next() << "\n"; - std::cout << c2.next() << "\n"; -} - int main() { save_stack_info(); initialize_util_module(); @@ -183,11 +148,8 @@ int main() { tst6(); tst7(); tst8(); - tst9(); - tst10(); tst11(); tst12(); - tst13(); finalize_util_module(); return has_violations() ? 1 : 0; } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 74ddb6854..86900f5a4 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,6 +1,6 @@ -add_library(util OBJECT debug.cpp name.cpp name_set.cpp - name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp - bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp - realpath.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp bitap_fuzzy_search.cpp - init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp - null_ostream.cpp file_lock.cpp) +add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp + exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp + safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp + stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp + bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.cpp + utf8.cpp name_map.cpp list_fn.cpp null_ostream.cpp file_lock.cpp) diff --git a/src/util/fresh_name.cpp b/src/util/fresh_name.cpp new file mode 100644 index 000000000..a74594240 --- /dev/null +++ b/src/util/fresh_name.cpp @@ -0,0 +1,57 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/fresh_name.h" +#include "util/thread.h" + +namespace lean { +MK_THREAD_LOCAL_GET_DEF(name, get_prefix); +LEAN_THREAD_VALUE(unsigned, g_next_idx, 0); + +name mk_fresh_name() { + name & prefix = get_prefix(); + if (prefix.is_anonymous()) { + // prefix has not been initialized for this thread yet. + prefix = name::mk_internal_unique_name(); + } + if (g_next_idx == std::numeric_limits::max()) { + // avoid overflow + prefix = name(prefix, g_next_idx); + g_next_idx = 0; + } + name r(prefix, g_next_idx); + g_next_idx++; + return r; +} + +name mk_tagged_fresh_name(name const & tag) { + lean_assert(tag.is_atomic()); + name & prefix = get_prefix(); + if (prefix.is_anonymous()) { + // prefix has not been initialized for this thread yet. + prefix = name::mk_internal_unique_name(); + } + if (g_next_idx == std::numeric_limits::max()) { + // avoid overflow + prefix = name(prefix, g_next_idx); + g_next_idx = 0; + } + name r(tag + prefix, g_next_idx); + g_next_idx++; + return r; +} + +bool is_tagged_by(name const & n, name const & tag) { + lean_assert(tag.is_atomic()); + if (n.is_atomic()) + return false; + name t = n; + while (!t.is_atomic()) + t = t.get_prefix(); + return t == tag; +} +} diff --git a/src/util/fresh_name.h b/src/util/fresh_name.h new file mode 100644 index 000000000..8fc4b706a --- /dev/null +++ b/src/util/fresh_name.h @@ -0,0 +1,21 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/name.h" + +namespace lean { +/** \brief Create a unique fresh name. This operation is thread-safe, and it guarantees the names are unique + even when multiple threads are used and they are created using */ +name mk_fresh_name(); + +/** \brief Create a unique fresh name prefixed with the given tag. The tag is used to mark the name. + \pre tag.is_atomic() */ +name mk_tagged_fresh_name(name const & tag); + +/** \brief Return true iff \c n is tagged by atomic name \c tag */ +bool is_tagged_by(name const & n, name const & tag); +} diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp index 4de7051ab..67fc607e8 100644 --- a/src/util/init_module.cpp +++ b/src/util/init_module.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "util/debug.h" #include "util/serializer.h" #include "util/name.h" -#include "util/name_generator.h" #include "util/lean_path.h" #include "util/thread.h" #include "util/memory_pool.h" @@ -20,12 +19,10 @@ void initialize_util_module() { initialize_thread(); initialize_ascii(); initialize_name(); - initialize_name_generator(); initialize_lean_path(); } void finalize_util_module() { finalize_lean_path(); - finalize_name_generator(); finalize_name(); finalize_ascii(); finalize_thread(); diff --git a/src/util/name_generator.cpp b/src/util/name_generator.cpp deleted file mode 100644 index 3581d4813..000000000 --- a/src/util/name_generator.cpp +++ /dev/null @@ -1,38 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/name_generator.h" - -namespace lean { -static name * g_tmp_prefix = nullptr; -name_generator::name_generator():name_generator(*g_tmp_prefix) {} - -name name_generator::next() { - if (m_next_idx == std::numeric_limits::max()) { - // avoid overflow - m_prefix = name(m_prefix, m_next_idx); - m_next_idx = 0; - } - name r(m_prefix, m_next_idx); - m_next_idx++; - return r; -} - -void swap(name_generator & a, name_generator & b) { - swap(a.m_prefix, b.m_prefix); - std::swap(a.m_next_idx, b.m_next_idx); -} - -void initialize_name_generator() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); -} - -void finalize_name_generator() { - delete g_tmp_prefix; -} -} diff --git a/src/util/name_generator.h b/src/util/name_generator.h deleted file mode 100644 index 7c5b6e441..000000000 --- a/src/util/name_generator.h +++ /dev/null @@ -1,43 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "util/name.h" - -namespace lean { -/** - \brief A generator of unique names modulo a prefix. - If the initial prefix is independent of all other names in the system, then all generated names are unique. - - \remark There is no risk of overflow in the m_next_idx. If m_next_idx reaches std::numeric_limits::max(), - then the prefix becomes name(m_prefix, m_next_idx), and m_next_idx is reset to 0 -*/ -class name_generator { - name m_prefix; - unsigned m_next_idx; -public: - name_generator(name const & prefix):m_prefix(prefix), m_next_idx(0) { lean_assert(!prefix.is_anonymous()); } - name_generator(); - - name const & prefix() const { return m_prefix; } - - /** \brief Return a unique name modulo \c prefix. */ - name next(); - - /** - \brief Create a child name_generator, each child name_generator is guaranteed to produce - names different from this name_generator and any other name_generator created with this generator. - */ - name_generator mk_child() { return name_generator(next()); } - - friend void swap(name_generator & a, name_generator & b); -}; -void swap(name_generator & a, name_generator & b); - -void initialize_name_generator(); -void finalize_name_generator(); -} diff --git a/tests/lean/pattern_hint1.lean.expected.out b/tests/lean/pattern_hint1.lean.expected.out index 2679a2d88..df0983573 100644 --- a/tests/lean/pattern_hint1.lean.expected.out +++ b/tests/lean/pattern_hint1.lean.expected.out @@ -2,8 +2,8 @@ definition foo₁ [forward] : ∀ (x : ℕ), f x ∧ g x := sorry (multi-)patterns: ?M_1 : ℕ -{f ?M_1} {g ?M_1} +{f ?M_1} definition foo₂ [forward] : ∀ (x : ℕ), (:f x:) ∧ g x := sorry (multi-)patterns: