From 1150b195983e27afbc8f7a92d2004515c608ea2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Apr 2015 23:34:06 -0700
Subject: [PATCH] perf(frontends/lean/elaborator): do not invoke recursive
 equation compiler when equations still contain metavariables

---
 src/frontends/lean/elaborator.cpp      | 8 ++++++--
 src/frontends/lean/elaborator.h        | 2 +-
 tests/lean/place_eqn.lean.expected.out | 8 +++-----
 tests/lean/run/eq13.lean               | 2 +-
 tests/lean/run/eq2.lean                | 4 ++--
 5 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index fdb2bd2d4..79f3952b8 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1053,7 +1053,8 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
         substitution new_s  = s;
         expr new_eqns       = new_s.instantiate_all(eqns);
         new_eqns            = solve_unassigned_mvars(new_s, new_eqns);
-        display_unassigned_mvars(new_eqns, new_s);
+        if (display_unassigned_mvars(new_eqns, new_s))
+            return lazy_list<constraints>();
         type_checker_ptr tc = mk_type_checker(_env, ngen, relax);
         new_eqns            = assign_equation_lhs_metas(*tc, new_eqns);
         expr val            = compile_equations(*tc, _ios, new_eqns, meta, meta_type, relax);
@@ -1746,7 +1747,8 @@ expr elaborator::solve_unassigned_mvars(substitution & subst, expr const & e) {
     return solve_unassigned_mvars(subst, e, visited);
 }
 
-void elaborator::display_unassigned_mvars(expr const & e, substitution const & s) {
+bool elaborator::display_unassigned_mvars(expr const & e, substitution const & s) {
+    bool r = false;
     if (check_unassigned() && has_metavar(e)) {
         substitution tmp_s(s);
         visit_unassigned_mvars(e, [&](expr const & mvar) {
@@ -1757,9 +1759,11 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s
                     bool relax     = true;
                     proof_state ps(goals(g), s, m_ngen, constraints(), relax);
                     display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder");
+                    r = true;
                 }
             });
     }
+    return r;
 }
 
 /** \brief Check whether the solution found by the elaborator is producing too specific
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index abb0ac2c5..4d6e3c825 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -155,7 +155,7 @@ class elaborator : public coercion_info_manager {
     void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr const & e);
-    void display_unassigned_mvars(expr const & e, substitution const & s);
+    bool display_unassigned_mvars(expr const & e, substitution const & s);
     void check_sort_assignments(substitution const & s);
     expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
     std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
diff --git a/tests/lean/place_eqn.lean.expected.out b/tests/lean/place_eqn.lean.expected.out
index aebf76354..eb8a6d0e6 100644
--- a/tests/lean/place_eqn.lean.expected.out
+++ b/tests/lean/place_eqn.lean.expected.out
@@ -5,8 +5,6 @@ place_eqn.lean:5:18: error: don't know how to synthesize placeholder
 foo : ℕ → ℕ,
 a : ℕ
 ⊢ ℕ
-place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
-remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a : ℕ),
-    nat.brec_on a
-      (λ (a_1 : ℕ) (b : …), nat.cases_on a_1 (λ (b_1 : …), ?M_1) (λ (a_2 : ℕ) (b_1 : …), ?M_2) b)
+place_eqn.lean:3:11: error: failed to synthesize placeholder
+
+⊢ ℕ → ℕ
diff --git a/tests/lean/run/eq13.lean b/tests/lean/run/eq13.lean
index d9f676e3b..099d28815 100644
--- a/tests/lean/run/eq13.lean
+++ b/tests/lean/run/eq13.lean
@@ -7,7 +7,7 @@ definition f : nat → nat → nat
 
 theorem f_zero_right : ∀ a, f a 0 = 0
 | f_zero_right 0        := rfl
-| f_zero_right (succ _) := rfl
+| f_zero_right (succ a) := rfl
 
 theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
 rfl
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index f3639b0aa..6ebf0d1cd 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,5 +1,5 @@
 definition symm {A : Type} : Π {a b : A}, a = b → b = a
-| symm rfl := rfl
+| a a rfl := rfl
 
 definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
-| trans rfl rfl := rfl
+| a a a rfl rfl := rfl