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

@@ -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<pair<expr, expr>> 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<pair<expr, expr>> 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) {

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 <functional>
 #include "library/unifier.h"
 #include "frontends/lean/info_manager.h"
+#include "frontends/lean/local_context.h"
 
 namespace lean {
+typedef std::function<void(expr const &)> 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();

src/frontends/lean/elaborator.cpp

@@ -310,9 +310,10 @@ expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, cons
     pair<expr, constraint_seq> 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;
 }

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 ...) */

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

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