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

fix(elaborator): fix bug in higher-order matching/unification

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-24 17:53:37 -07:00
parent d1a2a4ea7e
commit e3efe39eeb
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/frontend_elaborator.cpp
View file

@ -332,6 +332,10 @@ public:
// std::cout << "After preprocessing\n" << new_e << "\n"; // std::cout << "After preprocessing\n" << new_e << "\n";
if (has_metavar(new_e)) { if (has_metavar(new_e)) {
m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs); m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs);
// for (auto c : m_ucs) {
// formatter fmt = mk_simple_formatter();
// std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
// }
substitution s = elaborate_core(); substitution s = elaborate_core();
return instantiate_metavars(new_e, s); return instantiate_metavars(new_e, s);
} else { } else {

5
src/library/elaborator/elaborator.cpp
View file

@ -732,6 +732,7 @@ class elaborator::imp {
state new_state(m_state); state new_state(m_state);
justification new_assumption = mk_assumption(); justification new_assumption = mk_assumption();
expr imitation; expr imitation;
lean_assert(arg_types.size() == num_a - 1);
if (is_app(b)) { if (is_app(b)) {
// Imitation for applications // Imitation for applications
expr f_b = arg(b, 0); expr f_b = arg(b, 0);
@ -739,7 +740,7 @@ class elaborator::imp {
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), f_b (h_1 x_1 ... x_{num_a-1}) ... (h_{num_b-1} x_1 ... x_{num_a-1}) // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), f_b (h_1 x_1 ... x_{num_a-1}) ... (h_{num_b-1} x_1 ... x_{num_a-1})
// New constraints (h_i a_1 ... a_{num_a-1}) == arg(b, i) // New constraints (h_i a_1 ... a_{num_a-1}) == arg(b, i)
buffer<expr> imitation_args; // arguments for the imitation buffer<expr> imitation_args; // arguments for the imitation
imitation_args.push_back(f_b); imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1));
for (unsigned i = 1; i < num_b; i++) { for (unsigned i = 1; i < num_b; i++) {
expr h_i = new_state.m_menv.mk_metavar(ctx); expr h_i = new_state.m_menv.mk_metavar(ctx);
imitation_args.push_back(mk_app_vars(h_i, num_a - 1)); imitation_args.push_back(mk_app_vars(h_i, num_a - 1));
@ -767,7 +768,7 @@ class elaborator::imp {
expr h_2 = new_state.m_menv.mk_metavar(new_ctx); expr h_2 = new_state.m_menv.mk_metavar(new_ctx);
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption);
push_new_eq_constraint(new_state.m_queue, new_ctx, push_new_eq_constraint(new_state.m_queue, new_ctx,
mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b), new_assumption); mk_app(update_app(a, 0, h_2), mk_var(0)), abst_body(b), new_assumption);
imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a))); imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a)));
} else { } else {
// "Dumb imitation" aka the constant function // "Dumb imitation" aka the constant function