From 9676f48470ae42433f2c484d5e43e047eabfbdf7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 May 2014 18:51:34 -0700 Subject: [PATCH] feat(library/kernel_bindings): add list of certified_definitions in the Lua API Signed-off-by: Leonardo de Moura --- src/library/kernel_bindings.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 30bfc9789..fb3799131 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -821,14 +821,21 @@ static const struct luaL_Reg certified_definition_m[] = { {0, 0} }; +static void certified_definition_migrate(lua_State * src, int i, lua_State * tgt) { + push_certified_definition(tgt, to_certified_definition(src, i)); +} + static void open_certified_definition(lua_State * L) { luaL_newmetatable(L, certified_definition_mt); + set_migrate_fn_field(L, -1, certified_definition_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, certified_definition_m, 0); SET_GLOBAL_FUN(certified_definition_pred, "is_certified_definition"); } +static bool operator!=(certified_definition const &, certified_definition const &) { return true; } +DEFINE_LUA_LIST(certified_definition, push_certified_definition, to_certified_definition) // Environment DECL_UDATA(environment) @@ -1529,6 +1536,7 @@ void open_kernel_module(lua_State * L) { open_formatter(L); open_environment_id(L); open_certified_definition(L); + open_list_certified_definition(L); open_environment(L); open_io_state(L); open_justification(L);