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

feat(library/kernel_bindings): add remaining type_checker constructors in the Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-08 17:13:06 -07:00
parent 3aa1afdf51
commit 95262fb68d
1 changed files with 21 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/kernel_bindings.cpp
View file

@ -1414,6 +1414,12 @@ static void open_constraint_handler(lua_State * L) {
typedef std::shared_ptr<type_checker> type_checker_ref;
DECL_UDATA(type_checker_ref)
static void get_type_checker_args(lua_State * L, int idx, optional<module_idx> & mod_idx, bool & memoize, name_set & extra_opaque) {
mod_idx = get_opt_uint_named_param(L, idx, "module_idx", optional<module_idx>());
memoize = get_bool_named_param(L, idx, "memoize", true);
extra_opaque = get_name_set_named_param(L, idx, "extra_opaque", name_set());
}
int mk_type_checker(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs <= 2) {
@ -1421,12 +1427,23 @@ int mk_type_checker(lua_State * L) {
} else if (nargs == 3 && is_lua_constraint_handler(L, 3)) {
return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
to_lua_constraint_handler(L, 3)));
} else if (nargs == 3) {
// TODO(Leo)
} else {
// TODO(Leo)
optional<module_idx> mod_idx; bool memoize; name_set extra_opaque;
if (nargs == 3) {
get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque);
auto t = std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque),
memoize);
return push_type_checker_ref(L, t);
} else {
get_type_checker_args(L, 4, mod_idx, memoize, extra_opaque);
auto t = std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
to_lua_constraint_handler(L, 3),
mk_default_converter(to_environment(L, 1), mod_idx, memoize, extra_opaque),
memoize);
return push_type_checker_ref(L, t);
}
}
return 0;
}
int type_checker_whnf(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); }
int type_checker_ensure_pi(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->ensure_pi(to_expr(L, 2))); }