diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 4267da268..0cfcff7f0 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -731,6 +731,7 @@ expr parser::parse_notation(parse_table t, expr * left) { break; } case notation::action_kind::LuaExt: + m_last_script_pos = p; using_script([&](lua_State * L) { scoped_set_parser scope(L, *this); lua_getglobal(L, a.get_lua_fn().c_str()); @@ -745,7 +746,7 @@ expr parser::parse_notation(parse_table t, expr * left) { if (!is_expr(L, -1)) throw parser_error(sstream() << "failed to use notation implemented in Lua, value returned by function '" << a.get_lua_fn() << "' is not an expression", p); - args.push_back(to_expr(L, -1)); + args.push_back(rec_save_pos(to_expr(L, -1), p)); lua_pop(L, 1); }); break; @@ -1043,15 +1044,84 @@ bool parse_commands(environment & env, io_state & ios, char const * fname, bool return parse_commands(env, ios, in, fname, use_exceptions, num_threads); } -static int parse_expr(lua_State * L) { - script_state S = to_script_state(L); +static unsigned to_rbp(lua_State * L, int idx) { int nargs = lua_gettop(L); - expr r; - r = get_global_parser(L).parse_expr(nargs == 0 ? 0 : lua_tointeger(L, 1)); - return push_expr(L, r); + return idx < nargs ? 0 : lua_tointeger(L, idx); } +#define gparser get_global_parser(L) + +static int parse_level(lua_State * L) { return push_level(L, gparser.parse_level(to_rbp(L, 1))); } +static int parse_expr(lua_State * L) { return push_expr(L, gparser.parse_expr(to_rbp(L, 1))); } +static int parse_led(lua_State * L) { return push_expr(L, gparser.parse_led(to_expr(L, 1))); } +static int next(lua_State * L) { gparser.next(); return 0; } +static int curr(lua_State * L) { return push_integer(L, static_cast(gparser.curr())); } +static int curr_is_token(lua_State * L) { return push_boolean(L, gparser.curr_is_token(to_name_ext(L, 1))); } +static int curr_is_token_or_id(lua_State * L) { return push_boolean(L, gparser.curr_is_token_or_id(to_name_ext(L, 1))); } +static int curr_is_identifier(lua_State * L) { return push_boolean(L, gparser.curr_is_identifier()); } +static int curr_is_numeral(lua_State * L) { return push_boolean(L, gparser.curr_is_numeral()); } +static int curr_is_string(lua_State * L) { return push_boolean(L, gparser.curr_is_string()); } +static int curr_is_keyword(lua_State * L) { return push_boolean(L, gparser.curr_is_keyword()); } +static int curr_is_command(lua_State * L) { return push_boolean(L, gparser.curr_is_command()); } +static int curr_is_quoted_symbol(lua_State * L) { return push_boolean(L, gparser.curr_is_quoted_symbol()); } +static int check_token_next(lua_State * L) { gparser.check_token_next(to_name_ext(L, 1), lua_tostring(L, 2)); return 0; } +static int check_id_next(lua_State * L) { return push_name(L, gparser.check_id_next(lua_tostring(L, 1))); } +static int pos(lua_State * L) { + auto pos = gparser.pos(); + push_integer(L, pos.first); + push_integer(L, pos.second); + return 2; +} +static int save_pos(lua_State * L) { + return push_expr(L, gparser.save_pos(to_expr(L, 1), pos_info(lua_tointeger(L, 2), lua_tointeger(L, 3)))); +} +static int pos_of(lua_State * L) { + int nargs = lua_gettop(L); + pos_info pos; + if (nargs == 1) + pos = gparser.pos_of(to_expr(L, 1)); + else + pos = gparser.pos_of(to_expr(L, 1), pos_info(lua_tointeger(L, 2), lua_tointeger(L, 3))); + push_integer(L, pos.first); + push_integer(L, pos.second); + return 2; +} +static int env(lua_State * L) { return push_environment(L, gparser.env()); } +static int ios(lua_State * L) { return push_io_state(L, gparser.ios()); } + void open_parser(lua_State * L) { - SET_GLOBAL_FUN(parse_expr, "parse_expr"); + lua_newtable(L); + SET_FUN(parse_expr, "parse_expr"); + SET_FUN(parse_level, "parse_level"); + SET_FUN(parse_led, "parse_led"); + SET_FUN(next, "next"); + SET_FUN(curr, "curr"); + SET_FUN(curr_is_token, "curr_is_token"); + SET_FUN(curr_is_token_or_id, "curr_is_token_or_id"); + SET_FUN(curr_is_identifier, "curr_is_identifier"); + SET_FUN(curr_is_numeral, "curr_is_numeral"); + SET_FUN(curr_is_string, "curr_is_string"); + SET_FUN(curr_is_keyword, "curr_is_keyword"); + SET_FUN(curr_is_command, "curr_is_command"); + SET_FUN(curr_is_quoted_symbol, "curr_is_quoted_symbol"); + SET_FUN(check_token_next, "check_token_next"); + SET_FUN(check_id_next, "check_id_next"); + SET_FUN(pos, "pos"); + SET_FUN(save_pos, "save_pos"); + SET_FUN(pos_of, "pos_of"); + SET_FUN(env, "env"); + SET_FUN(ios, "ios"); + lua_setglobal(L, "parser"); + + lua_newtable(L); + SET_ENUM("Keyword", scanner::token_kind::Keyword); + SET_ENUM("CommandKeyword", scanner::token_kind::CommandKeyword); + SET_ENUM("ScriptBlock", scanner::token_kind::ScriptBlock); + SET_ENUM("Identifier", scanner::token_kind::Identifier); + SET_ENUM("Numeral", scanner::token_kind::Numeral); + SET_ENUM("Decimal", scanner::token_kind::Decimal); + SET_ENUM("String", scanner::token_kind::String); + SET_ENUM("QuotedSymbol", scanner::token_kind::QuotedSymbol); + lua_setglobal(L, "token_kind"); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 55ba647d6..338f8a4dd 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "util/name_map.h" #include "util/exception.h" #include "util/thread_script_state.h" +#include "util/script_exception.h" #include "kernel/environment.h" #include "kernel/expr_maps.h" #include "library/io_state.h" @@ -86,10 +87,14 @@ class parser { void protected_call(std::function && f, std::function && sync); template typename std::result_of::type using_script(F && f) { - script_state S = get_thread_script_state(); - set_io_state set1(S, m_ios); - set_environment set2(S, m_env); - return f(S.get_state()); + try { + script_state S = get_thread_script_state(); + set_io_state set1(S, m_ios); + set_environment set2(S, m_env); + return f(S.get_state()); + } catch (script_nested_exception & ex) { + ex.get_exception().rethrow(); + } } tag get_tag(expr e); diff --git a/src/util/lua.h b/src/util/lua.h index 3752a072e..ea23beb88 100644 --- a/src/util/lua.h +++ b/src/util/lua.h @@ -45,6 +45,7 @@ template void set_global_function(lua_State * L, char const * n lua_setglobal(L, name); } #define SET_GLOBAL_FUN(F, N) set_global_function(L, N) +#define SET_FUN(F, N) lua_pushstring(L, N); lua_pushcfunction(L, safe_function); lua_settable(L, -3) // Auxiliary macro for creating a Lua table that stores enumeration values #define SET_ENUM(N, V) lua_pushstring(L, N); lua_pushinteger(L, static_cast(V)); lua_settable(L, -3) diff --git a/tests/lean/run/n1.lean b/tests/lean/run/n1.lean index 37bf6a71d..0646d8e91 100644 --- a/tests/lean/run/n1.lean +++ b/tests/lean/run/n1.lean @@ -4,12 +4,30 @@ variable g : A → A variable f : A → A → A (* -function foo() - return Const("g")(parse_expr()) +local f = Const("f") +local g = Const("g") +local comma = name(",") +function parse_pair() + local p1 = parser.parse_expr() + parser.check_token_next(comma, "invalid pair, ',' expected") + print("line: " .. tostring(parser.pos())) + local p2 = parser.parse_expr() + return f(p1, p2) +end + +local lbracket = name("[") +local rbracket = name("]") +function parse_bracket() + local l, c = parser.pos() + parser.check_token_next(lbracket, "'[' expected") + local r = parser.parse_expr() + parser.check_token_next(rbracket, "']' expected") + return parser.save_pos(g(r), l, c) end *) -notation `tst` c1:(call foo) `with` c2:(call foo) := f c1 c2 -notation `simple` c:(call foo) := c + +notation `tst` A:(call parse_pair) := A +notation `simple` A:(call parse_bracket) `,` B:(call parse_bracket) := f A B variable b : A -check tst (simple b) with a +check g (tst (simple [b], [a]), a)