feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information

see issue #756

src/frontends/lean/builtin_cmds.cpp

@@ -143,7 +143,7 @@ static void print_prefix(parser & p) {
         p.regular_stream() << "no declaration starting with prefix '" << prefix << "'" << endl;
 }
 
-static void print_fields(parser & p, name const & S, pos_info const & pos) {
+static void print_fields(parser const & p, name const & S, pos_info const & pos) {
     environment const & env = p.env();
     if (!is_structure(env, S))
         throw parser_error(sstream() << "invalid 'print fields' command, '" << S << "' is not a structure", pos);
@@ -169,7 +169,7 @@ static bool uses_some_token(unsigned num, notation::transition const * ts, buffe
         std::any_of(tokens.begin(), tokens.end(), [&](name const & token) { return uses_token(num, ts, token); });
 }
 
-static bool print_parse_table(parser & p, parse_table const & t, bool nud, buffer<name> const & tokens) {
+static bool print_parse_table(parser const & p, parse_table const & t, bool nud, buffer<name> const & tokens) {
     bool found = false;
     io_state ios = p.ios();
     options os   = ios.get_options();
@@ -203,7 +203,7 @@ static void print_notation(parser & p) {
         p.regular_stream() << "no notation" << endl;
 }
 
-static void print_metaclasses(parser & p) {
+static void print_metaclasses(parser const & p) {
     buffer<name> c;
     get_metaclasses(c);
     for (name const & n : c)
@@ -225,7 +225,7 @@ static void print_definition(parser const & p, name const & n, pos_info const &
     new_out << d.get_value() << endl;
 }
 
-void print_attributes(parser & p, name const & n) {
+static void print_attributes(parser const & p, name const & n) {
     environment const & env = p.env();
     io_state_stream out = p.regular_stream();
     if (is_coercion(env, n))
@@ -246,7 +246,7 @@ void print_attributes(parser & p, name const & n) {
     }
 }
 
-static void print_inductive(parser & p, name const & n, pos_info const & pos) {
+static void print_inductive(parser const & p, name const & n, pos_info const & pos) {
     environment const & env = p.env();
     io_state_stream out = p.regular_stream();
     if (auto idecls = inductive::is_inductive_decl(env, n)) {
@@ -312,7 +312,7 @@ static void print_recursor_info(parser & p) {
     }
 }
 
-bool print_constant(parser & p, char const * kind, declaration const & d, bool is_def = false) {
+static bool print_constant(parser const & p, char const * kind, declaration const & d, bool is_def = false) {
     io_state_stream out = p.regular_stream();
     if (d.is_definition() && is_marked_noncomputable(p.env(), d.get_name()))
         out << "noncomputable ";
@@ -327,20 +327,21 @@ bool print_constant(parser & p, char const * kind, declaration const & d, bool i
     return true;
 }
 
-bool print_polymorphic(parser & p) {
-    environment const & env = p.env();
-    io_state_stream out = p.regular_stream();
-    auto pos = p.pos();
+bool print_id_info(parser const & p, name const & id, bool show_value, pos_info const & pos) {
+    // declarations
     try {
-        name id = p.check_id_next("");
-        // declarations
+        environment const & env = p.env();
+        io_state_stream out = p.regular_stream();
         try {
             list<name> cs = p.to_constants(id, "", pos);
+            bool first = true;
             for (name const & c : cs) {
+                if (first) first = false; else out << "\n";
                 declaration const & d = env.get(c);
                 if (d.is_theorem()) {
-                    print_constant(p, "theorem", d, true);
-                    print_definition(p, c, pos);
+                    print_constant(p, "theorem", d, show_value);
+                    if (show_value)
+                        print_definition(p, c, pos);
                 } else if (d.is_axiom() || d.is_constant_assumption()) {
                     if (inductive::is_inductive_decl(env, c)) {
                         print_inductive(p, c, pos);
@@ -355,8 +356,10 @@ bool print_polymorphic(parser & p) {
                     } else if (d.is_axiom()) {
                         if (p.in_theorem_queue(d.get_name())) {
                             print_constant(p, "theorem", d);
-                            out << "'" << d.get_name() << "' is still in the theorem queue, use command 'reveal "
-                                << d.get_name() << "' to access its definition.\n";
+                            if (show_value) {
+                                out << "'" << d.get_name() << "' is still in the theorem queue, use command 'reveal "
+                                    << d.get_name() << "' to access its definition.\n";
+                            }
                         } else {
                             print_constant(p, "axiom", d);
                         }
@@ -364,8 +367,9 @@ bool print_polymorphic(parser & p) {
                         print_constant(p, "constant", d);
                     }
                 } else if (d.is_definition()) {
-                    print_constant(p, "definition", d, true);
-                    print_definition(p, c, pos);
+                    print_constant(p, "definition", d, show_value);
+                    if (show_value)
+                        print_definition(p, c, pos);
                 }
             }
             return true;
@@ -393,25 +397,39 @@ bool print_polymorphic(parser & p) {
             }
         }
     } catch (exception &) {}
+    return false;
+}
+
+bool print_token_info(parser const & p, name const & tk) {
+    buffer<name> tokens;
+    tokens.push_back(tk);
+    bool found = false;
+    if (print_parse_table(p, get_nud_table(p.env()), true, tokens)) {
+        found = true;
+    }
+    if (print_parse_table(p, get_led_table(p.env()), false, tokens)) {
+        found = true;
+    }
+    return found;
+}
+
+bool print_polymorphic(parser & p) {
+    auto pos = p.pos();
+    try {
+        name id = p.check_id_next("");
+        bool show_value = true;
+        if (print_id_info(p, id, show_value, pos))
+            return true;
+    } catch (exception &) {}
 
     // notation
     if (p.curr_is_keyword()) {
-        buffer<name> tokens;
         name tk = p.get_token_info().token();
-        tokens.push_back(tk);
-        bool found = false;
-        if (print_parse_table(p, get_nud_table(p.env()), true, tokens)) {
+        if (print_token_info(p, tk)) {
             p.next();
-            found = true;
-        }
-        if (print_parse_table(p, get_led_table(p.env()), false, tokens)) {
-            p.next();
-            found = true;
-        }
-        if (found)
             return true;
+        }
     }
-
     return false;
 }
 
@@ -486,7 +504,12 @@ environment print_cmd(parser & p) {
         auto pos = p.pos();
         name id  = p.check_id_next("invalid 'print definition', constant expected");
         list<name> cs = p.to_constants(id, "invalid 'print definition', constant expected", pos);
+        bool first = true;
         for (name const & c : cs) {
+            if (first)
+                first = false;
+            else
+                p.regular_stream() << "\n";
             declaration const & d = p.env().get(c);
             if (d.is_theorem()) {
                 print_constant(p, "theorem", d);

src/frontends/lean/builtin_cmds.h

@@ -7,6 +7,9 @@ Author: Leonardo de Moura
 #pragma once
 #include "frontends/lean/cmd_table.h"
 namespace lean {
+bool print_id_info(parser const & p, name const & id, bool show_value, pos_info const & pos);
+bool print_token_info(parser const & p, name const & tk);
+
 cmd_table get_builtin_cmds();
 void initialize_builtin_cmds();
 void finalize_builtin_cmds();

src/frontends/lean/elaborator.cpp

@@ -56,6 +56,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/calc.h"
 #include "frontends/lean/decl_cmds.h"
+#include "frontends/lean/opt_cmd.h"
 
 namespace lean {
 type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator && ngen) {
@@ -264,9 +265,9 @@ void elaborator::instantiate_info(substitution s) {
         goal g(meta, meta_type);
         proof_state ps(goals(g), s, m_ngen, constraints());
         auto out = regular(env(), ios());
-        out << "LEAN_INFORMATION\n";
+        print_lean_info_header(out.get_stream());
         out << ps.pp(env(), ios()) << endl;
-        out << "END_LEAN_INFORMATION\n";
+        print_lean_info_footer(out.get_stream());
     }
     if (infom()) {
         m_pre_info_data.instantiate(s);
@@ -1850,7 +1851,7 @@ void elaborator::show_goal(proof_state const & ps, expr const & start, expr cons
     m_ctx.reset_show_goal_at();
     goals const & gs = ps.get_goals();
     auto out = regular(env(), ios());
-    out << "LEAN_INFORMATION\n";
+    print_lean_info_header(out.get_stream());
     out << "position " << curr_pos->first << ":" << curr_pos->second << "\n";
     if (empty(gs)) {
         out << "no goals\n";
@@ -1859,7 +1860,7 @@ void elaborator::show_goal(proof_state const & ps, expr const & start, expr cons
         g      = g.instantiate(ps.get_subst());
         out << g << "\n";
     }
-    out << "END_LEAN_INFORMATION\n";
+    print_lean_info_footer(out.get_stream());
 }
 
 bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {

src/frontends/lean/opt_cmd.cpp

@@ -39,4 +39,19 @@ options set_show_hole(options const & opts, unsigned line, unsigned col) {
 bool has_show_hole(options const & opts, unsigned & line, unsigned & col) {
     return has_show(opts, "show_hole", line, col);
 }
+
+options set_show_info(options const & opts, unsigned line, unsigned col) {
+    return set_line_col(opts.update(name("show_info"), true), line, col);
+}
+
+bool has_show_info(options const & opts, unsigned & line, unsigned & col) {
+    return has_show(opts, "show_info", line, col);
+}
+
+void print_lean_info_header(std::ostream & out) {
+    out << "LEAN_INFORMATION\n";
+}
+void print_lean_info_footer(std::ostream & out) {
+    out << "END_LEAN_INFORMATION\n";
+}
 }

src/frontends/lean/opt_cmd.h

@@ -15,4 +15,10 @@ bool has_show_goal(options const & opts, unsigned & line, unsigned & col);
 
 options set_show_hole(options const & _opts, unsigned line, unsigned col);
 bool has_show_hole(options const & opts, unsigned & line, unsigned & col);
+
+options set_show_info(options const & opts, unsigned line, unsigned col);
+bool has_show_info(options const & opts, unsigned & line, unsigned & col);
+
+void print_lean_info_header(std::ostream & out);
+void print_lean_info_footer(std::ostream & out);
 }

src/frontends/lean/parser.cpp

@@ -52,6 +52,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/update_environment_exception.h"
 #include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/opt_cmd.h"
+#include "frontends/lean/builtin_cmds.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -105,12 +106,16 @@ static name * g_tmp_prefix = nullptr;
 
 void parser::init_stop_at(options const & opts) {
     unsigned col;
+    m_info_at = false;
+    m_stop_at = false;
     if (has_show_goal(opts, m_stop_at_line, col)) {
         m_stop_at      = true;
     } else if (has_show_hole(opts, m_stop_at_line, col)) {
         m_stop_at      = true;
-    } else {
-        m_stop_at      = false;
+    } else if (has_show_info(opts, m_info_at_line, m_info_at_col)) {
+        m_info_at      = true;
+        m_stop_at      = true;
+        m_stop_at_line = m_info_at_line;
     }
 }
 
@@ -162,6 +167,39 @@ parser::~parser() {
     } catch (...) {}
 }
 
+void parser::scan() {
+    if (m_info_at) {
+        m_curr = m_scanner.scan(m_env);
+        pos_info p = pos();
+        if (p.first == m_info_at_line) {
+            if (curr_is_identifier()) {
+                name const & id = get_name_val();
+                if (p.second <= m_info_at_col && m_info_at_col < p.second + id.size()) {
+                    print_lean_info_header(regular_stream().get_stream());
+                    try {
+                        bool show_value = false;
+                        print_id_info(*this, id, show_value, p);
+                    } catch (exception &) {}
+                    print_lean_info_footer(regular_stream().get_stream());
+                    m_info_at = false;
+                }
+            } else if (curr_is_keyword()) {
+                name const & tk = get_token_info().token();
+                if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.size()) {
+                    print_lean_info_header(regular_stream().get_stream());
+                    try {
+                        print_token_info(*this, tk);
+                    } catch (exception &) {}
+                    print_lean_info_footer(regular_stream().get_stream());
+                    m_info_at = false;
+                }
+            }
+        }
+    } else {
+        m_curr = m_scanner.scan(m_env);
+    }
+}
+
 void parser::cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
                               level_param_names const & ls, expr const & type, expr const & value) {
     if (m_cache)
@@ -1278,25 +1316,59 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
     return *r;
 }
 
-list<name> parser::to_constants(name const & id, char const * msg, pos_info const & p) {
-    expr e  = id_to_expr(id, p);
-
+list<name> parser::to_constants(name const & id, char const * msg, pos_info const & p) const {
     buffer<name> rs;
-    std::function<void(expr const & e)> visit = [&](expr const & e) {
+
+    std::function<void(expr const & e)> extract_names = [&](expr const & e) {
         if (in_section(m_env) && is_as_atomic(e)) {
-            visit(get_app_fn(get_as_atomic_arg(e)));
+            extract_names(get_app_fn(get_as_atomic_arg(e)));
         } else if (is_explicit(e)) {
-            visit(get_explicit_arg(e));
+            extract_names(get_explicit_arg(e));
         } else if (is_choice(e)) {
             for (unsigned i = 0; i < get_num_choices(e); i++)
-                visit(get_choice(e, i));
+                extract_names(get_choice(e, i));
         } else if (is_constant(e)) {
             rs.push_back(const_name(e));
         } else {
             throw parser_error(msg, p);
         }
     };
-    visit(e);
+
+    // locals
+    if (auto it1 = m_local_decls.find(id)) {
+        extract_names(*it1);
+        return to_list(rs);
+    }
+
+    for (name const & ns : get_namespaces(m_env)) {
+        auto new_id = ns + id;
+        if (!ns.is_anonymous() && m_env.find(new_id) &&
+            (!id.is_atomic() || !is_protected(m_env, new_id))) {
+            return to_list(new_id);
+        }
+    }
+
+    if (!id.is_atomic()) {
+        name new_id = id;
+        new_id = remove_root_prefix(new_id);
+        if (m_env.find(new_id))
+            return to_list(new_id);
+    }
+
+    buffer<expr> alts;
+    // globals
+    if (m_env.find(id))
+        rs.push_back(id);
+    // aliases
+    auto as = get_expr_aliases(m_env, id);
+    for (name const & n : as) {
+        rs.push_back(n);
+    }
+
+    if (rs.empty()) {
+        throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
+    }
+
     return to_list(rs);
 }
 

src/frontends/lean/parser.h

@@ -147,9 +147,12 @@ class parser {
     // auxiliary field used to record the size of m_local_decls before a command is executed.
     unsigned               m_local_decls_size_at_beg_cmd;
 
-    // stop at line/col
+    // stop/info at line/col
     bool                   m_stop_at; // if true, then parser stops execution after the given line and column is reached
     unsigned               m_stop_at_line;
+    bool                   m_info_at;
+    unsigned               m_info_at_line;
+    unsigned               m_info_at_col;
 
     // If the following flag is true we do not raise error messages
     // noncomputable definitions not tagged as noncomputable.
@@ -332,7 +335,7 @@ public:
     bool in_theorem_queue(name const & n) const { return m_theorem_queue_set.contains(n); }
 
     /** \brief Read the next token. */
-    void scan() { m_curr = m_scanner.scan(m_env); }
+    void scan();
     /** \brief Return the current token */
     scanner::token_kind curr() const { return m_curr; }
     /** \brief Return true iff the current token is an identifier */
@@ -370,7 +373,7 @@ public:
     /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token,
         otherwise throw an exception. */
     name check_atomic_id_next(char const * msg);
-    list<name> to_constants(name const & id, char const * msg, pos_info const & p);
+    list<name> to_constants(name const & id, char const * msg, pos_info const & p) const;
     name to_constant(name const & id, char const * msg, pos_info const & p);
     /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */
     name check_constant_next(char const * msg);

src/shell/CMakeLists.txt

@@ -61,6 +61,9 @@ add_test(NAME "issue_755"
 add_test(NAME "show_goal_bag"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./show_goal_bag.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "print_info"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
   # The following test cannot be executed on Windows because of the
   # bash script timeout.sh

src/shell/lean.cpp

@@ -131,6 +131,8 @@ static void display_help(std::ostream & out) {
     std::cout << "  --col=value       column number for query\n";
     std::cout << "  --goal            display goal at close to given position\n";
     std::cout << "  --hole            display type of the \"hole\" in the given posivition\n";
+    std::cout << "  --info            display information about identifier or token in the given posivition\n";
+    std::cout << "Exporting data:\n";
     std::cout << "  --export=file -E  export final environment as textual low-level file\n";
     std::cout << "  --export-all=file -A  export final environment (and all dependencies) as textual low-level file\n";
 }
@@ -183,10 +185,11 @@ static struct option g_long_options[] = {
     {"col",          required_argument, 0, 'O'},
     {"goal",         no_argument,       0, 'G'},
     {"hole",         no_argument,       0, 'Z'},
+    {"info",         no_argument,       0, 'I'},
     {0, 0, 0, 0}
 };
 
-#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZA"
+#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZAI"
 
 #if defined(LEAN_TRACK_MEMORY)
 #define OPT_STR2 OPT_STR "M:012"
@@ -266,6 +269,7 @@ int main(int argc, char ** argv) {
     optional<std::string> export_all_txt;
     bool show_goal = false;
     bool show_hole = false;
+    bool show_info = false;
     input_kind default_k = input_kind::Unspecified;
     while (true) {
         int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
@@ -368,6 +372,9 @@ int main(int argc, char ** argv) {
         case 'Z':
             show_hole = true;
             break;
+        case 'I':
+            show_info = true;
+            break;
         case 'E':
             export_txt = std::string(optarg);
             break;
@@ -381,16 +388,18 @@ int main(int argc, char ** argv) {
         }
     }
 
-    if (show_hole && line && column) {
-        opts       = set_show_hole(opts, *line, *column);
-        save_cache = false;
-    }
     #if defined(__GNUC__) && !defined(__CLANG__)
     #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
     #endif
-    if (show_goal && line && column) {
+    if (show_hole && line && column) {
+        opts       = set_show_hole(opts, *line, *column);
+        save_cache = false;
+    } else if (show_goal && line && column) {
         opts       = set_show_goal(opts, *line, *column);
         save_cache = false;
+    } else if (show_info && line && column) {
+        opts       = set_show_info(opts, *line, *column);
+        save_cache = false;
     }
 
     #if !defined(LEAN_MULTI_THREAD)

tests/lean/608.hlean.expected.out

@@ -1,9 +1,11 @@
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a :=
 ID
+
 definition function.id [reducible] : Π {A : Type}, A → A :=
 λ (A : Type) (a : A), a
 -----------
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
 ID
+
 definition function.id [reducible] : Π {A : Type}, A → A
 λ (A : Type) (a : A), a

tests/lean/extra/print_info.12.19.expected.out

@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+definition int.mul : ℤ → ℤ → ℤ
+
+definition nat.mul : ℕ → ℕ → ℕ
+END_LEAN_INFORMATION
+print_info.lean:13:8: warning: using 'sorry'

tests/lean/extra/print_info.12.20.expected.out

@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+definition int.mul : ℤ → ℤ → ℤ
+
+definition nat.mul : ℕ → ℕ → ℕ
+END_LEAN_INFORMATION
+print_info.lean:13:8: warning: using 'sorry'

tests/lean/extra/print_info.12.30.expected.out

@@ -0,0 +1 @@
+print_info.lean:13:8: warning: using 'sorry'

tests/lean/extra/print_info.17.0.expected.out

@@ -0,0 +1,4 @@
+print_info.lean:13:8: warning: using 'sorry'
+LEAN_INFORMATION
+definition rfl : ∀ {A : Type} {a : A}, a = a
+END_LEAN_INFORMATION

tests/lean/extra/print_info.17.2.expected.out

@@ -0,0 +1,4 @@
+print_info.lean:13:8: warning: using 'sorry'
+LEAN_INFORMATION
+definition rfl : ∀ {A : Type} {a : A}, a = a
+END_LEAN_INFORMATION

tests/lean/extra/print_info.4.16.expected.out

@@ -0,0 +1,6 @@
+LEAN_INFORMATION
+inductive nat : Type₁
+constructors:
+nat.zero : ℕ
+nat.succ : ℕ → ℕ
+END_LEAN_INFORMATION

tests/lean/extra/print_info.7.18.expected.out

@@ -0,0 +1,5 @@
+LEAN_INFORMATION
+definition int.add : ℤ → ℤ → ℤ
+
+definition nat.add : ℕ → ℕ → ℕ
+END_LEAN_INFORMATION

tests/lean/extra/print_info.8.19.expected.out

@@ -0,0 +1,5 @@
+LEAN_INFORMATION
+_ `+`:65 _:65 :=
+  | nat.add #1 #0
+  | [priority 999] int.add #1 #0
+END_LEAN_INFORMATION

tests/lean/extra/print_info.lean

@@ -0,0 +1,17 @@
+import data.int
+open nat int
+
+variables a b : nat
+variables i j : int
+
+definition foo := add a i
+definition f₁ := a + i
+
+example (n : nat) : n + n = 2 * n :=
+begin
+  unfold [nat.add,mul],
+  apply sorry
+end
+
+example (n : nat) : n + n = n + n :=
+rfl

tests/lean/extra/print_info.sh

@@ -0,0 +1,34 @@
+#!/bin/bash
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: print_info.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export LEAN_PATH=../../../library:.
+
+lines=('4'  '7'  '8'  '12' '12' '12' '17' '17');
+cols=('16'  '18' '19' '19' '20' '30' '0'  '2');
+size=${#lines[@]}
+
+i=0
+while [ $i -lt $size ]; do
+    line=${lines[$i]}
+    col=${cols[$i]}
+    let i=i+1
+    produced=print_info.$line.$col.produced.out
+    expected=print_info.$line.$col.expected.out
+    $LEAN --line=$line --col=$col --info print_info.lean &> $produced
+    if test -f $expected; then
+        if diff --ignore-all-space -I "executing external script" "$produced" "$expected"; then
+            echo "-- checked"
+        else
+            echo "ERROR: file $produced does not match $expected"
+            exit 1
+        fi
+    else
+        echo "ERROR: file $expected does not exist"
+        exit 1
+    fi
+done
+echo "done"