michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/scope): add sections

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-31 21:44:12 -07:00
parent 286d7f0e64
commit 585f3adde1
9 changed files with 423 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/level.cpp
View file

@ -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) {

1
src/kernel/level.h
View file

@ -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

30
src/library/kernel_bindings.cpp
View file

@ -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,6 +1204,15 @@ 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<environment_is_descendant>},
@ -1219,6 +1235,12 @@ static const struct luaL_Reg environment_m[] = {
{"type_check", safe_function<environment_type_check>},
{"for_each", safe_function<environment_for_each>},
{"export", safe_function<export_module>},
{"begin_section_scope", safe_function<begin_section_scope>},
{"begin_namespace_scope", safe_function<begin_namespace_scope>},
{"end_scope", safe_function<end_scope>},
{"get_namespace", safe_function<get_namespace>},
{"get_name_in_namespace", safe_function<get_name_in_namespace>},
{"namespace_find", safe_function<namespace_find>},
{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) {

2
src/library/register_module.h
View file

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

294
src/library/scope.cpp
View file

@ -5,16 +5,199 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <memory>
#include <unordered_set>
#include <vector>
#include <algorithm>
#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<level>(m_level_deps, [](name const & n) { return mk_param_univ(n); });
}
};
typedef name_map<decl_info> decl_info_map;
typedef name_map<level_info> level_info_map;
typedef std::unordered_set<name, name_hash, name_eq> 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<level>(mk_param_univ(global_id(l)));
}
}
return optional<level>();
});
}
// 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<name> 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;
list<abstraction_fn> m_fns;
section(environment const & env):m_prev_env(env) {}
};
enum class scope_kind { Namespace, Section };
list<name> m_namespaces;
list<section> m_sections;
list<scope_kind> 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<scope_ext>(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<abstraction_fn>(fn, s.m_fns);
ext.m_sections = list<scope_ext::section>(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<abstraction_context_imp&>(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<abstraction_context_imp&>(ctx).add_local_decl(d, bi);
});
} else {
return add(env, [=](abstraction_context & ctx) {
static_cast<abstraction_context_imp&>(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>(scope_ext::scope_kind::Section, ext.m_scope_kinds);
ext.m_sections = list<scope_ext::section>(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>(scope_ext::scope_kind::Namespace, ext.m_scope_kinds);
ext.m_namespaces = list<name>(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);
case scope_ext::scope_kind::Section: {
scope_ext::section const & s = head(ext.m_sections);
environment new_env = s.m_prev_env;
buffer<abstraction_fn const *> 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");
}
}

58
src/library/scope.h
View file

@ -6,28 +6,75 @@ Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "util/lua.h"
#include <vector>
#include "kernel/environment.h"
namespace lean {
namespace scope {
typedef std::vector<expr> 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<void(abstraction_context & ctx)> 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<declaration> find(environment const & env, name const & n);
void open_scope(lua_State * L);
}
}

44
tests/lua/namespace1.lua
View file

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

21
tests/lua/sect1.lua Normal file
View file

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

11
tests/lua/sect2.lua Normal file
View file

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