From 6536232107c288a8498cff1523abffdcbd892f46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 May 2014 06:05:31 -0700 Subject: [PATCH] feat(library/coercion): expose coercion module in the Lua API Signed-off-by: Leonardo de Moura --- src/library/coercion.cpp | 56 +++++++++++++++++++++++++++++++++ src/library/coercion.h | 3 ++ src/library/kernel_bindings.cpp | 24 ++++++++------ src/library/kernel_bindings.h | 3 +- src/library/register_module.h | 4 +-- 5 files changed, 77 insertions(+), 13 deletions(-) diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index f6c1f90de..90f5c2d23 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/coercion.h" #include "library/module.h" #include "library/kernel_serializer.h" +#include "library/kernel_bindings.h" namespace lean { enum class coercion_class_kind { User, Sort, Fun }; @@ -408,4 +409,59 @@ bool get_user_coercions(environment const & env, expr const & C, buffer> r; + get_user_coercions(to_environment(L, 1), to_expr(L, 2), r); + lua_newtable(L); + int i = 1; + for (auto p : r) { + lua_newtable(L); + push_expr(L, p.first); + lua_rawseti(L, -2, 1); + push_name(L, p.second); + lua_rawseti(L, -2, 2); + lua_rawseti(L, -2, i); + i = i + 1; + } + return 1; +} + +void open_coercion(lua_State * L) { + SET_GLOBAL_FUN(add_coercion, "add_coercion"); + SET_GLOBAL_FUN(is_coercion, "is_coercion"); + SET_GLOBAL_FUN(has_coercions_from, "has_coercions_from"); + SET_GLOBAL_FUN(has_coercions_to, "has_coercions_to"); + SET_GLOBAL_FUN(get_coercion, "get_coercion"); + SET_GLOBAL_FUN(get_coercion_to_sort, "get_coercion_to_sort"); + SET_GLOBAL_FUN(get_coercion_to_fun, "get_coercion_to_fun"); + SET_GLOBAL_FUN(get_user_coercions, "get_user_coercions"); +} } diff --git a/src/library/coercion.h b/src/library/coercion.h index 462baffcc..4bb90d821 100644 --- a/src/library/coercion.h +++ b/src/library/coercion.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/lua.h" #include "kernel/environment.h" #include "library/expr_pair.h" #include "library/io_state.h" @@ -60,4 +61,6 @@ optional get_coercion_to_fun(environment const & env, expr const & C); \remark The most recent coercions occur first. */ bool get_user_coercions(environment const & env, expr const & C, buffer> & result); + +void open_coercion(lua_State * L); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 3ec2eb04a..9a9a26fb7 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -42,8 +42,14 @@ Author: Leonardo de Moura namespace lean { static environment get_global_environment(lua_State * L); -io_state * get_io_state(lua_State * L); +io_state * get_io_state_ptr(lua_State * L); io_state get_tmp_io_state(lua_State * L); +io_state get_io_state(lua_State * L) { + if (io_state * ios = get_io_state_ptr(L)) + return *ios; + else + return get_tmp_io_state(L); +} // Level DECL_UDATA(level) @@ -983,7 +989,7 @@ static char g_formatter_key; static formatter g_simple_formatter = mk_simple_formatter(); optional get_global_formatter_core(lua_State * L) { - io_state * io = get_io_state(L); + io_state * io = get_io_state_ptr(L); if (io != nullptr) { return optional(io->get_formatter()); } else { @@ -1009,7 +1015,7 @@ formatter get_global_formatter(lua_State * L) { } void set_global_formatter(lua_State * L, formatter const & fmt) { - io_state * io = get_io_state(L); + io_state * io = get_io_state_ptr(L); if (io != nullptr) { io->set_formatter(fmt); } else { @@ -1020,7 +1026,7 @@ void set_global_formatter(lua_State * L, formatter const & fmt) { } static int get_formatter(lua_State * L) { - io_state * io = get_io_state(L); + io_state * io = get_io_state_ptr(L); if (io != nullptr) { return push_formatter(L, io->get_formatter()); } else { @@ -1168,10 +1174,8 @@ static int import_modules(environment const & env, lua_State * L, int s) { if (nargs > s + 1 && is_io_state(L, s+2)) return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, to_io_state(L, s+2))); - else if (io_state * ios = get_io_state(L)) - return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, *ios)); else - return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, get_tmp_io_state(L))); + return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, get_io_state(L))); } static int import_modules(lua_State * L) { @@ -1304,7 +1308,7 @@ static void print(io_state * ios, bool reg, char const * msg) { /** \brief Thread safe version of print function */ static int print(lua_State * L, int start, bool reg) { lock_guard lock(g_print_mutex); - io_state * ios = get_io_state(L); + io_state * ios = get_io_state_ptr(L); int n = lua_gettop(L); int i; lua_getglobal(L, "tostring"); @@ -1370,7 +1374,7 @@ void set_global_io_state(lua_State * L, io_state & ios) { set_io_state::set_io_state(lua_State * L, io_state & st) { m_state = L; - m_prev = get_io_state(L); + m_prev = get_io_state_ptr(L); lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); lua_pushlightuserdata(m_state, &st); lua_settable(m_state, LUA_REGISTRYINDEX); @@ -1389,7 +1393,7 @@ set_io_state::~set_io_state() { set_global_options(m_state, m_prev->get_options()); } -io_state * get_io_state(lua_State * L) { +io_state * get_io_state_ptr(lua_State * L) { lua_pushlightuserdata(L, static_cast(&g_set_state_key)); lua_gettable(L, LUA_REGISTRYINDEX); if (lua_islightuserdata(L, -1)) { diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index bafd0a430..568367092 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -74,6 +74,7 @@ public: \brief Return the Lean state object associated with the given Lua state. Return nullptr is there is none. */ -io_state * get_io_state(lua_State * L); +io_state * get_io_state_ptr(lua_State * L); +io_state get_io_state(lua_State * L); void open_io_state(lua_State * L); } diff --git a/src/library/register_module.h b/src/library/register_module.h index 9f34d7230..9d407ec54 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "library/kernel_bindings.h" #include "library/resolve_macro.h" -// #include "library/substitution.h" +#include "library/coercion.h" // #include "library/fo_unify.h" // #include "library/hop_match.h" // #include "library/placeholder.h" @@ -17,7 +17,7 @@ namespace lean { inline void open_core_module(lua_State * L) { open_kernel_module(L); open_resolve_macro(L); - // open_substitution(L); + open_coercion(L); // open_fo_unify(L); // open_placeholder(L); // open_hop_match(L);