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

feat(library/kernel_bindings): expose abst_name, abst_domain and abst_body in the Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-16 00:03:16 -08:00
parent 8d73fb5699
commit d063828ff9
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/library/kernel_bindings.cpp
View file

@ -613,6 +613,26 @@ static int expr_beta_reduce(lua_State * L) {
return push_expr(L, beta_reduce(to_expr(L, 1)));
}
static void check_abstraction(lua_State * L, int idx, char const * msg) {
if (!is_abstraction(to_expr(L, idx)))
throw exception(msg);
}
static int expr_abst_name(lua_State * L) {
check_abstraction(L, 1, "invalid abst_name call, expression is not an abstraction");
return push_name(L, abst_name(to_expr(L, 1)));
}
static int expr_abst_domain(lua_State * L) {
check_abstraction(L, 1, "invalid abst_domain call, expression is not an abstraction");
return push_expr(L, abst_domain(to_expr(L, 1)));
}
static int expr_abst_body(lua_State * L) {
check_abstraction(L, 1, "invalid abst_body call, expression is not an abstraction");
return push_expr(L, abst_body(to_expr(L, 1)));
}
static const struct luaL_Reg expr_m[] = {
{"__gc", expr_gc}, // never throws
{"__tostring", safe_function<expr_tostring>},
@ -635,6 +655,9 @@ static const struct luaL_Reg expr_m[] = {
{"args", safe_function<expr_args>},
{"num_args", safe_function<expr_num_args>},
{"arg", safe_function<expr_arg>},
{"abst_name", safe_function<expr_abst_name>},
{"abst_domain", safe_function<expr_abst_domain>},
{"abst_body", safe_function<expr_abst_body>},
{"for_each", safe_function<expr_for_each>},
{"has_free_vars", safe_function<expr_has_free_vars>},
{"closed", safe_function<expr_closed>},