diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 21ee17f5a3..ec9e6c3455 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "frontends/lean/parse_table.h" #include "frontends/lean/token_table.h" #include "frontends/lean/info_tactic.h" +#include "frontends/lean/placeholder_elaborator.h" #include "frontends/lean/scanner.h" #include "frontends/lean/pp.h" #include "frontends/lean/server.h" @@ -52,10 +53,12 @@ void initialize_frontend_lean_module() { initialize_info_manager(); initialize_info_tactic(); initialize_pp(); + initialize_placeholder_elaborator(); initialize_server(); } void finalize_frontend_lean_module() { finalize_server(); + finalize_placeholder_elaborator(); finalize_pp(); finalize_info_tactic(); finalize_info_manager(); diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 36c131315b..7d4ddec85d 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/lazy_list_fn.h" #include "util/flet.h" +#include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" @@ -18,7 +19,28 @@ Author: Leonardo de Moura #include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" +#ifndef LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES +#define LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES false +#endif + namespace lean { +static name * g_elaborator_unique_class_instances = nullptr; + +void initialize_placeholder_elaborator() { + g_elaborator_unique_class_instances = new name{"elaborator", "unique_class_instances"}; + register_bool_option(*g_elaborator_unique_class_instances, LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES, + "(elaborator) generate an error if there is more than one solution " + "for a class-instance resolution problem"); +} + +void finalize_placeholder_elaborator() { + delete g_elaborator_unique_class_instances; +} + +bool get_elaborator_unique_class_instances(options const & o) { + return o.get_bool(*g_elaborator_unique_class_instances, LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES); +} + /** \brief Context for handling placeholder metavariable choice constraint */ struct placeholder_context { io_state m_ios; @@ -217,6 +239,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const unifier_config const & cfg, delay_factor const & 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 (!is_ext_class(C->tc(), meta_type)) { @@ -230,32 +253,63 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const unifier_config new_cfg(cfg); new_cfg.m_discard = false; new_cfg.m_use_exceptions = false; + + auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) { + substitution new_s = subst; + // some constraints may have been postponed (example: universe level constraints) + constraints postponed = map(cnstrs, + [&](constraint const & c) { + // we erase internal justifications + return update_justification(c, mk_composite1(j, 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); + }; + unify_result_seq seq1 = unify(env, 1, &c, ngen, substitution(), new_cfg); - unify_result_seq seq2 = filter(seq1, [=](pair const & p) { - substitution new_s = p.first; - 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; + if (get_elaborator_unique_class_instances(C->m_ios.get_options())) { + optional solution; + substitution subst; + constraints cnstrs; + for_each(seq1, [&](pair const & p) { + subst = p.first; + cnstrs = p.second; + expr next_solution = subst.instantiate(new_meta); + if (solution) { + // TODO(Leo): more informative error message + throw exception("ambiguous class-instance resolution, there is more than one solution"); + } else { + solution = next_solution; + } + }); + if (!solution) { + if (is_strict) + return lazy_list(); + else + return lazy_list(constraints()); + } else { // 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, mk_composite1(j, 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; + return lazy_list(to_cnstrs_fn(subst, cnstrs)); + } } else { - // make sure it does not fail by appending empty set of constraints - return append(seq3, lazy_list(constraints())); + unify_result_seq seq2 = filter(seq1, [=](pair const & p) { + substitution new_s = p.first; + expr result = new_s.instantiate(new_meta); + // We only keep complete solutions (modulo universe metavariables) + return !has_expr_metavar_relaxed(result); + }); + lazy_list seq3 = map2(seq2, [=](pair const & p) { + return to_cnstrs_fn(p.first, p.second); + }); + 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; diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/frontends/lean/placeholder_elaborator.h index 7647110681..0c6807a376 100644 --- a/src/frontends/lean/placeholder_elaborator.h +++ b/src/frontends/lean/placeholder_elaborator.h @@ -29,4 +29,7 @@ pair mk_placeholder_elaborator( environment const & env, io_state const & ios, local_context const & ctx, name const & prefix, optional const & suffix, bool relax_opaque, bool use_local_instances, bool is_strict, optional const & type, tag g, unifier_config const & cfg); + +void initialize_placeholder_elaborator(); +void finalize_placeholder_elaborator(); }