From a914345d29af761356d61dd8dc5ca0f67e36931b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Jun 2014 19:33:02 -0700 Subject: [PATCH] feat(library): new scoping framework Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 4 +- src/library/coercion.cpp | 112 ++++---- src/library/kernel_bindings.cpp | 32 +-- src/library/module.cpp | 5 + src/library/module.h | 12 + src/library/private.cpp | 13 +- src/library/register_module.h | 2 + src/library/scope.cpp | 457 -------------------------------- src/library/scope.h | 125 --------- src/library/scoped_ext.cpp | 122 +++++++++ src/library/scoped_ext.h | 181 +++++++++++++ tests/lua/namespace1.lua | 23 -- tests/lua/scope.lua | 121 +++++++++ tests/lua/sect1.lua | 21 -- tests/lua/sect10.lua | 34 --- tests/lua/sect1b.lua | 12 - tests/lua/sect1c.lua | 13 - tests/lua/sect2.lua | 11 - tests/lua/sect3.lua | 26 -- tests/lua/sect4.lua | 22 -- tests/lua/sect5.lua | 26 -- tests/lua/sect6.lua | 27 -- tests/lua/sect7.lua | 42 --- tests/lua/sect8.lua | 39 --- tests/lua/sect9.lua | 33 --- 25 files changed, 509 insertions(+), 1006 deletions(-) delete mode 100644 src/library/scope.cpp delete mode 100644 src/library/scope.h create mode 100644 src/library/scoped_ext.cpp create mode 100644 src/library/scoped_ext.h delete mode 100644 tests/lua/namespace1.lua create mode 100644 tests/lua/scope.lua delete mode 100644 tests/lua/sect1.lua delete mode 100644 tests/lua/sect10.lua delete mode 100644 tests/lua/sect1b.lua delete mode 100644 tests/lua/sect1c.lua delete mode 100644 tests/lua/sect2.lua delete mode 100644 tests/lua/sect3.lua delete mode 100644 tests/lua/sect4.lua delete mode 100644 tests/lua/sect5.lua delete mode 100644 tests/lua/sect6.lua delete mode 100644 tests/lua/sect7.lua delete mode 100644 tests/lua/sect8.lua delete mode 100644 tests/lua/sect9.lua diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 5054b9b0d..c5b11eaee 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -2,8 +2,8 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp kernel_bindings.cpp io_state_stream.cpp bin_app.cpp resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp - private.cpp placeholder.cpp aliases.cpp scope.cpp level_names.cpp - update_declaration.cpp choice.cpp) + private.cpp placeholder.cpp aliases.cpp level_names.cpp + update_declaration.cpp choice.cpp scoped_ext.cpp) # hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index c463132d2..0e4b1da01 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/kernel_serializer.h" #include "library/kernel_bindings.h" +#include "library/scoped_ext.h" namespace lean { enum class coercion_class_kind { User, Sort, Fun }; @@ -65,7 +66,7 @@ struct coercion_info { m_fun(f), m_fun_type(f_type), m_level_params(ls), m_num_args(num), m_to(cls) {} }; -struct coercion_ext : public environment_extension { +struct coercion_state : public environment_extension { rb_map, name_quick_cmp> m_coercion_info; // m_from and m_to contain "direct" coercions rb_map, name_quick_cmp> m_from; @@ -97,32 +98,6 @@ struct coercion_ext : public environment_extension { } }; -struct coercion_ext_reg { - unsigned m_ext_id; - coercion_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } -}; - -static coercion_ext_reg g_ext; -static coercion_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext.m_ext_id)); -} -static environment update(environment const & env, coercion_ext const & ext) { - return env.update(g_ext.m_ext_id, std::make_shared(ext)); -} - -// key used for module serialization -static std::string g_coercion_key = "coerce"; -static void coercion_reader(deserializer & d, module_idx, shared_environment &, - std::function &, - std::function & add_delayed_update) { - name f, C; - d >> f >> C; - add_delayed_update([=](environment const & env, io_state const & ios) -> environment { - return add_coercion(env, f, C, ios); - }); -} -register_module_object_reader_fn g_coercion_reader(g_coercion_key, coercion_reader); - static void check_pi(name const & f, expr const & t) { if (!is_pi(t)) throw exception(sstream() << "invalid coercion, '" << f << "' is not function"); @@ -173,8 +148,7 @@ static arrows insert(arrows const & a, name const & C, coercion_class const & D) } struct add_coercion_fn { - environment m_env; - coercion_ext m_ext; + coercion_state m_state; arrows m_visited; io_state const & m_ios; @@ -222,11 +196,11 @@ struct add_coercion_fn { level_param_names const & ls, unsigned num_args, coercion_class const & cls) { // apply transitivity using ext.m_to coercion_class C_cls = coercion_class::mk_user(C); - auto it1 = m_ext.m_to.find(C_cls); + auto it1 = m_state.m_to.find(C_cls); if (!it1) return; for (name const & B : *it1) { - coercion_info info = m_ext.get_info(B, C_cls); + coercion_info info = m_state.get_info(B, C_cls); // B >-> C >-> D add_coercion_trans(B, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, ls, f, f_type, num_args, cls); @@ -239,11 +213,11 @@ struct add_coercion_fn { if (cls.kind() != coercion_class_kind::User) return; // nothing to do Sort and Fun classes are terminal name const & D = cls.get_name(); - auto it = m_ext.m_from.find(D); + auto it = m_state.m_from.find(D); if (!it) return; for (coercion_class E : *it) { - coercion_info info = m_ext.get_info(D, E); + coercion_info info = m_state.get_info(D, E); // C >-> D >-> E add_coercion_trans(C, ls, f, f_type, num_args, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, info.m_to); @@ -252,18 +226,18 @@ struct add_coercion_fn { void add_coercion_core(name const & C, expr const & f, expr const & f_type, level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - auto it = m_ext.m_coercion_info.find(C); + auto it = m_state.m_coercion_info.find(C); if (!it) { list infos(coercion_info(f, f_type, ls, num_args, cls)); - m_ext.m_coercion_info.insert(C, infos); + m_state.m_coercion_info.insert(C, infos); } else { list infos = *it; infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; }); infos = list(coercion_info(f, f_type, ls, num_args, cls), infos); - m_ext.m_coercion_info.insert(C, infos); + m_state.m_coercion_info.insert(C, infos); } if (is_constant(f)) - m_ext.m_coercions.insert(const_name(f)); + m_state.m_coercions.insert(const_name(f)); } void add_coercion(name const & C, expr const & f, expr const & f_type, @@ -278,22 +252,18 @@ struct add_coercion_fn { add_coercion_trans_from(C, f, f_type, ls, num_args, cls); } - add_coercion_fn(environment const & env, io_state const & ios): - m_env(env), m_ext(get_extension(env)), m_ios(ios) {} + add_coercion_fn(coercion_state const & s, io_state const & ios): + m_state(s), m_ios(ios) {} - environment operator()(name const & C, expr const & f, expr const & f_type, - level_param_names const & ls, unsigned num_args, coercion_class const & cls) { + coercion_state operator()(name const & C, expr const & f, expr const & f_type, + level_param_names const & ls, unsigned num_args, coercion_class const & cls) { add_coercion(C, f, f_type, ls, num_args, cls); - m_ext.update_from_to(C, cls, m_ios); - name const & f_name = const_name(f); - m_env = module::add(m_env, g_coercion_key, [=](serializer & s) { - s << f_name << C; - }); - return update(m_env, m_ext); + m_state.update_from_to(C, cls, m_ios); + return m_state; } }; -environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios) { +coercion_state add_coercion(environment const & env, io_state const & ios, coercion_state const & st, name const & f, name const & C) { declaration d = env.get(f); unsigned num = 0; buffer args; @@ -313,7 +283,7 @@ environment add_coercion(environment const & env, name const & f, name const & C throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'"); else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C) throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); - return add_coercion_fn(env, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls); + return add_coercion_fn(st, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls); } t = binding_body(t); num++; @@ -321,6 +291,38 @@ environment add_coercion(environment const & env, name const & f, name const & C } } +typedef std::pair coercion_entry; +struct coercion_config { + typedef coercion_state state; + typedef coercion_entry entry; + static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) { + s = add_coercion(env, ios, s, e.first, e.second); + } + static name const & get_class_name() { + static name g_class_name("coercion"); + return g_class_name; + } + static std::string const & get_serialization_key() { + static std::string g_key("coerce"); + return g_key; + } + static void write_entry(serializer & s, entry const & e) { + s << e.first << e.second; + } + static entry read_entry(deserializer & d) { + entry e; + d >> e.first >> e.second; + return e; + } +}; + +template class scoped_ext; +typedef scoped_ext coercion_ext; + +environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios) { + return coercion_ext::add_entry(env, ios, coercion_entry(f, C)); +} + environment add_coercion(environment const & env, name const & f, io_state const & ios) { declaration d = env.get(f); expr t = d.get_type(); @@ -334,7 +336,7 @@ environment add_coercion(environment const & env, name const & f, io_state const } bool is_coercion(environment const & env, name const & f) { - coercion_ext const & ext = get_extension(env); + coercion_state const & ext = coercion_ext::get_state(env); return ext.m_coercions.contains(f); } @@ -343,7 +345,7 @@ bool is_coercion(environment const & env, expr const & f) { } bool has_coercions_from(environment const & env, name const & C) { - coercion_ext const & ext = get_extension(env); + coercion_state const & ext = coercion_ext::get_state(env); return ext.m_coercion_info.contains(C); } @@ -351,7 +353,7 @@ bool has_coercions_from(environment const & env, expr const & C) { expr const & C_fn = get_app_fn(C); if (!is_constant(C_fn)) return false; - coercion_ext const & ext = get_extension(env); + coercion_state const & ext = coercion_ext::get_state(env); auto it = ext.m_coercion_info.find(const_name(C_fn)); if (!it) return false; @@ -366,7 +368,7 @@ optional get_coercion(environment const & env, expr const & C, coercion_cl expr const & C_fn = get_app_rev_args(C, args); if (!is_constant(C_fn)) return none_expr(); - coercion_ext const & ext = get_extension(env); + coercion_state const & ext = coercion_ext::get_state(env); auto it = ext.m_coercion_info.find(const_name(C_fn)); if (!it) return none_expr(); @@ -396,7 +398,7 @@ bool get_user_coercions(environment const & env, expr const & C, buffer void for_each_coercion(environment const & env, F && f) { - coercion_ext const & ext = get_extension(env); + coercion_state const & ext = coercion_ext::get_state(env); ext.m_coercion_info.for_each([&](name const & C, list const & infos) { for (auto const & info : infos) { f(C, info); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index d780dacb1..5a03634cb 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -29,7 +29,6 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/normalize.h" #include "library/module.h" -#include "library/scope.h" // Lua Bindings for the Kernel classes. We do not include the Lua // bindings in the kernel because we do not want to inflate the Kernel. @@ -1154,20 +1153,16 @@ static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); } static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); } static int environment_add_global_level(lua_State * L) { - return push_environment(L, scope::add_global_level(to_environment(L, 1), to_name_ext(L, 2))); + return push_environment(L, module::add_global_level(to_environment(L, 1), to_name_ext(L, 2))); } static int environment_is_global_level(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_global_level(to_name_ext(L, 2))); } static int environment_find(lua_State * L) { return push_optional_declaration(L, to_environment(L, 1).find(to_name_ext(L, 2))); } static int environment_get(lua_State * L) { return push_declaration(L, to_environment(L, 1).get(to_name_ext(L, 2))); } static int environment_add(lua_State * L) { - int nargs = lua_gettop(L); - binder_info info; - if (nargs > 2) - info = to_binder_info(L, 3); if (is_declaration(L, 2)) - return push_environment(L, scope::add(to_environment(L, 1), to_declaration(L, 2), info)); + return push_environment(L, module::add(to_environment(L, 1), to_declaration(L, 2))); else - return push_environment(L, scope::add(to_environment(L, 1), to_certified_declaration(L, 2), info)); + return push_environment(L, module::add(to_environment(L, 1), to_certified_declaration(L, 2))); } static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_declaration(L, 2))); } static int mk_bare_environment(lua_State * L) { @@ -1252,15 +1247,6 @@ static int export_module(lua_State * L) { return 0; } -static int begin_section_scope(lua_State * L) { return push_environment(L, scope::begin_section(to_environment(L, 1))); } -static int begin_namespace_scope(lua_State * L) { return push_environment(L, scope::begin_namespace(to_environment(L, 1), lua_tostring(L, 2))); } -static int end_scope(lua_State * L) { return push_environment(L, scope::end(to_environment(L, 1))); } -static int get_namespace(lua_State * L) { return push_name(L, scope::get_namespace(to_environment(L, 1))); } -static int get_name_in_namespace(lua_State * L) { - return push_name(L, scope::get_name_in_namespace(to_environment(L, 1), to_name_ext(L, 2))); -} -static int namespace_find(lua_State * L) { return push_optional_declaration(L, scope::find(to_environment(L, 1), to_name_ext(L, 2))); } - static const struct luaL_Reg environment_m[] = { {"__gc", environment_gc}, // never throws {"is_descendant", safe_function}, @@ -1283,12 +1269,6 @@ static const struct luaL_Reg environment_m[] = { {"type_check", safe_function}, {"for_each", safe_function}, {"export", safe_function}, - {"begin_section_scope", safe_function}, - {"begin_namespace_scope", safe_function}, - {"end_scope", safe_function}, - {"get_namespace", safe_function}, - {"get_name_in_namespace", safe_function}, - {"namespace_find", safe_function}, {0, 0} }; @@ -1928,7 +1908,7 @@ static int add_declaration(lua_State * L) { d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4)); else d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5)); - return push_environment(L, scope::add(to_environment(L, 1), *d)); + return push_environment(L, module::add(to_environment(L, 1), *d)); } static void open_type_checker(lua_State * L) { @@ -1972,7 +1952,7 @@ static int add_inductive1(lua_State * L) { buffer irules; for (int i = idx+1; i <= nargs; i+=2) irules.push_back(intro_rule(to_name_ext(L, i), to_expr(L, i+1))); - return push_environment(L, scope::add_inductive(env, Iname, ls, num_params, Itype, to_list(irules.begin(), irules.end()))); + return push_environment(L, module::add_inductive(env, Iname, ls, num_params, Itype, to_list(irules.begin(), irules.end()))); } static int add_inductivek(lua_State * L) { environment env = to_environment(L, 1); @@ -2004,7 +1984,7 @@ static int add_inductivek(lua_State * L) { } if (decls.empty()) throw exception("invalid add_inductive, at least one inductive type must be defined"); - return push_environment(L, scope::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end()))); + return push_environment(L, module::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end()))); } static int add_inductive(lua_State * L) { if (is_name(L, 2) || lua_isstring(L, 2)) diff --git a/src/library/module.cpp b/src/library/module.cpp index 65117e76d..14746c541 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -146,6 +146,11 @@ static void inductive_reader(deserializer & d, module_idx, shared_environment & }); } +environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params, + unsigned num_params, expr const & type, list const & intro_rules) { + return add_inductive(env, level_params, num_params, list(inductive::inductive_decl(ind_name, type, intro_rules))); +} + static register_module_object_reader_fn g_reg_ind_reader(g_inductive, inductive_reader); } // end of namespace module diff --git a/src/library/module.h b/src/library/module.h index 774de6573..3aa3d08a3 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -91,5 +91,17 @@ environment add_inductive(environment env, level_param_names const & level_params, unsigned num_params, list const & decls); + +/** + \brief Declare a single inductive datatype. This is just a helper function implemented on top of + the previous (more general) add_inductive. +*/ +environment add_inductive(environment const & env, + name const & ind_name, // name of new inductive datatype + level_param_names const & level_params, // level parameters + unsigned num_params, // number of params + expr const & type, // type of the form: params -> indices -> Type + list const & intro_rules); // introduction rules + } } diff --git a/src/library/private.cpp b/src/library/private.cpp index d85dbe985..fe35f3bde 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "util/hash.h" #include "library/private.h" #include "library/module.h" -#include "library/scope.h" #include "library/kernel_bindings.h" namespace lean { @@ -39,17 +38,7 @@ static std::string g_prv_key("prv"); // Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and // export .olean files. static environment preserve_private_data(environment const & env, name const & r, name const & n) { - if (scope::has_open_sections(env)) { - return scope::add(env, [=](scope::abstraction_context & ctx) { - environment env = ctx.env(); - private_ext ext = get_extension(env); - ext.m_inv_map.insert(r, n); - ext.m_counter++; - ctx.update_env(preserve_private_data(update(env, ext), r, n)); - }); - } else { - return module::add(env, g_prv_key, [=](serializer & s) { s << n << r; }); - } + return module::add(env, g_prv_key, [=](serializer & s) { s << n << r; }); } std::pair add_private_name(environment const & env, name const & n, optional const & extra_hash) { diff --git a/src/library/register_module.h b/src/library/register_module.h index a1965a951..a90fa9234 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/aliases.h" #include "library/choice.h" +#include "library/scoped_ext.h" // #include "library/hop_match.h" namespace lean { @@ -24,6 +25,7 @@ inline void open_core_module(lua_State * L) { open_placeholder(L); open_aliases(L); open_choice(L); + open_scoped_ext(L); // open_hop_match(L); } inline void register_core_module() { diff --git a/src/library/scope.cpp b/src/library/scope.cpp deleted file mode 100644 index 9cb42ba2c..000000000 --- a/src/library/scope.cpp +++ /dev/null @@ -1,457 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include "util/list.h" -#include "util/name_hash_map.h" -#include "kernel/replace_fn.h" -#include "kernel/abstract.h" -#include "kernel/type_checker.h" -#include "kernel/inductive/inductive.h" -#include "library/scope.h" -#include "library/module.h" -#include "library/update_declaration.h" -#include "library/level_names.h" - -namespace lean { -namespace scope { -struct level_info { - unsigned m_pos; // position inside the section - level_info(unsigned p = 0):m_pos(p) {} -}; - -struct decl_info { - unsigned m_pos; // position inside the section - level_param_names m_level_deps; // local universe levels this declaration depends on - levels m_levels; // level_param_names ==> levels - dependencies m_var_deps; // local variable/local declarations this declaration depends on - expr m_type; // type of the new declaration - binder_info m_binder_info; // binder information - bool m_local; // true if local - - decl_info():m_pos(0), m_local(true) {} - decl_info(unsigned pos, level_param_names const & lvl_deps, dependencies const & var_deps, expr const & type, - binder_info const & bi, bool local): - m_pos(pos), m_level_deps(lvl_deps), m_var_deps(var_deps), m_type(type), m_binder_info(bi), m_local(local) { - m_levels = param_names_to_levels(m_level_deps); - } -}; - -typedef name_hash_map decl_info_map; -typedef name_hash_map level_info_map; -typedef std::unordered_set name_hash_set; - -class abstraction_context_imp : public abstraction_context { - unsigned m_next_local_pos; - - level_info_map m_levels_info; - decl_info_map m_decls_info; - - name_hash_set m_level_deps; - name_hash_set m_var_deps; - -public: - abstraction_context_imp(environment const & env):abstraction_context(env), m_next_local_pos(0) {} - - void clear_deps() { - m_level_deps.clear(); - m_var_deps.clear(); - } - - // Replace local universe level into parameters. - virtual level convert(level const & l) { - return replace(l, [&](level const & l) { - if (is_global(l)) { - auto it = m_levels_info.find(global_id(l)); - if (it != m_levels_info.end()) { - m_level_deps.insert(global_id(l)); - return optional(mk_param_univ(global_id(l))); - } - } - return optional(); - }); - } - - // Replace local decls and universe levels with parameters. - virtual expr convert(expr const & e) { - return replace(e, [&](expr const & e, unsigned) { - if (is_constant(e)) { - auto it = m_decls_info.find(const_name(e)); - if (it != m_decls_info.end()) { - auto const & info = it->second; - for (auto const & d : info.m_level_deps) - m_level_deps.insert(d); - for (auto const & d : info.m_var_deps) - m_var_deps.insert(const_name(d)); - if (info.m_local) { - return some_expr(update_constant(e, levels())); - } else { - return some_expr(mk_app(update_constant(e, append(info.m_levels, const_levels(e))), info.m_var_deps)); - } - } else { - levels new_ls = map(const_levels(e), [&](level const & l) { return convert(l); }); - return some_expr(update_constant(e, new_ls)); - } - } else if (is_sort(e)) { - return some_expr(update_sort(e, convert(sort_level(e)))); - } else { - return none_expr(); - } - }); - } - - // Convert m_level_deps into a level_param_names - virtual level_param_names mk_level_deps() { - buffer r; - for (auto d : m_level_deps) - r.push_back(d); - std::sort(r.begin(), r.end(), [&](name const & n1, name const & n2) { - return m_levels_info.find(n1)->second.m_pos < m_levels_info.find(n2)->second.m_pos; - }); - return to_list(r.begin(), r.end()); - } - - // Convert m_expr_deps into a vector of names - virtual dependencies mk_var_deps() { - dependencies r; - for (auto d : m_var_deps) - r.push_back(mk_constant(d)); - std::sort(r.begin(), r.end(), [&](expr const & n1, expr const & n2) { - return m_decls_info.find(const_name(n1))->second.m_pos < m_decls_info.find(const_name(n2))->second.m_pos; - }); - return r; - } - - // Create Pi/Lambda(deps, e) - expr abstract(bool is_lambda, expr e, dependencies const & deps) { - auto it = deps.end(); - auto begin = deps.begin(); - while (it != begin) { - --it; - auto const & info = m_decls_info.find(const_name(*it))->second; - if (is_lambda) - e = ::lean::Fun(*it, info.m_type, e, info.m_binder_info); - else - e = ::lean::Pi(*it, info.m_type, e, info.m_binder_info); - } - return e; - } - - // Create Pi(deps, e), the types (and binder_infos) are extracted from m_decls_info - virtual expr Pi(expr e, dependencies const & deps) { - return abstract(false, e, deps); - } - - // Create Lambda(deps, e), the types (and binder_infos) are extracted from m_decls_info - virtual expr Fun(expr e, dependencies const & deps) { - return abstract(true, e, deps); - } - - virtual void add_decl_info(name const & n, level_param_names const & ps, dependencies const & deps, expr const & type) { - m_decls_info.emplace(n, decl_info(0, ps, deps, type, binder_info(), false)); - } - - void add_global_level(name const & n) { - m_levels_info.emplace(n, level_info(m_next_local_pos)); - m_next_local_pos++; - } - - void add_local_decl(declaration const & d, binder_info const & bi) { - lean_assert(d.is_var_decl()); - lean_assert(is_nil(d.get_univ_params())); - expr new_type = convert(d.get_type()); - dependencies var_deps = mk_var_deps(); - var_deps.push_back(mk_constant(d.get_name())); - m_decls_info.emplace(d.get_name(), - decl_info(m_next_local_pos, mk_level_deps(), var_deps, new_type, bi, true)); - m_next_local_pos++; - } - - void add_definition(declaration d) { - lean_assert(d.is_definition()); - d = sanitize_level_params(d); - expr new_type = convert(d.get_type()); - expr new_value = convert(d.get_value()); - level_param_names level_deps = mk_level_deps(); - level_param_names new_ls = append(level_deps, d.get_univ_params()); - dependencies var_deps = mk_var_deps(); - new_type = Pi(new_type, var_deps); - new_value = Fun(new_value, var_deps); - add_decl_info(d.get_name(), level_deps, var_deps, new_type); - declaration new_d = update_declaration(d, new_ls, new_type, new_value); - m_env = add(m_env, check(m_env, new_d)); - } -}; - -struct scope_ext : public environment_extension { - struct section { - environment m_prev_env; - list m_fns; - section(environment const & env):m_prev_env(env) {} - }; - enum class scope_kind { Namespace, Section }; - list m_namespaces; - list
m_sections; - list m_scope_kinds; - scope_ext() {} -}; - -struct scope_ext_reg { - unsigned m_ext_id; - scope_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } -}; - -static scope_ext_reg g_ext; -static scope_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext.m_ext_id)); -} -static environment update(environment const & env, scope_ext const & ext) { - return env.update(g_ext.m_ext_id, std::make_shared(ext)); -} - -environment add(environment const & env, abstraction_fn const & fn) { - scope_ext ext = get_extension(env); - if (is_nil(ext.m_sections)) - throw exception("invalid section operation, there is no open scope"); - scope_ext::section s = head(ext.m_sections); - s.m_fns = list(fn, s.m_fns); - ext.m_sections = list(s, tail(ext.m_sections)); - return update(env, ext); -} - -environment add_global_level(environment const & env, name const & l) { - scope_ext const & ext = get_extension(env); - if (is_nil(ext.m_sections)) { - return module::add_global_level(env, l); - } else { - environment new_env = env.add_global_level(l); - return add(new_env, [=](abstraction_context & ctx) { - static_cast(ctx).add_global_level(l); - }); - } -} - -static environment save_section_declaration(environment const & env, declaration const & d, binder_info const & bi) { - if (d.is_var_decl()) { - if (!is_nil(d.get_univ_params())) - throw exception("section parameters and axiom cannot contain universe level parameter"); - return add(env, [=](abstraction_context & ctx) { - static_cast(ctx).add_local_decl(d, bi); - }); - } else { - return add(env, [=](abstraction_context & ctx) { - static_cast(ctx).add_definition(d); - }); - } -} - -environment add(environment const & env, certified_declaration const & d, binder_info const & bi) { - scope_ext const & ext = get_extension(env); - if (is_nil(ext.m_sections)) - return module::add(env, d); - else - return save_section_declaration(env.add(d), d.get_declaration(), bi); -} - -environment add(environment const & env, declaration const & d, binder_info const & bi) { - scope_ext const & ext = get_extension(env); - if (is_nil(ext.m_sections)) - return module::add(env, d); - else - return save_section_declaration(env.add(d), d, bi); -} - -using inductive::inductive_decl; -using inductive::inductive_decl_name; -using inductive::inductive_decl_type; -using inductive::inductive_decl_intros; -using inductive::intro_rule; -using inductive::intro_rule_name; -using inductive::intro_rule_type; - -// Return true iff \c t is one of the inductive types in \c decls -static bool is_inductive_type(expr const & t, list const & decls) { - expr fn = get_app_fn(t); - return - is_constant(fn) && - std::any_of(decls.begin(), decls.end(), [&](inductive_decl const & d) { return inductive_decl_name(d) == const_name(fn); }); -} - -// Add the extra universe levels and parameters to the inductive datatype \c t. -// For example, suppose t is of the form (T.{l} A I) where l and A are the existing levels and parameters, and I is the index. -// In this instance, this procedure returns the term: -// (T.{extra_ls l} extra_params A I) -static expr update_inductive_type(expr const & t, levels const & extra_ls, dependencies const & extra_params) { - buffer args; - expr T = get_app_args(t, args); - lean_assert(is_constant(T)); - expr new_T = update_constant(T, append(extra_ls, const_levels(T))); - buffer new_args; - new_args.append(extra_params); - new_args.append(args); - lean_assert(new_args.size() == args.size() + extra_params.size()); - expr r = mk_app(new_T, new_args); - return r; -} - -// Add the extra universe levels and parameters to every occurrence in t of an inductive datatype in \c decls. -// See update_inductive_type and is_inductive_type. -static expr update_inductive_types(expr const & t, list const & decls, - levels const & extra_ls, dependencies const & extra_params) { - return replace(t, [&](expr const & e, unsigned) { - if (is_inductive_type(e, decls)) - return some_expr(update_inductive_type(e, extra_ls, extra_params)); - else - return none_expr(); - }); -} - -environment add_inductive(environment env, - level_param_names const & level_params, - unsigned num_params, - list const & decls) { - scope_ext const & ext = get_extension(env); - if (is_nil(ext.m_sections)) { - return module::add_inductive(env, level_params, num_params, decls); - } else { - environment new_env = inductive::add_inductive(env, level_params, num_params, decls); - return add(new_env, [=](abstraction_context & ctx) { - // abstract types - auto new_ls_decls = sanitize_level_params(level_params, decls); - auto s_level_params = new_ls_decls.first; - auto s_decls = new_ls_decls.second; - buffer tmp_decls; - for (auto const & d : s_decls) { - expr new_type = ctx.convert(inductive_decl_type(d)); - buffer new_rules; - for (auto const & r : inductive_decl_intros(d)) { - expr new_rule_type = ctx.convert(intro_rule_type(r)); - new_rules.push_back(intro_rule(intro_rule_name(r), new_rule_type)); - } - tmp_decls.push_back(inductive_decl(inductive_decl_name(d), - new_type, - to_list(new_rules.begin(), new_rules.end()))); - } - // collect new params and level_params - level_param_names extra_ls = ctx.mk_level_deps(); - levels extra_lvls = param_names_to_levels(extra_ls); - dependencies extra_ps = ctx.mk_var_deps(); - unsigned new_num_params = num_params + extra_ps.size(); - level_param_names new_ls = append(extra_ls, s_level_params); - // create Pi(extra_ps, T) where T are the types in the declarations - buffer new_decls; - for (auto const & d : tmp_decls) { - expr new_type = ctx.Pi(inductive_decl_type(d), extra_ps); - ctx.add_decl_info(inductive_decl_name(d), extra_ls, extra_ps, new_type); - buffer new_rules; - for (auto const & r : inductive_decl_intros(d)) { - expr new_rule_type = update_inductive_types(intro_rule_type(r), s_decls, - extra_lvls, extra_ps); - new_rule_type = ctx.Pi(new_rule_type, extra_ps); - new_rules.push_back(intro_rule(intro_rule_name(r), new_rule_type)); - ctx.add_decl_info(intro_rule_name(r), extra_ls, extra_ps, new_rule_type); - } - new_decls.push_back(inductive_decl(inductive_decl_name(d), - new_type, - to_list(new_rules.begin(), new_rules.end()))); - } - environment env = ctx.env(); - env = add_inductive(env, new_ls, new_num_params, to_list(new_decls.begin(), new_decls.end())); - ctx.update_env(env); - }); - } -} - -environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params, - unsigned num_params, expr const & type, list const & intro_rules) { - return add_inductive(env, level_params, num_params, list(inductive::inductive_decl(ind_name, type, intro_rules))); -} - -environment begin_section(environment const & env) { - scope_ext ext = get_extension(env); - ext.m_scope_kinds = list(scope_ext::scope_kind::Section, ext.m_scope_kinds); - ext.m_sections = list(scope_ext::section(env), ext.m_sections); - return update(env, ext); -} - -environment begin_namespace(environment const & env, char const * n) { - scope_ext ext = get_extension(env); - ext.m_scope_kinds = list(scope_ext::scope_kind::Namespace, ext.m_scope_kinds); - ext.m_namespaces = list(name(get_namespace(env), n), ext.m_namespaces); - return update(env, ext); -} - -environment end(environment const & env) { - scope_ext ext = get_extension(env); - if (is_nil(ext.m_scope_kinds)) - throw exception("environment does not have open scopes"); - scope_ext::scope_kind k = head(ext.m_scope_kinds); - ext.m_scope_kinds = tail(ext.m_scope_kinds); - switch (k) { - case scope_ext::scope_kind::Namespace: - ext.m_namespaces = tail(ext.m_namespaces); - return update(env, ext); - case scope_ext::scope_kind::Section: { - scope_ext::section const & s = head(ext.m_sections); - environment new_env = s.m_prev_env; - buffer fns; - for (auto const & fn : s.m_fns) - fns.push_back(&fn); - std::reverse(fns.begin(), fns.end()); - abstraction_context_imp ctx(new_env); - for (auto p : fns) { - (*p)(ctx); - ctx.clear_deps(); - } - return ctx.env(); - }} - lean_unreachable(); // LCOV_EXCL_LINE -} - -bool has_open_sections(environment const & env) { - return !is_nil(get_extension(env).m_sections); -} - -name const & get_namespace(environment const & env) { - scope_ext const & ext = get_extension(env); - if (is_nil(ext.m_namespaces)) - return name::anonymous(); - else - return head(ext.m_namespaces); -} - -optional find(environment const & env, name const & n) { - scope_ext const & ext = get_extension(env); - for (auto const & p : ext.m_namespaces) { - name full_name = p + n; - if (auto d = env.find(full_name)) { - return d; - } - } - return env.find(n); -} - -name get_name_in_namespace(environment const & env, name const & n) { - if (auto d = env.find(n)) { - scope_ext const & ext = get_extension(env); - for (auto const & p : ext.m_namespaces) { - if (is_prefix_of(p, n)) { - name r = n.replace_prefix(p, name()); - if (auto d2 = find(env, r)) { - if (is_eqp(*d, *d2)) - return r; - } - return n; - } - } - } - return n; -} -} -} diff --git a/src/library/scope.h b/src/library/scope.h deleted file mode 100644 index baa4e8157..000000000 --- a/src/library/scope.h +++ /dev/null @@ -1,125 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "kernel/environment.h" - -namespace lean { -namespace scope { -typedef std::vector dependencies; // local var dependencies - -/** - \brief API provided to section abstraction functions. - Section abstraction functions are executed whenever a - section is closed. The are used to abstract the - section definitions with respect to universe levels, - and parameters/axioms declared inside the section. -*/ -class abstraction_context { -protected: - environment m_env; -public: - abstraction_context(environment const & env):m_env(env) {} - virtual ~abstraction_context() {} - - environment const & env() { return m_env; } - void update_env(environment const & env) { m_env = env; } - - virtual level convert(level const & e) = 0; - virtual expr convert(expr const & e) = 0; - virtual level_param_names mk_level_deps() = 0; - virtual dependencies mk_var_deps() = 0; - virtual expr Pi(expr e, dependencies const & deps) = 0; - virtual expr Fun(expr e, dependencies const & deps) = 0; - - virtual void add_decl_info(name const & n, level_param_names const & ps, dependencies const & deps, expr const & type) = 0; -}; - -typedef std::function abstraction_fn; - -/** \brief Add a function that should be executed when a section is closed. */ -environment add(environment const & env, abstraction_fn const & fn); - -/** - \brief Add the global level declaration to the environment and current section. - If there are no active sections, then this function behaves like \c module::add_global_level. -*/ -environment add_global_level(environment const & env, name const & l); - -/** - \brief Add the given declaration to the environment and currenct section. - If there are no active sections, then this function behaves like \c module::add. -*/ -environment add(environment const & env, certified_declaration const & d, binder_info const & bi = binder_info()); - -/** - \brief Add the given declaration to the environment and currenct section. - This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL - If there are no active sections, then this function behaves like \c module::add. -*/ -environment add(environment const & env, declaration const & d, binder_info const & bi = binder_info()); - -/** - \brief Add the given inductive declaration to the environment and current section. - If there are no active sections, then this function behaves like \c module::add_inductive. -*/ -environment add_inductive(environment env, - level_param_names const & level_params, - unsigned num_params, - list const & decls); - -/** - \brief Declare a single inductive datatype. This is just a helper function implemented on top of - the previous (more general) add_inductive. -*/ -environment add_inductive(environment const & env, - name const & ind_name, // name of new inductive datatype - level_param_names const & level_params, // level parameters - unsigned num_params, // number of params - expr const & type, // type of the form: params -> indices -> Type - list const & intro_rules); // introduction rules - -/** - \brief Create a section scope. When a section is closed all definitions and theorems are relativized with - respect to var_decls and axioms. That is, var_decls and axioms become new arguments for the definitions and axioms. -*/ -environment begin_section(environment const & env); - -/** - \brief Create a namespace scope. A namespace is just a mechanism - for appending the prefix n to declarations added to the - environment. -*/ -environment begin_namespace(environment const & env, char const * n); - -/** - \brief End/close a scoped created using \c begin_section_scope or \c begin_namespace_scope. - Throws an exception if there is no open scope. -*/ -environment end(environment const & env); - -/** \brief Return true iff the given environment has open sections. */ -bool has_open_sections(environment const & env); - -/** - \brief Return the current namespace for \c env. The namespace is composed by the sequence - of names provided to \c begin_namespace_scope. -*/ -name const & get_namespace(environment const & env); - -/** - \brief Return the name of \c n in the current namespace of \c env. - Example: if the current namespace is foo.bar and \c n is foo.bar.bla.1, then - the result is bla.1. -*/ -name get_name_in_namespace(environment const & env, name const & n); - -/** \brief Find a declaration named \c n in \c env by taking the active namespaces into account. */ -optional find(environment const & env, name const & n); -} -} diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp new file mode 100644 index 000000000..a0577a26b --- /dev/null +++ b/src/library/scoped_ext.cpp @@ -0,0 +1,122 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "library/scoped_ext.h" +#include "library/kernel_bindings.h" + +namespace lean { +typedef std::tuple entry; +typedef std::vector scoped_exts; + +static scoped_exts & get_exts() { + static std::unique_ptr> exts; + if (!exts.get()) + exts.reset(new std::vector()); + return *exts; +} + +void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop) { + get_exts().emplace_back(c, use, push, pop); +} + +struct scope_mng_ext : public environment_extension { + list m_namespaces; + list m_in_section; +}; + +struct scope_mng_ext_reg { + unsigned m_ext_id; + scope_mng_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static scope_mng_ext_reg g_ext; +static scope_mng_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext.m_ext_id)); +} +static environment update(environment const & env, scope_mng_ext const & ext) { + return env.update(g_ext.m_ext_id, std::make_shared(ext)); +} + +name const & get_namespace(environment const & env) { + scope_mng_ext const & ext = get_extension(env); + return !is_nil(ext.m_namespaces) ? head(ext.m_namespaces) : name::anonymous(); +} + +bool in_section(environment const & env) { + scope_mng_ext const & ext = get_extension(env); + return !is_nil(ext.m_in_section) && head(ext.m_in_section); +} + +environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c) { + environment r = env; + for (auto const & t : get_exts()) { + if (c.is_anonymous() || c == std::get<0>(t)) + r = std::get<1>(t)(r, ios, n); + } + return r; +} + +environment push_scope(environment const & env, io_state const & ios, name const & n) { + if (!n.is_anonymous() && in_section(env)) + throw exception("invalid namespace declaration, a namespace cannot be declared inside a section"); + name new_n = get_namespace(env) + n; + scope_mng_ext ext = get_extension(env); + ext.m_namespaces = list(new_n, ext.m_namespaces); + ext.m_in_section = list(n.is_anonymous(), ext.m_in_section); + environment r = update(env, ext); + for (auto const & t : get_exts()) + r = std::get<2>(t)(r); + if (!n.is_anonymous()) + r = using_namespace(r, ios, n); + return r; +} + +environment pop_scope(environment const & env) { + scope_mng_ext ext = get_extension(env); + if (is_nil(ext.m_namespaces)) + throw exception("invalid end of scope, there are no open namespaces/sections"); + ext.m_namespaces = tail(ext.m_namespaces); + ext.m_in_section = tail(ext.m_in_section); + environment r = update(env, ext); + for (auto const & t : get_exts()) + r = std::get<3>(t)(r); + return r; +} + +static int using_namespace_objects(lua_State * L) { + int nargs = lua_gettop(L); + environment const & env = to_environment(L, 1); + name n = to_name_ext(L, 2); + if (nargs == 2) + return push_environment(L, using_namespace(env, get_io_state(L), n)); + else if (nargs == 3) + return push_environment(L, using_namespace(env, get_io_state(L), n, to_name_ext(L, 3))); + else + return push_environment(L, using_namespace(env, to_io_state(L, 4), n, to_name_ext(L, 3))); +} + +static int push_scope(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 1) + return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L))); + else if (nargs == 2) + return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), to_name_ext(L, 2))); + else + return push_environment(L, push_scope(to_environment(L, 1), to_io_state(L, 3), to_name_ext(L, 2))); +} + +static int pop_scope(lua_State * L) { + return push_environment(L, pop_scope(to_environment(L, 1))); +} + +void open_scoped_ext(lua_State * L) { + SET_GLOBAL_FUN(using_namespace_objects, "using_namespace_objects"); + SET_GLOBAL_FUN(push_scope, "push_scope"); + SET_GLOBAL_FUN(pop_scope, "pop_scope"); +} +} diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h new file mode 100644 index 000000000..f8ec1a982 --- /dev/null +++ b/src/library/scoped_ext.h @@ -0,0 +1,181 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "util/list.h" +#include "util/rb_map.h" +#include "util/name.h" +#include "util/lua.h" +#include "kernel/environment.h" +#include "library/io_state.h" +#include "library/module.h" + +namespace lean { +typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &); +typedef environment (*push_scope_fn)(environment const &); +typedef environment (*pop_scope_fn)(environment const &); + +void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop); +/** \brief Use objects defined in the namespace \c n, if \c c is not the anonymous name, then only object from "class" \c c are considered. */ +environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c = name()); +/** \brief Create a new scope, all scoped extensions are notified. */ +environment push_scope(environment const & env, io_state const & ios, name const & n = name()); +/** \brief Delete the most recent scope, all scoped extensions are notified. */ +environment pop_scope(environment const & env); + +name const & get_namespace(environment const & env); +bool in_section(environment const & env); + +void open_scoped_ext(lua_State * L); + +/** + \brief Auxilary template used to simplify the creation of environment extensions that support + the scope +*/ +template +class scoped_ext : public environment_extension { + typedef typename Config::state state; + typedef typename Config::entry entry; + static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) { + Config::add_entry(env, ios, s, e); + } + static void write_entry(serializer & s, entry const & e) { Config::write_entry(s, e); } + static entry read_entry(deserializer & d) { return Config::read_entry(d); } + static name const & get_class_name() { return Config::get_class_name(); } + static std::string const & get_serialization_key() { return Config::get_serialization_key(); } + + state m_state; + list m_scopes; + rb_map, name_quick_cmp> m_entries; + + void using_namespace_core(environment const & env, io_state const & ios, name const & n) { + if (auto it = m_entries.find(n)) { + buffer entries; + to_buffer(*it, entries); + unsigned i = entries.size(); + while (i > 0) { + --i; + add_entry(env, ios, m_state, entries[i]); + } + } + } + + void register_entry_core(name n, entry const & e) { + while (!n.is_anonymous()) { + if (auto it = m_entries.find(n)) + m_entries.insert(n, list(e, *it)); + else + m_entries.insert(n, list(e)); + n = n.get_prefix(); + } + } + + void add_entry_core(environment const & env, io_state const & ios, entry const & e) { + add_entry(env, ios, m_state, e); + } + + scoped_ext _register_entry(environment const & env, io_state const & ios, name n, entry const & e) const { + lean_assert(get_namespace(env).is_anonymous()); + scoped_ext r(*this); + r.register_entry_core(n, e); + if (n.is_anonymous()) + add_entry(env, ios, r.m_state, e); + return r; + } + + scoped_ext _add_entry(environment const & env, io_state const & ios, entry const & e) const { + scoped_ext r(*this); + r.register_entry_core(get_namespace(env), e); + add_entry(env, ios, r.m_state, e); + return r; + } + + scoped_ext _add_tmp_entry(environment const & env, io_state const & ios, entry const & e) const { + scoped_ext r(*this); + add_entry(env, ios, r.m_state, e); + return r; + } + +public: + scoped_ext using_namespace(environment const & env, io_state const & ios, name const & n) const { + scoped_ext r(*this); + r.using_namespace_core(env, ios, n); + return r; + } + + scoped_ext push() const { + scoped_ext r(*this); + r.m_scopes = list(m_state, r.m_scopes); + return r; + } + + scoped_ext pop() const { + lean_assert(!is_nil(m_scopes)); + scoped_ext r(*this); + r.m_state = head(m_scopes); + r.m_scopes = tail(m_scopes); + return r; + } + + struct reg { + unsigned m_ext_id; + reg() { + register_scoped_ext(get_class_name(), using_namespace_fn, push_fn, pop_fn); + register_module_object_reader(get_serialization_key(), reader); + m_ext_id = environment::register_extension(std::make_shared()); + } + }; + + static reg g_ext; + static scoped_ext const & get(environment const & env) { + return static_cast(env.get_extension(g_ext.m_ext_id)); + } + static environment update(environment const & env, scoped_ext const & ext) { + return env.update(g_ext.m_ext_id, std::make_shared(ext)); + } + static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) { + return update(env, get(env).using_namespace(env, ios, n)); + } + static environment push_fn(environment const & env) { + return update(env, get(env).push()); + } + static environment pop_fn(environment const & env) { + return update(env, get(env).pop()); + } + static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) { + return update(env, get(env)._register_entry(env, ios, n, e)); + } + static environment add_entry(environment env, io_state const & ios, entry const & e) { + if (in_section(env)) { + return update(env, get(env)._add_tmp_entry(env, ios, e)); + } else { + name n = get_namespace(env); + env = module::add(env, get_serialization_key(), [=](serializer & s) { + s << n; + write_entry(s, e); + }); + return update(env, get(env)._add_entry(env, ios, e)); + } + } + static void reader(deserializer & d, module_idx, shared_environment &, + std::function &, + std::function & add_delayed_update) { + name n; + d >> n; + entry e = read_entry(d); + add_delayed_update([=](environment const & env, io_state const & ios) -> environment { + return register_entry(env, ios, n, e); + }); + } + static state const & get_state(environment const & env) { + return get(env).m_state; + } +}; + +template +typename scoped_ext::reg scoped_ext::g_ext; +} diff --git a/tests/lua/namespace1.lua b/tests/lua/namespace1.lua deleted file mode 100644 index e6a823283..000000000 --- a/tests/lua/namespace1.lua +++ /dev/null @@ -1,23 +0,0 @@ -local env = environment() -env = env:begin_namespace_scope("foo") -assert(env:get_namespace() == name("foo")) -env = add_decl(env, mk_var_decl(name(env:get_namespace(), "nat"), Type)) -env = add_decl(env, mk_var_decl(name(env:get_namespace(), "int"), Type)) -env = env:begin_namespace_scope("bar") -assert(env:get_namespace() == name("foo", "bar")) -assert(env:namespace_find("int"):name() == name("foo", "int")) -assert(env:namespace_find("nat"):name() == name("foo", "nat")) -env = add_decl(env, mk_var_decl(name(env:get_namespace(), "int"), Type)) -assert(env:namespace_find("int"):name() == name("foo", "bar", "int")) -assert(env:get_name_in_namespace(name("foo", "bar", "int")) == name("int")) -assert(env:get_name_in_namespace(name("foo", "int")) == name("foo", "int")) -- it was shadowed by foo.bar.int -assert(env:get_name_in_namespace(name("foo", "nat")) == name("nat")) -env = env:end_scope() -assert(env:get_namespace() == name("foo")) -assert(env:get_name_in_namespace(name("foo", "bar", "int")) == name("bar", "int")) -assert(env:get_name_in_namespace(name("foo", "nat")) == name("nat")) -env = env:end_scope() -assert(env:get_name_in_namespace(name("foo", "bar", "int")) == name("foo", "bar", "int")) -assert(env:get_name_in_namespace(name("foo", "nat")) == name("foo", "nat")) -check_error(function() env = env:end_scope() end) -assert(env:get_namespace() == name()) diff --git a/tests/lua/scope.lua b/tests/lua/scope.lua new file mode 100644 index 000000000..97bbddd88 --- /dev/null +++ b/tests/lua/scope.lua @@ -0,0 +1,121 @@ +local env = environment() +local l = param_univ("l") +local nat = Const("nat") +local real = Const("real") +local one = Const("one") +local Ul = mk_sort(l) +local lst_l = Const("lst", {l}) +local vec_l = Const("vec", {l}) +local mat_l = Const("mat", {l}) +local A = Local("A", Ul) +local n = Local("n", nat) +local ll = Local("ll", lst_l(A)) +local len_l = Const("len", {l}) +local lst_1 = Const("lst", {1}) +local l1 = param_univ("l1") +local l2 = param_univ("l2") +local m = Local("m", nat) +env = add_decl(env, mk_var_decl("nat", Type)) +env = add_decl(env, mk_var_decl("real", Type)) +env = add_decl(env, mk_var_decl("one", nat)) +env = add_decl(env, mk_var_decl("lst", {l}, mk_arrow(Ul, Ul))) +env = add_decl(env, mk_var_decl("len", {l}, Pi(A, mk_arrow(lst_l(A), nat)))) +env = add_decl(env, mk_var_decl("vec", {l}, mk_arrow(Ul, nat, Ul))) +env = add_decl(env, mk_var_decl("mat", {l}, mk_arrow(Ul, nat, nat, Ul))) +env = add_decl(env, mk_var_decl("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2))))) +env = add_decl(env, mk_var_decl("vec2lst", {l}, Pi({A, n}, mk_arrow(vec_l(A, n), lst_l(A))))) +env = add_decl(env, mk_var_decl("lst2vec", {l}, Pi({A, ll}, vec_l(A, len_l(A, ll))))) +env = add_decl(env, mk_var_decl("vec2mat", {l}, Pi({A, n}, mk_arrow(vec_l(A, n), mat_l(A, n, one))))) +env = add_decl(env, mk_var_decl("mat2dlst", {l}, Pi({A, n, m}, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat))))) +env = add_decl(env, mk_var_decl("nat2lst", mk_arrow(nat, lst_1(nat)))) +env = add_coercion(env, "lst2vec") +env = push_scope(env, "tst") +local lst_nat = lst_1(nat) +print(get_coercion(env, lst_nat, "vec")) +env = add_coercion(env, "vec2mat") +print(get_coercion(env, lst_nat, "mat")) +assert(env:type_check(get_coercion(env, lst_nat, "mat"))) +function get_num_coercions(env) + local r = 0 + for_each_coercion_user(env, function(C, D, f) r = r + 1 end) + return r +end +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 3) +env = pop_scope(env) +print("---------") +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 1) +print("---------") +env = push_scope(env) +env = using_namespace_objects(env, "tst") +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 3) +env = pop_scope(env) +print("---------") +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 1) +print("---------") +env = push_scope(env, "tst") +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 3) +print("---------") +env = push_scope(env) +env = add_coercion(env, "nat2lst") +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 6) +print("---------") +env = pop_scope(env) +assert(get_num_coercions(env) == 3) +env = pop_scope(env) +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +assert(get_num_coercions(env) == 1) +env = push_scope(env, "tst") +assert(get_num_coercions(env) == 3) + + +os.exit(0) + + + + +print(get_coercion(env, nat, "mat")) +assert(env:type_check(get_coercion(env, nat, "mat"))) +env = add_coercion(env, "mat2dlst") +print("---------") +for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +print(get_coercion(env, lst_nat, "dlst")) +assert(env:type_check(get_coercion(env, lst_nat, "dlst"))) + +env:export("coe1_mod.olean") +local env2 = import_modules("coe1_mod") +print(get_coercion(env2, lst_nat, "dlst")) +assert(env2:type_check(get_coercion(env2, lst_nat, "dlst"))) +assert(is_coercion(env2, "vec2mat")) +assert(is_coercion(env2, "lst2vec")) +env2 = add_decl(env2, mk_var_decl("lst2vec2", {l}, Pi({A, ll}, vec_l(A, len_l(A, ll))))) +print("======") +env2 = add_coercion(env2, "lst2vec2") +print("======") +print(get_coercion(env2, lst_nat, "dlst")) +print("---------") +for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) +env2 = add_coercion(env2, "vec2lst") +env2 = add_decl(env2, mk_var_decl("lst2nat", {l}, Pi({A}, mk_arrow(lst_l(A), nat)))) +env2 = add_coercion(env2, "lst2nat") +print("---------") +for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D)) end) +for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) + +assert(has_coercions_from(env2, lst_nat)) +assert(not has_coercions_from(env2, Const("foo"))) +assert(not has_coercions_from(env2, Const("lst", {1}))) +assert(has_coercions_from(env2, Const("vec", {1})(nat, one))) +assert(not has_coercions_from(env2, Const("vec", {1})(nat))) +assert(not has_coercions_from(env2, Const("vec")(nat, one))) + +print("Coercions (vec nat one): ") +cs = get_user_coercions(env2, Const("vec", {1})(nat, one)) +for i = 1, #cs do + print(tostring(cs[i][1]) .. " : " .. tostring(cs[i][3]) .. " : " .. tostring(cs[i][2])) +end diff --git a/tests/lua/sect1.lua b/tests/lua/sect1.lua deleted file mode 100644 index 648aef1f5..000000000 --- a/tests/lua/sect1.lua +++ /dev/null @@ -1,21 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -local A = Const("A") -env = add_decl(env, mk_var_decl("R", mk_arrow(A, A, Bool))) -local R = Const("R") -local a = Local("a", A) -env = add_decl(env, mk_definition("reflexive", Bool, Pi(a, R(a, a)))) -env = add_decl(env, mk_definition("id", mk_arrow(A, A), Fun(a, a))) -env = env:end_scope() -local A1 = Local("A", mk_sort(mk_param_univ("l"))) -local R1 = Local("R", mk_arrow(A1, A1, Bool)) -local a1 = Local("a", A1) -print(env:find("reflexive"):type()) -print(env:find("reflexive"):value()) -assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool)) -assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1)))) -print(env:find("id"):type()) -print(env:find("id"):value()) diff --git a/tests/lua/sect10.lua b/tests/lua/sect10.lua deleted file mode 100644 index 045f2f248..000000000 --- a/tests/lua/sect10.lua +++ /dev/null @@ -1,34 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:begin_section_scope() -local nat = Const("nat") -env = add_inductive(env, - "nat", Type, - "zero", nat, - "succ", mk_arrow(nat, nat)) -local zero = Const("zero") -local succ = Const("succ") -local one = succ(zero) -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true)) -local A = Const("A") -local l1 = mk_param_univ("l") -local D = Const("D", {l1}) -local n = Local("n", nat) -env = add_inductive(env, - "D", {l1}, 1, mk_arrow(nat, nat, mk_sort(max_univ(l1, l, 1))), - "mk1", Pi(n, mk_arrow(A, D(n, one))), - "mk0", Pi(n, mk_arrow(A, A, D(n, zero)))) -print(env:find("D_rec"):type()) -env = env:end_scope() -env = env:end_scope() -print(env:find("D_rec"):type()) - -local l = mk_param_univ("l") -local A = Local("A", mk_sort(l)) -local l1 = mk_param_univ("l_1") -local D = Const("D", {l, l1}) -print(env:find("mk1"):type()) -assert(env:find("mk1"):type() == Pi({A, n}, mk_arrow(A, D(A, n, one)))) diff --git a/tests/lua/sect1b.lua b/tests/lua/sect1b.lua deleted file mode 100644 index 68d6f8c9e..000000000 --- a/tests/lua/sect1b.lua +++ /dev/null @@ -1,12 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -local l1 = mk_param_univ("l1") -env = add_decl(env, mk_definition("A", {l1}, mk_sort(max_univ(l, l1)+1), mk_sort(max_univ(l, l1)))) -env = env:end_scope() -local ls = env:find("A"):univ_params() -assert(#ls == 2) -print(ls:head()) -assert(ls:head() == name("l")) -assert(ls:tail():head() == name("l1")) diff --git a/tests/lua/sect1c.lua b/tests/lua/sect1c.lua deleted file mode 100644 index fc0e2ed32..000000000 --- a/tests/lua/sect1c.lua +++ /dev/null @@ -1,13 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -local l1 = mk_param_univ("l") -env = add_decl(env, mk_definition("A", {l1}, mk_sort(max_univ(l, l1)+1), mk_sort(max_univ(l, l1)))) -env = env:end_scope() -print (env:find("A"):type()) -local ls = env:find("A"):univ_params() -assert(#ls == 2) -print(ls:head()) -assert(ls:head() == name("l")) -assert(ls:tail():head() == name("l_1")) diff --git a/tests/lua/sect2.lua b/tests/lua/sect2.lua deleted file mode 100644 index eb9d53517..000000000 --- a/tests/lua/sect2.lua +++ /dev/null @@ -1,11 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -local A = Const("A") -local l2 = mk_param_univ("l") -check_error(function() - env = add_decl(env, mk_var_decl("R", {l2}, mk_arrow(A, A, mk_sort(l2)))) - end -) diff --git a/tests/lua/sect3.lua b/tests/lua/sect3.lua deleted file mode 100644 index 661b38cad..000000000 --- a/tests/lua/sect3.lua +++ /dev/null @@ -1,26 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -local A = Const("A") -env = add_decl(env, mk_var_decl("R", mk_arrow(A, A, Bool))) -local R = Const("R") -local a = Local("a", A) -env = add_decl(env, mk_definition("reflexive", Bool, Pi(a, R(a, a)))) -env, id_prv = add_private_name(env, "id") -env = add_decl(env, mk_definition(id_prv, mk_arrow(A, A), Fun(a, a))) -assert(user_to_hidden_name(env, "id") == id_prv) -assert(hidden_to_user_name(env, id_prv) == name("id")) -env = env:end_scope() -local A1 = Local("A", mk_sort(mk_param_univ("l"))) -local R1 = Local("R", mk_arrow(A1, A1, Bool)) -local a1 = Local("a", A1) -print(env:find("reflexive"):type()) -print(env:find("reflexive"):value()) -assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool)) -assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1)))) -assert(not user_to_hidden_name(env, "id")) -assert(hidden_to_user_name(env, id_prv) == name("id")) -print(env:find(id_prv):type()) -print(env:find(id_prv):value()) diff --git a/tests/lua/sect4.lua b/tests/lua/sect4.lua deleted file mode 100644 index 487540858..000000000 --- a/tests/lua/sect4.lua +++ /dev/null @@ -1,22 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true)) -local A = Const("A") -local list = Const("list") -env = add_inductive(env, - "list", mk_sort(max_univ(l, 1)), - "nil", list, - "cons", mk_arrow(A, list, list)) -print(env:find("list_rec"):type()) -assert(env:find("cons"):type() == mk_arrow(A, list, list)) -env = env:end_scope() -print(env:find("list_rec"):type()) -print(env:find("cons"):type()) - -local l = mk_param_univ("l") -local A = Local("A", mk_sort(l)) -local list = Const("list", {l}) -assert(env:find("cons"):type() == Pi({A}, mk_arrow(A, list(A), list(A)))) diff --git a/tests/lua/sect5.lua b/tests/lua/sect5.lua deleted file mode 100644 index 28869005b..000000000 --- a/tests/lua/sect5.lua +++ /dev/null @@ -1,26 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true)) -local A = Const("A") -local list = Const("list") -env = add_inductive(env, - "list", mk_sort(max_univ(l, 1)), - "nil", list, - "cons", mk_arrow(A, list, list)) -print(env:find("list_rec"):type()) -assert(env:find("cons"):type() == mk_arrow(A, list, list)) -env = env:end_scope() -print(env:find("list_rec"):type()) -print(env:find("cons"):type()) -local l = mk_param_univ("l") -local A = Local("A", mk_sort(l)) -local list = Const("list", {l}) -assert(env:find("cons"):type() == Pi({A}, mk_arrow(A, list(A), list(A)))) -env = env:end_scope() - -print(env:find("list_rec"):type()) -print(env:find("cons"):type()) diff --git a/tests/lua/sect6.lua b/tests/lua/sect6.lua deleted file mode 100644 index 83b1cf29c..000000000 --- a/tests/lua/sect6.lua +++ /dev/null @@ -1,27 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -local A = Const("A") -env = add_decl(env, mk_var_decl("R", mk_arrow(A, A, Bool))) -local R = Const("R") -local a = Local("a", A) -env = add_decl(env, mk_definition("reflexive", Bool, Pi(a, R(a, a)))) -env = add_decl(env, mk_definition("id", mk_arrow(A, A), Fun(a, a))) -env = env:end_scope() -local A1 = Local("A", mk_sort(mk_param_univ("l"))) -local R1 = Local("R", mk_arrow(A1, A1, Bool)) -local a1 = Local("a", A1) -print(env:find("reflexive"):type()) -print(env:find("reflexive"):value()) -assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool)) -assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1)))) -print(env:find("id"):type()) -print(env:find("id"):value()) -env = env:end_scope() -print(env:find("reflexive"):type()) -print(env:find("reflexive"):value()) -assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool)) -assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1)))) diff --git a/tests/lua/sect7.lua b/tests/lua/sect7.lua deleted file mode 100644 index 356300ee8..000000000 --- a/tests/lua/sect7.lua +++ /dev/null @@ -1,42 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -local A = Const("A") -env = add_decl(env, mk_var_decl("R", mk_arrow(A, A, Bool))) -local R = Const("R") -local a = Local("a", A) -env = add_decl(env, mk_definition("reflexive", Bool, Pi(a, R(a, a)))) -env, id_prv = add_private_name(env, "id") -env = add_decl(env, mk_definition(id_prv, mk_arrow(A, A), Fun(a, a))) -assert(user_to_hidden_name(env, "id") == id_prv) -assert(hidden_to_user_name(env, id_prv) == name("id")) -env = env:end_scope() -local A1 = Local("A", mk_sort(mk_param_univ("l"))) -local R1 = Local("R", mk_arrow(A1, A1, Bool)) -local a1 = Local("a", A1) -print(env:find("reflexive"):type()) -print(env:find("reflexive"):value()) -assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool)) -assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1)))) -assert(not user_to_hidden_name(env, "id")) -assert(hidden_to_user_name(env, id_prv) == name("id")) -print(env:find(id_prv):type()) -print(env:find(id_prv):value()) -env = env:end_scope() -print(env:find("reflexive"):type()) -print(env:find("reflexive"):value()) -assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool)) -assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1)))) -assert(not user_to_hidden_name(env, "id")) -assert(hidden_to_user_name(env, id_prv) == name("id")) -print(env:find(id_prv):type()) -print(env:find(id_prv):value()) -env:export("sect7_mod.olean") -local env2 = import_modules("sect7_mod") -assert(hidden_to_user_name(env2, id_prv) == name("id")) -print(env2:find(id_prv):type()) -assert(env2:find(id_prv):type() == env:find(id_prv):type()) -assert(env2:find(id_prv):value() == env:find(id_prv):value()) diff --git a/tests/lua/sect8.lua b/tests/lua/sect8.lua deleted file mode 100644 index ff7c33e36..000000000 --- a/tests/lua/sect8.lua +++ /dev/null @@ -1,39 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -local nat = Const("nat") -env = add_inductive(env, - "nat", Type, - "zero", nat, - "succ", mk_arrow(nat, nat)) -local zero = Const("zero") -local succ = Const("succ") - -env = env:begin_section_scope() -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true)) -local A = Const("A") -local vector = Const("vector") -local n = Local("n", nat) -env = add_inductive(env, - "vector", mk_arrow(nat, mk_sort(max_univ(l, 1))), - "nil", vector(zero), - "cons", Pi(n, mk_arrow(A, vector(n), vector(succ(n))))) - -print(env:find("vector_rec"):type()) -assert(env:find("cons"):type() == Pi(n, mk_arrow(A, vector(n), vector(succ(n))))) -env = env:end_scope() -print(env:find("vector_rec"):type()) -print(env:find("cons"):type()) -local l = mk_param_univ("l") -local A = Local("A", mk_sort(l)) -local vector = Const("vector", {l}) -assert(env:find("cons"):type() == Pi({A, n}, mk_arrow(A, vector(A, n), vector(A, succ(n))))) -env = env:end_scope() - -print(env:find("vector_rec"):type()) -print(env:find("cons"):type()) -env:export("sect8_mod.olean") -local env2 = import_modules("sect8_mod") -assert(env:find("vector_rec"):type() == env2:find("vector_rec"):type()) diff --git a/tests/lua/sect9.lua b/tests/lua/sect9.lua deleted file mode 100644 index d597904c4..000000000 --- a/tests/lua/sect9.lua +++ /dev/null @@ -1,33 +0,0 @@ -local env = environment() -env = env:begin_section_scope() -env = env:begin_section_scope() -local nat = Const("nat") -env = add_inductive(env, - "nat", Type, - "zero", nat, - "succ", mk_arrow(nat, nat)) -local zero = Const("zero") -local succ = Const("succ") -local one = succ(zero) -env = env:add_global_level("l") -local l = mk_global_univ("l") -env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true)) -env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true)) -local A = Const("A") -local l1 = mk_param_univ("l1") -local D = Const("D", {l1}) -local n = Local("n", nat) -env = add_inductive(env, - "D", {l1}, 1, mk_arrow(nat, nat, mk_sort(max_univ(l1, l, 1))), - "mk1", Pi(n, mk_arrow(A, D(n, one))), - "mk0", Pi(n, mk_arrow(A, A, D(n, zero)))) -print(env:find("D_rec"):type()) -env = env:end_scope() -env = env:end_scope() -print(env:find("D_rec"):type()) - -local l = mk_param_univ("l") -local A = Local("A", mk_sort(l)) -local D = Const("D", {l, l1}) -print(env:find("mk1"):type()) -assert(env:find("mk1"):type() == Pi({A, n}, mk_arrow(A, D(A, n, one))))