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

feat(library): new scoping framework

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-12 19:33:02 -07:00
parent d50376249f
commit a914345d29
25 changed files with 509 additions and 1006 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/CMakeLists.txt
View file

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

110
src/library/coercion.cpp
View file

@ -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, list<coercion_info>, name_quick_cmp> m_coercion_info;
// m_from and m_to contain "direct" coercions
rb_map<name, list<coercion_class>, 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<coercion_ext>()); }
};
static coercion_ext_reg g_ext;
static coercion_ext const & get_extension(environment const & env) {
return static_cast<coercion_ext const &>(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<coercion_ext>(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<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> & 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<coercion_info> 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<coercion_info> infos = *it;
infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; });
infos = list<coercion_info>(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,
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<expr> 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<name, name> 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<coercion_config>;
typedef scoped_ext<coercion_config> 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<expr> 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<std::tup
expr const & C_fn = get_app_rev_args(C, args);
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;
@ -419,7 +421,7 @@ bool get_user_coercions(environment const & env, expr const & C, buffer<std::tup
template<typename F>
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<coercion_info> const & infos) {
for (auto const & info : infos) {
f(C, info);

32
src/library/kernel_bindings.cpp
View file

@ -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<environment_is_descendant>},
@ -1283,12 +1269,6 @@ 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}
};
@ -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<intro_rule> 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))

5
src/library/module.cpp
View file

@ -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<inductive::intro_rule> const & intro_rules) {
return add_inductive(env, level_params, num_params, list<inductive::inductive_decl>(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

12
src/library/module.h
View file

@ -91,5 +91,17 @@ environment add_inductive(environment env,
level_param_names const & level_params,
unsigned num_params,
list<inductive::inductive_decl> 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<inductive::intro_rule> const & intro_rules); // introduction rules
}
}

11
src/library/private.cpp
View file

@ -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; });
}
}
std::pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {

2
src/library/register_module.h
View file

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

457
src/library/scope.cpp
View file

@ -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 <memory>
#include <unordered_set>
#include <vector>
#include <algorithm>
#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> decl_info_map;
typedef name_hash_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(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<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_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<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;
scope_ext() {}
};
struct scope_ext_reg {
unsigned m_ext_id;
scope_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<scope_ext>()); }
};
static scope_ext_reg g_ext;
static scope_ext const & get_extension(environment const & env) {
return static_cast<scope_ext const &>(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<scope_ext>(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<abstraction_fn>(fn, s.m_fns);
ext.m_sections = list<scope_ext::section>(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<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_univ_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);
}
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<inductive_decl> 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<expr> 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<expr> 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<inductive_decl> 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<inductive_decl> 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<inductive_decl> tmp_decls;
for (auto const & d : s_decls) {
expr new_type = ctx.convert(inductive_decl_type(d));
buffer<intro_rule> 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<inductive_decl> 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<intro_rule> 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<inductive::intro_rule> const & intro_rules) {
return add_inductive(env, level_params, num_params, list<inductive::inductive_decl>(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>(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(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<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();
}
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<declaration> 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;
}
}
}

125
src/library/scope.h
View file

@ -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 <string>
#include <vector>
#include "kernel/environment.h"
namespace lean {
namespace scope {
typedef std::vector<expr> 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<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 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<inductive::inductive_decl> 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<inductive::intro_rule> 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 <tt>foo.bar</tt> and \c n is <tt>foo.bar.bla.1</tt>, then
the result is <tt>bla.1</tt>.
*/
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);
}
}

122
src/library/scoped_ext.cpp Normal file
View file

@ -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 <vector>
#include <memory>
#include "library/scoped_ext.h"
#include "library/kernel_bindings.h"
namespace lean {
typedef std::tuple<name, using_namespace_fn, push_scope_fn, pop_scope_fn> entry;
typedef std::vector<entry> scoped_exts;
static scoped_exts & get_exts() {
static std::unique_ptr<std::vector<entry>> exts;
if (!exts.get())
exts.reset(new std::vector<entry>());
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<name> m_namespaces;
list<bool> 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<scope_mng_ext>()); }
};
static scope_mng_ext_reg g_ext;
static scope_mng_ext const & get_extension(environment const & env) {
return static_cast<scope_mng_ext const &>(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<scope_mng_ext>(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<name>(new_n, ext.m_namespaces);
ext.m_in_section = list<bool>(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");
}
}

181
src/library/scoped_ext.h Normal file
View file

@ -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 <string>
#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<typename Config>
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<state> m_scopes;
rb_map<name, list<entry>, 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<entry> 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<entry>(e, *it));
else
m_entries.insert(n, list<entry>(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<state>(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<scoped_ext>());
}
};
static reg g_ext;
static scoped_ext const & get(environment const & env) {
return static_cast<scoped_ext const &>(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<scoped_ext>(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<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> & 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 Config>
typename scoped_ext<Config>::reg scoped_ext<Config>::g_ext;
}

23
tests/lua/namespace1.lua
View file

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

121
tests/lua/scope.lua Normal file
View file

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

21
tests/lua/sect1.lua
View file

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

34
tests/lua/sect10.lua
View file

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

12
tests/lua/sect1b.lua
View file

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

13
tests/lua/sect1c.lua
View file

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

11
tests/lua/sect2.lua
View file

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

26
tests/lua/sect3.lua
View file

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

22
tests/lua/sect4.lua
View file

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

26
tests/lua/sect5.lua
View file

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

27
tests/lua/sect6.lua
View file

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

42
tests/lua/sect7.lua
View file

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

39
tests/lua/sect8.lua
View file

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

33
tests/lua/sect9.lua
View file

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