feat(frontends/lean): add '#setline' directive

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

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

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<std::pair<pos_info, name>> & result);
+    unsigned get_small_nat();
     unsigned parse_small_nat();
 
     level parse_level(unsigned rbp = 0);

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

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

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<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/t8.lean

@@ -0,0 +1,9 @@
+#setline 1000
+
+prit "ok"
+
+#setline 33
+fo
+print "ok"
+check
+print "done"

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