michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(*): clarify name_generator ownership

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-21 14:32:36 -07:00
parent a7ead5fc14
commit f830bf54c2
22 changed files with 80 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/calc_proof_elaborator.cpp
View file

@ -123,11 +123,10 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
info_manager * im, update_type_info_fn const & fn) { info_manager * im, update_type_info_fn const & fn) {
justification j = mk_failed_to_synthesize_jst(env, m); justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & _s, auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & _s,
name_generator const & _ngen) { name_generator && ngen) {
local_context ctx = _ctx; local_context ctx = _ctx;
expr e = _e; expr e = _e;
substitution s = _s; substitution s = _s;
name_generator ngen(_ngen);
type_checker_ptr tc(mk_type_checker(env, ngen.mk_child())); type_checker_ptr tc(mk_type_checker(env, ngen.mk_child()));
constraint_seq new_cs = cs; constraint_seq new_cs = cs;
expr e_type = tc->infer(e, new_cs); expr e_type = tc->infer(e, new_cs);
@ -169,7 +168,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
unifier_config new_cfg(cfg); unifier_config new_cfg(cfg);
new_cfg.m_discard = false; new_cfg.m_discard = false;
new_cfg.m_kind = conservative ? unifier_kind::Conservative : unifier_kind::Liberal; new_cfg.m_kind = conservative ? unifier_kind::Conservative : unifier_kind::Liberal;
unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg); unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen.mk_child(), substitution(), new_cfg);
auto p = seq.pull(); auto p = seq.pull();
lean_assert(p); lean_assert(p);
substitution new_s = p->first.first; substitution new_s = p->first.first;
@ -218,8 +217,10 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
// 4. subst (eq.symm pr) (eq.refl lhs) // 4. subst (eq.symm pr) (eq.refl lhs)
if (symm) { if (symm) {
constraint_seq subst_cs = symm_cs; constraint_seq subst_cs = symm_cs;
if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) { if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second,
try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {} meta_type, subst_cs, g)) {
try { return try_alternative(subst->first, subst->second, subst_cs, conservative); }
catch (exception&) {}
} }
} }
} }
@ -240,7 +241,8 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
constraint_seq symm_cs = new_cs; 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, ngen, tc, e, e_type, symm_cs, g);
if (symm) { if (symm) {
try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } catch (exception &) {} try { return try_alternative(symm->first, symm->second, symm_cs, conservative); }
catch (exception &) {}
} }
// We use the exception for the first alternative as the error message // We use the exception for the first alternative as the error message

2
src/frontends/lean/coercion_elaborator.cpp
View file

