From baf99779dc25e709a4c36766e2867e0d104f5cb9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Dec 2013 17:57:51 -0800
Subject: [PATCH] feat(frontends/lean/frontend_elaborator): use is_convertible
 to minimize number of coercions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend_elaborator.cpp | 10 +++++++++-
 tests/lean/norm_tac.lean                   |  3 +++
 tests/lean/norm_tac.lean.expected.out      |  3 +++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index a966e491d..787f04bb9 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -172,6 +172,14 @@ class frontend_elaborator::imp {
             }
         }
 
+        bool is_convertible(expr const & from, expr const & to) {
+            try {
+                return m_ref.m_type_checker.is_convertible(from, to);
+            } catch (exception &) {
+                return false;
+            }
+        }
+
         /**
            \brief Make sure f_t is a Pi, if it is not, then return none_expr()
         */
@@ -363,7 +371,7 @@ class frontend_elaborator::imp {
                             new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a);
                         } else {
                             expr expected = abst_domain(*f_t);
-                            if (expected != *new_a_t) {
+                            if (!is_convertible(*new_a_t, expected)) {
                                 optional<expr> c = find_coercion(coercions, expected);
                                 if (c) {
                                     new_a = mk_app(*c, new_a); // apply coercion
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index fbebfac0c..b796eb8a9 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -1,8 +1,11 @@
 SetOption pp::implicit true
+SetOption pp::coercion true
+SetOption pp::notation false
 Variable vector (A : Type) (sz : Nat) : Type
 Variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 Variable V1 : vector Int 10
 Definition D := read V1 1 (by trivial_tac)
+Show Environment 1
 Variable b : Bool
 Definition a := b
 Theorem T : b => a := (by (** imp_tac() .. normalize_tac() .. assumption_tac() **))
diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out
index eabd3fbc4..c8d9283d4 100644
--- a/tests/lean/norm_tac.lean.expected.out
+++ b/tests/lean/norm_tac.lean.expected.out
@@ -1,10 +1,13 @@
   Set: pp::colors
   Set: pp::unicode
   Set: lean::pp::implicit
+  Set: lean::pp::coercion
+  Set: lean::pp::notation
   Assumed: vector
   Assumed: read
   Assumed: V1
   Defined: D
+Definition D : ℤ := @read ℤ 10 V1 1 Trivial
   Assumed: b
   Defined: a
   Proved: T