diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 5393794f26..a8a39a9c94 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -23,7 +23,6 @@ Author: Leonardo de Moura #include "library/print.h" #include "library/util.h" #include "library/pp_options.h" -#include "library/projection.h" #include "library/user_recursors.h" #include "library/aux_recursors.h" #include "library/abstract_context_cache.h" @@ -86,7 +85,6 @@ void initialize_library_module() { initialize_class(); initialize_library_util(); initialize_pp_options(); - initialize_projection(); initialize_user_recursors(); initialize_aux_recursors(); initialize_app_builder(); @@ -110,7 +108,6 @@ void finalize_library_module() { finalize_app_builder(); finalize_aux_recursors(); finalize_user_recursors(); - finalize_projection(); finalize_pp_options(); finalize_library_util(); finalize_class(); diff --git a/src/library/projection.cpp b/src/library/projection.cpp index 1a39bcd9d2..59b5717322 100644 --- a/src/library/projection.cpp +++ b/src/library/projection.cpp @@ -11,89 +11,32 @@ Author: Leonardo de Moura #include "kernel/inductive.h" #include "library/util.h" #include "library/projection.h" -#include "library/module.h" namespace lean { -/** \brief This environment extension stores information about all projection functions - defined in an environment object. -*/ -struct projection_ext : public environment_extension { - name_map m_info; - projection_ext() {} -}; - -struct projection_ext_reg { - unsigned m_ext_id; - projection_ext_reg() { - m_ext_id = environment::register_extension(new projection_ext()); - } -}; - -static projection_ext_reg * g_ext = nullptr; -static projection_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext->m_ext_id)); -} -static environment update(environment const & env, projection_ext const & ext) { - return env.update(g_ext->m_ext_id, new projection_ext(ext)); +projection_info::projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit): + object_ref(mk_cnstr(0, c, nat(nparams), nat(i))) { + cnstr_set_scalar(raw(), 3*sizeof(object*), static_cast(inst_implicit)); } -struct proj_modification : public modification { - LEAN_MODIFICATION("proj") - - name m_proj; - projection_info m_info; - - proj_modification() {} - proj_modification(name const & proj, projection_info const & info) : m_proj(proj), m_info(info) {} - - void perform(environment & env) const override { - projection_ext ext = get_extension(env); - ext.m_info.insert(m_proj, m_info); - env = update(env, ext); - } - - void serialize(serializer & s) const override { - s << m_proj << m_info.m_constructor << m_info.m_nparams << m_info.m_i << m_info.m_inst_implicit; - } - - static modification* deserialize(deserializer & d) { - name p, mk; unsigned nparams, i; bool inst_implicit; - d >> p >> mk >> nparams >> i >> inst_implicit; - return new proj_modification(p, projection_info(mk, nparams, i, inst_implicit)); - } -}; +object* add_projection_info_core(object* env, object* p, object* ctor, object* nparams, object* i, uint8 fromClass); +object* get_projection_info_core(object* env, object* p); environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) { - return module::add_and_perform(env, new proj_modification(p, projection_info(mk, nparams, i, inst_implicit))); + return environment(add_projection_info_core(env.to_obj_arg(), p.to_obj_arg(), mk.to_obj_arg(), mk_nat_obj(nparams), mk_nat_obj(i), inst_implicit)); } optional get_projection_info(environment const & env, name const & p) { - projection_ext const & ext = get_extension(env); - if (auto info = ext.m_info.find(p)) - return optional(*info); - else - return optional(); + return to_optional(get_projection_info_core(env.to_obj_arg(), p.to_obj_arg())); } /** \brief Return true iff the type named \c S can be viewed as a structure in the given environment. - If not, generate an error message using \c pos. -*/ + If not, generate an error message using \c pos. */ bool is_structure_like(environment const & env, name const & S) { constant_info S_info = env.get(S); if (!S_info.is_inductive()) return false; inductive_val S_val = S_info.to_inductive_val(); return length(S_val.get_cnstrs()) == 1 && S_val.get_nindices() == 0; } - -void initialize_projection() { - g_ext = new projection_ext_reg(); - proj_modification::init(); -} - -void finalize_projection() { - proj_modification::finalize(); - delete g_ext; -} } diff --git a/src/library/projection.h b/src/library/projection.h index deb105f673..72c176acaf 100644 --- a/src/library/projection.h +++ b/src/library/projection.h @@ -19,20 +19,22 @@ namespace lean { We also use this information in the rewriter/simplifier. */ -class projection_info { - name m_constructor; // mk in the rule above - unsigned m_nparams; // number of parameters of the inductive datatype - unsigned m_i; // i in the rule above - bool m_inst_implicit; // true if it is the projection of a "class" - friend struct proj_modification; +class projection_info : public object_ref { public: - projection_info() {} - projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit): - m_constructor(c), m_nparams(nparams), m_i(i), m_inst_implicit(inst_implicit) {} - name const & get_constructor() const { return m_constructor; } - unsigned get_nparams() const { return m_nparams; } - unsigned get_i() const { return m_i; } - bool is_inst_implicit() const { return m_inst_implicit; } + projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit); + projection_info():projection_info(name(), 0, 0, false) {} + projection_info(projection_info const & other):object_ref(other) {} + projection_info(projection_info && other):object_ref(other) {} + /* low-level constructors */ + explicit projection_info(object * o):object_ref(o) {} + explicit projection_info(b_obj_arg o, bool b):object_ref(o, b) {} + explicit projection_info(object_ref const & o):object_ref(o) {} + projection_info & operator=(projection_info const & other) { object_ref::operator=(other); return *this; } + projection_info & operator=(projection_info && other) { object_ref::operator=(other); return *this; } + name const & get_constructor() const { return static_cast(cnstr_get_ref(*this, 0)); } + unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 1)).get_small_value(); } + unsigned get_i() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } + bool is_inst_implicit() const { return cnstr_get_scalar(raw(), sizeof(object*)*3) != 0; } }; /** \brief Mark \c p as a projection in the given environment and store that @@ -58,7 +60,4 @@ inline bool is_projection(environment const & env, name const & n) { If not, generate an error message using \c pos. */ bool is_structure_like(environment const & env, name const & S); - -void initialize_projection(); -void finalize_projection(); }