From b15f1bb8c78da79a5c6bc3d7b3df0acc5857ddc6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Jul 2014 13:55:39 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): apply coercions in definitions Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 76 +++++++++++++++---------------- tests/lean/run/coercion_bug.lean | 5 ++ 2 files changed, 43 insertions(+), 38 deletions(-) create mode 100644 tests/lean/run/coercion_bug.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index bec85754f..e8d4cfca5 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -736,16 +736,41 @@ public: return mk_choice_cnstr(m, choice_fn, delay_factor, j, m_relax_main_opaque); } - /** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type, - create a "delayed coercion". The idea is to create a choice constraint and postpone the coercion - search. We do that whenever d_type or a_type is a metavar application, and d_type or a_type is a coercion source/target. - */ - expr mk_delayed_coercion(expr const & e, expr const & d_type, expr const & a_type) { - expr a = app_arg(e); - expr m = mk_meta(some_expr(d_type), a.get_tag()); - justification j = mk_app_justification(e, a, d_type, a_type); + /** \brief Given a term a : a_type, and an expected type generate a metavariable with a delayed coercion. */ + expr mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type, justification const & j) { + expr m = mk_meta(some_expr(expected_type), a.get_tag()); add_cnstr(mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic))); - return update_app(e, app_fn(e), m); + return m; + } + + /** \brief Given a term a : a_type, ensure it has type \c expected_type. Apply coercions if needed + + \remark relax == true affects how opaque definitions in the main module are treated. + */ + expr ensure_type(expr const & a, expr const & a_type, expr const & expected_type, justification const & j, bool relax) { + if (is_meta(expected_type) && has_coercions_from(a_type)) { + return mk_delayed_coercion(a, a_type, expected_type, j); + } else if (is_meta(a_type) && has_coercions_to(expected_type)) { + return mk_delayed_coercion(a, a_type, expected_type, j); + } else if (m_tc[relax]->is_def_eq(a_type, expected_type, j)) { + return a; + } else { + expr new_a = apply_coercion(a, a_type, expected_type); + bool coercion_worked = false; + if (!is_eqp(a, new_a)) { + expr new_a_type = instantiate_metavars(infer_type(new_a)); + coercion_worked = m_tc[relax]->is_def_eq(new_a_type, expected_type, j); + } + if (coercion_worked) { + return new_a; + } else if (has_metavar(a_type) || has_metavar(expected_type)) { + // rely on unification hints to solve this constraint + add_cnstr(mk_eq_cnstr(a_type, expected_type, j, relax)); + return a; + } else { + throw unifier_exception(j, m_subst); + } + } } bool is_choice_app(expr const & e) { @@ -798,32 +823,9 @@ public: expr a_type = instantiate_metavars(infer_type(a)); expr r = mk_app(f, a, e.get_tag()); - if (is_meta(d_type) && has_coercions_from(a_type)) { - return mk_delayed_coercion(r, d_type, a_type); - } else if (is_meta(a_type) && has_coercions_to(d_type)) { - return mk_delayed_coercion(r, d_type, a_type); - } else { - app_delayed_justification j(r, a, f_type, a_type); - if (!m_tc[m_relax_main_opaque]->is_def_eq(a_type, d_type, j)) { - expr new_a = apply_coercion(a, a_type, d_type); - bool coercion_worked = false; - if (!is_eqp(a, new_a)) { - expr new_a_type = instantiate_metavars(infer_type(new_a)); - coercion_worked = m_tc[m_relax_main_opaque]->is_def_eq(new_a_type, d_type, j); - } - if (coercion_worked) { - r = update_app(r, f, new_a); - } else { - if (has_metavar(a_type) || has_metavar(d_type)) { - // rely on unification hints to solve this constraint - add_cnstr(mk_eq_cnstr(a_type, d_type, j.get(), m_relax_main_opaque)); - } else { - throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, a, d_type, a_type); }); - } - } - } - return r; - } + justification j = mk_app_justification(e, a, d_type, a_type); + expr new_a = ensure_type(a, a_type, d_type, j, m_relax_main_opaque); + return update_app(r, app_fn(r), new_a); } expr visit_placeholder(expr const & e) { @@ -1207,9 +1209,7 @@ public: substitution s(subst); return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type)); }); - if (!m_tc[is_opaque]->is_def_eq(r_v_type, r_t, j)) { - throw_kernel_exception(m_env, v, [=](formatter const & fmt) { return pp_def_type_mismatch(fmt, n, r_t, r_v_type); }); - } + r_v = ensure_type(r_v, r_v_type, r_t, j, is_opaque); auto p = solve().pull(); lean_assert(p); substitution s = p->first; diff --git a/tests/lean/run/coercion_bug.lean b/tests/lean/run/coercion_bug.lean new file mode 100644 index 000000000..4a59d2b21 --- /dev/null +++ b/tests/lean/run/coercion_bug.lean @@ -0,0 +1,5 @@ +import nat +using nat + +definition tst1 : Prop := zero = 0 +definition tst2 : nat := 0