Remove sanitize_names from kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
e792e079e2
commit
0fbfef8eb0
3 changed files with 13 additions and 41 deletions
|
@ -5,35 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "context.h"
|
||||
#include "occurs.h"
|
||||
#include "exception.h"
|
||||
|
||||
namespace lean {
|
||||
context sanitize_names_core(context const & c, context const & r, unsigned sz, expr const * es) {
|
||||
if (is_nil(c)) {
|
||||
return c;
|
||||
} else {
|
||||
// Remark: if this code is a bottleneck, then we can collect
|
||||
// all used names in r and es[sz] once and avoid the multiple
|
||||
// calls to occurs.
|
||||
context new_tail = sanitize_names_core(tail(c), r, sz, es);
|
||||
context_entry const & e = head(c);
|
||||
name const & n = e.get_name();
|
||||
name n1 = n;
|
||||
unsigned i = 1;
|
||||
while (occurs(n1, r, sz, es) ||
|
||||
std::any_of(new_tail.begin(), new_tail.end(), [&](context_entry const & e2) { return n1 == e2.get_name(); })) {
|
||||
n1 = name(n, i);
|
||||
i++;
|
||||
}
|
||||
return extend(new_tail, n1, e.get_domain(), e.get_body());
|
||||
}
|
||||
}
|
||||
|
||||
context sanitize_names(context const & c, unsigned sz, expr const * es) {
|
||||
return sanitize_names_core(c, c, sz, es);
|
||||
}
|
||||
|
||||
std::pair<context_entry const &, context const &> lookup_ext(context const & c, unsigned i) {
|
||||
context const * it1 = &c;
|
||||
while (*it1) {
|
||||
|
@ -55,4 +29,17 @@ context_entry const & lookup(context const & c, unsigned i) {
|
|||
}
|
||||
throw exception("unknown free variable");
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return a new context where the names used in the context
|
||||
entries of \c c do not shadow constants occurring in \c c and \c es[sz].
|
||||
|
||||
Recall that the names in context entries are just "suggestions".
|
||||
These names are used to name free variables in \c es[sz] (and
|
||||
dependent entries in \c c).
|
||||
*/
|
||||
context sanitize_names(context const & c, unsigned sz, expr const * es);
|
||||
inline context sanitize_names(context const & c, expr const & e) { return sanitize_names(c, 1, &e); }
|
||||
inline context sanitize_names(context const & c, std::initializer_list<expr> const & l) { return sanitize_names(c, l.size(), l.begin()); }
|
||||
|
||||
}
|
||||
|
|
|
@ -45,16 +45,4 @@ inline context extend(context const & c, name const & n, expr const & d) {
|
|||
inline bool is_empty(context const & c) {
|
||||
return is_nil(c);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return a new context where the names used in the context
|
||||
entries of \c c do not shadow constants occurring in \c c and \c es[sz].
|
||||
|
||||
Recall that the names in context entries are just "suggestions".
|
||||
These names are used to name free variables in \c es[sz] (and
|
||||
dependent entries in \c c).
|
||||
*/
|
||||
context sanitize_names(context const & c, unsigned sz, expr const * es);
|
||||
inline context sanitize_names(context const & c, expr const & e) { return sanitize_names(c, 1, &e); }
|
||||
inline context sanitize_names(context const & c, std::initializer_list<expr> const & l) { return sanitize_names(c, l.size(), l.begin()); }
|
||||
}
|
||||
|
|
|
@ -51,9 +51,6 @@ static void tst2() {
|
|||
auto p = lookup_ext(c, 0);
|
||||
lean_assert(p.first.get_name() == "a");
|
||||
lean_assert(length(p.second) == 0);
|
||||
std::cout << sanitize_names(c, f(a));
|
||||
lean_assert(lookup(sanitize_names(c, f(a)), 0).get_name() != name("a"));
|
||||
std::cout << sanitize_names(c, f(b));
|
||||
}
|
||||
|
||||
int main() {
|
||||
|
|
Loading…
Reference in a new issue