From 858d21f20bd2767346d3c19a7ee20d54d607c044 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Jan 2015 16:26:56 -0800 Subject: [PATCH] feat(library/definitional/projection): store projection information --- src/library/definitional/init_module.cpp | 3 ++ src/library/definitional/projection.cpp | 65 ++++++++++++++++++++++++ src/library/definitional/projection.h | 28 ++++++++++ 3 files changed, 96 insertions(+) diff --git a/src/library/definitional/init_module.cpp b/src/library/definitional/init_module.cpp index fd527cbad..1da2a1fdc 100644 --- a/src/library/definitional/init_module.cpp +++ b/src/library/definitional/init_module.cpp @@ -6,13 +6,16 @@ Author: Leonardo de Moura */ #include "library/util.h" #include "library/definitional/equations.h" +#include "library/definitional/projection.h" namespace lean{ void initialize_definitional_module() { initialize_equations(); + initialize_projection(); } void finalize_definitional_module() { + finalize_projection(); finalize_equations(); } } diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 26790b8ff..5e241b8e8 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/sstream.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -11,8 +12,71 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/reducible.h" #include "library/module.h" +#include "library/definitional/projection.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(std::make_shared()); + } +}; + +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, std::make_shared(ext)); +} + +static std::string * g_proj_key = nullptr; + +static environment save_projection_info_core(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i) { + projection_ext ext = get_extension(env); + ext.m_info.insert(p, projection_info(mk, nparams, i)); + return update(env, ext); +} + +static environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i) { + environment new_env = save_projection_info_core(env, p, mk, nparams, i); + return module::add(new_env, *g_proj_key, [=](serializer & s) { s << p << mk << nparams << i; }); +} + +projection_info const * get_projection_info(environment const & env, name const & p) { + projection_ext const & ext = get_extension(env); + return ext.m_info.find(p); +} + +static void projection_reader(deserializer & d, module_idx, shared_environment & senv, + std::function &, + std::function &) { + name p, mk; unsigned nparams, i; + d >> p >> mk >> nparams >> i; + senv.update([=](environment const & env) -> environment { + return save_projection_info_core(env, p, mk, nparams, i); + }); +} + +void initialize_projection() { + g_ext = new projection_ext_reg(); + g_proj_key = new std::string("proj"); + register_module_object_reader(*g_proj_key, projection_reader); +} + +void finalize_projection() { + delete g_proj_key; + delete g_ext; +} + [[ noreturn ]] static void throw_ill_formed(name const & n) { throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype"); } @@ -116,6 +180,7 @@ environment mk_projections(environment const & env, name const & n, buffer opaque, rec_decl.get_module_idx(), use_conv_opt); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, proj_name, reducible_status::On); + new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); intro_type = instantiate(binding_body(intro_type), proj); i++; diff --git a/src/library/definitional/projection.h b/src/library/definitional/projection.h index 73af63718..cbe2d4c60 100644 --- a/src/library/definitional/projection.h +++ b/src/library/definitional/projection.h @@ -10,4 +10,32 @@ Author: Leonardo de Moura namespace lean { environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit = false); environment mk_projections(environment const & env, name const & n, bool inst_implicit = false); + +/** \brief Auxiliary information attached to projections. This information + is used to simplify projection over constructor (efficiently) + + That is, given a projection pr_i associated with the constructor mk + where A are parameters, we want to implement the following reduction + efficiently. The idea is to avoid unfolding pr_i. + + pr_i A (mk A f_1 ... f_n) ==> f_i + +*/ +struct 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 + projection_info() {} + projection_info(name const & c, unsigned nparams, unsigned i): + m_constructor(c), m_nparams(nparams), m_i(i) {} +}; + +/** \brief If \c p is a projection in the given environment, then return the information + associated with it (constructor, number of parameters, and index). + If \c p is not a projection, then return nullptr. +*/ +projection_info const * get_projection_info(environment const & env, name const & p); + +void initialize_projection(); +void finalize_projection(); }