From 83335004571d3e55d245e52688e1276019e7b979 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jun 2016 10:29:02 -0700 Subject: [PATCH] refactor(library): move try_eta to util --- src/frontends/lean/util.cpp | 3 +- src/library/defeq_simplifier.cpp | 1 + src/library/normalize.cpp | 62 ------------------------------- src/library/normalize.h | 5 --- src/library/util.cpp | 64 ++++++++++++++++++++++++++++++++ src/library/util.h | 5 +++ 6 files changed, 72 insertions(+), 68 deletions(-) diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index bbb069d4b3..e7c57d603e 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -18,12 +18,13 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/constants.h" #include "library/typed_expr.h" -#include "library/normalize.h" #include "library/placeholder.h" #include "library/abbreviation.h" #include "library/unfold_macros.h" #include "library/choice.h" #include "library/num.h" +#include "library/util.h" +#include "library/normalize.h" #include "library/replace_visitor.h" #include "frontends/lean/parser.h" #include "frontends/lean/tokens.h" diff --git a/src/library/defeq_simplifier.cpp b/src/library/defeq_simplifier.cpp index d9b345283a..b1e7f72725 100644 --- a/src/library/defeq_simplifier.cpp +++ b/src/library/defeq_simplifier.cpp @@ -11,6 +11,7 @@ Author: Daniel Selsam #include "kernel/abstract.h" #include "kernel/inductive/inductive.h" #include "library/trace.h" +#include "library/util.h" #include "library/tmp_type_context.h" #include "library/normalize.h" diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 3187321724..b9848715eb 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -194,68 +194,6 @@ void finalize_normalize() { delete g_key; } -expr try_eta(expr const & e) { - if (is_lambda(e)) { - expr const & b = binding_body(e); - if (is_lambda(b)) { - expr new_b = try_eta(b); - if (is_eqp(b, new_b)) { - return e; - } else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) { - return lower_free_vars(app_fn(new_b), 1); - } else { - return update_binding(e, binding_domain(e), new_b); - } - } else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) { - return lower_free_vars(app_fn(b), 1); - } else { - return e; - } - } else { - return e; - } -} - -template -class eta_beta_reduce_fn : public replace_visitor { -public: - virtual expr visit_app(expr const & e) override { - expr e1 = replace_visitor::visit_app(e); - if (Beta && is_head_beta(e1)) { - return visit(head_beta_reduce(e1)); - } else { - return e1; - } - } - - virtual expr visit_lambda(expr const & e) override { - expr e1 = replace_visitor::visit_lambda(e); - if (Eta) { - while (true) { - expr e2 = try_eta(e1); - if (is_eqp(e1, e2)) - return e1; - else - e1 = e2; - } - } else { - return e1; - } - } -}; - -expr beta_reduce(expr t) { - return eta_beta_reduce_fn()(t); -} - -expr eta_reduce(expr t) { - return eta_beta_reduce_fn()(t); -} - -expr beta_eta_reduce(expr t) { - return eta_beta_reduce_fn()(t); -} - class normalize_fn { old_type_checker & m_tc; // Remark: the normalizer/type-checker m_tc has been provided by the "user". diff --git a/src/library/normalize.h b/src/library/normalize.h index 4346d7f2e5..cbf897332e 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -63,11 +63,6 @@ environment erase_constructor_hint(environment const & env, name const & n, name /** \brief Retrieve the hint added with the procedure add_constructor_hint. */ bool has_constructor_hint(environment const & env, name const & d); -expr try_eta(expr const & e); -expr beta_reduce(expr t); -expr eta_reduce(expr t); -expr beta_eta_reduce(expr t); - void initialize_normalize(); void finalize_normalize(); } diff --git a/src/library/util.cpp b/src/library/util.cpp index e20d6ef1f4..51ee5f7118 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "kernel/find_fn.h" +#include "kernel/free_vars.h" #include "kernel/instantiate.h" #include "kernel/error_msgs.h" #include "kernel/abstract.h" @@ -17,6 +18,7 @@ Author: Leonardo de Moura #include "library/unfold_macros.h" #include "library/pp_options.h" #include "library/projection.h" +#include "library/replace_visitor.h" #include "library/old_type_checker.h" namespace lean { @@ -821,6 +823,68 @@ format pp_type_mismatch(formatter const & fmt, expr const & v, expr const & v_ty return r; } +expr try_eta(expr const & e) { + if (is_lambda(e)) { + expr const & b = binding_body(e); + if (is_lambda(b)) { + expr new_b = try_eta(b); + if (is_eqp(b, new_b)) { + return e; + } else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) { + return lower_free_vars(app_fn(new_b), 1); + } else { + return update_binding(e, binding_domain(e), new_b); + } + } else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) { + return lower_free_vars(app_fn(b), 1); + } else { + return e; + } + } else { + return e; + } +} + +template +class eta_beta_reduce_fn : public replace_visitor { +public: + virtual expr visit_app(expr const & e) override { + expr e1 = replace_visitor::visit_app(e); + if (Beta && is_head_beta(e1)) { + return visit(head_beta_reduce(e1)); + } else { + return e1; + } + } + + virtual expr visit_lambda(expr const & e) override { + expr e1 = replace_visitor::visit_lambda(e); + if (Eta) { + while (true) { + expr e2 = try_eta(e1); + if (is_eqp(e1, e2)) + return e1; + else + e1 = e2; + } + } else { + return e1; + } + } +}; + +expr beta_reduce(expr t) { + return eta_beta_reduce_fn()(t); +} + +expr eta_reduce(expr t) { + return eta_beta_reduce_fn()(t); +} + +expr beta_eta_reduce(expr t) { + return eta_beta_reduce_fn()(t); +} + void initialize_library_util() { g_true = new expr(mk_constant(get_true_name())); g_true_intro = new expr(mk_constant(get_true_intro_name())); diff --git a/src/library/util.h b/src/library/util.h index cc6c45c21a..1c64fa2f16 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -219,6 +219,11 @@ expr mk_not(abstract_type_context & ctx, expr const & e); /** \brief Create the term absurd e not_e : t. */ expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e); +expr try_eta(expr const & e); +expr beta_reduce(expr t); +expr eta_reduce(expr t); +expr beta_eta_reduce(expr t); + void initialize_library_util(); void finalize_library_util(); }