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

refactor(kernel/instantiate): remove hackish (dead) function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-20 14:37:05 -08:00
parent 4d05a8b65b
commit 84df182beb
2 changed files with 2 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/kernel/instantiate.cpp
View file

@ -12,7 +12,8 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
namespace lean { namespace lean {
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) { 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 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);
@ -34,16 +35,6 @@ expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s,
} }
}); });
} }
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv) {
return instantiate_with_closed_relaxed(a, n, s, some_menv(menv));
}
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s) {
return instantiate_with_closed_relaxed(a, n, s, none_menv());
}
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_with_closed_relaxed(a, 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()); }

9
src/kernel/instantiate.h
View file

@ -25,15 +25,6 @@ expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_en
expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv); expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv);
expr instantiate_with_closed(expr const & e, expr const & s); expr instantiate_with_closed(expr const & e, expr const & s);
/**
\brief Similar to instantiate_with_closed, but does not use an assertion for
testing whether arguments are close or not.
This version is useful, for example, when we want to treat metavariables as closed terms.
*/
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv);
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv);
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s);
/** /**
\brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.