michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(bindings/lua): move Lua bindings to the file associated with them

Browse source 
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-26 19:15:49 -08:00
parent 99a811a586
commit 956f203a55
95 changed files with 3470 additions and 3774 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -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})

9
src/bindings/lua/CMakeLists.txt
View file

@ -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})

119
src/bindings/lua/context.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<context_entry_get_name>},
{"get_domain", safe_function<context_entry_get_domain>},
{"get_body", safe_function<context_entry_get_body>},
{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<context_tostring>},
{"__len", safe_function<context_size>},
{"is_empty", safe_function<context_is_empty>},
{"size", safe_function<context_size>},
{"extend", safe_function<context_extend>},
{"lookup", safe_function<context_lookup>},
{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");
}
}

13
src/bindings/lua/context.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(context_entry)
UDATA_DEFS(context)
void open_context(lua_State * L);
}

284
src/bindings/lua/environment.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<environment_next_object>, 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<environment_tostring>},
{"mk_child", safe_function<environment_mk_child>},
{"has_parent", safe_function<environment_has_parent>},
{"has_children", safe_function<environment_has_children>},
{"parent", safe_function<environment_parent>},
{"add_uvar", safe_function<environment_add_uvar>},
{"is_ge", safe_function<environment_is_ge>},
{"get_uvar", safe_function<environment_get_uvar>},
{"add_definition", safe_function<environment_add_definition>},
{"add_theorem", safe_function<environment_add_theorem>},
{"add_var", safe_function<environment_add_var>},
{"add_axiom", safe_function<environment_add_axiom>},
{"find_object", safe_function<environment_find_object>},
{"has_object", safe_function<environment_has_object>},
{"check_type", safe_function<environment_check_type>},
{"infer_type", safe_function<environment_infer_type>},
{"normalize", safe_function<environment_normalize>},
{"objects", safe_function<environment_objects>},
{"local_objects", safe_function<environment_local_objects>},
{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<void *>(&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<void *>(&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<void *>(&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");
}
}

480
src/bindings/lua/expr.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#include <utility>
#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 << "<null-expr>";
}
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<expr> 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<expr, expr> 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<MkAbst1 F1, MkAbst2 F2>
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<Fun, Fun>(L); }
static int expr_pi(lua_State * L) { return expr_abst<Pi, Pi>(L); }
static int expr_let(lua_State * L) { return expr_abst<Let, Let>(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<int>(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<expr_next_arg>, 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<int>(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<decltype(f)> 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<expr> & 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<expr> 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<expr> 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<expr_tostring>},
{"__eq", safe_function<expr_eq>},
{"__lt", safe_function<expr_lt>},
{"__call", safe_function<expr_mk_app>},
{"kind", safe_function<expr_get_kind>},
{"is_null", safe_function<expr_is_null>},
{"is_var", safe_function<expr_is_var>},
{"is_constant", safe_function<expr_is_constant>},
{"is_app", safe_function<expr_is_app>},
{"is_eq", safe_function<expr_is_eq>},
{"is_lambda", safe_function<expr_is_lambda>},
{"is_pi", safe_function<expr_is_pi>},
{"is_abstraction", safe_function<expr_is_abstraction>},
{"is_let", safe_function<expr_is_let>},
{"is_value", safe_function<expr_is_value>},
{"is_metavar", safe_function<expr_is_metavar>},
{"fields", safe_function<expr_fields>},
{"data", safe_function<expr_fields>},
{"args", safe_function<expr_args>},
{"num_args", safe_function<expr_num_args>},
{"arg", safe_function<expr_arg>},
{"for_each", safe_function<expr_for_each>},
{"has_free_vars", safe_function<expr_has_free_vars>},
{"closed", safe_function<expr_closed>},
{"has_free_var", safe_function<expr_has_free_var>},
{"lift_free_vars", safe_function<expr_lift_free_vars>},
{"lower_free_vars", safe_function<expr_lower_free_vars>},
{"instantiate", safe_function<expr_instantiate>},
{"abstract", safe_function<expr_abstract>},
{"occurs", safe_function<expr_occurs>},
{"has_metavar", safe_function<expr_has_metavar>},
{"is_eqp", safe_function<expr_is_eqp>},
{"hash", safe_function<expr_hash>},
{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");
}
}

117
src/bindings/lua/format.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#include <cstring>
#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<int>(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<format_tostring>},
{"__concat", safe_function<format_concat>},
{"nest", safe_function<format_nest>},
{"group", safe_function<format_group>},
{"highlight", safe_function<format_highlight>},
{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");
}
}

12
src/bindings/lua/format.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(format)
void open_format(lua_State * L);
}

