diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 451dd791c..de1132820 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -111,6 +111,10 @@ static level_param_core const & to_param_core(level const & l) { name const & param_id(level const & l) { lean_assert(is_param(l)); return to_param_core(l).m_id; } name const & global_id(level const & l) { lean_assert(is_global(l)); return to_param_core(l).m_id; } name const & meta_id(level const & l) { lean_assert(is_meta(l)); return to_param_core(l).m_id; } +name const & level_id(level const & l) { + lean_assert(is_param(l) || is_global(l) || is_meta(l)); + return to_param_core(l).m_id; +} void level_cell::dealloc() { switch (m_kind) { diff --git a/src/kernel/level.h b/src/kernel/level.h index 4ca617663..52de40e18 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -106,6 +106,7 @@ level const & succ_of(level const & l); name const & param_id(level const & l); name const & global_id(level const & l); name const & meta_id(level const & l); +name const & level_id(level const & l); /** \brief Return true iff \c l is an explicit level. We say a level l is explicit iff diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index d9b588ffd..646f464d6 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -28,6 +28,7 @@ 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. @@ -1104,15 +1105,21 @@ static int environment_prop_proof_irrel(lua_State * L) { return push_boolean(L, static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, to_environment(L, 1).cls_proof_irrel()); } 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, module::add_global_level(to_environment(L, 1), to_name_ext(L, 2))); } +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))); +} 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, module::add(to_environment(L, 1), to_declaration(L, 2))); + return push_environment(L, scope::add(to_environment(L, 1), to_declaration(L, 2), info)); else - return push_environment(L, module::add(to_environment(L, 1), to_certified_declaration(L, 2))); + return push_environment(L, scope::add(to_environment(L, 1), to_certified_declaration(L, 2), info)); } 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) { @@ -1197,28 +1204,43 @@ 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}, - {"trust_lvl", safe_function}, - {"trust_level", safe_function}, - {"prop_proof_irrel", safe_function}, - {"cls_proof_irrel", safe_function}, - {"eta", safe_function}, - {"impredicative", safe_function}, - {"add_global_level", safe_function}, - {"is_global_level", safe_function}, - {"find", safe_function}, - {"get", safe_function}, - {"add", safe_function}, - {"replace", safe_function}, - {"forget", safe_function}, - {"whnf", safe_function}, - {"normalize", safe_function}, - {"infer_type", safe_function}, - {"type_check", safe_function}, - {"for_each", safe_function}, - {"export", safe_function}, + {"__gc", environment_gc}, // never throws + {"is_descendant", safe_function}, + {"trust_lvl", safe_function}, + {"trust_level", safe_function}, + {"prop_proof_irrel", safe_function}, + {"cls_proof_irrel", safe_function}, + {"eta", safe_function}, + {"impredicative", safe_function}, + {"add_global_level", safe_function}, + {"is_global_level", safe_function}, + {"find", safe_function}, + {"get", safe_function}, + {"add", safe_function}, + {"replace", safe_function}, + {"forget", safe_function}, + {"whnf", safe_function}, + {"normalize", safe_function}, + {"infer_type", safe_function}, + {"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} }; @@ -1859,7 +1881,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, module::add(to_environment(L, 1), *d)); + return push_environment(L, scope::add(to_environment(L, 1), *d)); } static void open_type_checker(lua_State * L) { diff --git a/src/library/register_module.h b/src/library/register_module.h index c5867a31e..c3e43f5a3 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/private.h" #include "library/placeholder.h" #include "library/aliases.h" -#include "library/scope.h" // #include "library/fo_unify.h" // #include "library/hop_match.h" @@ -24,7 +23,6 @@ inline void open_core_module(lua_State * L) { open_private(L); open_placeholder(L); open_aliases(L); - open_scope(L); // open_fo_unify(L); // open_hop_match(L); } diff --git a/src/library/scope.cpp b/src/library/scope.cpp index f36161704..a6dd41898 100644 --- a/src/library/scope.cpp +++ b/src/library/scope.cpp @@ -5,16 +5,199 @@ 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_map.h" +#include "kernel/replace_fn.h" +#include "kernel/abstract.h" +#include "kernel/type_checker.h" #include "library/scope.h" -#include "library/kernel_bindings.h" +#include "library/module.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 = map2(m_level_deps, [](name const & n) { return mk_param_univ(n); }); + } +}; + +typedef name_map decl_info_map; +typedef name_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(const_levels(e), info.m_levels)), 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_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 const & d) { + lean_assert(d.is_definition()); + 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(d.get_params(), level_deps); + 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); + if (d.is_definition()) { + declaration new_d = mk_definition(d.get_name(), new_ls, new_type, new_value, d.is_opaque(), + d.get_weight(), d.get_module_idx(), d.use_conv_opt()); + m_env = module::add(m_env, check(m_env, new_d)); + } else { + declaration new_d = mk_theorem(d.get_name(), new_ls, new_type, new_value); + m_env = module::add(m_env, check(m_env, new_d)); + } + } +}; + struct scope_ext : public environment_extension { - enum class scope_kind { Namespace, Section }; struct section { - environment m_prev_env; + 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; @@ -34,32 +217,98 @@ static environment update(environment const & env, scope_ext const & ext) { return env.update(g_ext.m_ext_id, std::make_shared(ext)); } -environment begin_section_scope(environment const & env) { - // TODO(Leo) - return env; +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 begin_namespace_scope(environment const & env, char const * n) { +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_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); +} + +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_scope(environment const & env) { +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"); - switch (head(ext.m_scope_kinds)) { + 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); - break; - case scope_ext::scope_kind::Section: - // TODO(Leo) - break; - } - ext.m_scope_kinds = tail(ext.m_scope_kinds); - return update(env, ext); + 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(); + } + ext.m_sections = tail(ext.m_sections); + return update(ctx.env(), ext); + }} + lean_unreachable(); // LCOV_EXCL_LINE } name const & get_namespace(environment const & env) { @@ -97,22 +346,5 @@ name get_name_in_namespace(environment const & env, name const & n) { } return n; } - -static int begin_section_scope(lua_State * L) { return push_environment(L, begin_section_scope(to_environment(L, 1))); } -static int begin_namespace_scope(lua_State * L) { return push_environment(L, begin_namespace_scope(to_environment(L, 1), lua_tostring(L, 2))); } -static int end_scope(lua_State * L) { return push_environment(L, end_scope(to_environment(L, 1))); } -static int get_namespace(lua_State * L) { return push_name(L, get_namespace(to_environment(L, 1))); } -static int get_name_in_namespace(lua_State * L) { - return push_name(L, get_name_in_namespace(to_environment(L, 1), to_name_ext(L, 2))); -} -static int find_decl(lua_State * L) { return push_optional_declaration(L, find(to_environment(L, 1), to_name_ext(L, 2))); } - -void open_scope(lua_State * L) { - SET_GLOBAL_FUN(begin_section_scope, "begin_section_scope"); - SET_GLOBAL_FUN(begin_namespace_scope, "begin_namespace_scope"); - SET_GLOBAL_FUN(end_scope, "end_scope"); - SET_GLOBAL_FUN(get_namespace, "get_namespace"); - SET_GLOBAL_FUN(get_name_in_namespace, "get_name_in_namespace"); - SET_GLOBAL_FUN(find_decl, "find_decl"); } } diff --git a/src/library/scope.h b/src/library/scope.h index 20dec80ec..e58e5b02b 100644 --- a/src/library/scope.h +++ b/src/library/scope.h @@ -6,28 +6,75 @@ Author: Leonardo de Moura */ #pragma once #include -#include "util/lua.h" +#include #include "kernel/environment.h" namespace lean { +namespace scope { +typedef std::vector dependencies; // local var dependencies + +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 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_scope(environment const & env); +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_scope(environment const & env, char const * n); +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_scope(environment const & env); +environment end(environment const & env); /** \brief Return the current namespace for \c env. The namespace is composed by the sequence @@ -44,6 +91,5 @@ 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); - -void open_scope(lua_State * L); +} } diff --git a/tests/lua/namespace1.lua b/tests/lua/namespace1.lua index 2dee12ff2..e6a823283 100644 --- a/tests/lua/namespace1.lua +++ b/tests/lua/namespace1.lua @@ -1,23 +1,23 @@ local env = environment() -env = begin_namespace_scope(env, "foo") -assert(get_namespace(env) == name("foo")) -env = add_decl(env, mk_var_decl(name(get_namespace(env), "nat"), Type)) -env = add_decl(env, mk_var_decl(name(get_namespace(env), "int"), Type)) -env = begin_namespace_scope(env, "bar") -assert(get_namespace(env) == name("foo", "bar")) -assert(find_decl(env, "int"):name() == name("foo", "int")) -assert(find_decl(env, "nat"):name() == name("foo", "nat")) -env = add_decl(env, mk_var_decl(name(get_namespace(env), "int"), Type)) -assert(find_decl(env, "int"):name() == name("foo", "bar", "int")) -assert(get_name_in_namespace(env, name("foo", "bar", "int")) == name("int")) -assert(get_name_in_namespace(env, name("foo", "int")) == name("foo", "int")) -- it was shadowed by foo.bar.int -assert(get_name_in_namespace(env, name("foo", "nat")) == name("nat")) -env = end_scope(env) -assert(get_namespace(env) == name("foo")) -assert(get_name_in_namespace(env, name("foo", "bar", "int")) == name("bar", "int")) -assert(get_name_in_namespace(env, name("foo", "nat")) == name("nat")) -env = end_scope(env) -assert(get_name_in_namespace(env, name("foo", "bar", "int")) == name("foo", "bar", "int")) -assert(get_name_in_namespace(env, name("foo", "nat")) == name("foo", "nat")) -check_error(function() env = end_scope(env) end) -assert(get_namespace(env) == name()) +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/sect1.lua b/tests/lua/sect1.lua new file mode 100644 index 000000000..648aef1f5 --- /dev/null +++ b/tests/lua/sect1.lua @@ -0,0 +1,21 @@ +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/sect2.lua b/tests/lua/sect2.lua new file mode 100644 index 000000000..eb9d53517 --- /dev/null +++ b/tests/lua/sect2.lua @@ -0,0 +1,11 @@ +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 +)