From d44d576194eb311323ecf0cc0a0f3d62b3514b50 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jul 2015 14:40:12 -0700
Subject: [PATCH] refactor(library/coercion): simplify coercion module API

---
 src/frontends/lean/coercion_elaborator.cpp |  5 ++--
 src/library/coercion.cpp                   | 23 ++++++++++++++++--
 src/library/coercion.h                     | 28 +++-------------------
 3 files changed, 26 insertions(+), 30 deletions(-)

diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp
index 8101b049b..4577669f4 100644
--- a/src/frontends/lean/coercion_elaborator.cpp
+++ b/src/frontends/lean/coercion_elaborator.cpp
@@ -133,7 +133,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc
                 it_from  = instantiate(binding_body(it_from), local);
                 it_to    = instantiate(binding_body(it_to), local);
             }
-            buffer<std::tuple<coercion_class, expr, expr>> alts;
+            buffer<expr> alts;
             get_coercions_from(from_tc.env(), it_from, alts);
             expr fn_a;
             if (!locals.empty())
@@ -146,8 +146,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc
             unsigned i = alts.size();
             while (i > 0) {
                 --i;
-                auto const & t = alts[i];
-                expr coe = std::get<1>(t);
+                expr coe = alts[i];
                 if (!locals.empty())
                     coe = Fun(fn_a, Fun(locals, mk_app(coe, mk_app(fn_a, locals))));
                 expr new_a = copy_tag(a, mk_app(coe, a));
diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp
index 79a2135cc..d1bd50574 100644
--- a/src/library/coercion.cpp
+++ b/src/library/coercion.cpp
@@ -16,6 +16,25 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 
 namespace lean {
+enum class coercion_class_kind { User, Sort, Fun };
+/**
+   \brief A coercion is a mapping between classes.
+   We support three kinds of classes: User, Sort, Function.
+*/
+class coercion_class {
+    name                m_name; // relevant only if m_kind == User
+    coercion_class(name const & n): m_name(n) {}
+public:
+    coercion_class();
+    static coercion_class mk_user(name n);
+    static coercion_class mk_sort();
+    static coercion_class mk_fun();
+    friend bool operator==(coercion_class const & c1, coercion_class const & c2) { return c1.m_name == c2.m_name; }
+    friend bool operator!=(coercion_class const & c1, coercion_class const & c2) { return c1.m_name != c2.m_name; }
+    coercion_class_kind kind() const;
+    name get_name() const { return m_name; }
+};
+
 static name * g_fun  = nullptr;
 static name * g_sort = nullptr;
 
@@ -489,7 +508,7 @@ list<expr> get_coercions_to_fun(environment const & env, expr const & C) {
     return get_coercions(env, C, coercion_class::mk_fun());
 }
 
-bool get_coercions_from(environment const & env, expr const & C, buffer<std::tuple<coercion_class, expr, expr>> & result) {
+bool get_coercions_from(environment const & env, expr const & C, buffer<expr> & result) {
     buffer<expr> args;
     expr const & C_fn = get_app_rev_args(C, args);
     if (!is_constant(C_fn))
@@ -507,7 +526,7 @@ bool get_coercions_from(environment const & env, expr const & C, buffer<std::tup
             expr t = instantiate_univ_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, c, t);
+            result.push_back(c);
             r = true;
         }
     }
diff --git a/src/library/coercion.h b/src/library/coercion.h
index 1a5c5e1b1..90cac2877 100644
--- a/src/library/coercion.h
+++ b/src/library/coercion.h
@@ -12,25 +12,6 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 
 namespace lean {
-enum class coercion_class_kind { User, Sort, Fun };
-/**
-   \brief A coercion is a mapping between classes.
-   We support three kinds of classes: User, Sort, Function.
-*/
-class coercion_class {
-    name                m_name; // relevant only if m_kind == User
-    coercion_class(name const & n): m_name(n) {}
-public:
-    coercion_class();
-    static coercion_class mk_user(name n);
-    static coercion_class mk_sort();
-    static coercion_class mk_fun();
-    friend bool operator==(coercion_class const & c1, coercion_class const & c2) { return c1.m_name == c2.m_name; }
-    friend bool operator!=(coercion_class const & c1, coercion_class const & c2) { return c1.m_name != c2.m_name; }
-    coercion_class_kind kind() const;
-    name get_name() const { return m_name; }
-};
-
 /**
    \brief Add an new coercion in the given environment.
 
@@ -58,8 +39,6 @@ public:
    \remark if persistent == true, then coercion is saved in .olean files
 */
 environment add_coercion(environment const & env, name const & f, io_state const & ios, bool persistent = true);
-environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios,
-                         bool persistent = true);
 /** \brief If \c f is a coercion, then return the name of the 'from-class' and the number of
     class parameters.
 */
@@ -67,7 +46,6 @@ optional<pair<name, unsigned>> is_coercion(environment const & env, name const &
 optional<pair<name, unsigned>> is_coercion(environment const & env, expr const & f);
 /** \brief Return true iff the given environment has coercions from a user-class named \c C. */
 bool has_coercions_from(environment const & env, name const & C);
-bool has_coercions_from(environment const & env, expr const & C);
 /** \brief Return true iff the given environment has coercions to a user-class named \c D. */
 bool has_coercions_to(environment const & env, name const & D);
 bool has_coercions_to_sort(environment const & env);
@@ -82,12 +60,12 @@ list<expr> get_coercions_to_sort(environment const & env, expr const & C);
 list<expr> get_coercions_to_fun(environment const & env, expr const & C);
 /**
    \brief Return all coercions C >-> D for the type C of the form (C_name.{l1 ... lk} t_1 ... t_n)
-   The result is a tuple (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.
+   The coercions are stored in result.
+   The Boolean result is true if at least one coercion is added to \c result.
 
    \remark The most recent coercions occur first.
 */
-bool get_coercions_from(environment const & env, expr const & C, buffer<std::tuple<coercion_class, expr, expr>> & result);
+bool get_coercions_from(environment const & env, expr const & C, buffer<expr> & result);
 
 typedef std::function<void(name const &, name const &, expr const &, level_param_names const &, unsigned)> coercion_user_fn;
 typedef std::function<void(name const &, expr const &, level_param_names const &, unsigned)> coercion_sort_fn;