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

fix(library/coercion): bug in de-Bruijn indices

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-25 07:01:49 -07:00
parent f050308df7
commit a408883c92
1 changed files with 9 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/library/coercion.cpp
View file

@ -147,11 +147,9 @@ static void add_coercion_trans(coercion_ext & ext, io_state const & ios, name co
level_param_names const & g_level_params, expr g, expr const & g_type, unsigned g_num_args) { level_param_names const & g_level_params, expr g, expr const & g_type, unsigned g_num_args) {
expr t = f_type; expr t = f_type;
buffer<expr> args; buffer<expr> args;
unsigned i = f_num_args; for (unsigned i = 0; i <= f_num_args; i++)
while (i > 0) {
i--;
args.push_back(mk_var(i)); args.push_back(mk_var(i));
} expr f_app = apply_beta(f, args.size(), args.data());
buffer<name> f_arg_names; buffer<name> f_arg_names;
buffer<expr> f_arg_types; buffer<expr> f_arg_types;
while (is_pi(t)) { while (is_pi(t)) {
@ -159,24 +157,23 @@ static void add_coercion_trans(coercion_ext & ext, io_state const & ios, name co
f_arg_types.push_back(binding_domain(t)); f_arg_types.push_back(binding_domain(t));
t = binding_body(t); t = binding_body(t);
} }
expr f_app = apply_beta(f, args.size(), args.data());
expr D_app = t; expr D_app = t;
buffer<expr> g_args; buffer<expr> gf_args;
expr D_cnst = get_app_args(D_app, g_args); gf_args.push_back(f_app);
if (g_args.size() != g_num_args) expr D_cnst = get_app_rev_args(D_app, gf_args);
if (gf_args.size() != g_num_args + 1)
return; return;
g_args.push_back(f_app);
if (length(const_levels(D_cnst)) != length(g_level_params)) if (length(const_levels(D_cnst)) != length(g_level_params))
return; return;
// C >-> D >-> E // C >-> D >-> E
g = instantiate_params(g, g_level_params, const_levels(D_cnst)); g = instantiate_params(g, g_level_params, const_levels(D_cnst));
expr gf = apply_beta(g, g_args.size(), g_args.data()); expr gf = apply_beta(g, gf_args.size(), gf_args.data());
expr gf_type = g_type; expr gf_type = g_type;
while (is_pi(gf_type)) while (is_pi(gf_type))
gf_type = binding_body(gf_type); gf_type = binding_body(gf_type);
coercion_class new_cls = *type_to_coercion_class(gf_type); coercion_class new_cls = *type_to_coercion_class(gf_type);
gf_type = instantiate(instantiate_params(gf_type, g_level_params, const_levels(D_cnst)), g_args.size(), g_args.data()); gf_type = instantiate(instantiate_params(gf_type, g_level_params, const_levels(D_cnst)), gf_args.size(), gf_args.data());
i = f_arg_types.size(); unsigned i = f_arg_types.size();
while (i > 0) { while (i > 0) {
--i; --i;
gf = mk_lambda(f_arg_names[i], f_arg_types[i], gf); gf = mk_lambda(f_arg_names[i], f_arg_types[i], gf);