feat(compiler,frontends/lean): add #compile command for debugging purposes, add compiler module

src/CMakeLists.txt

@@ -355,6 +355,8 @@ add_subdirectory(library/definitional)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
 add_subdirectory(library/error_handling)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:error_handling>)
+add_subdirectory(compiler)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
 add_subdirectory(frontends/lean)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:lean_frontend>)
 add_subdirectory(frontends/lua)

src/compiler/CMakeLists.txt

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

src/compiler/elim_rec.cpp

@@ -0,0 +1,42 @@
+/*
+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/declaration.h"
+#include "kernel/type_checker.h"
+#include "library/aux_recursors.h"
+#include "library/user_recursors.h"
+#include "library/normalize.h"
+#include "library/util.h"
+
+void pp(lean::environment const & env, lean::expr const & e);
+
+namespace lean {
+static expr expand_aux_recursors(environment const & env, expr const & e) {
+    auto tc = mk_type_checker(env, name_generator(), [=](name const & n) {
+            return !is_aux_recursor(env, n) && !is_user_defined_recursor(env, n);
+        });
+    constraint_seq cs;
+    return normalize(*tc, e, cs);
+}
+
+class elim_rec_fn {
+    environment           m_env;
+    buffer<declaration> & m_aux_decls;
+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());
+        ::pp(m_env, v);
+        // TODO(Leo)
+        return d;
+    }
+};
+
+declaration elim_rec(environment const & env, declaration const & d, buffer<declaration> & aux_decls) {
+    return elim_rec_fn(env, aux_decls)(d);
+}
+}

src/compiler/elim_rec.h

@@ -0,0 +1,12 @@
+/*
+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 {
+declaration elim_rec(environment const & env, declaration const & d, buffer<declaration> & aux_decls);
+}

src/frontends/lean/builtin_cmds.cpp

@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "library/composition_manager.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
+#include "compiler/elim_rec.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/calc.h"
@@ -1051,6 +1052,14 @@ static environment init_hits_cmd(parser & p) {
     return module::declare_hits(p.env());
 }
 
+static environment compile_cmd(parser & p) {
+    name n = p.check_constant_next("invalid #compile command, constant expected");
+    declaration d = p.env().get(n);
+    buffer<declaration> aux_decls;
+    elim_rec(p.env(), d, aux_decls);
+    return p.env();
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",          "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -1074,6 +1083,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#erase_cache",  "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
     add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));
+    add_cmd(r, cmd_info("#compile",      "(for debugging purposes)", compile_cmd));
     register_decl_cmds(r);
     register_inductive_cmd(r);
     register_structure_cmd(r);

src/frontends/lean/token_table.cpp

@@ -120,7 +120,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         nullptr};
+         "#compile", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},