From 8b804f1d22572913c4315c4bdcc5883f324a5b18 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 16:34:02 -0800 Subject: [PATCH] feat(frontends/lean): add option 'elaborator.flycheck_goals' --- src/frontends/lean/elaborator.cpp | 8 ++++++++ src/frontends/lean/elaborator_context.cpp | 17 ++++++++++++++++- src/frontends/lean/elaborator_context.h | 1 + 3 files changed, 25 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index ffe13fa3d..4a82ba9de 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1049,6 +1049,14 @@ void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr display_unsolved_proof_state(mvar, ps, "tactic failed", ptac); return; } + if (m_ctx.m_flycheck_goals) { + if (auto p = pip()->get_pos_info(ptac)) { + auto out = regular(env(), ios()); + flycheck_information info(out); + display_information_pos(out, pip()->get_file_name(), p->first, p->second); + out << " proof state:\n" << ps.pp(env(), ios()) << "\n"; + } + } ps = r->first; } catch (tactic_exception & ex) { auto out = regular(env(), ios()); diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp index 4cbaedb09..2e9f30d02 100644 --- a/src/frontends/lean/elaborator_context.cpp +++ b/src/frontends/lean/elaborator_context.cpp @@ -15,11 +15,16 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES false #endif +#ifndef LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS +#define LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS false +#endif + namespace lean { // ========================================== // elaborator configuration options static name * g_elaborator_local_instances = nullptr; static name * g_elaborator_ignore_instances = nullptr; +static name * g_elaborator_flycheck_goals = nullptr; name const & get_elaborator_ignore_instances_name() { return *g_elaborator_ignore_instances; @@ -32,6 +37,10 @@ bool get_elaborator_local_instances(options const & opts) { bool get_elaborator_ignore_instances(options const & opts) { return opts.get_bool(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES); } + +bool get_elaborator_flycheck_goals(options const & opts) { + return opts.get_bool(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS); +} // ========================================== elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, @@ -39,18 +48,24 @@ elaborator_context::elaborator_context(environment const & env, io_state const & m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) { m_use_local_instances = get_elaborator_local_instances(ios.get_options()); m_ignore_instances = get_elaborator_ignore_instances(ios.get_options()); + m_flycheck_goals = get_elaborator_flycheck_goals(ios.get_options()); } void initialize_elaborator_context() { - g_elaborator_local_instances = new name{"elaborator", "local_instances"}; + g_elaborator_local_instances = new name{"elaborator", "local_instances"}; g_elaborator_ignore_instances = new name{"elaborator", "ignore_instances"}; + g_elaborator_flycheck_goals = new name{"elaborator", "flycheck_goals"}; register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances"); register_bool_option(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES, "(lean elaborator) if true, then elaborator does not perform class-instance resolution"); + register_bool_option(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS, + "(lean elaborator) if true, then elaborator display current goals for flycheck before each " + "tactic is executed in a `begin ... end` block"); } void finalize_elaborator_context() { delete g_elaborator_local_instances; delete g_elaborator_ignore_instances; + delete g_elaborator_flycheck_goals; } } diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h index 1e892063c..14eb3357c 100644 --- a/src/frontends/lean/elaborator_context.h +++ b/src/frontends/lean/elaborator_context.h @@ -23,6 +23,7 @@ class elaborator_context { bool m_check_unassigned; bool m_use_local_instances; bool m_ignore_instances; + bool m_flycheck_goals; friend class elaborator; public: elaborator_context(environment const & env, io_state const & ios, local_decls const & lls,