From e750c9b67a816f95f1f17e350f3b59983e6e7e9a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Oct 2014 13:18:30 -0700 Subject: [PATCH] feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode --- library/tools/tactic.lean | 1 + src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 15 ++++++ src/frontends/lean/elaborator.h | 1 + src/frontends/lean/info_tactic.cpp | 52 +++++++++++++++++++ src/frontends/lean/info_tactic.h | 18 +++++++ src/frontends/lean/init_module.cpp | 3 ++ src/library/tactic/expr_to_tactic.cpp | 3 +- tests/lean/interactive/proof_state_info.input | 15 ++++++ .../proof_state_info.input.expected.out | 13 +++++ 10 files changed, 121 insertions(+), 2 deletions(-) create mode 100644 src/frontends/lean/info_tactic.cpp create mode 100644 src/frontends/lean/info_tactic.h create mode 100644 tests/lean/interactive/proof_state_info.input create mode 100644 tests/lean/interactive/proof_state_info.input.expected.out diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index e85285097..38468d85d 100644 --- a/library/tools/tactic.lean +++ b/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 diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 0783d0da4..8d1509d00 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/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) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 97109b12f..2e5950ba9 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 const & ctx, expr cons /** \brief Elaborate expression \c e in context \c ctx. */ pair elaborator::elaborate_nested(list 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); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 8debf5b71..e00bad826 100644 --- a/src/frontends/lean/elaborator.h +++ b/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); diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp new file mode 100644 index 000000000..fb29d9201 --- /dev/null +++ b/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 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() { +} +} diff --git a/src/frontends/lean/info_tactic.h b/src/frontends/lean/info_tactic.h new file mode 100644 index 000000000..7a69f969d --- /dev/null +++ b/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 get_info_tactic_proof_state(); +void initialize_info_tactic(); +void finalize_info_tactic(); +} diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index cc80e84cf..21ee17f5a 100644 --- a/src/frontends/lean/init_module.cpp +++ b/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(); diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 9976d8d0a..52e82d01c 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/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); } diff --git a/tests/lean/interactive/proof_state_info.input b/tests/lean/interactive/proof_state_info.input new file mode 100644 index 000000000..600bd76f6 --- /dev/null +++ b/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 diff --git a/tests/lean/interactive/proof_state_info.input.expected.out b/tests/lean/interactive/proof_state_info.input.expected.out new file mode 100644 index 000000000..e2e5f2031 --- /dev/null +++ b/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