refactor(library): move try_eta to util

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"

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"
 

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<bool Eta, bool Beta>
-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<false, true>()(t);
-}
-
-expr eta_reduce(expr t) {
-    return eta_beta_reduce_fn<true, false>()(t);
-}
-
-expr beta_eta_reduce(expr t) {
-    return eta_beta_reduce_fn<true, true>()(t);
-}
-
 class normalize_fn {
     old_type_checker   &                  m_tc;
     // Remark: the normalizer/type-checker m_tc has been provided by the "user".

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();
 }

src/library/util.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #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<bool Eta, bool Beta>
+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<false, true>()(t);
+}
+
+expr eta_reduce(expr t) {
+    return eta_beta_reduce_fn<true, false>()(t);
+}
+
+expr beta_eta_reduce(expr t) {
+    return eta_beta_reduce_fn<true, true>()(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()));

src/library/util.h

@@ -219,6 +219,11 @@ expr mk_not(abstract_type_context & ctx, expr const & e);
 /** \brief Create the term <tt>absurd e not_e : t</tt>. */
 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();
 }