111
src/bindings/lua/formatter.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<formatter_call>},
{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<void *>(&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<void *>(&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");
}
}

25
src/bindings/lua/formatter.h
View file

@ -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 <lua.hpp>
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);
}

10
src/bindings/lua/frontend_lean.cpp
View file

@ -5,15 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <sstream>
#include <lua.hpp>
#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 {

176
src/bindings/lua/goal.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<hypotheses_next>, 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<hypotheses_len>},
{"size", safe_function<hypotheses_len>},
{"pairs", safe_function<hypotheses_items>},
{"is_nil", safe_function<hypotheses_is_nil>},
{"empty", safe_function<hypotheses_is_nil>},
{"head", safe_function<hypotheses_head>},
{"tail", safe_function<hypotheses_tail>},
{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 << "<null-goal>";
}
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<goal_tostring>},
{"is_null", safe_function<goal_is_null>},
{"hypotheses", safe_function<goal_hypotheses>},
{"hyps", safe_function<goal_hypotheses>},
{"conclusion", safe_function<goal_conclusion>},
{"unique_name", safe_function<goal_unique_name>},
{"pp", safe_function<goal_pp>},
{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");
}
}

14
src/bindings/lua/goal.h
View file

@ -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 <lua.hpp>
#include "library/tactic/goal.h"
namespace lean {
UDATA_DEFS_CORE(hypotheses)
UDATA_DEFS(goal)
void open_goal(lua_State * L);
}

100
src/bindings/lua/io_state.cpp
View file

@ -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 <lua.hpp>
#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<io_state_get_options>},
{"set_options", safe_function<io_state_set_options>},
{"get_formatter", safe_function<io_state_get_formatter>},
{"print_diagnostic", safe_function<io_state_print_diagnostic>},
{"print_regular", safe_function<io_state_print_regular>},
{"print", safe_function<io_state_print_regular>},
{"diagnostic", safe_function<io_state_print_diagnostic>},
{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<void *>(&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<void *>(&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<void *>(&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<io_state*>(lua_touserdata(L, -1));
lua_pop(L, 1);
return r;
}
}
}

30
src/bindings/lua/io_state.h
View file

@ -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 <lua.hpp>
#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);
}

143
src/bindings/lua/justification.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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 << "<null-justification>";
}
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<justification_cell*> 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<justification_next_child>, 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<justification_tostring>},
{"is_null", safe_function<justification_is_null>},
{"has_children", safe_function<justification_has_children>},
{"children", safe_function<justification_children>},
{"get_main_expr", safe_function<justification_get_main_expr>},
{"pp", safe_function<justification_pp>},
{"depends_on", safe_function<justification_depends_on>},
{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");
}
}

12
src/bindings/lua/justification.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(justification)
void open_justification(lua_State * L);
}

167
src/bindings/lua/leanlua_state.cpp
View file

@ -9,43 +9,72 @@ Author: Leonardo de Moura
#include <thread>
#include <chrono>
#include <string>
#include <lua.hpp>
#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<std::mutex> 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) {

2
src/bindings/lua/leanlua_state.h
View file

@ -7,8 +7,8 @@ Author: Leonardo de Moura
#pragma once
#include <memory>
#include <lua.hpp>
#include "util/lua_exception.h"
#include "library/script_evaluator.h"
#include "bindings/lua/lua_exception.h"
namespace lean {
class environment;

139
src/bindings/lua/level.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<int>(kind(to_level(L, 1))));
return 1;
}
static const struct luaL_Reg level_m[] = {
{"__gc", level_gc}, // never throws
{"__tostring", safe_function<level_tostring>},
{"__eq", safe_function<level_eq>},
{"__lt", safe_function<level_lt>},
{"kind", safe_function<level_get_kind>},
{"is_bottom", safe_function<level_is_bottom>},
{"is_lift", safe_function<level_is_lift>},
{"is_max", safe_function<level_is_max>},
{"is_uvar", safe_function<level_is_uvar>},
{"uvar_name", safe_function<level_name>},
{"lift_of", safe_function<level_lift_of>},
{"lift_offset", safe_function<level_lift_offset>},
{"max_size", safe_function<level_max_size>},
{"max_level", safe_function<level_max_level>},
{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");
}
}

12
src/bindings/lua/level.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(level)
void open_level(lua_State * L);
}

