diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 374e1d571..aeb6209a9 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -12,6 +12,9 @@ struct parser_ext : public environment_extension { token_table m_tokens; parse_table m_nud; parse_table m_led; + parser_ext() { + m_tokens = mk_default_token_table(); + } }; struct parser_ext_reg { diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index c23f2486c..7a4a2f904 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/exception.h" #include "frontends/lean/scanner.h" +#include "frontends/lean/parser_config.h" namespace lean { void scanner::next() { @@ -211,7 +212,7 @@ auto scanner::read_key_cmd_id() -> token_kind { static char const * error_msg = "unexpected token"; char c = curr(); unsigned num_cs = 1; // number of characters read - token_table const * it = find(m_tokens, c); + token_table const * it = find(*m_tokens, c); token_info const * info = nullptr; unsigned key_size = 0; if (it) { @@ -278,7 +279,8 @@ static name g_begin_script_tk("(*"); static name g_begin_comment_tk("--"); static name g_begin_comment_block_tk("(--"); -auto scanner::scan() -> token_kind { +auto scanner::scan(environment const & env) -> token_kind { + m_tokens = &get_token_table(env); while (true) { char c = curr(); m_pos = m_spos; @@ -318,8 +320,8 @@ auto scanner::scan() -> token_kind { } } -scanner::scanner(token_table const & tks, std::istream & strm, char const * strm_name): - m_tokens(tks), m_stream(strm), m_spos(0), m_sline(1), m_curr(0), m_pos(0), m_line(1), +scanner::scanner(std::istream & strm, char const * strm_name): + m_tokens(nullptr), m_stream(strm), m_spos(0), m_sline(1), m_curr(0), m_pos(0), m_line(1), m_token_info(nullptr) { m_stream_name = strm_name ? strm_name : "[unknown]"; next(); diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index d4f4612aa..9e17babe1 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -8,8 +8,10 @@ Author: Leonardo de Moura #include #include "util/name.h" #include "util/numerics/mpq.h" +#include "kernel/environment.h" #include "frontends/lean/token_table.h" + namespace lean { /** \brief Scanner. The behavior of the scanner is controlled using a token set. @@ -22,22 +24,22 @@ class scanner { public: enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, Eof}; protected: - token_table m_tokens; - std::istream & m_stream; - std::string m_stream_name; + token_table const * m_tokens; + std::istream & m_stream; + std::string m_stream_name; - int m_spos; // current position - int m_sline; // current line - char m_curr; // current char; + int m_spos; // current position + int m_sline; // current line + char m_curr; // current char; - int m_pos; // start position of the token - int m_line; // line of the token + int m_pos; // start position of the token + int m_line; // line of the token - name m_name_val; - token_info const * m_token_info; - mpq m_num_val; - std::string m_buffer; - std::string m_aux_buffer; + name m_name_val; + token_info const * m_token_info; + mpq m_num_val; + std::string m_buffer; + std::string m_aux_buffer; [[ noreturn ]] void throw_exception(char const * msg) const; void next(); @@ -60,11 +62,11 @@ protected: token_kind read_key_cmd_id(); public: - scanner(token_table const & tks, std::istream & strm, char const * strm_name = nullptr); + scanner(std::istream & strm, char const * strm_name = nullptr); int get_line() const { return m_line; } int get_pos() const { return m_pos; } - token_kind scan(); + token_kind scan(environment const & env); mpq const & get_num_val() const { return m_num_val; } name const & get_name_val() const { return m_name_val; } diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp index 79afb254f..ba305ae50 100644 --- a/src/tests/frontends/lean/scanner.cpp +++ b/src/tests/frontends/lean/scanner.cpp @@ -9,15 +9,16 @@ Author: Leonardo de Moura #include "util/escaped.h" #include "util/exception.h" #include "frontends/lean/scanner.h" +#include "frontends/lean/parser_config.h" using namespace lean; #define tk scanner::token_kind -static void scan(char const * str, token_table set = mk_default_token_table()) { +static void scan(char const * str, environment const & env = environment()) { std::istringstream in(str); - scanner s(set, in, "[string]"); + scanner s(in, "[string]"); while (true) { - tk k = s.scan(); + tk k = s.scan(env); if (k == tk::Eof) break; if (k == tk::Identifier) @@ -35,9 +36,9 @@ static void scan(char const * str, token_table set = mk_default_token_table()) { std::cout << "\n"; } -static void scan_success(char const * str, token_table set = mk_default_token_table()) { +static void scan_success(char const * str, environment const & env = environment()) { try { - scan(str, set); + scan(str, env); } catch (exception & ex) { std::cout << "ERROR: " << ex.what() << "\n"; lean_unreachable(); @@ -54,13 +55,13 @@ static void scan_error(char const * str) { } static void check(char const * str, std::initializer_list const & l, - token_table set = mk_default_token_table()) { + environment const & env = environment()) { try { auto it = l.begin(); std::istringstream in(str); - scanner s(set, in, "[string]"); + scanner s(in, "[string]"); while (true) { - tk k = s.scan(); + tk k = s.scan(env); if (k == tk::Eof) { lean_assert(it == l.end()); return; @@ -75,37 +76,40 @@ static void check(char const * str, std::initializer_list const & l, } } -static void check_name(char const * str, name const & expected, token_table set = mk_default_token_table()) { +static void check_name(char const * str, name const & expected, environment const & env = environment()) { std::istringstream in(str); - scanner s(set, in, "[string]"); - tk k = s.scan(); + scanner s(in, "[string]"); + tk k = s.scan(env); lean_assert(k == tk::Identifier); lean_assert(s.get_name_val() == expected); - lean_assert(s.scan() == tk::Eof); + lean_assert(s.scan(env) == tk::Eof); } -static void check_keyword(char const * str, name const & expected, token_table set = mk_default_token_table()) { +static void check_keyword(char const * str, name const & expected, environment const & env = environment()) { std::istringstream in(str); - scanner s(set, in, "[string]"); - tk k = s.scan(); + scanner s(in, "[string]"); + tk k = s.scan(env); lean_assert(k == tk::Keyword); lean_assert(s.get_token_info().value() == expected); - lean_assert(s.scan() == tk::Eof); + lean_assert(s.scan(env) == tk::Eof); } static void tst1() { - token_table s = mk_default_token_table(); + environment env; + token_table s = get_token_table(env); s = add_token(s, "+", "plus"); s = add_token(s, "=", "eq"); + env = update_token_table(env, s); scan_success("a..a"); check("a..a", {tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier}); check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword}); s = add_token(s, "ab+cde", "weird1"); s = add_token(s, "+cd", "weird2"); - scan_success("ab+cd", s); - check("ab+cd", {tk::Identifier, tk::Keyword}, s); - scan_success("ab+cde", s); - check("ab+cde", {tk::Keyword}, s); + env = update_token_table(env, s); + scan_success("ab+cd", env); + check("ab+cd", {tk::Identifier, tk::Keyword}, env); + scan_success("ab+cde", env); + check("ab+cde", {tk::Keyword}, env); scan_success("Type.{0}"); scan_success("0.a a"); scan_success("0."); @@ -115,11 +119,11 @@ static void tst1() { scan_success(".."); scan_success("...."); scan_success("....\n.."); - scan_success("a", s); + scan_success("a", env); scan_success("a. b.c.."); scan_success(".. .."); scan_success("....\n.."); - scan_success("fun(x: forall A : Type, A -> A), x+1 = 2.0 λvalue.foo. . . a", s); + scan_success("fun(x: forall A : Type, A -> A), x+1 = 2.0 λvalue.foo. . . a", env); } static void tst2() { @@ -133,11 +137,14 @@ static void tst2() { check_name("x.bla", name({"x", "bla"})); scan_error("+++"); + environment env; token_table s = mk_default_token_table(); s = add_token(s, "+++", "tplus"); - check_keyword("+++", "tplus", s); + env = update_token_table(env, s); + check_keyword("+++", "tplus", env); s = add_token(s, "+", "plus"); - check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, s); + env = update_token_table(env, s); + check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env); check("-- testing", {}); check("(-- testing --)", {}); check("(-- (-- testing\n --) --)", {}); @@ -148,7 +155,8 @@ static void tst2() { check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier}); check_keyword("->", "->"); s = add_token(s, "-+->", "arrow"); - check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, s); + env = update_token_table(env, s); + check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env); check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral}); check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword}); check("\u03BB \u2200 \u2192", {tk::Keyword, tk::Keyword, tk::Keyword}); @@ -174,10 +182,28 @@ static void tst3() { scan("{ } . forall exists let in \u2200 := _"); } +static void tst4(unsigned N) { + std::string big; + for (unsigned i = 0; i < N; i++) + big += "aaa "; + std::istringstream in(big); + environment env; + scanner s(in, "[string]"); + unsigned i = 0; + while (true) { + tk k = s.scan(env); + if (k == tk::Eof) + break; + i++; + } + std::cout << i << "\n"; +} + int main() { save_stack_info(); tst1(); tst2(); tst3(); + tst4(100000); return has_violations() ? 1 : 0; }