From 5fc0f06a8dd66fd440902909c93fdc1c2c0c8391 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 May 2014 18:08:50 -0700 Subject: [PATCH] feat(library/kernel_bindings): add Lua API for declaring datatypes Signed-off-by: Leonardo de Moura --- src/kernel/inductive/inductive.cpp | 11 ++- src/library/kernel_bindings.cpp | 110 ++++++++++++++++++++++++++++- 2 files changed, 115 insertions(+), 6 deletions(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 2a63cdb9b..e78a7c4f2 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -21,9 +21,14 @@ environment add_inductive(environment const & env, optional const & univ_offset) { // TODO(Leo) std::cout << "add_inductive\n"; - for (auto l : level_params) { std::cout << l << " "; } std::cout << "\n"; - for (auto e : params) { std::cout << e.get_name() << " "; } std::cout << "\n"; - for (auto d : decls) { std::cout << std::get<0>(d) << " "; } std::cout << "\n"; + if (!is_nil(level_params)) { for (auto l : level_params) { std::cout << l << " "; } std::cout << "\n"; } + if (!is_nil(params)) { for (auto e : params) { std::cout << e.get_name() << " "; } std::cout << "\n"; } + for (auto d : decls) { + std::cout << inductive_decl_name(d) << "\n"; + for (auto ir : inductive_decl_intros(d)) { + std::cout << " " << intro_rule_name(ir) << " #" << length(intro_rule_args(ir)) << " " << intro_rule_type(ir) << "\n"; + } + } if (univ_offset) std::cout << "offset: " << *univ_offset << "\n"; return env; } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index a5d3566ca..8e33e3fc0 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -301,7 +301,10 @@ static expr get_expr_from_table(lua_State * L, int t, int i) { } static void throw_invalid_binder_table(int t) { - throw exception(sstream() << "arg #" << t << " must be a table {e_1, ..., e_k} where each entry e_i is of the form: {expr, expr}, {expr, expr, bool}, or {expr, expr, binder_info}, each entry represents a binder, the first expression in each entry must be a (local) constant, the second expression is the type, the optional Boolean can be used to mark implicit arguments."); + if (t > 0) + throw exception(sstream() << "arg #" << t << " must be a table {e_1, ..., e_k} where each entry e_i is of the form: {expr, expr}, {expr, expr, bool}, or {expr, expr, binder_info}, each entry represents a binder, the first expression in each entry must be a (local) constant, the second expression is the type, the optional Boolean can be used to mark implicit arguments."); + else + throw exception(sstream() << "invalid binder, it must of the form: {expr, expr}, {expr, expr, bool}, or {expr, expr, binder_info}, each entry represents a binder, the first expression in each entry must be a (local) constant, the second expression is the type, the optional Boolean can be used to mark implicit arguments."); } // t is a table of tuples {{a1, b1}, ..., {ak, bk}} @@ -1669,18 +1672,118 @@ static void open_type_checker(lua_State * L) { SET_GLOBAL_FUN(add_declaration, "add_decl"); } -telescope to_telescope(lua_State * L, int idx) { +template +static std::pair to_telescope(lua_State * L, int idx, T const & v, F const & v_abst) { luaL_checktype(L, idx, LUA_TTABLE); lua_pushvalue(L, idx); // push table on the top int sz = objlen(L, -1); // get table size telescope r; + T new_v = v; for (int i = sz; i >= 1; i--) { - // TODO(Leo) + auto const & t = get_binder_from_table(L, -1, i); + expr const & a = std::get<0>(t); + expr const & a_ty = std::get<1>(t); + binder_info const & bi = std::get<2>(t); + r = telescope(binder(const_name(a), a_ty, bi), abstract(r, a)); + new_v = v_abst(new_v, a, sz-i); } lua_pop(L, 1); // pop table from the top + return mk_pair(r, new_v); +} +static telescope to_telescope(lua_State * L, int idx) { + return to_telescope(L, idx, 0, [](int, expr const &, int) { return 0; }).first; +} + +namespace inductive { +static intro_rule to_intro_rule(lua_State * L, int idx) { + luaL_checktype(L, idx, LUA_TTABLE); + lua_pushvalue(L, idx); // push table on the top + if (objlen(L, idx) != 3) + throw exception("invalid introduction rule, it must have three arguments: name, telescope (arguments), type"); + lua_rawgeti(L, -1, 1); + lua_rawgeti(L, -2, 2); + lua_rawgeti(L, -3, 3); + name n = to_name_ext(L, -3); + expr ty = to_expr(L, -1); + auto args_ty = to_telescope(L, -2, ty, + [](expr const & v, expr const & a, unsigned i) -> expr { + return abstract(v, a, i); + }); + lua_pop(L, 4); + return intro_rule(n, args_ty.first, args_ty.second); +} + +static inductive_decl to_inductive_decl(lua_State * L, int idx) { + luaL_checktype(L, idx, LUA_TTABLE); + lua_pushvalue(L, idx); // push table on the top + int sz = objlen(L, idx); + if (sz < 2) + throw exception("invalid inductive decl, it must have at least two arguments: name, indices"); + list rs; + for (int i = sz; i >= 3; i--) { + lua_rawgeti(L, -1, i); + rs = list(to_intro_rule(L, -1), rs); + lua_pop(L, 1); + } + lua_rawgeti(L, -1, 2); + telescope const & indices = to_telescope(L, -1); + lua_pop(L, 1); + lua_rawgeti(L, -1, 1); + name const & n = to_name_ext(L, -1); + lua_pop(L, 2); + return inductive_decl(n, indices, rs); +} + +inductive_decl abstract(inductive_decl const & d, expr const & a, unsigned i = 0) { + telescope const & indices = inductive_decl_indices(d); + return inductive_decl(inductive_decl_name(d), abstract(indices, a, i), inductive_decl_intros(d)); +} + +list abstract(list const & ds, expr const & a, unsigned i = 0) { + return map(ds, [&](inductive_decl const & d) { return abstract(d, a, i); }); +} + +static list to_inductive_decls(lua_State * L, int idx) { + luaL_checktype(L, idx, LUA_TTABLE); + lua_pushvalue(L, idx); // push table on the top + int sz = objlen(L, idx); + list r; + for (int i = sz; i >= 1; i--) { + lua_rawgeti(L, -1, i); + r = list(to_inductive_decl(L, -1), r); + lua_pop(L, 1); + } + lua_pop(L, 1); return r; } +static int add_inductive(lua_State * L) { + int nargs = lua_gettop(L); + environment env = to_environment(L, 1); + level_param_names ls = to_level_param_names(L, 2); + list ds = to_inductive_decls(L, 4); + optional offset(0); + if (nargs == 5) { + if (lua_isnil(L, 5)) + offset = optional(); + else + offset = lua_tonumber(L, 5); + } + auto params_ds = + to_telescope>(L, 3, ds, + [](list const & ds, expr const & a, int i) { + return abstract(ds, a, i); + }); + ds = params_ds.second; + telescope const & ps = params_ds.first; + return push_environment(L, add_inductive(env, ls, ps, ds, offset)); +} +} + +static void open_inductive(lua_State * L) { + SET_GLOBAL_FUN(inductive::add_inductive, "add_inductive"); +} + void open_kernel_module(lua_State * L) { open_level(L); open_list_level(L); @@ -1700,5 +1803,6 @@ void open_kernel_module(lua_State * L) { open_substitution(L); open_constraint_handler(L); open_type_checker(L); + open_inductive(L); } }