@ -62,7 +62,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc
expr const & m, expr const & a, expr const & a_type, expr const & m, expr const & a, expr const & a_type,
justification const & j, unsigned delay_factor) { justification const & j, unsigned delay_factor) {
auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s, auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s,
name_generator const & /* ngen */) { name_generator && /* ngen */) {
expr new_a_type; expr new_a_type;
justification new_a_type_jst; justification new_a_type_jst;
if (is_meta(a_type)) { if (is_meta(a_type)) {

22
src/frontends/lean/elaborator.cpp
View file

@ -80,13 +80,13 @@ public:
} }
}; };
type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator const & ngen) { type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator && ngen) {
return std::unique_ptr<type_checker>(new type_checker(env, ngen, return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new coercion_from_converter(env)))); std::unique_ptr<converter>(new coercion_from_converter(env))));
} }
type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator const & ngen) { type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator && ngen) {
return std::unique_ptr<type_checker>(new type_checker(env, ngen, return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new coercion_to_converter(env)))); std::unique_ptr<converter>(new coercion_to_converter(env))));
} }
@ -141,7 +141,7 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
} }
}; };
elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names): elaborator::elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names):
m_ctx(ctx), m_ctx(ctx),
m_ngen(ngen), m_ngen(ngen),
m_context(), m_context(),
@ -334,7 +334,7 @@ expr elaborator::visit_choice(expr const & e, optional<expr> const & t, constrai
local_context ctx = m_context; local_context ctx = m_context;
local_context full_ctx = m_full_context; local_context full_ctx = m_full_context;
auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */, auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */,
name_generator const & /* ngen */) { name_generator && /* ngen */) {
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e)); return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e));
}; };
auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main) { auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main) {
@ -471,7 +471,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) { justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) {
return pp_function_expected(fmt, substitution(subst).instantiate(f)); return pp_function_expected(fmt, substitution(subst).instantiate(f));
}); });
auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator const &) { auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator &&) {
flet<local_context> save1(m_context, ctx); flet<local_context> save1(m_context, ctx);
flet<local_context> save2(m_full_context, full_ctx); flet<local_context> save2(m_full_context, full_ctx);
list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) { list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
@ -1112,13 +1112,13 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
io_state const & _ios = ios(); io_state const & _ios = ios();
justification j = mk_failed_to_synthesize_jst(_env, m); justification j = mk_failed_to_synthesize_jst(_env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator const & ngen) { name_generator && ngen) {
substitution new_s = s; substitution new_s = s;
expr new_eqns = new_s.instantiate_all(eqns); expr new_eqns = new_s.instantiate_all(eqns);
new_eqns = solve_unassigned_mvars(new_s, new_eqns); new_eqns = solve_unassigned_mvars(new_s, new_eqns);
if (display_unassigned_mvars(new_eqns, new_s)) if (display_unassigned_mvars(new_eqns, new_s))
return lazy_list<constraints>(); return lazy_list<constraints>();
type_checker_ptr tc = mk_type_checker(_env, ngen); type_checker_ptr tc = mk_type_checker(_env, std::move(ngen));
new_eqns = assign_equation_lhs_metas(*tc, new_eqns); new_eqns = assign_equation_lhs_metas(*tc, new_eqns);
expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type); expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type);
justification j = mk_justification("equation compilation", some_expr(eqns)); justification j = mk_justification("equation compilation", some_expr(eqns));
@ -1687,9 +1687,9 @@ optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) { optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
try { try {
auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional<expr> const & expected_type, auto fn = [=](goal const & g, name_generator && ngen, expr const & e, optional<expr> const & expected_type,
substitution const & subst, bool report_unassigned) { substitution const & subst, bool report_unassigned) {
elaborator aux_elaborator(m_ctx, ngen); elaborator aux_elaborator(m_ctx, std::move(ngen));
// Disable tactic hints when processing expressions nested in tactics. // Disable tactic hints when processing expressions nested in tactics.
// We must do it otherwise, it is easy to make the system loop. // We must do it otherwise, it is easy to make the system loop.
bool use_tactic_hints = false; bool use_tactic_hints = false;

2
src/frontends/lean/elaborator.h
View file

@ -181,7 +181,7 @@ class elaborator : public coercion_info_manager {
expr const & goal, bool first, constraint_seq & cs, expr const & src); expr const & goal, bool first, constraint_seq & cs, expr const & src);
expr visit_obtain_expr(expr const & e, constraint_seq & cs); expr visit_obtain_expr(expr const & e, constraint_seq & cs);
public: public:
elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false); elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names = false);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type); std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type);
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n); std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n);
}; };

7
src/frontends/lean/server.cpp
View file

