From 6f8f074f207c74b5c3ed01fe91e70c689fdc0b45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 May 2014 09:37:50 -0700 Subject: [PATCH] feat(library/kernel_bindings): make mk_arrow nary in the Lua API Signed-off-by: Leonardo de Moura --- src/library/kernel_bindings.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index fb4856c9d..a468d3da4 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -279,7 +279,15 @@ static int expr_mk_pi(lua_State * L) { else return push_expr(L, mk_pi(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr_binder_info(L, 4))); } -static int expr_mk_arrow(lua_State * L) { return push_expr(L, mk_arrow(to_expr(L, 1), to_expr(L, 2))); } +static int expr_mk_arrow(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs < 2) + throw exception("function must have at least 2 arguments"); + expr r = mk_arrow(to_expr(L, nargs - 1), to_expr(L, nargs)); + for (int i = nargs - 2; i >= 1; i--) + r = mk_arrow(to_expr(L, i), r); + return push_expr(L, r); +} static int expr_mk_let(lua_State * L) { return push_expr(L, mk_let(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr(L, 4))); } static expr get_expr_from_table(lua_State * L, int t, int i) {