From b31ab7d77a409062343924c46059b12e9f168960 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Sep 2015 10:49:07 -0700 Subject: [PATCH] feat(compiler,frontends/lean): add #compile command for debugging purposes, add compiler module --- src/CMakeLists.txt | 2 ++ src/compiler/CMakeLists.txt | 1 + src/compiler/elim_rec.cpp | 42 +++++++++++++++++++++++++++++ src/compiler/elim_rec.h | 12 +++++++++ src/frontends/lean/builtin_cmds.cpp | 10 +++++++ src/frontends/lean/token_table.cpp | 2 +- 6 files changed, 68 insertions(+), 1 deletion(-) create mode 100644 src/compiler/CMakeLists.txt create mode 100644 src/compiler/elim_rec.cpp create mode 100644 src/compiler/elim_rec.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1a6da0e02..e013ceb35 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -355,6 +355,8 @@ add_subdirectory(library/definitional) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/error_handling) set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(compiler) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lean) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lua) diff --git a/src/compiler/CMakeLists.txt b/src/compiler/CMakeLists.txt new file mode 100644 index 000000000..d74727555 --- /dev/null +++ b/src/compiler/CMakeLists.txt @@ -0,0 +1 @@ +add_library(compiler OBJECT elim_rec.cpp) diff --git a/src/compiler/elim_rec.cpp b/src/compiler/elim_rec.cpp new file mode 100644 index 000000000..8ab2af5e9 --- /dev/null +++ b/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 & m_aux_decls; +public: + elim_rec_fn(environment const & env, buffer & 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 & aux_decls) { + return elim_rec_fn(env, aux_decls)(d); +} +} diff --git a/src/compiler/elim_rec.h b/src/compiler/elim_rec.h new file mode 100644 index 000000000..3f67dc3c1 --- /dev/null +++ b/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 & aux_decls); +} diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 794037ba0..894ba6565 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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 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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 3c386217c..7a6b4daf7 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},