michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/coercion): simplify coercion_class

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-01 14:29:23 -07:00
parent 0f5b7a36f5
commit d5c38777af
2 changed files with 26 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/library/coercion.cpp
View file

@ -16,16 +16,22 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
namespace lean {
coercion_class coercion_class::mk_user(name n) { return coercion_class(coercion_class_kind::User, n); }
coercion_class coercion_class::mk_sort() { return coercion_class(coercion_class_kind::Sort); }
coercion_class coercion_class::mk_fun() { return coercion_class(coercion_class_kind::Fun); }
bool operator==(coercion_class const & c1, coercion_class const & c2) {
return c1.m_kind == c2.m_kind && c1.m_name == c2.m_name;
}
bool operator!=(coercion_class const & c1, coercion_class const & c2) {
return !(c1 == c2);
static name * g_fun = nullptr;
static name * g_sort = nullptr;
coercion_class::coercion_class():m_name(*g_sort) {}
coercion_class coercion_class::mk_user(name n) { return coercion_class(n); }
coercion_class coercion_class::mk_sort() { return coercion_class(*g_sort); }
coercion_class coercion_class::mk_fun() { return coercion_class(*g_fun); }
coercion_class_kind coercion_class::kind() const {
if (m_name == *g_sort) return coercion_class_kind::Sort;
else if (m_name == *g_fun) return coercion_class_kind::Fun;
else return coercion_class_kind::User;
}
std::ostream & operator<<(std::ostream & out, coercion_class const & cls) {
switch (cls.kind()) {
case coercion_class_kind::User: out << cls.get_name(); break;
@ -37,10 +43,7 @@ std::ostream & operator<<(std::ostream & out, coercion_class const & cls) {
struct coercion_class_cmp_fn {
int operator()(coercion_class const & c1, coercion_class const & c2) const {
if (c1.kind() != c2.kind())
return c1.kind() < c2.kind() ? -1 : 1;
else
return quick_cmp(c1.get_name(), c2.get_name());
return quick_cmp(c1.get_name(), c2.get_name());
}
};
@ -61,6 +64,7 @@ struct coercion_state {
typedef std::tuple<coercion_class, expr, expr> from_data;
name_map<list<from_data>> m_from; // map user-class -> list of (class, coercion-fun)
rb_map<coercion_class, list<name>, coercion_class_cmp_fn> m_to;
name_map<pair<name, unsigned>> m_coercions; // map coercion -> (from-class, num-args)
template<typename F>
@ -353,6 +357,9 @@ template class scoped_ext<coercion_config>;
typedef scoped_ext<coercion_config> coercion_ext;
void initialize_coercion() {
name p = name::mk_internal_unique_name();
g_fun = new name(p, "Fun");
g_sort = new name(p, "Sort");
g_class_name = new name("coercions");
g_key = new std::string("coerce");
coercion_ext::initialize();
@ -362,6 +369,8 @@ void finalize_coercion() {
coercion_ext::finalize();
delete g_key;
delete g_class_name;
delete g_fun;
delete g_sort;
}
environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios, bool persistent) {

11
src/library/coercion.h
View file

@ -18,17 +18,16 @@ enum class coercion_class_kind { User, Sort, Fun };
We support three kinds of classes: User, Sort, Function.
*/
class coercion_class {
coercion_class_kind m_kind;
name m_name; // relevant only if m_kind == User
coercion_class(coercion_class_kind k, name const & n = name()):m_kind(k), m_name(n) {}
coercion_class(name const & n): m_name(n) {}
public:
coercion_class():m_kind(coercion_class_kind::Sort) {}
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);
friend bool operator!=(coercion_class const & c1, coercion_class const & c2);
coercion_class_kind kind() const { return m_kind; }
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; }
};