feat(frontends/lean): add "show hole" command line option

src/emacs/lean-mode.el

@@ -154,6 +154,8 @@ will be flushed everytime it's executed."
   (local-set-key "\C-c\C-r"  'lean-server-restart-process)
   (local-set-key "\M-."      'lean-find-tag)
   (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)
+  (lean-define-key-binding "\C-c\C-p"
+                           '(lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole"))
   (lean-define-key-binding "\C-c\C-g"
                            '(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))
   )

src/frontends/lean/elaborator.cpp

@@ -225,6 +225,16 @@ void elaborator::save_placeholder_info(expr const & e, expr const & r) {
         save_type_data(e, r);
         save_synth_data(e, r);
     }
+    unsigned line, col;
+    if (m_ctx.has_show_hole_at(line, col)) {
+        if (auto p = pip()->get_pos_info(e)) {
+            if (p->first == line && p->second == col) {
+                m_to_show_hole = r;
+                m_to_show_hole_ref = e;
+                m_ctx.reset_show_goal_at();
+            }
+        }
+    }
 }
 
 /** \brief Auxiliary function for saving information about which coercion was used by the elaborator.
@@ -247,13 +257,23 @@ void elaborator::erase_coercion_info(expr const & e) {
     }
 }
 
-void elaborator::copy_info_to_manager(substitution s) {
-    if (!infom())
-        return;
+void elaborator::instantiate_info(substitution s) {
+    if (m_to_show_hole) {
+        expr meta      = s.instantiate(*m_to_show_hole);
+        expr meta_type = s.instantiate(type_checker(env()).infer(meta).first);
+        goal g(meta, meta_type);
+        proof_state ps(goals(g), s, m_ngen, constraints());
+        auto out = regular(env(), ios());
+        out << "LEAN_HOLE_INFORMATION\n";
+        out << ps.pp(env(), ios()) << endl;
+        out << "END_LEAN_HOLE_INFORMATION\n";
+    }
+    if (infom()) {
         m_pre_info_data.instantiate(s);
         bool overwrite = true;
         infom()->merge(m_pre_info_data, overwrite);
         m_pre_info_data.clear();
+    }
 }
 
 optional<name> elaborator::mk_mvar_suffix(expr const & b) {
@@ -2129,7 +2149,7 @@ auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure
     substitution s = p->first.first;
     auto result = apply(s, r);
     check_sort_assignments(s);
-    copy_info_to_manager(s);
+    instantiate_info(s);
     check_used_local_tactic_hints();
     return result;
 }
@@ -2156,7 +2176,7 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(expr const & t,
     expr new_r_t = apply(s, r_t, univ_params, new_params);
     expr new_r_v = apply(s, r_v, univ_params, new_params);
     check_sort_assignments(s);
-    copy_info_to_manager(s);
+    instantiate_info(s);
     check_used_local_tactic_hints();
     return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
 }
@@ -2231,7 +2251,7 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
     r = new_subst.instantiate_all(r);
     r = solve_unassigned_mvars(new_subst, r);
     rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, new_subst); });
-    copy_info_to_manager(new_subst);
+    instantiate_info(new_subst);
     if (report_unassigned)
         display_unassigned_mvars(r, new_subst);
     if (expected_type) {

src/frontends/lean/elaborator.h

@@ -69,6 +69,9 @@ class elaborator : public coercion_info_manager {
     // If m_nice_mvar_names is true, we append (when possible) a more informative name for a metavariable.
     // That is, whenever a metavariables comes from a binding, we add the binding name as a suffix
     bool                 m_nice_mvar_names;
+
+    optional<expr>       m_to_show_hole; // type information for "show hole" command line
+    expr                 m_to_show_hole_ref; // provide position information
     struct choice_expr_elaborator;
 
     environment const & env() const { return m_ctx.m_env; }
@@ -102,7 +105,7 @@ class elaborator : public coercion_info_manager {
     void save_placeholder_info(expr const & e, expr const & r);
     virtual void save_coercion_info(expr const & e, expr const & c);
     virtual void erase_coercion_info(expr const & e);
-    void copy_info_to_manager(substitution s);
+    void instantiate_info(substitution s);
     /** \brief If info manager is being used, then create a metavariable suffix based on binding_name(b) */
     optional<name> mk_mvar_suffix(expr const & b);
     expr mk_placeholder_meta(optional<name> const & suffix, optional<expr> const & type,

src/frontends/lean/elaborator_context.cpp

@@ -82,6 +82,11 @@ void elaborator_context::init_options(options const & opts) {
         m_show_goal_at = false;
     }
 
+    if (has_show_hole(opts, m_show_hole_line, m_show_hole_col)) {
+        m_show_hole_at = true;
+    } else {
+        m_show_hole_at = false;
+    }
 }
 
 bool elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) const {
@@ -98,6 +103,20 @@ void elaborator_context::reset_show_goal_at() {
     m_show_goal_at = false;
 }
 
+bool elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) const {
+    if (m_show_hole_at) {
+        line = m_show_hole_line;
+        col  = m_show_hole_col;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+void elaborator_context::reset_show_hole_at() {
+    m_show_hole_at = false;
+}
+
 void initialize_elaborator_context() {
     g_elaborator_local_instances    = new name{"elaborator", "local_instances"};
     g_elaborator_ignore_instances   = new name{"elaborator", "ignore_instances"};

src/frontends/lean/elaborator_context.h

@@ -32,11 +32,17 @@ class elaborator_context {
     unsigned m_show_goal_line;
     unsigned m_show_goal_col;
 
+    bool     m_show_hole_at;
+    unsigned m_show_hole_line;
+    unsigned m_show_hole_col;
+
     /** \brief Support for showing information using hot-keys */
     void init_options(options const & opts);
     bool has_show_goal_at(unsigned & line, unsigned & col) const;
     void reset_show_goal_at();
 
+    bool has_show_hole_at(unsigned & line, unsigned & col) const;
+    void reset_show_hole_at();
 public:
     elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
                        pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true);

src/frontends/lean/opt_cmd.cpp

@@ -7,16 +7,15 @@ Author: Leonardo de Moura
 #include "frontends/lean/opt_cmd.h"
 
 namespace lean {
-options set_show_goal(options const & _opts, unsigned line, unsigned col) {
+static options set_line_col(options const & _opts, unsigned line, unsigned col) {
     options opts = _opts;
-    opts = opts.update(name("show_goal"), true);
     opts = opts.update(name("line"), line);
     opts = opts.update(name("column"), col);
     return opts;
 }
 
-bool has_show_goal(options const & opts, unsigned & line, unsigned & col) {
-    if (opts.get_bool("show_goal")) {
+static bool has_show(options const & opts, name const & kind, unsigned & line, unsigned & col) {
+    if (opts.get_bool(kind)) {
         line = opts.get_unsigned("line", 0);
         col  = opts.get_unsigned("column", 0);
         return true;
@@ -24,4 +23,20 @@ bool has_show_goal(options const & opts, unsigned & line, unsigned & col) {
         return false;
     }
 }
+
+options set_show_goal(options const & opts, unsigned line, unsigned col) {
+    return set_line_col(opts.update(name("show_goal"), true), line, col);
+}
+
+bool has_show_goal(options const & opts, unsigned & line, unsigned & col) {
+    return has_show(opts, "show_goal", line, col);
+}
+
+options set_show_hole(options const & opts, unsigned line, unsigned col) {
+    return set_line_col(opts.update(name("show_hole"), true), line, col);
+}
+
+bool has_show_hole(options const & opts, unsigned & line, unsigned & col) {
+    return has_show(opts, "show_hole", line, col);
+}
 }

src/frontends/lean/opt_cmd.h

@@ -12,4 +12,7 @@ namespace lean {
 
 options set_show_goal(options const & opts, unsigned line, unsigned col);
 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);
 }

src/frontends/lean/parser.cpp

@@ -106,6 +106,8 @@ void parser::init_stop_at(options const & opts) {
     unsigned col;
     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;
     }

src/shell/lean.cpp

@@ -130,6 +130,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --line=value      line number for query\n";
     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 << "  --export=file -E  export final environment as textual low-level file\n";
 }
 
@@ -179,10 +180,11 @@ static struct option g_long_options[] = {
     {"line",         required_argument, 0, 'L'},
     {"col",          required_argument, 0, 'O'},
     {"goal",         no_argument,       0, 'G'},
+    {"hole",         no_argument,       0, 'Z'},
     {0, 0, 0, 0}
 };
 
-#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012G"
+#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZ"
 
 #if defined(LEAN_TRACK_MEMORY)
 #define OPT_STR2 OPT_STR "M:012"
@@ -259,6 +261,7 @@ int main(int argc, char ** argv) {
     optional<unsigned> column;
     optional<std::string> export_txt;
     bool show_goal = false;
+    bool show_hole = false;
     input_kind default_k = input_kind::Unspecified;
     while (true) {
         int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
@@ -357,6 +360,9 @@ int main(int argc, char ** argv) {
         case 'G':
             show_goal = true;
             break;
+        case 'Z':
+            show_hole = true;
+            break;
         case 'E':
             export_txt = std::string(optarg);
             break;
@@ -367,6 +373,12 @@ int main(int argc, char ** argv) {
         }
     }
 
+    if (show_hole && line && column) {
+        opts = set_show_hole(opts, *line, *column);
+    }
+    #if defined(__GNUC__) && !defined(__CLANG__)
+    #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+    #endif
     if (show_goal && line && column) {
         opts = set_show_goal(opts, *line, *column);
     }