feat(library,library/definitional): tag auxiliary recursors automatically generated by Lean

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)

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<aux_recursor_ext>()); }
+};
+
+static aux_recursor_ext_reg * g_ext = nullptr;
+static aux_recursor_ext const & get_extension(environment const & env) {
+    return static_cast<aux_recursor_ext const &>(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<aux_recursor_ext>(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<void(asynch_update_fn const &)> &,
+                                std::function<void(delayed_update_fn const &)> &) {
+    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;
+}
+}

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();
+}

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);
 }
 

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);
 }
 }

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);

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);
 }
 }

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();