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

feat(library/unifier): remove mk_macro_imitation, we instead expand the macro before solving flex-rigid constraints

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

43
src/library/unifier.cpp
View file

@ -1589,37 +1589,6 @@ struct unifier_fn {
margs.pop_back(); margs.pop_back();
} }
/**
\brief Given
m := a metavariable ?m
margs := [a_1 ... a_k]
rhs := M(b_1 ... b_n) where M is a macro with arguments b_1 ... b_n
Then create the constraints
(?m_1 a_1 ... a_k) =?= b_1
...
(?m_n a_1 ... a_k) =?= b_n
?m =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k))
*/
void mk_macro_imitation() {
lean_assert(is_metavar(m));
lean_assert(is_macro(rhs));
constraint_seq cs;
buffer<expr> locals;
flet<justification> let(j, j); // save j value
mk_local_context(locals, cs);
lean_assert(margs.size() == locals.size());
buffer<expr> sargs;
for (unsigned i = 0; i < macro_num_args(rhs); i++) {
expr rarg = macro_arg(rhs, i);
expr rarg_type = u.m_tc[relax]->infer(rarg, cs);
expr sarg = mk_imitiation_arg(rhs, rarg_type, locals, cs);
sargs.push_back(sarg);
}
expr v = Fun(locals, mk_macro(macro_def(rhs), sargs.size(), sargs.data()));
cs += mk_eq_cnstr(m, v, j, relax);
alts.push_back(cs.to_list());
}
public: public:
flex_rigid_core_fn(unifier_fn & _u, expr const & _lhs, expr const & _rhs, flex_rigid_core_fn(unifier_fn & _u, expr const & _lhs, expr const & _rhs,
justification const & _j, bool _relax, buffer<constraints> & _alts): justification const & _j, bool _relax, buffer<constraints> & _alts):
@ -1643,10 +1612,7 @@ struct unifier_fn {
mk_bindings_imitation(); mk_bindings_imitation();
break; break;
case expr_kind::Macro: case expr_kind::Macro:
if (!u.m_pattern) lean_unreachable(); // LCOV_EXCL_LINE
mk_simple_projections();
mk_macro_imitation();
break;
case expr_kind::App: case expr_kind::App:
mk_app_projections(); mk_app_projections();
mk_app_imitation(); mk_app_imitation();
@ -1720,6 +1686,13 @@ struct unifier_fn {
return false; return false;
} }
} }
} else if (is_macro(rhs)) {
if (auto new_rhs = expand_rhs(rhs, relax)) {
lean_assert(*new_rhs != rhs);
return is_def_eq(lhs, *new_rhs, j, relax);
} else {
return false;
}
} }
buffer<constraint> aux; buffer<constraint> aux;