From 5bb2a41c64bf57bcb4863fbed58425c24652cbdf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Jan 2015 10:37:15 -0800 Subject: [PATCH] feat(library/reducible): expose Lua API for reducible hints --- src/library/reducible.cpp | 71 +++++++++++++++++++++++++++++++++++ src/library/reducible.h | 1 + src/library/register_module.h | 2 + tests/lean/run/reducible.lean | 64 +++++++++++++++++++++++++++++++ 4 files changed, 138 insertions(+) create mode 100644 tests/lean/run/reducible.lean diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 3e568ea8c..ed0fafa4c 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/scoped_ext.h" #include "library/reducible.h" +#include "library/kernel_bindings.h" namespace lean { struct reducible_entry { @@ -144,4 +145,74 @@ std::unique_ptr mk_opaque_type_checker(environment const & env, na return std::unique_ptr(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque, memoize, pred))); } + +static int mk_opaque_type_checker(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + type_checker_ref r(mk_opaque_type_checker(get_global_environment(L), name_generator())); + return push_type_checker_ref(L, r); + } else if (nargs == 1) { + type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), name_generator())); + return push_type_checker_ref(L, r); + } else { + type_checker_ref r(mk_opaque_type_checker(to_environment(L, 1), to_name_generator(L, 2))); + return push_type_checker_ref(L, r); + } +} + +static int mk_reducible_checker_core(lua_State * L, reducible_behavior rb) { + int nargs = lua_gettop(L); + if (nargs == 0) { + type_checker_ref r(mk_type_checker(get_global_environment(L), name_generator(), false, rb)); + return push_type_checker_ref(L, r); + } else if (nargs == 1) { + type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), false, rb)); + return push_type_checker_ref(L, r); + } else { + type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), false, rb)); + return push_type_checker_ref(L, r); + } +} + +static int mk_reducible_type_checker(lua_State * L) { + return mk_reducible_checker_core(L, OpaqueIfNotReducibleOn); +} + +static int mk_non_irreducible_type_checker(lua_State * L) { + return mk_reducible_checker_core(L, OpaqueIfReducibleOff); +} + +static int is_reducible_on(lua_State * L) { + return push_boolean(L, is_reducible_on(to_environment(L, 1), to_name_ext(L, 2))); +} + +static int is_reducible_off(lua_State * L) { + return push_boolean(L, is_reducible_off(to_environment(L, 1), to_name_ext(L, 2))); +} + +static int set_reducible(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 3) { + return push_environment(L, set_reducible(to_environment(L, 1), to_name_ext(L, 2), + static_cast(lua_tonumber(L, 3)))); + } else { + return push_environment(L, set_reducible(to_environment(L, 1), to_name_ext(L, 2), + static_cast(lua_tonumber(L, 3)), + lua_toboolean(L, 4))); + } +} + +void open_reducible(lua_State * L) { + lua_newtable(L); + SET_ENUM("On", reducible_status::On); + SET_ENUM("Off", reducible_status::Off); + SET_ENUM("None", reducible_status::None); + lua_setglobal(L, "reducible_status"); + SET_GLOBAL_FUN(is_reducible_on, "is_reducible_on"); + SET_GLOBAL_FUN(is_reducible_off, "is_reducible_off"); + SET_GLOBAL_FUN(set_reducible, "set_reducible"); + SET_GLOBAL_FUN(mk_opaque_type_checker, "opaque_type_checker"); + SET_GLOBAL_FUN(mk_non_irreducible_type_checker, "non_irreducible_type_checker"); + SET_GLOBAL_FUN(mk_reducible_type_checker, "reducible_type_checker"); +} } diff --git a/src/library/reducible.h b/src/library/reducible.h index f1c537dc6..c5ead2f8c 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -47,4 +47,5 @@ std::unique_ptr mk_opaque_type_checker(environment const & env, na void initialize_reducible(); void finalize_reducible(); +void open_reducible(lua_State * L); } diff --git a/src/library/register_module.h b/src/library/register_module.h index 62efd1eec..8a0c7eb86 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/scoped_ext.h" #include "library/match.h" +#include "library/reducible.h" namespace lean { inline void open_core_module(lua_State * L) { @@ -31,6 +32,7 @@ inline void open_core_module(lua_State * L) { open_unifier(L); open_explicit(L); open_match(L); + open_reducible(L); } inline void register_core_module() { script_state::register_module(open_core_module); diff --git a/tests/lean/run/reducible.lean b/tests/lean/run/reducible.lean new file mode 100644 index 000000000..01b0d2e91 --- /dev/null +++ b/tests/lean/run/reducible.lean @@ -0,0 +1,64 @@ +definition x [reducible] := 10 +definition y := 20 +definition z [irreducible] := 30 +opaque definition w := 40 + +(* + local env = get_env() + local x = Const("x") + local y = Const("y") + local z = Const("z") + local w = Const("w") + local val_x = env:find("x"):value() + local val_y = env:find("y"):value() + local val_z = env:find("z"):value() + local val_w = env:find("w"):value() + -- All definitions are not unfolded + local tc = opaque_type_checker(env) + assert(tc:whnf(x) == x) + assert(tc:whnf(y) == y) + assert(tc:whnf(z) == z) + assert(tc:whnf(w) == w) + -- Opaque and definitions marked as irreducibled are not unfolded + local tc = non_irreducible_type_checker(env) + assert(tc:whnf(x) == val_x) + assert(tc:whnf(y) == val_y) + assert(tc:whnf(z) == z) + assert(tc:whnf(w) == w) + -- Only definitions marked as reducible are unfolded + local tc = reducible_type_checker(env) + assert(tc:whnf(x) == val_x) + assert(tc:whnf(y) == y) + assert(tc:whnf(z) == z) + assert(tc:whnf(w) == w) + -- Default: only opaque definitions are not unfolded. + -- Opaqueness is a feature of the kernel. + local tc = type_checker(env) + assert(tc:whnf(x) == val_x) + assert(tc:whnf(y) == val_y) + assert(tc:whnf(z) == val_z) + assert(tc:whnf(w) == w) +*) + +(* + local env = get_env() + assert(is_reducible_on(env, "x")) + assert(not is_reducible_on(env, "y")) + assert(not is_reducible_on(env, "z")) + assert(not is_reducible_off(env, "x")) + assert(not is_reducible_off(env, "y")) + assert(is_reducible_off(env, "z")) + env = set_reducible(env, "x", reducible_status.Off) + assert(not is_reducible_on(env, "x")) + assert(is_reducible_off(env, "x")) + env = set_reducible(env, "x", reducible_status.None) + assert(not is_reducible_on(env, "x")) + assert(not is_reducible_off(env, "x")) + env = set_reducible(env, "x", reducible_status.On) + assert(is_reducible_on(env, "x")) + assert(not is_reducible_off(env, "x")) + env = set_reducible(env, "x", reducible_status.Off) + set_env(env) +*) + +eval [whnf] x