@ -774,8 +774,8 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type
} }
} }
static std::unique_ptr<type_checker> mk_find_goal_type_checker(environment const & env, name_generator const & ngen) { static std::unique_ptr<type_checker> mk_find_goal_type_checker(environment const & env, name_generator && ngen) {
return mk_opaque_type_checker(env, ngen); return mk_opaque_type_checker(env, std::move(ngen));
} }
static name * g_tmp_prefix = nullptr; static name * g_tmp_prefix = nullptr;
@ -794,8 +794,7 @@ void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string
m_out << std::endl; m_out << std::endl;
environment const & env = env_opts->first; environment const & env = env_opts->first;
options const & opts = env_opts->second; options const & opts = env_opts->second;
name_generator ngen(*g_tmp_prefix); std::unique_ptr<type_checker> tc = mk_find_goal_type_checker(env, name_generator(*g_tmp_prefix));
std::unique_ptr<type_checker> tc = mk_find_goal_type_checker(env, ngen);
if (auto meta = m_file->infom().get_meta_at(line_num, col_num)) { if (auto meta = m_file->infom().get_meta_at(line_num, col_num)) {
if (is_meta(*meta)) { if (is_meta(*meta)) {
if (auto type = m_file->infom().get_type_at(line_num, col_num)) { if (auto type = m_file->infom().get_type_at(line_num, col_num)) {

2
src/kernel/constraint.h
View file

@ -57,7 +57,7 @@ typedef list<constraint> constraints;
One application of choice constraints is overloaded notation. One application of choice constraints is overloaded notation.
*/ */
typedef std::function<lazy_list<constraints>(expr const &, expr const &, substitution const &, name_generator const &)> choice_fn; typedef std::function<lazy_list<constraints>(expr const &, expr const &, substitution const &, name_generator &&)> choice_fn;
struct constraint_cell; struct constraint_cell;
class constraint { class constraint {

2
src/kernel/environment.h
View file

@ -224,7 +224,7 @@ class name_generator;
Only the type_checker class can create certified declarations. Only the type_checker class can create certified declarations.
*/ */
class certified_declaration { class certified_declaration {
friend certified_declaration check(environment const & env, declaration const & d, name_generator const & g); friend certified_declaration check(environment const & env, declaration const & d, name_generator && g);
environment_id m_id; environment_id m_id;
declaration m_declaration; declaration m_declaration;
certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {} certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}

2
src/kernel/expr.h
View file

@ -483,8 +483,6 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
/** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */ /** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag); expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag);
expr mk_local_for(expr const & b, name_generator const & ngen, tag g = nulltag);
bool enable_expr_caching(bool f); bool enable_expr_caching(bool f);
/** \brief Helper class for temporarily enabling/disabling expression caching */ /** \brief Helper class for temporarily enabling/disabling expression caching */
struct scoped_expr_caching { struct scoped_expr_caching {

12
src/kernel/type_checker.cpp
View file

@ -416,13 +416,13 @@ bool type_checker::is_opaque(expr const & c) const {
return true; return true;
} }
type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr<converter> && conv, bool memoize): type_checker::type_checker(environment const & env, name_generator && g, std::unique_ptr<converter> && conv, bool memoize):
m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this), m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this),
m_memoize(memoize), m_params(nullptr) { m_memoize(memoize), m_params(nullptr) {
} }
type_checker::type_checker(environment const & env, name_generator const & g, bool memoize): type_checker::type_checker(environment const & env, name_generator && g, bool memoize):
type_checker(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)), memoize) {} type_checker(env, std::move(g), std::unique_ptr<converter>(new default_converter(env, memoize)), memoize) {}
static name * g_tmp_prefix = nullptr; static name * g_tmp_prefix = nullptr;
@ -472,18 +472,18 @@ static void check_duplicated_params(environment const & env, declaration const &
} }
} }
certified_declaration check(environment const & env, declaration const & d, name_generator const & g) { certified_declaration check(environment const & env, declaration const & d, name_generator && g) {
if (d.is_definition()) if (d.is_definition())
check_no_mlocal(env, d.get_name(), d.get_value(), false); check_no_mlocal(env, d.get_name(), d.get_value(), false);
check_no_mlocal(env, d.get_name(), d.get_type(), true); check_no_mlocal(env, d.get_name(), d.get_type(), true);
check_name(env, d.get_name()); check_name(env, d.get_name());
check_duplicated_params(env, d); check_duplicated_params(env, d);
bool memoize = true; bool memoize = true;
type_checker checker1(env, g, std::unique_ptr<converter>(new default_converter(env, memoize))); type_checker checker1(env, g.mk_child(), std::unique_ptr<converter>(new default_converter(env, memoize)));
expr sort = checker1.check(d.get_type(), d.get_univ_params()).first; expr sort = checker1.check(d.get_type(), d.get_univ_params()).first;
checker1.ensure_sort(sort, d.get_type()); checker1.ensure_sort(sort, d.get_type());
if (d.is_definition()) { if (d.is_definition()) {
type_checker checker2(env, g, std::unique_ptr<converter>(new default_converter(env, memoize))); type_checker checker2(env, g.mk_child(), std::unique_ptr<converter>(new default_converter(env, memoize)));
expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first; expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first;
if (!checker2.is_def_eq(val_type, d.get_type()).first) { if (!checker2.is_def_eq(val_type, d.get_type()).first) {
throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) { throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {

6
src/kernel/type_checker.h
View file

@ -123,8 +123,8 @@ public:
memoize: if true, then inferred types are memoized/cached memoize: if true, then inferred types are memoized/cached
*/ */
type_checker(environment const & env, name_generator const & g, std::unique_ptr<converter> && conv, bool memoize = true); type_checker(environment const & env, name_generator && g, std::unique_ptr<converter> && conv, bool memoize = true);
type_checker(environment const & env, name_generator const & g, bool memoize = true); type_checker(environment const & env, name_generator && g, bool memoize = true);
type_checker(environment const & env); type_checker(environment const & env);
~type_checker(); ~type_checker();
@ -235,7 +235,7 @@ void check_no_metavar(environment const & env, name const & n, expr const & e, b
\brief Type check the given declaration, and return a certified declaration if it is type correct. \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. Throw an exception if the declaration is type incorrect.
*/ */
certified_declaration check(environment const & env, declaration const & d, name_generator const & g); certified_declaration check(environment const & env, declaration const & d, name_generator && g);
certified_declaration check(environment const & env, declaration const & d); certified_declaration check(environment const & env, declaration const & d);
/** /**

2
src/library/class.cpp
View file

@ -187,7 +187,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
declaration d = env.get(n); declaration d = env.get(n);
expr type = d.get_type(); expr type = d.get_type();
name_generator ngen(*g_tmp_prefix); name_generator ngen(*g_tmp_prefix);
auto tc = mk_type_checker(env, ngen); auto tc = mk_type_checker(env, ngen.mk_child());
while (true) { while (true) {
type = tc->whnf(type).first; type = tc->whnf(type).first;
if (!is_pi(type)) if (!is_pi(type))

6
src/library/inductive_unifier_plugin.cpp
View file

@ -43,7 +43,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...) 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. to the different constructors of decl.
*/ */
lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl, lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator & ngen, inductive::inductive_decl const & decl,
expr const & elim, buffer<expr> & args, expr const & t, justification const & j, expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
constraint_seq cs) const { constraint_seq cs) const {
lean_assert(is_constant(elim)); lean_assert(is_constant(elim));
@ -87,7 +87,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
return to_lazy(to_list(alts.begin(), alts.end())); return to_lazy(to_list(alts.begin(), alts.end()));
} }
lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen, lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator & ngen,
expr const & lhs, expr const & rhs, justification const & j) const { expr const & lhs, expr const & rhs, justification const & j) const {
lean_assert(inductive::is_elim_meta_app(tc, lhs)); lean_assert(inductive::is_elim_meta_app(tc, lhs));
auto dcs = tc.is_def_eq_types(lhs, rhs, j); auto dcs = tc.is_def_eq_types(lhs, rhs, j);
@ -111,7 +111,7 @@ public:
\brief Try to solve constraint of the form (elim ... (?m ...)) =?= t, by assigning (?m ...) to the introduction rules \brief Try to solve constraint of the form (elim ... (?m ...)) =?= t, by assigning (?m ...) to the introduction rules
associated with the eliminator \c elim. associated with the eliminator \c elim.
*/ */
virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator const & ngen) const { virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator && ngen) const {
if (!is_eq_cnstr(c)) if (!is_eq_cnstr(c))
return lazy_list<constraints>(); return lazy_list<constraints>();
expr const & lhs = cnstr_lhs_expr(c); expr const & lhs = cnstr_lhs_expr(c);

10
src/library/kernel_bindings.cpp
View file

@ -1766,7 +1766,8 @@ static int mk_type_checker(lua_State * L) {
if (nargs == 1) { if (nargs == 1) {
return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1))); return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1)));
} else { } else {
return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2))); return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1),
to_name_generator(L, 2).mk_child()));
} }
} }
static int type_checker_whnf(lua_State * L) { return push_ecs(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); } static int type_checker_whnf(lua_State * L) { return push_ecs(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); }
@ -1802,7 +1803,7 @@ static int mk_type_checker_with_hints(lua_State * L) {
if (nargs == 1) { if (nargs == 1) {
return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix))); return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix)));
} else { } else {
return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2))); return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2).mk_child()));
} }
} }
@ -1824,7 +1825,8 @@ static int type_check(lua_State * L) {
if (nargs == 2) { if (nargs == 2) {
return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2))); return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2)));
} else { } else {
return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3))); return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2),
to_name_generator(L, 3).mk_child()));
} }
} }
@ -1835,7 +1837,7 @@ static int add_declaration(lua_State * L) {
if (nargs == 2) { if (nargs == 2) {
d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2))); d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)));
} else { } else {
d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3)); d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3).mk_child());
} }
return push_environment(L, module::add(to_environment(L, 1), *d)); return push_environment(L, module::add(to_environment(L, 1), *d));
} }

