From d69db172a1633dbccaee471758152556e7696962 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 19 Jul 2014 12:53:01 +0100 Subject: [PATCH] chore(kernel/replace_fn): add syntax sugar for replace function Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/inductive_cmd.cpp | 4 ++-- src/frontends/lean/parser.cpp | 2 +- src/kernel/instantiate.cpp | 2 +- src/kernel/replace_fn.h | 3 +++ src/library/deep_copy.cpp | 2 +- src/library/level_names.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 2 +- 8 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0f87481bc..b436402f6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -101,7 +101,7 @@ public: if (!has_univ_metavar(e)) { return e; } else { - return replace(e, [&](expr const & e, unsigned) { + return replace(e, [&](expr const & e) { if (!has_univ_metavar(e)) { return some_expr(e); } else if (is_sort(e)) { diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 55e0ae5ed..bede699f3 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -341,7 +341,7 @@ struct inductive_cmd_fn { section parameters \c section_params as arguments. */ expr fix_inductive_occs(expr const & type, buffer const & decls, buffer const & section_params) { - return replace(type, [&](expr const & e, unsigned) { + return replace(type, [&](expr const & e) { if (!is_constant(e)) return none_expr(); if (!std::any_of(decls.begin(), decls.end(), @@ -455,7 +455,7 @@ struct inductive_cmd_fn { for (auto & d : decls) { buffer new_irs; for (auto & ir : inductive_decl_intros(d)) { - expr new_type = replace(intro_rule_type(ir), [&](expr const & e, unsigned) { + expr new_type = replace(intro_rule_type(ir), [&](expr const & e) { if (!is_constant(e)) return none_expr(); if (!std::any_of(decls.begin(), decls.end(), diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index e05b911cd..262907d57 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -243,7 +243,7 @@ expr parser::propagate_levels(expr const & e, levels const & ls) { if (is_nil(ls)) { return e; } else { - return replace(e, [&](expr const & e, unsigned) { + return replace(e, [&](expr const & e) { if (is_constant(e)) { auto it = m_env.find(const_name(e)); if (it) { diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index d3e661b16..97afa9e2e 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -156,7 +156,7 @@ expr beta_reduce(expr t) { expr instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls) { if (!has_param_univ(e)) return e; - return replace(e, [&](expr const & e, unsigned) -> optional { + return replace(e, [&](expr const & e) -> optional { if (!has_param_univ(e)) return some_expr(e); if (is_constant(e)) { diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index 073485c7f..17f79f6be 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -21,4 +21,7 @@ namespace lean { if f return none_expr. */ expr replace(expr const & e, std::function(expr const &, unsigned)> const & f); +inline expr replace(expr const & e, std::function(expr const &)> const & f) { + return replace(e, [&](expr const & e, unsigned) { return f(e); }); +} } diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index da9eeb9aa..03cc8ebd4 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -27,7 +27,7 @@ expr copy(expr const & a) { expr deep_copy(expr const & e) { scoped_expr_caching scope(false); - return replace(e, [](expr const & e, unsigned) { + return replace(e, [](expr const & e) { if (is_atomic(e)) return some_expr(copy(e)); else diff --git a/src/library/level_names.cpp b/src/library/level_names.cpp index 05452dbb1..5a08f229e 100644 --- a/src/library/level_names.cpp +++ b/src/library/level_names.cpp @@ -78,7 +78,7 @@ static levels rename_param_levels(levels const & ls, name_map const & para // Rename universe parameters occurring in e using the given mapping static expr rename_param_levels(expr const & e, name_map const & param_name_map) { - return replace(e, [&](expr const & e, unsigned) { + return replace(e, [&](expr const & e) { if (is_constant(e)) return some_expr(update_constant(e, rename_param_levels(const_levels(e), param_name_map))); else if (is_sort(e)) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index eb9060003..abe10becd 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -165,7 +165,7 @@ level refresh_univ_metavars(level const & l, name_generator & ngen, name_map level_map; - return replace(e, [&](expr const & e, unsigned) { + return replace(e, [&](expr const & e) { if (!has_univ_metavar(e)) return some_expr(e); if (is_sort(e))