michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add option for disabling "coercion lifting"

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-30 17:07:42 -07:00
parent 6f6848968d
commit e5a82ef516
7 changed files with 64 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/coercion_elaborator.cpp
View file

@ -24,12 +24,12 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons
}
list<expr> 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<expr> 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<expr> coe = get_coercions_from_to(from_tc, to_tc, A, B, new_cs);
list<expr> 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>(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>(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<expr> 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<expr> coes = get_coercions_from_to(from_tc, to_tc, new_a_type, d_type, cs);
list<expr> 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);

5
src/frontends/lean/coercion_elaborator.h
View file

@ -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<expr> 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);
}

14
src/frontends/lean/elaborator.cpp
View file

@ -481,10 +481,12 @@ pair<expr, expr> 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<expr> coes = get_coercions_from_to(*m_coercion_from_tc, *m_coercion_to_tc, a_type, d_type, aux_cs);
list<expr> 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<expr, constraint_seq> 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);
}

24
src/frontends/lean/elaborator_context.cpp
View file

@ -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<level> 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;
}
}

1
src/frontends/lean/elaborator_context.h
View file

@ -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<level> const & lls,

15
tests/lean/lift_coe_off.lean Normal file
View file

@ -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

10
tests/lean/lift_coe_off.lean.expected.out Normal file
View file

@ -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