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

feat(kernel/expr): change the rules for inferring implicit arguments, closes #344

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-25 12:54:07 -08:00
parent 24a15b6c46
commit ef75cac1c0
3 changed files with 22 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/kernel/expr.cpp
View file

@ -596,9 +596,13 @@ optional<expr> has_expr_metavar_strict(expr const & e) {
return r;
}
static bool has_free_var_in_domain(expr const & b, unsigned vidx) {
static bool has_free_var_in_domain(expr const & b, unsigned vidx, bool strict) {
if (is_pi(b)) {
return has_free_var(binding_domain(b), vidx) || has_free_var_in_domain(binding_body(b), vidx+1);
return
(has_free_var(binding_domain(b), vidx) && is_explicit(binding_info(b))) ||
has_free_var_in_domain(binding_body(b), vidx+1, strict);
} else if (!strict) {
return has_free_var(b, vidx);
} else {
return false;
}
@ -612,8 +616,7 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict) {
if (binding_info(t).is_implicit() || binding_info(t).is_strict_implicit()) {
// argument is already marked as implicit
return update_binding(t, binding_domain(t), new_body);
} else if ((strict && has_free_var_in_domain(new_body, 0)) ||
(!strict && has_free_var(new_body, 0))) {
} else if (has_free_var_in_domain(new_body, 0, strict)) {
return update_binding(t, binding_domain(t), new_body, mk_implicit_binder_info());
} else {
return update_binding(t, binding_domain(t), new_body);

4
src/library/definitional/projection.cpp
View file

@ -68,7 +68,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
for (unsigned i = 0; i < nparams; i++) {
if (!is_pi(intro_type))
throw_ill_formed(n);
expr param = mk_local(ngen.next(), binding_name(intro_type), binding_domain(intro_type), mk_implicit_binder_info());
expr param = mk_local(ngen.next(), binding_name(intro_type), binding_domain(intro_type), binder_info());
intro_type = instantiate(binding_body(intro_type), param);
params.push_back(param);
}
@ -107,6 +107,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
rec_args.push_back(major_premise);
expr rec_app = mk_app(rec, rec_args);
expr proj_type = Pi(proj_args, result_type);
bool strict = false;
proj_type = infer_implicit(proj_type, nparams, strict);
expr proj_val = Fun(proj_args, rec_app);
bool opaque = false;
bool use_conv_opt = false;

12
tests/lean/run/imp3.lean Normal file
View file

@ -0,0 +1,12 @@
structure is_equiv [class] {A B : Type} (f : A → B) :=
(inv : B → A)
check @is_equiv.inv
namespace is_equiv
context
parameters A B : Type
parameter f : A → B
parameter c : is_equiv f
check inv f
end
end is_equiv