16
src/library/reducible.cpp
View file

@ -134,17 +134,17 @@ bool unfold_semireducible_converter::is_opaque(declaration const & d) const {
return default_converter::is_opaque(d); return default_converter::is_opaque(d);
} }
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen, std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator && ngen,
reducible_behavior rb, bool memoize) { reducible_behavior rb, bool memoize) {
switch (rb) { switch (rb) {
case UnfoldReducible: case UnfoldReducible:
return std::unique_ptr<type_checker>(new type_checker(env, ngen, return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new unfold_reducible_converter(env, memoize)))); std::unique_ptr<converter>(new unfold_reducible_converter(env, memoize))));
case UnfoldQuasireducible: case UnfoldQuasireducible:
return std::unique_ptr<type_checker>(new type_checker(env, ngen, return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new unfold_quasireducible_converter(env, memoize)))); std::unique_ptr<converter>(new unfold_quasireducible_converter(env, memoize))));
case UnfoldSemireducible: case UnfoldSemireducible:
return std::unique_ptr<type_checker>(new type_checker(env, ngen, return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new unfold_semireducible_converter(env, memoize)))); std::unique_ptr<converter>(new unfold_semireducible_converter(env, memoize))));
} }
lean_unreachable(); lean_unreachable();
@ -160,8 +160,8 @@ public:
virtual bool is_opaque(declaration const &) const { return true; } virtual bool is_opaque(declaration const &) const { return true; }
}; };
std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator const & ngen) { std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator && ngen) {
return std::unique_ptr<type_checker>(new type_checker(env, ngen, return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new opaque_converter(env)))); std::unique_ptr<converter>(new opaque_converter(env))));
} }
@ -174,7 +174,7 @@ static int mk_opaque_type_checker(lua_State * L) {
type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), name_generator())); type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), name_generator()));
return push_type_checker_ref(L, r); return push_type_checker_ref(L, r);
} else { } else {
type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), to_name_generator(L, 2))); type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), to_name_generator(L, 2).mk_child()));
return push_type_checker_ref(L, r); return push_type_checker_ref(L, r);
} }
} }
@ -188,7 +188,7 @@ static int mk_reducible_checker_core(lua_State * L, reducible_behavior rb) {
type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), rb)); type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), rb));
return push_type_checker_ref(L, r); return push_type_checker_ref(L, r);
} else { } else {
type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), rb)); type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2).mk_child(), rb));
return push_type_checker_ref(L, r); return push_type_checker_ref(L, r);
} }
} }

