refactor(library/definitional/projection): move projection "database" to library/projection

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"

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})

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

src/library/definitional/projection.cpp

@@ -6,228 +6,18 @@ Author: Leonardo de Moura
 */
 #include <string>
 #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<projection_info> m_info;
-    projection_ext() {}
-};
-
-struct projection_ext_reg {
-    unsigned m_ext_id;
-    projection_ext_reg() {
-        m_ext_id = environment::register_extension(std::make_shared<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, std::make_shared<projection_ext>(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<void(asynch_update_fn const &)> &,
-                                   std::function<void(delayed_update_fn const &)> &) {
-    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<name> 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<name>(const_name(fn));
-    return optional<name>();
-}
-
-/** \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<name> 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<name>();
-    auto decl = env.find(const_name(f));
-    if (!decl || !decl->is_definition() || decl->is_opaque())
-        return optional<name>();
-    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<expr, constraint_seq> 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<expr> 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<expr> process_proj_arg(environment const & env, name const & c, expr const & s) {
-        if (optional<name> 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<expr> 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<expr> mk = process_proj_arg(env, info->m_constructor, s)) {
-            // efficient version
-            buffer<expr> 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<expr> 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.
 

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

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

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 <string>
+#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<projection_info> m_info;
+    projection_ext() {}
+};
+
+struct projection_ext_reg {
+    unsigned m_ext_id;
+    projection_ext_reg() {
+        m_ext_id = environment::register_extension(std::make_shared<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, std::make_shared<projection_ext>(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<void(asynch_update_fn const &)> &,
+                                   std::function<void(delayed_update_fn const &)> &) {
+    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<name> 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<name>(const_name(fn));
+    return optional<name>();
+}
+
+/** \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<name> 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<name>();
+    auto decl = env.find(const_name(f));
+    if (!decl || !decl->is_definition() || decl->is_opaque())
+        return optional<name>();
+    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<expr, constraint_seq> 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<expr> 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<expr> process_proj_arg(environment const & env, name const & c, expr const & s) {
+        if (optional<name> 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<expr> 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<expr> mk = process_proj_arg(env, info->m_constructor, s)) {
+            // efficient version
+            buffer<expr> 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<expr> 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;
+}
+}

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