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
The modifications started at commit 1852c86948
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 <leonardo@microsoft.com>
This commit is contained in:
parent
70b7e519f8
commit
160a8379ef
2 changed files with 16 additions and 12 deletions
|
@ -145,6 +145,10 @@ class frontend_elaborator::imp {
|
||||||
imp & m_ref;
|
imp & m_ref;
|
||||||
preprocessor(imp & r):m_ref(r) {}
|
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) {
|
virtual expr visit_constant(expr const & e, context const & ctx) {
|
||||||
if (is_placeholder(e)) {
|
if (is_placeholder(e)) {
|
||||||
expr m = m_ref.m_menv->mk_metavar(ctx, visit(const_type(e), ctx));
|
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++;
|
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) {
|
if (i == num_args) {
|
||||||
|
@ -372,7 +376,7 @@ class frontend_elaborator::imp {
|
||||||
}
|
}
|
||||||
new_args.push_back(new_a);
|
new_args.push_back(new_a);
|
||||||
if (f_t)
|
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);
|
return mk_app(new_args);
|
||||||
}
|
}
|
||||||
|
|
|
@ -454,7 +454,7 @@ class elaborator::imp {
|
||||||
// in the assign(a, b, c) branch above.
|
// in the assign(a, b, c) branch above.
|
||||||
justification new_jst(new normalize_justification(c));
|
justification new_jst(new normalize_justification(c));
|
||||||
expr new_a = pop_meta_context(a);
|
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
|
context new_ctx = ctx.insert_at(me.s(), g_x_name, Type()); // insert a dummy at position s
|
||||||
if (!is_lhs)
|
if (!is_lhs)
|
||||||
swap(new_a, new_b);
|
swap(new_a, new_b);
|
||||||
|
@ -522,7 +522,7 @@ class elaborator::imp {
|
||||||
/** \brief Unfold let-expression */
|
/** \brief Unfold let-expression */
|
||||||
void process_let(expr & a) {
|
void process_let(expr & a) {
|
||||||
if (is_let(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. */
|
/** \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})
|
// 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)
|
// New constraints (h_i a_1 ... a_{num_a}) == arg(b, i)
|
||||||
buffer<expr> imitation_args; // arguments for the imitation
|
buffer<expr> 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++) {
|
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
|
// 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);
|
expr h_i = new_state.m_menv->mk_metavar(h_ctx);
|
||||||
|
@ -822,7 +822,7 @@ class elaborator::imp {
|
||||||
} else {
|
} else {
|
||||||
// "Dumb imitation" aka the constant function
|
// "Dumb imitation" aka the constant function
|
||||||
// Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), b
|
// 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);
|
push_new_eq_constraint(new_state.m_queue, ctx, f_a, imitation, new_assumption);
|
||||||
new_cs->push_back(new_state, 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++) {
|
for (unsigned j = 1; j < num_b; j++) {
|
||||||
expr h_j = new_state.m_menv->mk_metavar(ctx);
|
expr h_j = new_state.m_menv->mk_metavar(ctx);
|
||||||
imitation_args.push_back(h_j);
|
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);
|
imitation = mk_app(imitation_args);
|
||||||
} else if (is_eq(b)) {
|
} else if (is_eq(b)) {
|
||||||
|
@ -921,20 +921,20 @@ class elaborator::imp {
|
||||||
expr h_1 = new_state.m_menv->mk_metavar(ctx);
|
expr h_1 = new_state.m_menv->mk_metavar(ctx);
|
||||||
expr h_2 = new_state.m_menv->mk_metavar(ctx);
|
expr h_2 = new_state.m_menv->mk_metavar(ctx);
|
||||||
imitation = mk_eq(h_1, h_2);
|
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_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_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)) {
|
} else if (is_abstraction(b)) {
|
||||||
// Lambdas and Pis
|
// Lambdas and Pis
|
||||||
// Imitation for Lambdas and Pis, b == Fun(x:T) B
|
// Imitation for Lambdas and Pis, b == Fun(x:T) B
|
||||||
// mname <- Fun (x:?h_1) ?h_2
|
// mname <- Fun (x:?h_1) ?h_2
|
||||||
expr h_1 = new_state.m_menv->mk_metavar(ctx);
|
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));
|
context new_ctx = extend(ctx, abst_name(b), abst_domain(b));
|
||||||
expr h_2 = new_state.m_menv->mk_metavar(new_ctx);
|
expr h_2 = new_state.m_menv->mk_metavar(new_ctx);
|
||||||
imitation = update_abstraction(b, h_1, h_2);
|
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 {
|
} 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);
|
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);
|
new_cs->push_back(new_state, new_assumption);
|
||||||
|
|
Loading…
Reference in a new issue