From 40fca8efd4fbec60203f27dca40eb8decf847b1e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Nov 2016 11:51:05 -0800
Subject: [PATCH] feat(frontends/lean): add tactic.save_type_info, preserve pos
 info at translate

---
 library/init/meta/interactive.lean |  7 ++++---
 library/init/meta/tactic.lean      |  2 ++
 src/frontends/lean/elaborator.cpp  | 30 ++++++++++++++++++++++++++----
 3 files changed, 32 insertions(+), 7 deletions(-)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 2f18c79e52..433831b591 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -135,9 +135,10 @@ fail ("failed to resolve name '" ++ to_string n ++ "'")
    Example: the elaborator will force any unassigned ?A that must have be an instance of (has_one ?A) to nat.
    Remark: another benefit is that auxiliary temporary metavariables do not appear in error messages. -/
 private meta def to_expr' (p : pexpr) : tactic expr :=
-match pexpr.to_raw_expr p with
-| (const c [])          := resolve_name c
-| (local_const c _ _ _) := resolve_name c
+let e := pexpr.to_raw_expr p in
+match e with
+| (const c [])          := do new_e ← resolve_name c, save_type_info new_e e, return new_e
+| (local_const c _ _ _) := do new_e ← resolve_name c, save_type_info new_e e, return new_e
 | _                     := to_expr p
 end
 
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index f3aa558ac1..fa1199148d 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -362,6 +362,8 @@ try $ do
   prio ← has_attribute attr_name src,
   set_basic_attribute_core attr_name tgt p (some prio)
 
+/- (save_type_info e ref) save (typeof e) at position associated with ref -/
+meta constant save_type_info : expr → expr → tactic unit
 open list nat
 
 /- Remark: set_goals will erase any solved goal -/
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2316189801..a8c9f25b26 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/module.h"
 #include "library/vm/vm.h"
+#include "library/vm/vm_expr.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/kabstract.h"
@@ -2764,11 +2765,11 @@ elaborate(environment & env, options const & opts,
 static expr translate_local_name(environment const & env, local_context const & lctx, name const & local_name,
                                  expr const & src) {
     if (auto decl = lctx.get_local_decl_from_user_name(local_name)) {
-        return decl->mk_ref();
+        return copy_tag(src, decl->mk_ref());
     }
     if (env.find(local_name)) {
         if (is_local(src))
-            return mk_constant(local_name);
+            return copy_tag(src, mk_constant(local_name));
         else
             return src;
     }
@@ -2779,8 +2780,7 @@ static expr translate_local_name(environment const & env, local_context const &
 
 /** \brief Translated local constants (and undefined constants) occurring in \c e into
     local constants provided by \c ctx.
-    Throw exception is \c ctx does not contain the local constant.
-*/
+    Throw exception is \c ctx does not contain the local constant. */
 static expr translate(environment const & env, local_context const & lctx, expr const & e) {
     auto fn = [&](expr const & e) {
         if (is_placeholder(e) || is_by(e) || is_as_is(e)) {
@@ -2810,6 +2810,26 @@ expr nested_elaborate(environment & env, options const & opts, metavar_context &
     return r;
 }
 
+static vm_obj tactic_save_type_info(vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) {
+    expr const & e = to_expr(_e);
+    tactic_state const & s = to_tactic_state(_s);
+    if (!g_infom || !get_pos_info_provider()) return mk_tactic_success(s);
+    auto pos = get_pos_info_provider()->get_pos_info(to_expr(ref));
+    if (!pos) return mk_tactic_success(s);
+    type_context ctx = mk_type_context_for(s);
+    try {
+        expr type = ctx.infer(e);
+        g_infom->add_type_info(pos->first, pos->second, type);
+        if (is_constant(e))
+            g_infom->add_identifier_info(pos->first, pos->second, const_name(e));
+        else if (is_local(e))
+            g_infom->add_identifier_info(pos->first, pos->second, local_pp_name(e));
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+    return mk_tactic_success(s);
+}
+
 void initialize_elaborator() {
     g_elab_strategy = new name("elab_strategy");
     g_level_prefix = new name("_elab_u");
@@ -2847,6 +2867,8 @@ void initialize_elaborator() {
     register_incompatible("elab_simple", "elab_with_expected_type");
     register_incompatible("elab_simple", "elab_as_eliminator");
     register_incompatible("elab_with_expected_type", "elab_as_eliminator");
+
+    DECLARE_VM_BUILTIN(name({"tactic", "save_type_info"}), tactic_save_type_info);
 }
 
 void finalize_elaborator() {