From d64a8d24f9cce5f9dbf9f424fe6f49c7b80cf253 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 May 2016 12:04:28 -0700 Subject: [PATCH] fix(library/replace_visitor): remove replace_visitor_closed, it does not handle nested let-expr correctly --- src/library/replace_visitor.cpp | 9 --------- src/library/replace_visitor.h | 8 -------- 2 files changed, 17 deletions(-) diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp index 5bbe6546e6..07ad00ae72 100644 --- a/src/library/replace_visitor.cpp +++ b/src/library/replace_visitor.cpp @@ -77,13 +77,4 @@ expr replace_visitor::visit(expr const & e) { lean_unreachable(); // LCOV_EXCL_LINE } - -expr replace_visitor_closed::visit_binding(expr const & e) { - // TODO(Leo): improve performance by grouping calls to abstract_locals and instantiate. - lean_assert(is_binding(e)); - expr new_d = visit(binding_domain(e)); - expr new_l = mk_local(mk_fresh_name(), binding_name(e), new_d, binding_info(e)); - expr new_b = visit(instantiate(binding_body(e), new_l)); - return update_binding(e, new_d, abstract_local(new_b, new_l)); -} } diff --git a/src/library/replace_visitor.h b/src/library/replace_visitor.h index b4efc86a07..a6f451e79c 100644 --- a/src/library/replace_visitor.h +++ b/src/library/replace_visitor.h @@ -35,12 +35,4 @@ public: expr operator()(expr const & e) { return visit(e); } void clear() { m_cache.clear(); } }; - -/** \brief A replace_visitor class that provides a default visit_binding implementation - that replaces de-Bruijn variables with local constants. - Thus, any visited term is guaranteed to be closed. */ -class replace_visitor_closed : public replace_visitor { -protected: - virtual expr visit_binding(expr const &) override; -}; }