From 8666c92bae5a80dce8fd17ee4cea5172858b87eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Sep 2015 10:08:54 -0700 Subject: [PATCH] feat(library,library/definitional): tag auxiliary recursors automatically generated by Lean --- src/library/CMakeLists.txt | 2 +- src/library/aux_recursors.cpp | 64 +++++++++++++++++++++++ src/library/aux_recursors.h | 20 +++++++ src/library/definitional/brec_on.cpp | 2 + src/library/definitional/cases_on.cpp | 2 + src/library/definitional/induction_on.cpp | 2 + src/library/definitional/rec_on.cpp | 2 + src/library/init_module.cpp | 3 ++ 8 files changed, 96 insertions(+), 1 deletion(-) create mode 100644 src/library/aux_recursors.cpp create mode 100644 src/library/aux_recursors.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index b3a698a06..79bf7b8d7 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -15,4 +15,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp relation_manager.cpp export.cpp user_recursors.cpp class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp - tc_multigraph.cpp noncomputable.cpp) + tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp) diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp new file mode 100644 index 000000000..002777e81 --- /dev/null +++ b/src/library/aux_recursors.cpp @@ -0,0 +1,64 @@ +/* +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 "library/aux_recursors.h" +#include "library/scoped_ext.h" +#include "library/module.h" + +namespace lean { +struct aux_recursor_ext : public environment_extension { + name_set m_set; +}; + +struct aux_recursor_ext_reg { + unsigned m_ext_id; + aux_recursor_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static aux_recursor_ext_reg * g_ext = nullptr; +static aux_recursor_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext->m_ext_id)); +} +static environment update(environment const & env, aux_recursor_ext const & ext) { + return env.update(g_ext->m_ext_id, std::make_shared(ext)); +} + +static std::string * g_prv_key = nullptr; + +environment add_aux_recursor(environment const & env, name const & r) { + aux_recursor_ext ext = get_extension(env); + ext.m_set.insert(r); + environment new_env = update(env, ext); + return module::add(new_env, *g_prv_key, [=](environment const &, serializer & s) { s << r; }); +} + +bool is_aux_recursor(environment const & env, name const & r) { + return get_extension(env).m_set.contains(r); +} + +static void aux_recursor_reader(deserializer & d, shared_environment & senv, + std::function &, + std::function &) { + name r; + d >> r; + senv.update([=](environment const & env) -> environment { + aux_recursor_ext ext = get_extension(env); + ext.m_set.insert(r); + return update(env, ext); + }); +} + +void initialize_aux_recursors() { + g_ext = new aux_recursor_ext_reg(); + g_prv_key = new std::string("auxrec"); + register_module_object_reader(*g_prv_key, aux_recursor_reader); +} + +void finalize_aux_recursors() { + delete g_prv_key; + delete g_ext; +} +} diff --git a/src/library/aux_recursors.h b/src/library/aux_recursors.h new file mode 100644 index 000000000..eb170174c --- /dev/null +++ b/src/library/aux_recursors.h @@ -0,0 +1,20 @@ +/* +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 Mark \c r as an auxiliary recursor automatically created by the system. + We use it to mark recursors such as brec_on, rec_on, induction_on, etc. */ +environment add_aux_recursor(environment const & env, name const & r); +/** \brief Return true iff \c n is the name of an auxiliary recursor. + \see add_aux_recursor */ +bool is_aux_recursor(environment const & env, name const & n); + +void initialize_aux_recursors(); +void finalize_aux_recursors(); +} diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index c5683b64f..282edd865 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/bin_app.h" #include "library/util.h" #include "library/normalize.h" +#include "library/aux_recursors.h" namespace lean { static void throw_corrupted(name const & n) { @@ -334,6 +335,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible); if (!ind) new_env = add_unfold_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); + new_env = add_aux_recursor(new_env, brec_on_name); return add_protected(new_env, brec_on_name); } diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 6fe4628f3..725b26847 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/constants.h" #include "library/normalize.h" +#include "library/aux_recursors.h" namespace lean { static void throw_corrupted(name const & n) { @@ -183,6 +184,7 @@ environment mk_cases_on(environment const & env, name const & n) { environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible); new_env = add_unfold_hint(new_env, cases_on_name, cases_on_major_idx); + new_env = add_aux_recursor(new_env, cases_on_name); return add_protected(new_env, cases_on_name); } } diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp index 6a8ce3071..a88848de9 100644 --- a/src/library/definitional/induction_on.cpp +++ b/src/library/definitional/induction_on.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/protected.h" #include "library/util.h" +#include "library/aux_recursors.h" namespace lean { environment mk_induction_on(environment const & env, name const & n) { @@ -43,6 +44,7 @@ environment mk_induction_on(environment const & env, name const & n) { mk_definition(new_env, induction_on_name, induction_on_univs, induction_on_type, induction_on_value, use_conv_opt)); + new_env = add_aux_recursor(new_env, induction_on_name); new_env = module::add(new_env, cdecl); } return add_protected(new_env, induction_on_name); diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index 6dc7b4210..a2ecc09f6 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/protected.h" #include "library/normalize.h" +#include "library/aux_recursors.h" namespace lean { environment mk_rec_on(environment const & env, name const & n) { @@ -59,6 +60,7 @@ environment mk_rec_on(environment const & env, name const & n) { rec_on_type, rec_on_val, use_conv_opt))); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible); new_env = add_unfold_hint(new_env, rec_on_name, rec_on_major_idx); + new_env = add_aux_recursor(new_env, rec_on_name); return add_protected(new_env, rec_on_name); } } diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 0cdda071f..57fff7ea0 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -41,6 +41,7 @@ Author: Leonardo de Moura #include "library/class_instance_synth.h" #include "library/composition_manager.h" #include "library/noncomputable.h" +#include "library/aux_recursors.h" namespace lean { void initialize_library_module() { @@ -81,9 +82,11 @@ void initialize_library_module() { initialize_class_instance_elaborator(); initialize_composition_manager(); initialize_noncomputable(); + initialize_aux_recursors(); } void finalize_library_module() { + finalize_aux_recursors(); finalize_noncomputable(); finalize_composition_manager(); finalize_class_instance_elaborator();