core(library/projection): switch to Lean implementation

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

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<projection_info> 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<projection_ext const &>(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<unsigned char>(raw(), 3*sizeof(object*), static_cast<unsigned char>(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<projection_info> 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<projection_info>(*info);
-    else
-        return optional<projection_info>();
+    return to_optional<projection_info>(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;
-}
 }

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<name const &>(cnstr_get_ref(*this, 0)); }
+    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
+    unsigned get_i() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
+    bool is_inst_implicit() const { return cnstr_get_scalar<unsigned char>(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();
 }