max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use aux recursor extension implemented in Lean

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-02 11:48:02 -07:00
parent 1702579a76
commit ba7f2849dc
3 changed files with 8 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

90
src/library/aux_recursors.cpp
View file

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

3
src/library/aux_recursors.h
View file

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

3
src/library/init_module.cpp
View file

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