120
src/bindings/lua/local_context.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<local_entry_eq>},
{"is_lift", safe_function<local_entry_is_lift>},
{"is_inst", safe_function<local_entry_is_inst>},
{"s", safe_function<local_entry_s>},
{"n", safe_function<local_entry_n>},
{"v", safe_function<local_entry_v>},
{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");
}
}

14
src/bindings/lua/local_context.h
View file

@ -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 <lua.hpp>
#include "kernel/expr.h"
namespace lean {
UDATA_DEFS(local_entry)
UDATA_DEFS_CORE(local_context)
void open_local_context(lua_State * L);
}

167
src/bindings/lua/metavar_env.cpp
View file

@ -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 <lua.hpp>
#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<menv_mk_metavar>},
{"get_timestamp", safe_function<menv_get_timestamp>},
{"get_context", safe_function<menv_get_context>},
{"has_type", safe_function<menv_has_type>},
{"get_type", safe_function<menv_get_type>},
{"is_assigned", safe_function<menv_is_assigned>},
{"assign", safe_function<menv_assign>},
{"get_subst", safe_function<menv_get_subst>},
{"get_justification", safe_function<menv_get_justification>},
{"get_subst_jst", safe_function<menv_get_subst_jst>},
{"for_each_subst", safe_function<menv_for_each_subst>},
{"copy", safe_function<menv_copy>},
{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");
}
}

12
src/bindings/lua/metavar_env.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(metavar_env)
void open_metavar_env(lua_State * L);
}

92
src/bindings/lua/name.cpp
View file

@ -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 <lua.hpp>
#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<name_tostring>},
{"__eq", safe_function<name_eq>},
{"__lt", safe_function<name_lt>},
{"hash", safe_function<name_hash>},
{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");
}
}

13
src/bindings/lua/name.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(name)
void open_name(lua_State * L);
name to_name_ext(lua_State * L, int idx);
}

