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

refactor(library/unifier): cleanup mk_macro_imitation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-28 13:19:19 -07:00
parent b51fa2b547
commit e303651dee
1 changed files with 12 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/library/unifier.cpp
View file

@ -1505,8 +1505,7 @@ struct unifier_fn {
} }
} catch (exception&) {} } catch (exception&) {}
expr v = Fun(locals, mk_app(f, sargs)); expr v = Fun(locals, mk_app(f, sargs));
// std::cout << " >> app imitation, v: " << v << "\n"; cs += mk_eq_cnstr(m, v, j, relax);
cs = cs + mk_eq_cnstr(m, v, j, relax);
alts.push_back(cs.to_list()); alts.push_back(cs.to_list());
} }
@ -1584,7 +1583,7 @@ struct unifier_fn {
expr binding = is_pi(rhs) ? Pi(local, B) : Fun(local, B); expr binding = is_pi(rhs) ? Pi(local, B) : Fun(local, B);
locals.pop_back(); locals.pop_back();
expr v = Fun(locals, binding); expr v = Fun(locals, binding);
cs = cs + mk_eq_cnstr(m, v, j, relax); cs += mk_eq_cnstr(m, v, j, relax);
alts.push_back(cs.to_list()); alts.push_back(cs.to_list());
} catch (exception&) {} } catch (exception&) {}
margs.pop_back(); margs.pop_back();
@ -1602,26 +1601,22 @@ struct unifier_fn {
?m =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k)) ?m =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k))
*/ */
void mk_macro_imitation() { void mk_macro_imitation() {
// TODO(Leo): use same approach used in mk_app_imitation
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
lean_assert(is_macro(rhs)); lean_assert(is_macro(rhs));
constraint_seq cs; constraint_seq cs;
expr mtype = mlocal_type(m); buffer<expr> locals;
mtype = ensure_sufficient_args(mtype, cs); flet<justification> let(j, j); // save j value
// create an auxiliary metavariable for each macro argument mk_local_context(locals, cs);
lean_assert(margs.size() == locals.size());
buffer<expr> sargs; buffer<expr> sargs;
for (unsigned i = 0; i < macro_num_args(rhs); i++) { for (unsigned i = 0; i < macro_num_args(rhs); i++) {
expr maux = mk_aux_metavar_for(u.m_ngen, mtype); expr rarg = macro_arg(rhs, i);
cs = mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j, relax) + cs; expr rarg_type = u.m_tc[relax]->infer(rarg, cs);
sargs.push_back(mk_app_vars(maux, margs.size())); expr sarg = mk_imitiation_arg(rhs, rarg_type, locals, cs);
sargs.push_back(sarg);
} }
expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data()); expr v = Fun(locals, mk_macro(macro_def(rhs), sargs.size(), sargs.data()));
v = mk_lambda_for(mtype, v); cs += mk_eq_cnstr(m, v, j, relax);
// if (check_imitation(v, cs)) {
// cs.push_back(mk_eq_cnstr(m, v, j, relax));
// alts.push_back(to_list(cs.begin(), cs.end()));
// }
cs = cs + mk_eq_cnstr(m, v, j, relax);
alts.push_back(cs.to_list()); alts.push_back(cs.to_list());
} }