From 8f67348c055bc5635e11eafcfaa50c80c146e4ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2013 18:06:10 -0800 Subject: [PATCH] fix(library/elaborator): remove nasty hack, this hack was throwing away the local context at process_meta_app_core Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 31 ++++++++++++++------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index e1d9687c1..ccc75f525 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -176,12 +176,6 @@ class elaborator::imp { return *(m_state.m_menv.get_subst_jst(m)); } - /** \brief Return the type of an metavariable */ - expr get_mvar_type(expr const & m) { - lean_assert(is_metavar(m)); - return m_state.m_menv.get_type(m); - } - /** \brief Return true iff \c e contains the metavariable \c m. The substitutions in the current state are taken into account. @@ -872,7 +866,7 @@ class elaborator::imp { buffer ucs; expr b_type = m_type_inferer(b, ctx, &menv, &ucs); for (auto uc : ucs) - m_state.m_queue.push_front(uc); + push_front(uc); context ctx_with_i = ctx.insert_at(i, g_x_name, b_type); // must add entry for variable #i in the context std::unique_ptr new_cs(new generic_case_split(c, m_state)); @@ -902,9 +896,10 @@ class elaborator::imp { unsigned num_b = num_args(b); buffer imitation_args; imitation_args.push_back(f_b); - for (unsigned i = 1; i < num_b; i++) { - expr h_i = new_state.m_menv.mk_metavar(ctx); - imitation_args.push_back(h_i); + for (unsigned j = 1; j < num_b; j++) { + expr h_j = new_state.m_menv.mk_metavar(ctx); + imitation_args.push_back(h_j); + push_new_eq_constraint(new_state.m_queue, ctx, h_j, lift_free_vars(arg(b, j), i, 1), new_assumption); } imitation = mk_app(imitation_args); } else if (is_eq(b)) { @@ -913,6 +908,8 @@ class elaborator::imp { expr h_1 = new_state.m_menv.mk_metavar(ctx); expr h_2 = new_state.m_menv.mk_metavar(ctx); imitation = mk_eq(h_1, h_2); + push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(eq_lhs(b), i, 1), new_assumption); + push_new_eq_constraint(new_state.m_queue, ctx, h_2, lift_free_vars(eq_rhs(b), i, 1), new_assumption); } else if (is_abstraction(b)) { // Lambdas and Pis // Imitation for Lambdas and Pis, b == Fun(x:T) B @@ -922,17 +919,21 @@ class elaborator::imp { // 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)) + if (is_neutral_abstraction(b, new_state.m_menv)) { imitation = update_abstraction(b, h_1, h_2); - else - imitation = update_abstraction(b, h_1, mk_app(h_2, Var(0))); + 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); + } } else { imitation = lift_free_vars(b, i, 1); } - new_state.m_queue.push_front(c); // keep c - push_new_eq_constraint(new_state.m_queue, ctx_with_i, mk_metavar(metavar_name(a)), imitation, new_assumption); + push_new_eq_constraint(new_state.m_queue, ctx_with_i, pop_meta_context(a), imitation, new_assumption); new_cs->push_back(new_state, new_assumption); } bool r = new_cs->next(*this);