216
src/bindings/lua/numerics.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<unsigned idx>
static mpz const & to_mpz(lua_State * L) {
static thread_local mpz arg;
switch (lua_type(L, idx)) {
case LUA_TNUMBER: arg = static_cast<long>(lua_tointeger(L, idx)); return arg;
case LUA_TSTRING: arg = mpz(lua_tostring(L, idx)); return arg;
case LUA_TUSERDATA: return *static_cast<mpz*>(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<long>(lua_tointeger(L, idx)));
case LUA_TSTRING: return mpz(lua_tostring(L, idx));
case LUA_TUSERDATA: return *static_cast<mpz*>(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<mpz*>(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<mpz_tostring>},
{"__eq", safe_function<mpz_eq>},
{"__lt", safe_function<mpz_lt>},
{"__add", safe_function<mpz_add>},
{"__sub", safe_function<mpz_sub>},
{"__mul", safe_function<mpz_mul>},
{"__div", safe_function<mpz_div>},
{"__pow", safe_function<mpz_power>},
{"__unm", safe_function<mpz_umn>},
{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<unsigned idx>
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<idx>(L));
return arg;
} else {
return *static_cast<mpq*>(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<mpq*>(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<mpq*>(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<mpq_tostring>},
{"__eq", safe_function<mpq_eq>},
{"__lt", safe_function<mpq_lt>},
{"__add", safe_function<mpq_add>},
{"__sub", safe_function<mpq_sub>},
{"__mul", safe_function<mpq_mul>},
{"__div", safe_function<mpq_div>},
{"__pow", safe_function<mpq_power>},
{"__unm", safe_function<mpq_umn>},
{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");
}
}

154
src/bindings/lua/object.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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 << "<null-kernel-object>";
lua_pushstring(L, out.str().c_str());
return 1;
}
static const struct luaL_Reg object_m[] = {
{"__gc", object_gc}, // never throws
{"__tostring", safe_function<object_tostring>},
{"is_null", safe_function<object_is_null>},
{"keyword", safe_function<object_keyword>},
{"has_name", safe_function<object_has_name>},
{"get_name", safe_function<object_get_name>},
{"has_type", safe_function<object_has_type>},
{"get_type", safe_function<object_get_type>},
{"has_cnstr_level", safe_function<object_has_cnstr_level>},
{"get_cnstr_level", safe_function<object_get_cnstr_level>},
{"is_definition", safe_function<object_is_definition>},
{"is_opaque", safe_function<object_is_opaque>},
{"get_value", safe_function<object_get_value>},
{"get_weight", safe_function<object_get_weight>},
{"is_axiom", safe_function<object_is_axiom>},
{"is_theorem", safe_function<object_is_theorem>},
{"is_var_decl", safe_function<object_is_var_decl>},
{"is_builtin", safe_function<object_is_builtin>},
{"is_builtin_set", safe_function<object_is_builtin_set>},
{"in_builtin_set", safe_function<object_in_builtin_set>},
{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");
}
}

12
src/bindings/lua/object.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(object)
void open_object(lua_State * L);
}

242
src/bindings/lua/options.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<bool>(lua_toboolean(L, i+1))); break;
case IntOption: r = r.update(k, static_cast<int>(lua_tointeger(L, i+1))); break;
case UnsignedOption: r = r.update(k, static_cast<unsigned>(lua_tointeger(L, i+1))); break;
case DoubleOption: r = r.update(k, static_cast<double>(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<bool>(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<int>(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<unsigned>(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<void *>(&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<void *>(&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<options_tostring>},
{"__len", safe_function<options_size> },
{"contains", safe_function<options_contains>},
{"size", safe_function<options_size>},
{"empty", safe_function<options_empty>},
{"get", safe_function<options_get>},
{"update", safe_function<options_update>},
// low-level API
{"get_bool", safe_function<options_get_bool>},
{"get_int", safe_function<options_get_int>},
{"get_unsigned", safe_function<options_get_unsigned>},
{"get_double", safe_function<options_get_double>},
{"get_string", safe_function<options_get_string>},
{"update_bool", safe_function<options_update_bool>},
{"update_int", safe_function<options_update_int>},
{"update_unsigned", safe_function<options_update_unsigned>},
{"update_double", safe_function<options_update_double>},
{"update_string", safe_function<options_update_string>},
{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");
}
}

25
src/bindings/lua/options.h
View file

@ -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 <lua.hpp>
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);
}

124
src/bindings/lua/proof_builder.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<proof_map_len>},
{"size", safe_function<proof_map_len>},
{"find", safe_function<proof_map_find>},
{"insert", safe_function<proof_map_insert>},
{"erase", safe_function<proof_map_erase>},
{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<assignment_call>},
{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<proof_builder_call>},
{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");
}
}

15
src/bindings/lua/proof_builder.h
View file

@ -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 <lua.hpp>
#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);
}

218
src/bindings/lua/proof_state.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<goals_next>, 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<goals_len>},
{"size", safe_function<goals_len>},
{"pairs", safe_function<goals_items>},
{"is_nil", safe_function<goals_is_nil>},
{"empty", safe_function<goals_is_nil>},
{"head", safe_function<goals_head>},
{"tail", safe_function<goals_tail>},
{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<int>(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<proof_state_tostring>},
{"pp", safe_function<proof_state_pp>},
{"get_precision", safe_function<proof_state_get_precision>},
{"get_goals", safe_function<proof_state_get_goals>},
{"get_menv", safe_function<proof_state_get_menv>},
{"get_proof_builder", safe_function<proof_state_get_proof_builder>},
{"get_cex_builder", safe_function<proof_state_get_cex_builder>},
{"precision", safe_function<proof_state_get_precision>},
{"goals", safe_function<proof_state_get_goals>},
{"menv", safe_function<proof_state_get_menv>},
{"proof_builder", safe_function<proof_state_get_proof_builder>},
{"cex_builder", safe_function<proof_state_get_cex_builder>},
{"is_proof_final_state", safe_function<proof_state_is_proof_final_state>},
{"is_cex_final_state", safe_function<proof_state_is_cex_final_state>},
{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");
}
}

14
src/bindings/lua/proof_state.h
View file

@ -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 <lua.hpp>
#include "library/tactic/proof_state.h"
namespace lean {
UDATA_DEFS_CORE(goals)
UDATA_DEFS(proof_state)
void open_proof_state(lua_State * L);
}

