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

refactor(library/coercion): simplify coercion module API

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-01 14:40:12 -07:00
parent d5c38777af
commit d44d576194
3 changed files with 26 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/coercion_elaborator.cpp
View file

@ -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));

23
src/library/coercion.cpp
View file

@ -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;
}
}

28
src/library/coercion.h
View file

@ -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;