From ea9c810fca829277b181e6f8ad3d81f3f140c1b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 30 May 2015 14:45:14 -0700 Subject: [PATCH] feat(frontends/lean/coercion_elaborator): implement "coercion lifting" closes #644 --- src/frontends/lean/coercion_elaborator.cpp | 49 ++++++++++++++++------ src/frontends/lean/elaborator.cpp | 4 ++ tests/lean/644.lean | 38 +++++++++++++++++ tests/lean/644.lean.expected.out | 4 ++ 4 files changed, 82 insertions(+), 13 deletions(-) create mode 100644 tests/lean/644.lean create mode 100644 tests/lean/644.lean.expected.out diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp index 5f6401ea4..a24aae69a 100644 --- a/src/frontends/lean/coercion_elaborator.cpp +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/metavar.h" #include "kernel/constraint.h" +#include "kernel/abstract.h" #include "library/coercion.h" #include "library/unifier.h" #include "library/choice_iterator.h" @@ -21,23 +22,45 @@ 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 & /* from_tc */, type_checker & to_tc, +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; 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(env, from_type, const_name(fn)); - } else if (is_pi(whnf_to_type)) { - r = get_coercions_to_fun(env, from_type); - } else if (is_sort(whnf_to_type)) { - r = get_coercions_to_sort(env, from_type); + expr whnf_from_type = from_tc.whnf(from_type, new_cs); + expr whnf_to_type = to_tc.whnf(to_type, new_cs); + if (is_arrow(whnf_from_type)) { + // Try to lift coercions. + // The idea is to convert a coercion from A to B, into a coercion from D->A to D->B + if (!is_arrow(whnf_to_type)) + return list(); // failed + if (!from_tc.is_def_eq(binding_domain(whnf_from_type), binding_domain(whnf_to_type), justification(), new_cs)) + return list(); // failed, the domains must be definitionally equal + list coe = get_coercions_from_to(from_tc, to_tc, binding_body(whnf_from_type), binding_body(whnf_to_type), new_cs); + if (coe) { + cs += new_cs; + // Remark: each coercion c in coe is a function from A to B + // We create a new list: (fun (f : D -> A) (x : D), c (f x)) + expr f = mk_local(from_tc.mk_fresh_name(), "f", whnf_from_type, binder_info()); + expr x = mk_local(from_tc.mk_fresh_name(), "x", binding_domain(whnf_from_type), binder_info()); + expr fx = mk_app(f, x); + return map(coe, [&](expr const & c) { return Fun(f, Fun(x, mk_app(c, fx))); }); + } else { + return list(); + } + } else { + expr const & fn = get_app_fn(whnf_to_type); + list r; + if (is_constant(fn)) { + r = get_coercions(env, whnf_from_type, const_name(fn)); + } else if (is_pi(whnf_to_type)) { + r = get_coercions_to_fun(env, whnf_from_type); + } else if (is_sort(whnf_to_type)) { + r = get_coercions_to_sort(env, whnf_from_type); + } + if (r) + cs += new_cs; + return r; } - if (r) - cs += new_cs; - return r; } optional coercion_elaborator::next() { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e41092f69..4333d9fdc 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -481,6 +481,10 @@ 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(m_coercion_from_tc->whnf(a_type).first); + while (is_pi(a_cls)) { + expr local = mk_local(binding_name(a_cls), binding_domain(a_cls), binding_info(a_cls)); + a_cls = get_app_fn(m_coercion_from_tc->whnf(instantiate(binding_body(a_cls), local)).first); + } return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls)); } catch (exception&) { return false; diff --git a/tests/lean/644.lean b/tests/lean/644.lean new file mode 100644 index 000000000..65ea69e3c --- /dev/null +++ b/tests/lean/644.lean @@ -0,0 +1,38 @@ +import data.list + +constant A : Type₁ +constant B : Type₁ +constant coe : A → B +attribute coe [coercion] +variable f : B → B +variable a : A +set_option pp.coercions true +check f a + +constant C : Type₁ +variable g : (C → B) → B +variable h : C → A +check g h + +definition tst (g : C → B) : Prop := g = h + +open bool list + +definition bool_to_Prop [coercion] [reducible] (b : bool) : Prop := b = tt + +definition bpred_dec [instance] {A : Type} (p : A → bool) : ∀ a, decidable (p a = tt) := +begin + intro a, + eapply (bool.rec_on (p a)), + right, contradiction, + left, reflexivity +end + +definition negb : bool → bool := bool.rec tt ff + +check filter negb [tt, ff, tt, ff] + +eval filter negb [tt, ff, tt, ff] + +example : filter negb [tt, ff, tt, ff] = [ff, ff] := +rfl diff --git a/tests/lean/644.lean.expected.out b/tests/lean/644.lean.expected.out new file mode 100644 index 000000000..0567b0bcb --- /dev/null +++ b/tests/lean/644.lean.expected.out @@ -0,0 +1,4 @@ +f (coe a) : B +g (λ (x : C), coe (h x)) : B +filter (λ (x : bool), bool_to_Prop (negb x)) [tt, ff, tt, ff] : list bool +[ff, ff]