From 160a8379ef7907332bf6a8b1d45e5eac78c8d6db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Dec 2013 15:55:12 -0800 Subject: [PATCH] feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The modifications started at commit 1852c86948dd7da8a2bac224e3c7c0ee309db224 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as: [x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈ ?M::22 x a After the changes, only very simple constraints are generated. The most complicated one is: [] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18 Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 8 ++++++-- src/library/elaborator/elaborator.cpp | 20 ++++++++++---------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 2f57f7aa9..4bf2d2b6e 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -145,6 +145,10 @@ class frontend_elaborator::imp { imp & m_ref; preprocessor(imp & r):m_ref(r) {} + expr instantiate(expr const & e, expr const & v) { + return ::lean::instantiate(e, v, m_ref.m_menv); + } + virtual expr visit_constant(expr const & e, context const & ctx) { if (is_placeholder(e)) { expr m = m_ref.m_menv->mk_metavar(ctx, visit(const_type(e), ctx)); @@ -249,7 +253,7 @@ class frontend_elaborator::imp { num_skipped_args++; } } - f_t = some_expr(::lean::instantiate(abst_body(*f_t), args[i])); + f_t = some_expr(instantiate(abst_body(*f_t), args[i])); } } if (i == num_args) { @@ -372,7 +376,7 @@ class frontend_elaborator::imp { } new_args.push_back(new_a); if (f_t) - f_t = some_expr(::lean::instantiate(abst_body(*f_t), new_a)); + f_t = some_expr(instantiate(abst_body(*f_t), new_a)); } return mk_app(new_args); } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 42870b3ee..d92a03db6 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -454,7 +454,7 @@ class elaborator::imp { // in the assign(a, b, c) branch above. justification new_jst(new normalize_justification(c)); expr new_a = pop_meta_context(a); - expr new_b = lift_free_vars(b, me.s(), 1); + expr new_b = lift_free_vars(b, me.s(), 1, m_state.m_menv); context new_ctx = ctx.insert_at(me.s(), g_x_name, Type()); // insert a dummy at position s if (!is_lhs) swap(new_a, new_b); @@ -522,7 +522,7 @@ class elaborator::imp { /** \brief Unfold let-expression */ void process_let(expr & a) { if (is_let(a)) - a = instantiate(let_body(a), let_value(a)); + a = instantiate(let_body(a), let_value(a), m_state.m_menv); } /** \brief Replace variables by their definition if the context contains it. */ @@ -788,7 +788,7 @@ class elaborator::imp { // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), f_b (h_1 x_1 ... x_{num_a}) ... (h_{num_b} x_1 ... x_{num_a}) // New constraints (h_i a_1 ... a_{num_a}) == arg(b, i) buffer imitation_args; // arguments for the imitation - imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1)); + imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1, new_state.m_menv)); for (unsigned i = 1; i < num_b; i++) { // Remark: h_ctx is "ctx, (x_{num_a} : T_{num_a}) ... (x_1 : T_1)" because h_i is inside of the lambda expr h_i = new_state.m_menv->mk_metavar(h_ctx); @@ -822,7 +822,7 @@ class elaborator::imp { } else { // "Dumb imitation" aka the constant function // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), b - imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1)); + imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1, new_state.m_menv)); } push_new_eq_constraint(new_state.m_queue, ctx, f_a, imitation, new_assumption); new_cs->push_back(new_state, new_assumption); @@ -912,7 +912,7 @@ class elaborator::imp { 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); + push_new_eq_constraint(new_state.m_queue, ctx, h_j, lift_free_vars(arg(b, j), i, 1, new_state.m_menv), new_assumption); } imitation = mk_app(imitation_args); } else if (is_eq(b)) { @@ -921,20 +921,20 @@ 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); + push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(eq_lhs(b), i, 1, new_state.m_menv), new_assumption); + push_new_eq_constraint(new_state.m_queue, ctx, h_2, lift_free_vars(eq_rhs(b), i, 1, new_state.m_menv), new_assumption); } else if (is_abstraction(b)) { // Lambdas and Pis // Imitation for Lambdas and Pis, b == Fun(x:T) B // mname <- Fun (x:?h_1) ?h_2 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); + push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(abst_domain(b), i, 1, new_state.m_menv), new_assumption); context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); expr h_2 = new_state.m_menv->mk_metavar(new_ctx); 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); + push_new_eq_constraint(new_state.m_queue, new_ctx, h_2, lift_free_vars(abst_body(b), i+1, 1, new_state.m_menv), new_assumption); } else { - imitation = lift_free_vars(b, i, 1); + imitation = lift_free_vars(b, i, 1, new_state.m_menv); } 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);