feat(compiler): add eta expansion

src/compiler/CMakeLists.txt

@@ -1 +1 @@
-add_library(compiler OBJECT elim_rec.cpp)
+add_library(compiler OBJECT elim_rec.cpp eta_expansion.cpp)

src/compiler/elim_rec.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/user_recursors.h"
 #include "library/normalize.h"
 #include "library/util.h"
+#include "compiler/eta_expansion.h"
 
 void pp(lean::environment const & env, lean::expr const & e);
 
@@ -29,7 +30,9 @@ public:
     elim_rec_fn(environment const & env, buffer<declaration> & aux_decls): m_env(env), m_aux_decls(aux_decls) {}
 
     declaration operator()(declaration const & d) {
-        expr v = expand_aux_recursors(m_env, d.get_value());
+        expr v = d.get_value();
+        v = expand_aux_recursors(m_env, v);
+        v = eta_expand(m_env, v);
         ::pp(m_env, v);
         // TODO(Leo)
         return d;

src/compiler/eta_expansion.cpp

@@ -0,0 +1,84 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/type_checker.h"
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
+#include "library/replace_visitor.h"
+#include "compiler/eta_expansion.h"
+
+namespace lean {
+class eta_expand_fn : public replace_visitor {
+    environment  m_env;
+    type_checker m_tc;
+
+    optional<expr> expand_core(expr const & e) {
+        lean_assert(!is_lambda(e));
+        expr t = m_tc.whnf(m_tc.infer(e).first).first;
+        if (!is_pi(t))
+            return none_expr();
+        expr r = mk_lambda(name("x"), binding_domain(t), mk_app(e, mk_var(0)));
+        return some_expr(visit(r));
+    }
+
+    expr expand(expr const & e) {
+        if (auto r = expand_core(e))
+            return *r;
+        else
+            return e;
+    }
+
+    virtual expr visit_var(expr const &) { lean_unreachable(); }
+
+    virtual expr visit_meta(expr const &) { lean_unreachable(); }
+
+    virtual expr visit_macro(expr const & e) {
+        if (auto r = expand_core(e))
+            return *r;
+        else
+            return replace_visitor::visit_macro(e);
+    }
+
+    virtual expr visit_constant(expr const & e) { return expand(e); }
+
+    virtual expr visit_local(expr const & e) { return expand(e); }
+
+    virtual expr visit_app(expr const & e) {
+        if (auto r = expand_core(e)) {
+            return *r;
+        } else {
+            buffer<expr> args;
+            expr f = get_app_args(e, args);
+            bool modified = false;
+            for (unsigned i = 0; i < args.size(); i++) {
+                expr arg     = args[i];
+                expr new_arg = visit(arg);
+                if (!is_eqp(arg, new_arg))
+                    modified = true;
+                args[i] = new_arg;
+            }
+            if (!modified)
+                return e;
+            else
+                return mk_app(f, args);
+        }
+    }
+
+    virtual expr visit_binding(expr const & b) {
+        expr new_domain = visit(binding_domain(b));
+        expr l          = mk_local(m_tc.mk_fresh_name(), new_domain);
+        expr new_body   = abstract(visit(instantiate(binding_body(b), l)), l);
+        return update_binding(b, new_domain, new_body);
+    }
+
+public:
+    eta_expand_fn(environment const & env):m_env(env), m_tc(env, name_generator()) {}
+};
+
+expr eta_expand(environment const & env, expr const & e) {
+    return eta_expand_fn(env)(e);
+}
+}

src/compiler/eta_expansion.h

@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+namespace lean {
+/** \brief Return the eta expanded normal form for \c e.
+    \pre \c e does not contain variables nor metavariables. */
+expr eta_expand(environment const & env, expr const & e);
+}