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

refactor(library/kernel_bindings): remove unnecessary procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 18:57:46 -08:00
parent 1640568f6a
commit f018fdabb9
2 changed files with 1 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/kernel_bindings.cpp
View file

@ -1814,26 +1814,12 @@ static void open_substitution(lua_State * L) {
// type_checker
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());
}
static int mk_type_checker(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 1) {
return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1)));
} else if (nargs == 2) {
return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2)));
} else {
optional<module_idx> mod_idx; bool memoize; name_set extra_opaque;
get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque);
extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); });
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, pred),
memoize);
return push_type_checker_ref(L, t);
return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2)));
}
}
static int type_checker_whnf(lua_State * L) { return push_ecs(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); }

4
tests/lua/env5.lua
View file

@ -55,7 +55,3 @@ assert(tc2:check(id_2(Type, a)) == Type)
assert(not pcall(function() print(tc2:check(id_1(Type, a))) end))
assert(tc2:whnf(id_2(Type, a)) == a)
assert(tc2:whnf(id_2(Type, id_2(Type, a))) == a)
local tc3 = type_checker(env, name_generator("foo"), {extra_opaque=name_set("id")})
print(tc3:whnf(id_2(Type, id_2(Type, a))))
assert(tc3:whnf(id_2(Type, id_2(Type, a))) == id_2(Type, id_2(Type, a)))
print(id_2(Type, id_2(Type, a)))