diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a79911634..0295e53d4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -162,7 +162,7 @@ set(LEAN_LIBS ${LEAN_LIBS} tactic) add_subdirectory(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) add_subdirectory(bindings/lua) -set(LEAN_LIBS ${LEAN_LIBS} lua) +set(LEAN_LIBS ${LEAN_LIBS} leanlua) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index 0ca02d379..d718e57f6 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -1,8 +1,3 @@ -add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp -lref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp -local_context.cpp expr.cpp context.cpp object.cpp environment.cpp -formatter.cpp justification.cpp metavar_env.cpp type_inferer.cpp -io_state.cpp goal.cpp proof_builder.cpp cex_builder.cpp -proof_state.cpp leanlua_state.cpp frontend_lean.cpp) +add_library(leanlua leanlua_state.cpp frontend_lean.cpp) -target_link_libraries(lua ${LEAN_LIBS}) +target_link_libraries(leanlua ${LEAN_LIBS}) diff --git a/src/bindings/lua/context.cpp b/src/bindings/lua/context.cpp deleted file mode 100644 index b05462090..000000000 --- a/src/bindings/lua/context.cpp +++ /dev/null @@ -1,119 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/sexpr/options.h" -#include "kernel/context.h" -#include "kernel/formatter.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/options.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/context.h" -#include "bindings/lua/formatter.h" - -namespace lean { -DECL_UDATA(context_entry) - -static int mk_context_entry(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 2) - return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2))); - else - return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); -} - -static int context_entry_get_name(lua_State * L) { return push_name(L, to_context_entry(L, 1).get_name()); } -static int context_entry_get_domain(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_domain()); } -static int context_entry_get_body(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_body()); } - -static const struct luaL_Reg context_entry_m[] = { - {"__gc", context_entry_gc}, // never throws - {"get_name", safe_function}, - {"get_domain", safe_function}, - {"get_body", safe_function}, - {0, 0} -}; - -DECL_UDATA(context) - -static int context_tostring(lua_State * L) { - std::ostringstream out; - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(fmt(to_context(L, 1), opts), opts); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int mk_context(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_context(L, context()); - } else if (nargs == 2) { - context_entry & e = to_context_entry(L, 2); - return push_context(L, context(to_context(L, 1), e.get_name(), e.get_domain(), e.get_body())); - } else if (nargs == 3) { - return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_nonnull_expr(L, 3))); - } else { - return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_nonnull_expr(L, 4))); - } -} - -static int context_extend(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs != 3 && nargs != 4) - throw exception("extend expect 3 or 4 arguments"); - return mk_context(L); -} - -static int context_is_empty(lua_State * L) { - lua_pushboolean(L, empty(to_context(L, 1))); - return 1; -} - -static int context_lookup(lua_State * L) { - auto p = lookup_ext(to_context(L, 1), luaL_checkinteger(L, 2)); - push_context_entry(L, p.first); - push_context(L, p.second); - return 2; -} - -static int context_size(lua_State * L) { - lua_pushinteger(L, to_context(L, 1).size()); - return 1; -} - -static const struct luaL_Reg context_m[] = { - {"__gc", context_gc}, // never throws - {"__tostring", safe_function}, - {"__len", safe_function}, - {"is_empty", safe_function}, - {"size", safe_function}, - {"extend", safe_function}, - {"lookup", safe_function}, - {0, 0} -}; - -void open_context(lua_State * L) { - luaL_newmetatable(L, context_entry_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, context_entry_m, 0); - SET_GLOBAL_FUN(mk_context_entry, "context_entry"); - SET_GLOBAL_FUN(context_entry_pred, "is_context_entry"); - - luaL_newmetatable(L, context_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, context_m, 0); - SET_GLOBAL_FUN(mk_context, "context"); - SET_GLOBAL_FUN(context_pred, "is_context"); - SET_GLOBAL_FUN(context_extend, "extend"); - SET_GLOBAL_FUN(context_lookup, "lookup"); -} -} diff --git a/src/bindings/lua/context.h b/src/bindings/lua/context.h deleted file mode 100644 index 6fd44aaa9..000000000 --- a/src/bindings/lua/context.h +++ /dev/null @@ -1,13 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(context_entry) -UDATA_DEFS(context) -void open_context(lua_State * L); -} diff --git a/src/bindings/lua/environment.cpp b/src/bindings/lua/environment.cpp deleted file mode 100644 index 8939a9a4b..000000000 --- a/src/bindings/lua/environment.cpp +++ /dev/null @@ -1,284 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "kernel/environment.h" -#include "kernel/formatter.h" -#include "library/type_inferer.h" -#include "frontends/lean/frontend.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/options.h" -#include "bindings/lua/level.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/object.h" -#include "bindings/lua/context.h" -#include "bindings/lua/environment.h" -#include "bindings/lua/formatter.h" - -namespace lean { -DECL_UDATA(environment) - -static environment get_global_environment(lua_State * L); - -ro_environment::ro_environment(lua_State * L, int idx): - read_only_environment(to_environment(L, idx)) { -} - -ro_environment::ro_environment(lua_State * L): - read_only_environment(get_global_environment(L)) { -} - -rw_environment::rw_environment(lua_State * L, int idx): - read_write_environment(to_environment(L, idx)) { -} - -rw_environment::rw_environment(lua_State * L): - read_write_environment(get_global_environment(L)) { -} - -static int mk_empty_environment(lua_State * L) { - return push_environment(L, environment()); -} - -static int mk_environment(lua_State * L) { - frontend f; - return push_environment(L, f.get_environment()); -} - -static int environment_mk_child(lua_State * L) { - rw_environment env(L, 1); - return push_environment(L, env->mk_child()); -} - -static int environment_has_parent(lua_State * L) { - ro_environment env(L, 1); - lua_pushboolean(L, env->has_parent()); - return 1; -} - -static int environment_has_children(lua_State * L) { - ro_environment env(L, 1); - lua_pushboolean(L, env->has_children()); - return 1; -} - -static int environment_parent(lua_State * L) { - ro_environment env(L, 1); - if (!env->has_parent()) - throw exception("environment does not have a parent environment"); - return push_environment(L, env->parent()); -} - -static int environment_add_uvar(lua_State * L) { - rw_environment env(L, 1); - int nargs = lua_gettop(L); - if (nargs == 2) - env->add_uvar(to_name_ext(L, 2)); - else - env->add_uvar(to_name_ext(L, 2), to_level(L, 3)); - return 0; -} - -static int environment_is_ge(lua_State * L) { - ro_environment env(L, 1); - lua_pushboolean(L, env->is_ge(to_level(L, 2), to_level(L, 3))); - return 1; -} - -static int environment_get_uvar(lua_State * L) { - ro_environment env(L, 1); - return push_level(L, env->get_uvar(to_name_ext(L, 2))); -} - -static int environment_add_definition(lua_State * L) { - rw_environment env(L, 1); - int nargs = lua_gettop(L); - if (nargs == 3) { - env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3)); - } else if (nargs == 4) { - if (is_expr(L, 4)) - env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)); - else - env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), lua_toboolean(L, 4)); - } else { - env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4), lua_toboolean(L, 5)); - } - return 0; -} - -static int environment_add_theorem(lua_State * L) { - rw_environment env(L, 1); - env->add_theorem(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)); - return 0; -} - -static int environment_add_var(lua_State * L) { - rw_environment env(L, 1); - env->add_var(to_name_ext(L, 2), to_nonnull_expr(L, 3)); - return 0; -} - -static int environment_add_axiom(lua_State * L) { - rw_environment env(L, 1); - env->add_axiom(to_name_ext(L, 2), to_nonnull_expr(L, 3)); - return 0; -} - -static int environment_find_object(lua_State * L) { - ro_environment env(L, 1); - return push_object(L, env->find_object(to_name_ext(L, 2))); -} - -static int environment_has_object(lua_State * L) { - ro_environment env(L, 1); - lua_pushboolean(L, env->has_object(to_name_ext(L, 2))); - return 1; -} - -static int environment_check_type(lua_State * L) { - ro_environment env(L, 1); - int nargs = lua_gettop(L); - if (nargs == 2) - return push_expr(L, env->infer_type(to_nonnull_expr(L, 2))); - else - return push_expr(L, env->infer_type(to_nonnull_expr(L, 2), to_context(L, 3))); -} - -static int environment_normalize(lua_State * L) { - ro_environment env(L, 1); - int nargs = lua_gettop(L); - if (nargs == 2) - return push_expr(L, env->normalize(to_nonnull_expr(L, 2))); - else - return push_expr(L, env->normalize(to_nonnull_expr(L, 2), to_context(L, 3))); -} - -/** - \brief Iterator (closure base function) for kernel objects. - - \see environment_objects - \see environment_local_objects. -*/ -static int environment_next_object(lua_State * L) { - ro_environment env(L, lua_upvalueindex(1)); - unsigned i = lua_tointeger(L, lua_upvalueindex(2)); - unsigned num = lua_tointeger(L, lua_upvalueindex(3)); - if (i >= num) { - lua_pushnil(L); - } else { - bool local = lua_toboolean(L, lua_upvalueindex(4)); - lua_pushinteger(L, i + 1); - lua_replace(L, lua_upvalueindex(2)); // update closure - push_object(L, env->get_object(i, local)); - } - return 1; -} - -static int environment_objects_core(lua_State * L, bool local) { - ro_environment env(L, 1); - push_environment(L, env); // upvalue(1): environment - lua_pushinteger(L, 0); // upvalue(2): index - lua_pushinteger(L, env->get_num_objects(local)); // upvalue(3): size - lua_pushboolean(L, local); // upvalue(4): local flag - lua_pushcclosure(L, &safe_function, 4); // create closure with 4 upvalues - return 1; -} - -static int environment_objects(lua_State * L) { - return environment_objects_core(L, false); -} - -static int environment_local_objects(lua_State * L) { - return environment_objects_core(L, true); -} - -static int environment_infer_type(lua_State * L) { - int nargs = lua_gettop(L); - type_inferer inferer(to_environment(L, 1)); - if (nargs == 2) - return push_expr(L, inferer(to_nonnull_expr(L, 2))); - else - return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3))); -} - -static int environment_tostring(lua_State * L) { - ro_environment env(L, 1); - std::ostringstream out; - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(fmt(env, opts), opts); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static const struct luaL_Reg environment_m[] = { - {"__gc", environment_gc}, // never throws - {"__tostring", safe_function}, - {"mk_child", safe_function}, - {"has_parent", safe_function}, - {"has_children", safe_function}, - {"parent", safe_function}, - {"add_uvar", safe_function}, - {"is_ge", safe_function}, - {"get_uvar", safe_function}, - {"add_definition", safe_function}, - {"add_theorem", safe_function}, - {"add_var", safe_function}, - {"add_axiom", safe_function}, - {"find_object", safe_function}, - {"has_object", safe_function}, - {"check_type", safe_function}, - {"infer_type", safe_function}, - {"normalize", safe_function}, - {"objects", safe_function}, - {"local_objects", safe_function}, - {0, 0} -}; - -static char g_set_environment_key; - -set_environment::set_environment(lua_State * L, environment & env) { - m_state = L; - lua_pushlightuserdata(m_state, static_cast(&g_set_environment_key)); - push_environment(m_state, env); - lua_settable(m_state, LUA_REGISTRYINDEX); -} - -set_environment::~set_environment() { - lua_pushlightuserdata(m_state, static_cast(&g_set_environment_key)); - lua_pushnil(m_state); - lua_settable(m_state, LUA_REGISTRYINDEX); -} - -static environment get_global_environment(lua_State * L) { - lua_pushlightuserdata(L, static_cast(&g_set_environment_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (!is_environment(L, -1)) - throw exception("Lua registry does not contain a Lean environment"); - environment r = to_environment(L, -1); - lua_pop(L, 1); - return r; -} - -int get_environment(lua_State * L) { - return push_environment(L, get_global_environment(L)); -} - -void open_environment(lua_State * L) { - luaL_newmetatable(L, environment_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, environment_m, 0); - - SET_GLOBAL_FUN(mk_empty_environment, "empty_environment"); - SET_GLOBAL_FUN(mk_environment, "environment"); - SET_GLOBAL_FUN(environment_pred, "is_environment"); - SET_GLOBAL_FUN(get_environment, "get_environment"); - SET_GLOBAL_FUN(get_environment, "get_env"); -} -} diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp deleted file mode 100644 index 543699d42..000000000 --- a/src/bindings/lua/expr.cpp +++ /dev/null @@ -1,480 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/debug.h" -#include "util/name.h" -#include "util/buffer.h" -#include "util/sexpr/options.h" -#include "util/sstream.h" -#include "kernel/expr.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/formatter.h" -#include "kernel/for_each_fn.h" -#include "kernel/free_vars.h" -#include "kernel/occurs.h" -#include "kernel/metavar.h" -#include "library/expr_lt.h" -#include "library/arith/nat.h" -#include "library/arith/int.h" -#include "library/arith/real.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/options.h" -#include "bindings/lua/level.h" -#include "bindings/lua/local_context.h" -#include "bindings/lua/formatter.h" -#include "bindings/lua/numerics.h" - -namespace lean { -DECL_UDATA(expr) - -expr & to_nonnull_expr(lua_State * L, int idx) { - expr & r = to_expr(L, idx); - if (!r) - throw exception("non-null Lean expression expected"); - return r; -} - -expr & to_app(lua_State * L, int idx) { - expr & r = to_nonnull_expr(L, idx); - if (!is_app(r)) - throw exception("Lean application expression expected"); - return r; -} - -static int expr_tostring(lua_State * L) { - std::ostringstream out; - expr & e = to_expr(L, 1); - if (e) { - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(fmt(to_expr(L, 1), opts), opts); - } else { - out << ""; - } - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int expr_eq(lua_State * L) { - lua_pushboolean(L, to_expr(L, 1) == to_expr(L, 2)); - return 1; -} - -static int expr_lt(lua_State * L) { - lua_pushboolean(L, to_expr(L, 1) < to_expr(L, 2)); - return 1; -} - -static int expr_mk_constant(lua_State * L) { - return push_expr(L, mk_constant(to_name_ext(L, 1))); -} - -static int expr_mk_var(lua_State * L) { - return push_expr(L, mk_var(luaL_checkinteger(L, 1))); -} - -static int expr_mk_app(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs < 2) - throw exception("application must have at least two arguments"); - buffer args; - for (int i = 1; i <= nargs; i++) - args.push_back(to_nonnull_expr(L, i)); - return push_expr(L, mk_app(args)); -} - -static int expr_mk_eq(lua_State * L) { - return push_expr(L, mk_eq(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2))); -} - -static int expr_mk_lambda(lua_State * L) { - return push_expr(L, mk_lambda(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); -} - -static int expr_mk_pi(lua_State * L) { - return push_expr(L, mk_pi(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); -} - -static int expr_mk_arrow(lua_State * L) { - return push_expr(L, mk_arrow(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2))); -} - -static int expr_mk_let(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 3) - return push_expr(L, mk_let(to_name_ext(L, 1), expr(), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); - else - return push_expr(L, mk_let(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4))); -} - -static expr get_expr_from_table(lua_State * L, int t, int i) { - lua_pushvalue(L, t); // push table to the top - lua_pushinteger(L, i); - lua_gettable(L, -2); - expr r = to_nonnull_expr(L, -1); - lua_pop(L, 2); // remove table and value - return r; -} - -// t is a table of pairs {{a1, b1}, ..., {ak, bk}} -// Each ai and bi is an expression -static std::pair get_expr_pair_from_table(lua_State * L, int t, int i) { - lua_pushvalue(L, t); // push table on the top - lua_pushinteger(L, i); - lua_gettable(L, -2); // now table {ai, bi} is on the top - if (!lua_istable(L, -1) || objlen(L, -1) != 2) - throw exception("arg #1 must be of the form '{{expr, expr}, ...}'"); - expr ai = get_expr_from_table(L, -1, 1); - expr bi = get_expr_from_table(L, -1, 2); - lua_pop(L, 2); // pop table {ai, bi} and t from stack - return mk_pair(ai, bi); -} - -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) { - int nargs = lua_gettop(L); - if (nargs < 2) - throw exception("function must have at least 2 arguments"); - if (nargs == 2) { - if (!lua_istable(L, 1)) - throw exception("function expects arg #1 to be of the form '{{expr, expr}, ...}'"); - int len = objlen(L, 1); - if (len == 0) - throw exception("function expects arg #1 to be a non-empty table"); - expr r = to_nonnull_expr(L, 2); - for (int i = len; i >= 1; i--) { - auto p = get_expr_pair_from_table(L, 1, i); - r = F1(p.first, p.second, r); - } - return push_expr(L, r); - } else { - if (nargs % 2 == 0) - throw exception("function must have an odd number of arguments"); - expr r = to_nonnull_expr(L, nargs); - for (int i = nargs - 1; i >= 1; i-=2) { - if (is_expr(L, i - 1)) - r = F1(to_nonnull_expr(L, i - 1), to_nonnull_expr(L, i), r); - else - r = F2(to_name_ext(L, i - 1), to_nonnull_expr(L, i), r); - } - return push_expr(L, r); - } -} - -static int expr_fun(lua_State * L) { return expr_abst(L); } -static int expr_pi(lua_State * L) { return expr_abst(L); } -static int expr_let(lua_State * L) { return expr_abst(L); } - -static int expr_type(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - return push_expr(L, Type()); - else - return push_expr(L, Type(to_level(L, 1))); -} - -static int expr_mk_metavar(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 1) - return push_expr(L, mk_metavar(to_name_ext(L, 1))); - else - return push_expr(L, mk_metavar(to_name_ext(L, 1), to_local_context(L, 2))); -} - -static int expr_is_null(lua_State * L) { - lua_pushboolean(L, !to_expr(L, 1)); - return 1; -} - -static int expr_get_kind(lua_State * L) { - lua_pushinteger(L, static_cast(to_nonnull_expr(L, 1).kind())); - return 1; -} - -#define EXPR_PRED(P) \ -static int expr_ ## P(lua_State * L) { \ - lua_pushboolean(L, P(to_nonnull_expr(L, 1))); \ - return 1; \ -} - -EXPR_PRED(is_constant) -EXPR_PRED(is_var) -EXPR_PRED(is_app) -EXPR_PRED(is_eq) -EXPR_PRED(is_lambda) -EXPR_PRED(is_pi) -EXPR_PRED(is_abstraction) -EXPR_PRED(is_let) -EXPR_PRED(is_value) -EXPR_PRED(is_metavar) -EXPR_PRED(has_free_vars) -EXPR_PRED(closed) -EXPR_PRED(has_metavar) - -/** - \brief Iterator (closure base function) for application args. See \c expr_args -*/ -static int expr_next_arg(lua_State * L) { - expr & e = to_expr(L, lua_upvalueindex(1)); - unsigned i = lua_tointeger(L, lua_upvalueindex(2)); - if (i >= num_args(e)) { - lua_pushnil(L); - } else { - lua_pushinteger(L, i + 1); - lua_replace(L, lua_upvalueindex(2)); // update closure - push_expr(L, arg(e, i)); - } - return 1; -} - -static int expr_args(lua_State * L) { - expr & e = to_app(L, 1); - push_expr(L, e); // upvalue(1): expr - lua_pushinteger(L, 0); // upvalue(2): index - lua_pushcclosure(L, &safe_function, 2); // create closure with 2 upvalues - return 1; -} - -static int expr_num_args(lua_State * L) { - lua_pushinteger(L, num_args(to_app(L, 1))); - return 1; -} - -static int expr_arg(lua_State * L) { - expr & e = to_app(L, 1); - int i = luaL_checkinteger(L, 2); - if (i >= static_cast(num_args(e)) || i < 0) - throw exception(sstream() << "invalid application argument #" << i << ", application has " << num_args(e) << " arguments"); - return push_expr(L, arg(e, i)); -} - -static int expr_fields(lua_State * L) { - expr & e = to_nonnull_expr(L, 1); - switch (e.kind()) { - case expr_kind::Var: lua_pushinteger(L, var_idx(e)); return 1; - case expr_kind::Constant: return push_name(L, const_name(e)); - case expr_kind::Type: return push_level(L, ty_level(e)); - case expr_kind::Value: - if (is_nat_value(e)) { - return push_mpz(L, nat_value_numeral(e)); - } else if (is_int_value(e)) { - return push_mpz(L, int_value_numeral(e)); - } else if (is_real_value(e)) { - return push_mpq(L, real_value_numeral(e)); - } else { - return 0; - } - case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2; - case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2; - case expr_kind::Lambda: - case expr_kind::Pi: push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3; - case expr_kind::Let: push_name(L, let_name(e)); push_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4; - case expr_kind::MetaVar: push_name(L, metavar_name(e)); push_local_context(L, metavar_lctx(e)); return 2; - } - lean_unreachable(); // LCOV_EXCL_LINE - return 0; // LCOV_EXCL_LINE -} - -static int expr_for_each(lua_State * L) { - expr & e = to_nonnull_expr(L, 1); // expr - luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun - auto f = [&](expr const & a, unsigned offset) { - lua_pushvalue(L, 2); // push user-fun - push_expr(L, a); - lua_pushinteger(L, offset); - pcall(L, 2, 1, 0); - bool r = true; - if (lua_isboolean(L, -1)) - r = lua_toboolean(L, -1); - lua_pop(L, 1); - return r; - }; - for_each_fn proc(f); - proc(e); - return 0; -} - -static int expr_has_free_var(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 2) - lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2))); - else - lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3))); - return 1; -} - -static int expr_lift_free_vars(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 2) - return push_expr(L, lift_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2))); - else - return push_expr(L, lift_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3))); -} - -static int expr_lower_free_vars(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 2) - return push_expr(L, lower_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2))); - else - return push_expr(L, lower_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3))); -} - -// Copy Lua table/array elements to r -static void copy_lua_array(lua_State * L, int tidx, buffer & r) { - luaL_checktype(L, tidx, LUA_TTABLE); - int n = objlen(L, tidx); - for (int i = 1; i <= n; i++) { - lua_rawgeti(L, tidx, i); - r.push_back(to_expr(L, -1)); - lua_pop(L, 1); - } -} - -static int expr_instantiate(lua_State * L) { - expr const & e = to_expr(L, 1); - if (is_expr(L, 2)) { - return push_expr(L, instantiate(e, to_expr(L, 2))); - } else { - buffer s; - copy_lua_array(L, 2, s); - return push_expr(L, instantiate(e, s.size(), s.data())); - } -} - -static int expr_abstract(lua_State * L) { - expr const & e = to_expr(L, 1); - if (is_expr(L, 2)) { - expr const & e2 = to_expr(L, 2); - return push_expr(L, abstract(e, 1, &e2)); - } else { - buffer s; - copy_lua_array(L, 2, s); - return push_expr(L, abstract(e, s.size(), s.data())); - } -} - -static int expr_occurs(lua_State * L) { - lua_pushboolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); - return 1; -} - -static int expr_is_eqp(lua_State * L) { - lua_pushboolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); - return 1; -} - -static int expr_hash(lua_State * L) { - lua_pushinteger(L, to_expr(L, 1).hash()); - return 1; -} - -static const struct luaL_Reg expr_m[] = { - {"__gc", expr_gc}, // never throws - {"__tostring", safe_function}, - {"__eq", safe_function}, - {"__lt", safe_function}, - {"__call", safe_function}, - {"kind", safe_function}, - {"is_null", safe_function}, - {"is_var", safe_function}, - {"is_constant", safe_function}, - {"is_app", safe_function}, - {"is_eq", safe_function}, - {"is_lambda", safe_function}, - {"is_pi", safe_function}, - {"is_abstraction", safe_function}, - {"is_let", safe_function}, - {"is_value", safe_function}, - {"is_metavar", safe_function}, - {"fields", safe_function}, - {"data", safe_function}, - {"args", safe_function}, - {"num_args", safe_function}, - {"arg", safe_function}, - {"for_each", safe_function}, - {"has_free_vars", safe_function}, - {"closed", safe_function}, - {"has_free_var", safe_function}, - {"lift_free_vars", safe_function}, - {"lower_free_vars", safe_function}, - {"instantiate", safe_function}, - {"abstract", safe_function}, - {"occurs", safe_function}, - {"has_metavar", safe_function}, - {"is_eqp", safe_function}, - {"hash", safe_function}, - {0, 0} -}; - -static int mk_nat_value(lua_State * L) { - mpz v = to_mpz_ext(L, 1); - if (v < 0) - throw exception("arg #1 must be non-negative"); - return push_expr(L, mk_nat_value(v)); -} - -static int mk_int_value(lua_State * L) { - return push_expr(L, mk_int_value(to_mpz_ext(L, 1))); -} - -static int mk_real_value(lua_State * L) { - return push_expr(L, mk_real_value(to_mpq_ext(L, 1))); -} - -void open_expr(lua_State * L) { - luaL_newmetatable(L, expr_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, expr_m, 0); - - SET_GLOBAL_FUN(expr_mk_constant, "mk_constant"); - SET_GLOBAL_FUN(expr_mk_constant, "Const"); - SET_GLOBAL_FUN(expr_mk_var, "mk_var"); - SET_GLOBAL_FUN(expr_mk_var, "Var"); - SET_GLOBAL_FUN(expr_mk_app, "mk_app"); - SET_GLOBAL_FUN(expr_mk_eq, "mk_eq"); - SET_GLOBAL_FUN(expr_mk_eq, "Eq"); - SET_GLOBAL_FUN(expr_mk_lambda, "mk_lambda"); - SET_GLOBAL_FUN(expr_mk_pi, "mk_pi"); - SET_GLOBAL_FUN(expr_mk_arrow, "mk_arrow"); - SET_GLOBAL_FUN(expr_mk_let, "mk_let"); - SET_GLOBAL_FUN(expr_fun, "fun"); - SET_GLOBAL_FUN(expr_fun, "Fun"); - SET_GLOBAL_FUN(expr_pi, "Pi"); - SET_GLOBAL_FUN(expr_let, "Let"); - SET_GLOBAL_FUN(expr_type, "mk_type"); - SET_GLOBAL_FUN(expr_type, "Type"); - SET_GLOBAL_FUN(expr_mk_metavar, "mk_metavar"); - SET_GLOBAL_FUN(expr_pred, "is_expr"); - SET_GLOBAL_FUN(mk_nat_value, "mk_nat_value"); - SET_GLOBAL_FUN(mk_nat_value, "nVal"); - SET_GLOBAL_FUN(mk_int_value, "mk_int_value"); - SET_GLOBAL_FUN(mk_int_value, "iVal"); - SET_GLOBAL_FUN(mk_real_value, "mk_real_value"); - SET_GLOBAL_FUN(mk_real_value, "rVal"); - - lua_newtable(L); - SET_ENUM("Var", expr_kind::Var); - SET_ENUM("Constant", expr_kind::Constant); - SET_ENUM("Type", expr_kind::Type); - SET_ENUM("Value", expr_kind::Value); - SET_ENUM("App", expr_kind::App); - SET_ENUM("Eq", expr_kind::Eq); - SET_ENUM("Lambda", expr_kind::Lambda); - SET_ENUM("Pi", expr_kind::Pi); - SET_ENUM("Let", expr_kind::Let); - SET_ENUM("MetaVar", expr_kind::MetaVar); - lua_setglobal(L, "expr_kind"); -} -} diff --git a/src/bindings/lua/format.cpp b/src/bindings/lua/format.cpp deleted file mode 100644 index b1ad24202..000000000 --- a/src/bindings/lua/format.cpp +++ /dev/null @@ -1,117 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/debug.h" -#include "util/sstream.h" -#include "util/sexpr/options.h" -#include "util/sexpr/format.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/numerics.h" -#include "bindings/lua/options.h" - -namespace lean { -DECL_UDATA(format) - -format to_format_elem(lua_State * L, int idx) { - if (is_format(L, idx)) - return to_format(L, idx); - else if (lua_isnumber(L, idx)) - return format(static_cast(lua_tonumber(L, idx))); - else if (is_name(L, idx)) - return format(to_name(L, idx)); - else if (is_mpz(L, idx)) - return format(to_mpz(L, idx)); - else if (is_mpq(L, idx)) - return format(to_mpq(L, idx)); - else - return format(lua_tostring(L, idx)); -} - -static int format_tostring(lua_State * L) { - std::ostringstream out; - out << mk_pair(to_format(L, 1), get_global_options(L)); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int format_concat(lua_State * L) { - return push_format(L, compose(to_format_elem(L, 1), to_format_elem(L, 2))); -} - -static int mk_format(lua_State * L) { - format r; - int nargs = lua_gettop(L); - if (nargs == 0) { - r = format(); - } else { - int i = nargs; - r = to_format_elem(L, i); - i--; - for (; i >= 1; i--) { - r = compose(to_format_elem(L, i), r); - } - } - return push_format(L, r); -} - -static int format_nest(lua_State * L) { - return push_format(L, nest(luaL_checkinteger(L, 2), to_format(L, 1))); -} - -static int format_group(lua_State * L) { - return push_format(L, group(to_format(L, 1))); -} - -static int format_highlight(lua_State * L) { - char const * color_str = luaL_checkstring(L, 2); - format::format_color color; - if (strcmp(color_str, "red") == 0) { - color = format::RED; - } else if (strcmp(color_str, "green") == 0) { - color = format::GREEN; - } else if (strcmp(color_str, "orange") == 0) { - color = format::ORANGE; - } else if (strcmp(color_str, "blue") == 0) { - color = format::BLUE; - } else if (strcmp(color_str, "cyan") == 0) { - color = format::CYAN; - } else if (strcmp(color_str, "grey") == 0) { - color = format::GREY; - } else { - throw exception(sstream() << "unknown color '" << color_str << "'"); - } - return push_format(L, highlight(to_format(L, 1), color)); -} - -static int format_line(lua_State * L) { return push_format(L, line()); } -static int format_space(lua_State * L) { return push_format(L, space()); } - -static const struct luaL_Reg format_m[] = { - {"__gc", format_gc}, // never throws - {"__tostring", safe_function}, - {"__concat", safe_function}, - {"nest", safe_function}, - {"group", safe_function}, - {"highlight", safe_function}, - {0, 0} -}; - -void open_format(lua_State * L) { - luaL_newmetatable(L, format_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, format_m, 0); - - SET_GLOBAL_FUN(mk_format, "format"); - SET_GLOBAL_FUN(format_line, "line"); - SET_GLOBAL_FUN(format_space, "space"); - SET_GLOBAL_FUN(format_pred, "is_format"); -} -} diff --git a/src/bindings/lua/format.h b/src/bindings/lua/format.h deleted file mode 100644 index 6013e75f3..000000000 --- a/src/bindings/lua/format.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(format) -void open_format(lua_State * L); -} diff --git a/src/bindings/lua/formatter.cpp b/src/bindings/lua/formatter.cpp deleted file mode 100644 index 19decb657..000000000 --- a/src/bindings/lua/formatter.cpp +++ /dev/null @@ -1,111 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "kernel/formatter.h" -#include "bindings/lua/util.h" -#include "bindings/lua/options.h" -#include "bindings/lua/format.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/context.h" -#include "bindings/lua/environment.h" -#include "bindings/lua/object.h" -#include "bindings/lua/io_state.h" - -namespace lean { -DECL_UDATA(formatter) - -[[ noreturn ]] void throw_invalid_formatter_call() { - throw exception("invalid formatter invocation, the acceptable arguments are: (expr, options?), (context, options?), (context, expr, bool? options?), (kernel object, options?), (environment, options?)"); -} - -static int formatter_call(lua_State * L) { - int nargs = lua_gettop(L); - formatter & fmt = to_formatter(L, 1); - options opts = get_global_options(L); - if (nargs <= 3) { - if (nargs == 3) { - if (is_options(L, 3)) - opts = to_options(L, 3); - else if (is_context(L, 2) && is_expr(L, 3)) - return push_format(L, fmt(to_context(L, 2), to_expr(L, 3))); - else - throw_invalid_formatter_call(); - } - if (is_expr(L, 2)) { - return push_format(L, fmt(to_expr(L, 2), opts)); - } else if (is_context(L, 2)) { - return push_format(L, fmt(to_context(L, 2), opts)); - } else if (is_environment(L, 2)) { - ro_environment env(L, 2); - return push_format(L, fmt(env, opts)); - } else if (is_object(L, 2)) { - return push_format(L, fmt(to_object(L, 2), opts)); - } else { - throw_invalid_formatter_call(); - } - } else if (nargs <= 5) { - if (nargs == 5) - opts = to_options(L, 5); - return push_format(L, fmt(to_context(L, 2), to_expr(L, 3), lua_toboolean(L, 4), opts)); - } else { - throw_invalid_formatter_call(); - } -} - -static const struct luaL_Reg formatter_m[] = { - {"__gc", formatter_gc}, // never throws - {"__call", safe_function}, - {0, 0} -}; - -static char g_formatter_key; -static formatter g_simple_formatter = mk_simple_formatter(); - -formatter get_global_formatter(lua_State * L) { - io_state * io = get_io_state(L); - if (io != nullptr) { - return io->get_formatter(); - } else { - lua_pushlightuserdata(L, static_cast(&g_formatter_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (is_formatter(L, -1)) { - formatter r = to_formatter(L, -1); - lua_pop(L, 1); - return r; - } else { - lua_pop(L, 1); - return g_simple_formatter; - } - } -} - -void set_global_formatter(lua_State * L, formatter const & fmt) { - io_state * io = get_io_state(L); - if (io != nullptr) { - io->set_formatter(fmt); - } else { - lua_pushlightuserdata(L, static_cast(&g_formatter_key)); - push_formatter(L, fmt); - lua_settable(L, LUA_REGISTRYINDEX); - } -} - -int get_formatter(lua_State * L) { - return push_formatter(L, get_global_formatter(L)); -} - -void open_formatter(lua_State * L) { - luaL_newmetatable(L, formatter_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, formatter_m, 0); - - SET_GLOBAL_FUN(formatter_pred, "is_formatter"); - SET_GLOBAL_FUN(get_formatter, "get_formatter"); -} -} diff --git a/src/bindings/lua/formatter.h b/src/bindings/lua/formatter.h deleted file mode 100644 index e36e6433a..000000000 --- a/src/bindings/lua/formatter.h +++ /dev/null @@ -1,25 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(formatter) -void open_formatter(lua_State * L); -/** - \brief Return the formatter object associated with the given Lua State. - This procedure checks for options at: - 1- Lean state object associated with \c L - 2- Lua Registry associated with \c L -*/ -formatter get_global_formatter(lua_State * L); -/** - \brief Update the formatter object associated with the given Lua State. - If \c L is associated with a Lean state object \c S, then we update the formatter of \c S. - Otherwise, we update the registry of \c L. -*/ -void set_global_formatter(lua_State * L, formatter const & fmt); -} diff --git a/src/bindings/lua/frontend_lean.cpp b/src/bindings/lua/frontend_lean.cpp index 1007ecea9..04c452fee 100644 --- a/src/bindings/lua/frontend_lean.cpp +++ b/src/bindings/lua/frontend_lean.cpp @@ -5,15 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include +#include "util/lua.h" +#include "util/sexpr/options.h" #include "library/io_state.h" +#include "library/kernel_bindings.h" #include "frontends/lean/parser.h" -#include "bindings/lua/util.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/environment.h" -#include "bindings/lua/options.h" -#include "bindings/lua/formatter.h" -#include "bindings/lua/io_state.h" #include "bindings/lua/leanlua_state.h" namespace lean { diff --git a/src/bindings/lua/goal.cpp b/src/bindings/lua/goal.cpp deleted file mode 100644 index 5346100b0..000000000 --- a/src/bindings/lua/goal.cpp +++ /dev/null @@ -1,176 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "library/tactic/goal.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/formatter.h" -#include "bindings/lua/format.h" -#include "bindings/lua/options.h" - -namespace lean { -DECL_UDATA(hypotheses) - -static int mk_hypotheses(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_hypotheses(L, hypotheses()); - } else if (nargs == 2) { - return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses())); - } else if (nargs == 3) { - return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), to_hypotheses(L, 3))); - } else { - throw exception("hypotheses functions expects 0 (empty list), 2 (name & expr for singleton hypotheses list), or 3 (name & expr & hypotheses list) arguments"); - } -} - -static int hypotheses_is_nil(lua_State * L) { - lua_pushboolean(L, !to_hypotheses(L, 1)); - return 1; -} - -static int hypotheses_head(lua_State * L) { - hypotheses const & hs = to_hypotheses(L, 1); - if (!hs) - throw exception("head method expects a non-empty hypotheses list"); - push_name(L, head(hs).first); - push_expr(L, head(hs).second); - return 2; -} - -static int hypotheses_tail(lua_State * L) { - hypotheses const & hs = to_hypotheses(L, 1); - if (!hs) - throw exception("tail method expects a non-empty hypotheses list"); - push_hypotheses(L, tail(hs)); - return 1; -} - -static int hypotheses_next(lua_State * L) { - hypotheses & hs = to_hypotheses(L, lua_upvalueindex(1)); - if (hs) { - push_hypotheses(L, tail(hs)); - lua_replace(L, lua_upvalueindex(1)); - push_name(L, head(hs).first); - push_expr(L, head(hs).second); - return 2; - } else { - lua_pushnil(L); - return 1; - } -} - -static int hypotheses_items(lua_State * L) { - hypotheses & hs = to_hypotheses(L, 1); - push_hypotheses(L, hs); // upvalue(1): hypotheses - lua_pushcclosure(L, &safe_function, 1); // create closure with 1 upvalue - return 1; -} - -static int hypotheses_len(lua_State * L) { - lua_pushinteger(L, length(to_hypotheses(L, 1))); - return 1; -} - -static const struct luaL_Reg hypotheses_m[] = { - {"__gc", hypotheses_gc}, // never throws - {"__len", safe_function}, - {"size", safe_function}, - {"pairs", safe_function}, - {"is_nil", safe_function}, - {"empty", safe_function}, - {"head", safe_function}, - {"tail", safe_function}, - {0, 0} -}; - -DECL_UDATA(goal) - -static int mk_goal(lua_State * L) { - return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); -} - -static int goal_is_null(lua_State * L) { - lua_pushboolean(L, !to_goal(L, 1)); - return 1; -} - -static int goal_hypotheses(lua_State * L) { - return push_hypotheses(L, to_goal(L, 1).get_hypotheses()); -} - -static int goal_conclusion(lua_State * L) { - return push_expr(L, to_goal(L, 1).get_conclusion()); -} - -static int goal_unique_name(lua_State * L) { - return push_name(L, to_goal(L, 1).mk_unique_hypothesis_name(to_name_ext(L, 2))); -} - -static int goal_tostring(lua_State * L) { - std::ostringstream out; - goal & g = to_goal(L, 1); - if (g) { - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(g.pp(fmt, opts), opts); - } else { - out << ""; - } - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int goal_pp(lua_State * L) { - int nargs = lua_gettop(L); - goal & g = to_goal(L, 1); - if (!g) { - return push_format(L, format()); - } else if (nargs == 1) { - return push_format(L, g.pp(get_global_formatter(L), get_global_options(L))); - } else if (nargs == 2) { - if (is_formatter(L, 2)) - return push_format(L, g.pp(to_formatter(L, 2), get_global_options(L))); - else - return push_format(L, g.pp(get_global_formatter(L), to_options(L, 2))); - } else { - return push_format(L, g.pp(to_formatter(L, 2), to_options(L, 3))); - } -} - -static const struct luaL_Reg goal_m[] = { - {"__gc", goal_gc}, // never throws - {"__tostring", safe_function}, - {"is_null", safe_function}, - {"hypotheses", safe_function}, - {"hyps", safe_function}, - {"conclusion", safe_function}, - {"unique_name", safe_function}, - {"pp", safe_function}, - {0, 0} -}; - -void open_goal(lua_State * L) { - luaL_newmetatable(L, hypotheses_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, hypotheses_m, 0); - - SET_GLOBAL_FUN(hypotheses_pred, "is_hypotheses"); - SET_GLOBAL_FUN(mk_hypotheses, "hypotheses"); - - luaL_newmetatable(L, goal_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, goal_m, 0); - - SET_GLOBAL_FUN(goal_pred, "is_goal"); - SET_GLOBAL_FUN(mk_goal, "goal"); -} -} diff --git a/src/bindings/lua/goal.h b/src/bindings/lua/goal.h deleted file mode 100644 index dabac273f..000000000 --- a/src/bindings/lua/goal.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "library/tactic/goal.h" -namespace lean { -UDATA_DEFS_CORE(hypotheses) -UDATA_DEFS(goal) -void open_goal(lua_State * L); -} diff --git a/src/bindings/lua/io_state.cpp b/src/bindings/lua/io_state.cpp deleted file mode 100644 index fc0c72336..000000000 --- a/src/bindings/lua/io_state.cpp +++ /dev/null @@ -1,100 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "library/io_state.h" -#include "bindings/lua/util.h" -#include "bindings/lua/io_state.h" -#include "bindings/lua/options.h" -#include "bindings/lua/formatter.h" - -namespace lean { -DECL_UDATA(io_state) - -int mk_io_state(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - return push_io_state(L, io_state()); - else if (nargs == 1) - return push_io_state(L, io_state(to_io_state(L, 1))); - else - 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; -} - -int print(lua_State * L, io_state & ios, int start, bool reg); - -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 const struct luaL_Reg io_state_m[] = { - {"__gc", io_state_gc}, // never throws - {"get_options", safe_function}, - {"set_options", safe_function}, - {"get_formatter", safe_function}, - {"print_diagnostic", safe_function}, - {"print_regular", safe_function}, - {"print", safe_function}, - {"diagnostic", safe_function}, - {0, 0} -}; - -void open_io_state(lua_State * L) { - luaL_newmetatable(L, io_state_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, io_state_m, 0); - - SET_GLOBAL_FUN(io_state_pred, "is_io_state"); - SET_GLOBAL_FUN(mk_io_state, "io_state"); -} - -static char g_set_state_key; - -set_io_state::set_io_state(lua_State * L, io_state & st) { - m_state = L; - m_prev = get_io_state(L); - lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); - lua_pushlightuserdata(m_state, &st); - lua_settable(m_state, LUA_REGISTRYINDEX); -} - -set_io_state::~set_io_state() { - lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); - lua_pushlightuserdata(m_state, m_prev); - lua_settable(m_state, LUA_REGISTRYINDEX); -} - -io_state * get_io_state(lua_State * L) { - lua_pushlightuserdata(L, static_cast(&g_set_state_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (!lua_islightuserdata(L, -1)) { - lua_pop(L, 1); - return nullptr; - } else { - io_state * r = static_cast(lua_touserdata(L, -1)); - lua_pop(L, 1); - return r; - } -} -} diff --git a/src/bindings/lua/io_state.h b/src/bindings/lua/io_state.h deleted file mode 100644 index d5cf34c69..000000000 --- a/src/bindings/lua/io_state.h +++ /dev/null @@ -1,30 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "library/io_state.h" - -namespace lean { -UDATA_DEFS(io_state) -void open_io_state(lua_State * L); -/** - \brief Auxiliary class for temporarily setting the Lua registry of a Lua state - with a Lean io_state object. -*/ -class set_io_state { - lua_State * m_state; - io_state * m_prev; -public: - set_io_state(lua_State * L, io_state & st); - ~set_io_state(); -}; -/** - \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); -} diff --git a/src/bindings/lua/justification.cpp b/src/bindings/lua/justification.cpp deleted file mode 100644 index d4561672f..000000000 --- a/src/bindings/lua/justification.cpp +++ /dev/null @@ -1,143 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "kernel/justification.h" -#include "bindings/lua/util.h" -#include "bindings/lua/options.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/format.h" -#include "bindings/lua/formatter.h" - -namespace lean { -DECL_UDATA(justification) - -static int justification_tostring(lua_State * L) { - std::ostringstream out; - justification & jst = to_justification(L, 1); - if (jst) { - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(jst.pp(fmt, opts), opts); - } else { - out << ""; - } - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int justification_has_children(lua_State * L) { - lua_pushboolean(L, to_justification(L, 1).has_children()); - return 1; -} - -static int justification_is_null(lua_State * L) { - lua_pushboolean(L, !to_justification(L, 1)); - return 1; -} - -/** - \brief Iterator (closure base function) for justification children. See \c justification_children -*/ -static int justification_next_child(lua_State * L) { - unsigned i = lua_tointeger(L, lua_upvalueindex(2)); - unsigned num = objlen(L, lua_upvalueindex(1)); - if (i > num) { - lua_pushnil(L); - } else { - lua_pushinteger(L, i + 1); - lua_replace(L, lua_upvalueindex(2)); // update i - lua_rawgeti(L, lua_upvalueindex(1), i); // read children[i] - } - return 1; -} - -static int justification_children(lua_State * L) { - buffer children; - to_justification(L, 1).get_children(children); - lua_newtable(L); - int i = 1; - for (auto jcell : children) { - push_justification(L, justification(jcell)); - lua_rawseti(L, -2, i); - i = i + 1; - } - lua_pushinteger(L, 1); - lua_pushcclosure(L, &safe_function, 2); // create closure with 2 upvalues - return 1; -} - -static int justification_get_main_expr(lua_State * L) { - return push_expr(L, to_justification(L, 1).get_main_expr()); -} - -static int justification_pp(lua_State * L) { - int nargs = lua_gettop(L); - justification & jst = to_justification(L, 1); - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - bool display_children = true; - - if (nargs == 2) { - if (lua_isboolean(L, 2)) { - display_children = lua_toboolean(L, 2); - } else { - luaL_checktype(L, 2, LUA_TTABLE); - - lua_pushstring(L, "formatter"); - lua_gettable(L, 2); - if (is_formatter(L, -1)) - fmt = to_formatter(L, -1); - lua_pop(L, 1); - - lua_pushstring(L, "options"); - lua_gettable(L, 2); - if (is_options(L, -1)) - opts = to_options(L, -1); - lua_pop(L, 1); - - lua_pushstring(L, "display_children"); - lua_gettable(L, 2); - if (lua_isboolean(L, -1)) - display_children = lua_toboolean(L, -1); - lua_pop(L, 1); - } - } - return push_format(L, jst.pp(fmt, opts, nullptr, display_children)); -} - -static int justification_depends_on(lua_State * L) { - lua_pushboolean(L, depends_on(to_justification(L, 1), to_justification(L, 2))); - return 1; -} - -static int mk_assumption_justification(lua_State * L) { - return push_justification(L, mk_assumption_justification(luaL_checkinteger(L, 1))); -} - -static const struct luaL_Reg justification_m[] = { - {"__gc", justification_gc}, // never throws - {"__tostring", safe_function}, - {"is_null", safe_function}, - {"has_children", safe_function}, - {"children", safe_function}, - {"get_main_expr", safe_function}, - {"pp", safe_function}, - {"depends_on", safe_function}, - {0, 0} -}; - -void open_justification(lua_State * L) { - luaL_newmetatable(L, justification_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, justification_m, 0); - - SET_GLOBAL_FUN(mk_assumption_justification, "mk_assumption_justification"); - SET_GLOBAL_FUN(justification_pred, "is_justification"); -} -} diff --git a/src/bindings/lua/justification.h b/src/bindings/lua/justification.h deleted file mode 100644 index e534315c8..000000000 --- a/src/bindings/lua/justification.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(justification) -void open_justification(lua_State * L); -} diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index b4c9f17e1..46ab84a5c 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -9,43 +9,72 @@ Author: Leonardo de Moura #include #include #include -#include +#include "util/lua.h" #include "util/debug.h" #include "util/exception.h" #include "util/memory.h" #include "util/buffer.h" #include "util/interrupt.h" -#include "library/io_state.h" +#include "util/open_module.h" +#include "util/numerics/open_module.h" +#include "util/sexpr/open_module.h" +#include "kernel/kernel_exception.h" +#include "library/kernel_bindings.h" +#include "library/arith/open_module.h" +#include "library/tactic/open_module.h" +#include "library/elaborator/elaborator_exception.h" +#include "frontends/lean/frontend.h" #include "bindings/lua/leanlua_state.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/splay_map.h" -#include "bindings/lua/numerics.h" -#include "bindings/lua/options.h" -#include "bindings/lua/sexpr.h" -#include "bindings/lua/format.h" -#include "bindings/lua/formatter.h" -#include "bindings/lua/level.h" -#include "bindings/lua/local_context.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/context.h" -#include "bindings/lua/object.h" -#include "bindings/lua/environment.h" -#include "bindings/lua/justification.h" -#include "bindings/lua/metavar_env.h" -#include "bindings/lua/goal.h" -#include "bindings/lua/proof_builder.h" -#include "bindings/lua/cex_builder.h" -#include "bindings/lua/proof_state.h" -#include "bindings/lua/io_state.h" -#include "bindings/lua/type_inferer.h" #include "bindings/lua/frontend_lean.h" #include "bindings/lua/lean.lua" extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); } namespace lean { -static void open_patch(lua_State * L); +void _check_result(lua_State * L, int result) { + if (result) { + if (is_justification(L, -1)) + throw elaborator_exception(to_justification(L, -1)); + else + throw lua_exception(lua_tostring(L, -1)); + } +} + +static set_check_result set_check(_check_result); + +static int _safe_function_wrapper(lua_State * L, lua_CFunction f) { + try { + return f(L); + } catch (kernel_exception & e) { + std::ostringstream out; + options o = get_global_options(L); + out << mk_pair(e.pp(get_global_formatter(L), o), o); + lua_pushstring(L, out.str().c_str()); + } catch (elaborator_exception & e) { + push_justification(L, e.get_justification()); + } catch (exception & e) { + lua_pushstring(L, e.what()); + } catch (std::bad_alloc &) { + lua_pushstring(L, "out of memory"); + } catch (std::exception & e) { + lua_pushstring(L, e.what()); + } catch(...) { + lua_pushstring(L, "unknown error"); + } + return lua_error(L); +} + +static int mk_environment(lua_State * L) { + frontend f; + return push_environment(L, f.get_environment()); +} + +static void decl_environment(lua_State * L) { + SET_GLOBAL_FUN(mk_environment, "environment"); +} + +static set_safe_function_wrapper set_wrapper(_safe_function_wrapper); + static void open_state(lua_State * L); static void open_thread(lua_State * L); static void open_interrupt(lua_State * L); @@ -138,6 +167,8 @@ static void copy_values(lua_State * src, int first, int last, lua_State * tgt) { } } +void open_splay_map(lua_State * L); + static char g_weak_ptr_key; // key for Lua registry (used at get_weak_ptr and save_weak_ptr) struct leanlua_state::imp { @@ -170,33 +201,20 @@ struct leanlua_state::imp { if (m_state == nullptr) throw exception("fail to create Lua interpreter"); luaL_openlibs(m_state); - open_patch(m_state); - open_name(m_state); - open_splay_map(m_state); - open_mpz(m_state); - open_mpq(m_state); - open_options(m_state); - open_sexpr(m_state); - open_format(m_state); - open_formatter(m_state); - open_level(m_state); - open_local_context(m_state); - open_expr(m_state); - open_context(m_state); - open_object(m_state); - open_environment(m_state); - open_justification(m_state); - open_metavar_env(m_state); + open_util_module(m_state); + open_numerics_module(m_state); + open_sexpr_module(m_state); + open_kernel_module(m_state); + open_arith_module(m_state); + open_tactic_module(m_state); + open_state(m_state); - open_type_inferer(m_state); - open_goal(m_state); - open_proof_builder(m_state); - open_cex_builder(m_state); - open_proof_state(m_state); open_frontend_lean(m_state); open_thread(m_state); open_interrupt(m_state); - open_io_state(m_state); + + decl_environment(m_state); + dostring(g_leanlua_extra); } @@ -252,59 +270,6 @@ void leanlua_state::dostring(char const * str, environment & env, io_state & st) m_ptr->dostring(str, env, st); } -static std::mutex g_print_mutex; - -static void print(io_state * ios, bool reg, char const * msg) { - if (ios) { - if (reg) - regular(*ios) << msg; - else - diagnostic(*ios) << msg; - } else { - std::cout << msg; - } -} - -/** \brief Thread safe version of print function */ -static int print(lua_State * L, int start, bool reg = false) { - std::lock_guard lock(g_print_mutex); - io_state * ios = get_io_state(L); - int n = lua_gettop(L); - int i; - lua_getglobal(L, "tostring"); - for (i = start; i <= n; i++) { - char const * s; - size_t l; - lua_pushvalue(L, -1); - lua_pushvalue(L, i); - lua_call(L, 1, 1); - s = lua_tolstring(L, -1, &l); - if (s == NULL) - throw exception("'to_string' must return a string to 'print'"); - if (i > start) { - print(ios, reg, "\t"); - } - print(ios, reg, s); - lua_pop(L, 1); - } - print(ios, reg, "\n"); - return 0; -} - -int print(lua_State * L, io_state & ios, int start, bool reg) { - set_io_state set(L, ios); - return print(L, start, reg); -} - -static int print(lua_State * L) { - return print(L, 1, true); -} - -/** \brief Redefine some functions from the Lua library */ -static void open_patch(lua_State * L) { - SET_GLOBAL_FUN(print, "print"); -} - constexpr char const * state_mt = "luastate.mt"; bool is_state(lua_State * L, int idx) { diff --git a/src/bindings/lua/leanlua_state.h b/src/bindings/lua/leanlua_state.h index 60be38bed..a98c9ccb1 100644 --- a/src/bindings/lua/leanlua_state.h +++ b/src/bindings/lua/leanlua_state.h @@ -7,8 +7,8 @@ Author: Leonardo de Moura #pragma once #include #include +#include "util/lua_exception.h" #include "library/script_evaluator.h" -#include "bindings/lua/lua_exception.h" namespace lean { class environment; diff --git a/src/bindings/lua/level.cpp b/src/bindings/lua/level.cpp deleted file mode 100644 index 27b267948..000000000 --- a/src/bindings/lua/level.cpp +++ /dev/null @@ -1,139 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/buffer.h" -#include "util/sexpr/options.h" -#include "kernel/level.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/options.h" - -namespace lean { -DECL_UDATA(level) - -static int level_tostring(lua_State * L) { - std::ostringstream out; - options opts = get_global_options(L); - out << mk_pair(pp(to_level(L, 1), opts), opts); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int level_eq(lua_State * L) { - lua_pushboolean(L, to_level(L, 1) == to_level(L, 2)); - return 1; -} - -static int level_lt(lua_State * L) { - lua_pushboolean(L, to_level(L, 1) < to_level(L, 2)); - return 1; -} - -static int mk_level(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - // bottom - return push_level(L, level()); - } else if (nargs == 1) { - // uvar - return push_level(L, level(to_name_ext(L, 1))); - } else if (nargs == 2 && lua_isnumber(L, 2)) { - // lift - return push_level(L, to_level(L, 1) + luaL_checkinteger(L, 2)); - } else { - // max - level r = to_level(L, 1); - for (int i = 2; i <= nargs; i++) { - r = max(r, to_level(L, i)); - } - return push_level(L, r); - } -} - -#define LEVEL_PRED(P) \ -static int level_ ## P(lua_State * L) { \ - lua_pushboolean(L, P(to_level(L, 1))); \ - return 1; \ -} - -LEVEL_PRED(is_bottom) -LEVEL_PRED(is_uvar) -LEVEL_PRED(is_lift) -LEVEL_PRED(is_max) - -static int level_name(lua_State * L) { - if (!is_uvar(to_level(L, 1))) - throw exception("arg #1 must be a Lean level universal variable"); - return push_name(L, uvar_name(to_level(L, 1))); -} - -static int level_lift_of(lua_State * L) { - if (!is_lift(to_level(L, 1))) - throw exception("arg #1 must be a Lean level lift"); - return push_level(L, lift_of(to_level(L, 1))); -} - -static int level_lift_offset(lua_State * L) { - if (!is_lift(to_level(L, 1))) - throw exception("arg #1 must be a Lean level lift"); - lua_pushinteger(L, lift_offset(to_level(L, 1))); - return 1; -} - -static int level_max_size(lua_State * L) { - if (!is_max(to_level(L, 1))) - throw exception("arg #1 must be a Lean level max"); - lua_pushinteger(L, max_size(to_level(L, 1))); - return 1; -} - -static int level_max_level(lua_State * L) { - if (!is_max(to_level(L, 1))) - throw exception("arg #1 must be a Lean level max"); - return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2))); -} - -static int level_get_kind(lua_State * L) { - lua_pushinteger(L, static_cast(kind(to_level(L, 1)))); - return 1; -} - -static const struct luaL_Reg level_m[] = { - {"__gc", level_gc}, // never throws - {"__tostring", safe_function}, - {"__eq", safe_function}, - {"__lt", safe_function}, - {"kind", safe_function}, - {"is_bottom", safe_function}, - {"is_lift", safe_function}, - {"is_max", safe_function}, - {"is_uvar", safe_function}, - {"uvar_name", safe_function}, - {"lift_of", safe_function}, - {"lift_offset", safe_function}, - {"max_size", safe_function}, - {"max_level", safe_function}, - {0, 0} -}; - -void open_level(lua_State * L) { - luaL_newmetatable(L, level_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, level_m, 0); - - SET_GLOBAL_FUN(mk_level, "level"); - SET_GLOBAL_FUN(level_pred, "is_level"); - - lua_newtable(L); - SET_ENUM("UVar", level_kind::UVar); - SET_ENUM("Lift", level_kind::Lift); - SET_ENUM("Max", level_kind::Max); - lua_setglobal(L, "level_kind"); -} -} diff --git a/src/bindings/lua/level.h b/src/bindings/lua/level.h deleted file mode 100644 index 917146ae7..000000000 --- a/src/bindings/lua/level.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(level) -void open_level(lua_State * L); -} diff --git a/src/bindings/lua/local_context.cpp b/src/bindings/lua/local_context.cpp deleted file mode 100644 index 41b74f5d9..000000000 --- a/src/bindings/lua/local_context.cpp +++ /dev/null @@ -1,120 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "kernel/expr.h" -#include "bindings/lua/util.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/local_context.h" - -namespace lean { -DECL_UDATA(local_entry) - -static int local_entry_eq(lua_State * L) { - lua_pushboolean(L, to_local_entry(L, 1) == to_local_entry(L, 2)); - return 1; -} - -static int local_entry_mk_lift(lua_State * L) { - return push_local_entry(L, mk_lift(luaL_checkinteger(L, 1), luaL_checkinteger(L, 2))); -} - -static int local_entry_mk_inst(lua_State * L) { - return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_nonnull_expr(L, 2))); -} - -static int local_entry_is_lift(lua_State * L) { - lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_lift()); - return 1; -} - -static int local_entry_is_inst(lua_State * L) { - lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_inst()); - return 1; -} - -static int local_entry_s(lua_State * L) { - lua_pushinteger(L, to_local_entry(L, 1).s()); - return 1; -} - -static int local_entry_n(lua_State * L) { - local_entry & e = to_local_entry(L, 1); - if (!e.is_lift()) - throw exception("Lean lift local entry expected"); - lua_pushinteger(L, to_local_entry(L, 1).n()); - return 1; -} - -static int local_entry_v(lua_State * L) { - local_entry & e = to_local_entry(L, 1); - if (!e.is_inst()) - throw exception("Lean inst local entry expected"); - return push_expr(L, to_local_entry(L, 1).v()); - return 1; -} - -static const struct luaL_Reg local_entry_m[] = { - {"__gc", local_entry_gc}, // never throws - {"__eq", safe_function}, - {"is_lift", safe_function}, - {"is_inst", safe_function}, - {"s", safe_function}, - {"n", safe_function}, - {"v", safe_function}, - {0, 0} -}; - -DECL_UDATA(local_context) - -static int mk_local_context(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_local_context(L, local_context()); - } else { - return push_local_context(L, local_context(to_local_entry(L, 1), to_local_context(L, 2))); - } -} - -static int local_context_head(lua_State * L) { - return push_local_entry(L, head(to_local_context(L, 1))); -} - -static int local_context_tail(lua_State * L) { - return push_local_context(L, tail(to_local_context(L, 1))); -} - -static int local_context_is_nil(lua_State * L) { - lua_pushboolean(L, !to_local_context(L, 1)); - return 1; -} - -static const struct luaL_Reg local_context_m[] = { - {"__gc", local_context_gc}, - {"head", local_context_head}, - {"tail", local_context_tail}, - {"is_nil", local_context_is_nil}, - {0, 0} -}; - -void open_local_context(lua_State * L) { - luaL_newmetatable(L, local_entry_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, local_entry_m, 0); - SET_GLOBAL_FUN(local_entry_mk_lift, "mk_lift"); - SET_GLOBAL_FUN(local_entry_mk_inst, "mk_inst"); - SET_GLOBAL_FUN(local_entry_pred, "is_local_entry"); - - luaL_newmetatable(L, local_context_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, local_context_m, 0); - SET_GLOBAL_FUN(mk_local_context, "local_context"); - SET_GLOBAL_FUN(local_context_pred, "is_local_context"); -} -} diff --git a/src/bindings/lua/local_context.h b/src/bindings/lua/local_context.h deleted file mode 100644 index e59bb810a..000000000 --- a/src/bindings/lua/local_context.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "kernel/expr.h" -namespace lean { -UDATA_DEFS(local_entry) -UDATA_DEFS_CORE(local_context) -void open_local_context(lua_State * L); -} diff --git a/src/bindings/lua/metavar_env.cpp b/src/bindings/lua/metavar_env.cpp deleted file mode 100644 index eef17b03b..000000000 --- a/src/bindings/lua/metavar_env.cpp +++ /dev/null @@ -1,167 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/sstream.h" -#include "kernel/metavar.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/context.h" -#include "bindings/lua/justification.h" - -namespace lean { -DECL_UDATA(metavar_env) - -static int menv_mk_metavar(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 1) { - return push_expr(L, to_metavar_env(L, 1).mk_metavar()); - } else if (nargs == 2) { - return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2))); - } else { - return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), to_expr(L, 3))); - } -} - -static expr & to_metavar(lua_State * L, int i, bool lctx = true) { - expr & e = to_expr(L, i); - if (is_metavar(e)) { - if (lctx || !has_local_context(e)) - return e; - throw exception(sstream() << "arg #" << i << " must be a metavariable without a local context"); - } - throw exception(sstream() << "arg #" << i << " must be a metavariable"); -} - -static int menv_get_timestamp(lua_State * L) { - lua_pushinteger(L, to_metavar_env(L, 1).get_timestamp()); - return 1; -} - -static int menv_get_context(lua_State * L) { - if (is_expr(L, 2)) - return push_context(L, to_metavar_env(L, 1).get_context(to_metavar(L, 2, false))); - else - return push_context(L, to_metavar_env(L, 1).get_context(to_name_ext(L, 2))); -} - -static int menv_has_type(lua_State * L) { - if (is_expr(L, 2)) - lua_pushboolean(L, to_metavar_env(L, 1).has_type(to_metavar(L, 2))); - else - lua_pushboolean(L, to_metavar_env(L, 1).has_type(to_name_ext(L, 2))); - return 1; -} - -static int menv_get_type(lua_State * L) { - if (is_expr(L, 2)) - return push_expr(L, to_metavar_env(L, 1).get_type(to_metavar(L, 2))); - else - return push_expr(L, to_metavar_env(L, 1).get_type(to_name_ext(L, 2))); -} - -static int menv_is_assigned(lua_State * L) { - if (is_expr(L, 2)) - lua_pushboolean(L, to_metavar_env(L, 1).is_assigned(to_metavar(L, 2))); - else - lua_pushboolean(L, to_metavar_env(L, 1).is_assigned(to_name_ext(L, 2))); - return 1; -} - -static int menv_assign(lua_State * L) { - int nargs = lua_gettop(L); - justification jst; - if (nargs == 4) - jst = to_justification(L, 4); - if (is_expr(L, 2)) - to_metavar_env(L, 1).assign(to_metavar(L, 2, false), to_expr(L, 3), jst); - else - to_metavar_env(L, 1).assign(to_name_ext(L, 2), to_expr(L, 3), jst); - return 0; -} - -static int menv_get_subst(lua_State * L) { - if (is_expr(L, 2)) - return push_expr(L, to_metavar_env(L, 1).get_subst(to_metavar(L, 2))); - else - return push_expr(L, to_metavar_env(L, 1).get_subst(to_name_ext(L, 2))); -} - -static int menv_get_justification(lua_State * L) { - if (is_expr(L, 2)) - return push_justification(L, to_metavar_env(L, 1).get_justification(to_metavar(L, 2))); - else - return push_justification(L, to_metavar_env(L, 1).get_justification(to_name_ext(L, 2))); -} - -static int menv_get_subst_jst(lua_State * L) { - if (is_expr(L, 2)) { - auto p = to_metavar_env(L, 1).get_subst_jst(to_metavar(L, 2)); - push_expr(L, p.first); - push_justification(L, p.second); - } else { - auto p = to_metavar_env(L, 1).get_subst_jst(to_name_ext(L, 2)); - push_expr(L, p.first); - push_justification(L, p.second); - } - return 2; -} - -static int menv_for_each_subst(lua_State * L) { - luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun - to_metavar_env(L, 1).for_each_subst([&](name const & n, expr const & e) { - lua_pushvalue(L, 2); // push user-fun - push_name(L, n); - push_expr(L, e); - pcall(L, 2, 0, 0); - }); - return 0; -} - -static int mk_metavar_env(lua_State * L) { - if (lua_gettop(L) == 1) - return push_metavar_env(L, metavar_env(to_name_ext(L, 1))); - else - return push_metavar_env(L, metavar_env()); -} - -static int menv_copy(lua_State * L) { - return push_metavar_env(L, metavar_env(to_metavar_env(L, 1))); -} - -static int instantiate_metavars(lua_State * L) { - return push_expr(L, instantiate_metavars(to_expr(L, 1), to_metavar_env(L, 2))); -} - -static const struct luaL_Reg metavar_env_m[] = { - {"__gc", metavar_env_gc}, // never throws - {"mk_metavar", safe_function}, - {"get_timestamp", safe_function}, - {"get_context", safe_function}, - {"has_type", safe_function}, - {"get_type", safe_function}, - {"is_assigned", safe_function}, - {"assign", safe_function}, - {"get_subst", safe_function}, - {"get_justification", safe_function}, - {"get_subst_jst", safe_function}, - {"for_each_subst", safe_function}, - {"copy", safe_function}, - {0, 0} -}; - -void open_metavar_env(lua_State * L) { - luaL_newmetatable(L, metavar_env_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, metavar_env_m, 0); - - SET_GLOBAL_FUN(mk_metavar_env, "metavar_env"); - SET_GLOBAL_FUN(metavar_env_pred, "is_metavar_env"); - SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars"); -} -} diff --git a/src/bindings/lua/metavar_env.h b/src/bindings/lua/metavar_env.h deleted file mode 100644 index ad97d0076..000000000 --- a/src/bindings/lua/metavar_env.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(metavar_env) -void open_metavar_env(lua_State * L); -} diff --git a/src/bindings/lua/name.cpp b/src/bindings/lua/name.cpp deleted file mode 100644 index a54a9ef77..000000000 --- a/src/bindings/lua/name.cpp +++ /dev/null @@ -1,92 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/debug.h" -#include "util/name.h" -#include "util/sstream.h" -#include "bindings/lua/util.h" - -namespace lean { -DECL_UDATA(name) - -static int mk_name(lua_State * L) { - int nargs = lua_gettop(L); - name r; - for (int i = 1; i <= nargs; i++) { - switch (lua_type(L, i)) { - case LUA_TNIL: break; // skip - case LUA_TNUMBER: r = name(r, lua_tointeger(L, i)); break; - case LUA_TSTRING: r = name(r, lua_tostring(L, i)); break; - case LUA_TUSERDATA: r = r + to_name(L, i); break; - default: throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer"); - } - } - return push_name(L, r); -} - -name to_name_ext(lua_State * L, int idx) { - if (lua_isstring(L, idx)) { - return luaL_checkstring(L, idx); - } else if (lua_istable(L, idx)) { - name r; - int n = objlen(L, idx); - for (int i = 1; i <= n; i++) { - lua_rawgeti(L, idx, i); - switch (lua_type(L, -1)) { - case LUA_TNIL: break; // skip - case LUA_TNUMBER: r = name(r, lua_tointeger(L, -1)); break; - case LUA_TSTRING: r = name(r, lua_tostring(L, -1)); break; - case LUA_TUSERDATA: r = r + to_name(L, -1); break; - default: throw exception("invalid array arguments, elements must be a hierarchical name, string, or integer"); - } - lua_pop(L, 1); - } - return r; - } else { - return to_name(L, idx); - } -} - -static int name_tostring(lua_State * L) { - lua_pushstring(L, to_name(L, 1).to_string().c_str()); - return 1; -} - -static int name_eq(lua_State * L) { - lua_pushboolean(L, to_name(L, 1) == to_name(L, 2)); - return 1; -} - -static int name_lt(lua_State * L) { - lua_pushboolean(L, to_name(L, 1) < to_name(L, 2)); - return 1; -} - -static int name_hash(lua_State * L) { - lua_pushinteger(L, to_name(L, 1).hash()); - return 1; -} - -static const struct luaL_Reg name_m[] = { - {"__gc", name_gc}, // never throws - {"__tostring", safe_function}, - {"__eq", safe_function}, - {"__lt", safe_function}, - {"hash", safe_function}, - {0, 0} -}; - -void open_name(lua_State * L) { - luaL_newmetatable(L, name_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, name_m, 0); - - SET_GLOBAL_FUN(mk_name, "name"); - SET_GLOBAL_FUN(name_pred, "is_name"); -} -} diff --git a/src/bindings/lua/name.h b/src/bindings/lua/name.h deleted file mode 100644 index 9435cc4d4..000000000 --- a/src/bindings/lua/name.h +++ /dev/null @@ -1,13 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(name) -void open_name(lua_State * L); -name to_name_ext(lua_State * L, int idx); -} diff --git a/src/bindings/lua/numerics.cpp b/src/bindings/lua/numerics.cpp deleted file mode 100644 index bd9c7fa08..000000000 --- a/src/bindings/lua/numerics.cpp +++ /dev/null @@ -1,216 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/debug.h" -#include "util/sstream.h" -#include "util/numerics/mpz.h" -#include "util/numerics/mpq.h" -#include "bindings/lua/util.h" - -namespace lean { -DECL_UDATA(mpz) - -template -static mpz const & to_mpz(lua_State * L) { - static thread_local mpz arg; - switch (lua_type(L, idx)) { - case LUA_TNUMBER: arg = static_cast(lua_tointeger(L, idx)); return arg; - case LUA_TSTRING: arg = mpz(lua_tostring(L, idx)); return arg; - case LUA_TUSERDATA: return *static_cast(luaL_checkudata(L, idx, mpz_mt)); - default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz"); - } -} - -mpz to_mpz_ext(lua_State * L, int idx) { - switch (lua_type(L, idx)) { - case LUA_TNUMBER: return mpz(static_cast(lua_tointeger(L, idx))); - case LUA_TSTRING: return mpz(lua_tostring(L, idx)); - case LUA_TUSERDATA: return *static_cast(luaL_checkudata(L, idx, mpz_mt)); - default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz"); - } -} - -static int mpz_tostring(lua_State * L) { - mpz * n = static_cast(luaL_checkudata(L, 1, mpz_mt)); - std::ostringstream out; - out << *n; - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int mpz_eq(lua_State * L) { - lua_pushboolean(L, to_mpz<1>(L) == to_mpz<2>(L)); - return 1; -} - -static int mpz_lt(lua_State * L) { - lua_pushboolean(L, to_mpz<1>(L) < to_mpz<2>(L)); - return 1; -} - -static int mpz_add(lua_State * L) { - return push_mpz(L, to_mpz<1>(L) + to_mpz<2>(L)); -} - -static int mpz_sub(lua_State * L) { - return push_mpz(L, to_mpz<1>(L) - to_mpz<2>(L)); -} - -static int mpz_mul(lua_State * L) { - return push_mpz(L, to_mpz<1>(L) * to_mpz<2>(L)); -} - -static int mpz_div(lua_State * L) { - mpz const & arg2 = to_mpz<2>(L); - if (arg2 == 0) throw exception("division by zero"); - return push_mpz(L, to_mpz<1>(L) / arg2); -} - -static int mpz_umn(lua_State * L) { - return push_mpz(L, 0 - to_mpz<1>(L)); -} - -static int mpz_power(lua_State * L) { - int k = luaL_checkinteger(L, 2); - if (k < 0) throw exception("argument #2 must be positive"); - return push_mpz(L, pow(to_mpz<1>(L), k)); -} - -static int mk_mpz(lua_State * L) { - mpz const & arg = to_mpz<1>(L); - return push_mpz(L, arg); -} - -static const struct luaL_Reg mpz_m[] = { - {"__gc", mpz_gc}, // never throws - {"__tostring", safe_function}, - {"__eq", safe_function}, - {"__lt", safe_function}, - {"__add", safe_function}, - {"__sub", safe_function}, - {"__mul", safe_function}, - {"__div", safe_function}, - {"__pow", safe_function}, - {"__unm", safe_function}, - {0, 0} -}; - -void open_mpz(lua_State * L) { - luaL_newmetatable(L, mpz_mt); - setfuncs(L, mpz_m, 0); - - SET_GLOBAL_FUN(mk_mpz, "mpz"); - SET_GLOBAL_FUN(mpz_pred, "is_mpz"); -} - -DECL_UDATA(mpq) - -template -static mpq const & to_mpq(lua_State * L) { - static thread_local mpq arg; - switch (lua_type(L, idx)) { - case LUA_TNUMBER: arg = lua_tonumber(L, idx); return arg; - case LUA_TSTRING: arg = mpq(lua_tostring(L, idx)); return arg; - case LUA_TUSERDATA: - if (is_mpz(L, idx)) { - arg = mpq(to_mpz(L)); - return arg; - } else { - return *static_cast(luaL_checkudata(L, idx, mpq_mt)); - } - default: throw exception(sstream() << "arg #" << idx << " must be a number, string, mpz or mpq"); - } -} - -mpq to_mpq_ext(lua_State * L, int idx) { - switch (lua_type(L, idx)) { - case LUA_TNUMBER: return mpq(lua_tonumber(L, idx)); - case LUA_TSTRING: return mpq(lua_tostring(L, idx)); - case LUA_TUSERDATA: - if (is_mpz(L, idx)) { - return mpq(to_mpz<1>(L)); - } else { - return *static_cast(luaL_checkudata(L, idx, mpq_mt)); - } - default: throw exception(sstream() << "arg #" << idx << " must be a number, string, mpz or mpq"); - } -} - -static int mpq_tostring(lua_State * L) { - mpq * n = static_cast(luaL_checkudata(L, 1, mpq_mt)); - std::ostringstream out; - out << *n; - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int mpq_eq(lua_State * L) { - lua_pushboolean(L, to_mpq<1>(L) == to_mpq<2>(L)); - return 1; -} - -static int mpq_lt(lua_State * L) { - lua_pushboolean(L, to_mpq<1>(L) < to_mpq<2>(L)); - return 1; -} - -static int mpq_add(lua_State * L) { - return push_mpq(L, to_mpq<1>(L) + to_mpq<2>(L)); -} - -static int mpq_sub(lua_State * L) { - return push_mpq(L, to_mpq<1>(L) - to_mpq<2>(L)); -} - -static int mpq_mul(lua_State * L) { - return push_mpq(L, to_mpq<1>(L) * to_mpq<2>(L)); -} - -static int mpq_div(lua_State * L) { - mpq const & arg2 = to_mpq<2>(L); - if (arg2 == 0) throw exception("division by zero"); - return push_mpq(L, to_mpq<1>(L) / arg2); -} - -static int mpq_umn(lua_State * L) { - return push_mpq(L, 0 - to_mpq<1>(L)); -} - -static int mpq_power(lua_State * L) { - int k = luaL_checkinteger(L, 2); - if (k < 0) throw exception("argument #2 must be positive"); - return push_mpq(L, pow(to_mpq<1>(L), k)); -} - -static int mk_mpq(lua_State * L) { - mpq const & arg = to_mpq<1>(L); - return push_mpq(L, arg); -} - -static const struct luaL_Reg mpq_m[] = { - {"__gc", mpq_gc}, // never throws - {"__tostring", safe_function}, - {"__eq", safe_function}, - {"__lt", safe_function}, - {"__add", safe_function}, - {"__sub", safe_function}, - {"__mul", safe_function}, - {"__div", safe_function}, - {"__pow", safe_function}, - {"__unm", safe_function}, - {0, 0} -}; - -void open_mpq(lua_State * L) { - luaL_newmetatable(L, mpq_mt); - setfuncs(L, mpq_m, 0); - - SET_GLOBAL_FUN(mk_mpq, "mpq"); - SET_GLOBAL_FUN(mpq_pred, "is_mpq"); -} -} diff --git a/src/bindings/lua/object.cpp b/src/bindings/lua/object.cpp deleted file mode 100644 index 4c6d4bb33..000000000 --- a/src/bindings/lua/object.cpp +++ /dev/null @@ -1,154 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/sexpr/options.h" -#include "kernel/object.h" -#include "kernel/formatter.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/options.h" -#include "bindings/lua/level.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/formatter.h" - -namespace lean { -DECL_UDATA(object) - -object & to_nonnull_object(lua_State * L, int idx) { - object & r = to_object(L, idx); - if (!r) - throw exception("non-null kernel object expected"); - return r; -} - -static int object_is_null(lua_State * L) { - lua_pushboolean(L, !to_object(L, 1)); - return 1; -} - -static int object_keyword(lua_State * L) { - lua_pushstring(L, to_nonnull_object(L, 1).keyword()); - return 1; -} - -static int object_has_name(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).has_name()); - return 1; -} - -static int object_get_name(lua_State * L) { - object const & o = to_nonnull_object(L, 1); - if (!o.has_name()) - throw exception("kernel object does not have a name"); - return push_name(L, o.get_name()); -} - -static int object_has_type(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).has_type()); - return 1; -} - -static int object_get_type(lua_State * L) { - object const & o = to_nonnull_object(L, 1); - if (!o.has_type()) - throw exception("kernel object does not have a type"); - return push_expr(L, o.get_type()); -} - -static int object_has_cnstr_level(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).has_cnstr_level()); - return 1; -} - -static int object_get_cnstr_level(lua_State * L) { - object const & o = to_nonnull_object(L, 1); - if (!o.has_cnstr_level()) - throw exception("kernel object does not have a constraint level"); - return push_level(L, o.get_cnstr_level()); -} - -static int object_get_value(lua_State * L) { - object const & o = to_nonnull_object(L, 1); - if (!o.is_definition() && !o.is_builtin()) - throw exception("kernel object is not a definition/theorem/builtin"); - return push_expr(L, o.get_value()); -} - -static int object_get_weight(lua_State * L) { - object const & o = to_nonnull_object(L, 1); - if (!o.is_definition()) - throw exception("kernel object is not a definition"); - lua_pushinteger(L, o.get_weight()); - return 1; -} - -#define OBJECT_PRED(P) \ -static int object_ ## P(lua_State * L) { \ - lua_pushboolean(L, to_nonnull_object(L, 1).P()); \ - return 1; \ -} - -OBJECT_PRED(is_definition) -OBJECT_PRED(is_opaque) -OBJECT_PRED(is_axiom) -OBJECT_PRED(is_theorem) -OBJECT_PRED(is_var_decl) -OBJECT_PRED(is_builtin) -OBJECT_PRED(is_builtin_set) - -static int object_in_builtin_set(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).in_builtin_set(to_expr(L, 2))); - return 1; -} - -static int object_tostring(lua_State * L) { - std::ostringstream out; - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - object & obj = to_object(L, 1); - if (obj) - out << mk_pair(fmt(to_object(L, 1), opts), opts); - else - out << ""; - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static const struct luaL_Reg object_m[] = { - {"__gc", object_gc}, // never throws - {"__tostring", safe_function}, - {"is_null", safe_function}, - {"keyword", safe_function}, - {"has_name", safe_function}, - {"get_name", safe_function}, - {"has_type", safe_function}, - {"get_type", safe_function}, - {"has_cnstr_level", safe_function}, - {"get_cnstr_level", safe_function}, - {"is_definition", safe_function}, - {"is_opaque", safe_function}, - {"get_value", safe_function}, - {"get_weight", safe_function}, - {"is_axiom", safe_function}, - {"is_theorem", safe_function}, - {"is_var_decl", safe_function}, - {"is_builtin", safe_function}, - {"is_builtin_set", safe_function}, - {"in_builtin_set", safe_function}, - {0, 0} -}; - -void open_object(lua_State * L) { - luaL_newmetatable(L, object_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, object_m, 0); - - SET_GLOBAL_FUN(object_pred, "is_kernel_object"); -} -} diff --git a/src/bindings/lua/object.h b/src/bindings/lua/object.h deleted file mode 100644 index ac7c7c62e..000000000 --- a/src/bindings/lua/object.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(object) -void open_object(lua_State * L); -} diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp deleted file mode 100644 index d4bcd2a1d..000000000 --- a/src/bindings/lua/options.cpp +++ /dev/null @@ -1,242 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/debug.h" -#include "util/name.h" -#include "util/sstream.h" -#include "util/sexpr/options.h" -#include "util/sexpr/option_declarations.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/io_state.h" - -namespace lean { -DECL_UDATA(options) - -static int mk_options(lua_State * L) { - options r; - int nargs = lua_gettop(L); - if (nargs % 2 != 0) - throw exception("options expects an even number of arguments"); - for (int i = 1; i < nargs; i+=2) { - name k = to_name_ext(L, i); - auto it = get_option_declarations().find(k); - if (it == get_option_declarations().end()) { - throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); - } else { - option_declaration const & d = it->second; - switch (d.kind()) { - case BoolOption: r = r.update(k, static_cast(lua_toboolean(L, i+1))); break; - case IntOption: r = r.update(k, static_cast(lua_tointeger(L, i+1))); break; - case UnsignedOption: r = r.update(k, static_cast(lua_tointeger(L, i+1))); break; - case DoubleOption: r = r.update(k, static_cast(lua_tonumber(L, i+1))); break; - case StringOption: r = r.update(k, lua_tostring(L, i+1)); break; - default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'"); - } - } - } - return push_options(L, r); -} - -static int options_tostring(lua_State * L) { - std::ostringstream out; - out << to_options(L, 1); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int options_size(lua_State * L) { - lua_pushinteger(L, to_options(L, 1).size()); - return 1; -} - -static int options_contains(lua_State * L) { - lua_pushboolean(L, to_options(L, 1).contains(to_name_ext(L, 2))); - return 1; -} - -static int options_empty(lua_State * L) { - lua_pushboolean(L, to_options(L, 1).empty()); - return 1; -} - -static int options_get_bool(lua_State * L) { - int nargs = lua_gettop(L); - bool defval = nargs < 3 ? false : lua_toboolean(L, 3); - lua_pushboolean(L, to_options(L, 1).get_bool(to_name_ext(L, 2), defval)); - return 1; -} - -static int options_get_int(lua_State * L) { - int nargs = lua_gettop(L); - int defval = nargs < 3 ? 0 : lua_tointeger(L, 3); - lua_pushinteger(L, to_options(L, 1).get_int(to_name_ext(L, 2), defval)); - return 1; -} - -static int options_get_unsigned(lua_State * L) { - int nargs = lua_gettop(L); - unsigned defval = nargs < 3 ? 0 : lua_tointeger(L, 3); - lua_pushnumber(L, to_options(L, 1).get_unsigned(to_name_ext(L, 2), defval)); - return 1; -} - -static int options_get_double(lua_State * L) { - int nargs = lua_gettop(L); - double defval = nargs < 3 ? 0.0 : lua_tonumber(L, 3); - lua_pushnumber(L, to_options(L, 1).get_double(to_name_ext(L, 2), defval)); - return 1; -} - -static int options_get_string(lua_State * L) { - int nargs = lua_gettop(L); - char const * defval = nargs < 3 ? "" : lua_tostring(L, 3); - lua_pushstring(L, to_options(L, 1).get_string(to_name_ext(L, 2), defval)); - return 1; -} - -static int options_update_bool(lua_State * L) { - return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), static_cast(lua_toboolean(L, 3)))); -} - -static int options_update_int(lua_State * L) { - return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), static_cast(lua_tointeger(L, 3)))); -} - -static int options_update_unsigned(lua_State * L) { - return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), static_cast(lua_tointeger(L, 3)))); -} - -static int options_update_double(lua_State * L) { - return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), lua_tonumber(L, 3))); -} - -static int options_update_string(lua_State * L) { - return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), lua_tostring(L, 3))); -} - -static int options_get(lua_State * L) { - name k = to_name_ext(L, 2); - auto it = get_option_declarations().find(k); - if (it == get_option_declarations().end()) { - throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); - } else { - option_declaration const & d = it->second; - switch (d.kind()) { - case BoolOption: return options_get_bool(L); - case IntOption: return options_get_int(L); - case UnsignedOption: return options_get_unsigned(L); - case DoubleOption: return options_get_double(L); - case StringOption: return options_get_string(L); - default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'"); - } - } -} - -static int options_update(lua_State * L) { - name k = to_name_ext(L, 2); - auto it = get_option_declarations().find(k); - if (it == get_option_declarations().end()) { - throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); - } else { - option_declaration const & d = it->second; - switch (d.kind()) { - case BoolOption: return options_update_bool(L); - case IntOption: return options_update_int(L); - case UnsignedOption: return options_update_unsigned(L); - case DoubleOption: return options_update_double(L); - case StringOption: return options_update_string(L); - default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'"); - } - } -} - -static char g_options_key; - -options get_global_options(lua_State * L) { - io_state * S = get_io_state(L); - if (S != nullptr) { - return S->get_options(); - } else { - lua_pushlightuserdata(L, static_cast(&g_options_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - options r; - if (is_options(L, -1)) - r = to_options(L, -1); - lua_pop(L, 1); - return r; - } -} - -void set_global_options(lua_State * L, options const & o) { - io_state * S = get_io_state(L); - if (S != nullptr) { - S->set_options(o); - } else { - lua_pushlightuserdata(L, static_cast(&g_options_key)); - push_options(L, o); - lua_settable(L, LUA_REGISTRYINDEX); - } -} - -static int _get_global_options(lua_State * L) { - return push_options(L, get_global_options(L)); -} - -static int _set_global_options(lua_State * L) { - options o = to_options(L, 1); - set_global_options(L, o); - return 0; -} - -static int _set_global_option(lua_State * L) { - options o = get_global_options(L); - push_options(L, o); - lua_insert(L, 1); - options_update(L); - o = to_options(L, -1); - set_global_options(L, o); - return 0; -} - -static const struct luaL_Reg options_m[] = { - {"__gc", options_gc}, // never throws - {"__tostring", safe_function}, - {"__len", safe_function }, - {"contains", safe_function}, - {"size", safe_function}, - {"empty", safe_function}, - {"get", safe_function}, - {"update", safe_function}, - // low-level API - {"get_bool", safe_function}, - {"get_int", safe_function}, - {"get_unsigned", safe_function}, - {"get_double", safe_function}, - {"get_string", safe_function}, - {"update_bool", safe_function}, - {"update_int", safe_function}, - {"update_unsigned", safe_function}, - {"update_double", safe_function}, - {"update_string", safe_function}, - {0, 0} -}; - -void open_options(lua_State * L) { - luaL_newmetatable(L, options_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, options_m, 0); - - SET_GLOBAL_FUN(mk_options, "options"); - SET_GLOBAL_FUN(options_pred, "is_options"); - SET_GLOBAL_FUN(_get_global_options, "get_options"); - SET_GLOBAL_FUN(_set_global_options, "set_options"); - SET_GLOBAL_FUN(_set_global_option, "set_option"); -} -} diff --git a/src/bindings/lua/options.h b/src/bindings/lua/options.h deleted file mode 100644 index 90db30373..000000000 --- a/src/bindings/lua/options.h +++ /dev/null @@ -1,25 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(options) -void open_options(lua_State * L); -/** - \brief Return the set of options associated with the given Lua State. - This procedure checks for options at: - 1- Lean state object associated with \c L - 2- Lua Registry associated with \c L -*/ -options get_global_options(lua_State * L); -/** - \brief Update the set of options associated with the given Lua State. - If \c L is associated with a Lean state object \c S, then we update the options of \c S. - Otherwise, we update the registry of \c L. -*/ -void set_global_options(lua_State * L, options const & o); -} diff --git a/src/bindings/lua/proof_builder.cpp b/src/bindings/lua/proof_builder.cpp deleted file mode 100644 index c97d8ae2c..000000000 --- a/src/bindings/lua/proof_builder.cpp +++ /dev/null @@ -1,124 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "library/tactic/proof_builder.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/metavar_env.h" -#include "bindings/lua/lref.h" - -namespace lean { -DECL_UDATA(proof_map) - -static int mk_proof_map(lua_State * L) { - return push_proof_map(L, proof_map()); -} - -static int proof_map_len(lua_State * L) { - lua_pushinteger(L, to_proof_map(L, 1).size()); - return 1; -} - -static int proof_map_find(lua_State * L) { - return push_expr(L, find(to_proof_map(L, 1), to_name_ext(L, 2))); -} - -static int proof_map_insert(lua_State * L) { - to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3)); - return 0; -} - -static int proof_map_erase(lua_State * L) { - to_proof_map(L, 1).erase(to_name_ext(L, 2)); - return 0; -} - -static const struct luaL_Reg proof_map_m[] = { - {"__gc", proof_map_gc}, // never throws - {"__len", safe_function}, - {"size", safe_function}, - {"find", safe_function}, - {"insert", safe_function}, - {"erase", safe_function}, - {0, 0} -}; - -DECL_UDATA(assignment); - -static int mk_assignment(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - return push_assignment(L, assignment(metavar_env())); - else - return push_assignment(L, assignment(to_metavar_env(L, 1))); -} - -static int assignment_call(lua_State * L) { - return push_expr(L, to_assignment(L, 1)(to_name_ext(L, 2))); -} - -static const struct luaL_Reg assignment_m[] = { - {"__gc", assignment_gc}, // never throws - {"__call", safe_function}, - {0, 0} -}; - -DECL_UDATA(proof_builder); - -static int mk_proof_builder(lua_State * L) { - luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun - lref ref(L, 1); - return push_proof_builder(L, - mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { - ref.push(); // push user-fun on the stack - push_proof_map(L, m); - push_assignment(L, a); - pcall(L, 2, 1, 0); - expr r = to_expr(L, -1); - lua_pop(L, 1); - return r; - })); -} - -static int proof_builder_call(lua_State * L) { - return push_expr(L, to_proof_builder(L, 1)(to_proof_map(L, 2), to_assignment(L, 3))); -} - -static const struct luaL_Reg proof_builder_m[] = { - {"__gc", proof_builder_gc}, // never throws - {"__call", safe_function}, - {0, 0} -}; - -void open_proof_builder(lua_State * L) { - luaL_newmetatable(L, proof_map_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, proof_map_m, 0); - - SET_GLOBAL_FUN(proof_map_pred, "is_proof_map"); - SET_GLOBAL_FUN(mk_proof_map, "proof_map"); - - luaL_newmetatable(L, assignment_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, assignment_m, 0); - - SET_GLOBAL_FUN(assignment_pred, "is_assignment"); - SET_GLOBAL_FUN(mk_assignment, "assignment"); - - luaL_newmetatable(L, proof_builder_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, proof_builder_m, 0); - - SET_GLOBAL_FUN(proof_builder_pred, "is_proof_builder"); - SET_GLOBAL_FUN(mk_proof_builder, "proof_builder"); -} -} diff --git a/src/bindings/lua/proof_builder.h b/src/bindings/lua/proof_builder.h deleted file mode 100644 index f5c08c7f5..000000000 --- a/src/bindings/lua/proof_builder.h +++ /dev/null @@ -1,15 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "library/tactic/proof_builder.h" -namespace lean { -UDATA_DEFS_CORE(proof_map) -UDATA_DEFS(assignment) -UDATA_DEFS(proof_builder) -void open_proof_builder(lua_State * L); -} diff --git a/src/bindings/lua/proof_state.cpp b/src/bindings/lua/proof_state.cpp deleted file mode 100644 index e877aa328..000000000 --- a/src/bindings/lua/proof_state.cpp +++ /dev/null @@ -1,218 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "library/tactic/proof_state.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/options.h" -#include "bindings/lua/formatter.h" -#include "bindings/lua/format.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/context.h" -#include "bindings/lua/environment.h" -#include "bindings/lua/metavar_env.h" -#include "bindings/lua/goal.h" -#include "bindings/lua/proof_builder.h" -#include "bindings/lua/cex_builder.h" - -namespace lean { -DECL_UDATA(goals) - -static int mk_goals(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_goals(L, goals()); - } else if (nargs == 2) { - return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), goals())); - } else if (nargs == 3) { - return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), to_goals(L, 3))); - } else { - throw exception("goals functions expects 0 (empty list), 2 (name & goal for singleton goal list), or 3 (name & goal & goal list) arguments"); - } -} - -static int goals_is_nil(lua_State * L) { - lua_pushboolean(L, !to_goals(L, 1)); - return 1; -} - -static int goals_head(lua_State * L) { - goals const & hs = to_goals(L, 1); - if (!hs) - throw exception("head method expects a non-empty goal list"); - push_name(L, head(hs).first); - push_goal(L, head(hs).second); - return 2; -} - -static int goals_tail(lua_State * L) { - goals const & hs = to_goals(L, 1); - if (!hs) - throw exception("tail method expects a non-empty goal list"); - push_goals(L, tail(hs)); - return 1; -} - -static int goals_next(lua_State * L) { - goals & hs = to_goals(L, lua_upvalueindex(1)); - if (hs) { - push_goals(L, tail(hs)); - lua_replace(L, lua_upvalueindex(1)); - push_name(L, head(hs).first); - push_goal(L, head(hs).second); - return 2; - } else { - lua_pushnil(L); - return 1; - } -} - -static int goals_items(lua_State * L) { - goals & hs = to_goals(L, 1); - push_goals(L, hs); // upvalue(1): goals - lua_pushcclosure(L, &safe_function, 1); // create closure with 1 upvalue - return 1; -} - -static int goals_len(lua_State * L) { - lua_pushinteger(L, length(to_goals(L, 1))); - return 1; -} - -static const struct luaL_Reg goals_m[] = { - {"__gc", goals_gc}, // never throws - {"__len", safe_function}, - {"size", safe_function}, - {"pairs", safe_function}, - {"is_nil", safe_function}, - {"empty", safe_function}, - {"head", safe_function}, - {"tail", safe_function}, - {0, 0} -}; - -DECL_UDATA(proof_state) - -static int mk_proof_state(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_proof_state(L, proof_state()); - } else if (nargs == 4) { - return push_proof_state(L, proof_state(to_goals(L, 1), to_metavar_env(L, 2), to_proof_builder(L, 3), to_cex_builder(L, 4))); - } else if (nargs == 3) { - return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3))); - } else { - throw exception("proof_state expectes 0, 3, or 4 arguments"); - } -} - -static int to_proof_state(lua_State * L) { - return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_expr(L, 3))); -} - -static int proof_state_tostring(lua_State * L) { - std::ostringstream out; - proof_state & s = to_proof_state(L, 1); - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(s.pp(fmt, opts), opts); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static int proof_state_get_precision(lua_State * L) { - lua_pushinteger(L, static_cast(to_proof_state(L, 1).get_precision())); - return 1; -} - -static int proof_state_get_goals(lua_State * L) { - return push_goals(L, to_proof_state(L, 1).get_goals()); -} - -static int proof_state_get_menv(lua_State * L) { - return push_metavar_env(L, to_proof_state(L, 1).get_menv()); -} - -static int proof_state_get_proof_builder(lua_State * L) { - return push_proof_builder(L, to_proof_state(L, 1).get_proof_builder()); -} - -static int proof_state_get_cex_builder(lua_State * L) { - return push_cex_builder(L, to_proof_state(L, 1).get_cex_builder()); -} - -static int proof_state_is_proof_final_state(lua_State * L) { - lua_pushboolean(L, to_proof_state(L, 1).is_proof_final_state()); - return 1; -} - -static int proof_state_is_cex_final_state(lua_State * L) { - lua_pushboolean(L, to_proof_state(L, 1).is_cex_final_state()); - return 1; -} - -static int proof_state_pp(lua_State * L) { - int nargs = lua_gettop(L); - proof_state & s = to_proof_state(L, 1); - if (nargs == 1) { - return push_format(L, s.pp(get_global_formatter(L), get_global_options(L))); - } else if (nargs == 2) { - if (is_formatter(L, 2)) - return push_format(L, s.pp(to_formatter(L, 2), get_global_options(L))); - else - return push_format(L, s.pp(get_global_formatter(L), to_options(L, 2))); - } else { - return push_format(L, s.pp(to_formatter(L, 2), to_options(L, 3))); - } -} - -static const struct luaL_Reg proof_state_m[] = { - {"__gc", proof_state_gc}, // never throws - {"__tostring", safe_function}, - {"pp", safe_function}, - {"get_precision", safe_function}, - {"get_goals", safe_function}, - {"get_menv", safe_function}, - {"get_proof_builder", safe_function}, - {"get_cex_builder", safe_function}, - {"precision", safe_function}, - {"goals", safe_function}, - {"menv", safe_function}, - {"proof_builder", safe_function}, - {"cex_builder", safe_function}, - {"is_proof_final_state", safe_function}, - {"is_cex_final_state", safe_function}, - {0, 0} -}; - -void open_proof_state(lua_State * L) { - luaL_newmetatable(L, goals_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, goals_m, 0); - - SET_GLOBAL_FUN(goals_pred, "is_goals"); - SET_GLOBAL_FUN(mk_goals, "goals"); - - luaL_newmetatable(L, proof_state_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, proof_state_m, 0); - - SET_GLOBAL_FUN(proof_state_pred, "is_proof_state"); - SET_GLOBAL_FUN(mk_proof_state, "proof_state"); - SET_GLOBAL_FUN(to_proof_state, "to_proof_state"); - - lua_newtable(L); - SET_ENUM("Precise", precision::Precise); - SET_ENUM("Over", precision::Over); - SET_ENUM("Under", precision::Under); - SET_ENUM("UnderOver", precision::UnderOver); - lua_setglobal(L, "precision"); -} -} diff --git a/src/bindings/lua/proof_state.h b/src/bindings/lua/proof_state.h deleted file mode 100644 index 725d0cbd8..000000000 --- a/src/bindings/lua/proof_state.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "library/tactic/proof_state.h" -namespace lean { -UDATA_DEFS_CORE(goals) -UDATA_DEFS(proof_state) -void open_proof_state(lua_State * L); -} diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp deleted file mode 100644 index 6d73cf14b..000000000 --- a/src/bindings/lua/sexpr.cpp +++ /dev/null @@ -1,232 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/debug.h" -#include "util/sexpr/sexpr.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/numerics.h" - -namespace lean { -DECL_UDATA(sexpr) - -static int sexpr_tostring(lua_State * L) { - std::ostringstream out; - out << to_sexpr(L, 1); - lua_pushstring(L, out.str().c_str()); - return 1; -} - -static sexpr to_sexpr_elem(lua_State * L, int idx) { - if (lua_isnil(L, idx)) { - return sexpr(); - } else if (lua_isboolean(L, idx)) { - return sexpr(static_cast(lua_toboolean(L, idx))); - } else if (lua_isnumber(L, idx)) { - // Remark: we convert to integer by default - return sexpr(static_cast(lua_tointeger(L, idx))); - } else if (is_name(L, idx)) { - return sexpr(to_name(L, idx)); - } else if (is_sexpr(L, idx)) { - return *static_cast(lua_touserdata(L, idx)); - } else if (is_mpz(L, idx)) { - return sexpr(to_mpz(L, idx)); - } else if (is_mpq(L, idx)) { - return sexpr(to_mpq(L, idx)); - } else { - return sexpr(lua_tostring(L, idx)); - } -} - -static int mk_sexpr(lua_State * L) { - sexpr r; - int nargs = lua_gettop(L); - if (nargs == 0) { - r = sexpr(); - } else { - int i = nargs; - r = to_sexpr_elem(L, i); - i--; - for (; i >= 1; i--) { - r = sexpr(to_sexpr_elem(L, i), r); - } - } - return push_sexpr(L, r); -} - -static int sexpr_eq(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); return 1; } -static int sexpr_lt(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); return 1; } - -#define SEXPR_PRED(P) \ -static int sexpr_ ## P(lua_State * L) { \ - lua_pushboolean(L, P(to_sexpr(L, 1))); \ - return 1; \ -} - -SEXPR_PRED(is_nil) -SEXPR_PRED(is_cons) -SEXPR_PRED(is_list) -SEXPR_PRED(is_atom) -SEXPR_PRED(is_string) -SEXPR_PRED(is_bool) -SEXPR_PRED(is_int) -SEXPR_PRED(is_double) -SEXPR_PRED(is_name) -SEXPR_PRED(is_mpz) -SEXPR_PRED(is_mpq) - -static int sexpr_length(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_list(e)) - throw exception("s-expression is not a list"); - lua_pushinteger(L, length(e)); - return 1; -} - -static int sexpr_head(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_cons(e)) - throw exception("s-expression is not a cons cell"); - return push_sexpr(L, head(e)); -} - -static int sexpr_tail(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_cons(e)) - throw exception("s-expression is not a cons cell"); - return push_sexpr(L, tail(e)); -} - -static int sexpr_to_bool(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_bool(e)) - throw exception("s-expression is not a Boolean"); - lua_pushboolean(L, to_bool(e)); - return 1; -} - -static int sexpr_to_string(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_string(e)) - throw exception("s-expression is not a string"); - lua_pushstring(L, to_string(e).c_str()); - return 1; -} - -static int sexpr_to_int(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_int(e)) - throw exception("s-expression is not an integer"); - lua_pushinteger(L, to_int(e)); - return 1; -} - -static int sexpr_to_double(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_double(e)) - throw exception("s-expression is not a double"); - lua_pushnumber(L, to_double(e)); - return 1; -} - -static int sexpr_to_name(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_name(e)) - throw exception("s-expression is not a name"); - return push_name(L, to_name(e)); -} - -static int sexpr_to_mpz(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_mpz(e)) - throw exception("s-expression is not a multi-precision integer"); - return push_mpz(L, to_mpz(e)); -} - -static int sexpr_to_mpq(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - if (!is_mpq(e)) - throw exception("s-expression is not a multi-precision rational"); - return push_mpq(L, to_mpq(e)); -} - -static int sexpr_get_kind(lua_State * L) { - lua_pushinteger(L, static_cast(to_sexpr(L, 1).kind())); - return 1; -} - -static int sexpr_fields(lua_State * L) { - sexpr const & e = to_sexpr(L, 1); - switch (e.kind()) { - case sexpr_kind::Nil: return 0; - case sexpr_kind::String: return sexpr_to_string(L); - case sexpr_kind::Bool: return sexpr_to_bool(L); - case sexpr_kind::Int: return sexpr_to_int(L); - case sexpr_kind::Double: return sexpr_to_double(L); - case sexpr_kind::Name: return sexpr_to_name(L); - case sexpr_kind::MPZ: return sexpr_to_mpz(L); - case sexpr_kind::MPQ: return sexpr_to_mpq(L); - case sexpr_kind::Cons: sexpr_head(L); sexpr_tail(L); return 2; - } - lean_unreachable(); // LCOV_EXCL_LINE - return 0; // LCOV_EXCL_LINE -} - -static const struct luaL_Reg sexpr_m[] = { - {"__gc", sexpr_gc}, // never throws - {"__tostring", safe_function}, - {"__eq", safe_function}, - {"__lt", safe_function}, - {"kind", safe_function}, - {"is_nil", safe_function}, - {"is_cons", safe_function}, - {"is_list", safe_function}, - {"is_atom", safe_function}, - {"is_string", safe_function}, - {"is_bool", safe_function}, - {"is_int", safe_function}, - {"is_double", safe_function}, - {"is_name", safe_function}, - {"is_mpz", safe_function}, - {"is_mpq", safe_function}, - {"head", safe_function}, - {"tail", safe_function}, - {"length", safe_function}, - {"to_bool", safe_function}, - {"to_string", safe_function}, - {"to_int", safe_function}, - {"to_double", safe_function}, - {"to_name", safe_function}, - {"to_mpz", safe_function}, - {"to_mpq", safe_function}, - {"fields", safe_function}, - {0, 0} -}; - -void open_sexpr(lua_State * L) { - luaL_newmetatable(L, sexpr_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, sexpr_m, 0); - - SET_GLOBAL_FUN(mk_sexpr, "sexpr"); - SET_GLOBAL_FUN(sexpr_pred, "is_sexpr"); - - lua_newtable(L); - SET_ENUM("Nil", sexpr_kind::Nil); - SET_ENUM("String", sexpr_kind::String); - SET_ENUM("Bool", sexpr_kind::Bool); - SET_ENUM("Int", sexpr_kind::Int); - SET_ENUM("Double", sexpr_kind::Double); - SET_ENUM("Name", sexpr_kind::Name); - SET_ENUM("MPZ", sexpr_kind::MPZ); - SET_ENUM("MPQ", sexpr_kind::MPQ); - SET_ENUM("Cons", sexpr_kind::Cons); - lua_setglobal(L, "sexpr_kind"); -} -} diff --git a/src/bindings/lua/sexpr.h b/src/bindings/lua/sexpr.h deleted file mode 100644 index e7aedc349..000000000 --- a/src/bindings/lua/sexpr.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -UDATA_DEFS(sexpr) -void open_sexpr(lua_State * L); -} diff --git a/src/bindings/lua/splay_map.h b/src/bindings/lua/splay_map.h deleted file mode 100644 index 7fb5b69a3..000000000 --- a/src/bindings/lua/splay_map.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -void open_splay_map(lua_State * L); -} diff --git a/src/bindings/lua/type_inferer.cpp b/src/bindings/lua/type_inferer.cpp deleted file mode 100644 index f79c793e4..000000000 --- a/src/bindings/lua/type_inferer.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "library/type_inferer.h" -#include "bindings/lua/util.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/context.h" -#include "bindings/lua/environment.h" - -namespace lean { -constexpr char const * type_inferer_mt = "type_inferer"; -type_inferer & to_type_inferer(lua_State * L, int i) { return *static_cast(luaL_checkudata(L, i, type_inferer_mt)); } -DECL_PRED(type_inferer) -DECL_GC(type_inferer) - -static int type_inferer_call(lua_State * L) { - int nargs = lua_gettop(L); - type_inferer & inferer = to_type_inferer(L, 1); - if (nargs == 2) - return push_expr(L, inferer(to_nonnull_expr(L, 2))); - else - return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3))); -} - -static int type_inferer_clear(lua_State * L) { - to_type_inferer(L, 1).clear(); - return 0; -} - -static int mk_type_inferer(lua_State * L) { - void * mem = lua_newuserdata(L, sizeof(type_inferer)); - new (mem) type_inferer(to_environment(L, 1)); - luaL_getmetatable(L, type_inferer_mt); - lua_setmetatable(L, -2); - return 1; -} - -static const struct luaL_Reg type_inferer_m[] = { - {"__gc", type_inferer_gc}, // never throws - {"__call", safe_function}, - {"clear", safe_function}, - {0, 0} -}; - -void open_type_inferer(lua_State * L) { - luaL_newmetatable(L, type_inferer_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, type_inferer_m, 0); - - SET_GLOBAL_FUN(mk_type_inferer, "type_inferer"); - SET_GLOBAL_FUN(type_inferer_pred, "is_type_inferer"); -} -} diff --git a/src/bindings/lua/type_inferer.h b/src/bindings/lua/type_inferer.h deleted file mode 100644 index e02d905da..000000000 --- a/src/bindings/lua/type_inferer.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -void open_type_inferer(lua_State * L); -} diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 992c0ac3f..fa57aa39a 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -178,6 +178,7 @@ bool value::operator<(value const & other) const { format value::pp() const { return format(get_name()); } format value::pp(bool unicode, bool) const { return unicode ? format(get_unicode_name()) : pp(); } unsigned value::hash() const { return get_name().hash(); } +int value::push_lua(lua_State * L) const { lean_assert(L); return 0; } expr_value::expr_value(value & v): expr_cell(expr_kind::Value, v.hash(), false), m_val(v) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index d64a21b40..d147efd4a 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/lua.h" #include "util/rc.h" #include "util/name.h" #include "util/hash.h" @@ -267,6 +268,7 @@ public: virtual void display(std::ostream & out) const; virtual format pp() const; virtual format pp(bool unicode, bool coercion) const; + virtual int push_lua(lua_State * L) const; virtual unsigned hash() const; }; /** \brief Semantic attachments */ diff --git a/src/kernel/threadsafe_environment.h b/src/kernel/threadsafe_environment.h index 65ce109ec..19d2aa9fc 100644 --- a/src/kernel/threadsafe_environment.h +++ b/src/kernel/threadsafe_environment.h @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#pragma once #include "util/shared_mutex.h" #include "kernel/environment.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index b06d5554c..38c37799e 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ -add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp - context_to_lambda.cpp io_state.cpp update_expr.cpp type_inferer.cpp - placeholder.cpp expr_lt.cpp script_evaluator.cpp) +add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp + max_sharing.cpp context_to_lambda.cpp io_state.cpp update_expr.cpp + type_inferer.cpp placeholder.cpp expr_lt.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index d2bea96f6..f227e02bf 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" +#include "library/kernel_bindings.h" #include "library/arith/int.h" #include "library/arith/nat.h" #include "library/arith/num_type.h" @@ -45,6 +46,7 @@ public: return format(m_val); } virtual unsigned hash() const { return m_val.hash(); } + virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); } mpz const & get_num() const { return m_val; } }; @@ -174,4 +176,13 @@ void import_int(environment & env) { env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); } + +static int mk_int_value(lua_State * L) { + return push_expr(L, mk_int_value(to_mpz_ext(L, 1))); +} + +void open_int(lua_State * L) { + SET_GLOBAL_FUN(mk_int_value, "mk_int_value"); + SET_GLOBAL_FUN(mk_int_value, "iVal"); +} } diff --git a/src/library/arith/int.h b/src/library/arith/int.h index 0e4ae37f6..a96c1f4a3 100644 --- a/src/library/arith/int.h +++ b/src/library/arith/int.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lua.h" #include "util/numerics/mpz.h" #include "kernel/expr.h" #include "kernel/builtin.h" @@ -90,4 +91,6 @@ class environment; It will also load the natural number library. */ void import_int(environment & env); + +void open_int(lua_State * L); } diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index a7c1a8581..bdfba2e58 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" +#include "library/kernel_bindings.h" #include "library/arith/nat.h" #include "library/arith/num_type.h" @@ -39,6 +40,7 @@ public: virtual format pp() const { return format(m_val); } virtual format pp(bool, bool) const { return pp(); } virtual unsigned hash() const { return m_val.hash(); } + virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); } mpz const & get_num() const { return m_val; } }; @@ -126,4 +128,16 @@ void import_nat(environment & env) { env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); } + +static int mk_nat_value(lua_State * L) { + mpz v = to_mpz_ext(L, 1); + if (v < 0) + throw exception("arg #1 must be non-negative"); + return push_expr(L, mk_nat_value(v)); +} + +void open_nat(lua_State * L) { + SET_GLOBAL_FUN(mk_nat_value, "mk_nat_value"); + SET_GLOBAL_FUN(mk_nat_value, "nVal"); +} } diff --git a/src/library/arith/nat.h b/src/library/arith/nat.h index 19ecc3b32..bd49ce821 100644 --- a/src/library/arith/nat.h +++ b/src/library/arith/nat.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lua.h" #include "kernel/expr.h" #include "kernel/builtin.h" #include "util/numerics/mpz.h" @@ -55,4 +56,6 @@ inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(N class environment; /** \brief Import Natural number library in the given environment (if it has not been imported already). */ void import_nat(environment & env); + +void open_nat(lua_State * L); } diff --git a/src/bindings/lua/numerics.h b/src/library/arith/open_module.h similarity index 50% rename from src/bindings/lua/numerics.h rename to src/library/arith/open_module.h index 36d3fe8ea..a68879fe3 100644 --- a/src/bindings/lua/numerics.h +++ b/src/library/arith/open_module.h @@ -5,13 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include -namespace lean { -UDATA_DEFS(mpz) -mpz to_mpz_ext(lua_State * L, int idx); -void open_mpz(lua_State * L); +#include "library/arith/nat.h" +#include "library/arith/int.h" +#include "library/arith/real.h" -UDATA_DEFS(mpq) -mpq to_mpq_ext(lua_State * L, int idx); -void open_mpq(lua_State * L); +namespace lean { +inline void open_arith_module(lua_State * L) { + open_nat(L); + open_int(L); + open_real(L); +} } diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index c0d635f08..4e21e780f 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" +#include "library/kernel_bindings.h" #include "library/arith/real.h" #include "library/arith/int.h" #include "library/arith/nat.h" @@ -48,6 +49,7 @@ public: return format(m_val); } virtual unsigned hash() const { return m_val.hash(); } + virtual int push_lua(lua_State * L) const { return push_mpq(L, m_val); } mpq const & get_num() const { return m_val; } }; @@ -181,4 +183,13 @@ void import_int_to_real_coercions(environment & env) { expr x = Const("x"); env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); } + +static int mk_real_value(lua_State * L) { + return push_expr(L, mk_real_value(to_mpq_ext(L, 1))); +} + +void open_real(lua_State * L) { + SET_GLOBAL_FUN(mk_real_value, "mk_real_value"); + SET_GLOBAL_FUN(mk_real_value, "rVal"); +} } diff --git a/src/library/arith/real.h b/src/library/arith/real.h index 8d8e6761a..05b255509 100644 --- a/src/library/arith/real.h +++ b/src/library/arith/real.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lua.h" #include "util/numerics/mpq.h" #include "kernel/expr.h" #include "kernel/builtin.h" @@ -77,4 +78,6 @@ inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); } /** \brief Import the coercions \c i2r and \c n2r. The Integer and (basic) Real libraries are also imported. */ void import_int_to_real_coercions(environment & env); + +void open_real(lua_State * L); } diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index f0c34c046..c172e04fe 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/kernel_exception.h" +#include "library/kernel_bindings.h" #include "library/io_state.h" namespace lean { @@ -94,4 +95,145 @@ diagnostic const & operator<<(diagnostic const & out, kernel_exception const & e out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(ex.pp(out.m_io_state.get_formatter(), opts), opts); return out; } + +DECL_UDATA(io_state) + +int mk_io_state(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) + return push_io_state(L, io_state()); + else if (nargs == 1) + return push_io_state(L, io_state(to_io_state(L, 1))); + else + 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 std::mutex g_print_mutex; + +static void print(io_state * ios, bool reg, char const * msg) { + if (ios) { + if (reg) + regular(*ios) << msg; + else + diagnostic(*ios) << msg; + } else { + std::cout << msg; + } +} + +/** \brief Thread safe version of print function */ +static int print(lua_State * L, int start, bool reg) { + std::lock_guard lock(g_print_mutex); + io_state * ios = get_io_state(L); + int n = lua_gettop(L); + int i; + lua_getglobal(L, "tostring"); + for (i = start; i <= n; i++) { + char const * s; + size_t l; + lua_pushvalue(L, -1); + lua_pushvalue(L, i); + lua_call(L, 1, 1); + s = lua_tolstring(L, -1, &l); + if (s == NULL) + throw exception("'to_string' must return a string to 'print'"); + if (i > start) { + print(ios, reg, "\t"); + } + print(ios, reg, s); + lua_pop(L, 1); + } + print(ios, reg, "\n"); + return 0; +} + +static int print(lua_State * L, io_state & ios, int start, bool reg) { + set_io_state set(L, ios); + 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 const struct luaL_Reg io_state_m[] = { + {"__gc", io_state_gc}, // never throws + {"get_options", safe_function}, + {"set_options", safe_function}, + {"get_formatter", safe_function}, + {"print_diagnostic", safe_function}, + {"print_regular", safe_function}, + {"print", safe_function}, + {"diagnostic", safe_function}, + {0, 0} +}; + +void open_io_state(lua_State * L) { + luaL_newmetatable(L, io_state_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, io_state_m, 0); + + SET_GLOBAL_FUN(io_state_pred, "is_io_state"); + SET_GLOBAL_FUN(mk_io_state, "io_state"); + SET_GLOBAL_FUN(print, "print"); +} + +static char g_set_state_key; + +set_io_state::set_io_state(lua_State * L, io_state & st) { + m_state = L; + m_prev = get_io_state(L); + lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); + lua_pushlightuserdata(m_state, &st); + lua_settable(m_state, LUA_REGISTRYINDEX); + if (!m_prev) + m_prev_options = get_global_options(m_state); + set_global_options(m_state, st.get_options()); +} + +set_io_state::~set_io_state() { + lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); + lua_pushlightuserdata(m_state, m_prev); + lua_settable(m_state, LUA_REGISTRYINDEX); + if (!m_prev) + set_global_options(m_state, m_prev_options); +} + +io_state * get_io_state(lua_State * L) { + lua_pushlightuserdata(L, static_cast(&g_set_state_key)); + lua_gettable(L, LUA_REGISTRYINDEX); + if (lua_islightuserdata(L, -1)) { + io_state * r = static_cast(lua_touserdata(L, -1)); + if (r) { + lua_pop(L, 1); + options o = get_global_options(L); + r->set_options(o); + return r; + } + } + lua_pop(L, 1); + return nullptr; +} } diff --git a/src/library/io_state.h b/src/library/io_state.h index ac5fa13ae..f51d82cf0 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -87,4 +87,24 @@ inline diagnostic const & operator<<(diagnostic const & out, T const & t) { out.m_io_state.get_diagnostic_channel().get_stream() << t; return out; } + +UDATA_DEFS(io_state) +/** + \brief Auxiliary class for temporarily setting the Lua registry of a Lua state + with a Lean io_state object. +*/ +class set_io_state { + lua_State * m_state; + io_state * m_prev; + options m_prev_options; +public: + set_io_state(lua_State * L, io_state & st); + ~set_io_state(); +}; +/** + \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); +void open_io_state(lua_State * L); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp new file mode 100644 index 000000000..9676a7f88 --- /dev/null +++ b/src/library/kernel_bindings.cpp @@ -0,0 +1,1547 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/lua.h" +#include "util/sstream.h" +#include "kernel/expr.h" +#include "kernel/context.h" +#include "kernel/formatter.h" +#include "kernel/environment.h" +#include "kernel/metavar.h" +#include "kernel/abstract.h" +#include "kernel/free_vars.h" +#include "kernel/for_each_fn.h" +#include "kernel/instantiate.h" +#include "kernel/occurs.h" +#include "library/expr_lt.h" +#include "library/kernel_bindings.h" +#include "library/io_state.h" +#include "library/type_inferer.h" + +// Lua Bindings for the Kernel classes. We do not include the Lua +// bindings in the kernel because we do not want to inflate the Kernel. + +namespace lean { +DECL_UDATA(level) + +static int level_tostring(lua_State * L) { + std::ostringstream out; + options opts = get_global_options(L); + out << mk_pair(pp(to_level(L, 1), opts), opts); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int level_eq(lua_State * L) { + lua_pushboolean(L, to_level(L, 1) == to_level(L, 2)); + return 1; +} + +static int level_lt(lua_State * L) { + lua_pushboolean(L, to_level(L, 1) < to_level(L, 2)); + return 1; +} + +static int mk_level(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + // bottom + return push_level(L, level()); + } else if (nargs == 1) { + // uvar + return push_level(L, level(to_name_ext(L, 1))); + } else if (nargs == 2 && lua_isnumber(L, 2)) { + // lift + return push_level(L, to_level(L, 1) + luaL_checkinteger(L, 2)); + } else { + // max + level r = to_level(L, 1); + for (int i = 2; i <= nargs; i++) { + r = max(r, to_level(L, i)); + } + return push_level(L, r); + } +} + +#define LEVEL_PRED(P) \ +static int level_ ## P(lua_State * L) { \ + lua_pushboolean(L, P(to_level(L, 1))); \ + return 1; \ +} + +LEVEL_PRED(is_bottom) +LEVEL_PRED(is_uvar) +LEVEL_PRED(is_lift) +LEVEL_PRED(is_max) + +static int level_name(lua_State * L) { + if (!is_uvar(to_level(L, 1))) + throw exception("arg #1 must be a Lean level universal variable"); + return push_name(L, uvar_name(to_level(L, 1))); +} + +static int level_lift_of(lua_State * L) { + if (!is_lift(to_level(L, 1))) + throw exception("arg #1 must be a Lean level lift"); + return push_level(L, lift_of(to_level(L, 1))); +} + +static int level_lift_offset(lua_State * L) { + if (!is_lift(to_level(L, 1))) + throw exception("arg #1 must be a Lean level lift"); + lua_pushinteger(L, lift_offset(to_level(L, 1))); + return 1; +} + +static int level_max_size(lua_State * L) { + if (!is_max(to_level(L, 1))) + throw exception("arg #1 must be a Lean level max"); + lua_pushinteger(L, max_size(to_level(L, 1))); + return 1; +} + +static int level_max_level(lua_State * L) { + if (!is_max(to_level(L, 1))) + throw exception("arg #1 must be a Lean level max"); + return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2))); +} + +static int level_get_kind(lua_State * L) { + lua_pushinteger(L, static_cast(kind(to_level(L, 1)))); + return 1; +} + +static const struct luaL_Reg level_m[] = { + {"__gc", level_gc}, // never throws + {"__tostring", safe_function}, + {"__eq", safe_function}, + {"__lt", safe_function}, + {"kind", safe_function}, + {"is_bottom", safe_function}, + {"is_lift", safe_function}, + {"is_max", safe_function}, + {"is_uvar", safe_function}, + {"uvar_name", safe_function}, + {"lift_of", safe_function}, + {"lift_offset", safe_function}, + {"max_size", safe_function}, + {"max_level", safe_function}, + {0, 0} +}; + +static void open_level(lua_State * L) { + luaL_newmetatable(L, level_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, level_m, 0); + + SET_GLOBAL_FUN(mk_level, "level"); + SET_GLOBAL_FUN(level_pred, "is_level"); + + lua_newtable(L); + SET_ENUM("UVar", level_kind::UVar); + SET_ENUM("Lift", level_kind::Lift); + SET_ENUM("Max", level_kind::Max); + lua_setglobal(L, "level_kind"); +} + +DECL_UDATA(local_entry) + +static int local_entry_eq(lua_State * L) { + lua_pushboolean(L, to_local_entry(L, 1) == to_local_entry(L, 2)); + return 1; +} + +static int local_entry_mk_lift(lua_State * L) { + return push_local_entry(L, mk_lift(luaL_checkinteger(L, 1), luaL_checkinteger(L, 2))); +} + +static int local_entry_mk_inst(lua_State * L) { + return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_nonnull_expr(L, 2))); +} + +static int local_entry_is_lift(lua_State * L) { + lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_lift()); + return 1; +} + +static int local_entry_is_inst(lua_State * L) { + lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_inst()); + return 1; +} + +static int local_entry_s(lua_State * L) { + lua_pushinteger(L, to_local_entry(L, 1).s()); + return 1; +} + +static int local_entry_n(lua_State * L) { + local_entry & e = to_local_entry(L, 1); + if (!e.is_lift()) + throw exception("Lean lift local entry expected"); + lua_pushinteger(L, to_local_entry(L, 1).n()); + return 1; +} + +static int local_entry_v(lua_State * L) { + local_entry & e = to_local_entry(L, 1); + if (!e.is_inst()) + throw exception("Lean inst local entry expected"); + return push_expr(L, to_local_entry(L, 1).v()); + return 1; +} + +static const struct luaL_Reg local_entry_m[] = { + {"__gc", local_entry_gc}, // never throws + {"__eq", safe_function}, + {"is_lift", safe_function}, + {"is_inst", safe_function}, + {"s", safe_function}, + {"n", safe_function}, + {"v", safe_function}, + {0, 0} +}; + +DECL_UDATA(local_context) + +static int mk_local_context(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_local_context(L, local_context()); + } else { + return push_local_context(L, local_context(to_local_entry(L, 1), to_local_context(L, 2))); + } +} + +static int local_context_head(lua_State * L) { + return push_local_entry(L, head(to_local_context(L, 1))); +} + +static int local_context_tail(lua_State * L) { + return push_local_context(L, tail(to_local_context(L, 1))); +} + +static int local_context_is_nil(lua_State * L) { + lua_pushboolean(L, !to_local_context(L, 1)); + return 1; +} + +static const struct luaL_Reg local_context_m[] = { + {"__gc", local_context_gc}, + {"head", local_context_head}, + {"tail", local_context_tail}, + {"is_nil", local_context_is_nil}, + {0, 0} +}; + +static void open_local_context(lua_State * L) { + luaL_newmetatable(L, local_entry_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, local_entry_m, 0); + SET_GLOBAL_FUN(local_entry_mk_lift, "mk_lift"); + SET_GLOBAL_FUN(local_entry_mk_inst, "mk_inst"); + SET_GLOBAL_FUN(local_entry_pred, "is_local_entry"); + + luaL_newmetatable(L, local_context_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, local_context_m, 0); + SET_GLOBAL_FUN(mk_local_context, "local_context"); + SET_GLOBAL_FUN(local_context_pred, "is_local_context"); +} + +DECL_UDATA(expr) + +expr & to_nonnull_expr(lua_State * L, int idx) { + expr & r = to_expr(L, idx); + if (!r) + throw exception("non-null Lean expression expected"); + return r; +} + +expr & to_app(lua_State * L, int idx) { + expr & r = to_nonnull_expr(L, idx); + if (!is_app(r)) + throw exception("Lean application expression expected"); + return r; +} + +static int expr_tostring(lua_State * L) { + std::ostringstream out; + expr & e = to_expr(L, 1); + if (e) { + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(fmt(to_expr(L, 1), opts), opts); + } else { + out << ""; + } + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int expr_eq(lua_State * L) { + lua_pushboolean(L, to_expr(L, 1) == to_expr(L, 2)); + return 1; +} + +static int expr_lt(lua_State * L) { + lua_pushboolean(L, to_expr(L, 1) < to_expr(L, 2)); + return 1; +} + +static int expr_mk_constant(lua_State * L) { + return push_expr(L, mk_constant(to_name_ext(L, 1))); +} + +static int expr_mk_var(lua_State * L) { + return push_expr(L, mk_var(luaL_checkinteger(L, 1))); +} + +static int expr_mk_app(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs < 2) + throw exception("application must have at least two arguments"); + buffer args; + for (int i = 1; i <= nargs; i++) + args.push_back(to_nonnull_expr(L, i)); + return push_expr(L, mk_app(args)); +} + +static int expr_mk_eq(lua_State * L) { + return push_expr(L, mk_eq(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2))); +} + +static int expr_mk_lambda(lua_State * L) { + return push_expr(L, mk_lambda(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); +} + +static int expr_mk_pi(lua_State * L) { + return push_expr(L, mk_pi(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); +} + +static int expr_mk_arrow(lua_State * L) { + return push_expr(L, mk_arrow(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2))); +} + +static int expr_mk_let(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 3) + return push_expr(L, mk_let(to_name_ext(L, 1), expr(), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); + else + return push_expr(L, mk_let(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4))); +} + +static expr get_expr_from_table(lua_State * L, int t, int i) { + lua_pushvalue(L, t); // push table to the top + lua_pushinteger(L, i); + lua_gettable(L, -2); + expr r = to_nonnull_expr(L, -1); + lua_pop(L, 2); // remove table and value + return r; +} + +// t is a table of pairs {{a1, b1}, ..., {ak, bk}} +// Each ai and bi is an expression +static std::pair get_expr_pair_from_table(lua_State * L, int t, int i) { + lua_pushvalue(L, t); // push table on the top + lua_pushinteger(L, i); + lua_gettable(L, -2); // now table {ai, bi} is on the top + if (!lua_istable(L, -1) || objlen(L, -1) != 2) + throw exception("arg #1 must be of the form '{{expr, expr}, ...}'"); + expr ai = get_expr_from_table(L, -1, 1); + expr bi = get_expr_from_table(L, -1, 2); + lua_pop(L, 2); // pop table {ai, bi} and t from stack + return mk_pair(ai, bi); +} + +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) { + int nargs = lua_gettop(L); + if (nargs < 2) + throw exception("function must have at least 2 arguments"); + if (nargs == 2) { + if (!lua_istable(L, 1)) + throw exception("function expects arg #1 to be of the form '{{expr, expr}, ...}'"); + int len = objlen(L, 1); + if (len == 0) + throw exception("function expects arg #1 to be a non-empty table"); + expr r = to_nonnull_expr(L, 2); + for (int i = len; i >= 1; i--) { + auto p = get_expr_pair_from_table(L, 1, i); + r = F1(p.first, p.second, r); + } + return push_expr(L, r); + } else { + if (nargs % 2 == 0) + throw exception("function must have an odd number of arguments"); + expr r = to_nonnull_expr(L, nargs); + for (int i = nargs - 1; i >= 1; i-=2) { + if (is_expr(L, i - 1)) + r = F1(to_nonnull_expr(L, i - 1), to_nonnull_expr(L, i), r); + else + r = F2(to_name_ext(L, i - 1), to_nonnull_expr(L, i), r); + } + return push_expr(L, r); + } +} + +static int expr_fun(lua_State * L) { return expr_abst(L); } +static int expr_pi(lua_State * L) { return expr_abst(L); } +static int expr_let(lua_State * L) { return expr_abst(L); } + +static int expr_type(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) + return push_expr(L, Type()); + else + return push_expr(L, Type(to_level(L, 1))); +} + +static int expr_mk_metavar(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 1) + return push_expr(L, mk_metavar(to_name_ext(L, 1))); + else + return push_expr(L, mk_metavar(to_name_ext(L, 1), to_local_context(L, 2))); +} + +static int expr_is_null(lua_State * L) { + lua_pushboolean(L, !to_expr(L, 1)); + return 1; +} + +static int expr_get_kind(lua_State * L) { + lua_pushinteger(L, static_cast(to_nonnull_expr(L, 1).kind())); + return 1; +} + +#define EXPR_PRED(P) \ +static int expr_ ## P(lua_State * L) { \ + lua_pushboolean(L, P(to_nonnull_expr(L, 1))); \ + return 1; \ +} + +EXPR_PRED(is_constant) +EXPR_PRED(is_var) +EXPR_PRED(is_app) +EXPR_PRED(is_eq) +EXPR_PRED(is_lambda) +EXPR_PRED(is_pi) +EXPR_PRED(is_abstraction) +EXPR_PRED(is_let) +EXPR_PRED(is_value) +EXPR_PRED(is_metavar) +EXPR_PRED(has_free_vars) +EXPR_PRED(closed) +EXPR_PRED(has_metavar) + +/** + \brief Iterator (closure base function) for application args. See \c expr_args +*/ +static int expr_next_arg(lua_State * L) { + expr & e = to_expr(L, lua_upvalueindex(1)); + unsigned i = lua_tointeger(L, lua_upvalueindex(2)); + if (i >= num_args(e)) { + lua_pushnil(L); + } else { + lua_pushinteger(L, i + 1); + lua_replace(L, lua_upvalueindex(2)); // update closure + push_expr(L, arg(e, i)); + } + return 1; +} + +static int expr_args(lua_State * L) { + expr & e = to_app(L, 1); + push_expr(L, e); // upvalue(1): expr + lua_pushinteger(L, 0); // upvalue(2): index + lua_pushcclosure(L, &safe_function, 2); // create closure with 2 upvalues + return 1; +} + +static int expr_num_args(lua_State * L) { + lua_pushinteger(L, num_args(to_app(L, 1))); + return 1; +} + +static int expr_arg(lua_State * L) { + expr & e = to_app(L, 1); + int i = luaL_checkinteger(L, 2); + if (i >= static_cast(num_args(e)) || i < 0) + throw exception(sstream() << "invalid application argument #" << i << ", application has " << num_args(e) << " arguments"); + return push_expr(L, arg(e, i)); +} + +static int expr_fields(lua_State * L) { + expr & e = to_nonnull_expr(L, 1); + switch (e.kind()) { + case expr_kind::Var: lua_pushinteger(L, var_idx(e)); return 1; + case expr_kind::Constant: return push_name(L, const_name(e)); + case expr_kind::Type: return push_level(L, ty_level(e)); + case expr_kind::Value: return to_value(e).push_lua(L); + case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2; + case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2; + case expr_kind::Lambda: + case expr_kind::Pi: push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3; + case expr_kind::Let: push_name(L, let_name(e)); push_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4; + case expr_kind::MetaVar: push_name(L, metavar_name(e)); push_local_context(L, metavar_lctx(e)); return 2; + } + lean_unreachable(); // LCOV_EXCL_LINE + return 0; // LCOV_EXCL_LINE +} + +static int expr_for_each(lua_State * L) { + expr & e = to_nonnull_expr(L, 1); // expr + luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun + auto f = [&](expr const & a, unsigned offset) { + lua_pushvalue(L, 2); // push user-fun + push_expr(L, a); + lua_pushinteger(L, offset); + pcall(L, 2, 1, 0); + bool r = true; + if (lua_isboolean(L, -1)) + r = lua_toboolean(L, -1); + lua_pop(L, 1); + return r; + }; + for_each_fn proc(f); + proc(e); + return 0; +} + +static int expr_has_free_var(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2))); + else + lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3))); + return 1; +} + +static int expr_lift_free_vars(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_expr(L, lift_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2))); + else + return push_expr(L, lift_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3))); +} + +static int expr_lower_free_vars(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_expr(L, lower_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2))); + else + return push_expr(L, lower_free_vars(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3))); +} + +// Copy Lua table/array elements to r +static void copy_lua_array(lua_State * L, int tidx, buffer & r) { + luaL_checktype(L, tidx, LUA_TTABLE); + int n = objlen(L, tidx); + for (int i = 1; i <= n; i++) { + lua_rawgeti(L, tidx, i); + r.push_back(to_expr(L, -1)); + lua_pop(L, 1); + } +} + +static int expr_instantiate(lua_State * L) { + expr const & e = to_expr(L, 1); + if (is_expr(L, 2)) { + return push_expr(L, instantiate(e, to_expr(L, 2))); + } else { + buffer s; + copy_lua_array(L, 2, s); + return push_expr(L, instantiate(e, s.size(), s.data())); + } +} + +static int expr_abstract(lua_State * L) { + expr const & e = to_expr(L, 1); + if (is_expr(L, 2)) { + expr const & e2 = to_expr(L, 2); + return push_expr(L, abstract(e, 1, &e2)); + } else { + buffer s; + copy_lua_array(L, 2, s); + return push_expr(L, abstract(e, s.size(), s.data())); + } +} + +static int expr_occurs(lua_State * L) { + lua_pushboolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); + return 1; +} + +static int expr_is_eqp(lua_State * L) { + lua_pushboolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); + return 1; +} + +static int expr_hash(lua_State * L) { + lua_pushinteger(L, to_expr(L, 1).hash()); + return 1; +} + +static const struct luaL_Reg expr_m[] = { + {"__gc", expr_gc}, // never throws + {"__tostring", safe_function}, + {"__eq", safe_function}, + {"__lt", safe_function}, + {"__call", safe_function}, + {"kind", safe_function}, + {"is_null", safe_function}, + {"is_var", safe_function}, + {"is_constant", safe_function}, + {"is_app", safe_function}, + {"is_eq", safe_function}, + {"is_lambda", safe_function}, + {"is_pi", safe_function}, + {"is_abstraction", safe_function}, + {"is_let", safe_function}, + {"is_value", safe_function}, + {"is_metavar", safe_function}, + {"fields", safe_function}, + {"data", safe_function}, + {"args", safe_function}, + {"num_args", safe_function}, + {"arg", safe_function}, + {"for_each", safe_function}, + {"has_free_vars", safe_function}, + {"closed", safe_function}, + {"has_free_var", safe_function}, + {"lift_free_vars", safe_function}, + {"lower_free_vars", safe_function}, + {"instantiate", safe_function}, + {"abstract", safe_function}, + {"occurs", safe_function}, + {"has_metavar", safe_function}, + {"is_eqp", safe_function}, + {"hash", safe_function}, + {0, 0} +}; + +static void open_expr(lua_State * L) { + luaL_newmetatable(L, expr_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, expr_m, 0); + + SET_GLOBAL_FUN(expr_mk_constant, "mk_constant"); + SET_GLOBAL_FUN(expr_mk_constant, "Const"); + SET_GLOBAL_FUN(expr_mk_var, "mk_var"); + SET_GLOBAL_FUN(expr_mk_var, "Var"); + SET_GLOBAL_FUN(expr_mk_app, "mk_app"); + SET_GLOBAL_FUN(expr_mk_eq, "mk_eq"); + SET_GLOBAL_FUN(expr_mk_eq, "Eq"); + SET_GLOBAL_FUN(expr_mk_lambda, "mk_lambda"); + SET_GLOBAL_FUN(expr_mk_pi, "mk_pi"); + SET_GLOBAL_FUN(expr_mk_arrow, "mk_arrow"); + SET_GLOBAL_FUN(expr_mk_let, "mk_let"); + SET_GLOBAL_FUN(expr_fun, "fun"); + SET_GLOBAL_FUN(expr_fun, "Fun"); + SET_GLOBAL_FUN(expr_pi, "Pi"); + SET_GLOBAL_FUN(expr_let, "Let"); + SET_GLOBAL_FUN(expr_type, "mk_type"); + SET_GLOBAL_FUN(expr_type, "Type"); + SET_GLOBAL_FUN(expr_mk_metavar, "mk_metavar"); + SET_GLOBAL_FUN(expr_pred, "is_expr"); + + lua_newtable(L); + SET_ENUM("Var", expr_kind::Var); + SET_ENUM("Constant", expr_kind::Constant); + SET_ENUM("Type", expr_kind::Type); + SET_ENUM("Value", expr_kind::Value); + SET_ENUM("App", expr_kind::App); + SET_ENUM("Eq", expr_kind::Eq); + SET_ENUM("Lambda", expr_kind::Lambda); + SET_ENUM("Pi", expr_kind::Pi); + SET_ENUM("Let", expr_kind::Let); + SET_ENUM("MetaVar", expr_kind::MetaVar); + lua_setglobal(L, "expr_kind"); +} + +DECL_UDATA(context_entry) + +static int mk_context_entry(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2))); + else + return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); +} + +static int context_entry_get_name(lua_State * L) { return push_name(L, to_context_entry(L, 1).get_name()); } +static int context_entry_get_domain(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_domain()); } +static int context_entry_get_body(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_body()); } + +static const struct luaL_Reg context_entry_m[] = { + {"__gc", context_entry_gc}, // never throws + {"get_name", safe_function}, + {"get_domain", safe_function}, + {"get_body", safe_function}, + {0, 0} +}; + +DECL_UDATA(context) + +static int context_tostring(lua_State * L) { + std::ostringstream out; + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(fmt(to_context(L, 1), opts), opts); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int mk_context(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_context(L, context()); + } else if (nargs == 2) { + context_entry & e = to_context_entry(L, 2); + return push_context(L, context(to_context(L, 1), e.get_name(), e.get_domain(), e.get_body())); + } else if (nargs == 3) { + return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_nonnull_expr(L, 3))); + } else { + return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_nonnull_expr(L, 4))); + } +} + +static int context_extend(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs != 3 && nargs != 4) + throw exception("extend expect 3 or 4 arguments"); + return mk_context(L); +} + +static int context_is_empty(lua_State * L) { + lua_pushboolean(L, empty(to_context(L, 1))); + return 1; +} + +static int context_lookup(lua_State * L) { + auto p = lookup_ext(to_context(L, 1), luaL_checkinteger(L, 2)); + push_context_entry(L, p.first); + push_context(L, p.second); + return 2; +} + +static int context_size(lua_State * L) { + lua_pushinteger(L, to_context(L, 1).size()); + return 1; +} + +static const struct luaL_Reg context_m[] = { + {"__gc", context_gc}, // never throws + {"__tostring", safe_function}, + {"__len", safe_function}, + {"is_empty", safe_function}, + {"size", safe_function}, + {"extend", safe_function}, + {"lookup", safe_function}, + {0, 0} +}; + +static void open_context(lua_State * L) { + luaL_newmetatable(L, context_entry_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, context_entry_m, 0); + SET_GLOBAL_FUN(mk_context_entry, "context_entry"); + SET_GLOBAL_FUN(context_entry_pred, "is_context_entry"); + + luaL_newmetatable(L, context_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, context_m, 0); + SET_GLOBAL_FUN(mk_context, "context"); + SET_GLOBAL_FUN(context_pred, "is_context"); + SET_GLOBAL_FUN(context_extend, "extend"); + SET_GLOBAL_FUN(context_lookup, "lookup"); +} + +DECL_UDATA(formatter) + +[[ noreturn ]] void throw_invalid_formatter_call() { + throw exception("invalid formatter invocation, the acceptable arguments are: (expr, options?), (context, options?), (context, expr, bool? options?), (kernel object, options?), (environment, options?)"); +} + +static int formatter_call(lua_State * L) { + int nargs = lua_gettop(L); + formatter & fmt = to_formatter(L, 1); + options opts = get_global_options(L); + if (nargs <= 3) { + if (nargs == 3) { + if (is_options(L, 3)) + opts = to_options(L, 3); + else if (is_context(L, 2) && is_expr(L, 3)) + return push_format(L, fmt(to_context(L, 2), to_expr(L, 3))); + else + throw_invalid_formatter_call(); + } + if (is_expr(L, 2)) { + return push_format(L, fmt(to_expr(L, 2), opts)); + } else if (is_context(L, 2)) { + return push_format(L, fmt(to_context(L, 2), opts)); + } else if (is_environment(L, 2)) { + ro_environment env(L, 2); + return push_format(L, fmt(env, opts)); + } else if (is_object(L, 2)) { + return push_format(L, fmt(to_object(L, 2), opts)); + } else { + throw_invalid_formatter_call(); + } + } else if (nargs <= 5) { + if (nargs == 5) + opts = to_options(L, 5); + return push_format(L, fmt(to_context(L, 2), to_expr(L, 3), lua_toboolean(L, 4), opts)); + } else { + throw_invalid_formatter_call(); + } +} + +static const struct luaL_Reg formatter_m[] = { + {"__gc", formatter_gc}, // never throws + {"__call", safe_function}, + {0, 0} +}; + +static char g_formatter_key; +static formatter g_simple_formatter = mk_simple_formatter(); + +formatter get_global_formatter(lua_State * L) { + io_state * io = get_io_state(L); + if (io != nullptr) { + return io->get_formatter(); + } else { + lua_pushlightuserdata(L, static_cast(&g_formatter_key)); + lua_gettable(L, LUA_REGISTRYINDEX); + if (is_formatter(L, -1)) { + formatter r = to_formatter(L, -1); + lua_pop(L, 1); + return r; + } else { + lua_pop(L, 1); + return g_simple_formatter; + } + } +} + +void set_global_formatter(lua_State * L, formatter const & fmt) { + io_state * io = get_io_state(L); + if (io != nullptr) { + io->set_formatter(fmt); + } else { + lua_pushlightuserdata(L, static_cast(&g_formatter_key)); + push_formatter(L, fmt); + lua_settable(L, LUA_REGISTRYINDEX); + } +} + +int get_formatter(lua_State * L) { + return push_formatter(L, get_global_formatter(L)); +} + +static void open_formatter(lua_State * L) { + luaL_newmetatable(L, formatter_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, formatter_m, 0); + + SET_GLOBAL_FUN(formatter_pred, "is_formatter"); + SET_GLOBAL_FUN(get_formatter, "get_formatter"); +} + +DECL_UDATA(environment) + +static environment get_global_environment(lua_State * L); + +ro_environment::ro_environment(lua_State * L, int idx): + read_only_environment(to_environment(L, idx)) { +} + +ro_environment::ro_environment(lua_State * L): + read_only_environment(get_global_environment(L)) { +} + +rw_environment::rw_environment(lua_State * L, int idx): + read_write_environment(to_environment(L, idx)) { +} + +rw_environment::rw_environment(lua_State * L): + read_write_environment(get_global_environment(L)) { +} + +static int mk_empty_environment(lua_State * L) { + return push_environment(L, environment()); +} + +static int environment_mk_child(lua_State * L) { + rw_environment env(L, 1); + return push_environment(L, env->mk_child()); +} + +static int environment_has_parent(lua_State * L) { + ro_environment env(L, 1); + lua_pushboolean(L, env->has_parent()); + return 1; +} + +static int environment_has_children(lua_State * L) { + ro_environment env(L, 1); + lua_pushboolean(L, env->has_children()); + return 1; +} + +static int environment_parent(lua_State * L) { + ro_environment env(L, 1); + if (!env->has_parent()) + throw exception("environment does not have a parent environment"); + return push_environment(L, env->parent()); +} + +static int environment_add_uvar(lua_State * L) { + rw_environment env(L, 1); + int nargs = lua_gettop(L); + if (nargs == 2) + env->add_uvar(to_name_ext(L, 2)); + else + env->add_uvar(to_name_ext(L, 2), to_level(L, 3)); + return 0; +} + +static int environment_is_ge(lua_State * L) { + ro_environment env(L, 1); + lua_pushboolean(L, env->is_ge(to_level(L, 2), to_level(L, 3))); + return 1; +} + +static int environment_get_uvar(lua_State * L) { + ro_environment env(L, 1); + return push_level(L, env->get_uvar(to_name_ext(L, 2))); +} + +static int environment_add_definition(lua_State * L) { + rw_environment env(L, 1); + int nargs = lua_gettop(L); + if (nargs == 3) { + env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3)); + } else if (nargs == 4) { + if (is_expr(L, 4)) + env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)); + else + env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), lua_toboolean(L, 4)); + } else { + env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4), lua_toboolean(L, 5)); + } + return 0; +} + +static int environment_add_theorem(lua_State * L) { + rw_environment env(L, 1); + env->add_theorem(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)); + return 0; +} + +static int environment_add_var(lua_State * L) { + rw_environment env(L, 1); + env->add_var(to_name_ext(L, 2), to_nonnull_expr(L, 3)); + return 0; +} + +static int environment_add_axiom(lua_State * L) { + rw_environment env(L, 1); + env->add_axiom(to_name_ext(L, 2), to_nonnull_expr(L, 3)); + return 0; +} + +static int environment_find_object(lua_State * L) { + ro_environment env(L, 1); + return push_object(L, env->find_object(to_name_ext(L, 2))); +} + +static int environment_has_object(lua_State * L) { + ro_environment env(L, 1); + lua_pushboolean(L, env->has_object(to_name_ext(L, 2))); + return 1; +} + +static int environment_check_type(lua_State * L) { + ro_environment env(L, 1); + int nargs = lua_gettop(L); + if (nargs == 2) + return push_expr(L, env->infer_type(to_nonnull_expr(L, 2))); + else + return push_expr(L, env->infer_type(to_nonnull_expr(L, 2), to_context(L, 3))); +} + +static int environment_normalize(lua_State * L) { + ro_environment env(L, 1); + int nargs = lua_gettop(L); + if (nargs == 2) + return push_expr(L, env->normalize(to_nonnull_expr(L, 2))); + else + return push_expr(L, env->normalize(to_nonnull_expr(L, 2), to_context(L, 3))); +} + +/** + \brief Iterator (closure base function) for kernel objects. + + \see environment_objects + \see environment_local_objects. +*/ +static int environment_next_object(lua_State * L) { + ro_environment env(L, lua_upvalueindex(1)); + unsigned i = lua_tointeger(L, lua_upvalueindex(2)); + unsigned num = lua_tointeger(L, lua_upvalueindex(3)); + if (i >= num) { + lua_pushnil(L); + } else { + bool local = lua_toboolean(L, lua_upvalueindex(4)); + lua_pushinteger(L, i + 1); + lua_replace(L, lua_upvalueindex(2)); // update closure + push_object(L, env->get_object(i, local)); + } + return 1; +} + +static int environment_objects_core(lua_State * L, bool local) { + ro_environment env(L, 1); + push_environment(L, env); // upvalue(1): environment + lua_pushinteger(L, 0); // upvalue(2): index + lua_pushinteger(L, env->get_num_objects(local)); // upvalue(3): size + lua_pushboolean(L, local); // upvalue(4): local flag + lua_pushcclosure(L, &safe_function, 4); // create closure with 4 upvalues + return 1; +} + +static int environment_objects(lua_State * L) { + return environment_objects_core(L, false); +} + +static int environment_local_objects(lua_State * L) { + return environment_objects_core(L, true); +} + +static int environment_infer_type(lua_State * L) { + int nargs = lua_gettop(L); + type_inferer inferer(to_environment(L, 1)); + if (nargs == 2) + return push_expr(L, inferer(to_nonnull_expr(L, 2))); + else + return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3))); +} + +static int environment_tostring(lua_State * L) { + ro_environment env(L, 1); + std::ostringstream out; + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(fmt(env, opts), opts); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static const struct luaL_Reg environment_m[] = { + {"__gc", environment_gc}, // never throws + {"__tostring", safe_function}, + {"mk_child", safe_function}, + {"has_parent", safe_function}, + {"has_children", safe_function}, + {"parent", safe_function}, + {"add_uvar", safe_function}, + {"is_ge", safe_function}, + {"get_uvar", safe_function}, + {"add_definition", safe_function}, + {"add_theorem", safe_function}, + {"add_var", safe_function}, + {"add_axiom", safe_function}, + {"find_object", safe_function}, + {"has_object", safe_function}, + {"check_type", safe_function}, + {"infer_type", safe_function}, + {"normalize", safe_function}, + {"objects", safe_function}, + {"local_objects", safe_function}, + {0, 0} +}; + +static char g_set_environment_key; + +set_environment::set_environment(lua_State * L, environment & env) { + m_state = L; + lua_pushlightuserdata(m_state, static_cast(&g_set_environment_key)); + push_environment(m_state, env); + lua_settable(m_state, LUA_REGISTRYINDEX); +} + +set_environment::~set_environment() { + lua_pushlightuserdata(m_state, static_cast(&g_set_environment_key)); + lua_pushnil(m_state); + lua_settable(m_state, LUA_REGISTRYINDEX); +} + +static environment get_global_environment(lua_State * L) { + lua_pushlightuserdata(L, static_cast(&g_set_environment_key)); + lua_gettable(L, LUA_REGISTRYINDEX); + if (!is_environment(L, -1)) + throw exception("Lua registry does not contain a Lean environment"); + environment r = to_environment(L, -1); + lua_pop(L, 1); + return r; +} + +int get_environment(lua_State * L) { + return push_environment(L, get_global_environment(L)); +} + +static void open_environment(lua_State * L) { + luaL_newmetatable(L, environment_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, environment_m, 0); + + SET_GLOBAL_FUN(mk_empty_environment, "empty_environment"); + SET_GLOBAL_FUN(environment_pred, "is_environment"); + SET_GLOBAL_FUN(get_environment, "get_environment"); + SET_GLOBAL_FUN(get_environment, "get_env"); +} + +DECL_UDATA(object) + +object & to_nonnull_object(lua_State * L, int idx) { + object & r = to_object(L, idx); + if (!r) + throw exception("non-null kernel object expected"); + return r; +} + +static int object_is_null(lua_State * L) { + lua_pushboolean(L, !to_object(L, 1)); + return 1; +} + +static int object_keyword(lua_State * L) { + lua_pushstring(L, to_nonnull_object(L, 1).keyword()); + return 1; +} + +static int object_has_name(lua_State * L) { + lua_pushboolean(L, to_nonnull_object(L, 1).has_name()); + return 1; +} + +static int object_get_name(lua_State * L) { + object const & o = to_nonnull_object(L, 1); + if (!o.has_name()) + throw exception("kernel object does not have a name"); + return push_name(L, o.get_name()); +} + +static int object_has_type(lua_State * L) { + lua_pushboolean(L, to_nonnull_object(L, 1).has_type()); + return 1; +} + +static int object_get_type(lua_State * L) { + object const & o = to_nonnull_object(L, 1); + if (!o.has_type()) + throw exception("kernel object does not have a type"); + return push_expr(L, o.get_type()); +} + +static int object_has_cnstr_level(lua_State * L) { + lua_pushboolean(L, to_nonnull_object(L, 1).has_cnstr_level()); + return 1; +} + +static int object_get_cnstr_level(lua_State * L) { + object const & o = to_nonnull_object(L, 1); + if (!o.has_cnstr_level()) + throw exception("kernel object does not have a constraint level"); + return push_level(L, o.get_cnstr_level()); +} + +static int object_get_value(lua_State * L) { + object const & o = to_nonnull_object(L, 1); + if (!o.is_definition() && !o.is_builtin()) + throw exception("kernel object is not a definition/theorem/builtin"); + return push_expr(L, o.get_value()); +} + +static int object_get_weight(lua_State * L) { + object const & o = to_nonnull_object(L, 1); + if (!o.is_definition()) + throw exception("kernel object is not a definition"); + lua_pushinteger(L, o.get_weight()); + return 1; +} + +#define OBJECT_PRED(P) \ +static int object_ ## P(lua_State * L) { \ + lua_pushboolean(L, to_nonnull_object(L, 1).P()); \ + return 1; \ +} + +OBJECT_PRED(is_definition) +OBJECT_PRED(is_opaque) +OBJECT_PRED(is_axiom) +OBJECT_PRED(is_theorem) +OBJECT_PRED(is_var_decl) +OBJECT_PRED(is_builtin) +OBJECT_PRED(is_builtin_set) + +static int object_in_builtin_set(lua_State * L) { + lua_pushboolean(L, to_nonnull_object(L, 1).in_builtin_set(to_expr(L, 2))); + return 1; +} + +static int object_tostring(lua_State * L) { + std::ostringstream out; + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + object & obj = to_object(L, 1); + if (obj) + out << mk_pair(fmt(to_object(L, 1), opts), opts); + else + out << ""; + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static const struct luaL_Reg object_m[] = { + {"__gc", object_gc}, // never throws + {"__tostring", safe_function}, + {"is_null", safe_function}, + {"keyword", safe_function}, + {"has_name", safe_function}, + {"get_name", safe_function}, + {"has_type", safe_function}, + {"get_type", safe_function}, + {"has_cnstr_level", safe_function}, + {"get_cnstr_level", safe_function}, + {"is_definition", safe_function}, + {"is_opaque", safe_function}, + {"get_value", safe_function}, + {"get_weight", safe_function}, + {"is_axiom", safe_function}, + {"is_theorem", safe_function}, + {"is_var_decl", safe_function}, + {"is_builtin", safe_function}, + {"is_builtin_set", safe_function}, + {"in_builtin_set", safe_function}, + {0, 0} +}; + +static void open_object(lua_State * L) { + luaL_newmetatable(L, object_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, object_m, 0); + + SET_GLOBAL_FUN(object_pred, "is_kernel_object"); +} + +DECL_UDATA(justification) + +static int justification_tostring(lua_State * L) { + std::ostringstream out; + justification & jst = to_justification(L, 1); + if (jst) { + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(jst.pp(fmt, opts), opts); + } else { + out << ""; + } + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int justification_has_children(lua_State * L) { + lua_pushboolean(L, to_justification(L, 1).has_children()); + return 1; +} + +static int justification_is_null(lua_State * L) { + lua_pushboolean(L, !to_justification(L, 1)); + return 1; +} + +/** + \brief Iterator (closure base function) for justification children. See \c justification_children +*/ +static int justification_next_child(lua_State * L) { + unsigned i = lua_tointeger(L, lua_upvalueindex(2)); + unsigned num = objlen(L, lua_upvalueindex(1)); + if (i > num) { + lua_pushnil(L); + } else { + lua_pushinteger(L, i + 1); + lua_replace(L, lua_upvalueindex(2)); // update i + lua_rawgeti(L, lua_upvalueindex(1), i); // read children[i] + } + return 1; +} + +static int justification_children(lua_State * L) { + buffer children; + to_justification(L, 1).get_children(children); + lua_newtable(L); + int i = 1; + for (auto jcell : children) { + push_justification(L, justification(jcell)); + lua_rawseti(L, -2, i); + i = i + 1; + } + lua_pushinteger(L, 1); + lua_pushcclosure(L, &safe_function, 2); // create closure with 2 upvalues + return 1; +} + +static int justification_get_main_expr(lua_State * L) { + return push_expr(L, to_justification(L, 1).get_main_expr()); +} + +static int justification_pp(lua_State * L) { + int nargs = lua_gettop(L); + justification & jst = to_justification(L, 1); + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + bool display_children = true; + + if (nargs == 2) { + if (lua_isboolean(L, 2)) { + display_children = lua_toboolean(L, 2); + } else { + luaL_checktype(L, 2, LUA_TTABLE); + + lua_pushstring(L, "formatter"); + lua_gettable(L, 2); + if (is_formatter(L, -1)) + fmt = to_formatter(L, -1); + lua_pop(L, 1); + + lua_pushstring(L, "options"); + lua_gettable(L, 2); + if (is_options(L, -1)) + opts = to_options(L, -1); + lua_pop(L, 1); + + lua_pushstring(L, "display_children"); + lua_gettable(L, 2); + if (lua_isboolean(L, -1)) + display_children = lua_toboolean(L, -1); + lua_pop(L, 1); + } + } + return push_format(L, jst.pp(fmt, opts, nullptr, display_children)); +} + +static int justification_depends_on(lua_State * L) { + lua_pushboolean(L, depends_on(to_justification(L, 1), to_justification(L, 2))); + return 1; +} + +static int mk_assumption_justification(lua_State * L) { + return push_justification(L, mk_assumption_justification(luaL_checkinteger(L, 1))); +} + +static const struct luaL_Reg justification_m[] = { + {"__gc", justification_gc}, // never throws + {"__tostring", safe_function}, + {"is_null", safe_function}, + {"has_children", safe_function}, + {"children", safe_function}, + {"get_main_expr", safe_function}, + {"pp", safe_function}, + {"depends_on", safe_function}, + {0, 0} +}; + +static void open_justification(lua_State * L) { + luaL_newmetatable(L, justification_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, justification_m, 0); + + SET_GLOBAL_FUN(mk_assumption_justification, "mk_assumption_justification"); + SET_GLOBAL_FUN(justification_pred, "is_justification"); +} + +DECL_UDATA(metavar_env) + +static int menv_mk_metavar(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 1) { + return push_expr(L, to_metavar_env(L, 1).mk_metavar()); + } else if (nargs == 2) { + return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2))); + } else { + return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), to_expr(L, 3))); + } +} + +static expr & to_metavar(lua_State * L, int i, bool lctx = true) { + expr & e = to_expr(L, i); + if (is_metavar(e)) { + if (lctx || !has_local_context(e)) + return e; + throw exception(sstream() << "arg #" << i << " must be a metavariable without a local context"); + } + throw exception(sstream() << "arg #" << i << " must be a metavariable"); +} + +static int menv_get_timestamp(lua_State * L) { + lua_pushinteger(L, to_metavar_env(L, 1).get_timestamp()); + return 1; +} + +static int menv_get_context(lua_State * L) { + if (is_expr(L, 2)) + return push_context(L, to_metavar_env(L, 1).get_context(to_metavar(L, 2, false))); + else + return push_context(L, to_metavar_env(L, 1).get_context(to_name_ext(L, 2))); +} + +static int menv_has_type(lua_State * L) { + if (is_expr(L, 2)) + lua_pushboolean(L, to_metavar_env(L, 1).has_type(to_metavar(L, 2))); + else + lua_pushboolean(L, to_metavar_env(L, 1).has_type(to_name_ext(L, 2))); + return 1; +} + +static int menv_get_type(lua_State * L) { + if (is_expr(L, 2)) + return push_expr(L, to_metavar_env(L, 1).get_type(to_metavar(L, 2))); + else + return push_expr(L, to_metavar_env(L, 1).get_type(to_name_ext(L, 2))); +} + +static int menv_is_assigned(lua_State * L) { + if (is_expr(L, 2)) + lua_pushboolean(L, to_metavar_env(L, 1).is_assigned(to_metavar(L, 2))); + else + lua_pushboolean(L, to_metavar_env(L, 1).is_assigned(to_name_ext(L, 2))); + return 1; +} + +static int menv_assign(lua_State * L) { + int nargs = lua_gettop(L); + justification jst; + if (nargs == 4) + jst = to_justification(L, 4); + if (is_expr(L, 2)) + to_metavar_env(L, 1).assign(to_metavar(L, 2, false), to_expr(L, 3), jst); + else + to_metavar_env(L, 1).assign(to_name_ext(L, 2), to_expr(L, 3), jst); + return 0; +} + +static int menv_get_subst(lua_State * L) { + if (is_expr(L, 2)) + return push_expr(L, to_metavar_env(L, 1).get_subst(to_metavar(L, 2))); + else + return push_expr(L, to_metavar_env(L, 1).get_subst(to_name_ext(L, 2))); +} + +static int menv_get_justification(lua_State * L) { + if (is_expr(L, 2)) + return push_justification(L, to_metavar_env(L, 1).get_justification(to_metavar(L, 2))); + else + return push_justification(L, to_metavar_env(L, 1).get_justification(to_name_ext(L, 2))); +} + +static int menv_get_subst_jst(lua_State * L) { + if (is_expr(L, 2)) { + auto p = to_metavar_env(L, 1).get_subst_jst(to_metavar(L, 2)); + push_expr(L, p.first); + push_justification(L, p.second); + } else { + auto p = to_metavar_env(L, 1).get_subst_jst(to_name_ext(L, 2)); + push_expr(L, p.first); + push_justification(L, p.second); + } + return 2; +} + +static int menv_for_each_subst(lua_State * L) { + luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun + to_metavar_env(L, 1).for_each_subst([&](name const & n, expr const & e) { + lua_pushvalue(L, 2); // push user-fun + push_name(L, n); + push_expr(L, e); + pcall(L, 2, 0, 0); + }); + return 0; +} + +static int mk_metavar_env(lua_State * L) { + if (lua_gettop(L) == 1) + return push_metavar_env(L, metavar_env(to_name_ext(L, 1))); + else + return push_metavar_env(L, metavar_env()); +} + +static int menv_copy(lua_State * L) { + return push_metavar_env(L, metavar_env(to_metavar_env(L, 1))); +} + +static int instantiate_metavars(lua_State * L) { + return push_expr(L, instantiate_metavars(to_expr(L, 1), to_metavar_env(L, 2))); +} + +static const struct luaL_Reg metavar_env_m[] = { + {"__gc", metavar_env_gc}, // never throws + {"mk_metavar", safe_function}, + {"get_timestamp", safe_function}, + {"get_context", safe_function}, + {"has_type", safe_function}, + {"get_type", safe_function}, + {"is_assigned", safe_function}, + {"assign", safe_function}, + {"get_subst", safe_function}, + {"get_justification", safe_function}, + {"get_subst_jst", safe_function}, + {"for_each_subst", safe_function}, + {"copy", safe_function}, + {0, 0} +}; + +static void open_metavar_env(lua_State * L) { + luaL_newmetatable(L, metavar_env_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, metavar_env_m, 0); + + SET_GLOBAL_FUN(mk_metavar_env, "metavar_env"); + SET_GLOBAL_FUN(metavar_env_pred, "is_metavar_env"); + SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars"); +} + + +void open_kernel_module(lua_State * L) { + open_level(L); + open_local_context(L); + open_expr(L); + open_context(L); + open_formatter(L); + open_environment(L); + open_object(L); + open_justification(L); + open_metavar_env(L); + open_io_state(L); + open_type_inferer(L); +} +} diff --git a/src/bindings/lua/environment.h b/src/library/kernel_bindings.h similarity index 53% rename from src/bindings/lua/environment.h rename to src/library/kernel_bindings.h index 3389d929e..e3e018387 100644 --- a/src/bindings/lua/environment.h +++ b/src/library/kernel_bindings.h @@ -5,12 +5,36 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "util/lua.h" #include "kernel/threadsafe_environment.h" namespace lean { +void open_kernel_module(lua_State * L); +UDATA_DEFS(level) +UDATA_DEFS(local_entry) +UDATA_DEFS_CORE(local_context) +UDATA_DEFS(expr); +UDATA_DEFS(context_entry) +UDATA_DEFS(context) +UDATA_DEFS(formatter) +UDATA_DEFS(object) UDATA_DEFS(environment) -void open_environment(lua_State * L); +UDATA_DEFS(justification) +UDATA_DEFS(metavar_env) +expr & to_nonnull_expr(lua_State * L, int idx); +/** + \brief Return the formatter object associated with the given Lua State. + This procedure checks for options at: + 1- Lean state object associated with \c L + 2- Lua Registry associated with \c L +*/ +formatter get_global_formatter(lua_State * L); +/** + \brief Update the formatter object associated with the given Lua State. + If \c L is associated with a Lean state object \c S, then we update the formatter of \c S. + Otherwise, we update the registry of \c L. +*/ +void set_global_formatter(lua_State * L, formatter const & fmt); /** \brief Auxiliary class for setting the Lua registry of a Lua state with an environment object. diff --git a/src/library/script_evaluator.h b/src/library/script_evaluator.h index d4961d050..4d917b3e6 100644 --- a/src/library/script_evaluator.h +++ b/src/library/script_evaluator.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "util/exception.h" +#include "util/script_exception.h" namespace lean { class environment; @@ -21,17 +21,4 @@ public: virtual void dostring(char const * str) = 0; virtual void dostring(char const * str, environment & env, io_state & st) = 0; }; - -/** - \brief Base class for exceptions producing when evaluating scripts. -*/ -class script_exception : public exception { -public: - enum class source { String, File, Unknown }; - virtual source get_source() const = 0; - virtual char const * get_filename() const = 0; - virtual unsigned get_line() const = 0; - virtual char const * get_msg() const noexcept = 0; - virtual char const * what() const noexcept; -}; } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 53c9e9564..ff3f1d26e 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,2 +1,4 @@ -add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp tactic.cpp boolean.cpp) +add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp +proof_state.cpp tactic.cpp boolean.cpp) + target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/bindings/lua/cex_builder.cpp b/src/library/tactic/cex_builder.cpp similarity index 86% rename from src/bindings/lua/cex_builder.cpp rename to src/library/tactic/cex_builder.cpp index 5948078d7..bb271f578 100644 --- a/src/bindings/lua/cex_builder.cpp +++ b/src/library/tactic/cex_builder.cpp @@ -4,24 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include -#include -#include "util/optional.h" -#include "kernel/environment.h" +#include "util/luaref.h" +#include "library/kernel_bindings.h" +#include "library/tactic/proof_builder.h" #include "library/tactic/cex_builder.h" -#include "bindings/lua/util.h" -#include "bindings/lua/name.h" -#include "bindings/lua/expr.h" -#include "bindings/lua/environment.h" -#include "bindings/lua/proof_builder.h" -#include "bindings/lua/lref.h" namespace lean { +cex_builder & cex_builder::operator=(cex_builder const & s) { LEAN_COPY_REF(cex_builder, s); } +cex_builder & cex_builder::operator=(cex_builder && s) { LEAN_MOVE_REF(cex_builder, s); } + DECL_UDATA(cex_builder) static int mk_cex_builder(lua_State * L) { luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun - lref ref(L, 1); + luaref ref(L, 1); return push_cex_builder(L, mk_cex_builder([=](name const & n, optional const & cex, assignment const & a) -> counterexample { ref.push(); // push user-fun on the stack diff --git a/src/library/tactic/cex_builder.h b/src/library/tactic/cex_builder.h index 7e28ec0c3..071bd7bfd 100644 --- a/src/library/tactic/cex_builder.h +++ b/src/library/tactic/cex_builder.h @@ -6,9 +6,11 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/lua.h" #include "util/debug.h" #include "util/name.h" #include "util/rc.h" +#include "util/optional.h" #include "kernel/expr.h" #include "kernel/environment.h" #include "library/tactic/assignment.h" @@ -55,8 +57,8 @@ public: cex_builder(cex_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~cex_builder() { if (m_ptr) m_ptr->dec_ref(); } friend void swap(cex_builder & a, cex_builder & b) { std::swap(a.m_ptr, b.m_ptr); } - cex_builder & operator=(cex_builder const & s) { LEAN_COPY_REF(cex_builder, s); } - cex_builder & operator=(cex_builder && s) { LEAN_MOVE_REF(cex_builder, s); } + cex_builder & operator=(cex_builder const & s); + cex_builder & operator=(cex_builder && s); counterexample operator()(name const & n, optional const & cex, assignment const & a) const { return m_ptr->operator()(n, cex, a); } }; @@ -65,4 +67,7 @@ template cex_builder mk_cex_builder(F && f) { return cex_builder(new cex_builder_tpl(std::forward(f))); } + +UDATA_DEFS(cex_builder) +void open_cex_builder(lua_State * L); } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index aebeb735a..7f3a6c43f 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/replace.h" #include "kernel/abstract.h" +#include "library/kernel_bindings.h" #include "library/type_inferer.h" #include "library/tactic/goal.h" @@ -151,4 +152,163 @@ std::pair to_goal(environment const & env, context const & return mk_pair(goal(reverse_to_list(hypotheses.begin(), hypotheses.end()), conclusion), goal_proof_fn(std::move(consts))); } + +DECL_UDATA(hypotheses) + +static int mk_hypotheses(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_hypotheses(L, hypotheses()); + } else if (nargs == 2) { + return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses())); + } else if (nargs == 3) { + return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), to_hypotheses(L, 3))); + } else { + throw exception("hypotheses functions expects 0 (empty list), 2 (name & expr for singleton hypotheses list), or 3 (name & expr & hypotheses list) arguments"); + } +} + +static int hypotheses_is_nil(lua_State * L) { + lua_pushboolean(L, !to_hypotheses(L, 1)); + return 1; +} + +static int hypotheses_head(lua_State * L) { + hypotheses const & hs = to_hypotheses(L, 1); + if (!hs) + throw exception("head method expects a non-empty hypotheses list"); + push_name(L, head(hs).first); + push_expr(L, head(hs).second); + return 2; +} + +static int hypotheses_tail(lua_State * L) { + hypotheses const & hs = to_hypotheses(L, 1); + if (!hs) + throw exception("tail method expects a non-empty hypotheses list"); + push_hypotheses(L, tail(hs)); + return 1; +} + +static int hypotheses_next(lua_State * L) { + hypotheses & hs = to_hypotheses(L, lua_upvalueindex(1)); + if (hs) { + push_hypotheses(L, tail(hs)); + lua_replace(L, lua_upvalueindex(1)); + push_name(L, head(hs).first); + push_expr(L, head(hs).second); + return 2; + } else { + lua_pushnil(L); + return 1; + } +} + +static int hypotheses_items(lua_State * L) { + hypotheses & hs = to_hypotheses(L, 1); + push_hypotheses(L, hs); // upvalue(1): hypotheses + lua_pushcclosure(L, &safe_function, 1); // create closure with 1 upvalue + return 1; +} + +static int hypotheses_len(lua_State * L) { + lua_pushinteger(L, length(to_hypotheses(L, 1))); + return 1; +} + +static const struct luaL_Reg hypotheses_m[] = { + {"__gc", hypotheses_gc}, // never throws + {"__len", safe_function}, + {"size", safe_function}, + {"pairs", safe_function}, + {"is_nil", safe_function}, + {"empty", safe_function}, + {"head", safe_function}, + {"tail", safe_function}, + {0, 0} +}; + +DECL_UDATA(goal) + +static int mk_goal(lua_State * L) { + return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); +} + +static int goal_is_null(lua_State * L) { + lua_pushboolean(L, !to_goal(L, 1)); + return 1; +} + +static int goal_hypotheses(lua_State * L) { + return push_hypotheses(L, to_goal(L, 1).get_hypotheses()); +} + +static int goal_conclusion(lua_State * L) { + return push_expr(L, to_goal(L, 1).get_conclusion()); +} + +static int goal_unique_name(lua_State * L) { + return push_name(L, to_goal(L, 1).mk_unique_hypothesis_name(to_name_ext(L, 2))); +} + +static int goal_tostring(lua_State * L) { + std::ostringstream out; + goal & g = to_goal(L, 1); + if (g) { + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(g.pp(fmt, opts), opts); + } else { + out << ""; + } + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int goal_pp(lua_State * L) { + int nargs = lua_gettop(L); + goal & g = to_goal(L, 1); + if (!g) { + return push_format(L, format()); + } else if (nargs == 1) { + return push_format(L, g.pp(get_global_formatter(L), get_global_options(L))); + } else if (nargs == 2) { + if (is_formatter(L, 2)) + return push_format(L, g.pp(to_formatter(L, 2), get_global_options(L))); + else + return push_format(L, g.pp(get_global_formatter(L), to_options(L, 2))); + } else { + return push_format(L, g.pp(to_formatter(L, 2), to_options(L, 3))); + } +} + +static const struct luaL_Reg goal_m[] = { + {"__gc", goal_gc}, // never throws + {"__tostring", safe_function}, + {"is_null", safe_function}, + {"hypotheses", safe_function}, + {"hyps", safe_function}, + {"conclusion", safe_function}, + {"unique_name", safe_function}, + {"pp", safe_function}, + {0, 0} +}; + +void open_goal(lua_State * L) { + luaL_newmetatable(L, hypotheses_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, hypotheses_m, 0); + + SET_GLOBAL_FUN(hypotheses_pred, "is_hypotheses"); + SET_GLOBAL_FUN(mk_hypotheses, "hypotheses"); + + luaL_newmetatable(L, goal_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, goal_m, 0); + + SET_GLOBAL_FUN(goal_pred, "is_goal"); + SET_GLOBAL_FUN(mk_goal, "goal"); +} } diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 5c446b4e4..fedded9bd 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include "util/lua.h" #include "util/list.h" #include "util/name.h" #include "kernel/formatter.h" @@ -64,4 +65,8 @@ public: to convert the proof for the goal into the proof term \c ?p. */ std::pair to_goal(environment const & env, context const & ctx, expr const & t); + +UDATA_DEFS_CORE(hypotheses) +UDATA_DEFS(goal) +void open_goal(lua_State * L); } diff --git a/src/library/tactic/open_module.h b/src/library/tactic/open_module.h new file mode 100644 index 000000000..4f0bb700f --- /dev/null +++ b/src/library/tactic/open_module.h @@ -0,0 +1,20 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/goal.h" +#include "library/tactic/proof_builder.h" +#include "library/tactic/cex_builder.h" +#include "library/tactic/proof_state.h" + +namespace lean { +inline void open_tactic_module(lua_State * L) { + open_goal(L); + open_proof_builder(L); + open_cex_builder(L); + open_proof_state(L); +} +} diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index 3cffbd1ea..cff29ab0c 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/src/library/tactic/proof_builder.cpp @@ -6,6 +6,8 @@ Author: Leonardo de Moura */ #include "util/exception.h" #include "util/sstream.h" +#include "util/luaref.h" +#include "library/kernel_bindings.h" #include "library/tactic/proof_builder.h" namespace lean { @@ -15,4 +17,112 @@ expr find(proof_map const & m, name const & n) { return *r; throw exception(sstream() << "proof for goal '" << n << "' not found"); } + +DECL_UDATA(proof_map) + +static int mk_proof_map(lua_State * L) { + return push_proof_map(L, proof_map()); +} + +static int proof_map_len(lua_State * L) { + lua_pushinteger(L, to_proof_map(L, 1).size()); + return 1; +} + +static int proof_map_find(lua_State * L) { + return push_expr(L, find(to_proof_map(L, 1), to_name_ext(L, 2))); +} + +static int proof_map_insert(lua_State * L) { + to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3)); + return 0; +} + +static int proof_map_erase(lua_State * L) { + to_proof_map(L, 1).erase(to_name_ext(L, 2)); + return 0; +} + +static const struct luaL_Reg proof_map_m[] = { + {"__gc", proof_map_gc}, // never throws + {"__len", safe_function}, + {"size", safe_function}, + {"find", safe_function}, + {"insert", safe_function}, + {"erase", safe_function}, + {0, 0} +}; + +DECL_UDATA(assignment); + +static int mk_assignment(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) + return push_assignment(L, assignment(metavar_env())); + else + return push_assignment(L, assignment(to_metavar_env(L, 1))); +} + +static int assignment_call(lua_State * L) { + return push_expr(L, to_assignment(L, 1)(to_name_ext(L, 2))); +} + +static const struct luaL_Reg assignment_m[] = { + {"__gc", assignment_gc}, // never throws + {"__call", safe_function}, + {0, 0} +}; + +DECL_UDATA(proof_builder); + +static int mk_proof_builder(lua_State * L) { + luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun + luaref ref(L, 1); + return push_proof_builder(L, + mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { + ref.push(); // push user-fun on the stack + push_proof_map(L, m); + push_assignment(L, a); + pcall(L, 2, 1, 0); + expr r = to_expr(L, -1); + lua_pop(L, 1); + return r; + })); +} + +static int proof_builder_call(lua_State * L) { + return push_expr(L, to_proof_builder(L, 1)(to_proof_map(L, 2), to_assignment(L, 3))); +} + +static const struct luaL_Reg proof_builder_m[] = { + {"__gc", proof_builder_gc}, // never throws + {"__call", safe_function}, + {0, 0} +}; + +void open_proof_builder(lua_State * L) { + luaL_newmetatable(L, proof_map_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, proof_map_m, 0); + + SET_GLOBAL_FUN(proof_map_pred, "is_proof_map"); + SET_GLOBAL_FUN(mk_proof_map, "proof_map"); + + luaL_newmetatable(L, assignment_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, assignment_m, 0); + + SET_GLOBAL_FUN(assignment_pred, "is_assignment"); + SET_GLOBAL_FUN(mk_assignment, "assignment"); + + luaL_newmetatable(L, proof_builder_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, proof_builder_m, 0); + + SET_GLOBAL_FUN(proof_builder_pred, "is_proof_builder"); + SET_GLOBAL_FUN(mk_proof_builder, "proof_builder"); +} } diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index 3c0f3744c..c1cf5b2f1 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/lua.h" #include "util/debug.h" #include "util/name.h" #include "util/splay_map.h" @@ -66,4 +67,9 @@ template proof_builder mk_proof_builder(F && f) { return proof_builder(new proof_builder_tpl(std::forward(f))); } + +UDATA_DEFS_CORE(proof_map) +UDATA_DEFS(assignment) +UDATA_DEFS(proof_builder) +void open_proof_builder(lua_State * L); } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 8084767d7..bb34fa076 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/sstream.h" #include "kernel/builtin.h" +#include "library/kernel_bindings.h" #include "library/tactic/proof_state.h" namespace lean { @@ -68,4 +69,199 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co }); return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder); } + +DECL_UDATA(goals) + +static int mk_goals(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_goals(L, goals()); + } else if (nargs == 2) { + return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), goals())); + } else if (nargs == 3) { + return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), to_goals(L, 3))); + } else { + throw exception("goals functions expects 0 (empty list), 2 (name & goal for singleton goal list), or 3 (name & goal & goal list) arguments"); + } +} + +static int goals_is_nil(lua_State * L) { + lua_pushboolean(L, !to_goals(L, 1)); + return 1; +} + +static int goals_head(lua_State * L) { + goals const & hs = to_goals(L, 1); + if (!hs) + throw exception("head method expects a non-empty goal list"); + push_name(L, head(hs).first); + push_goal(L, head(hs).second); + return 2; +} + +static int goals_tail(lua_State * L) { + goals const & hs = to_goals(L, 1); + if (!hs) + throw exception("tail method expects a non-empty goal list"); + push_goals(L, tail(hs)); + return 1; +} + +static int goals_next(lua_State * L) { + goals & hs = to_goals(L, lua_upvalueindex(1)); + if (hs) { + push_goals(L, tail(hs)); + lua_replace(L, lua_upvalueindex(1)); + push_name(L, head(hs).first); + push_goal(L, head(hs).second); + return 2; + } else { + lua_pushnil(L); + return 1; + } +} + +static int goals_items(lua_State * L) { + goals & hs = to_goals(L, 1); + push_goals(L, hs); // upvalue(1): goals + lua_pushcclosure(L, &safe_function, 1); // create closure with 1 upvalue + return 1; +} + +static int goals_len(lua_State * L) { + lua_pushinteger(L, length(to_goals(L, 1))); + return 1; +} + +static const struct luaL_Reg goals_m[] = { + {"__gc", goals_gc}, // never throws + {"__len", safe_function}, + {"size", safe_function}, + {"pairs", safe_function}, + {"is_nil", safe_function}, + {"empty", safe_function}, + {"head", safe_function}, + {"tail", safe_function}, + {0, 0} +}; + +DECL_UDATA(proof_state) + +static int mk_proof_state(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_proof_state(L, proof_state()); + } else if (nargs == 4) { + return push_proof_state(L, proof_state(to_goals(L, 1), to_metavar_env(L, 2), to_proof_builder(L, 3), to_cex_builder(L, 4))); + } else if (nargs == 3) { + return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3))); + } else { + throw exception("proof_state expectes 0, 3, or 4 arguments"); + } +} + +static int to_proof_state(lua_State * L) { + return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_expr(L, 3))); +} + +static int proof_state_tostring(lua_State * L) { + std::ostringstream out; + proof_state & s = to_proof_state(L, 1); + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(s.pp(fmt, opts), opts); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int proof_state_get_precision(lua_State * L) { + lua_pushinteger(L, static_cast(to_proof_state(L, 1).get_precision())); + return 1; +} + +static int proof_state_get_goals(lua_State * L) { + return push_goals(L, to_proof_state(L, 1).get_goals()); +} + +static int proof_state_get_menv(lua_State * L) { + return push_metavar_env(L, to_proof_state(L, 1).get_menv()); +} + +static int proof_state_get_proof_builder(lua_State * L) { + return push_proof_builder(L, to_proof_state(L, 1).get_proof_builder()); +} + +static int proof_state_get_cex_builder(lua_State * L) { + return push_cex_builder(L, to_proof_state(L, 1).get_cex_builder()); +} + +static int proof_state_is_proof_final_state(lua_State * L) { + lua_pushboolean(L, to_proof_state(L, 1).is_proof_final_state()); + return 1; +} + +static int proof_state_is_cex_final_state(lua_State * L) { + lua_pushboolean(L, to_proof_state(L, 1).is_cex_final_state()); + return 1; +} + +static int proof_state_pp(lua_State * L) { + int nargs = lua_gettop(L); + proof_state & s = to_proof_state(L, 1); + if (nargs == 1) { + return push_format(L, s.pp(get_global_formatter(L), get_global_options(L))); + } else if (nargs == 2) { + if (is_formatter(L, 2)) + return push_format(L, s.pp(to_formatter(L, 2), get_global_options(L))); + else + return push_format(L, s.pp(get_global_formatter(L), to_options(L, 2))); + } else { + return push_format(L, s.pp(to_formatter(L, 2), to_options(L, 3))); + } +} + +static const struct luaL_Reg proof_state_m[] = { + {"__gc", proof_state_gc}, // never throws + {"__tostring", safe_function}, + {"pp", safe_function}, + {"get_precision", safe_function}, + {"get_goals", safe_function}, + {"get_menv", safe_function}, + {"get_proof_builder", safe_function}, + {"get_cex_builder", safe_function}, + {"precision", safe_function}, + {"goals", safe_function}, + {"menv", safe_function}, + {"proof_builder", safe_function}, + {"cex_builder", safe_function}, + {"is_proof_final_state", safe_function}, + {"is_cex_final_state", safe_function}, + {0, 0} +}; + +void open_proof_state(lua_State * L) { + luaL_newmetatable(L, goals_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, goals_m, 0); + + SET_GLOBAL_FUN(goals_pred, "is_goals"); + SET_GLOBAL_FUN(mk_goals, "goals"); + + luaL_newmetatable(L, proof_state_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, proof_state_m, 0); + + SET_GLOBAL_FUN(proof_state_pred, "is_proof_state"); + SET_GLOBAL_FUN(mk_proof_state, "proof_state"); + SET_GLOBAL_FUN(to_proof_state, "to_proof_state"); + + lua_newtable(L); + SET_ENUM("Precise", precision::Precise); + SET_ENUM("Over", precision::Over); + SET_ENUM("Under", precision::Under); + SET_ENUM("UnderOver", precision::UnderOver); + lua_setglobal(L, "precision"); +} } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 34af333a0..2a2e8857b 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include "util/lua.h" #include "util/rc.h" #include "util/interrupt.h" #include "util/optional.h" @@ -95,4 +96,8 @@ goals map_goals(proof_state const & s, F && f) { } }); } + +UDATA_DEFS_CORE(goals) +UDATA_DEFS(proof_state) +void open_proof_state(lua_State * L); } diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 719b31403..7b3b6532c 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/free_vars.h" #include "kernel/metavar.h" +#include "library/kernel_bindings.h" #include "library/type_inferer.h" namespace lean { @@ -260,4 +261,48 @@ bool type_inferer::is_proposition(expr const & e, context const & ctx) { return m_ptr->is_proposition(e, ctx); } void type_inferer::clear() { m_ptr->clear(); } + +constexpr char const * type_inferer_mt = "type_inferer"; +type_inferer & to_type_inferer(lua_State * L, int i) { return *static_cast(luaL_checkudata(L, i, type_inferer_mt)); } +DECL_PRED(type_inferer) +DECL_GC(type_inferer) + +static int type_inferer_call(lua_State * L) { + int nargs = lua_gettop(L); + type_inferer & inferer = to_type_inferer(L, 1); + if (nargs == 2) + return push_expr(L, inferer(to_nonnull_expr(L, 2))); + else + return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3))); +} + +static int type_inferer_clear(lua_State * L) { + to_type_inferer(L, 1).clear(); + return 0; +} + +static int mk_type_inferer(lua_State * L) { + void * mem = lua_newuserdata(L, sizeof(type_inferer)); + new (mem) type_inferer(to_environment(L, 1)); + luaL_getmetatable(L, type_inferer_mt); + lua_setmetatable(L, -2); + return 1; +} + +static const struct luaL_Reg type_inferer_m[] = { + {"__gc", type_inferer_gc}, // never throws + {"__call", safe_function}, + {"clear", safe_function}, + {0, 0} +}; + +void open_type_inferer(lua_State * L) { + luaL_newmetatable(L, type_inferer_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, type_inferer_m, 0); + + SET_GLOBAL_FUN(mk_type_inferer, "type_inferer"); + SET_GLOBAL_FUN(type_inferer_pred, "is_type_inferer"); +} } diff --git a/src/library/type_inferer.h b/src/library/type_inferer.h index 42ae718bd..4e2c4a568 100644 --- a/src/library/type_inferer.h +++ b/src/library/type_inferer.h @@ -36,4 +36,6 @@ public: bool is_proposition(expr const & e, context const & ctx = context()); void clear(); }; + +void open_type_inferer(lua_State * L); } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 54e5c3319..c5f6775c7 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,3 +1,7 @@ add_library(util trace.cpp debug.cpp name.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp - ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp) + ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp + script_exception.cpp splay_map.cpp lua.cpp luaref.cpp + lua_exception.cpp) + +target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/bindings/lua/util.cpp b/src/util/lua.cpp similarity index 71% rename from src/bindings/lua/util.cpp rename to src/util/lua.cpp index 02fd0d568..461d19671 100644 --- a/src/bindings/lua/util.cpp +++ b/src/util/lua.cpp @@ -4,17 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include +#include #include #include -#include "kernel/kernel_exception.h" -#include "library/elaborator/elaborator_exception.h" -#include "bindings/lua/util.h" -#include "bindings/lua/lua_exception.h" -#include "bindings/lua/options.h" -#include "bindings/lua/format.h" -#include "bindings/lua/formatter.h" -#include "bindings/lua/justification.h" +#include +#include +#include "util/lua.h" +#include "util/lua_exception.h" namespace lean { /** @@ -92,15 +88,26 @@ static void exec(lua_State * L) { pcall(L, 0, LUA_MULTRET, 0); } -static void check_result(lua_State * L, int result) { +/** + \brief check_result for "customers" that are only using a subset + of Lean libraries. +*/ +void simple_check_result(lua_State * L, int result) { if (result) { - if (is_justification(L, -1)) - throw elaborator_exception(to_justification(L, -1)); - else - throw lua_exception(lua_tostring(L, -1)); + throw lua_exception(lua_tostring(L, -1)); } } +static void (*g_check_result)(lua_State *, int) = simple_check_result; + +static void check_result(lua_State * L, int result) { + g_check_result(L, result); +} + +set_check_result::set_check_result(void (*f)(lua_State *, int)) { + g_check_result = f; +} + void dofile(lua_State * L, char const * fname) { int result = luaL_loadfile(L, fname); check_result(L, result); @@ -118,16 +125,13 @@ void pcall(lua_State * L, int nargs, int nresults, int errorfun) { check_result(L, result); } -int safe_function_wrapper(lua_State * L, lua_CFunction f){ +/** + \brief Wrapper for "customers" that are only using a subset + of Lean libraries. +*/ +int simple_safe_function_wrapper(lua_State * L, lua_CFunction f){ try { return f(L); - } catch (kernel_exception & e) { - std::ostringstream out; - options o = get_global_options(L); - out << mk_pair(e.pp(get_global_formatter(L), o), o); - lua_pushstring(L, out.str().c_str()); - } catch (elaborator_exception & e) { - push_justification(L, e.get_justification()); } catch (exception & e) { lua_pushstring(L, e.what()); } catch (std::bad_alloc &) { @@ -139,4 +143,27 @@ int safe_function_wrapper(lua_State * L, lua_CFunction f){ } return lua_error(L); } + +int (*g_safe_function_wrapper)(lua_State * L, lua_CFunction f) = simple_safe_function_wrapper; + +set_safe_function_wrapper::set_safe_function_wrapper(int (*f)(lua_State *, lua_CFunction)) { + g_safe_function_wrapper = f; +} + +static std::unique_ptr> g_modules; + +lua_module::lua_module(init_fn f) { + if (!g_modules) { + g_modules.reset(new std::vector()); + } + g_modules->push_back(f); +} + +void lua_module::init(lua_State * L) { + if (g_modules) { + for (auto f : *g_modules) { + f(L); + } + } +} } diff --git a/src/bindings/lua/util.h b/src/util/lua.h similarity index 78% rename from src/bindings/lua/util.h rename to src/util/lua.h index 29aa5fde7..dd9b3b62e 100644 --- a/src/bindings/lua/util.h +++ b/src/util/lua.h @@ -8,6 +8,11 @@ Author: Leonardo de Moura #include namespace lean { +// ======================================= +// Lua 5.1 and 5.2 compatibility +// +// The following helper functions make sure +// we can compile using Lua 5.1 or 5.2 void setfuncs(lua_State * L, luaL_Reg const * l, int nup); bool testudata(lua_State * L, int idx, char const * mt); int load(lua_State * L, lua_Reader reader, void * data, char const * source); @@ -18,24 +23,49 @@ void pcall(lua_State * L, int nargs, int nresults, int errorfun); int lessthan(lua_State * L, int idx1, int idx2); int equal(lua_State * L, int idx1, int idx2); int get_nonnil_top(lua_State * L); +// ======================================= + +// ======================================= +// Goodies/Macros for automating Lua binding +// generation. +/** + \brief Helper class for registering a new + set of Lua bindings. +*/ +class lua_module { +public: + typedef void (*init_fn)(lua_State * L); + lua_module(init_fn f); + static void init(lua_State * L); +}; + /** \brief Wrapper for invoking function f, and catching Lean exceptions. */ -int safe_function_wrapper(lua_State * L, lua_CFunction f); +extern int (*g_safe_function_wrapper)(lua_State * L, lua_CFunction f); template int safe_function(lua_State * L) { - return safe_function_wrapper(L, F); + return g_safe_function_wrapper(L, F); } template void set_global_function(lua_State * L, char const * name) { lua_pushcfunction(L, safe_function); lua_setglobal(L, name); } +/** + \brief Helper object for setting g_safe_function_wrapper. +*/ +struct set_safe_function_wrapper { set_safe_function_wrapper(int (*f)(lua_State *, lua_CFunction)); }; + +/** + \brief Helper object for setting a different check_result function. +*/ +struct set_check_result { set_check_result(void (*f)(lua_State *, int)); }; #define SET_GLOBAL_FUN(F, N) set_global_function(L, N) // Auxiliary macro for creating a Lua table that stores enumeration values #define SET_ENUM(N, V) lua_pushstring(L, N); lua_pushinteger(L, static_cast(V)); lua_settable(L, -3) -#define DECL_PUSH_CORE(NAME, T, TREF) \ +#define DECL_PUSH_CORE(NAME, T, TREF) \ int push_ ## NAME(lua_State * L, TREF val) { \ void * mem = lua_newuserdata(L, sizeof(T)); \ new (mem) T(val); \ @@ -97,4 +127,5 @@ int push_ ## T(lua_State * L, T && e); #define UDATA_DEFS(T) \ class T; \ UDATA_DEFS_CORE(T) +// ======================================= } diff --git a/src/bindings/lua/lua_exception.cpp b/src/util/lua_exception.cpp similarity index 97% rename from src/bindings/lua/lua_exception.cpp rename to src/util/lua_exception.cpp index 7fa96ed4e..cda3b762a 100644 --- a/src/bindings/lua/lua_exception.cpp +++ b/src/util/lua_exception.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/debug.h" -#include "bindings/lua/lua_exception.h" +#include "util/lua_exception.h" namespace lean { lua_exception::lua_exception(char const * lua_error):script_exception() { diff --git a/src/bindings/lua/lua_exception.h b/src/util/lua_exception.h similarity index 95% rename from src/bindings/lua/lua_exception.h rename to src/util/lua_exception.h index f0842013c..b35dd6195 100644 --- a/src/bindings/lua/lua_exception.h +++ b/src/util/lua_exception.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "util/exception.h" -#include "library/script_evaluator.h" +#include "util/script_exception.h" namespace lean { /** diff --git a/src/bindings/lua/lref.cpp b/src/util/luaref.cpp similarity index 81% rename from src/bindings/lua/lref.cpp rename to src/util/luaref.cpp index 635e26f01..abd2dc82e 100644 --- a/src/bindings/lua/lref.cpp +++ b/src/util/luaref.cpp @@ -4,19 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/luaref.h" #include "util/debug.h" -#include "bindings/lua/util.h" -#include "bindings/lua/lref.h" namespace lean { -lref::lref(lua_State * L, int i) { +luaref::luaref(lua_State * L, int i) { lean_assert(L); m_state = L; lua_pushvalue(m_state, i); m_ref = luaL_ref(m_state, LUA_REGISTRYINDEX); } -lref::lref(lref const & r) { +luaref::luaref(luaref const & r) { m_state = r.m_state; if (m_state) { r.push(); @@ -24,18 +23,18 @@ lref::lref(lref const & r) { } } -lref::lref(lref && r) { +luaref::luaref(luaref && r) { m_state = r.m_state; m_ref = r.m_ref; r.m_state = nullptr; } -lref::~lref() { +luaref::~luaref() { if (m_state) luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref); } -lref & lref::operator=(lref const & r) { +luaref & luaref::operator=(luaref const & r) { if (m_ref == r.m_ref) return *this; if (m_state) @@ -48,12 +47,12 @@ lref & lref::operator=(lref const & r) { return *this; } -void lref::push() const { +void luaref::push() const { lean_assert(m_state); lua_rawgeti(m_state, LUA_REGISTRYINDEX, m_ref); } -int lref_lt_proc::operator()(lref const & r1, lref const & r2) const { +int luaref_lt_proc::operator()(luaref const & r1, luaref const & r2) const { lean_assert(r1.get_state() == r2.get_state()); lua_State * L = r1.get_state(); r1.push(); diff --git a/src/bindings/lua/lref.h b/src/util/luaref.h similarity index 57% rename from src/bindings/lua/lref.h rename to src/util/luaref.h index b3213cedd..d4abd696e 100644 --- a/src/bindings/lua/lref.h +++ b/src/util/luaref.h @@ -4,33 +4,34 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include +#include "util/lua.h" +#pragma once namespace lean { /** \brief Reference to Lua object. */ -class lref { +class luaref { lua_State * m_state; int m_ref; public: - lref():m_state(nullptr) {} + luaref():m_state(nullptr) {} /** \brief Create a reference to the Lua object at position \c i on \c L stack. */ - lref(lua_State * L, int i); - lref(lref const & r); - lref(lref && r); - ~lref(); - lref & operator=(lref const & r); + luaref(lua_State * L, int i); + luaref(luaref const & r); + luaref(luaref && r); + ~luaref(); + luaref & operator=(luaref const & r); void push() const; lua_State * get_state() const { return m_state; } }; /** - \brief '<' functor for lref. + \brief '<' functor for luaref. */ -struct lref_lt_proc { - int operator()(lref const & r1, lref const & r2) const; +struct luaref_lt_proc { + int operator()(luaref const & r1, luaref const & r2) const; }; } diff --git a/src/util/name.cpp b/src/util/name.cpp index fee811411..d428dd0a9 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include #include #include "util/name.h" +#include "util/sstream.h" #include "util/debug.h" #include "util/rc.h" #include "util/buffer.h" @@ -358,5 +359,84 @@ name operator+(name const & n1, name const & n2) { return name(prefix, n2.m_ptr->m_k); } } + +DECL_UDATA(name) + +static int mk_name(lua_State * L) { + int nargs = lua_gettop(L); + name r; + for (int i = 1; i <= nargs; i++) { + switch (lua_type(L, i)) { + case LUA_TNIL: break; // skip + case LUA_TNUMBER: r = name(r, lua_tointeger(L, i)); break; + case LUA_TSTRING: r = name(r, lua_tostring(L, i)); break; + case LUA_TUSERDATA: r = r + to_name(L, i); break; + default: throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer"); + } + } + return push_name(L, r); +} + +name to_name_ext(lua_State * L, int idx) { + if (lua_isstring(L, idx)) { + return luaL_checkstring(L, idx); + } else if (lua_istable(L, idx)) { + name r; + int n = objlen(L, idx); + for (int i = 1; i <= n; i++) { + lua_rawgeti(L, idx, i); + switch (lua_type(L, -1)) { + case LUA_TNIL: break; // skip + case LUA_TNUMBER: r = name(r, lua_tointeger(L, -1)); break; + case LUA_TSTRING: r = name(r, lua_tostring(L, -1)); break; + case LUA_TUSERDATA: r = r + to_name(L, -1); break; + default: throw exception("invalid array arguments, elements must be a hierarchical name, string, or integer"); + } + lua_pop(L, 1); + } + return r; + } else { + return to_name(L, idx); + } +} + +static int name_tostring(lua_State * L) { + lua_pushstring(L, to_name(L, 1).to_string().c_str()); + return 1; +} + +static int name_eq(lua_State * L) { + lua_pushboolean(L, to_name(L, 1) == to_name(L, 2)); + return 1; +} + +static int name_lt(lua_State * L) { + lua_pushboolean(L, to_name(L, 1) < to_name(L, 2)); + return 1; +} + +static int name_hash(lua_State * L) { + lua_pushinteger(L, to_name(L, 1).hash()); + return 1; +} + +static const struct luaL_Reg name_m[] = { + {"__gc", name_gc}, // never throws + {"__tostring", safe_function}, + {"__eq", safe_function}, + {"__lt", safe_function}, + {"hash", safe_function}, + {0, 0} +}; + +void open_name(lua_State * L) { + luaL_newmetatable(L, name_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, name_m, 0); + + SET_GLOBAL_FUN(mk_name, "name"); + SET_GLOBAL_FUN(name_pred, "is_name"); +} } void print(lean::name const & n) { std::cout << n << std::endl; } diff --git a/src/util/name.h b/src/util/name.h index c551478d8..fc8ee0d76 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/lua.h" namespace lean { constexpr char const * lean_name_separator = "::"; @@ -121,4 +122,8 @@ struct name_hash { unsigned operator()(name const & n) const { return n.hash(); struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } }; struct name_cmp { int operator()(name const & n1, name const & n2) const { return cmp(n1, n2); } }; struct name_quick_cmp { int operator()(name const & n1, name const & n2) const { return quick_cmp(n1, n2); } }; + +UDATA_DEFS(name) +name to_name_ext(lua_State * L, int idx); +void open_name(lua_State * L); } diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index d29e7ad4e..ffc5c3f22 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sstream.h" #include "util/numerics/mpq.h" #include "util/numerics/mpbq.h" @@ -122,6 +123,112 @@ mpq const & numeric_traits::zero() { lean_assert(is_zero(g_zero)); return g_zero; } + +DECL_UDATA(mpq) + +template +static mpq const & to_mpq(lua_State * L) { + static thread_local mpq arg; + switch (lua_type(L, idx)) { + case LUA_TNUMBER: arg = lua_tonumber(L, idx); return arg; + case LUA_TSTRING: arg = mpq(lua_tostring(L, idx)); return arg; + case LUA_TUSERDATA: + if (is_mpz(L, idx)) { + arg = mpq(to_mpz(L, idx)); + return arg; + } else { + return *static_cast(luaL_checkudata(L, idx, mpq_mt)); + } + default: throw exception(sstream() << "arg #" << idx << " must be a number, string, mpz or mpq"); + } +} + +mpq to_mpq_ext(lua_State * L, int idx) { + switch (lua_type(L, idx)) { + case LUA_TNUMBER: return mpq(lua_tonumber(L, idx)); + case LUA_TSTRING: return mpq(lua_tostring(L, idx)); + case LUA_TUSERDATA: + if (is_mpz(L, idx)) { + return mpq(to_mpz(L, idx)); + } else { + return *static_cast(luaL_checkudata(L, idx, mpq_mt)); + } + default: throw exception(sstream() << "arg #" << idx << " must be a number, string, mpz or mpq"); + } +} + +static int mpq_tostring(lua_State * L) { + mpq * n = static_cast(luaL_checkudata(L, 1, mpq_mt)); + std::ostringstream out; + out << *n; + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int mpq_eq(lua_State * L) { + lua_pushboolean(L, to_mpq<1>(L) == to_mpq<2>(L)); + return 1; +} + +static int mpq_lt(lua_State * L) { + lua_pushboolean(L, to_mpq<1>(L) < to_mpq<2>(L)); + return 1; +} + +static int mpq_add(lua_State * L) { + return push_mpq(L, to_mpq<1>(L) + to_mpq<2>(L)); +} + +static int mpq_sub(lua_State * L) { + return push_mpq(L, to_mpq<1>(L) - to_mpq<2>(L)); +} + +static int mpq_mul(lua_State * L) { + return push_mpq(L, to_mpq<1>(L) * to_mpq<2>(L)); +} + +static int mpq_div(lua_State * L) { + mpq const & arg2 = to_mpq<2>(L); + if (arg2 == 0) throw exception("division by zero"); + return push_mpq(L, to_mpq<1>(L) / arg2); +} + +static int mpq_umn(lua_State * L) { + return push_mpq(L, 0 - to_mpq<1>(L)); +} + +static int mpq_power(lua_State * L) { + int k = luaL_checkinteger(L, 2); + if (k < 0) throw exception("argument #2 must be positive"); + return push_mpq(L, pow(to_mpq<1>(L), k)); +} + +static int mk_mpq(lua_State * L) { + mpq const & arg = to_mpq<1>(L); + return push_mpq(L, arg); +} + +static const struct luaL_Reg mpq_m[] = { + {"__gc", mpq_gc}, // never throws + {"__tostring", safe_function}, + {"__eq", safe_function}, + {"__lt", safe_function}, + {"__add", safe_function}, + {"__sub", safe_function}, + {"__mul", safe_function}, + {"__div", safe_function}, + {"__pow", safe_function}, + {"__unm", safe_function}, + {0, 0} +}; + +void open_mpq(lua_State * L) { + luaL_newmetatable(L, mpq_mt); + setfuncs(L, mpq_m, 0); + + SET_GLOBAL_FUN(mk_mpq, "mpq"); + SET_GLOBAL_FUN(mpq_pred, "is_mpq"); +} } void print(lean::mpq const & v) { std::cout << v << std::endl; } diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h index 5664d41f7..c3f3b3a6a 100644 --- a/src/util/numerics/mpq.h +++ b/src/util/numerics/mpq.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lua.h" #include "util/numerics/mpz.h" namespace lean { @@ -276,4 +277,7 @@ public: static void atanh(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE }; +UDATA_DEFS(mpq) +mpq to_mpq_ext(lua_State * L, int idx); +void open_mpq(lua_State * L); } diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp index 33d9f9de7..fc07db87e 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/numerics/mpz.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/sstream.h" #include "util/numerics/mpz.h" namespace lean { @@ -81,6 +82,101 @@ mpz const & numeric_traits::zero() { lean_assert(is_zero(g_zero)); return g_zero; } + +DECL_UDATA(mpz) + +template +static mpz const & to_mpz(lua_State * L) { + static thread_local mpz arg; + switch (lua_type(L, idx)) { + case LUA_TNUMBER: arg = static_cast(lua_tointeger(L, idx)); return arg; + case LUA_TSTRING: arg = mpz(lua_tostring(L, idx)); return arg; + case LUA_TUSERDATA: return *static_cast(luaL_checkudata(L, idx, mpz_mt)); + default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz"); + } +} + +mpz to_mpz_ext(lua_State * L, int idx) { + switch (lua_type(L, idx)) { + case LUA_TNUMBER: return mpz(static_cast(lua_tointeger(L, idx))); + case LUA_TSTRING: return mpz(lua_tostring(L, idx)); + case LUA_TUSERDATA: return *static_cast(luaL_checkudata(L, idx, mpz_mt)); + default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz"); + } +} + +static int mpz_tostring(lua_State * L) { + mpz * n = static_cast(luaL_checkudata(L, 1, mpz_mt)); + std::ostringstream out; + out << *n; + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int mpz_eq(lua_State * L) { + lua_pushboolean(L, to_mpz<1>(L) == to_mpz<2>(L)); + return 1; +} + +static int mpz_lt(lua_State * L) { + lua_pushboolean(L, to_mpz<1>(L) < to_mpz<2>(L)); + return 1; +} + +static int mpz_add(lua_State * L) { + return push_mpz(L, to_mpz<1>(L) + to_mpz<2>(L)); +} + +static int mpz_sub(lua_State * L) { + return push_mpz(L, to_mpz<1>(L) - to_mpz<2>(L)); +} + +static int mpz_mul(lua_State * L) { + return push_mpz(L, to_mpz<1>(L) * to_mpz<2>(L)); +} + +static int mpz_div(lua_State * L) { + mpz const & arg2 = to_mpz<2>(L); + if (arg2 == 0) throw exception("division by zero"); + return push_mpz(L, to_mpz<1>(L) / arg2); +} + +static int mpz_umn(lua_State * L) { + return push_mpz(L, 0 - to_mpz<1>(L)); +} + +static int mpz_power(lua_State * L) { + int k = luaL_checkinteger(L, 2); + if (k < 0) throw exception("argument #2 must be positive"); + return push_mpz(L, pow(to_mpz<1>(L), k)); +} + +static int mk_mpz(lua_State * L) { + mpz const & arg = to_mpz<1>(L); + return push_mpz(L, arg); +} + +static const struct luaL_Reg mpz_m[] = { + {"__gc", mpz_gc}, // never throws + {"__tostring", safe_function}, + {"__eq", safe_function}, + {"__lt", safe_function}, + {"__add", safe_function}, + {"__sub", safe_function}, + {"__mul", safe_function}, + {"__div", safe_function}, + {"__pow", safe_function}, + {"__unm", safe_function}, + {0, 0} +}; + +void open_mpz(lua_State * L) { + luaL_newmetatable(L, mpz_mt); + setfuncs(L, mpz_m, 0); + + SET_GLOBAL_FUN(mk_mpz, "mpz"); + SET_GLOBAL_FUN(mpz_pred, "is_mpz"); +} } void print(lean::mpz const & n) { std::cout << n << std::endl; } diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h index 5d2c18282..a8e42876c 100644 --- a/src/util/numerics/mpz.h +++ b/src/util/numerics/mpz.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/debug.h" +#include "util/lua.h" #include "util/numerics/numeric_traits.h" namespace lean { @@ -234,4 +235,8 @@ public: static void power(mpz & v, unsigned k) { _power(v, v, k); } static mpz const & zero(); }; + +UDATA_DEFS(mpz) +mpz to_mpz_ext(lua_State * L, int idx); +void open_mpz(lua_State * L); } diff --git a/src/bindings/lua/expr.h b/src/util/numerics/open_module.h similarity index 56% rename from src/bindings/lua/expr.h rename to src/util/numerics/open_module.h index 36ecb648e..2ca166036 100644 --- a/src/bindings/lua/expr.h +++ b/src/util/numerics/open_module.h @@ -5,9 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "util/numerics/mpz.h" +#include "util/numerics/mpq.h" + namespace lean { -UDATA_DEFS(expr); -expr & to_nonnull_expr(lua_State * L, int idx); -void open_expr(lua_State * L); +inline void open_numerics_module(lua_State * L) { + open_mpz(L); + open_mpq(L); +} } diff --git a/src/bindings/lua/cex_builder.h b/src/util/open_module.h similarity index 58% rename from src/bindings/lua/cex_builder.h rename to src/util/open_module.h index 5fa93e089..da7332332 100644 --- a/src/bindings/lua/cex_builder.h +++ b/src/util/open_module.h @@ -5,8 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "util/name.h" +#include "util/splay_map.h" + namespace lean { -UDATA_DEFS(cex_builder) -void open_cex_builder(lua_State * L); +inline void open_util_module(lua_State * L) { + open_name(L); + open_splay_map(L); +} } diff --git a/src/library/script_evaluator.cpp b/src/util/script_exception.cpp similarity index 94% rename from src/library/script_evaluator.cpp rename to src/util/script_exception.cpp index 741ca36f6..9accf6e3d 100644 --- a/src/library/script_evaluator.cpp +++ b/src/util/script_exception.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include -#include "library/script_evaluator.h" +#include "util/script_exception.h" namespace lean { char const * script_exception::what() const noexcept { diff --git a/src/util/script_exception.h b/src/util/script_exception.h new file mode 100644 index 000000000..d1e65a9c8 --- /dev/null +++ b/src/util/script_exception.h @@ -0,0 +1,23 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/exception.h" + +namespace lean { +/** + \brief Base class for exceptions producing when evaluating scripts. +*/ +class script_exception : public exception { +public: + enum class source { String, File, Unknown }; + virtual source get_source() const = 0; + virtual char const * get_filename() const = 0; + virtual unsigned get_line() const = 0; + virtual char const * get_msg() const noexcept = 0; + virtual char const * what() const noexcept; +}; +} diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index ec21dcb71..bd54ad86e 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -6,8 +6,12 @@ */ #include #include +#include #include +#include "util/sstream.h" #include "util/escaped.h" +#include "util/numerics/mpz.h" +#include "util/numerics/mpq.h" #include "util/sexpr/sexpr.h" #include "util/sexpr/format.h" #include "util/sexpr/sexpr_fn.h" @@ -438,4 +442,102 @@ struct sexpr_pp_fn { format pp(sexpr const & s) { return sexpr_pp_fn()(s); } + +DECL_UDATA(format) + +format to_format_elem(lua_State * L, int idx) { + if (is_format(L, idx)) + return to_format(L, idx); + else if (lua_isnumber(L, idx)) + return format(static_cast(lua_tonumber(L, idx))); + else if (is_name(L, idx)) + return format(to_name(L, idx)); + else if (is_mpz(L, idx)) + return format(to_mpz(L, idx)); + else if (is_mpq(L, idx)) + return format(to_mpq(L, idx)); + else + return format(lua_tostring(L, idx)); +} + +static int format_tostring(lua_State * L) { + std::ostringstream out; + out << mk_pair(to_format(L, 1), get_global_options(L)); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int format_concat(lua_State * L) { + return push_format(L, compose(to_format_elem(L, 1), to_format_elem(L, 2))); +} + +static int mk_format(lua_State * L) { + format r; + int nargs = lua_gettop(L); + if (nargs == 0) { + r = format(); + } else { + int i = nargs; + r = to_format_elem(L, i); + i--; + for (; i >= 1; i--) { + r = compose(to_format_elem(L, i), r); + } + } + return push_format(L, r); +} + +static int format_nest(lua_State * L) { + return push_format(L, nest(luaL_checkinteger(L, 2), to_format(L, 1))); +} + +static int format_group(lua_State * L) { + return push_format(L, group(to_format(L, 1))); +} + +static int format_highlight(lua_State * L) { + char const * color_str = luaL_checkstring(L, 2); + format::format_color color; + if (strcmp(color_str, "red") == 0) { + color = format::RED; + } else if (strcmp(color_str, "green") == 0) { + color = format::GREEN; + } else if (strcmp(color_str, "orange") == 0) { + color = format::ORANGE; + } else if (strcmp(color_str, "blue") == 0) { + color = format::BLUE; + } else if (strcmp(color_str, "cyan") == 0) { + color = format::CYAN; + } else if (strcmp(color_str, "grey") == 0) { + color = format::GREY; + } else { + throw exception(sstream() << "unknown color '" << color_str << "'"); + } + return push_format(L, highlight(to_format(L, 1), color)); +} + +static int format_line(lua_State * L) { return push_format(L, line()); } +static int format_space(lua_State * L) { return push_format(L, space()); } + +static const struct luaL_Reg format_m[] = { + {"__gc", format_gc}, // never throws + {"__tostring", safe_function}, + {"__concat", safe_function}, + {"nest", safe_function}, + {"group", safe_function}, + {"highlight", safe_function}, + {0, 0} +}; + +void open_format(lua_State * L) { + luaL_newmetatable(L, format_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, format_m, 0); + + SET_GLOBAL_FUN(mk_format, "format"); + SET_GLOBAL_FUN(format_line, "line"); + SET_GLOBAL_FUN(format_space, "space"); + SET_GLOBAL_FUN(format_pred, "is_format"); +} } diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 2f8b362bc..75fbf8a04 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -13,6 +13,7 @@ Author: Soonho Kong #include #include "util/pair.h" #include "util/debug.h" +#include "util/lua.h" #include "util/numerics/mpz.h" #include "util/sexpr/sexpr.h" @@ -317,4 +318,7 @@ format pp(name const & n); /** \brief Format a S-expression */ format pp(sexpr const & s, options const & o); format pp(sexpr const & s); + +UDATA_DEFS(format) +void open_format(lua_State * L); } diff --git a/src/util/sexpr/open_module.h b/src/util/sexpr/open_module.h new file mode 100644 index 000000000..b341f5b25 --- /dev/null +++ b/src/util/sexpr/open_module.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/sexpr/sexpr.h" +#include "util/sexpr/options.h" +#include "util/sexpr/format.h" + +namespace lean { +inline void open_sexpr_module(lua_State * L) { + open_sexpr(L); + open_options(L); + open_format(L); +} +} diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index a1d8a82df..efbafb6fb 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include "util/sstream.h" #include "util/sexpr/options.h" #include "util/sexpr/option_declarations.h" #include "util/sexpr/sexpr_fn.h" @@ -170,4 +171,218 @@ std::ostream & operator<<(std::ostream & out, options const & o) { out << (unicode ? g_right_angle_bracket : ")"); return out; } + +DECL_UDATA(options) + +static int mk_options(lua_State * L) { + options r; + int nargs = lua_gettop(L); + if (nargs % 2 != 0) + throw exception("options expects an even number of arguments"); + for (int i = 1; i < nargs; i+=2) { + name k = to_name_ext(L, i); + auto it = get_option_declarations().find(k); + if (it == get_option_declarations().end()) { + throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); + } else { + option_declaration const & d = it->second; + switch (d.kind()) { + case BoolOption: r = r.update(k, static_cast(lua_toboolean(L, i+1))); break; + case IntOption: r = r.update(k, static_cast(lua_tointeger(L, i+1))); break; + case UnsignedOption: r = r.update(k, static_cast(lua_tointeger(L, i+1))); break; + case DoubleOption: r = r.update(k, static_cast(lua_tonumber(L, i+1))); break; + case StringOption: r = r.update(k, lua_tostring(L, i+1)); break; + default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'"); + } + } + } + return push_options(L, r); +} + +static int options_tostring(lua_State * L) { + std::ostringstream out; + out << to_options(L, 1); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int options_size(lua_State * L) { + lua_pushinteger(L, to_options(L, 1).size()); + return 1; +} + +static int options_contains(lua_State * L) { + lua_pushboolean(L, to_options(L, 1).contains(to_name_ext(L, 2))); + return 1; +} + +static int options_empty(lua_State * L) { + lua_pushboolean(L, to_options(L, 1).empty()); + return 1; +} + +static int options_get_bool(lua_State * L) { + int nargs = lua_gettop(L); + bool defval = nargs < 3 ? false : lua_toboolean(L, 3); + lua_pushboolean(L, to_options(L, 1).get_bool(to_name_ext(L, 2), defval)); + return 1; +} + +static int options_get_int(lua_State * L) { + int nargs = lua_gettop(L); + int defval = nargs < 3 ? 0 : lua_tointeger(L, 3); + lua_pushinteger(L, to_options(L, 1).get_int(to_name_ext(L, 2), defval)); + return 1; +} + +static int options_get_unsigned(lua_State * L) { + int nargs = lua_gettop(L); + unsigned defval = nargs < 3 ? 0 : lua_tointeger(L, 3); + lua_pushnumber(L, to_options(L, 1).get_unsigned(to_name_ext(L, 2), defval)); + return 1; +} + +static int options_get_double(lua_State * L) { + int nargs = lua_gettop(L); + double defval = nargs < 3 ? 0.0 : lua_tonumber(L, 3); + lua_pushnumber(L, to_options(L, 1).get_double(to_name_ext(L, 2), defval)); + return 1; +} + +static int options_get_string(lua_State * L) { + int nargs = lua_gettop(L); + char const * defval = nargs < 3 ? "" : lua_tostring(L, 3); + lua_pushstring(L, to_options(L, 1).get_string(to_name_ext(L, 2), defval)); + return 1; +} + +static int options_update_bool(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), static_cast(lua_toboolean(L, 3)))); +} + +static int options_update_int(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), static_cast(lua_tointeger(L, 3)))); +} + +static int options_update_unsigned(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), static_cast(lua_tointeger(L, 3)))); +} + +static int options_update_double(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), lua_tonumber(L, 3))); +} + +static int options_update_string(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_name_ext(L, 2), lua_tostring(L, 3))); +} + +static int options_get(lua_State * L) { + name k = to_name_ext(L, 2); + auto it = get_option_declarations().find(k); + if (it == get_option_declarations().end()) { + throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); + } else { + option_declaration const & d = it->second; + switch (d.kind()) { + case BoolOption: return options_get_bool(L); + case IntOption: return options_get_int(L); + case UnsignedOption: return options_get_unsigned(L); + case DoubleOption: return options_get_double(L); + case StringOption: return options_get_string(L); + default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'"); + } + } +} + +int options_update(lua_State * L) { + name k = to_name_ext(L, 2); + auto it = get_option_declarations().find(k); + if (it == get_option_declarations().end()) { + throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'"); + } else { + option_declaration const & d = it->second; + switch (d.kind()) { + case BoolOption: return options_update_bool(L); + case IntOption: return options_update_int(L); + case UnsignedOption: return options_update_unsigned(L); + case DoubleOption: return options_update_double(L); + case StringOption: return options_update_string(L); + default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'"); + } + } +} + +static const struct luaL_Reg options_m[] = { + {"__gc", options_gc}, // never throws + {"__tostring", safe_function}, + {"__len", safe_function }, + {"contains", safe_function}, + {"size", safe_function}, + {"empty", safe_function}, + {"get", safe_function}, + {"update", safe_function}, + // low-level API + {"get_bool", safe_function}, + {"get_int", safe_function}, + {"get_unsigned", safe_function}, + {"get_double", safe_function}, + {"get_string", safe_function}, + {"update_bool", safe_function}, + {"update_int", safe_function}, + {"update_unsigned", safe_function}, + {"update_double", safe_function}, + {"update_string", safe_function}, + {0, 0} +}; + +static char g_options_key; + +options get_global_options(lua_State * L) { + lua_pushlightuserdata(L, static_cast(&g_options_key)); + lua_gettable(L, LUA_REGISTRYINDEX); + options r; + if (is_options(L, -1)) + r = to_options(L, -1); + lua_pop(L, 1); + return r; +} + +void set_global_options(lua_State * L, options const & o) { + lua_pushlightuserdata(L, static_cast(&g_options_key)); + push_options(L, o); + lua_settable(L, LUA_REGISTRYINDEX); +} + +static int _get_global_options(lua_State * L) { + return push_options(L, get_global_options(L)); +} + +static int _set_global_options(lua_State * L) { + options o = to_options(L, 1); + set_global_options(L, o); + return 0; +} + +static int _set_global_option(lua_State * L) { + options o = get_global_options(L); + push_options(L, o); + lua_insert(L, 1); + options_update(L); + o = to_options(L, -1); + set_global_options(L, o); + return 0; +} + +void open_options(lua_State * L) { + luaL_newmetatable(L, options_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, options_m, 0); + + SET_GLOBAL_FUN(mk_options, "options"); + SET_GLOBAL_FUN(options_pred, "is_options"); + SET_GLOBAL_FUN(_get_global_options, "get_options"); + SET_GLOBAL_FUN(_set_global_options, "set_options"); + SET_GLOBAL_FUN(_set_global_option, "set_option"); +} } diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index 6d3429358..c7f831b46 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/sexpr/sexpr.h" #include "util/sexpr/format.h" +#include "util/lua.h" namespace lean { enum option_kind { BoolOption, IntOption, UnsignedOption, DoubleOption, StringOption, SExprOption }; @@ -74,4 +75,21 @@ struct mk_option_declaration { #define RegisterOptionCore(N, K, D, DESC) RegisterOption(N, K, #D, DESC) #define RegisterBoolOption(N, D, DESC) RegisterOptionCore(N, BoolOption, D, DESC); #define RegisterUnsignedOption(N, D, DESC) RegisterOptionCore(N, UnsignedOption, D, DESC); + +UDATA_DEFS(options) +int options_update(lua_State * L); +/** + \brief Return the set of options associated with the given Lua State. + This procedure checks for options at: + 1- Lean state object associated with \c L + 2- Lua Registry associated with \c L +*/ +options get_global_options(lua_State * L); +/** + \brief Update the set of options associated with the given Lua State. + If \c L is associated with a Lean state object \c S, then we update the options of \c S. + Otherwise, we update the registry of \c L. +*/ +void set_global_options(lua_State * L, options const & o); +void open_options(lua_State * L); } diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index 7ed410a74..00dde2bb6 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include #include #include "util/rc.h" @@ -289,6 +290,223 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) { bool operator==(sexpr const & a, name const & b) { return is_name(a) && to_name(a) == b; } bool operator==(sexpr const & a, mpz const & b) { return is_mpz(a) && to_mpz(a) == b; } bool operator==(sexpr const & a, mpq const & b) { return is_mpq(a) && to_mpq(a) == b; } + +DECL_UDATA(sexpr) + +static int sexpr_tostring(lua_State * L) { + std::ostringstream out; + out << to_sexpr(L, 1); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static sexpr to_sexpr_elem(lua_State * L, int idx) { + if (lua_isnil(L, idx)) { + return sexpr(); + } else if (lua_isboolean(L, idx)) { + return sexpr(static_cast(lua_toboolean(L, idx))); + } else if (lua_isnumber(L, idx)) { + // Remark: we convert to integer by default + return sexpr(static_cast(lua_tointeger(L, idx))); + } else if (is_name(L, idx)) { + return sexpr(to_name(L, idx)); + } else if (is_sexpr(L, idx)) { + return *static_cast(lua_touserdata(L, idx)); + } else if (is_mpz(L, idx)) { + return sexpr(to_mpz(L, idx)); + } else if (is_mpq(L, idx)) { + return sexpr(to_mpq(L, idx)); + } else { + return sexpr(lua_tostring(L, idx)); + } +} + +static int mk_sexpr(lua_State * L) { + sexpr r; + int nargs = lua_gettop(L); + if (nargs == 0) { + r = sexpr(); + } else { + int i = nargs; + r = to_sexpr_elem(L, i); + i--; + for (; i >= 1; i--) { + r = sexpr(to_sexpr_elem(L, i), r); + } + } + return push_sexpr(L, r); +} + +static int sexpr_eq(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); return 1; } +static int sexpr_lt(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); return 1; } + +#define SEXPR_PRED(P) \ +static int sexpr_ ## P(lua_State * L) { \ + lua_pushboolean(L, P(to_sexpr(L, 1))); \ + return 1; \ +} + +SEXPR_PRED(is_nil) +SEXPR_PRED(is_cons) +SEXPR_PRED(is_list) +SEXPR_PRED(is_atom) +SEXPR_PRED(is_string) +SEXPR_PRED(is_bool) +SEXPR_PRED(is_int) +SEXPR_PRED(is_double) +SEXPR_PRED(is_name) +SEXPR_PRED(is_mpz) +SEXPR_PRED(is_mpq) + +static int sexpr_length(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_list(e)) + throw exception("s-expression is not a list"); + lua_pushinteger(L, length(e)); + return 1; +} + +static int sexpr_head(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_cons(e)) + throw exception("s-expression is not a cons cell"); + return push_sexpr(L, head(e)); +} + +static int sexpr_tail(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_cons(e)) + throw exception("s-expression is not a cons cell"); + return push_sexpr(L, tail(e)); +} + +static int sexpr_to_bool(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_bool(e)) + throw exception("s-expression is not a Boolean"); + lua_pushboolean(L, to_bool(e)); + return 1; +} + +static int sexpr_to_string(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_string(e)) + throw exception("s-expression is not a string"); + lua_pushstring(L, to_string(e).c_str()); + return 1; +} + +static int sexpr_to_int(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_int(e)) + throw exception("s-expression is not an integer"); + lua_pushinteger(L, to_int(e)); + return 1; +} + +static int sexpr_to_double(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_double(e)) + throw exception("s-expression is not a double"); + lua_pushnumber(L, to_double(e)); + return 1; +} + +static int sexpr_to_name(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_name(e)) + throw exception("s-expression is not a name"); + return push_name(L, to_name(e)); +} + +static int sexpr_to_mpz(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_mpz(e)) + throw exception("s-expression is not a multi-precision integer"); + return push_mpz(L, to_mpz(e)); +} + +static int sexpr_to_mpq(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + if (!is_mpq(e)) + throw exception("s-expression is not a multi-precision rational"); + return push_mpq(L, to_mpq(e)); +} + +static int sexpr_get_kind(lua_State * L) { + lua_pushinteger(L, static_cast(to_sexpr(L, 1).kind())); + return 1; +} + +static int sexpr_fields(lua_State * L) { + sexpr const & e = to_sexpr(L, 1); + switch (e.kind()) { + case sexpr_kind::Nil: return 0; + case sexpr_kind::String: return sexpr_to_string(L); + case sexpr_kind::Bool: return sexpr_to_bool(L); + case sexpr_kind::Int: return sexpr_to_int(L); + case sexpr_kind::Double: return sexpr_to_double(L); + case sexpr_kind::Name: return sexpr_to_name(L); + case sexpr_kind::MPZ: return sexpr_to_mpz(L); + case sexpr_kind::MPQ: return sexpr_to_mpq(L); + case sexpr_kind::Cons: sexpr_head(L); sexpr_tail(L); return 2; + } + lean_unreachable(); // LCOV_EXCL_LINE + return 0; // LCOV_EXCL_LINE +} + +static const struct luaL_Reg sexpr_m[] = { + {"__gc", sexpr_gc}, // never throws + {"__tostring", safe_function}, + {"__eq", safe_function}, + {"__lt", safe_function}, + {"kind", safe_function}, + {"is_nil", safe_function}, + {"is_cons", safe_function}, + {"is_list", safe_function}, + {"is_atom", safe_function}, + {"is_string", safe_function}, + {"is_bool", safe_function}, + {"is_int", safe_function}, + {"is_double", safe_function}, + {"is_name", safe_function}, + {"is_mpz", safe_function}, + {"is_mpq", safe_function}, + {"head", safe_function}, + {"tail", safe_function}, + {"length", safe_function}, + {"to_bool", safe_function}, + {"to_string", safe_function}, + {"to_int", safe_function}, + {"to_double", safe_function}, + {"to_name", safe_function}, + {"to_mpz", safe_function}, + {"to_mpq", safe_function}, + {"fields", safe_function}, + {0, 0} +}; + +void open_sexpr(lua_State * L) { + luaL_newmetatable(L, sexpr_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, sexpr_m, 0); + + SET_GLOBAL_FUN(mk_sexpr, "sexpr"); + SET_GLOBAL_FUN(sexpr_pred, "is_sexpr"); + + lua_newtable(L); + SET_ENUM("Nil", sexpr_kind::Nil); + SET_ENUM("String", sexpr_kind::String); + SET_ENUM("Bool", sexpr_kind::Bool); + SET_ENUM("Int", sexpr_kind::Int); + SET_ENUM("Double", sexpr_kind::Double); + SET_ENUM("Name", sexpr_kind::Name); + SET_ENUM("MPZ", sexpr_kind::MPZ); + SET_ENUM("MPQ", sexpr_kind::MPQ); + SET_ENUM("Cons", sexpr_kind::Cons); + lua_setglobal(L, "sexpr_kind"); +} } void print(lean::sexpr const & n) { std::cout << n << "\n"; } diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h index 97c12d430..cfaa6c6ad 100644 --- a/src/util/sexpr/sexpr.h +++ b/src/util/sexpr/sexpr.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/lua.h" namespace lean { class name; @@ -158,4 +159,6 @@ inline bool operator>(sexpr const & a, sexpr const & b) { return cmp(a, b) > 0; inline bool operator<=(sexpr const & a, sexpr const & b) { return cmp(a, b) <= 0; } inline bool operator>=(sexpr const & a, sexpr const & b) { return cmp(a, b) >= 0; } +UDATA_DEFS(sexpr) +void open_sexpr(lua_State * L); } diff --git a/src/bindings/lua/splay_map.cpp b/src/util/splay_map.cpp similarity index 86% rename from src/bindings/lua/splay_map.cpp rename to src/util/splay_map.cpp index 903a27706..1d41a1e54 100644 --- a/src/bindings/lua/splay_map.cpp +++ b/src/util/splay_map.cpp @@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include +#include "util/lua.h" +#include "util/luaref.h" #include "util/splay_map.h" -#include "bindings/lua/util.h" -#include "bindings/lua/lref.h" namespace lean { -typedef splay_map lua_splay_map; - +typedef splay_map lua_splay_map; DECL_UDATA(lua_splay_map) static int mk_lua_splay_map(lua_State * L) { @@ -25,7 +23,7 @@ static int lua_splay_map_size(lua_State * L) { } static int lua_splay_map_contains(lua_State * L) { - lua_pushboolean(L, to_lua_splay_map(L, 1).contains(lref(L, 2))); + lua_pushboolean(L, to_lua_splay_map(L, 1).contains(luaref(L, 2))); return 1; } @@ -35,18 +33,18 @@ static int lua_splay_map_empty(lua_State * L) { } static int lua_splay_map_insert(lua_State * L) { - to_lua_splay_map(L, 1).insert(lref(L, 2), lref(L, 3)); + to_lua_splay_map(L, 1).insert(luaref(L, 2), luaref(L, 3)); return 0; } static int lua_splay_map_erase(lua_State * L) { - to_lua_splay_map(L, 1).erase(lref(L, 2)); + to_lua_splay_map(L, 1).erase(luaref(L, 2)); return 0; } static int lua_splay_map_find(lua_State * L) { lua_splay_map & m = to_lua_splay_map(L, 1); - lref * val = m.splay_find(lref(L, 2)); + luaref * val = m.splay_find(luaref(L, 2)); if (val) { lean_assert(val->get_state() == L); val->push(); @@ -67,7 +65,7 @@ static int lua_splay_map_for_each(lua_State * L) { // The copy operation is very cheap O(1). lua_splay_map m(to_lua_splay_map(L, 1)); // map luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun - m.for_each([&](lref const & k, lref const & v) { + m.for_each([&](luaref const & k, luaref const & v) { lua_pushvalue(L, 2); // push user-fun k.push(); v.push(); diff --git a/src/util/splay_map.h b/src/util/splay_map.h index 044031a7c..eb702e588 100644 --- a/src/util/splay_map.h +++ b/src/util/splay_map.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/lua.h" #include "util/pair.h" #include "util/splay_tree.h" @@ -114,4 +115,6 @@ void for_each(splay_map const & m, F f) { "for_each: return type of f is not void"); return m.for_each(f); } + +void open_splay_map(lua_State * L); }