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

chore(kernel/replace_fn): add syntax sugar for replace function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-19 12:53:01 +01:00
parent 6b60db7b93
commit d69db172a1
8 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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)) {

4
src/frontends/lean/inductive_cmd.cpp
View file

@ -341,7 +341,7 @@ struct inductive_cmd_fn {
section parameters \c section_params as arguments.
*/
expr fix_inductive_occs(expr const & type, buffer<inductive_decl> const & decls, buffer<expr> 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<intro_rule> 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(),

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

@ -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) {

2
src/kernel/instantiate.cpp
View file

@ -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<expr> {
return replace(e, [&](expr const & e) -> optional<expr> {
if (!has_param_univ(e))
return some_expr(e);
if (is_constant(e)) {

3
src/kernel/replace_fn.h
View file

@ -21,4 +21,7 @@ namespace lean {
if f return none_expr.
*/
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f);
inline expr replace(expr const & e, std::function<optional<expr>(expr const &)> const & f) {
return replace(e, [&](expr const & e, unsigned) { return f(e); });
}
}

2
src/library/deep_copy.cpp
View file

@ -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

2
src/library/level_names.cpp
View file

@ -78,7 +78,7 @@ static levels rename_param_levels(levels const & ls, name_map<name> const & para
// Rename universe parameters occurring in e using the given mapping
static expr rename_param_levels(expr const & e, name_map<name> 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))

2
src/library/tactic/apply_tactic.cpp
View file

@ -165,7 +165,7 @@ level refresh_univ_metavars(level const & l, name_generator & ngen, name_map<lev
expr refresh_univ_metavars(expr const & e, name_generator & ngen) {
if (has_univ_metavar(e)) {
name_map<level> 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))