From c92f3bec65bb682e599990c5cca37ee26ec53622 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 07:06:32 -0800 Subject: [PATCH] refactor(library/definitional/projection): move projection "database" to library/projection --- src/frontends/lean/structure_cmd.cpp | 1 + src/library/CMakeLists.txt | 2 +- src/library/definitional/init_module.cpp | 3 - src/library/definitional/projection.cpp | 214 +-------------------- src/library/definitional/projection.h | 36 ---- src/library/init_module.cpp | 3 + src/library/projection.cpp | 226 +++++++++++++++++++++++ src/library/projection.h | 58 ++++++ 8 files changed, 291 insertions(+), 252 deletions(-) create mode 100644 src/library/projection.cpp create mode 100644 src/library/projection.h diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index ba0a4c78c2..6494c78bd0 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -30,6 +30,7 @@ Author: Leonardo de Moura #include "library/class.h" #include "library/constants.h" #include "library/util.h" +#include "library/projection.h" #include "library/kernel_serializer.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 61095271bf..1b81dc045d 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -12,6 +12,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp metavar_closure.cpp reducible.cpp init_module.cpp generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp - app_builder.cpp) + app_builder.cpp projection.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/definitional/init_module.cpp b/src/library/definitional/init_module.cpp index 1da2a1fdc7..fd527cbad1 100644 --- a/src/library/definitional/init_module.cpp +++ b/src/library/definitional/init_module.cpp @@ -6,16 +6,13 @@ 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 9d4cad375f..172fcfb777 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -6,228 +6,18 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" -#include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/type_checker.h" +#include "kernel/instantiate.h" #include "kernel/kernel_exception.h" #include "kernel/inductive/inductive.h" #include "library/reducible.h" +#include "library/projection.h" #include "library/module.h" #include "library/util.h" -#include "library/kernel_serializer.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_info_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); - }); -} - -/** \brief If \c e is a constructor application, then return the name of the constructor. - Otherwise, return none. -*/ -optional is_constructor_app(environment const & env, expr const & e) { - expr const & fn = get_app_fn(e); - if (is_constant(fn)) - if (auto I = inductive::is_intro_rule(env, const_name(fn))) - return optional(const_name(fn)); - return optional(); -} - -/** \brief If \c e is a constructor application, or a definition that wraps a - constructor application, then return the name of the constructor. - Otherwise, return none. -*/ -optional is_constructor_app_ext(environment const & env, expr const & e) { - if (auto r = is_constructor_app(env, e)) - return r; - expr const & f = get_app_fn(e); - if (!is_constant(f)) - return optional(); - auto decl = env.find(const_name(f)); - if (!decl || !decl->is_definition() || decl->is_opaque()) - return optional(); - expr const * it = &decl->get_value(); - while (is_lambda(*it)) - it = &binding_body(*it); - return is_constructor_app_ext(env, *it); -} - -static name * g_projection_macro_name = nullptr; -static std::string * g_projection_opcode = nullptr; - -class projection_macro_definition_cell : public macro_definition_cell { - name m_proj_name; - void check_macro(expr const & m) const { - if (!is_macro(m) || macro_num_args(m) != 1) - throw exception(sstream() << "invalid '" << m_proj_name - << "' projection macro, incorrect number of arguments"); - } - -public: - projection_macro_definition_cell(name const & n):m_proj_name(n) {} - name const & get_proj_name() const { return m_proj_name; } - virtual name get_name() const { return m_proj_name; } // *g_projection_macro_name; } - virtual format pp(formatter const &) const { return format(m_proj_name); } - virtual void display(std::ostream & out) const { out << m_proj_name; } - - virtual pair get_type(expr const & m, extension_context & ctx) const { - check_macro(m); - environment const & env = ctx.env(); - constraint_seq cs; - expr s = macro_arg(m, 0); - expr s_t = ctx.whnf(ctx.infer_type(s, cs), cs); - buffer I_args; - expr const & I = get_app_args(s_t, I_args); - if (is_constant(I)) { - declaration proj_decl = env.get(m_proj_name); - if (length(const_levels(I)) != proj_decl.get_num_univ_params()) - throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name - << "', incorrect number of universe parameters", m); - expr t = instantiate_type_univ_params(proj_decl, const_levels(I)); - I_args.push_back(s); - unsigned num = I_args.size(); - for (unsigned i = 0; i < num; i++) { - if (!is_pi(t)) - throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name - << "', number of arguments mismatch", m); - t = binding_body(t); - } - return mk_pair(instantiate_rev(t, I_args.size(), I_args.data()), cs); - } else { - // TODO(Leo) - throw_kernel_exception(env, sstream() << "projection macros do not support arbitrary terms " - << "containing metavariables yet (solution: use trust-level 0)", m); - } - } - - // try to unfold projection argument into a \c c constructor application - static optional process_proj_arg(environment const & env, name const & c, expr const & s) { - if (optional mk_name = is_constructor_app_ext(env, s)) { - if (*mk_name == c) { - expr new_s = s; - while (is_app(new_s) && !is_constructor_app(env, new_s)) { - if (auto next_new_s = unfold_app(env, new_s)) - new_s = *next_new_s; - else - return none_expr(); - } - if (is_app(new_s)) - return some_expr(new_s); - } - } - return none_expr(); - } - - virtual optional expand(expr const & m, extension_context & ctx) const { - check_macro(m); - environment const & env = ctx.env(); - auto info = get_projection_info(env, m_proj_name); - if (!info) - throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name - << "', constant is not a projection function", m); - expr const & s = macro_arg(m, 0); - if (optional mk = process_proj_arg(env, info->m_constructor, s)) { - // efficient version - buffer mk_args; - get_app_args(*mk, mk_args); - unsigned i = info->m_nparams + info->m_i; - lean_assert(i < mk_args.size()); - return some_expr(mk_args[i]); - } else { - // use definition - constraint_seq cs; - expr s_t = ctx.whnf(ctx.infer_type(s, cs), cs); - if (cs) - return none_expr(); - buffer I_args; - expr const & I = get_app_args(s_t, I_args); - if (!is_constant(I)) - return none_expr(); - return some_expr(mk_app(mk_app(mk_constant(m_proj_name, const_levels(I)), I_args), s)); - } - } - - virtual void write(serializer & s) const { - s.write_string(*g_projection_opcode); - s << m_proj_name; - } -}; - -expr mk_projection_macro(name const & proj_name, expr const & e) { - macro_definition def(new projection_macro_definition_cell(proj_name)); - return mk_macro(def, 1, &e); -} - -void initialize_projection() { - g_ext = new projection_ext_reg(); - g_proj_key = new std::string("proj"); - register_module_object_reader(*g_proj_key, projection_info_reader); - g_projection_macro_name = new name("projection"); - g_projection_opcode = new std::string("Proj"); - register_macro_deserializer(*g_projection_opcode, - [](deserializer & d, unsigned num, expr const * args) { - if (num != 1) - throw corrupted_stream_exception(); - name proj_name; - d >> proj_name; - return mk_projection_macro(proj_name, args[0]); - }); -} - -void finalize_projection() { - delete g_proj_key; - delete g_ext; - delete g_projection_macro_name; - delete g_projection_opcode; -} - /** \brief Return true iff the type named \c S can be viewed as a structure in the given environment. diff --git a/src/library/definitional/projection.h b/src/library/definitional/projection.h index 264df62756..ce673a2001 100644 --- a/src/library/definitional/projection.h +++ b/src/library/definitional/projection.h @@ -29,40 +29,4 @@ environment mk_projections(environment const & env, name const & n, If not, generate an error message using \c pos. */ bool is_structure(environment const & env, name const & S); - -/** \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); - -/** \brief Create a projection macro term that can peform the following reduction efficiently - - pr_i A (mk A f_1 ... f_n) ==> f_i - - \remark proj_name is the name of the definition that implements the actual projection. -*/ -expr mk_projection_macro(name const & proj_name, expr const & e); - -void initialize_projection(); -void finalize_projection(); } diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 699ceff613..ead8cb2e3d 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "library/fingerprint.h" #include "library/util.h" #include "library/pp_options.h" +#include "library/projection.h" namespace lean { void initialize_library_module() { @@ -65,9 +66,11 @@ void initialize_library_module() { initialize_class(); initialize_library_util(); initialize_pp_options(); + initialize_projection(); } void finalize_library_module() { + finalize_projection(); finalize_pp_options(); finalize_library_util(); finalize_class(); diff --git a/src/library/projection.cpp b/src/library/projection.cpp new file mode 100644 index 0000000000..881aa5f84b --- /dev/null +++ b/src/library/projection.cpp @@ -0,0 +1,226 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/sstream.h" +#include "kernel/kernel_exception.h" +#include "kernel/instantiate.h" +#include "library/util.h" +#include "library/projection.h" +#include "library/module.h" +#include "library/kernel_serializer.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); +} + +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_info_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); + }); +} + +/** \brief If \c e is a constructor application, then return the name of the constructor. + Otherwise, return none. +*/ +optional is_constructor_app(environment const & env, expr const & e) { + expr const & fn = get_app_fn(e); + if (is_constant(fn)) + if (auto I = inductive::is_intro_rule(env, const_name(fn))) + return optional(const_name(fn)); + return optional(); +} + +/** \brief If \c e is a constructor application, or a definition that wraps a + constructor application, then return the name of the constructor. + Otherwise, return none. +*/ +optional is_constructor_app_ext(environment const & env, expr const & e) { + if (auto r = is_constructor_app(env, e)) + return r; + expr const & f = get_app_fn(e); + if (!is_constant(f)) + return optional(); + auto decl = env.find(const_name(f)); + if (!decl || !decl->is_definition() || decl->is_opaque()) + return optional(); + expr const * it = &decl->get_value(); + while (is_lambda(*it)) + it = &binding_body(*it); + return is_constructor_app_ext(env, *it); +} + +static name * g_projection_macro_name = nullptr; +static std::string * g_projection_opcode = nullptr; + +class projection_macro_definition_cell : public macro_definition_cell { + name m_proj_name; + void check_macro(expr const & m) const { + if (!is_macro(m) || macro_num_args(m) != 1) + throw exception(sstream() << "invalid '" << m_proj_name + << "' projection macro, incorrect number of arguments"); + } + +public: + projection_macro_definition_cell(name const & n):m_proj_name(n) {} + name const & get_proj_name() const { return m_proj_name; } + virtual name get_name() const { return m_proj_name; } // *g_projection_macro_name; } + virtual format pp(formatter const &) const { return format(m_proj_name); } + virtual void display(std::ostream & out) const { out << m_proj_name; } + + virtual pair get_type(expr const & m, extension_context & ctx) const { + check_macro(m); + environment const & env = ctx.env(); + constraint_seq cs; + expr s = macro_arg(m, 0); + expr s_t = ctx.whnf(ctx.infer_type(s, cs), cs); + buffer I_args; + expr const & I = get_app_args(s_t, I_args); + if (is_constant(I)) { + declaration proj_decl = env.get(m_proj_name); + if (length(const_levels(I)) != proj_decl.get_num_univ_params()) + throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name + << "', incorrect number of universe parameters", m); + expr t = instantiate_type_univ_params(proj_decl, const_levels(I)); + I_args.push_back(s); + unsigned num = I_args.size(); + for (unsigned i = 0; i < num; i++) { + if (!is_pi(t)) + throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name + << "', number of arguments mismatch", m); + t = binding_body(t); + } + return mk_pair(instantiate_rev(t, I_args.size(), I_args.data()), cs); + } else { + // TODO(Leo) + throw_kernel_exception(env, sstream() << "projection macros do not support arbitrary terms " + << "containing metavariables yet (solution: use trust-level 0)", m); + } + } + + // try to unfold projection argument into a \c c constructor application + static optional process_proj_arg(environment const & env, name const & c, expr const & s) { + if (optional mk_name = is_constructor_app_ext(env, s)) { + if (*mk_name == c) { + expr new_s = s; + while (is_app(new_s) && !is_constructor_app(env, new_s)) { + if (auto next_new_s = unfold_app(env, new_s)) + new_s = *next_new_s; + else + return none_expr(); + } + if (is_app(new_s)) + return some_expr(new_s); + } + } + return none_expr(); + } + + virtual optional expand(expr const & m, extension_context & ctx) const { + check_macro(m); + environment const & env = ctx.env(); + auto info = get_projection_info(env, m_proj_name); + if (!info) + throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name + << "', constant is not a projection function", m); + expr const & s = macro_arg(m, 0); + if (optional mk = process_proj_arg(env, info->m_constructor, s)) { + // efficient version + buffer mk_args; + get_app_args(*mk, mk_args); + unsigned i = info->m_nparams + info->m_i; + lean_assert(i < mk_args.size()); + return some_expr(mk_args[i]); + } else { + // use definition + constraint_seq cs; + expr s_t = ctx.whnf(ctx.infer_type(s, cs), cs); + if (cs) + return none_expr(); + buffer I_args; + expr const & I = get_app_args(s_t, I_args); + if (!is_constant(I)) + return none_expr(); + return some_expr(mk_app(mk_app(mk_constant(m_proj_name, const_levels(I)), I_args), s)); + } + } + + virtual void write(serializer & s) const { + s.write_string(*g_projection_opcode); + s << m_proj_name; + } +}; + +expr mk_projection_macro(name const & proj_name, expr const & e) { + macro_definition def(new projection_macro_definition_cell(proj_name)); + return mk_macro(def, 1, &e); +} + +void initialize_projection() { + g_ext = new projection_ext_reg(); + g_proj_key = new std::string("proj"); + register_module_object_reader(*g_proj_key, projection_info_reader); + g_projection_macro_name = new name("projection"); + g_projection_opcode = new std::string("Proj"); + register_macro_deserializer(*g_projection_opcode, + [](deserializer & d, unsigned num, expr const * args) { + if (num != 1) + throw corrupted_stream_exception(); + name proj_name; + d >> proj_name; + return mk_projection_macro(proj_name, args[0]); + }); +} + +void finalize_projection() { + delete g_proj_key; + delete g_ext; + delete g_projection_macro_name; + delete g_projection_opcode; +} +} diff --git a/src/library/projection.h b/src/library/projection.h new file mode 100644 index 0000000000..0e630e1c59 --- /dev/null +++ b/src/library/projection.h @@ -0,0 +1,58 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/** \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 + + We also use this information in the rewriter/simplifier. +*/ +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 Mark \c p as a projection in the given environment and store that + \c mk is the constructor associated with it, \c nparams is the number of parameters, and + \c i says that \c p is the i-th projection. +*/ +environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned 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); + +inline bool is_projection(environment const & env, name const & n) { + return get_projection_info(env, n) != nullptr; +} + +/** \brief Create a projection macro term that can peform the following reduction efficiently + + pr_i A (mk A f_1 ... f_n) ==> f_i + + \remark proj_name is the name of the definition that implements the actual projection. +*/ +expr mk_projection_macro(name const & proj_name, expr const & e); + +void initialize_projection(); +void finalize_projection(); +}