feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode

library/tools/tactic.lean

@@ -36,6 +36,7 @@ opaque definition state       : tactic := builtin
 opaque definition fail        : tactic := builtin
 opaque definition id          : tactic := builtin
 opaque definition beta        : tactic := builtin
+opaque definition info        : tactic := builtin
 
 -- This is just a trick to embed expressions into tactics.
 -- The nested expressions are "raw". They tactic should

src/frontends/lean/CMakeLists.txt

@@ -6,7 +6,7 @@ inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
 begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
 theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp
 extra_info.cpp local_context.cpp choice_iterator.cpp
-placeholder_elaborator.cpp coercion_elaborator.cpp
+placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp
 proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp)
 
 

src/frontends/lean/elaborator.cpp

@@ -43,6 +43,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/placeholder_elaborator.h"
 #include "frontends/lean/proof_qed_elaborator.h"
+#include "frontends/lean/info_tactic.h"
 #include "frontends/lean/pp_options.h"
 
 namespace lean {
@@ -151,6 +152,15 @@ void elaborator::save_extra_type_data(expr const & e, expr const & r) {
     }
 }
 
+/** \brief Store proof_state information at pos(e) in the info_manager */
+void elaborator::save_proof_state_info(proof_state const & ps, expr const & e) {
+    if (!m_no_info && infom() && pip()) {
+        if (auto p = pip()->get_pos_info(e)) {
+            m_pre_info_data.add_proof_state_info(p->first, p->second, ps);
+        }
+    }
+}
+
 /** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
 void elaborator::save_identifier_info(expr const & f) {
     if (!m_no_info && infom() && pip() && is_constant(f)) {
@@ -1167,6 +1177,11 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
 /** \brief Elaborate expression \c e in context \c ctx. */
 pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, expr const & n,
                                                      bool relax, bool use_tactic_hints) {
+    if (infom()) {
+        if (auto ps = get_info_tactic_proof_state()) {
+            save_proof_state_info(*ps, n);
+        }
+    }
     expr e = translate(env(), ctx, n);
     m_context.set_ctx(ctx);
     m_full_context.set_ctx(ctx);

src/frontends/lean/elaborator.h

@@ -78,6 +78,7 @@ class elaborator : public coercion_info_manager {
     void save_type_data(expr const & e, expr const & r);
     void save_binder_type(expr const & e, expr const & r);
     void save_extra_type_data(expr const & e, expr const & r);
+    void save_proof_state_info(proof_state const & ps, expr const & e);
     void save_identifier_info(expr const & f);
     void save_synth_data(expr const & e, expr const & r);
     void save_placeholder_info(expr const & e, expr const & r);

src/frontends/lean/info_tactic.cpp

@@ -0,0 +1,52 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/tactic/elaborate.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+LEAN_THREAD_PTR(proof_state const, g_info_proof_state);
+
+optional<proof_state> get_info_tactic_proof_state() {
+    if (g_info_proof_state) {
+        return some_proof_state(*g_info_proof_state);
+    } else {
+        return none_proof_state();
+    }
+}
+
+void set_info_tactic_proof_state(proof_state const * ps) {
+    g_info_proof_state = ps;
+}
+
+struct scoped_info_tactic_proof_state {
+    scoped_info_tactic_proof_state(proof_state const & s) {
+        set_info_tactic_proof_state(&s);
+    }
+    ~scoped_info_tactic_proof_state() {
+        set_info_tactic_proof_state(nullptr);
+    }
+};
+
+tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
+    return tactic1([=](environment const &, io_state const &, proof_state const & ps) -> proof_state {
+            // create dummy variable just to communicate position to the elaborator
+            expr dummy = mk_sort(mk_level_zero(), e.get_tag());
+            scoped_info_tactic_proof_state scope(ps);
+            fn(goal(), name_generator("dummy"), dummy);
+            return ps;
+        });
+}
+
+void initialize_info_tactic() {
+    register_tac(name({"tactic", "info"}),
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     return mk_info_tactic(fn, e);
+                 });
+}
+void finalize_info_tactic() {
+}
+}

src/frontends/lean/info_tactic.h

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/tactic/proof_state.h"
+
+namespace lean {
+/** \brief The tactic framework does not have access to the info manager.
+    Thus, it cannot store the proof_state there. The info tactic accomplishes
+    that by (temporarily) saving the proof state in a thread-local storage
+    that is accessed by the elaborator using this function. */
+optional<proof_state> get_info_tactic_proof_state();
+void initialize_info_tactic();
+void finalize_info_tactic();
+}

src/frontends/lean/init_module.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/token_table.h"
+#include "frontends/lean/info_tactic.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/server.h"
@@ -49,12 +50,14 @@ void initialize_frontend_lean_module() {
     initialize_inductive_cmd();
     initialize_structure_cmd();
     initialize_info_manager();
+    initialize_info_tactic();
     initialize_pp();
     initialize_server();
 }
 void finalize_frontend_lean_module() {
     finalize_server();
     finalize_pp();
+    finalize_info_tactic();
     finalize_info_manager();
     finalize_structure_cmd();
     finalize_inductive_cmd();

src/library/tactic/expr_to_tactic.cpp

@@ -209,7 +209,8 @@ static name_generator next_name_generator() {
 }
 
 tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
-    type_checker tc(env, next_name_generator());
+    bool memoize             = false;
+    type_checker tc(env, next_name_generator(), memoize);
     return expr_to_tactic(tc, fn, e, p);
 }
 

tests/lean/interactive/proof_state_info.input

@@ -0,0 +1,15 @@
+VISIT proof_state_info.lean
+SYNC 11
+import logic
+open tactic
+theorem tst (a b c : Prop) : a → b → a ∧ b :=
+begin
+  info,
+  intros (Ha, Hb),
+  info,
+  apply and.intro,
+  apply Ha,
+  apply Hb,
+end
+WAIT
+INFO 7 2

tests/lean/interactive/proof_state_info.input.expected.out

@@ -0,0 +1,13 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|7|2
+tactic
+-- ACK
+-- IDENTIFIER|7|2
+tactic.info
+-- ACK
+-- PROOF_STATE|7|2
+a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a ∧ b
+-- ACK
+-- ENDINFO