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

feat(library/kernel_bindings): improve Fun/Pi Lua APIs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-20 09:00:19 -07:00
parent eb6807e1d3
commit 4103c85ce3
1 changed files with 18 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/kernel_bindings.cpp
View file

@ -430,8 +430,12 @@ static int expr_abst(lua_State * L) {
if (nargs < 2) if (nargs < 2)
throw exception("function must have at least 2 arguments"); throw exception("function must have at least 2 arguments");
if (nargs == 2) { if (nargs == 2) {
if (!lua_istable(L, 1)) if (is_expr(L, 1) && is_local(to_expr(L, 1))) {
throw exception("function expects arg #1 to be of the form '{{expr, expr}, ...}'"); if (pi)
return push_expr(L, Pi(to_expr(L, 1), to_expr(L, 2)));
else
return push_expr(L, Fun(to_expr(L, 1), to_expr(L, 2)));
} else if (lua_istable(L, 1)) {
int len = objlen(L, 1); int len = objlen(L, 1);
if (len == 0) if (len == 0)
throw exception("function expects arg #1 to be a non-empty table"); throw exception("function expects arg #1 to be a non-empty table");
@ -444,6 +448,9 @@ static int expr_abst(lua_State * L) {
r = Fun(std::get<0>(p), std::get<1>(p), r, std::get<2>(p)); r = Fun(std::get<0>(p), std::get<1>(p), r, std::get<2>(p));
} }
return push_expr(L, r); return push_expr(L, r);
} else {
throw exception("function expects arg #1 to be a local constant or a table of the form '{{expr, expr}, ...}'");
}
} else { } else {
if (nargs % 2 == 0) if (nargs % 2 == 0)
throw exception("function must have an odd number of arguments"); throw exception("function must have an odd number of arguments");