From a1d200e1c629dc8b745c065224c8a952239c81be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Oct 2015 14:45:39 -0700 Subject: [PATCH] feat(library/class_instance_resolution): add support for nested type class resolution --- src/library/class_instance_resolution.cpp | 73 +++++++++++++++-------- src/library/type_inference.h | 2 +- 2 files changed, 48 insertions(+), 27 deletions(-) diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index fc0d3dd6c..8de4402fc 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -173,9 +173,9 @@ struct cienv { metavariable whose type is a type class, and (?m t_1 ... t_n) must be synthesized by type class resolution, then we return ?m. Otherwise, we return none */ - optional find_unsynth_metavar(expr const & e) { + optional> find_unsynth_metavar(expr const & e) { if (!has_meta_arg(e)) - return none_expr(); + return optional>(); buffer args; expr const & fn = get_app_args(e, args); expr type = m_cienv.infer_type(fn); @@ -183,39 +183,46 @@ struct cienv { while (i < args.size()) { type = m_cienv.whnf(type); if (!is_pi(type)) - return none_expr(); + return optional>(); expr const & arg = args[i]; if (binding_info(type).is_inst_implicit() && is_meta(arg)) { expr const & m = get_app_fn(arg); if (is_mvar(m)) { expr m_type = instantiate_uvars_mvars(infer_metavar(m)); if (!has_expr_metavar_relaxed(m_type)) { - return some_expr(m); + return some(mk_pair(m, m_type)); } } } type = instantiate(binding_body(type), arg); i++; } - return none_expr(); + return optional>(); } - bool mk_instance(expr const & m) { + bool mk_instance(expr const & m, expr const & m_type) { lean_assert(m); - std::cout << "\n\nFOUND CANDIDATE: " << m << "\n\n"; - // TODO(Leo) - return false; + if (auto r = m_cienv.mk_nested_instance(m_type)) { + m_cienv.update_assignment(m, *r); + return true; + } else { + return false; + } } - virtual bool on_is_def_eq_failure(expr const & e1, expr const & e2) { + virtual bool on_is_def_eq_failure(expr & e1, expr & e2) { if (is_app(e1) && is_app(e2)) { - if (auto m1 = find_unsynth_metavar(e1)) { - if (mk_instance(*m1)) + if (auto p1 = find_unsynth_metavar(e1)) { + if (mk_instance(p1->first, p1->second)) { + e1 = m_cienv.instantiate_uvars_mvars(e1); return true; + } } - if (auto m2 = find_unsynth_metavar(e2)) { - if (mk_instance(*m2)) + if (auto p2 = find_unsynth_metavar(e2)) { + if (mk_instance(p2->first, p2->second)) { + e2 = m_cienv.instantiate_uvars_mvars(e2); return true; + } } } return false; @@ -497,10 +504,10 @@ struct cienv { } } - void set_pos_info(pos_info_provider const * pip, expr const & type) { + void set_pos_info(pos_info_provider const * pip, expr const & pos_ref) { m_pip = pip; if (m_pip) - m_pos = m_pip->get_pos_info(type); + m_pos = m_pip->get_pos_info(pos_ref); } // Create an internal universal metavariable @@ -803,10 +810,9 @@ struct cienv { } void init_search(expr const & type) { - m_state = state(); - m_main_mvar = mk_mvar(type); + m_state = state(); + m_main_mvar = mk_mvar(type); m_state.m_stack = cons(mk_pair(0u, m_main_mvar), m_state.m_stack); - m_displayed_trace_header = false; m_choices.clear(); } @@ -822,13 +828,7 @@ struct cienv { } } - optional operator()(environment const & env, options const & o, pos_info_provider const * pip, list const & ctx, expr const & type, - expr const & pos_ref) { - set_env(env); - set_options(o); - set_ctx(ctx); - set_pos_info(pip, pos_ref); - + optional mk_instance_core(expr const & type) { if (auto r = check_cache(type)) { if (m_trace_instances) { auto out = diagnostic(); @@ -842,12 +842,33 @@ struct cienv { return ensure_no_meta(r); } + optional operator()(environment const & env, options const & o, pos_info_provider const * pip, list const & ctx, expr const & type, + expr const & pos_ref) { + set_env(env); + set_options(o); + set_ctx(ctx); + set_pos_info(pip, pos_ref); + m_displayed_trace_header = false; + + return mk_instance_core(type); + } + optional next() { if (!m_multiple_instances) return none_expr(); auto r = next_solution(); return ensure_no_meta(r); } + + optional mk_nested_instance(expr const & type) { + std::vector choices; + m_choices.swap(choices); // save choice stack + flet save_state(m_state, state()); + flet save_main_mvar(m_main_mvar, expr()); + auto r = mk_instance_core(type); + m_choices.swap(choices); // restore choice stack + return r; + } }; MK_THREAD_LOCAL_GET_DEF(cienv, get_cienv); diff --git a/src/library/type_inference.h b/src/library/type_inference.h index b62df50da..c372de644 100644 --- a/src/library/type_inference.h +++ b/src/library/type_inference.h @@ -144,7 +144,7 @@ public: /** \brief This method is invoked before failure. The "customer" may try to assign unassigned mvars in the given expression. The result is true to indicate that some metavariable has been assigned. */ - virtual bool on_is_def_eq_failure(expr const &, expr const &) { return false; } + virtual bool on_is_def_eq_failure(expr &, expr &) { return false; } bool is_assigned(level const & u) const { return get_assignment(u) != nullptr; } bool is_assigned(expr const & m) const { return get_assignment(m) != nullptr; }