diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 5552bc161..99ce13e31 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -351,7 +351,7 @@ public: while (true) { lean_assert(is_pi(type)); tag g = e.get_tag(); - bool is_strict = false; + bool is_strict = true; expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, cs); e = mk_app(e, imp_arg, g); type = instantiate(binding_body(type), imp_arg); @@ -556,7 +556,7 @@ public: bool first = true; while (binding_info(f_type).is_strict_implicit() || (!first && binding_info(f_type).is_implicit())) { tag g = f.get_tag(); - bool is_strict = false; + bool is_strict = true; expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, f_cs); f = mk_app(f, imp_arg, g); auto f_t = ensure_fun(f, f_cs); @@ -804,7 +804,7 @@ public: tag g = e.get_tag(); expr r_type = whnf(infer_type(r, cs), cs); expr imp_arg; - bool is_strict = false; + bool is_strict = true; while (is_pi(r_type) && binding_info(r_type).is_implicit()) { imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs); r = mk_app(r, imp_arg, g); diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 38233cca9..e03732cc7 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "util/lazy_list_fn.h" #include "util/flet.h" #include "kernel/instantiate.h" +#include "kernel/for_each_fn.h" #include "kernel/abstract.h" #include "library/unifier.h" #include "library/reducible.h" @@ -44,7 +45,7 @@ struct placeholder_context { }; pair mk_placeholder_elaborator(std::shared_ptr const & C, - bool is_strict, optional const & type, tag g); + optional const & type, tag g); /** \brief Whenever the elaborator finds a placeholder '_' or introduces an implicit argument, it creates a metavariable \c ?m. It also creates a @@ -86,8 +87,8 @@ struct placeholder_elaborator : public choice_iterator { expr const & meta, expr const & meta_type, list const & local_insts, list const & instances, list const & tacs, - justification const & j, bool ignore_failure): - choice_iterator(ignore_failure), m_C(C), + justification const & j): + choice_iterator(), m_C(C), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances), m_tactics(tacs), @@ -124,9 +125,7 @@ struct placeholder_elaborator : public choice_iterator { type = tc.whnf(type).first; if (!is_pi(type)) break; - bool is_strict = true; - pair ac = mk_placeholder_elaborator(m_C, is_strict, - some_expr(binding_domain(type)), g); + pair ac = mk_placeholder_elaborator(m_C, some_expr(binding_domain(type)), g); expr arg = ac.first; cs.push_back(ac.second); r = mk_app(r, arg).set_tag(g); @@ -205,7 +204,7 @@ struct placeholder_elaborator : public choice_iterator { }; -constraint mk_placeholder_cnstr(std::shared_ptr const & C, expr const & m, bool is_strict) { +constraint mk_placeholder_cnstr(std::shared_ptr const & C, expr const & m) { environment const & env = C->env(); justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, @@ -224,18 +223,10 @@ constraint mk_placeholder_cnstr(std::shared_ptr const & C, if (empty(local_insts) && empty(insts) && empty(tacs)) return lazy_list(); // nothing to be done // we are always strict with placeholders associated with classes - bool ignore_failure = false; - return choose(std::make_shared(C, meta, meta_type, local_insts, insts, tacs, - j, ignore_failure)); - } else if (s.is_assigned(mvar)) { - // if the metavariable is assigned and it is not a class, then we just ignore it, and return - // the an empty set of constraints. - return lazy_list(constraints()); + return choose(std::make_shared(C, meta, meta_type, local_insts, insts, tacs, j)); } else { - list tacs = get_tactic_hints(env); - bool ignore_failure = !is_strict; - return choose(std::make_shared(C, meta, meta_type, list(), list(), - tacs, j, ignore_failure)); + // do nothing, type is not a class... + return lazy_list(constraints()); } }; bool owner = false; @@ -245,52 +236,82 @@ constraint mk_placeholder_cnstr(std::shared_ptr const & C, } pair mk_placeholder_elaborator(std::shared_ptr const & C, - bool is_strict, optional const & type, tag g) { + optional const & type, tag g) { expr m = C->m_ctx.mk_meta(C->m_ngen, type, g); - constraint c = mk_placeholder_cnstr(C, m, is_strict); + constraint c = mk_placeholder_cnstr(C, m); return mk_pair(m, c); } +/** \brief Similar to has_expr_metavar, but ignores metavariables occurring in the type + of local constants */ +static bool has_expr_metavar_relaxed(expr const & e) { + if (!has_expr_metavar(e)) + return false; + bool found = false; + for_each(e, [&](expr const & e, unsigned) { + if (found || !has_expr_metavar(e)) + return false; + if (is_metavar(e)) { + found = true; + return false; + } + if (is_local(e)) + return false; // do not visit type + return true; + }); + return found; +} + constraint mk_placeholder_root_cnstr(std::shared_ptr const & C, expr const & m, bool is_strict, unifier_config const & cfg, unsigned delay_factor) { environment const & env = C->env(); justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & ngen) { - if (has_expr_metavar(meta_type)) { + if (has_expr_metavar_relaxed(meta_type)) { if (delay_factor < to_delay_factor(cnstr_group::ClassInstance)) { constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, delay_factor+1); return lazy_list(constraints(delayed_c)); } } - expr const & mvar = get_app_fn(meta); - if (!is_ext_class(C->tc(), meta_type) && s.is_assigned(mvar)) { - // see mk_placeholder_cnstr + if (!is_ext_class(C->tc(), meta_type)) { + // do nothing, since type is not a class. return lazy_list(constraints()); } pair mj = update_meta(meta, s); expr new_meta = mj.first; justification new_j = mj.second; - constraint c = mk_placeholder_cnstr(C, new_meta, is_strict); + constraint c = mk_placeholder_cnstr(C, new_meta); unifier_config new_cfg(cfg); new_cfg.m_discard = false; new_cfg.m_use_exceptions = false; - unify_result_seq seq = unify(env, 1, &c, ngen, new_cfg); - return map2(seq, [=](pair const & p) { + unify_result_seq seq1 = unify(env, 1, &c, ngen, new_cfg); + unify_result_seq seq2 = filter(seq1, [=](pair const & p) { substitution new_s = p.first; - if (!new_s.is_expr_assigned(mlocal_name(get_app_fn(new_meta)))) - return constraints(); - constraints postponed = map(p.second, - [&](constraint const & c) { - // we erase internal justifications - return update_justification(c, new_j); - }); - metavar_closure cls(new_meta); - cls.add(meta_type); - bool relax = C->m_relax; - constraints cs = cls.mk_constraints(new_s, new_j, relax); - return append(cs, postponed); + expr result = new_s.instantiate(new_meta); + // We only keep complete solution (modulo universe metavariables) + return !has_expr_metavar_relaxed(result); }); + lazy_list seq3 = map2(seq2, [=](pair const & p) { + substitution new_s = p.first; + // some constraints may have been postponed (example: universe level constraints) + constraints postponed = map(p.second, + [&](constraint const & c) { + // we erase internal justifications + return update_justification(c, new_j); + }); + metavar_closure cls(new_meta); + cls.add(meta_type); + bool relax = C->m_relax; + constraints cs = cls.mk_constraints(new_s, new_j, relax); + return append(cs, postponed); + }); + if (is_strict) { + return seq3; + } else { + // make sure it does not fail by appending empty set of constraints + return append(seq3, lazy_list(constraints())); + } }; bool owner = false; bool relax = C->m_relax; diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean index a1eed0c45..7c525defc 100644 --- a/tests/lean/run/class7.lean +++ b/tests/lean/run/class7.lean @@ -4,22 +4,15 @@ open tactic inductive inh (A : Type) : Type := intro : A -> inh A -instance inh.intro - theorem inh_bool [instance] : inh Prop := inh.intro true theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) := inh.rec (λ b, inh.intro (λ a : A, b)) H -definition assump := eassumption; now - -set_option elaborator.local_instances false -tactic_hint [inh] assump -tactic_hint assump - theorem tst {A B : Type} (H : inh B) : inh (A → B → B) -theorem T1 {A : Type} (a : A) : inh A +theorem T1 {A : Type} (a : A) : inh A := +by repeat [apply @inh.intro | eassumption] theorem T2 : inh Prop diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index bf9905e71..4ace94760 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -9,7 +9,7 @@ instance inh.intro theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B := inh.rec H2 H1 -theorem inh_exists [instance] {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A +theorem inh_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A := obtain w Hw, from H, inh.intro w theorem inh_bool [instance] : inh Prop @@ -26,7 +26,10 @@ tactic_hint assump theorem tst {A B : Type} (H : inh B) : inh (A → B → B) -theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) +theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) := +have h1 [visible] : inh A, from inh.intro a, +have h2 [visible] : inh C, from inh_exists H2, +_ (* print(get_env():find("T1"):value())