From 282a35bd1b778b1bbf9759335401c70f3104d217 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Jun 2014 07:28:56 -0700 Subject: [PATCH] feat(frontends/lean): add '#setline' directive Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 10 ++++++++++ src/frontends/lean/parser.cpp | 12 ++++++++---- src/frontends/lean/parser.h | 2 ++ src/frontends/lean/scanner.cpp | 5 +++++ src/frontends/lean/scanner.h | 1 + src/frontends/lean/token_table.cpp | 2 +- tests/lean/t8.lean | 9 +++++++++ tests/lean/t8.lean.expected.out | 5 +++++ 8 files changed, 41 insertions(+), 5 deletions(-) create mode 100644 tests/lean/t8.lean create mode 100644 tests/lean/t8.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2be5db557..81c2b9870 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -297,6 +297,15 @@ environment check_cmd(parser & p) { return p.env(); } +environment set_line_cmd(parser & p) { + if (!p.curr_is_numeral()) + throw parser_error("invalid #setline command, numeral expected", p.pos()); + unsigned r = p.get_small_nat(); + p.set_line(r); + p.next(); + return p.env(); +} + cmd_table init_cmd_table() { cmd_table r; add_cmd(r, cmd_info("print", "print a string", print_cmd)); @@ -313,6 +322,7 @@ cmd_table init_cmd_table() { add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd)); add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); + add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd)); return r; } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f6373a736..80acab732 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -299,16 +299,20 @@ static name g_cup("\u2294"); static unsigned g_level_add_prec = 10; static unsigned g_level_cup_prec = 5; -unsigned parser::parse_small_nat() { - auto p = pos(); +unsigned parser::get_small_nat() { mpz val = get_num_val().get_numerator(); - next(); lean_assert(val >= 0); if (!val.is_unsigned_int()) - throw parser_error("invalid level expression, value does not fit in a machine integer", p); + throw parser_error("invalid level expression, value does not fit in a machine integer", pos()); return val.get_unsigned_int(); } +unsigned parser::parse_small_nat() { + unsigned r = get_small_nat(); + next(); + return r; +} + static level lift(level l, unsigned k) { while (k > 0) { k--; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index c44ac9e60..eaf3f9c9e 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -141,6 +141,7 @@ public: pos_info pos_of(expr const & e, pos_info default_pos); pos_info pos_of(expr const & e) { return pos_of(e, pos()); } pos_info cmd_pos() const { return m_last_cmd_pos; } + void set_line(unsigned p) { return m_scanner.set_line(p); } /** \brief Read the next token. */ void scan() { m_curr = m_scanner.scan(m_env); } @@ -169,6 +170,7 @@ public: diagnostic diagnostic_stream() const { return diagnostic(env(), ios()); } void parse_names(buffer> & result); + unsigned get_small_nat(); unsigned parse_small_nat(); level parse_level(unsigned rbp = 0); diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 5be8bb47f..9f9d536e7 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -11,6 +11,11 @@ Author: Leonardo de Moura #include "frontends/lean/parser_config.h" namespace lean { +void scanner::set_line(unsigned p) { + m_line = p; + m_sline = p; +} + void scanner::next() { lean_assert(m_curr != EOF); m_curr = m_stream.get(); diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index aaf8d2608..b7cf1d4bf 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -67,6 +67,7 @@ public: int get_line() const { return m_line; } int get_pos() const { return m_pos; } token_kind scan(environment const & env); + void set_line(unsigned p); mpq const & get_num_val() const { return m_num_val; } name const & get_name_val() const { return m_name_val; } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 98cd8c933..f9b6c5fa0 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -61,7 +61,7 @@ token_table init_token_table() { "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", - nullptr}; + "#setline", nullptr}; std::pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/tests/lean/t8.lean b/tests/lean/t8.lean new file mode 100644 index 000000000..5b962db50 --- /dev/null +++ b/tests/lean/t8.lean @@ -0,0 +1,9 @@ +#setline 1000 + +prit "ok" + +#setline 33 +fo +print "ok" +check +print "done" \ No newline at end of file diff --git a/tests/lean/t8.lean.expected.out b/tests/lean/t8.lean.expected.out new file mode 100644 index 000000000..67367b3b1 --- /dev/null +++ b/tests/lean/t8.lean.expected.out @@ -0,0 +1,5 @@ +t8.lean:1002:0: error: command expected +t8.lean:34:0: error: command expected +ok +t8.lean:37:0: error: invalid expression, unexpected token +done