From f728f8096020be27882baef55c331f5e1159a566 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2013 19:41:24 -0800 Subject: [PATCH] fix(library/elaborator): remove is_neutral_abstraction hack, and bug at process_metavar_lift_abstraction Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 44 ++++++--------------------- 1 file changed, 10 insertions(+), 34 deletions(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index ccc75f525..c75d49c1f 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -835,17 +835,6 @@ class elaborator::imp { return is_metavar(a) && has_local_context(a) && head(metavar_lctx(a)).is_lift(); } - /** - \brief A neutral abstraction is an Arrow (if the abstraction is a Pi) or a constant function (if the abstraction is a lambda). - */ - bool is_neutral_abstraction(expr const & a, metavar_env const & menv) { - return is_abstraction(a) && !has_free_var(abst_body(a), 0, menv); - } - bool is_neutral_abstraction(expr const & a) { - return is_neutral_abstraction(a, m_state.m_menv); - } - - /** \brief Process a constraint ctx |- a == b where \c a is of the form ?m[(inst:i t), ...]. We perform a "case split", @@ -854,9 +843,6 @@ class elaborator::imp { */ bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { if (is_metavar_inst(a) && !is_metavar_inst(b) && !is_meta_app(b)) { - // Remark: the condition !is_abstraction(b) || is_neutral_abstraction(b) - // is used to make sure we don't enter a loop. - // This is just a conservative step to make sure the elaborator does diverge. context const & ctx = get_context(c); local_context lctx = metavar_lctx(a); unsigned i = head(lctx).s(); @@ -914,22 +900,12 @@ class elaborator::imp { // Lambdas and Pis // Imitation for Lambdas and Pis, b == Fun(x:T) B // mname <- Fun (x:?h_1) ?h_2 - // Remark: we don't need to use (Fun (x:?h_1) (?h_2 x)) because when b - // is a neutral abstraction (arrow or constant function). - // We avoid the more general (Fun (x:?h_1) (?h_2 x)) because it produces - // non-termination. expr h_1 = new_state.m_menv.mk_metavar(ctx); push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(abst_domain(b), i, 1), new_assumption); context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); expr h_2 = new_state.m_menv.mk_metavar(new_ctx); - if (is_neutral_abstraction(b, new_state.m_menv)) { - imitation = update_abstraction(b, h_1, h_2); - push_new_eq_constraint(new_state.m_queue, new_ctx, h_2, lift_free_vars(abst_body(b), i+1, 1), new_assumption); - } else { - expr h2_x = mk_app(h_2, Var(0)); - imitation = update_abstraction(b, h_1, h2_x); - push_new_eq_constraint(new_state.m_queue, new_ctx, h2_x, lift_free_vars(abst_body(b), i+1, 1), new_assumption); - } + imitation = update_abstraction(b, h_1, h_2); + push_new_eq_constraint(new_state.m_queue, new_ctx, h_2, lift_free_vars(abst_body(b), i+1, 1), new_assumption); } else { imitation = lift_free_vars(b, i, 1); } @@ -952,18 +928,18 @@ class elaborator::imp { We just add a new assignment that forces ?m to have the corresponding kind. */ bool process_metavar_lift_abstraction(expr const & a, expr const & b, unification_constraint const & c) { - if (is_metavar_lift(a) && is_abstraction(b) && is_neutral_abstraction(b)) { + if (is_metavar_lift(a) && is_abstraction(b)) { push_back(c); - context const & ctx = get_context(c); - expr h_1 = m_state.m_menv.mk_metavar(ctx); - expr h_2 = m_state.m_menv.mk_metavar(ctx); - // We don't use h_2(Var 0) in the body of the imitation term because - // b is a neutral abstraction (arrow or constant function). - // See comment at process_metavar_inst + // a <- (fun x : ?h1, ?h2) or (Pi x : ?h1, ?h2) + // ?h1 is in the same context where 'a' was defined + // ?h2 is in the context of 'a' + domain of b + context ctx_a = m_state.m_menv.get_context(metavar_name(a)); + expr h_1 = m_state.m_menv.mk_metavar(ctx_a); + expr h_2 = m_state.m_menv.mk_metavar(extend(ctx_a, abst_name(b), abst_domain(b))); expr imitation = update_abstraction(b, h_1, h_2); expr ma = mk_metavar(metavar_name(a)); justification new_jst(new imitation_justification(c)); - push_new_constraint(true, ctx, ma, imitation, new_jst); + push_new_constraint(true, ctx_a, ma, imitation, new_jst); return true; } else { return false;