232
src/bindings/lua/sexpr.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<bool>(lua_toboolean(L, idx)));
} else if (lua_isnumber(L, idx)) {
// Remark: we convert to integer by default
return sexpr(static_cast<int>(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<sexpr*>(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<int>(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<sexpr_tostring>},
{"__eq", safe_function<sexpr_eq>},
{"__lt", safe_function<sexpr_lt>},
{"kind", safe_function<sexpr_get_kind>},
{"is_nil", safe_function<sexpr_is_nil>},
{"is_cons", safe_function<sexpr_is_cons>},
{"is_list", safe_function<sexpr_is_list>},
{"is_atom", safe_function<sexpr_is_atom>},
{"is_string", safe_function<sexpr_is_string>},
{"is_bool", safe_function<sexpr_is_bool>},
{"is_int", safe_function<sexpr_is_int>},
{"is_double", safe_function<sexpr_is_double>},
{"is_name", safe_function<sexpr_is_name>},
{"is_mpz", safe_function<sexpr_is_mpz>},
{"is_mpq", safe_function<sexpr_is_mpq>},
{"head", safe_function<sexpr_head>},
{"tail", safe_function<sexpr_tail>},
{"length", safe_function<sexpr_length>},
{"to_bool", safe_function<sexpr_to_bool>},
{"to_string", safe_function<sexpr_to_string>},
{"to_int", safe_function<sexpr_to_int>},
{"to_double", safe_function<sexpr_to_double>},
{"to_name", safe_function<sexpr_to_name>},
{"to_mpz", safe_function<sexpr_to_mpz>},
{"to_mpq", safe_function<sexpr_to_mpq>},
{"fields", safe_function<sexpr_fields>},
{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");
}
}

12
src/bindings/lua/sexpr.h
View file

@ -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 <lua.hpp>
namespace lean {
UDATA_DEFS(sexpr)
void open_sexpr(lua_State * L);
}

11
src/bindings/lua/splay_map.h
View file

@ -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 <lua.hpp>
namespace lean {
void open_splay_map(lua_State * L);
}

59
src/bindings/lua/type_inferer.cpp
View file

@ -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 <sstream>
#include <lua.hpp>
#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<type_inferer*>(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<type_inferer_call>},
{"clear", safe_function<type_inferer_clear>},
{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");
}
}

11
src/bindings/lua/type_inferer.h
View file

@ -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 <lua.hpp>
namespace lean {
void open_type_inferer(lua_State * L);
}

1
src/kernel/expr.cpp
View file

@ -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) {

2
src/kernel/expr.h
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include <limits>
#include <utility>
#include <tuple>
#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 */

1
src/kernel/threadsafe_environment.h
View file

@ -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"

6
src/library/CMakeLists.txt
View file

@ -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})

11
src/library/arith/int.cpp
View file

@ -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");
}
}

3
src/library/arith/int.h
View file

@ -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);
}

14
src/library/arith/nat.cpp
View file

@ -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");
}
}

3
src/library/arith/nat.h
View file

@ -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);
}

17
src/bindings/lua/numerics.h → src/library/arith/open_module.h
View file

@ -5,13 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <lua.hpp>
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);
}
}

11
src/library/arith/real.cpp
View file

@ -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");
}
}

3
src/library/arith/real.h
View file

@ -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);
}

142
src/library/io_state.cpp
View file

@ -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<std::mutex> 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<io_state_get_options>},
{"set_options", safe_function<io_state_set_options>},
{"get_formatter", safe_function<io_state_get_formatter>},
{"print_diagnostic", safe_function<io_state_print_diagnostic>},
{"print_regular", safe_function<io_state_print_regular>},
{"print", safe_function<io_state_print_regular>},
{"diagnostic", safe_function<io_state_print_diagnostic>},
{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<void *>(&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<void *>(&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<void *>(&g_set_state_key));
lua_gettable(L, LUA_REGISTRYINDEX);
if (lua_islightuserdata(L, -1)) {
io_state * r = static_cast<io_state*>(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;
}
}

20
src/library/io_state.h
View file

@ -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);
}

1547
src/library/kernel_bindings.cpp Normal file
View file

File diff suppressed because it is too large Load diff

28
src/bindings/lua/environment.h → src/library/kernel_bindings.h
View file

@ -5,12 +5,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <lua.hpp>
#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.

15
src/library/script_evaluator.h
View file

@ -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;
};
}

4
src/library/tactic/CMakeLists.txt
View file

@ -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})

18
src/bindings/lua/cex_builder.cpp → src/library/tactic/cex_builder.cpp
View file

@ -4,24 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <sstream>
#include <lua.hpp>
#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<counterexample> const & cex, assignment const & a) -> counterexample {
ref.push(); // push user-fun on the stack

9
src/library/tactic/cex_builder.h
View file

@ -6,9 +6,11 @@ Author: Leonardo de Moura
*/
#pragma once
#include <algorithm>
#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<counterexample> const & cex, assignment const & a) const { return m_ptr->operator()(n, cex, a); }
};
@ -65,4 +67,7 @@ template<typename F>
cex_builder mk_cex_builder(F && f) {
return cex_builder(new cex_builder_tpl<F>(std::forward<F>(f)));
}
UDATA_DEFS(cex_builder)
void open_cex_builder(lua_State * L);
}

160
src/library/tactic/goal.cpp
View file

@ -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<goal, goal_proof_fn> 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<hypotheses_next>, 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<hypotheses_len>},
{"size", safe_function<hypotheses_len>},
{"pairs", safe_function<hypotheses_items>},
{"is_nil", safe_function<hypotheses_is_nil>},
{"empty", safe_function<hypotheses_is_nil>},
{"head", safe_function<hypotheses_head>},
{"tail", safe_function<hypotheses_tail>},
{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 << "<null-goal>";
}
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<goal_tostring>},
{"is_null", safe_function<goal_is_null>},
{"hypotheses", safe_function<goal_hypotheses>},
{"hyps", safe_function<goal_hypotheses>},
{"conclusion", safe_function<goal_conclusion>},
{"unique_name", safe_function<goal_unique_name>},
{"pp", safe_function<goal_pp>},
{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");
}
}

5
src/library/tactic/goal.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <utility>
#include <vector>
#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<goal, goal_proof_fn> to_goal(environment const & env, context const & ctx, expr const & t);
UDATA_DEFS_CORE(hypotheses)
UDATA_DEFS(goal)
void open_goal(lua_State * L);
}

20
src/library/tactic/open_module.h Normal file
View file

@ -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);
}
}

110
src/library/tactic/proof_builder.cpp
View file

@ -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<proof_map_len>},
{"size", safe_function<proof_map_len>},
{"find", safe_function<proof_map_find>},
{"insert", safe_function<proof_map_insert>},
{"erase", safe_function<proof_map_erase>},
{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<assignment_call>},
{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<proof_builder_call>},
{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");
}
}

6
src/library/tactic/proof_builder.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include <algorithm>
#include "util/lua.h"
#include "util/debug.h"
#include "util/name.h"
#include "util/splay_map.h"
@ -66,4 +67,9 @@ template<typename F>
proof_builder mk_proof_builder(F && f) {
return proof_builder(new proof_builder_tpl<F>(std::forward<F>(f)));
}
UDATA_DEFS_CORE(proof_map)
UDATA_DEFS(assignment)
UDATA_DEFS(proof_builder)
void open_proof_builder(lua_State * L);
}

196
src/library/tactic/proof_state.cpp
View file

@ -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<goals_next>, 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<goals_len>},
{"size", safe_function<goals_len>},
{"pairs", safe_function<goals_items>},
{"is_nil", safe_function<goals_is_nil>},
{"empty", safe_function<goals_is_nil>},
{"head", safe_function<goals_head>},
{"tail", safe_function<goals_tail>},
{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<int>(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<proof_state_tostring>},
{"pp", safe_function<proof_state_pp>},
{"get_precision", safe_function<proof_state_get_precision>},
{"get_goals", safe_function<proof_state_get_goals>},
{"get_menv", safe_function<proof_state_get_menv>},
{"get_proof_builder", safe_function<proof_state_get_proof_builder>},
{"get_cex_builder", safe_function<proof_state_get_cex_builder>},
{"precision", safe_function<proof_state_get_precision>},
{"goals", safe_function<proof_state_get_goals>},
{"menv", safe_function<proof_state_get_menv>},
{"proof_builder", safe_function<proof_state_get_proof_builder>},
{"cex_builder", safe_function<proof_state_get_cex_builder>},
{"is_proof_final_state", safe_function<proof_state_is_proof_final_state>},
{"is_cex_final_state", safe_function<proof_state_is_cex_final_state>},
{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");
}
}

5
src/library/tactic/proof_state.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <utility>
#include <algorithm>
#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);
}

45
src/library/type_inferer.cpp
View file

@ -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<type_inferer*>(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<type_inferer_call>},
{"clear", safe_function<type_inferer_clear>},
{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");
}
}

2
src/library/type_inferer.h
View file

@ -36,4 +36,6 @@ public:
bool is_proposition(expr const & e, context const & ctx = context());
void clear();
};
void open_type_inferer(lua_State * L);
}

6
src/util/CMakeLists.txt
View file

@ -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})

71
src/bindings/lua/util.cpp → src/util/lua.cpp
View file

@ -4,17 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <lua.hpp>
#include <iostream>
#include <string>
#include <sstream>
#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 <vector>
#include <memory>
#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<std::vector<lua_module::init_fn>> g_modules;
lua_module::lua_module(init_fn f) {
if (!g_modules) {
g_modules.reset(new std::vector<init_fn>());
}
g_modules->push_back(f);
}
void lua_module::init(lua_State * L) {
if (g_modules) {
for (auto f : *g_modules) {
f(L);
}
}
}
}

