fix(library/blast/blast): convert uref and mref back into tactic metavariables

src/library/blast/blast.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
+#include "kernel/replace_fn.h"
 #include "kernel/type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/util.h"
@@ -473,6 +474,60 @@ class blastenv {
         m_initial_context = to_list(ctx);
     }
 
+    name_map<level> mk_uref2uvar() {
+        name_map<level> r;
+        m_uvar2uref.for_each([&](name const & uvar_id, level const & uref) {
+                lean_assert(is_uref(uref));
+                r.insert(meta_id(uref), mk_meta_univ(uvar_id));
+            });
+        return r;
+    }
+
+    name_map<expr> mk_mref2meta() {
+        name_map<expr> r;
+        m_mvar2meta_mref.for_each([&](name const &, pair<expr, expr> const & p) {
+                lean_assert(is_mref(p.second));
+                r.insert(mlocal_name(p.second), p.first);
+            });
+        return r;
+    }
+
+    level restore_uvars(level const & l, name_map<level> const & uref2uvar) {
+        return replace(l, [&](level const & l) {
+                if (is_meta(l)) {
+                    if (auto uvar = uref2uvar.find(meta_id(l)))
+                        return some_level(*uvar);
+                }
+                return none_level();
+            });
+    }
+
+    levels restore_uvars(levels const & ls, name_map<level> const & uref2uvar) {
+        return map(ls, [&](level const & l) { return restore_uvars(l, uref2uvar); });
+    }
+
+    /* Convert uref's and mref's back into tactic metavariables */
+    expr restore_uvars_mvars(expr const & e) {
+        if (m_uvar2uref.empty())
+            return e;
+        name_map<level> uref2uvar = mk_uref2uvar();
+        name_map<expr>  mref2meta = mk_mref2meta();
+        return replace(e, [&](expr const & e, unsigned) {
+                if (is_mref(e))  {
+                    if (auto m = mref2meta.find(mlocal_name(e))) {
+                        return some_expr(*m);
+                    } else {
+                        throw blast_exception(sstream() << "blast tactic failed, resultant proof still contains internal meta-variables");
+                    }
+                } else if (is_sort(e)) {
+                    return some_expr(update_sort(e, restore_uvars(sort_level(e), uref2uvar)));
+                } else if (is_constant(e)) {
+                    return some_expr(update_constant(e, restore_uvars(const_levels(e), uref2uvar)));
+                } else {
+                    return none_expr();
+                }
+            });
+    }
 
     expr to_tactic_proof(expr const & pr) {
         // When a proof is found we must
@@ -482,10 +537,11 @@ class blastenv {
         //    and convert unassigned meta-variables back into
         //    tactic meta-variables.
         expr pr2 = m_curr_state.instantiate_urefs_mrefs(pr1);
+        expr pr3 = restore_uvars_mvars(pr2);
         // TODO(Leo):
         // 3- The external tactic meta-variables that have been instantiated
         //    by blast must also be communicated back to the tactic framework.
-        return pr2;
+        return pr3;
     }
 
 public:

tests/lean/run/blast_equiv_tests.lean

@@ -0,0 +1,39 @@
+import data.sum data.nat
+open function
+
+structure equiv [class] (A B : Type) :=
+  (to_fun    : A → B)
+  (inv_fun   : B → A)
+  (left_inv  : left_inverse inv_fun to_fun)
+  (right_inv : right_inverse inv_fun to_fun)
+
+namespace equiv
+infix ` ≃ `:50 := equiv
+
+protected definition refl [refl] (A : Type) : A ≃ A :=
+mk (@id A) (@id A) (λ x, rfl) (λ x, rfl)
+
+protected definition symm [symm] {A B : Type} : A ≃ B → B ≃ A
+| (mk f g h₁ h₂) := mk g f h₂ h₁
+
+protected definition trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C
+| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
+  mk (f₂ ∘ f₁) (g₁ ∘ g₂)
+   (show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁]; reflexivity)
+   (show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂]; reflexivity)
+
+definition arrow_congr₁ {A₁ A₂ B₁ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
+| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
+  mk
+   (λ (h : A₁ → B₁) (a : A₂), f₂ (h (g₁ a)))
+   (λ (h : A₂ → B₂) (a : A₁), g₂ (h (f₁ a)))
+   (λ h, funext (λ a, begin rewrite [l₁, l₂], reflexivity end))
+   (begin unfold [left_inverse, right_inverse] at *, intros, apply funext, intros, simp end)
+
+local attribute left_inverse right_inverse [reducible]
+
+definition arrow_congr₂ {A₁ A₂ B₁ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
+| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
+  mk (λ h a, f₂ (h (g₁ a))) (λ h a, g₂ (h (f₁ a))) (by simp) (by simp)
+
+end equiv