From 76c3757db787f455614c6c9d7b780f0124e13d1c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2015 16:06:20 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type closes #547 --- src/frontends/lean/coercion_elaborator.cpp | 26 +++++----- src/frontends/lean/coercion_elaborator.h | 5 +- src/frontends/lean/elaborator.cpp | 60 +++++++++++++++++++--- src/frontends/lean/elaborator.h | 2 + tests/lean/run/finset_coe.lean | 10 ++++ tests/lean/run/rat_coe.lean | 17 ++++++ 6 files changed, 99 insertions(+), 21 deletions(-) create mode 100644 tests/lean/run/finset_coe.lean create mode 100644 tests/lean/run/rat_coe.lean diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp index bdb5ebb36..1c8ec63e0 100644 --- a/src/frontends/lean/coercion_elaborator.cpp +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -21,17 +21,19 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons lean_assert(use_id || length(m_coercions) == length(m_choices)); } -list get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs) { +list get_coercions_from_to(type_checker & /* from_tc */, type_checker & to_tc, + expr const & from_type, expr const & to_type, constraint_seq & cs) { constraint_seq new_cs; - expr whnf_to_type = tc.whnf(to_type, new_cs); + environment const & env = to_tc.env(); + expr whnf_to_type = to_tc.whnf(to_type, new_cs); expr const & fn = get_app_fn(whnf_to_type); list r; if (is_constant(fn)) { - r = get_coercions(tc.env(), from_type, const_name(fn)); + r = get_coercions(env, from_type, const_name(fn)); } else if (is_pi(whnf_to_type)) { - r = get_coercions_to_fun(tc.env(), from_type); + r = get_coercions_to_fun(env, from_type); } else if (is_sort(whnf_to_type)) { - r = get_coercions_to_sort(tc.env(), from_type); + r = get_coercions_to_sort(env, from_type); } if (r) cs += new_cs; @@ -56,11 +58,11 @@ optional coercion_elaborator::next() { /** \brief Given a term a : a_type, and a metavariable \c m, creates a constraint that considers coercions from a_type to the type assigned to \c m. */ -constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, +constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coercion_info_manager & infom, expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) { - auto choice_fn = [=, &tc, &infom](expr const & meta, expr const & d_type, substitution const & s, - name_generator const & /* ngen */) { + auto choice_fn = [=, &from_tc, &to_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; if (is_meta(a_type)) { @@ -73,7 +75,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, if (is_meta(new_a_type)) { if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) { // postpone... - return lazy_list(constraints(mk_coercion_cnstr(tc, infom, m, a, a_type, justification(), + return lazy_list(constraints(mk_coercion_cnstr(from_tc, to_tc, infom, m, a, a_type, justification(), delay_factor+1))); } else { // giveup... @@ -81,11 +83,11 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, } } constraint_seq cs; - new_a_type = tc.whnf(new_a_type, cs); + new_a_type = from_tc.whnf(new_a_type, cs); if (is_meta(d_type)) { // case-split buffer> alts; - get_coercions_from(tc.env(), new_a_type, alts); + get_coercions_from(from_tc.env(), new_a_type, alts); buffer choices; buffer coes; // first alternative: no coercion @@ -105,7 +107,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, to_list(choices.begin(), choices.end()), to_list(coes.begin(), coes.end()))); } else { - list coes = get_coercions_from_to(tc, new_a_type, d_type, cs); + list coes = get_coercions_from_to(from_tc, to_tc, new_a_type, d_type, cs); if (is_nil(coes)) { expr new_a = a; infom.erase_coercion_info(a); diff --git a/src/frontends/lean/coercion_elaborator.h b/src/frontends/lean/coercion_elaborator.h index 956a0a0ea..6003eb149 100644 --- a/src/frontends/lean/coercion_elaborator.h +++ b/src/frontends/lean/coercion_elaborator.h @@ -40,9 +40,10 @@ public: \see coercion_info_manager */ -constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, +constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coercion_info_manager & infom, expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor); -list get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs); +list get_coercions_from_to(type_checker & from_tc, type_checker & to_tc, + expr const & from_type, expr const & to_type, constraint_seq & cs); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0854bd92c..fe2934215 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -54,6 +54,42 @@ Author: Leonardo de Moura #include "frontends/lean/calc.h" namespace lean { +/** \brief Custom converter that does not unfold constants that contains coercions from it. + We use this converter for detecting whether we have coercions from a given type. */ +class coercion_from_converter : public unfold_semireducible_converter { + environment m_env; +public: + coercion_from_converter(environment const & env):unfold_semireducible_converter(env, true), m_env(env) {} + virtual bool is_opaque(declaration const & d) const { + if (has_coercions_from(m_env, d.get_name())) + return true; + return unfold_semireducible_converter::is_opaque(d); + } +}; + +/** \brief Custom converter that does not unfold constants that contains coercions to it. + We use this converter for detecting whether we have coercions to a given type. */ +class coercion_to_converter : public unfold_semireducible_converter { + environment m_env; +public: + coercion_to_converter(environment const & env):unfold_semireducible_converter(env, true), m_env(env) {} + virtual bool is_opaque(declaration const & d) const { + if (has_coercions_to(m_env, d.get_name())) + return true; + return unfold_semireducible_converter::is_opaque(d); + } +}; + +type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator const & ngen) { + return std::unique_ptr(new type_checker(env, ngen, + std::unique_ptr(new coercion_from_converter(env)))); +} + +type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator const & ngen) { + return std::unique_ptr(new type_checker(env, ngen, + std::unique_ptr(new coercion_to_converter(env)))); +} + /** \brief 'Choice' expressions (choice e_1 ... e_n) are mapped into a metavariable \c ?m and a choice constraints (?m in fn) where \c fn is a choice function. The choice function produces a stream of alternatives. In this case, it produces a stream of @@ -116,6 +152,8 @@ elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen, bo m_no_info = false; m_in_equation_lhs = false; m_tc = mk_type_checker(ctx.m_env, m_ngen.mk_child()); + m_coercion_from_tc = mk_coercion_from_type_checker(ctx.m_env, m_ngen.mk_child()); + m_coercion_to_tc = mk_coercion_to_type_checker(ctx.m_env, m_ngen.mk_child()); m_nice_mvar_names = nice_mvar_names; } @@ -383,6 +421,8 @@ static expr mk_coercion_app(expr const & coe, expr const & a) { */ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { expr f_type = infer_type(f, cs); + expr saved_f_type = f_type; + constraint_seq saved_cs = cs; if (!is_pi(f_type)) f_type = whnf(f_type, cs); if (is_pi(f_type)) { @@ -392,6 +432,8 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { f_type = m_tc->ensure_pi(f_type, f, cs); erase_coercion_info(f); } else { + cs = saved_cs; + f_type = m_coercion_from_tc->whnf(saved_f_type, cs); // try coercion to function-class list coes = get_coercions_to_fun(env(), f_type); if (is_nil(coes)) { @@ -438,7 +480,7 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { bool elaborator::has_coercions_from(expr const & a_type) { try { - expr a_cls = get_app_fn(whnf(a_type).first); + expr a_cls = get_app_fn(m_coercion_from_tc->whnf(a_type).first); return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls)); } catch (exception&) { return false; @@ -447,7 +489,7 @@ bool elaborator::has_coercions_from(expr const & a_type) { bool elaborator::has_coercions_to(expr d_type) { try { - d_type = whnf(d_type).first; + d_type = m_coercion_to_tc->whnf(d_type).first; expr const & fn = get_app_fn(d_type); if (is_constant(fn)) return ::lean::has_coercions_to(env(), const_name(fn)); @@ -463,10 +505,10 @@ bool elaborator::has_coercions_to(expr d_type) { } expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) { - a_type = whnf(a_type).first; - d_type = whnf(d_type).first; + a_type = m_coercion_from_tc->whnf(a_type).first; + d_type = m_coercion_to_tc->whnf(d_type).first; constraint_seq aux_cs; - list coes = get_coercions_from_to(*m_tc, a_type, d_type, aux_cs); + list coes = get_coercions_from_to(*m_coercion_from_tc, *m_coercion_to_tc, a_type, d_type, aux_cs); if (is_nil(coes)) { erase_coercion_info(a); return a; @@ -495,10 +537,10 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) { pair elaborator::mk_delayed_coercion( expr const & a, expr const & a_type, expr const & expected_type, justification const & j) { - type_checker & tc = *m_tc; expr m = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag()); register_meta(m); - constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic)); + constraint c = mk_coercion_cnstr(*m_coercion_from_tc, *m_coercion_to_tc, *this, m, a, a_type, j, + to_delay_factor(cnstr_group::Basic)); return to_ecs(m, c); } @@ -695,6 +737,8 @@ expr elaborator::ensure_type(expr const & e, constraint_seq & cs) { erase_coercion_info(e); if (is_sort(t)) return e; + expr saved_t = t; + constraint_seq saved_cs = cs; t = whnf(t, cs); if (is_sort(t)) return e; @@ -708,6 +752,8 @@ expr elaborator::ensure_type(expr const & e, constraint_seq & cs) { return e; } } + cs = saved_cs; + t = m_coercion_from_tc->whnf(saved_t, cs); 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); }); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 8d1ddaf93..c510ce9d4 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -33,6 +33,8 @@ class elaborator : public coercion_info_manager { elaborator_context & m_ctx; name_generator m_ngen; type_checker_ptr m_tc; + type_checker_ptr m_coercion_from_tc; + type_checker_ptr m_coercion_to_tc; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants // representing the context where ?m was created. local_context m_context; // current local context: a list of local constants diff --git a/tests/lean/run/finset_coe.lean b/tests/lean/run/finset_coe.lean new file mode 100644 index 000000000..7798bad38 --- /dev/null +++ b/tests/lean/run/finset_coe.lean @@ -0,0 +1,10 @@ +import data.finset data.set +open finset set + +definition to_set [coercion] {A : Type} (s : finset A) : set A := λ a, a ∈ s + +constant P {A : Type} (s : set A) : Prop + +variable s : finset nat + +check P s diff --git a/tests/lean/run/rat_coe.lean b/tests/lean/run/rat_coe.lean new file mode 100644 index 000000000..8f269965a --- /dev/null +++ b/tests/lean/run/rat_coe.lean @@ -0,0 +1,17 @@ +import data.rat +open rat + +attribute rat.of_int [coercion] + +check (0 : ℚ) +check (rat.of_int 0 : ℚ) + +constant f : ℚ → Prop +variable a : nat + +check f 0 +check f a + +set_option pp.coercions true + +check f a