diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp index 7474ce96c..8101b049b 100644 --- a/src/frontends/lean/coercion_elaborator.cpp +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -24,12 +24,12 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons } list get_coercions_from_to(type_checker & from_tc, type_checker & to_tc, - expr const & from_type, expr const & to_type, constraint_seq & cs) { + expr const & from_type, expr const & to_type, constraint_seq & cs, bool lift_coe) { constraint_seq new_cs; environment const & env = to_tc.env(); expr whnf_from_type = from_tc.whnf(from_type, new_cs); expr whnf_to_type = to_tc.whnf(to_type, new_cs); - if (is_pi(whnf_from_type)) { + if (lift_coe && is_pi(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_pi(whnf_to_type)) @@ -39,7 +39,7 @@ list get_coercions_from_to(type_checker & from_tc, type_checker & to_tc, expr x = mk_local(from_tc.mk_fresh_name(), "x", binding_domain(whnf_from_type), binder_info()); expr A = instantiate(binding_body(whnf_from_type), x); expr B = instantiate(binding_body(whnf_to_type), x); - list coe = get_coercions_from_to(from_tc, to_tc, A, B, new_cs); + list coe = get_coercions_from_to(from_tc, to_tc, A, B, new_cs, lift_coe); if (coe) { cs += new_cs; // Remark: each coercion c in coe is a function from A to B @@ -94,7 +94,7 @@ bool is_pi_meta(expr const & e) { that considers coercions from a_type to the type assigned to \c m. */ 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) { + justification const & j, unsigned delay_factor, bool lift_coe) { auto choice_fn = [=, &from_tc, &to_tc, &infom](expr const & meta, expr const & d_type, substitution const & s, name_generator && /* ngen */) { expr new_a_type; @@ -110,7 +110,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) { // postpone... return lazy_list(constraints(mk_coercion_cnstr(from_tc, to_tc, infom, m, a, a_type, justification(), - delay_factor+1))); + delay_factor+1, lift_coe))); } else { // giveup... return lazy_list(constraints(mk_eq_cnstr(meta, a, justification()))); @@ -118,7 +118,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc } constraint_seq cs; new_a_type = from_tc.whnf(new_a_type, cs); - if (is_pi_meta(d_type)) { + if ((lift_coe && is_pi_meta(d_type)) || (!lift_coe && is_meta(d_type))) { // case-split buffer locals; expr it_from = new_a_type; @@ -159,7 +159,7 @@ constraint mk_coercion_cnstr(type_checker & from_tc, type_checker & to_tc, coerc to_list(choices.begin(), choices.end()), to_list(coes.begin(), coes.end()))); } else { - list coes = get_coercions_from_to(from_tc, to_tc, new_a_type, d_type, cs); + list coes = get_coercions_from_to(from_tc, to_tc, new_a_type, d_type, cs, lift_coe); 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 f96ab3a77..2e296d94b 100644 --- a/src/frontends/lean/coercion_elaborator.h +++ b/src/frontends/lean/coercion_elaborator.h @@ -45,8 +45,9 @@ bool is_pi_meta(expr const & e); */ 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); + justification const & j, unsigned delay_factor, bool lift_coe); list get_coercions_from_to(type_checker & from_tc, type_checker & to_tc, - expr const & from_type, expr const & to_type, constraint_seq & cs); + expr const & from_type, expr const & to_type, constraint_seq & cs, + bool lift_coe); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d55e0a086..8b63d0af9 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -481,10 +481,12 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { bool elaborator::has_coercions_from(expr const & a_type, bool & lifted_coe) { 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); - lifted_coe = true; + if (m_ctx.m_lift_coercions) { + 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); + lifted_coe = true; + } } return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls)); } catch (exception&) { @@ -513,7 +515,7 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) { 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_coercion_from_tc, *m_coercion_to_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, m_ctx.m_lift_coercions); if (is_nil(coes)) { erase_coercion_info(a); return a; @@ -545,7 +547,7 @@ pair elaborator::mk_delayed_coercion( expr m = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag()); register_meta(m); 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)); + to_delay_factor(cnstr_group::Basic), m_ctx.m_lift_coercions); return to_ecs(m, c); } diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp index a00c2acc7..f7e697c53 100644 --- a/src/frontends/lean/elaborator_context.cpp +++ b/src/frontends/lean/elaborator_context.cpp @@ -23,6 +23,11 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_ELABORATOR_FAIL_MISSING_FIELD false #endif +#ifndef LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS +#define LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS true +#endif + + namespace lean { // ========================================== // elaborator configuration options @@ -30,6 +35,7 @@ static name * g_elaborator_local_instances = nullptr; static name * g_elaborator_ignore_instances = nullptr; static name * g_elaborator_flycheck_goals = nullptr; static name * g_elaborator_fail_missing_field = nullptr; +static name * g_elaborator_lift_coercions = nullptr; name const & get_elaborator_ignore_instances_name() { return *g_elaborator_ignore_instances; @@ -51,6 +57,10 @@ bool get_elaborator_fail_missing_field(options const & opts) { return opts.get_bool(*g_elaborator_fail_missing_field, LEAN_DEFAULT_ELABORATOR_FAIL_MISSING_FIELD); } +bool get_elaborator_lift_coercions(options const & opts) { + return opts.get_bool(*g_elaborator_lift_coercions, LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS); +} + // ========================================== elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, @@ -60,6 +70,7 @@ elaborator_context::elaborator_context(environment const & env, io_state const & m_ignore_instances = get_elaborator_ignore_instances(ios.get_options()); m_flycheck_goals = get_elaborator_flycheck_goals(ios.get_options()); m_fail_missing_field = get_elaborator_fail_missing_field(ios.get_options()); + m_lift_coercions = get_elaborator_lift_coercions(ios.get_options()); } void initialize_elaborator_context() { @@ -67,21 +78,26 @@ void initialize_elaborator_context() { g_elaborator_ignore_instances = new name{"elaborator", "ignore_instances"}; g_elaborator_flycheck_goals = new name{"elaborator", "flycheck_goals"}; g_elaborator_fail_missing_field = new name{"elaborator", "fail_if_missing_field"}; + g_elaborator_lift_coercions = new name{"elaborator", "lift_coercions"}; register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, - "(lean elaborator) use local declarates as class instances"); + "(elaborator) use local declarates as class instances"); register_bool_option(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES, - "(lean elaborator) if true, then elaborator does not perform class-instance resolution"); + "(elaborator) if true, then elaborator does not perform class-instance resolution"); register_bool_option(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS, - "(lean elaborator) if true, then elaborator display current goals for flycheck before each " + "(elaborator) if true, then elaborator display current goals for flycheck before each " "tactic is executed in a `begin ... end` block"); register_bool_option(*g_elaborator_fail_missing_field, LEAN_DEFAULT_ELABORATOR_FAIL_MISSING_FIELD, - "(lean elaborator) if true, then elaborator generates an error for missing fields instead " + "(elaborator) if true, then elaborator generates an error for missing fields instead " "of adding placeholders"); + register_bool_option(*g_elaborator_lift_coercions, LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS, + "(elaborator) if true, the elaborator will automatically lift coercions from A to B " + "into coercions from (C -> A) to (C -> B)"); } void finalize_elaborator_context() { delete g_elaborator_local_instances; delete g_elaborator_ignore_instances; delete g_elaborator_flycheck_goals; delete g_elaborator_fail_missing_field; + delete g_elaborator_lift_coercions; } } diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h index ee2acaf5a..a4e10d9d5 100644 --- a/src/frontends/lean/elaborator_context.h +++ b/src/frontends/lean/elaborator_context.h @@ -25,6 +25,7 @@ class elaborator_context { bool m_ignore_instances; bool m_flycheck_goals; bool m_fail_missing_field; + bool m_lift_coercions; friend class elaborator; public: elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, diff --git a/tests/lean/lift_coe_off.lean b/tests/lean/lift_coe_off.lean new file mode 100644 index 000000000..279f3b6ce --- /dev/null +++ b/tests/lean/lift_coe_off.lean @@ -0,0 +1,15 @@ +open nat + +inductive tree (A : Type) := +leaf : A → tree A, +node : tree A → tree A → tree A + +set_option elaborator.lift_coercions false + +definition size {A : Type} (t : tree A) := +tree.rec (λ a, 1) (λ t₁ t₂ n₁ n₂, n₁ + n₂) t + +set_option elaborator.lift_coercions true + +definition size {A : Type} (t : tree A) := +tree.rec (λ a, 1) (λ t₁ t₂ n₁ n₂, n₁ + n₂) t diff --git a/tests/lean/lift_coe_off.lean.expected.out b/tests/lean/lift_coe_off.lean.expected.out new file mode 100644 index 000000000..4817487fb --- /dev/null +++ b/tests/lean/lift_coe_off.lean.expected.out @@ -0,0 +1,10 @@ +lift_coe_off.lean:10:0: error: type mismatch at application + tree.rec (λ (a : A), 1) (λ (t₁ t₂ : tree A) (n₁ : ?M_1) (n₂ : ?M_2), ?M_3 + ?M_4) +term + λ (t₁ t₂ : tree A) (n₁ : ?M_1) (n₂ : ?M_2), + ?M_3 + ?M_4 +has type + Π (t₁ t₂ : tree A) (n₁ : ?M_1), + ?M_2 → ℕ +but is expected to have type + tree A → tree A → num → num → num