diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 015ef30bf..dba276086 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -291,7 +291,7 @@ public: expr mk_placeholder_meta(optional const & type, tag g, bool is_strict, constraint_seq & cs) { auto ec = mk_placeholder_elaborator(env(), ios(), m_context.get_data(), m_ngen.next(), m_relax_main_opaque, use_local_instances(), - is_strict, type, g); + is_strict, type, g, m_unifier_config); cs += ec.second; return ec.first; } diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 55b7e864c..02d263a33 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/opaque_hints.h" #include "library/metavar_closure.h" +#include "library/error_handling/error_handling.h" #include "frontends/lean/util.h" #include "frontends/lean/class.h" #include "frontends/lean/tactic_hint.h" @@ -202,9 +203,7 @@ struct placeholder_elaborator : public choice_iterator { }; -pair mk_placeholder_elaborator(std::shared_ptr const & C, - bool is_strict, optional const & type, tag g) { - expr m = C->m_ctx.mk_meta(type, g); +constraint mk_placeholder_cnstr(std::shared_ptr const & C, expr const & m, bool is_strict) { 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, @@ -239,19 +238,98 @@ pair mk_placeholder_elaborator(std::shared_ptrm_relax; - constraint c = mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance), - owner, j, relax); + return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance), + owner, j, relax); +} + +pair mk_placeholder_elaborator(std::shared_ptr const & C, + bool is_strict, optional const & type, tag g) { + expr m = C->m_ctx.mk_meta(type, g); + constraint c = mk_placeholder_cnstr(C, m, is_strict); return mk_pair(m, c); } +/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of + ?m and local constants l_i + Return the updated expression and a justification for all substitutions. +*/ +static pair update_meta(expr const & meta, substitution s) { + buffer args; + expr mvar = get_app_args(meta, args); + justification j; + auto p = s.instantiate_metavars(mlocal_type(mvar)); + mvar = update_mlocal(mvar, p.first); + j = p.second; + for (expr & arg : args) { + auto p = s.instantiate_metavars(mlocal_type(arg)); + arg = update_mlocal(arg, p.first); + j = mk_composite1(j, p.second); + } + return mk_pair(mk_app(mvar, args), j); +} + +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 (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 + return lazy_list(constraints()); + } + pair mj = update_meta(meta, s); + expr new_meta = mj.first; + justification new_j = mj.second; + try { + constraint c = mk_placeholder_cnstr(C, new_meta, is_strict); + unifier_config new_cfg(cfg); + new_cfg.m_discard = false; + unify_result_seq seq = unify(env, 1, &c, ngen, new_cfg); + auto p = seq.pull(); + if (!p) + return lazy_list(); + substitution new_s = p->first.first; + constraints postponed = map(p->first.second, + [&](constraint const & c) { + // we erase internal justifications + return update_justification(c, new_j); + }); + if (!new_s.is_expr_assigned(mlocal_name(get_app_fn(new_meta)))) { + lazy_list(constraints()); + } + 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 lazy_list(append(cs, postponed)); + } catch (exception & ex) { + return lazy_list(); + } + return lazy_list(); + }; + bool owner = false; + bool relax = C->m_relax; + return mk_choice_cnstr(m, choice_fn, delay_factor, owner, j, relax); +} + /** \brief Create a metavariable, and attach choice constraint for generating solutions using class-instances and tactic-hints. */ pair mk_placeholder_elaborator( environment const & env, io_state const & ios, list const & ctx, name const & prefix, bool relax, bool use_local_instances, - bool is_strict, optional const & type, tag g) { - auto C = std::make_shared(env, ios, ctx, prefix, relax, use_local_instances); - return mk_placeholder_elaborator(C, is_strict, type, g); + bool is_strict, optional const & type, tag g, unifier_config const & cfg) { + auto C = std::make_shared(env, ios, ctx, prefix, relax, use_local_instances); + expr m = C->m_ctx.mk_meta(type, g); + constraint c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, to_delay_factor(cnstr_group::Basic)); + return mk_pair(m, c); } } diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/frontends/lean/placeholder_elaborator.h index d4ad1d9f2..bc0378f7b 100644 --- a/src/frontends/lean/placeholder_elaborator.h +++ b/src/frontends/lean/placeholder_elaborator.h @@ -26,5 +26,5 @@ namespace lean { pair mk_placeholder_elaborator( environment const & env, io_state const & ios, list const & ctx, name const & prefix, bool relax_opaque, bool use_local_instances, - bool is_strict, optional const & type, tag g); + bool is_strict, optional const & type, tag g, unifier_config const & cfg); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index cf136f640..675a910ce 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1897,15 +1897,15 @@ struct unifier_fn { if (is_level_eq_cnstr(c)) { if (modified) return process_constraint(c); - status st = try_level_eq_zero(c); - if (st != Continue) return st == Solved; - if (cidx < get_group_first_index(cnstr_group::FlexFlex)) { - add_cnstr(c, cnstr_group::FlexFlex); - return true; - } if (m_config.m_discard) { - // try_merge_max is too imprecise, and is only used if we are discarding - // constraints that cannot be solved. + // we only try try_level_eq_zero and try_merge_max when we are discarding + // constraints that canno be solved. + status st = try_level_eq_zero(c); + if (st != Continue) return st == Solved; + if (cidx < get_group_first_index(cnstr_group::FlexFlex)) { + add_cnstr(c, cnstr_group::FlexFlex); + return true; + } st = try_merge_max(c); if (st != Continue) return st == Solved; return process_plugin_constraint(c); diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out index d6862512f..83750af98 100644 --- a/tests/lean/empty.lean.expected.out +++ b/tests/lean/empty.lean.expected.out @@ -1,9 +1,2 @@ -empty.lean:6:25: error: type error in placeholder assigned to - num_inhabited -placeholder has type - inhabited num -but is expected to have type - inhabited ?M_1 -the assignment was attempted when trying to solve - failed to synthesize placeholder - ⊢ inhabited Empty +empty.lean:6:25: error: failed to synthesize placeholder + ⊢ nonempty Empty