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

refactor(kernel/instantiate): remove code duplication

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-21 14:30:38 -08:00
parent 7299b2d5d6
commit 2089b85532
1 changed files with 20 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/kernel/instantiate.cpp
View file

@ -12,29 +12,40 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
namespace lean { namespace lean {
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) { template<bool ClosedSubst>
lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); })); expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
return replace(a, [=](expr const & m, unsigned offset) -> expr { return replace(a, [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) { if (is_var(m)) {
unsigned vidx = var_idx(m); unsigned vidx = var_idx(m);
if (vidx >= offset) { if (vidx >= offset + s) {
if (vidx < offset + n) if (vidx < offset + s + n) {
return s[n - (vidx - offset) - 1]; if (ClosedSubst)
return subst[n - (vidx - s - offset) - 1];
else else
return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv);
} else {
return mk_var(vidx - n); return mk_var(vidx - n);
}
} else { } else {
return m; return m;
} }
} else if (is_metavar(m)) { } else if (is_metavar(m)) {
expr r = m; expr r = m;
for (unsigned i = 0; i < n; i++) for (unsigned i = 0; i < n; i++) {
r = add_inst(r, offset + n - i - 1, s[i], menv); expr v = ClosedSubst ? subst[i] : lift_free_vars(subst[i], offset + n - i - 1, menv);
r = add_inst(r, offset + s + n - i - 1, v, menv);
}
return r; return r;
} else { } else {
return m; return m;
} }
}); });
} }
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
return instantiate_core<true>(a, 0, n, s, menv);
}
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_menv(menv)); } expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_menv(menv)); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_menv()); } expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_menv()); }
expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); } expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); }
@ -43,26 +54,7 @@ expr instantiate_with_closed(expr const & e, expr const & s) { return instantiat
expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) { return instantiate_with_closed(e, s, some_menv(menv)); } expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) { return instantiate_with_closed(e, s, some_menv(menv)); }
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) { expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
return replace(a, [=](expr const & m, unsigned offset) -> expr { return instantiate_core<false>(a, s, n, subst, menv);
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset + s) {
if (vidx < offset + s + n)
return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv);
else
return mk_var(vidx - n);
} else {
return m;
}
} else if (is_metavar(m)) {
expr r = m;
for (unsigned i = 0; i < n; i++)
r = add_inst(r, offset + s + n - i - 1, lift_free_vars(subst[i], offset + n - i - 1, menv), menv);
return r;
} else {
return m;
}
});
} }
expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); } expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate(e, n, s, some_menv(menv)); } expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate(e, n, s, some_menv(menv)); }