From ba7f2849dc75ff7d621606a8863d733ae3438ee1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Nov 2019 11:48:02 -0700
Subject: [PATCH] chore: use aux recursor extension implemented in Lean

---
 src/library/aux_recursors.cpp | 90 ++++-------------------------------
 src/library/aux_recursors.h   |  3 --
 src/library/init_module.cpp   |  3 --
 3 files changed, 8 insertions(+), 88 deletions(-)

diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp
index a2b58aadb3..b40732436e 100644
--- a/src/library/aux_recursors.cpp
+++ b/src/library/aux_recursors.cpp
@@ -4,101 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <string>
 #include "library/aux_recursors.h"
-#include "library/constants.h"
-#include "library/module.h"
 
 namespace lean {
-struct aux_recursor_ext : public environment_extension {
-    name_set m_aux_recursor_set;
-    name_set m_no_confusion_set;
-};
-
-struct aux_recursor_ext_reg {
-    unsigned m_ext_id;
-    aux_recursor_ext_reg() { m_ext_id = environment::register_extension(new 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, new aux_recursor_ext(ext));
-}
-
-struct auxrec_modification : public modification {
-    LEAN_MODIFICATION("auxrec")
-
-    name m_decl;
-
-    auxrec_modification() {}
-    auxrec_modification(name const & decl) : m_decl(decl) {}
-
-    void perform(environment & env) const override {
-        aux_recursor_ext ext = get_extension(env);
-        ext.m_aux_recursor_set.insert(m_decl);
-        env = update(env, ext);
-    }
-
-    void serialize(serializer & s) const override {
-        s << m_decl;
-    }
-
-    static modification* deserialize(deserializer & d) {
-        return new auxrec_modification(read_name(d));
-    }
-};
-
-struct no_conf_modification : public modification {
-    LEAN_MODIFICATION("no_conf")
-
-    name m_decl;
-
-    no_conf_modification() {}
-    no_conf_modification(name const & decl) : m_decl(decl) {}
-
-    void perform(environment & env) const override {
-        aux_recursor_ext ext = get_extension(env);
-        ext.m_no_confusion_set.insert(m_decl);
-        env = update(env, ext);
-    }
-
-    void serialize(serializer & s) const override {
-        s << m_decl;
-    }
-
-    static modification* deserialize(deserializer & d) {
-        return new no_conf_modification(read_name(d));
-    }
-};
+extern "C" object * lean_mark_aux_recursor(object * env, object * n);
+extern "C" object * lean_mark_no_confusion(object * env, object * n);
+extern "C" uint8 lean_is_aux_recursor(object * env, object * n);
+extern "C" uint8 lean_is_no_confusion(object * env, object * n);
 
 environment add_aux_recursor(environment const & env, name const & r) {
-    return module::add_and_perform(env, new auxrec_modification(r));
+    return environment(lean_mark_aux_recursor(env.to_obj_arg(), r.to_obj_arg()));
 }
 
 environment add_no_confusion(environment const & env, name const & r) {
-    return module::add_and_perform(env, new no_conf_modification(r));
+    return environment(lean_mark_no_confusion(env.to_obj_arg(), r.to_obj_arg()));
 }
 
 bool is_aux_recursor(environment const & env, name const & r) {
-    return get_extension(env).m_aux_recursor_set.contains(r);
+    return lean_is_aux_recursor(env.to_obj_arg(), r.to_obj_arg());
 }
 
 bool is_no_confusion(environment const & env, name const & r) {
-    return get_extension(env).m_no_confusion_set.contains(r);
-}
-
-void initialize_aux_recursors() {
-    g_ext              = new aux_recursor_ext_reg();
-    auxrec_modification::init();
-    no_conf_modification::init();
-}
-
-void finalize_aux_recursors() {
-    auxrec_modification::finalize();
-    no_conf_modification::finalize();
-    delete g_ext;
+    return lean_is_no_confusion(env.to_obj_arg(), r.to_obj_arg());
 }
 }
diff --git a/src/library/aux_recursors.h b/src/library/aux_recursors.h
index 86774e40e1..2ece578fe9 100644
--- a/src/library/aux_recursors.h
+++ b/src/library/aux_recursors.h
@@ -16,7 +16,4 @@ environment add_no_confusion(environment const & env, name const & r);
     \see add_aux_recursor */
 bool is_aux_recursor(environment const & env, name const & n);
 bool is_no_confusion(environment const & env, name const & n);
-
-void initialize_aux_recursors();
-void finalize_aux_recursors();
 }
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index c665849b8d..c6a9d607f7 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -24,7 +24,6 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/pp_options.h"
 #include "library/user_recursors.h"
-#include "library/aux_recursors.h"
 #include "library/abstract_context_cache.h"
 #include "library/type_context.h"
 #include "library/local_context.h"
@@ -81,7 +80,6 @@ void initialize_library_module() {
     initialize_library_util();
     initialize_pp_options();
     initialize_user_recursors();
-    initialize_aux_recursors();
     initialize_app_builder();
     initialize_fun_info();
     initialize_abstract_context_cache();
@@ -97,7 +95,6 @@ void finalize_library_module() {
     finalize_abstract_context_cache();
     finalize_fun_info();
     finalize_app_builder();
-    finalize_aux_recursors();
     finalize_user_recursors();
     finalize_pp_options();
     finalize_library_util();