diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index dd166d850..cead933c7 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/script_state.h" #include "util/list_lua.h" +#include "util/pair_lua.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" #include "kernel/free_vars.h" @@ -154,6 +155,10 @@ static void open_level(lua_State * L) { lua_setglobal(L, "level_kind"); } +DEFINE_LUA_HOMO_PAIR(level, push_level, to_level) +typedef std::pair pair_level; +DEFINE_LUA_LIST(pair_level, push_pair_level, to_pair_level_ext) + // Expr_binder_info DECL_UDATA(expr_binder_info) static int mk_binder_info(lua_State * L) { @@ -275,7 +280,7 @@ typedef expr (*MkAbst1)(expr const & n, expr const & t, expr const & b); typedef expr (*MkAbst2)(name const & n, expr const & t, expr const & b); template -int expr_abst(lua_State * L) { +static int expr_abst(lua_State * L) { int nargs = lua_gettop(L); if (nargs < 2) throw exception("function must have at least 2 arguments"); @@ -557,11 +562,10 @@ static void open_expr(lua_State * L) { } // macro_definition DECL_UDATA(macro_definition) - -int macro_get_name(lua_State * L) { return push_name(L, to_macro_definition(L, 1).get_name()); } -int macro_trust_level(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).trust_level()); } -int macro_eq(lua_State * L) { return push_boolean(L, to_macro_definition(L, 1) == to_macro_definition(L, 2)); } -int macro_hash(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).hash()); } +static int macro_get_name(lua_State * L) { return push_name(L, to_macro_definition(L, 1).get_name()); } +static int macro_trust_level(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).trust_level()); } +static int macro_eq(lua_State * L) { return push_boolean(L, to_macro_definition(L, 1) == to_macro_definition(L, 2)); } +static int macro_hash(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).hash()); } static int macro_tostring(lua_State * L) { std::ostringstream out; formatter fmt = get_global_formatter(L); @@ -580,7 +584,7 @@ static const struct luaL_Reg macro_definition_m[] = { {0, 0} }; -void open_macro_definition(lua_State * L) { +static void open_macro_definition(lua_State * L) { luaL_newmetatable(L, macro_definition_mt); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); @@ -589,6 +593,130 @@ void open_macro_definition(lua_State * L) { SET_GLOBAL_FUN(macro_definition_pred, "is_macro_definition"); } +// definition +DECL_UDATA(definition) +int push_optional_definition(lua_State * L, optional const & e) { return e ? push_definition(L, *e) : push_nil(L); } +#define DEFINITION_PRED(P) static int definition_ ## P(lua_State * L) { return push_boolean(L, to_definition(L, 1).P()); } +DEFINITION_PRED(is_definition) +DEFINITION_PRED(is_theorem) +DEFINITION_PRED(is_axiom) +DEFINITION_PRED(is_var_decl) +DEFINITION_PRED(is_opaque) +DEFINITION_PRED(use_conv_opt) +static int definition_get_name(lua_State * L) { return push_name(L, to_definition(L, 1).get_name()); } +static int definition_get_params(lua_State * L) { return push_list_name(L, to_definition(L, 1).get_params()); } +static int definition_get_level_cnstrs(lua_State * L) { return push_list_pair_level(L, to_definition(L, 1).get_level_cnstrs()); } +static int definition_get_type(lua_State * L) { return push_expr(L, to_definition(L, 1).get_type()); } +static int definition_get_value(lua_State * L) { + if (to_definition(L, 1).is_definition()) + return push_expr(L, to_definition(L, 1).get_value()); + throw exception("arg #1 must be a definition"); +} +static int definition_get_weight(lua_State * L) { return push_integer(L, to_definition(L, 1).get_weight()); } +static int definition_get_module_idx(lua_State * L) { return push_integer(L, to_definition(L, 1).get_module_idx()); } +static int mk_var_decl(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_definition(L, mk_var_decl(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2))); + else + return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4))); +} +static int mk_axiom(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_definition(L, mk_axiom(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2))); + else + return push_definition(L, mk_axiom(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4))); +} +static int mk_theorem(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 3) + return push_definition(L, mk_theorem(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2), to_expr(L, 3))); + else + return push_definition(L, mk_theorem(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4), to_expr(L, 5))); +} +static void get_definition_args(lua_State * L, int idx, bool & opaque, int & weight, module_idx & mod_idx, bool & use_conv_opt) { + if (lua_istable(L, idx)) { + push_string(L, "opaque"); + lua_gettable(L, idx); + if (lua_isboolean(L, -1)) + opaque = lua_toboolean(L, -1); + lua_pop(L, 1); + + push_string(L, "use_conv_opt"); + lua_gettable(L, idx); + if (lua_isboolean(L, -1)) + use_conv_opt = lua_toboolean(L, -1); + lua_pop(L, 1); + + push_string(L, "module_idx"); + lua_gettable(L, idx); + if (lua_isnumber(L, -1)) + mod_idx = lua_tointeger(L, -1); + lua_pop(L, 1); + + push_string(L, "weight"); + lua_gettable(L, idx); + if (lua_isnumber(L, -1)) + weight = lua_tointeger(L, -1); + lua_pop(L, 1); + } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { + throw exception(sstream() << "arg #" << idx << " must be a table"); + } +} +static int mk_definition(lua_State * L) { + int nargs = lua_gettop(L); + bool opaque = true; int weight = 0; module_idx mod_idx = 0; bool use_conv_opt = true; + if (is_environment(L, 1)) { + if (nargs <= 5) { + get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt); + return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(), level_cnstrs(), to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt)); + } else { + get_definition_args(L, 7, opaque, weight, mod_idx, use_conv_opt); + return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_list_name_ext(L, 3), to_list_pair_level_ext(L, 4), to_expr(L, 5), to_expr(L, 6), opaque, mod_idx, use_conv_opt)); + } + } else { + if (nargs <= 4) { + get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt); + return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2), to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt)); + } else { + get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt); + return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4), to_expr(L, 5), opaque, weight, mod_idx, use_conv_opt)); + } + } +} + +static const struct luaL_Reg definition_m[] = { + {"__gc", definition_gc}, // never throws + {"is_definition", safe_function}, + {"is_theorem", safe_function}, + {"is_axiom", safe_function}, + {"is_var_decl", safe_function}, + {"opaque", safe_function}, + {"use_conv_opt", safe_function}, + {"name", safe_function}, + {"univ_params", safe_function}, + {"univ_cnstrs", safe_function}, + {"type", safe_function}, + {"value", safe_function}, + {"weight", safe_function}, + {"module_idx", safe_function}, + {0, 0} +}; + +static void open_definition(lua_State * L) { + luaL_newmetatable(L, definition_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, definition_m, 0); + + SET_GLOBAL_FUN(definition_pred, "is_definition"); + SET_GLOBAL_FUN(mk_var_decl, "mk_var_decl"); + SET_GLOBAL_FUN(mk_axiom, "mk_axiom"); + SET_GLOBAL_FUN(mk_theorem, "mk_theorem"); + SET_GLOBAL_FUN(mk_definition, "mk_definition"); +} + // Formatter DECL_UDATA(formatter) @@ -753,9 +881,9 @@ int mk_io_state(lua_State * L) { return push_io_state(L, io_state(to_options(L, 1), to_formatter(L, 2))); } -int io_state_get_options(lua_State * L) { return push_options(L, to_io_state(L, 1).get_options()); } -int io_state_get_formatter(lua_State * L) { return push_formatter(L, to_io_state(L, 1).get_formatter()); } -int io_state_set_options(lua_State * L) { to_io_state(L, 1).set_options(to_options(L, 2)); return 0; } +static int io_state_get_options(lua_State * L) { return push_options(L, to_io_state(L, 1).get_options()); } +static int io_state_get_formatter(lua_State * L) { return push_formatter(L, to_io_state(L, 1).get_formatter()); } +static int io_state_set_options(lua_State * L) { to_io_state(L, 1).set_options(to_options(L, 2)); return 0; } static mutex g_print_mutex; @@ -801,17 +929,9 @@ static int print(lua_State * L, io_state & ios, int start, bool reg) { return print(L, start, reg); } -static int print(lua_State * L) { - return print(L, 1, true); -} - -int io_state_print_regular(lua_State * L) { - return print(L, to_io_state(L, 1), 2, true); -} - -int io_state_print_diagnostic(lua_State * L) { - return print(L, to_io_state(L, 1), 2, false); -} +static int print(lua_State * L) { return print(L, 1, true); } +static int io_state_print_regular(lua_State * L) { return print(L, to_io_state(L, 1), 2, true); } +static int io_state_print_diagnostic(lua_State * L) { return print(L, to_io_state(L, 1), 2, false); } static const struct luaL_Reg io_state_m[] = { {"__gc", io_state_gc}, // never throws @@ -1205,13 +1325,15 @@ static void open_substitution(lua_State * L) { } void open_kernel_module(lua_State * L) { - // TODO(Leo) open_level(L); open_list_level(L); + open_pair_level(L); + open_list_pair_level(L); open_binder_info(L); open_expr(L); open_list_expr(L); open_macro_definition(L); + open_definition(L); open_formatter(L); open_environment(L); open_io_state(L); diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index 90b820c0b..bafd0a430 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -23,7 +23,7 @@ UDATA_DEFS(substitution) UDATA_DEFS(io_state) int push_optional_expr(lua_State * L, optional const & e); int push_optional_justification(lua_State * L, optional const & j); -int push_optional_definition(lua_State * L, optional const & o); +int push_optional_definition(lua_State * L, optional const & d); /** \brief Return the formatter object associated with the given Lua State. This procedure checks for options at: