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

refactor(frontends/lua): rename leanlua_state to script_state, and move it to util

Browse source 
This commit also minimizes the dependencies of script_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-27 14:57:33 -08:00
parent 0934d7b2f4
commit f7e8545e97
25 changed files with 252 additions and 261 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp
notation.cpp frontend_elaborator.cpp)
notation.cpp frontend_elaborator.cpp register_module.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

38
src/frontends/lean/parser.cpp
View file

@ -19,8 +19,10 @@ Author: Leonardo de Moura
#include "util/scoped_map.h"
#include "util/exception.h"
#include "util/sstream.h"
#include "util/sexpr/option_declarations.h"
#include "util/script_state.h"
#include "util/script_exception.h"
#include "util/interrupt.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/normalizer.h"
#include "kernel/type_checker.h"
#include "kernel/free_vars.h"
@ -31,7 +33,7 @@ Author: Leonardo de Moura
#include "library/arith/arith.h"
#include "library/io_state.h"
#include "library/placeholder.h"
#include "library/script_evaluator.h"
#include "library/kernel_bindings.h"
#include "library/elaborator/elaborator_exception.h"
#include "frontends/lean/frontend.h"
#include "frontends/lean/frontend_elaborator.h"
@ -131,7 +133,7 @@ class parser::imp {
pos_info m_last_cmd_pos;
pos_info m_last_script_pos;
script_evaluator * m_script_evaluator;
script_state * m_script_state;
bool m_verbose;
bool m_show_errors;
@ -1404,7 +1406,7 @@ class parser::imp {
try {
if (m_verbose)
regular(m_frontend) << "Importing file '" << fname << "'" << endl;
parser import_parser(m_frontend, in, m_script_evaluator, true /* use exceptions */, false /* not interactive */);
parser import_parser(m_frontend, in, m_script_state, true /* use exceptions */, false /* not interactive */);
import_parser();
} catch (interrupted &) {
throw;
@ -1591,21 +1593,25 @@ class parser::imp {
void parse_script() {
m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos());
if (!m_script_evaluator)
if (!m_script_state)
throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
std::string script_code = m_scanner.get_str_val();
next();
m_script_evaluator->dostring(script_code.c_str(), m_frontend.get_environment(), m_frontend.get_state());
m_script_state->apply([&](lua_State * L) {
set_io_state set1(L, m_frontend.get_state());
set_environment set2(L, m_frontend.get_environment());
dostring(L, script_code.c_str());
});
}
public:
imp(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive):
imp(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive):
m_frontend(fe),
m_scanner(in),
m_elaborator(fe),
m_use_exceptions(use_exceptions),
m_interactive(interactive) {
m_script_evaluator = S;
m_script_state = S;
updt_options();
m_found_errors = false;
m_num_local_decls = 0;
@ -1689,7 +1695,7 @@ public:
}
};
parser::parser(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
parser::parser(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
parser::imp::show_prompt(interactive, fe);
m_ptr.reset(new imp(fe, in, S, use_exceptions, interactive));
}
@ -1705,7 +1711,7 @@ expr parser::parse_expr() {
return m_ptr->parse_expr_main();
}
shell::shell(frontend & fe, script_evaluator * S):m_frontend(fe), m_script_evaluator(S) {
shell::shell(frontend & fe, script_state * S):m_frontend(fe), m_script_state(S) {
}
shell::~shell() {
@ -1721,34 +1727,34 @@ bool shell::operator()() {
add_history(input);
std::istringstream strm(input);
{
parser p(m_frontend, strm, m_script_evaluator, false, false);
parser p(m_frontend, strm, m_script_state, false, false);
if (!p())
errors = true;
}
free(input);
}
#else
parser p(m_frontend, std::cin, m_script_evaluator, false, true);
parser p(m_frontend, std::cin, m_script_state, false, true);
return p();
#endif
}
bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
bool parse_commands(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
return parser(fe, in, S, use_exceptions, interactive)();
}
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
frontend f(env, st);
bool r = parse_commands(f, in, S, use_exceptions, interactive);
st = f.get_state();
return r;
}
expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions) {
expr parse_expr(frontend & fe, std::istream & in, script_state * S, bool use_exceptions) {
return parser(fe, in, S, use_exceptions).parse_expr();
}
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_evaluator * S, bool use_exceptions) {
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S, bool use_exceptions) {
frontend f(env, st);
expr r = parse_expr(f, in, S, use_exceptions);
st = f.get_state();

18
src/frontends/lean/parser.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <iostream>
namespace lean {
class script_evaluator;
class script_state;
class frontend;
class io_state;
class environment;
@ -17,7 +17,7 @@ class parser {
class imp;
std::unique_ptr<imp> m_ptr;
public:
parser(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions = true, bool interactive = false);
parser(frontend & fe, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false);
~parser();
/** \brief Parse a sequence of commands */
@ -29,17 +29,17 @@ public:
/** \brief Implements the Read Eval Print loop */
class shell {
frontend & m_frontend;
script_evaluator * m_script_evaluator;
frontend & m_frontend;
script_state * m_script_state;
public:
shell(frontend & fe, script_evaluator * S);
shell(frontend & fe, script_state * S);
~shell();
bool operator()();
};
bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
bool parse_commands(frontend & fe, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false);
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false);
expr parse_expr(frontend & fe, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
}

21
src/frontends/lua/frontend_lean.cpp → src/frontends/lean/register_module.cpp
View file

@ -6,18 +6,19 @@ Author: Leonardo de Moura
*/
#include <sstream>
#include "util/lua.h"
#include "util/script_state.h"
#include "util/sexpr/options.h"
#include "library/io_state.h"
#include "library/kernel_bindings.h"
#include "frontends/lean/parser.h"
#include "frontends/lua/leanlua_state.h"
#include "frontends/lean/frontend.h"
namespace lean {
/** \see parse_lean_expr */
static int parse_lean_expr_core(lua_State * L, ro_environment const & env, io_state & st) {
char const * src = luaL_checkstring(L, 1);
std::istringstream in(src);
leanlua_state S = to_leanlua_state(L);
script_state S = to_script_state(L);
push_expr(L, parse_expr(env, st, in, &S));
return 1;
}
@ -73,7 +74,7 @@ static int parse_lean_expr(lua_State * L) {
static void parse_lean_cmds_core(lua_State * L, rw_environment & env, io_state & st) {
char const * src = luaL_checkstring(L, 1);
std::istringstream in(src);
leanlua_state S = to_leanlua_state(L);
script_state S = to_script_state(L);
parse_commands(env, st, in, &S);
}
@ -117,8 +118,18 @@ static int parse_lean_cmds(lua_State * L) {
}
}
static int mk_environment(lua_State * L) {
frontend f;
return push_environment(L, f.get_environment());
}
void open_frontend_lean(lua_State * L) {
SET_GLOBAL_FUN(parse_lean_expr, "parse_lean");
SET_GLOBAL_FUN(parse_lean_cmds, "parse_lean_cmds");
SET_GLOBAL_FUN(mk_environment, "environment");
SET_GLOBAL_FUN(parse_lean_expr, "parse_lean");
SET_GLOBAL_FUN(parse_lean_cmds, "parse_lean_cmds");
}
void register_frontend_lean_module() {
script_state::register_module(open_frontend_lean);
}
}

1
src/frontends/lua/frontend_lean.h → src/frontends/lean/register_module.h
View file

@ -8,4 +8,5 @@ Author: Leonardo de Moura
#include <lua.hpp>
namespace lean {
void open_frontend_lean(lua_State * L);
void register_frontend_lean_module();
}

2
src/frontends/lua/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(leanlua leanlua_state.cpp frontend_lean.cpp)
add_library(leanlua register_modules.cpp)
target_link_libraries(leanlua ${LEAN_LIBS})

2
src/frontends/lua/lean.lua
View file

@ -1,4 +1,4 @@
static char const * g_leanlua_extra = R"Lua(
static char const * g_extra_code = R"Lua(
function Consts(s)
r = {}
i = 1

26
src/frontends/lua/register_modules.cpp Normal file
View file

@ -0,0 +1,26 @@
/*
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 "util/script_state.h"
#include "util/numerics/register_module.h"
#include "util/sexpr/register_module.h"
#include "library/kernel_bindings.h"
#include "library/arith/register_module.h"
#include "library/tactic/register_module.h"
#include "frontends/lean/register_module.h"
#include "frontends/lua/lean.lua"
namespace lean {
void register_modules() {
register_numerics_module();
register_sexpr_module();
register_kernel_module();
register_arith_module();
register_tactic_module();
register_frontend_lean_module();
script_state::register_code(g_extra_code);
}
}

13
src/util/open_module.h → src/frontends/lua/register_modules.h
View file

@ -5,14 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/exception.h"
#include "util/name.h"
#include "util/splay_map.h"
namespace lean {
inline void open_util_module(lua_State * L) {
open_exception(L);
open_name(L);
open_splay_map(L);
}
/**
\brief Register all modules at \c script_state.
*/
void register_modules();
}

4
src/library/arith/open_module.h → src/library/arith/register_module.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/script_state.h"
#include "library/arith/nat.h"
#include "library/arith/int.h"
#include "library/arith/real.h"
@ -15,4 +16,7 @@ inline void open_arith_module(lua_State * L) {
open_int(L);
open_real(L);
}
inline void register_arith_module() {
script_state::register_module(open_arith_module);
}
}

7
src/library/kernel_bindings.cpp
View file

@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "util/lua.h"
#include "util/sstream.h"
#include "util/script_state.h"
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/formatter.h"
@ -1560,7 +1560,6 @@ static void open_metavar_env(lua_State * L) {
SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars");
}
void open_kernel_module(lua_State * L) {
open_level(L);
open_local_context(L);
@ -1574,4 +1573,8 @@ void open_kernel_module(lua_State * L) {
open_io_state(L);
open_type_inferer(L);
}
void register_kernel_module() {
script_state::register_module(open_kernel_module);
}
}

1
src/library/kernel_bindings.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
namespace lean {
void open_kernel_module(lua_State * L);
void register_kernel_module();
UDATA_DEFS(level)
UDATA_DEFS(local_entry)
UDATA_DEFS_CORE(local_context)

24
src/library/script_evaluator.h
View file

@ -1,24 +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 "util/script_exception.h"
namespace lean {
class environment;
class io_state;
/**
\brief Abstract base class for script code evaluators.
These evaluators are used to execute user-supplied code embedded in frontend files (.e.g., .lean, .smt2, etc).
In the current implementation we only have one implementation of this class based on the Lua programming language. So, the main purpose of this class is to organize the dependencies between modules.
*/
class script_evaluator {
public:
virtual ~script_evaluator() {}
virtual void dostring(char const * str) = 0;
virtual void dostring(char const * str, environment & env, io_state & st) = 0;
};
}

4
src/library/tactic/open_module.h → src/library/tactic/register_module.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/script_state.h"
#include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/cex_builder.h"
@ -17,4 +18,7 @@ inline void open_tactic_module(lua_State * L) {
open_cex_builder(L);
open_proof_state(L);
}
inline void register_tactic_module() {
script_state::register_module(open_tactic_module);
}
}

8
src/shell/lean.cpp
View file

@ -10,16 +10,17 @@ Author: Leonardo de Moura
#include <getopt.h>
#include "util/debug.h"
#include "util/interrupt.h"
#include "util/script_state.h"
#include "kernel/printer.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/frontend.h"
#include "frontends/lua/leanlua_state.h"
#include "frontends/lua/register_modules.h"
#include "version.h"
using lean::shell;
using lean::frontend;
using lean::parser;
using lean::leanlua_state;
using lean::script_state;
using lean::unreachable_reached;
using lean::invoke_debugger;
using lean::notify_assertion_violation;
@ -67,6 +68,7 @@ static struct option g_long_options[] = {
};
int main(int argc, char ** argv) {
lean::register_modules();
input_kind default_k = input_kind::Lean; // default
int optind = 1;
while (true) {
@ -93,7 +95,7 @@ int main(int argc, char ** argv) {
}
}
frontend f;
leanlua_state S;
script_state S;
if (optind >= argc) {
display_header(std::cout);
std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;

4
src/util/CMakeLists.txt
View file

@ -1,7 +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
script_exception.cpp splay_map.cpp lua.cpp luaref.cpp
lua_exception.cpp)
script_state.cpp script_exception.cpp splay_map.cpp lua.cpp
luaref.cpp)
target_link_libraries(util ${LEAN_LIBS})

6
src/util/lua.cpp
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include <vector>
#include <memory>
#include "util/lua.h"
#include "util/lua_exception.h"
#include "util/script_exception.h"
#include "util/debug.h"
namespace lean {
@ -94,7 +94,7 @@ void check_result(lua_State * L, int result) {
if (is_exception(L, -1))
to_exception(L, -1).rethrow();
else
throw lua_exception(lua_tostring(L, -1));
throw script_exception(lua_tostring(L, -1));
}
}
@ -122,7 +122,7 @@ void pcall(lua_State * L, int nargs, int nresults, int errorfun) {
int safe_function_wrapper(lua_State * L, lua_CFunction f) {
try {
return f(L);
} catch (lua_exception & e) {
} catch (script_exception & e) {
lua_pushstring(L, e.what());
} catch (exception & e) {
push_exception(L, e);

71
src/util/lua_exception.cpp
View file

@ -1,71 +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 <string>
#include <cstdlib>
#include "util/debug.h"
#include "util/lua_exception.h"
namespace lean {
lua_exception::lua_exception(char const * lua_error):script_exception() {
lean_assert(lua_error);
std::string fname;
std::string line;
std::string msg;
int state = 0;
char const * it = lua_error;
while (*it) {
if (state == 0) {
if (*it == ':') {
state = 1;
} else {
fname += *it;
}
} else if (state == 1) {
if (*it == ':') {
state = 2;
} else {
line += *it;
}
} else {
msg += *it;
}
it++;
}
if (state != 2) {
// failed to decode Lua error message
m_source = source::Unknown;
m_msg = lua_error;
} else {
if (fname == "[string \"...\"]") {
m_source = source::String;
} else {
m_source = source::File;
m_file = fname;
}
m_line = atoi(line.c_str());
m_msg = msg;
}
}
lua_exception::~lua_exception() {
}
char const * lua_exception::get_filename() const {
lean_assert(get_source() == source::File);
return m_file.c_str();
}
unsigned lua_exception::get_line() const {
lean_assert(get_source() != source::Unknown);
return m_line;
}
char const * lua_exception::get_msg() const noexcept {
return exception::what();
}
}

33
src/util/lua_exception.h
View file

@ -1,33 +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 <string>
#include "util/exception.h"
#include "util/script_exception.h"
namespace lean {
/**
\brief Exception for wrapping errors produced by the Lua engine.
*/
class lua_exception : public script_exception {
private:
source m_source;
std::string m_file; // if source == File, then this field contains the filename that triggered the error.
unsigned m_line; // line number
lua_exception(source s, std::string f, unsigned l):m_source(s), m_file(f), m_line(l) {}
public:
lua_exception(char const * lua_error);
virtual ~lua_exception();
virtual source get_source() const { return m_source; }
virtual char const * get_filename() const;
virtual unsigned get_line() const;
/** \brief Return error message without position information */
virtual char const * get_msg() const noexcept;
virtual exception * clone() const { return new lua_exception(m_source, m_file, m_line); }
virtual void rethrow() const { throw *this; }
};
}

4
src/util/numerics/open_module.h → src/util/numerics/register_module.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/script_state.h"
#include "util/numerics/mpz.h"
#include "util/numerics/mpq.h"
@ -13,4 +14,7 @@ inline void open_numerics_module(lua_State * L) {
open_mpz(L);
open_mpq(L);
}
inline void register_numerics_module() {
script_state::register_module(open_numerics_module);
}
}

59
src/util/script_exception.cpp
View file

@ -6,9 +6,68 @@ Author: Leonardo de Moura
*/
#include <sstream>
#include <string>
#include "util/debug.h"
#include "util/script_exception.h"
namespace lean {
script_exception::script_exception(char const * lua_error) {
lean_assert(lua_error);
std::string fname;
std::string line;
std::string msg;
int state = 0;
char const * it = lua_error;
while (*it) {
if (state == 0) {
if (*it == ':') {
state = 1;
} else {
fname += *it;
}
} else if (state == 1) {
if (*it == ':') {
state = 2;
} else {
line += *it;
}
} else {
msg += *it;
}
it++;
}
if (state != 2) {
// failed to decode Lua error message
m_source = source::Unknown;
m_msg = lua_error;
} else {
if (fname == "[string \"...\"]") {
m_source = source::String;
} else {
m_source = source::File;
m_file = fname;
}
m_line = atoi(line.c_str());
m_msg = msg;
}
}
script_exception::~script_exception() {
}
char const * script_exception::get_filename() const {
lean_assert(get_source() == source::File);
return m_file.c_str();
}
unsigned script_exception::get_line() const {
lean_assert(get_source() != source::Unknown);
return m_line;
}
char const * script_exception::get_msg() const noexcept {
return exception::what();
}
char const * script_exception::what() const noexcept {
static thread_local std::string buffer;
std::ostringstream strm;

22
src/util/script_exception.h
View file

@ -5,19 +5,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "util/exception.h"
namespace lean {
/**
\brief Base class for exceptions producing when evaluating scripts.
\brief Exception for wrapping errors produced by the Lua engine.
*/
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;
private:
source m_source;
std::string m_file; // if source == File, then this field contains the filename that triggered the error.
unsigned m_line; // line number
script_exception(source s, std::string f, unsigned l):m_source(s), m_file(f), m_line(l) {}
public:
script_exception(char const * lua_error);
virtual ~script_exception();
virtual char const * what() const noexcept;
virtual source get_source() const { return m_source; }
virtual char const * get_filename() const;
virtual unsigned get_line() const;
/** \brief Return error message without position information */
virtual char const * get_msg() const noexcept;
virtual exception * clone() const { return new script_exception(m_source, m_file, m_line); }
virtual void rethrow() const { throw *this; }
};
}

109
src/frontends/lua/leanlua_state.cpp → src/util/script_state.cpp
View file

@ -9,31 +9,38 @@ Author: Leonardo de Moura
#include <thread>
#include <chrono>
#include <string>
#include <vector>
#include <condition_variable>
#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 "util/open_module.h"
#include "util/numerics/open_module.h"
#include "util/sexpr/open_module.h"
#include "library/kernel_bindings.h"
#include "library/arith/open_module.h"
#include "library/tactic/open_module.h"
#include "frontends/lean/frontend.h"
#include "frontends/lua/leanlua_state.h"
#include "frontends/lua/frontend_lean.h"
#include "frontends/lua/lean.lua"
#include "util/script_state.h"
#include "util/script_exception.h"
#include "util/name.h"
#include "util/splay_map.h"
extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
namespace lean {
static std::vector<script_state::reg_fn> g_modules;
static std::vector<char const *> g_code;
void script_state::register_module(reg_fn f) {
g_modules.push_back(f);
}
void script_state::register_code(char const * code) {
g_code.push_back(code);
}
void open_extra(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 {
struct script_state::imp {
lua_State * m_state;
std::recursive_mutex m_mutex;
@ -63,16 +70,18 @@ struct leanlua_state::imp {
if (m_state == nullptr)
throw exception("fail to create Lua interpreter");
luaL_openlibs(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_frontend_lean(m_state);
open_exception(m_state);
open_name(m_state);
open_splay_map(m_state);
open_extra(m_state);
dostring(g_leanlua_extra);
for (auto f : g_modules) {
f(m_state);
}
for (auto c : g_code) {
dostring(c);
}
}
~imp() {
@ -91,47 +100,37 @@ struct leanlua_state::imp {
std::lock_guard<std::recursive_mutex> lock(m_mutex);
::lean::dostring(m_state, str);
}
void dostring(char const * str, environment & env, io_state & st) {
set_io_state set1(m_state, st);
set_environment set2(m_state, env);
dostring(str);
}
};
leanlua_state to_leanlua_state(lua_State * L) {
return leanlua_state(*leanlua_state::imp::get_weak_ptr(L));
script_state to_script_state(lua_State * L) {
return script_state(*script_state::imp::get_weak_ptr(L));
}
leanlua_state::leanlua_state():
script_state::script_state():
m_ptr(new imp()) {
m_ptr->save_weak_ptr(m_ptr);
}
leanlua_state::leanlua_state(std::weak_ptr<imp> const & ptr):m_ptr(ptr.lock()) {
script_state::script_state(std::weak_ptr<imp> const & ptr):m_ptr(ptr.lock()) {
lean_assert(m_ptr);
}
leanlua_state::~leanlua_state() {
script_state::~script_state() {
}
void leanlua_state::dofile(char const * fname) {
void script_state::dofile(char const * fname) {
m_ptr->dofile(fname);
}
void leanlua_state::dostring(char const * str) {
void script_state::dostring(char const * str) {
m_ptr->dostring(str);
}
void leanlua_state::dostring(char const * str, environment & env, io_state & st) {
m_ptr->dostring(str, env, st);
}
std::recursive_mutex & leanlua_state::get_mutex() {
std::recursive_mutex & script_state::get_mutex() {
return m_ptr->m_mutex;
}
lua_State * leanlua_state::get_state() {
lua_State * script_state::get_state() {
return m_ptr->m_state;
}
@ -141,25 +140,25 @@ bool is_state(lua_State * L, int idx) {
return testudata(L, idx, state_mt);
}
leanlua_state & to_state(lua_State * L, int idx) {
return *static_cast<leanlua_state*>(luaL_checkudata(L, idx, state_mt));
script_state & to_state(lua_State * L, int idx) {
return *static_cast<script_state*>(luaL_checkudata(L, idx, state_mt));
}
int push_state(lua_State * L, leanlua_state const & s) {
void * mem = lua_newuserdata(L, sizeof(leanlua_state));
new (mem) leanlua_state(s);
int push_state(lua_State * L, script_state const & s) {
void * mem = lua_newuserdata(L, sizeof(script_state));
new (mem) script_state(s);
luaL_getmetatable(L, state_mt);
lua_setmetatable(L, -2);
return 1;
}
static int mk_state(lua_State * L) {
leanlua_state r;
script_state r;
return push_state(L, r);
}
static int state_gc(lua_State * L) {
to_state(L, 1).~leanlua_state();
to_state(L, 1).~script_state();
return 0;
}
@ -237,7 +236,7 @@ int state_dostring(lua_State * L) {
int sz_before = lua_gettop(S);
int status = luaL_loadstring(S, script);
if (status)
throw lua_exception(lua_tostring(S, -1));
throw script_exception(lua_tostring(S, -1));
copy_values(L, first, last, S);
@ -296,7 +295,7 @@ class data_channel {
// We use a lua_State to implement the channel. This is quite hackish,
// but it is a convenient storage for Lua objects sent from one state to
// another.
leanlua_state m_channel;
script_state m_channel;
int m_ini;
std::mutex m_mutex;
std::condition_variable m_cv;
@ -390,14 +389,14 @@ int channel_write(lua_State * L) {
}
class leanlua_thread {
leanlua_state m_state;
script_state m_state;
int m_sz_before;
std::unique_ptr<exception> m_exception;
std::atomic<data_channel_ref *> m_in_channel_addr;
std::atomic<data_channel_ref *> m_out_channel_addr;
interruptible_thread m_thread;
public:
leanlua_thread(leanlua_state const & st, int sz_before, int num_args):
leanlua_thread(script_state const & st, int sz_before, int num_args):
m_state(st),
m_sz_before(sz_before),
m_in_channel_addr(0),
@ -411,7 +410,7 @@ public:
if (is_exception(S, -1))
m_exception.reset(to_exception(S, -1).clone());
else
m_exception.reset(new lua_exception(lua_tostring(S, -1)));
m_exception.reset(new script_exception(lua_tostring(S, -1)));
}
});
}) {
@ -476,7 +475,7 @@ leanlua_thread & to_thread(lua_State * L, int idx) {
int mk_thread(lua_State * L) {
check_threadsafe();
leanlua_state & st = to_state(L, 1);
script_state & st = to_state(L, 1);
char const * script = luaL_checkstring(L, 2);
int first = 3;
int last = lua_gettop(L);
@ -486,7 +485,7 @@ int mk_thread(lua_State * L) {
sz_before = lua_gettop(S);
int result = luaL_loadstring(S, script);
if (result)
throw lua_exception(lua_tostring(S, -1));
throw script_exception(lua_tostring(S, -1));
copy_values(L, first, last, S);
});
void * mem = lua_newuserdata(L, sizeof(leanlua_thread));
@ -560,15 +559,9 @@ static void open_interrupt(lua_State * L) {
SET_GLOBAL_FUN(channel_write, "write");
}
static int mk_environment(lua_State * L) {
frontend f;
return push_environment(L, f.get_environment());
}
void open_extra(lua_State * L) {
open_state(L);
open_thread(L);
open_interrupt(L);
SET_GLOBAL_FUN(mk_environment, "environment");
}
}

30
src/frontends/lua/leanlua_state.h → src/util/script_state.h
View file

@ -8,27 +8,23 @@ Author: Leonardo de Moura
#include <memory>
#include <mutex>
#include <lua.hpp>
#include "util/lua_exception.h"
#include "library/script_evaluator.h"
namespace lean {
class environment;
class io_state;
/**
\brief Wrapper for lua_State objects which contains all Lean bindings.
*/
class leanlua_state : public script_evaluator {
class script_state {
public:
struct imp;
private:
std::shared_ptr<imp> m_ptr;
leanlua_state(std::weak_ptr<imp> const & ptr);
friend leanlua_state to_leanlua_state(lua_State * L);
script_state(std::weak_ptr<imp> const & ptr);
friend script_state to_script_state(lua_State * L);
std::recursive_mutex & get_mutex();
lua_State * get_state();
public:
leanlua_state();
virtual ~leanlua_state();
script_state();
virtual ~script_state();
/**
\brief Execute the file with the given name.
@ -41,13 +37,6 @@ public:
*/
virtual void dostring(char const * str);
/**
\brief Execute the given script, but sets the registry with the given environment object.
The registry can be accessed by \str by invoking the function <tt>env()</tt>.
The script \c str should not store a reference to the environment \c env.
*/
virtual void dostring(char const * str, environment & env, io_state & st);
/**
\brief Execute \c f in the using the internal Lua State.
*/
@ -68,9 +57,14 @@ public:
typename std::result_of<F(lua_State * L)>::type unguarded_apply(F && f) {
return f(get_state());
}
typedef void (*reg_fn)(lua_State *); // NOLINT
static void register_module(reg_fn f);
static void register_code(char const * code);
};
/**
\brief Return a reference to the leanlua_state object that is wrapping \c L.
\brief Return a reference to the script_state object that is wrapping \c L.
*/
leanlua_state to_leanlua_state(lua_State * L);
script_state to_script_state(lua_State * L);
}

4
src/util/sexpr/open_module.h → src/util/sexpr/register_module.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/script_state.h"
#include "util/sexpr/sexpr.h"
#include "util/sexpr/options.h"
#include "util/sexpr/format.h"
@ -15,4 +16,7 @@ inline void open_sexpr_module(lua_State * L) {
open_options(L);
open_format(L);
}
inline void register_sexpr_module() {
script_state::register_module(open_sexpr_module);
}
}