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

feat(library/blast/expr): add instantiate_rev

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-21 17:12:45 -07:00
parent c5921fca6d
commit 2411fa3d2b
2 changed files with 26 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/library/blast/expr.cpp
View file

@ -420,9 +420,9 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) {
if (s >= get_free_var_range(a) || n == 0)
return a;
if (s == 0)
if (auto r = instantiate_easy_fn<false>(n, subst)(a, true))
if (auto r = blast::instantiate_easy_fn<false>(n, subst)(a, true))
return *r;
return replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
return blast::replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
unsigned s1 = s + offset;
if (s1 < s)
return some_expr(m); // overflow, vidx can't be >= max unsigned
@ -447,6 +447,29 @@ expr instantiate(expr const & e, unsigned n, expr const * s) {
return blast::instantiate(e, 0, n, s);
}
expr instantiate_rev(expr const & a, unsigned n, expr const * subst) {
if (closed(a))
return a;
if (auto r = blast::instantiate_easy_fn<true>(n, subst)(a, true))
return *r;
return blast::replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
if (offset >= get_free_var_range(m))
return some_expr(m); // expression m does not contain free variables with idx >= offset
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset) {
unsigned h = offset + n;
if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) {
return some_expr(blast::lift_free_vars(subst[n - (vidx - offset) - 1], offset));
} else {
return some_expr(blast::mk_var(vidx - n));
}
}
}
return none_expr();
});
}
class replace_level_fn {
std::function<optional<level>(level const &)> m_f;
level apply(level const & l) {

1
src/library/blast/expr.h
View file

@ -93,6 +93,7 @@ expr lift_free_vars(expr const & e, unsigned s, unsigned d);
expr lift_free_vars(expr const & e, unsigned d);
expr instantiate(expr const & e, unsigned n, expr const * s);
expr instantiate_rev(expr const & e, unsigned n, expr const * s);
level instantiate(level const & l, level_param_names const & ps, levels const & ls);
expr instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls);