From 49a574dbbf5178989abef43280e808f62c07a477 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Sep 2015 17:12:32 -0700 Subject: [PATCH] refactor(compiler): rename elim_rec to preprocess_rec --- src/compiler/CMakeLists.txt | 3 +- src/compiler/elim_rec.h | 12 -------- .../{elim_rec.cpp => preprocess_rec.cpp} | 28 +++++++++++++------ src/compiler/preprocess_rec.h | 23 +++++++++++++++ src/frontends/lean/builtin_cmds.cpp | 6 ++-- src/init/init.cpp | 3 ++ 6 files changed, 50 insertions(+), 25 deletions(-) delete mode 100644 src/compiler/elim_rec.h rename src/compiler/{elim_rec.cpp => preprocess_rec.cpp} (66%) create mode 100644 src/compiler/preprocess_rec.h diff --git a/src/compiler/CMakeLists.txt b/src/compiler/CMakeLists.txt index 541261520d..360bff55de 100644 --- a/src/compiler/CMakeLists.txt +++ b/src/compiler/CMakeLists.txt @@ -1 +1,2 @@ -add_library(compiler OBJECT rec_args.cpp eta_expansion.cpp simp_pr1_rec.cpp elim_rec.cpp) +add_library(compiler OBJECT rec_args.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess_rec.cpp + init_module.cpp) diff --git a/src/compiler/elim_rec.h b/src/compiler/elim_rec.h deleted file mode 100644 index 3f67dc3c1f..0000000000 --- a/src/compiler/elim_rec.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -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/compiler/elim_rec.cpp b/src/compiler/preprocess_rec.cpp similarity index 66% rename from src/compiler/elim_rec.cpp rename to src/compiler/preprocess_rec.cpp index 47c0abc804..c9e61c2764 100644 --- a/src/compiler/elim_rec.cpp +++ b/src/compiler/preprocess_rec.cpp @@ -25,22 +25,24 @@ static expr expand_aux_recursors(environment const & env, expr const & e) { return normalize(*tc, e, cs); } -class elim_rec_fn { - environment m_env; - buffer & m_aux_decls; +static name * g_tmp_prefix = nullptr; + +class preprocess_rec_fn { + environment m_env; + buffer & m_aux_decls; bool check(declaration const & d, expr const & v) { type_checker tc(m_env); expr t = tc.check(v, d.get_univ_params()).first; if (!tc.is_def_eq(d.get_type(), t).first) - throw exception("elim_rec failed"); + throw exception("preprocess_rec failed"); return true; } public: - elim_rec_fn(environment const & env, buffer & aux_decls): m_env(env), m_aux_decls(aux_decls) {} + preprocess_rec_fn(environment const & env, buffer & aux_decls): m_env(env), m_aux_decls(aux_decls) {} - declaration operator()(declaration const & d) { + environment operator()(declaration const & d) { expr v = d.get_value(); v = expand_aux_recursors(m_env, v); v = eta_expand(m_env, v); @@ -48,11 +50,19 @@ public: ::pp(m_env, v); // TODO(Leo) check(d, v); - return d; + return m_env; } }; -declaration elim_rec(environment const & env, declaration const & d, buffer & aux_decls) { - return elim_rec_fn(env, aux_decls)(d); +environment preprocess_rec(environment const & env, declaration const & d, buffer & aux_decls) { + return preprocess_rec_fn(env, aux_decls)(d); +} + +void initialize_preprocess_rec() { + g_tmp_prefix = new name(name::mk_internal_unique_name()); +} + +void finalize_preprocess_rec() { + delete g_tmp_prefix; } } diff --git a/src/compiler/preprocess_rec.h b/src/compiler/preprocess_rec.h new file mode 100644 index 0000000000..f5814ac527 --- /dev/null +++ b/src/compiler/preprocess_rec.h @@ -0,0 +1,23 @@ +/* +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 Expand user-defined and auxiliary recursors, simplify declaration, + put definition in eta-expanded normal form, and + eliminate nested (recursive) recursor applications. + Each nested recursive application becomes a new definition. + + All new declarations are added to the resulting environment. + \remark The new declaration corresponding to \c d is in the last one in \c new_decls. +*/ +environment preprocess_rec(environment const & env, declaration const & d, buffer & new_decls); + +void initialize_preprocess_rec(); +void finalize_preprocess_rec(); +} diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 894ba6565f..5790413af9 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -35,7 +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 "compiler/preprocess_rec.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" #include "frontends/lean/calc.h" @@ -1055,8 +1055,8 @@ static environment init_hits_cmd(parser & p) { 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); + buffer aux_decls; + preprocess_rec(p.env(), d, aux_decls); return p.env(); } diff --git a/src/init/init.cpp b/src/init/init.cpp index 82761fc61a..52240ad9ee 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "library/tactic/init_module.h" #include "library/definitional/init_module.h" #include "library/print.h" +#include "compiler/init_module.h" #include "frontends/lean/init_module.h" #include "frontends/lua/register_modules.h" #include "init/init.h" @@ -37,12 +38,14 @@ void initialize() { initialize_tactic_module(); initialize_simplifier_module(); initialize_definitional_module(); + initialize_compiler_module(); initialize_frontend_lean_module(); register_modules(); } void finalize() { run_thread_finalizers(); finalize_frontend_lean_module(); + finalize_compiler_module(); finalize_definitional_module(); finalize_simplifier_module(); finalize_tactic_module();