From 2d31c6c0b22c80d02c8e4a7219b41d08c2c35e3a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 May 2014 11:35:47 -0700
Subject: [PATCH] feat(library/coercion): improve get_user_coercions API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/coercion.cpp | 15 ++++++++++-----
 src/library/coercion.h   |  4 ++--
 tests/lua/coe1.lua       | 13 +++++++++++++
 3 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp
index 22e8e2af7..3ab54393f 100644
--- a/src/library/coercion.cpp
+++ b/src/library/coercion.cpp
@@ -391,7 +391,7 @@ optional<expr> get_coercion_to_fun(environment const & env, expr const & C) {
     return get_coercion(env, C, coercion_class::mk_fun());
 }
 
-bool get_user_coercions(environment const & env, expr const & C, buffer<std::pair<expr, name>> & result) {
+bool get_user_coercions(environment const & env, expr const & C, buffer<std::tuple<name, expr, expr>> & result) {
     buffer<expr> args;
     expr const & C_fn = get_app_rev_args(C, args);
     if (!is_constant(C_fn))
@@ -407,7 +407,10 @@ bool get_user_coercions(environment const & env, expr const & C, buffer<std::pai
             length(info.m_level_params) == length(const_levels(C_fn))) {
             expr f = instantiate_params(info.m_fun, info.m_level_params, const_levels(C_fn));
             expr c = apply_beta(f, args.size(), args.data());
-            result.emplace_back(c, info.m_to.get_name());
+            expr t = instantiate_params(info.m_fun_type, info.m_level_params, const_levels(C_fn));
+            for (unsigned i = 0; i < args.size(); i++) t = binding_body(t);
+            t = instantiate(t, args.size(), args.data());
+            result.emplace_back(info.m_to.get_name(), c, t);
             r = true;
         }
     }
@@ -472,16 +475,18 @@ static int get_coercion(lua_State * L) { return push_optional_expr(L, get_coerci
 static int get_coercion_to_sort(lua_State * L) { return push_optional_expr(L, get_coercion_to_sort(to_environment(L, 1), to_expr(L, 2))); }
 static int get_coercion_to_fun(lua_State * L) { return push_optional_expr(L, get_coercion_to_fun(to_environment(L, 1), to_expr(L, 2))); }
 static int get_user_coercions(lua_State * L) {
-    buffer<std::pair<expr, name>> r;
+    buffer<std::tuple<name, expr, expr>> r;
     get_user_coercions(to_environment(L, 1), to_expr(L, 2), r);
     lua_newtable(L);
     int i = 1;
     for (auto p : r) {
         lua_newtable(L);
-        push_expr(L, p.first);
+        push_name(L, std::get<0>(p));
         lua_rawseti(L, -2, 1);
-        push_name(L, p.second);
+        push_expr(L, std::get<1>(p));
         lua_rawseti(L, -2, 2);
+        push_expr(L, std::get<2>(p));
+        lua_rawseti(L, -2, 3);
         lua_rawseti(L, -2, i);
         i = i + 1;
     }
diff --git a/src/library/coercion.h b/src/library/coercion.h
index 200a74949..c7b26fa53 100644
--- a/src/library/coercion.h
+++ b/src/library/coercion.h
@@ -53,12 +53,12 @@ optional<expr> get_coercion_to_sort(environment const & env, expr const & C);
 optional<expr> get_coercion_to_fun(environment const & env, expr const & C);
 /**
    \brief Return all user coercions C >-> D for the type C of the form (C_name.{l1 ... lk} t_1 ... t_n)
-   The result is a pair (coercion, user-class D), and is stored in the result buffer \c result.
+   The result is a pair (user-class D, coercion, coercion type), and is stored in the result buffer \c result.
    The Boolean result is true if at least one pair is added to \c result.
 
    \remark The most recent coercions occur first.
 */
-bool get_user_coercions(environment const & env, expr const & C, buffer<std::pair<expr, name>> & result);
+bool get_user_coercions(environment const & env, expr const & C, buffer<std::tuple<name, expr, expr>> & result);
 
 void for_each_coercion_user(environment const & env,
                             std::function<void(name const &, name const &, expr const &, level_param_names const &, unsigned)> const & f);
diff --git a/tests/lua/coe1.lua b/tests/lua/coe1.lua
index 0eda8e988..c4ea55eb5 100644
--- a/tests/lua/coe1.lua
+++ b/tests/lua/coe1.lua
@@ -67,3 +67,16 @@ env2 = add_coercion(env2, "lst2nat")
 print("---------")
 for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D)) end)
 for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
+
+assert(has_coercions_from(env2, lst_nat))
+assert(not has_coercions_from(env2, Const("foo")))
+assert(not has_coercions_from(env2, Const("lst", {1})))
+assert(has_coercions_from(env2, Const("vec", {1})(nat, one)))
+assert(not has_coercions_from(env2, Const("vec", {1})(nat)))
+assert(not has_coercions_from(env2, Const("vec")(nat, one)))
+
+print("Coercions (vec nat one): ")
+cs = get_user_coercions(env2, Const("vec", {1})(nat, one))
+for i = 1, #cs do
+   print(tostring(cs[i][1]) .. " : " .. tostring(cs[i][3]) .. " : " .. tostring(cs[i][2]))
+end