max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf(library/compiler/csimp): avoid unnecessary local decl

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-08 17:03:34 -08:00
parent 6eca6bdb0e
commit f38cbeda5f
3 changed files with 16 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/compiler/csimp.cpp
View file

@ -481,13 +481,20 @@ class csimp_fn {
}
/* Given `e[x]`, create a let-decl `y := v`, and return `e[y]`
Note that, this transformation may produce type incorrect terms. */
Note that, this transformation may produce type incorrect terms.
Remove: if `v` is an atom, we do not create `y`. */
expr apply_at(expr const & x, expr const & e, expr const & v) {
local_decl x_decl = m_lctx.get_local_decl(x);
expr y = m_lctx.mk_local_decl(ngen(), x_decl.get_user_name(), x_decl.get_type(), v);
expr e_y = replace_fvar(e, x, y);
m_fvars.push_back(y);
return visit(e_y, false);
if (is_lcnf_atom(v)) {
expr e_v = replace_fvar(e, x, v);
return visit(e_v, false);
} else {
local_decl x_decl = m_lctx.get_local_decl(x);
expr y = m_lctx.mk_local_decl(ngen(), x_decl.get_user_name(), x_decl.get_type(), v);
expr e_y = replace_fvar(e, x, y);
m_fvars.push_back(y);
return visit(e_y, false);
}
}
expr_pair mk_jp_cache_key(expr const & x, expr const & e, expr const & jp) {

4
src/library/compiler/util.cpp
View file

@ -269,12 +269,12 @@ void mark_used_fvars(expr const & e, buffer<expr> const & fvars, buffer<bool> &
});
}
expr replace_fvar(expr const & e, expr const & fvar, expr const & new_fvar) {
expr replace_fvar(expr const & e, expr const & fvar, expr const & new_term) {
if (!has_fvar(e)) return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_fvar(e)) return some_expr(e);
if (is_fvar(e) && fvar_name(fvar) == fvar_name(e))
return some_expr(new_fvar);
return some_expr(new_term);
return none_expr();
});
}

2
src/library/compiler/util.h
View file

@ -107,7 +107,7 @@ void mark_used_fvars(expr const & e, buffer<expr> const & fvars, buffer<bool> &
/* Return true if `e` contains the free variable `fvar` */
bool has_fvar(expr const & e, expr const & fvar);
expr replace_fvar(expr const & e, expr const & fvar, expr const & new_fvar);
expr replace_fvar(expr const & e, expr const & fvar, expr const & new_term);
void sort_fvars(local_ctx const & lctx, buffer<expr> & fvars);