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

feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type

Browse source 
closes #547
This commit is contained in:
Leonardo de Moura 2015-05-20 16:06:20 -07:00
parent 608984cd4c
commit 76c3757db7
6 changed files with 99 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<expr> get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs) {
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) {
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<expr> 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<constraints> coercion_elaborator::next() {
/** \brief Given a term <tt>a : a_type</tt>, 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>(constraints(mk_coercion_cnstr(tc, infom, m, a, a_type, justification(),
return lazy_list<constraints>(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<std::tuple<coercion_class, expr, expr>> alts;
get_coercions_from(tc.env(), new_a_type, alts);
get_coercions_from(from_tc.env(), new_a_type, alts);
buffer<constraints> choices;
buffer<expr> 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<expr> coes = get_coercions_from_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);
if (is_nil(coes)) {
expr new_a = a;
infom.erase_coercion_info(a);

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

@ -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<expr> get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs);
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);
}

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

@ -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<type_checker>(new type_checker(env, ngen,
std::unique_ptr<converter>(new coercion_from_converter(env))));
}
type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator const & ngen) {
return std::unique_ptr<type_checker>(new type_checker(env, ngen,
std::unique_ptr<converter>(new coercion_to_converter(env))));
}
/** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
and a choice constraints <tt>(?m in fn)</tt> 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<expr, expr> 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<expr, expr> 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<expr> coes = get_coercions_to_fun(env(), f_type);
if (is_nil(coes)) {
@ -438,7 +480,7 @@ pair<expr, expr> 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<expr> coes = get_coercions_from_to(*m_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);
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<expr, constraint_seq> 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<expr> 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); });

2
src/frontends/lean/elaborator.h
View file

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

10
tests/lean/run/finset_coe.lean Normal file
View file

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

17
tests/lean/run/rat_coe.lean Normal file
View file

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