From 57b19b787b800d49dfa0ea758ea3065c077a5cbf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 31 Oct 2014 09:39:20 -0700 Subject: [PATCH] feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if `!` was used --- src/frontends/lean/calc_proof_elaborator.cpp | 8 ++++++-- src/frontends/lean/calc_proof_elaborator.h | 6 +++++- src/frontends/lean/elaborator.cpp | 3 ++- src/frontends/lean/elaborator.h | 1 + tests/lean/interactive/calc_assistant.input | 17 +++++++++++++++++ .../calc_assistant.input.expected.out | 10 ++++++++++ 6 files changed, 41 insertions(+), 4 deletions(-) create mode 100644 tests/lean/interactive/calc_assistant.input create mode 100644 tests/lean/interactive/calc_assistant.input.expected.out diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index 91d9918d9..2a8fcdecd 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "frontends/lean/local_context.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/calc.h" +#include "frontends/lean/calc_proof_elaborator.h" #ifndef LEAN_DEFAULT_CALC_ASSISTANT #define LEAN_DEFAULT_CALC_ASSISTANT true @@ -101,7 +102,8 @@ static optional> apply_subst(environment const & env, local_con if (auto refl_it = get_calc_refl_info(env, const_name(op))) { name refl; unsigned refl_nargs; unsigned refl_univs; std::tie(refl, refl_nargs, refl_univs) = *refl_it; - if (auto refl_pair = mk_op(env, ctx, ngen, tc, refl, refl_univs, refl_nargs-1, { pred_args[npargs-2] }, cs, g)) { + if (auto refl_pair = mk_op(env, ctx, ngen, tc, refl, refl_univs, refl_nargs-1, + { pred_args[npargs-2] }, cs, g)) { return mk_op(env, ctx, ngen, tc, subst, subst_univs, subst_nargs-2, {e, refl_pair->first}, cs, g); } } @@ -120,7 +122,7 @@ static optional> apply_subst(environment const & env, local_con constraint mk_calc_proof_cnstr(environment const & env, options const & opts, local_context const & _ctx, expr const & m, expr const & _e, constraint_seq const & cs, unifier_config const & cfg, - info_manager * im, bool relax) { + info_manager * im, bool relax, update_type_info_fn const & fn) { justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & _s, name_generator const & _ngen) { @@ -151,6 +153,8 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts, e = mk_app(e, imp_arg, g); e_type = tc->whnf(instantiate(binding_body(e_type), imp_arg), new_cs); } + if (im) + fn(e); } auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs) { diff --git a/src/frontends/lean/calc_proof_elaborator.h b/src/frontends/lean/calc_proof_elaborator.h index 19c8d3b3f..0e5d35570 100644 --- a/src/frontends/lean/calc_proof_elaborator.h +++ b/src/frontends/lean/calc_proof_elaborator.h @@ -5,10 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "library/unifier.h" #include "frontends/lean/info_manager.h" +#include "frontends/lean/local_context.h" namespace lean { +typedef std::function update_type_info_fn; + /** \brief Create a "choice" constraint that postpones the resolution of a calc proof step. By delaying it, we can perform quick fixes such as: @@ -19,7 +23,7 @@ namespace lean { constraint mk_calc_proof_cnstr(environment const & env, options const & opts, local_context const & ctx, expr const & m, expr const & e, constraint_seq const & cs, unifier_config const & cfg, - info_manager * im, bool relax); + info_manager * im, bool relax, update_type_info_fn const & fn); void initialize_calc_proof_elaborator(); void finalize_calc_proof_elaborator(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4c480b156..4fe5062bc 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -310,9 +310,10 @@ expr elaborator::visit_calc_proof(expr const & e, optional const & t, cons pair ecs = visit(get_annotation_arg(e)); expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); register_meta(m); + auto fn = [=](expr const & t) { save_type_data(get_annotation_arg(e), t); }; constraint c = mk_calc_proof_cnstr(env(), ios().get_options(), m_context, m, ecs.first, ecs.second, m_unifier_config, - im, m_relax_main_opaque); + im, m_relax_main_opaque, fn); cs += c; return m; } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 57cd18da4..f797a61a9 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/util.h" #include "frontends/lean/local_context.h" +#include "frontends/lean/calc_proof_elaborator.h" namespace lean { /** \brief Mapping from metavariable names to metavariable applications (?M ...) */ diff --git a/tests/lean/interactive/calc_assistant.input b/tests/lean/interactive/calc_assistant.input new file mode 100644 index 000000000..b7802b86f --- /dev/null +++ b/tests/lean/interactive/calc_assistant.input @@ -0,0 +1,17 @@ +VISIT calc_assistant.lean +SYNC 13 +import logic algebra.category.basic +open eq eq.ops category functor natural_transformation +variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D} +protected definition compose2 (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := +natural_transformation.mk + (λ a, η a ∘ θ a) + (λ a b f, calc + H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc + ... = (η b ∘ G f) ∘ θ a : naturality η f + ... = η b ∘ (G f ∘ θ a) : + assoc + ... = η b ∘ (θ b ∘ F f) : naturality θ f + ... = (η b ∘ θ b) ∘ F f : assoc) +WAIT +INFO 11 diff --git a/tests/lean/interactive/calc_assistant.input.expected.out b/tests/lean/interactive/calc_assistant.input.expected.out new file mode 100644 index 000000000..42da28ead --- /dev/null +++ b/tests/lean/interactive/calc_assistant.input.expected.out @@ -0,0 +1,10 @@ +-- BEGINWAIT +-- ENDWAIT +-- BEGININFO +-- TYPE|11|28 +η b ∘ G f ∘ θ a = (η b ∘ G f) ∘ θ a +-- ACK +-- IDENTIFIER|11|28 +category.assoc +-- ACK +-- ENDINFO