37
src/bindings/lua/util.h → src/util/lua.h
View file

@ -8,6 +8,11 @@ Author: Leonardo de Moura
#include <lua.hpp>
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<lua_CFunction F> int safe_function(lua_State * L) {
return safe_function_wrapper(L, F);
return g_safe_function_wrapper(L, F);
}
template<lua_CFunction F> void set_global_function(lua_State * L, char const * name) {
lua_pushcfunction(L, safe_function<F>);
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<F>(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<int>(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)
// =======================================
}

2
src/bindings/lua/lua_exception.cpp → src/util/lua_exception.cpp
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <string>
#include <cstdlib>
#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() {

2
src/bindings/lua/lua_exception.h → src/util/lua_exception.h
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <string>
#include "util/exception.h"
#include "library/script_evaluator.h"
#include "util/script_exception.h"
namespace lean {
/**

17
src/bindings/lua/lref.cpp → src/util/luaref.cpp
View file

@ -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();

23
src/bindings/lua/lref.h → src/util/luaref.h
View file

@ -4,33 +4,34 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <lua.hpp>
#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;
};
}

80
src/util/name.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include <string>
#include <atomic>
#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<name_tostring>},
{"__eq", safe_function<name_eq>},
{"__lt", safe_function<name_lt>},
{"hash", safe_function<name_hash>},
{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; }

5
src/util/name.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <string>
#include <iostream>
#include <algorithm>
#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);
}

107
src/util/numerics/mpq.cpp
View file

@ -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<mpq>::zero() {
lean_assert(is_zero(g_zero));
return g_zero;
}
DECL_UDATA(mpq)
template<int idx>
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<mpq*>(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<mpq*>(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<mpq*>(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<mpq_tostring>},
{"__eq", safe_function<mpq_eq>},
{"__lt", safe_function<mpq_lt>},
{"__add", safe_function<mpq_add>},
{"__sub", safe_function<mpq_sub>},
{"__mul", safe_function<mpq_mul>},
{"__div", safe_function<mpq_div>},
{"__pow", safe_function<mpq_power>},
{"__unm", safe_function<mpq_umn>},
{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; }

4
src/util/numerics/mpq.h
View file

@ -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);
}

96
src/util/numerics/mpz.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <memory>
#include "util/sstream.h"
#include "util/numerics/mpz.h"
namespace lean {
@ -81,6 +82,101 @@ mpz const & numeric_traits<mpz>::zero() {
lean_assert(is_zero(g_zero));
return g_zero;
}
DECL_UDATA(mpz)
template<int idx>
static mpz const & to_mpz(lua_State * L) {
static thread_local mpz arg;
switch (lua_type(L, idx)) {
case LUA_TNUMBER: arg = static_cast<long>(lua_tointeger(L, idx)); return arg;
case LUA_TSTRING: arg = mpz(lua_tostring(L, idx)); return arg;
case LUA_TUSERDATA: return *static_cast<mpz*>(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<long>(lua_tointeger(L, idx)));
case LUA_TSTRING: return mpz(lua_tostring(L, idx));
case LUA_TUSERDATA: return *static_cast<mpz*>(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<mpz*>(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<mpz_tostring>},
{"__eq", safe_function<mpz_eq>},
{"__lt", safe_function<mpz_lt>},
{"__add", safe_function<mpz_add>},
{"__sub", safe_function<mpz_sub>},
{"__mul", safe_function<mpz_mul>},
{"__div", safe_function<mpz_div>},
{"__pow", safe_function<mpz_power>},
{"__unm", safe_function<mpz_umn>},
{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; }

5
src/util/numerics/mpz.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <gmp.h>
#include <iostream>
#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);
}

11
src/bindings/lua/expr.h → src/util/numerics/open_module.h
View file

@ -5,9 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <lua.hpp>
#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);
}
}

10
src/bindings/lua/cex_builder.h → src/util/open_module.h
View file

@ -5,8 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <lua.hpp>
#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);
}
}

2
src/library/script_evaluator.cpp → src/util/script_exception.cpp
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
*/
#include <sstream>
#include <string>
#include "library/script_evaluator.h"
#include "util/script_exception.h"
namespace lean {
char const * script_exception::what() const noexcept {

23
src/util/script_exception.h Normal file
View file

@ -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;
};
}

102
src/util/sexpr/format.cpp
View file

@ -6,8 +6,12 @@
*/
#include <sstream>
#include <string>
#include <cstring>
#include <utility>
#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<int>(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<format_tostring>},
{"__concat", safe_function<format_concat>},
{"nest", safe_function<format_nest>},
{"group", safe_function<format_group>},
{"highlight", safe_function<format_highlight>},
{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");
}
}

4
src/util/sexpr/format.h
View file

@ -13,6 +13,7 @@ Author: Soonho Kong
#include <string>
#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);
}

