diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 3deaf7ea46..b93fb3e145 100644 --- a/src/kernel/environment.cpp +++ b/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 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 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); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index b2742d913d..9f7b82ff35 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -156,6 +156,12 @@ public: - The environment does not contain an axiom named t.get_declaration().get_name() */ 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 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 diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index db61f34d71..2fa16c3267 100644 --- a/src/kernel/type_checker.cpp +++ b/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); } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 27983fede3..19abe9fb81 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -142,6 +142,8 @@ typedef std::shared_ptr 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. */ diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h index 0c0a07f265..319f14a36c 100644 --- a/src/library/kernel_serializer.h +++ b/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); diff --git a/src/library/module.cpp b/src/library/module.cpp index 10e90ddb2d..11b003da68 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -323,6 +323,33 @@ struct decl_modification : public modification { } }; +struct meta_decls_modification : public modification { + LEAN_MODIFICATION("meta_decl") + list m_decls; + + meta_decls_modification() {} + meta_decls_modification(list const & decl): + m_decls(decl) {} + + void perform(environment & env) const override { + buffer 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 deserialize(deserializer & d) { + list decls = read_list(d); + return std::make_shared(std::move(decls)); + } + + void get_task_dependencies(buffer &) 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 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(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; diff --git a/src/library/module.h b/src/library/module.h index 30592b2312..71e637d17b 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -137,6 +137,7 @@ environment add_and_perform(environment const & env, std::shared_ptr 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);