4
src/library/reducible.h
View file

@ -63,13 +63,13 @@ public:
enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireducible }; enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireducible };
/** \brief Create a type checker that takes the "reducibility" hints into account. */ /** \brief Create a type checker that takes the "reducibility" hints into account. */
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen, std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator && ngen,
reducible_behavior r = UnfoldSemireducible, reducible_behavior r = UnfoldSemireducible,
bool memoize = true); bool memoize = true);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible); std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
/** \brief Create a type checker that treats all definitions as opaque. */ /** \brief Create a type checker that treats all definitions as opaque. */
std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator const & ngen); std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator && ngen);
void initialize_reducible(); void initialize_reducible();
void finalize_reducible(); void finalize_reducible();

4
src/library/tactic/class_instance_synth.cpp
View file

@ -328,7 +328,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
justification j = mk_failed_to_synthesize_jst(env, m); justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator const & ngen) { name_generator && ngen) {
environment const & env = C->env(); environment const & env = C->env();
auto cls_name_it = is_ext_class(C->tc(), meta_type); auto cls_name_it = is_ext_class(C->tc(), meta_type);
if (!cls_name_it) { if (!cls_name_it) {
@ -368,7 +368,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
return lazy_list<constraints>(constraints()); return lazy_list<constraints>(constraints());
}; };
unify_result_seq seq1 = unify(env, 1, &c, ngen, substitution(), new_cfg); unify_result_seq seq1 = unify(env, 1, &c, std::move(ngen), substitution(), new_cfg);
unify_result_seq seq2 = filter(seq1, [=](pair<substitution, constraints> const & p) { unify_result_seq seq2 = filter(seq1, [=](pair<substitution, constraints> const & p) {
substitution new_s = p.first; substitution new_s = p.first;
expr result = new_s.instantiate(new_meta); expr result = new_s.instantiate(new_meta);

2
src/library/tactic/elaborate.h
View file

@ -25,7 +25,7 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
3- postponed constraints 3- postponed constraints
*/ */
typedef std::tuple<expr, substitution, constraints> elaborate_result; typedef std::tuple<expr, substitution, constraints> elaborate_result;
typedef std::function<elaborate_result(goal const &, name_generator const &, expr const &, typedef std::function<elaborate_result(goal const &, name_generator &&, expr const &,
optional<expr> const &, substitution const &, bool)> elaborate_fn; optional<expr> const &, substitution const &, bool)> elaborate_fn;
/** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed

25
src/library/unifier.cpp
View file

@ -432,7 +432,7 @@ struct unifier_fn {
optional<justification> m_conflict; //!< if different from none, then there is a conflict. optional<justification> m_conflict; //!< if different from none, then there is a conflict.
unifier_fn(environment const & env, unsigned num_cs, constraint const * cs, unifier_fn(environment const & env, unsigned num_cs, constraint const * cs,
name_generator const & ngen, substitution const & s, name_generator && ngen, substitution const & s,
unifier_config const & cfg): unifier_config const & cfg):
m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
m_config(cfg), m_num_steps(0) { m_config(cfg), m_num_steps(0) {
@ -2326,17 +2326,17 @@ unify_result_seq unify(std::shared_ptr<unifier_fn> u) {
} }
} }
unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator && ngen,
substitution const & s, unifier_config const & cfg) { substitution const & s, unifier_config const & cfg) {
return unify(std::make_shared<unifier_fn>(env, num_cs, cs, ngen, s, cfg)); return unify(std::make_shared<unifier_fn>(env, num_cs, cs, std::move(ngen), s, cfg));
} }
unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator && ngen,
substitution const & s, unifier_config const & cfg) { substitution const & s, unifier_config const & cfg) {
substitution new_s = s; substitution new_s = s;
expr _lhs = new_s.instantiate(lhs); expr _lhs = new_s.instantiate(lhs);
expr _rhs = new_s.instantiate(rhs); expr _rhs = new_s.instantiate(rhs);
auto u = std::make_shared<unifier_fn>(env, 0, nullptr, ngen, new_s, cfg); auto u = std::make_shared<unifier_fn>(env, 0, nullptr, std::move(ngen), new_s, cfg);
constraint_seq cs; constraint_seq cs;
if (!u->m_tc->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) { if (!u->m_tc->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) {
return unify_result_seq(); return unify_result_seq();
@ -2411,7 +2411,7 @@ static constraints to_constraints(lua_State * L, int idx) {
static unifier_plugin to_unifier_plugin(lua_State * L, int idx) { static unifier_plugin to_unifier_plugin(lua_State * L, int idx) {
luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun
luaref f(L, idx); luaref f(L, idx);
return unifier_plugin([=](constraint const & c, name_generator const & ngen) { return unifier_plugin([=](constraint const & c, name_generator && ngen) {
lua_State * L = f.get_state(); lua_State * L = f.get_state();
f.push(); f.push();
push_constraint(L, c); push_constraint(L, c);
@ -2465,21 +2465,22 @@ static int unify(lua_State * L) {
environment const & env = to_environment(L, 1); environment const & env = to_environment(L, 1);
if (is_expr(L, 2)) { if (is_expr(L, 2)) {
if (nargs == 6) if (nargs == 6)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child(), to_substitution(L, 5),
unifier_config(to_options(L, 6))); unifier_config(to_options(L, 6)));
else if (nargs == 5) else if (nargs == 5)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5)); r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child(), to_substitution(L, 5));
else else
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4)); r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4).mk_child());
} else { } else {
buffer<constraint> cs; buffer<constraint> cs;
to_constraint_buffer(L, 2, cs); to_constraint_buffer(L, 2, cs);
if (nargs == 5) if (nargs == 5)
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4), unifier_config(to_options(L, 5))); r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child(), to_substitution(L, 4),
unifier_config(to_options(L, 5)));
else if (nargs == 4) else if (nargs == 4)
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4)); r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child(), to_substitution(L, 4));
else else
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3)); r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3).mk_child());
} }
return push_unify_result_seq_it(L, r); return push_unify_result_seq_it(L, r);
} }

4
src/library/unifier.h
View file

@ -74,9 +74,9 @@ struct unifier_config {
/** \brief The unification procedures produce a lazy list of pair substitution + constraints that could not be solved. */ /** \brief The unification procedures produce a lazy list of pair substitution + constraints that could not be solved. */
typedef lazy_list<pair<substitution, constraints>> unify_result_seq; typedef lazy_list<pair<substitution, constraints>> unify_result_seq;
unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator && ngen,
substitution const & s = substitution(), unifier_config const & c = unifier_config()); substitution const & s = substitution(), unifier_config const & c = unifier_config());
unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator && ngen,
substitution const & s = substitution(), unifier_config const & c = unifier_config()); substitution const & s = substitution(), unifier_config const & c = unifier_config());
/** /**

10
src/library/unifier_plugin.cpp
View file

@ -22,16 +22,16 @@ public:
class append_unifier_plugin_cell : public binary_unifier_plugin_cell { class append_unifier_plugin_cell : public binary_unifier_plugin_cell {
public: public:
append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {} append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator const & ngen) const { virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator && ngen) const {
return append(m_p1->solve(tc, c, ngen), m_p2->solve(tc, c, ngen)); return append(m_p1->solve(tc, c, ngen.mk_child()), m_p2->solve(tc, c, ngen.mk_child()));
} }
}; };
class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell { class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell {
public: public:
orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {} orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator const & ngen) const { virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator && ngen) const {
return orelse(m_p1->solve(tc, c, ngen), m_p2->solve(tc, c, ngen)); return orelse(m_p1->solve(tc, c, ngen.mk_child()), m_p2->solve(tc, c, ngen.mk_child()));
} }
}; };
@ -46,7 +46,7 @@ unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2) {
static unifier_plugin noop_unifier_plugin() { static unifier_plugin noop_unifier_plugin() {
class noop_unifier_plugin_cell : public unifier_plugin_cell { class noop_unifier_plugin_cell : public unifier_plugin_cell {
public: public:
virtual lazy_list<constraints> solve(type_checker &, constraint const &, name_generator const &) const { virtual lazy_list<constraints> solve(type_checker &, constraint const &, name_generator &&) const {
return lazy_list<constraints>(); return lazy_list<constraints>();
} }
virtual bool delay_constraint(type_checker &, constraint const &) const { return false; } virtual bool delay_constraint(type_checker &, constraint const &) const { return false; }

2
src/library/unifier_plugin.h
View file

@ -23,7 +23,7 @@ namespace lean {
class unifier_plugin_cell { class unifier_plugin_cell {
public: public:
virtual ~unifier_plugin_cell() {} virtual ~unifier_plugin_cell() {}
virtual lazy_list<constraints> solve(type_checker &, constraint const &, name_generator const &) const = 0; virtual lazy_list<constraints> solve(type_checker &, constraint const &, name_generator &&) const = 0;
virtual bool delay_constraint(type_checker &, constraint const &) const = 0; virtual bool delay_constraint(type_checker &, constraint const &) const = 0;
}; };

3
src/tests/library/unifier.cpp
View file

@ -14,7 +14,6 @@ using namespace lean;
static void tst1() { static void tst1() {
environment env; environment env;
name_generator ngen("foo");
expr Type = mk_Type(); expr Type = mk_Type();
expr A = Local("A", Type); expr A = Local("A", Type);
expr f = Local("f", A >> (A >> A)); expr f = Local("f", A >> (A >> A));
@ -23,7 +22,7 @@ static void tst1() {
expr m = mk_metavar("m", A); expr m = mk_metavar("m", A);
expr t1 = mk_app(f, m, m); expr t1 = mk_app(f, m, m);
expr t2 = mk_app(f, a, b); expr t2 = mk_app(f, a, b);
auto r = unify(env, t1, t2, ngen); auto r = unify(env, t1, t2, name_generator("foo"));
lean_assert(!r.pull()); lean_assert(!r.pull());
} }