18
src/util/sexpr/open_module.h Normal file
View file

@ -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);
}
}

215
src/util/sexpr/options.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <memory>
#include <string>
#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<bool>(lua_toboolean(L, i+1))); break;
case IntOption: r = r.update(k, static_cast<int>(lua_tointeger(L, i+1))); break;
case UnsignedOption: r = r.update(k, static_cast<unsigned>(lua_tointeger(L, i+1))); break;
case DoubleOption: r = r.update(k, static_cast<double>(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<bool>(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<int>(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<unsigned>(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<options_tostring>},
{"__len", safe_function<options_size> },
{"contains", safe_function<options_contains>},
{"size", safe_function<options_size>},
{"empty", safe_function<options_empty>},
{"get", safe_function<options_get>},
{"update", safe_function<options_update>},
// low-level API
{"get_bool", safe_function<options_get_bool>},
{"get_int", safe_function<options_get_int>},
{"get_unsigned", safe_function<options_get_unsigned>},
{"get_double", safe_function<options_get_double>},
{"get_string", safe_function<options_get_string>},
{"update_bool", safe_function<options_update_bool>},
{"update_int", safe_function<options_update_int>},
{"update_unsigned", safe_function<options_update_unsigned>},
{"update_double", safe_function<options_update_double>},
{"update_string", safe_function<options_update_string>},
{0, 0}
};
static char g_options_key;
options get_global_options(lua_State * L) {
lua_pushlightuserdata(L, static_cast<void *>(&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<void *>(&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");
}
}

18
src/util/sexpr/options.h
View file

@ -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);
}

218
src/util/sexpr/sexpr.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <sstream>
#include <cstring>
#include <string>
#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<bool>(lua_toboolean(L, idx)));
} else if (lua_isnumber(L, idx)) {
// Remark: we convert to integer by default
return sexpr(static_cast<int>(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<sexpr*>(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<int>(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<sexpr_tostring>},
{"__eq", safe_function<sexpr_eq>},
{"__lt", safe_function<sexpr_lt>},
{"kind", safe_function<sexpr_get_kind>},
{"is_nil", safe_function<sexpr_is_nil>},
{"is_cons", safe_function<sexpr_is_cons>},
{"is_list", safe_function<sexpr_is_list>},
{"is_atom", safe_function<sexpr_is_atom>},
{"is_string", safe_function<sexpr_is_string>},
{"is_bool", safe_function<sexpr_is_bool>},
{"is_int", safe_function<sexpr_is_int>},
{"is_double", safe_function<sexpr_is_double>},
{"is_name", safe_function<sexpr_is_name>},
{"is_mpz", safe_function<sexpr_is_mpz>},
{"is_mpq", safe_function<sexpr_is_mpq>},
{"head", safe_function<sexpr_head>},
{"tail", safe_function<sexpr_tail>},
{"length", safe_function<sexpr_length>},
{"to_bool", safe_function<sexpr_to_bool>},
{"to_string", safe_function<sexpr_to_string>},
{"to_int", safe_function<sexpr_to_int>},
{"to_double", safe_function<sexpr_to_double>},
{"to_name", safe_function<sexpr_to_name>},
{"to_mpz", safe_function<sexpr_to_mpz>},
{"to_mpq", safe_function<sexpr_to_mpq>},
{"fields", safe_function<sexpr_fields>},
{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"; }

3
src/util/sexpr/sexpr.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <iostream>
#include <string>
#include <algorithm>
#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);
}

18
src/bindings/lua/splay_map.cpp → src/util/splay_map.cpp
View file

@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <lua.hpp>
#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<lref, lref, lref_lt_proc> lua_splay_map;
typedef splay_map<luaref, luaref, luaref_lt_proc> 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();

3
src/util/splay_map.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include <utility>
#include "util/lua.h"
#include "util/pair.h"
#include "util/splay_tree.h"
@ -114,4 +115,6 @@ void for_each(splay_map<K, T, CMP> 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);
}