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

feat(library/kernel_bindings): cleanup level Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-29 17:05:25 -07:00
parent 93a61748e9
commit fd034521dc
2 changed files with 4 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/library/kernel_bindings.cpp
View file

@ -49,6 +49,7 @@ LEVEL_PRED(has_param)
LEVEL_PRED(is_not_zero)
static int level_get_kind(lua_State * L) { return pushinteger(L, static_cast<int>(kind(to_level(L, 1)))); }
static int level_trivially_leq(lua_State * L) { return pushboolean(L, is_trivial(to_level(L, 1), to_level(L, 2))); }
static int level_is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_level(L, 1), to_level(L, 2))); }
static int level_id(lua_State * L) {
level const & l = to_level(L, 1);
@ -103,6 +104,7 @@ static const struct luaL_Reg level_m[] = {
{"has_param", safe_function<level_has_param>},
{"is_not_zero", safe_function<level_is_not_zero>},
{"trivially_leq", safe_function<level_trivially_leq>},
{"is_eqp", safe_function<level_is_eqp>},
{"id", safe_function<level_id>},
{"lhs", safe_function<level_lhs>},
{"rhs", safe_function<level_rhs>},
@ -146,40 +148,6 @@ void open_kernel_module(lua_State * L) {
#if 0
namespace lean {
static int level_name(lua_State * L) {
if (!is_uvar(to_level(L, 1)))
throw exception("arg #1 must be a Lean level universal variable");
return push_name(L, uvar_name(to_level(L, 1)));
}
static int level_lift_of(lua_State * L) {
if (!is_lift(to_level(L, 1)))
throw exception("arg #1 must be a Lean level lift");
return push_level(L, lift_of(to_level(L, 1)));
}
static int level_lift_offset(lua_State * L) {
if (!is_lift(to_level(L, 1)))
throw exception("arg #1 must be a Lean level lift");
lua_pushinteger(L, lift_offset(to_level(L, 1)));
return 1;
}
static int level_max_size(lua_State * L) {
if (!is_max(to_level(L, 1)))
throw exception("arg #1 must be a Lean level max");
lua_pushinteger(L, max_size(to_level(L, 1)));
return 1;
}
static int level_max_level(lua_State * L) {
if (!is_max(to_level(L, 1)))
throw exception("arg #1 must be a Lean level max");
return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2)));
}
DECL_UDATA(expr)
int push_optional_expr(lua_State * L, optional<expr> const & e) {

3
tests/lua/level1.lua
View file

@ -30,4 +30,5 @@ local l = mk_level_max(mk_param_univ("a"), mk_param_univ("b"))
assert(l:instantiate({"a"}, {mk_level_one()}) == mk_level_max(mk_level_one(), mk_param_univ("b")))
assert(l:instantiate({"a", "b"}, {mk_level_one(), mk_param_univ("c")}) == mk_level_max(mk_level_one(), mk_param_univ("c")))
assert(not pcall(function() l:instantiate({"a", "b", "C"}, {mk_level_one(), mk_param_univ("c")}) end))
assert(l:is_eqp(l))
assert(not l:is_eqp(level()))