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

refactor(library/unifier): remove redundant code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-09 15:04:34 -07:00
parent 4bcde576b8
commit ee9be2837b
1 changed files with 2 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/library/unifier.cpp
View file

@ -117,19 +117,6 @@ occurs_check_status occurs_context_check(substitution & s, expr const & e, expr
return occurs_context_check(s, e, m, locals, bad_local); return occurs_context_check(s, e, m, locals, bad_local);
} }
// Create a lambda abstraction by abstracting the local constants \c locals in \c e
expr lambda_abstract_locals(expr const & e, buffer<expr> const & locals) {
expr v = abstract_locals(e, locals.size(), locals.data());
unsigned i = locals.size();
while (i > 0) {
--i;
expr t = abstract_locals(mlocal_type(locals[i]), i, locals.data());
v = mk_lambda(local_pp_name(locals[i]), t, v);
}
return v;
}
unify_status unify_simple_core(substitution & s, expr const & lhs, expr const & rhs, justification const & j) { unify_status unify_simple_core(substitution & s, expr const & lhs, expr const & rhs, justification const & j) {
lean_assert(is_meta(lhs)); lean_assert(is_meta(lhs));
buffer<expr> args; buffer<expr> args;
@ -144,7 +131,7 @@ unify_status unify_simple_core(substitution & s, expr const & lhs, expr const &
case occurs_check_status::Maybe: case occurs_check_status::Maybe:
return unify_status::Unsupported; return unify_status::Unsupported;
case occurs_check_status::Ok: { case occurs_check_status::Ok: {
expr v = lambda_abstract_locals(rhs, args); expr v = Fun(args, rhs);
s.assign(mlocal_name(*m), v, j); s.assign(mlocal_name(*m), v, j);
return unify_status::Solved; return unify_status::Solved;
}} }}
@ -627,7 +614,7 @@ struct unifier_fn {
return Continue; return Continue;
case occurs_check_status::Ok: case occurs_check_status::Ok:
lean_assert(!m_subst.is_assigned(*m)); lean_assert(!m_subst.is_assigned(*m));
if (assign(*m, lambda_abstract_locals(rhs, locals), j, relax, lhs, rhs)) { if (assign(*m, Fun(locals, rhs), j, relax, lhs, rhs)) {
return Solved; return Solved;
} else { } else {
return Failed; return Failed;