feat(kernel): add add_meta

src/kernel/environment.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "runtime/thread.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/type_checker.h"
 
 namespace lean {
 environment_header::environment_header(unsigned trust_lvl, std::unique_ptr<normalizer_extension const> ext):
@@ -108,6 +109,20 @@ environment environment::add(certified_declaration const & d) const {
     return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_extensions);
 }
 
+environment environment::add_meta(buffer<declaration> const & ds) const {
+    environment new_env = *this;
+    /* Check declarations header, and add them to new_env.m_declarations */
+    for (declaration const & d : ds) {
+        check_decl_type(new_env, d);
+        new_env.m_declarations.insert(d.get_name(), d);
+    }
+    /* Check actual definitions */
+    for (declaration const & d : ds) {
+        check_decl_value(new_env, d);
+    }
+    return new_env;
+}
+
 environment environment::replace(certified_declaration const & t) const {
     if (!m_id.is_descendant(t.get_id()))
         throw_incompatible_environment(*this);

src/kernel/environment.h

@@ -156,6 +156,12 @@ public:
           - The environment does not contain an axiom named <tt>t.get_declaration().get_name()</tt> */
     environment replace(certified_declaration const & t) const;
 
+    /** \brief Add a sequence of (possibly mutually recursive) meta declarations.
+        The type checking occurs in two phases:
+        1- We type check each declaration type and add to a new environment.
+        2- We type check the definitions body. */
+    environment add_meta(buffer<declaration> const & ds) const;
+
     /** \brief Register an environment extension. Every environment
         object may contain this extension. The argument \c initial is
         the initial value for the new extensions. The extension object

src/kernel/type_checker.cpp

@@ -757,14 +757,32 @@ static void check_definition(environment const & env, declaration const & d, typ
     }
 }
 
-certified_declaration check(environment const & env, declaration const & d) {
+static void check_decl_type(environment const & env, declaration const & d, type_checker & checker) {
     check_no_mlocal(env, d.get_name(), d.get_type(), true);
     check_name(env, d.get_name());
     check_duplicated_params(env, d);
-    bool memoize = true; bool non_meta_only = !d.is_meta();
-    type_checker checker(env, memoize, non_meta_only);
     expr sort = checker.check(d.get_type(), d.get_univ_params());
     checker.ensure_sort(sort, d.get_type());
+}
+
+void check_decl_type(environment const & env, declaration const & d) {
+    bool memoize = true; bool non_meta_only = !d.is_meta();
+    type_checker checker(env, memoize, non_meta_only);
+    check_decl_type(env, d, checker);
+}
+
+void check_decl_value(environment const & env, declaration const & d) {
+    bool memoize = true; bool non_meta_only = !d.is_meta();
+    type_checker checker(env, memoize, non_meta_only);
+    if (d.is_definition()) {
+        check_definition(env, d, checker);
+    }
+}
+
+certified_declaration check(environment const & env, declaration const & d) {
+    bool memoize = true; bool non_meta_only = !d.is_meta();
+    type_checker checker(env, memoize, non_meta_only);
+    check_decl_type(env, d, checker);
     if (d.is_definition()) {
         check_definition(env, d, checker);
     }

src/kernel/type_checker.h

@@ -142,6 +142,8 @@ typedef std::shared_ptr<type_checker> type_checker_ref;
 
 void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type);
 void check_no_mlocal(environment const & env, name const & n, expr const & e, bool is_type);
+void check_decl_type(environment const & env, declaration const & d);
+void check_decl_value(environment const & env, declaration const & d);
 
 /** \brief Type check the given declaration, and return a certified declaration if it is type correct.
     Throw an exception if the declaration is type incorrect. */

src/library/kernel_serializer.h

@@ -28,6 +28,7 @@ inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d);
 
 serializer & operator<<(serializer & s, declaration const & d);
 declaration read_declaration(deserializer & d);
+inline deserializer & operator>>(deserializer & d, declaration & decl) { decl = read_declaration(d); return d; }
 
 serializer & operator<<(serializer & s, inductive::certified_inductive_decl const & d);
 inductive::certified_inductive_decl read_certified_inductive_decl(deserializer & d);

src/library/module.cpp

@@ -323,6 +323,33 @@ struct decl_modification : public modification {
     }
 };
 
+struct meta_decls_modification : public modification {
+    LEAN_MODIFICATION("meta_decl")
+    list<declaration> m_decls;
+
+    meta_decls_modification() {}
+    meta_decls_modification(list<declaration> const & decl):
+        m_decls(decl) {}
+
+    void perform(environment & env) const override {
+        buffer<declaration> decls;
+        to_buffer(m_decls, decls);
+        env = env.add_meta(decls);
+    }
+
+    void serialize(serializer & s) const override {
+        write_list(s, m_decls);
+    }
+
+    static std::shared_ptr<modification const> deserialize(deserializer & d) {
+        list<declaration> decls = read_list<declaration>(d);
+        return std::make_shared<meta_decls_modification>(std::move(decls));
+    }
+
+    void get_task_dependencies(buffer<gtask> &) const override {
+    }
+};
+
 struct inductive_modification : public modification {
     LEAN_MODIFICATION("ind")
 
@@ -397,6 +424,17 @@ environment add(environment const & env, certified_declaration const & d) {
     return add_decl_pos_info(new_env, _d.get_name());
 }
 
+environment add_meta(environment const & env, buffer<declaration> const & ds) {
+    environment new_env = env.add_meta(ds);
+    for (declaration const & d : ds) {
+        if (!check_computable(new_env, d.get_name()))
+            new_env = mark_noncomputable(new_env, d.get_name());
+        new_env = update_module_defs(new_env, d);
+        new_env = add_decl_pos_info(new_env, d.get_name());
+    }
+    return add(new_env, std::make_shared<meta_decls_modification>(to_list(ds)));
+}
+
 bool is_definition(environment const & env, name const & n) {
     module_ext const & ext = get_extension(env);
     return ext.m_module_defs.contains(n);
@@ -606,6 +644,7 @@ void initialize_module() {
     g_ext            = new module_ext_reg();
     g_object_readers = new object_readers();
     decl_modification::init();
+    meta_decls_modification::init();
     inductive_modification::init();
     quot_modification::init();
     pos_info_mod::init();
@@ -615,6 +654,7 @@ void finalize_module() {
     quot_modification::finalize();
     pos_info_mod::finalize();
     inductive_modification::finalize();
+    meta_decls_modification::finalize();
     decl_modification::finalize();
     delete g_object_readers;
     delete g_ext;

src/library/module.h

@@ -137,6 +137,7 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
 
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
+environment add_meta(environment const & env, buffer<declaration> const & ds);
 
 /** \brief Return true iff \c n is a definition added to the current module using #module::add */
 bool is_definition(environment const & env, name const & n);