From edcbe6fe107c02c2ac44248bf0ad9b4cb632a5c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Sep 2014 12:01:14 -0700 Subject: [PATCH] feat(frontends/lean): allow multiple coercions from class A to B, closes #187 See new tests (for examples) tests/lean/run/coe10.lean tests/lean/run/coe11.lean tests/lean/run/coe9.lean Signed-off-by: Leonardo de Moura --- src/frontends/lean/coercion_elaborator.cpp | 87 +++++++------- src/frontends/lean/coercion_elaborator.h | 17 +++ src/frontends/lean/elaborator.cpp | 74 ++++++++++-- src/frontends/lean/info_manager.cpp | 6 + src/library/coercion.cpp | 131 ++++++++++++--------- src/library/coercion.h | 6 +- tests/lean/run/coe10.lean | 17 +++ tests/lean/run/coe11.lean | 25 ++++ tests/lean/run/coe9.lean | 27 +++++ tests/lua/coe1.lua | 28 +++-- tests/lua/coe2.lua | 6 +- tests/lua/coe3.lua | 4 +- tests/lua/coe5.lua | 4 +- tests/lua/scope.lua | 6 +- 14 files changed, 308 insertions(+), 130 deletions(-) create mode 100644 tests/lean/run/coe10.lean create mode 100644 tests/lean/run/coe11.lean create mode 100644 tests/lean/run/coe9.lean diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp index 8357ac2c3..656f2e011 100644 --- a/src/frontends/lean/coercion_elaborator.cpp +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -13,41 +13,33 @@ Author: Leonardo de Moura #include "frontends/lean/coercion_elaborator.h" namespace lean { +coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr const & arg, + list const & choices, list const & coes, + bool use_id): + m_info(info), m_arg(arg), m_id(use_id), m_choices(choices), m_coercions(coes) { + lean_assert(length(m_coercions) + 1 == length(m_choices)); +} -struct coercion_elaborator : public choice_iterator { - coercion_info_manager & m_info; - expr m_arg; - bool m_id; // true if identity was not tried yet - list m_choices; - list m_coercions; - - coercion_elaborator(coercion_info_manager & info, expr const & arg, - list const & choices, list const & coes): - m_info(info), m_arg(arg), m_id(true), m_choices(choices), m_coercions(coes) { - lean_assert(length(m_coercions) + 1 == length(m_choices)); +optional coercion_elaborator::next() { + if (!m_choices) + return optional(); + if (m_id) { + m_id = false; + m_info.erase_coercion_info(m_arg); + } else if (m_coercions) { + expr c = head(m_coercions); + m_coercions = tail(m_coercions); + m_info.save_coercion_info(m_arg, mk_app(c, m_arg)); } - - optional next() { - if (!m_choices) - return optional(); - if (m_id) { - m_id = false; - m_info.erase_coercion_info(m_arg); - } else if (m_coercions) { - expr c = head(m_coercions); - m_coercions = tail(m_coercions); - m_info.save_coercion_info(m_arg, mk_app(c, m_arg)); - } - auto r = head(m_choices); - m_choices = tail(m_choices); - return optional(r); - } -}; + auto r = head(m_choices); + m_choices = tail(m_choices); + return optional(r); +} constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor, bool relax) { - auto choice_fn = [=, &tc, &infom](expr const & mvar, expr const & d_type, substitution const & s, + auto choice_fn = [=, &tc, &infom](expr const & meta, expr const & d_type, substitution const & s, name_generator const & /* ngen */) { expr new_a_type; justification new_a_type_jst; @@ -65,7 +57,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, delay_factor+1, relax))); } else { // giveup... - return lazy_list(constraints(mk_eq_cnstr(mvar, a, justification(), relax))); + return lazy_list(constraints(mk_eq_cnstr(meta, a, justification(), relax))); } } constraint_seq cs; @@ -77,7 +69,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, buffer choices; buffer coes; // first alternative: no coercion - constraint_seq cs1 = cs + mk_eq_cnstr(mvar, a, justification(), relax); + constraint_seq cs1 = cs + mk_eq_cnstr(meta, a, justification(), relax); choices.push_back(cs1.to_list()); unsigned i = alts.size(); while (i > 0) { @@ -86,26 +78,41 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, expr coe = std::get<1>(t); expr new_a = copy_tag(a, mk_app(coe, a)); coes.push_back(coe); - constraint_seq csi = cs + mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax); + constraint_seq csi = cs + mk_eq_cnstr(meta, new_a, new_a_type_jst, relax); choices.push_back(csi.to_list()); } - return choose(std::make_shared(infom, mvar, + return choose(std::make_shared(infom, meta, to_list(choices.begin(), choices.end()), to_list(coes.begin(), coes.end()))); } else { - expr new_a = a; expr new_d_type = tc.whnf(d_type, cs); expr const & d_cls = get_app_fn(new_d_type); if (is_constant(d_cls)) { - if (auto c = get_coercion(tc.env(), new_a_type, const_name(d_cls))) { - new_a = copy_tag(a, mk_app(*c, a)); - infom.save_coercion_info(a, new_a); - } else { + list coes = get_coercions(tc.env(), new_a_type, const_name(d_cls)); + if (is_nil(coes)) { + expr new_a = a; infom.erase_coercion_info(a); + cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax); + return lazy_list(cs.to_list()); + } else if (is_nil(tail(coes))) { + expr new_a = copy_tag(a, mk_app(head(coes), a)); + infom.save_coercion_info(a, new_a); + cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax); + return lazy_list(cs.to_list()); + } else { + list choices = map2(coes, [&](expr const & coe) { + expr new_a = copy_tag(a, mk_app(coe, a)); + constraint c = mk_eq_cnstr(meta, new_a, new_a_type_jst, relax); + return (cs + c).to_list(); + }); + return choose(std::make_shared(infom, meta, choices, coes, false)); } + } else { + expr new_a = a; + infom.erase_coercion_info(a); + cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax); + return lazy_list(cs.to_list()); } - cs += mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax); - return lazy_list(cs.to_list()); } }; return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax); diff --git a/src/frontends/lean/coercion_elaborator.h b/src/frontends/lean/coercion_elaborator.h index 84b1e6c91..f59759410 100644 --- a/src/frontends/lean/coercion_elaborator.h +++ b/src/frontends/lean/coercion_elaborator.h @@ -17,6 +17,19 @@ public: virtual void save_coercion_info(expr const & e, expr const & c) = 0; }; +class coercion_elaborator : public choice_iterator { + coercion_info_manager & m_info; + expr m_arg; + bool m_id; // true if identity was not tried yet + list m_choices; + list m_coercions; +public: + coercion_elaborator(coercion_info_manager & info, expr const & arg, + list const & choices, list const & coes, + bool use_id = true); + optional next(); +}; + /** \brief Create a metavariable, and attach choice constraint for generating coercions of the form f a, where \c f is registered coercion, and \c a is the input argument that has type \c a_type, but is expected @@ -34,4 +47,8 @@ public: pair mk_coercion_elaborator( type_checker & tc, coercion_info_manager & infom, local_context & ctx, bool relax, expr const & a, expr const & a_type, expr const & expected_type, justification const & j); + +pair coercions_to_choice(coercion_info_manager & infom, local_context & ctx, + list const & coes, expr const & a, + justification const & j, bool relax); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e0a6fa48c..fceda5e2f 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -357,15 +357,48 @@ public: } if (!is_pi(f_type)) { // try coercion to function-class - optional c = get_coercion_to_fun(env(), f_type); - if (c) { + list coes = get_coercions_to_fun(env(), f_type); + if (is_nil(coes)) { + throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); + } else if (is_nil(tail(coes))) { expr old_f = f; - f = mk_app(*c, f, f.get_tag()); + f = mk_app(head(coes), f, f.get_tag()); f_type = infer_type(f, cs); save_coercion_info(old_f, f); lean_assert(is_pi(f_type)); } else { - throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); + bool relax = m_relax_main_opaque; + justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) { + return pp_function_expected(fmt, substitution(subst).instantiate(f)); + }); + auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator const &) { + list choices = map2(coes, [&](expr const & coe) { + expr new_f = copy_tag(f, ::lean::mk_app(coe, f)); + constraint_seq cs; + while (true) { + expr new_f_type = m_tc[relax]->infer(new_f, cs); + if (!is_pi(new_f_type)) + break; + binder_info bi = binding_info(new_f_type); + if (!bi.is_strict_implicit() && !bi.is_implicit()) + break; + tag g = f.get_tag(); + bool is_strict = false; + expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(new_f_type)), g, is_strict, cs); + new_f = mk_app(new_f, imp_arg, g); + } + cs += mk_eq_cnstr(meta, new_f, j, relax); + return cs.to_list(); + }); + return choose(std::make_shared(*this, f, choices, coes, false)); + }; + f = m_full_context.mk_meta(none_expr(), f.get_tag()); + cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j, relax); + lean_assert(is_meta(f)); + // let type checker add constraint + f_type = infer_type(f, cs); + lean_assert(is_pi(f_type)); + f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs); } } else { erase_coercion_info(f); @@ -389,15 +422,30 @@ public: d_type = whnf(d_type).first; expr const & d_cls = get_app_fn(d_type); if (is_constant(d_cls)) { - if (auto c = get_coercion(env(), a_type, const_name(d_cls))) { - expr r = mk_app(*c, a, a.get_tag()); + list coes = get_coercions(env(), a_type, const_name(d_cls)); + if (is_nil(coes)) { + erase_coercion_info(a); + return a; + } else if (is_nil(tail(coes))) { + expr r = mk_app(head(coes), a, a.get_tag()); save_coercion_info(a, r); return r; } else { + for (expr const & coe : coes) { + expr r = mk_app(coe, a, a.get_tag()); + expr r_type = infer_type(r).first; + if (m_tc[m_relax_main_opaque]->is_def_eq(r_type, d_type).first) { + save_coercion_info(a, r); + return r; + } + } erase_coercion_info(a); + return a; } + } else { + erase_coercion_info(a); + return a; } - return a; } /** \brief Given a term a : a_type, and an expected type generate a metavariable with a delayed coercion. */ @@ -426,8 +474,8 @@ public: return to_ecs(a, dcs.second); } else { expr new_a = apply_coercion(a, a_type, expected_type); - bool coercion_worked = false; constraint_seq cs; + bool coercion_worked = false; if (!is_eqp(a, new_a)) { expr new_a_type = infer_type(new_a, cs); coercion_worked = m_tc[relax]->is_def_eq(new_a_type, expected_type, j, cs); @@ -575,13 +623,15 @@ public: return e; } } - optional c = get_coercion_to_sort(env(), t); - if (c) { - expr r = mk_app(*c, e, e.get_tag()); + list coes = get_coercions_to_sort(env(), t); + if (is_nil(coes)) { + throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); + } else { + // Remark: we ignore other coercions to sort + expr r = mk_app(head(coes), e, e.get_tag()); save_coercion_info(e, r); return r; } - throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); } /** \brief Similar to instantiate_rev, but assumes that subst contains only local constants. diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 80f8d6e4b..d881d9223 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -212,6 +212,12 @@ public: ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl; ios << "-- ACK" << endl; } + + virtual info_data_cell * instantiate(substitution & s) const { + expr e = s.instantiate(m_expr); + expr t = s.instantiate(m_type); + return is_eqp(e, m_expr) && is_eqp(t, m_type) ? nullptr : new coercion_info_data(get_column(), e, t); + } }; class symbol_info_data : public info_data_cell { diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index a995a88e2..0d5d781a7 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -71,31 +71,39 @@ struct coercion_info { struct coercion_state { rb_map, name_quick_cmp> m_coercion_info; // m_from and m_to contain "direct" coercions - rb_map>, name_quick_cmp> m_from; // map user-class -> list of (class, coercion-fun) + typedef std::tuple from_data; + rb_map, name_quick_cmp> m_from; // map user-class -> list of (class, coercion-fun) rb_map, coercion_class_cmp_fn> m_to; rb_map, name_quick_cmp> m_coercions; // map coercion -> (from-class, num-args) - coercion_info get_info(name const & from, coercion_class const & to) { + + template + void for_each_info(name const & from, coercion_class const & to, F && f) { auto it = m_coercion_info.find(from); lean_assert(it); for (coercion_info info : *it) { - if (info.m_to == to) - return info; + if (info.m_to == to) { + f(info); + } } - lean_unreachable(); // LCOV_EXCL_LINE } - void update_from_to(name const & C, coercion_class const & D, expr const & f, io_state const & ios) { + + void update_from_to(type_checker & tc, name const & C, coercion_class const & D, + expr const & f, expr const & f_type, io_state const & ios) { auto it1 = m_from.find(C); if (!it1) { - m_from.insert(C, to_list(mk_pair(D, f))); + m_from.insert(C, to_list(from_data(D, f, f_type))); } else { + coercion_class D_it; expr f_it, f_type_it; auto it = it1->begin(); auto end = it1->end(); - for (; it != end; ++it) - if (it->first == D) + for (; it != end; ++it) { + std::tie(D_it, f_it, f_type_it) = *it; + if (D_it == D && tc.is_def_eq(f_type_it, f_type).first) break; + } if (it == end) - m_from.insert(C, cons(mk_pair(D, f), *it1)); - else if (it->second != f) + m_from.insert(C, cons(from_data(D, f, f_type), *it1)); + else if (std::get<1>(*it) != f) ios.get_diagnostic_channel() << "replacing the coercion from '" << C << "' to '" << D << "'\n"; } auto it2 = m_to.find(D); @@ -158,18 +166,26 @@ optional type_to_coercion_class(expr const & t) { } } -typedef list> arrows; -static bool contains(arrows const & a, name const & C, coercion_class const & D) { - return std::find(a.begin(), a.end(), mk_pair(C, D)) != a.end(); +typedef std::tuple arrow; +typedef list arrows; +static bool contains(type_checker & tc, arrows const & as, name const & C, coercion_class const & D, expr const & f_type) { + name C_it; coercion_class D_it; expr f_type_it; + for (arrow const & a : as) { + std::tie(C_it, D_it, f_type_it) = a; + if (C == C_it && D == D_it && tc.is_def_eq(f_type_it, f_type).first) + return true; + } + return false; } -static arrows insert(arrows const & a, name const & C, coercion_class const & D) { - return arrows(mk_pair(C, D), a); +static arrows insert(arrows const & a, name const & C, coercion_class const & D, expr const & f_type) { + return arrows(arrow(C, D, f_type), a); } struct add_coercion_fn { - coercion_state m_state; - arrows m_visited; - io_state const & m_ios; + type_checker m_tc; + coercion_state m_state; + arrows m_visited; + io_state const & m_ios; void add_coercion_trans(name const & C, level_param_names const & f_level_params, expr const & f, expr const & f_type, unsigned f_num_args, @@ -220,10 +236,11 @@ struct add_coercion_fn { if (!it1) return; for (name const & B : *it1) { - coercion_info info = m_state.get_info(B, C_cls); - // B >-> C >-> D - add_coercion_trans(B, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, - ls, f, f_type, num_args, cls); + m_state.for_each_info(B, C_cls, [&](coercion_info const & info) { + // B >-> C >-> D + add_coercion_trans(B, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, + ls, f, f_type, num_args, cls); + }); } } @@ -237,11 +254,12 @@ struct add_coercion_fn { if (!it) return; for (auto const & p : *it) { - coercion_class E = p.first; - coercion_info info = m_state.get_info(D, E); - // C >-> D >-> E - add_coercion_trans(C, ls, f, f_type, num_args, - info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, info.m_to); + coercion_class E = std::get<0>(p); + m_state.for_each_info(D, E, [&](coercion_info const & info) { + // C >-> D >-> E + add_coercion_trans(C, ls, f, f_type, num_args, + info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, info.m_to); + }); } } @@ -253,7 +271,9 @@ struct add_coercion_fn { m_state.m_coercion_info.insert(C, infos); } else { list infos = *it; - infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; }); + infos = filter(infos, [&](coercion_info const & info) { + return info.m_to != cls || !m_tc.is_def_eq(info.m_fun_type, f_type).first; + }); infos = cons(coercion_info(f, f_type, ls, num_args, cls), infos); m_state.m_coercion_info.insert(C, infos); } @@ -263,23 +283,23 @@ struct add_coercion_fn { void add_coercion(name const & C, expr const & f, expr const & f_type, level_param_names const & ls, unsigned num_args, coercion_class const & cls) { - if (contains(m_visited, C, cls)) + if (contains(m_tc, m_visited, C, cls, f_type)) return; if (cls.kind() == coercion_class_kind::User && cls.get_name() == C) return; - m_visited = insert(m_visited, C, cls); + m_visited = insert(m_visited, C, cls, f_type); add_coercion_core(C, f, f_type, ls, num_args, cls); add_coercion_trans_to(C, f, f_type, ls, num_args, cls); add_coercion_trans_from(C, f, f_type, ls, num_args, cls); } - add_coercion_fn(coercion_state const & s, io_state const & ios): - m_state(s), m_ios(ios) {} + add_coercion_fn(environment const & env, coercion_state const & s, io_state const & ios): + m_tc(env), m_state(s), m_ios(ios) {} coercion_state operator()(name const & C, expr const & f, expr const & f_type, level_param_names const & ls, unsigned num_args, coercion_class const & cls) { add_coercion(C, f, f_type, ls, num_args, cls); - m_state.update_from_to(C, cls, f, m_ios); + m_state.update_from_to(m_tc, C, cls, f, f_type, m_ios); return m_state; } }; @@ -305,7 +325,7 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'"); else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C) throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); - return add_coercion_fn(st, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls); + return add_coercion_fn(env, st, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls); } t = binding_body(t); num++; @@ -414,34 +434,35 @@ bool has_coercions_from(environment const & env, expr const & C) { length(head(cs).m_level_params) == length(const_levels(C_fn)); } -optional get_coercion(environment const & env, expr const & C, coercion_class const & D) { +list get_coercions(environment const & env, expr const & C, coercion_class const & D) { buffer args; expr const & C_fn = get_app_rev_args(C, args); if (!is_constant(C_fn)) - return none_expr(); + return list(); coercion_state const & ext = coercion_ext::get_state(env); auto it = ext.m_coercion_info.find(const_name(C_fn)); if (!it) - return none_expr(); + return list(); + buffer r; for (coercion_info const & info : *it) { if (info.m_to == D && info.m_num_args == args.size() && length(info.m_level_params) == length(const_levels(C_fn))) { expr f = instantiate_univ_params(info.m_fun, info.m_level_params, const_levels(C_fn)); - return some_expr(apply_beta(f, args.size(), args.data())); + r.push_back(apply_beta(f, args.size(), args.data())); } } - return none_expr(); + return to_list(r.begin(), r.end()); } -optional get_coercion(environment const & env, expr const & C, name const & D) { - return get_coercion(env, C, coercion_class::mk_user(D)); +list get_coercions(environment const & env, expr const & C, name const & D) { + return get_coercions(env, C, coercion_class::mk_user(D)); } -optional get_coercion_to_sort(environment const & env, expr const & C) { - return get_coercion(env, C, coercion_class::mk_sort()); +list get_coercions_to_sort(environment const & env, expr const & C) { + return get_coercions(env, C, coercion_class::mk_sort()); } -optional get_coercion_to_fun(environment const & env, expr const & C) { - return get_coercion(env, C, coercion_class::mk_fun()); +list get_coercions_to_fun(environment const & env, expr const & C) { + return get_coercions(env, C, coercion_class::mk_fun()); } bool get_user_coercions(environment const & env, expr const & C, buffer> & result) { @@ -535,16 +556,16 @@ static int has_coercions_from(lua_State * L) { return push_boolean(L, has_coercions_from(to_environment(L, 1), to_name_ext(L, 2))); } -static int get_coercion(lua_State * L) { - return push_optional_expr(L, get_coercion(to_environment(L, 1), to_expr(L, 2), to_name_ext(L, 3))); +static int get_coercions(lua_State * L) { + return push_list_expr(L, get_coercions(to_environment(L, 1), to_expr(L, 2), to_name_ext(L, 3))); } -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_coercions_to_sort(lua_State * L) { + return push_list_expr(L, get_coercions_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_coercions_to_fun(lua_State * L) { + return push_list_expr(L, get_coercions_to_fun(to_environment(L, 1), to_expr(L, 2))); } static int get_user_coercions(lua_State * L) { @@ -595,9 +616,9 @@ void open_coercion(lua_State * L) { SET_GLOBAL_FUN(add_coercion, "add_coercion"); SET_GLOBAL_FUN(is_coercion, "is_coercion"); SET_GLOBAL_FUN(has_coercions_from, "has_coercions_from"); - SET_GLOBAL_FUN(get_coercion, "get_coercion"); - SET_GLOBAL_FUN(get_coercion_to_sort, "get_coercion_to_sort"); - SET_GLOBAL_FUN(get_coercion_to_fun, "get_coercion_to_fun"); + SET_GLOBAL_FUN(get_coercions, "get_coercions"); + SET_GLOBAL_FUN(get_coercions_to_sort, "get_coercions_to_sort"); + SET_GLOBAL_FUN(get_coercions_to_fun, "get_coercions_to_fun"); SET_GLOBAL_FUN(get_user_coercions, "get_user_coercions"); SET_GLOBAL_FUN(for_each_coercion_user, "for_each_coercion_user"); SET_GLOBAL_FUN(for_each_coercion_sort, "for_each_coercion_sort"); diff --git a/src/library/coercion.h b/src/library/coercion.h index f8d917450..e6c998e3e 100644 --- a/src/library/coercion.h +++ b/src/library/coercion.h @@ -53,9 +53,9 @@ bool has_coercions_to(environment const & env, name const & D); The coercion is a unary function that takes a term of type (C_name.{l1 lk} t_1 ... t_n) and returns and element of type (D.{L_1 L_o} s_1 ... s_m) */ -optional get_coercion(environment const & env, expr const & C, name const & D); -optional get_coercion_to_sort(environment const & env, expr const & C); -optional get_coercion_to_fun(environment const & env, expr const & C); +list get_coercions(environment const & env, expr const & C, name const & D); +list get_coercions_to_sort(environment const & env, expr const & C); +list get_coercions_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 (user-class D, coercion, coercion type), and is stored in the result buffer \c result. diff --git a/tests/lean/run/coe10.lean b/tests/lean/run/coe10.lean new file mode 100644 index 000000000..28330219f --- /dev/null +++ b/tests/lean/run/coe10.lean @@ -0,0 +1,17 @@ +import data.nat +open nat + +inductive fn2 (A B C : Type) := +mk : (A → C) → (B → C) → fn2 A B C + +definition to_ac [coercion] {A B C : Type} (f : fn2 A B C) : A → C := +fn2.rec (λ f g, f) f + +definition to_bc [coercion] {A B C : Type} (f : fn2 A B C) : B → C := +fn2.rec (λ f g, g) f + +variable f : fn2 Prop nat nat +variable a : Prop +variable n : nat +check f a +check f n diff --git a/tests/lean/run/coe11.lean b/tests/lean/run/coe11.lean new file mode 100644 index 000000000..b9cf657c8 --- /dev/null +++ b/tests/lean/run/coe11.lean @@ -0,0 +1,25 @@ +import data.category +open category + +inductive my_functor {obC obD : Type} (C : category obC) (D : category obD) : Type := +mk : Π (obF : obC → obD) (morF : Π{A B : obC}, mor A B → mor (obF A) (obF B)), + (Π {A : obC}, morF (ID A) = ID (obF A)) → + (Π {A B C : obC} {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF f) → + my_functor C D + +definition my_object [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) : obC → obD := +my_functor.rec (λ obF morF Hid Hcomp, obF) F + +definition my_morphism [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) : + Π{A B : obC}, mor A B → mor (my_object F A) (my_object F B) := +my_functor.rec (λ obF morF Hid Hcomp, morF) F + +variables obC obD : Type +variables a b : obC +variable C : category obC +instance C +variable D : category obD +variable F : my_functor C D +variable m : mor a b +check F a +check F m diff --git a/tests/lean/run/coe9.lean b/tests/lean/run/coe9.lean new file mode 100644 index 000000000..9c16af0d7 --- /dev/null +++ b/tests/lean/run/coe9.lean @@ -0,0 +1,27 @@ +import data.nat +open nat + +variable list.{l} : Type.{l} → Type.{l} +variable vector.{l} : Type.{l} → nat → Type.{l} +variable matrix.{l} : Type.{l} → nat → nat → Type.{l} +variable length : Pi {A : Type}, list A → nat + +variable list_to_vec {A : Type} (l : list A) : vector A (length l) +variable to_row {A : Type} {n : nat} : vector A n → matrix A 1 n +variable to_col {A : Type} {n : nat} : vector A n → matrix A n 1 +variable to_list {A : Type} {n : nat} : vector A n → list A + +coercion to_row +coercion to_col +coercion list_to_vec +coercion to_list + +variable f {A : Type} {n : nat} (M : matrix A n 1) : nat +variable g {A : Type} {n : nat} (M : matrix A 1 n) : nat +variable v : vector nat 10 +variable l : list nat + +check f v +check g v +check f l +check g l diff --git a/tests/lua/coe1.lua b/tests/lua/coe1.lua index e62322339..6f64eee7a 100644 --- a/tests/lua/coe1.lua +++ b/tests/lua/coe1.lua @@ -32,33 +32,41 @@ env = add_coercion(env, "lst2vec") assert(is_coercion(env, Const("lst2vec", {l}))) assert(has_coercions_from(env, "lst")) local lst_nat = lst_1(nat) -print(get_coercion(env, lst_nat, "vec")) + +function display_coercions(coes) + if not coes:is_nil() then + print(coes:head()) + display_coercions(coes:tail()) + end +end + +display_coercions(get_coercions(env, lst_nat, "vec")) env = add_coercion(env, "vec2mat") -print(get_coercion(env, lst_nat, "mat")) -assert(env:type_check(get_coercion(env, lst_nat, "mat"))) +display_coercions(get_coercions(env, lst_nat, "mat")) +assert(env:type_check(get_coercions(env, lst_nat, "mat"):head())) for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) env = add_coercion(env, "nat2lst") print("---------") for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) -print(get_coercion(env, nat, "mat")) -assert(env:type_check(get_coercion(env, nat, "mat"))) +print(get_coercions(env, nat, "mat"):head()) +assert(env:type_check(get_coercions(env, nat, "mat"):head())) env = add_coercion(env, "mat2dlst") print("---------") for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) -print(get_coercion(env, lst_nat, "dlst")) -assert(env:type_check(get_coercion(env, lst_nat, "dlst"))) +print(get_coercions(env, lst_nat, "dlst"):head()) +assert(env:type_check(get_coercions(env, lst_nat, "dlst"):head())) env:export("coe1_mod.olean") local env2 = import_modules("coe1_mod") -print(get_coercion(env2, lst_nat, "dlst")) -assert(env2:type_check(get_coercion(env2, lst_nat, "dlst"))) +print(get_coercions(env2, lst_nat, "dlst"):head()) +assert(env2:type_check(get_coercions(env2, lst_nat, "dlst"):head())) assert(is_coercion(env2, "vec2mat")) assert(is_coercion(env2, "lst2vec")) env2 = add_decl(env2, mk_var_decl("lst2vec2", {l}, Pi(A, ll, vec_l(A, len_l(A, ll))))) print("======") env2 = add_coercion(env2, "lst2vec2") print("======") -print(get_coercion(env2, lst_nat, "dlst")) +print(get_coercions(env2, lst_nat, "dlst"):head()) print("---------") for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) env2 = add_coercion(env2, "vec2lst") diff --git a/tests/lua/coe2.lua b/tests/lua/coe2.lua index cc4dacdb2..0d49d9601 100644 --- a/tests/lua/coe2.lua +++ b/tests/lua/coe2.lua @@ -13,9 +13,9 @@ env = add_decl(env, mk_var_decl("real", Type)) local nat = Const("nat") local real = Const("real") env = add_decl(env, mk_var_decl("f1", Const("functor", {1, 1})(nat, real))) -print(get_coercion_to_fun(env, Const("functor", {1, 1})(nat, real))) +print(get_coercions_to_fun(env, Const("functor", {1, 1})(nat, real)):head()) env = add_decl(env, mk_var_decl("sfunctor", {l1}, mk_arrow(mk_sort(l1), mk_sort(l1)))) env = add_decl(env, mk_var_decl("sf2f", {l1}, Pi(A, mk_arrow(Const("sfunctor", {l1})(A), Const("functor", {l1, l1})(A, A))))) env = add_coercion(env, "sf2f") -print(get_coercion_to_fun(env, Const("sfunctor", {1})(nat))) -assert(env:type_check(get_coercion_to_fun(env, Const("sfunctor", {1})(nat)))) +print(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head()) +assert(env:type_check(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head())) diff --git a/tests/lua/coe3.lua b/tests/lua/coe3.lua index 716925f0e..aa1634ca3 100644 --- a/tests/lua/coe3.lua +++ b/tests/lua/coe3.lua @@ -9,5 +9,5 @@ env = add_coercion(env, "carrier") env = add_decl(env, mk_var_decl("abg2g", {l}, mk_arrow(ab_group, group))) env = add_coercion(env, "abg2g") for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end) -print(get_coercion_to_sort(env, Const("abelian_group", {1}))) -assert(env:type_check(get_coercion_to_sort(env, Const("abelian_group", {1})))) +print(get_coercions_to_sort(env, Const("abelian_group", {1})):head()) +assert(env:type_check(get_coercions_to_sort(env, Const("abelian_group", {1})):head())) diff --git a/tests/lua/coe5.lua b/tests/lua/coe5.lua index f86fda9b2..e281c06f7 100644 --- a/tests/lua/coe5.lua +++ b/tests/lua/coe5.lua @@ -22,8 +22,8 @@ env = add_coercion(env, "ar2ag") for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end) for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) -print(get_coercion_to_sort(env, Const("abelian_ring", {1}))) -assert(env:type_check(get_coercion_to_sort(env, Const("abelian_ring", {1})))) +print(get_coercions_to_sort(env, Const("abelian_ring", {1})):head()) +assert(env:type_check(get_coercions_to_sort(env, Const("abelian_ring", {1})):head())) print("Coercions (abelian ring): ") cs = get_user_coercions(env, ab_ring) for i = 1, #cs do diff --git a/tests/lua/scope.lua b/tests/lua/scope.lua index 59acb6ac4..d49b37a0b 100644 --- a/tests/lua/scope.lua +++ b/tests/lua/scope.lua @@ -31,10 +31,10 @@ env = add_decl(env, mk_var_decl("nat2lst", mk_arrow(nat, lst_1(nat)))) env = add_coercion(env, "lst2vec") env = push_scope(env, "tst") local lst_nat = lst_1(nat) -print(get_coercion(env, lst_nat, "vec")) +print(get_coercions(env, lst_nat, "vec"):head()) env = add_coercion(env, "vec2mat") -print(get_coercion(env, lst_nat, "mat")) -assert(env:type_check(get_coercion(env, lst_nat, "mat"))) +print(get_coercions(env, lst_nat, "mat"):head()) +assert(env:type_check(get_coercions(env, lst_nat, "mat"):head())) function get_num_coercions(env) local r = 0 for_each_coercion_user(env, function(C, D, f) r = r + 1 end)