From 6a36bffe4bb2a8b6de43fe28698fd63ce44ba797 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Oct 2015 13:53:38 -0700 Subject: [PATCH] fix(library/class_instance_resolution): bugs in new type class resolution procedure --- src/frontends/lean/elaborator.cpp | 4 +- src/library/CMakeLists.txt | 18 +- src/library/class_instance_resolution.cpp | 214 ++++++--- src/library/class_instance_resolution.h | 27 ++ src/library/class_instance_synth.cpp | 539 ---------------------- src/library/class_instance_synth.h | 55 --- src/library/init_module.cpp | 9 +- src/library/tactic/apply_tactic.cpp | 4 +- src/library/tactic/congruence_tactic.cpp | 2 +- src/library/tactic/induction_tactic.cpp | 5 +- src/library/tactic/inversion_tactic.cpp | 2 +- src/library/tactic/rewrite_tactic.cpp | 6 +- 12 files changed, 199 insertions(+), 686 deletions(-) delete mode 100644 src/library/class_instance_synth.cpp delete mode 100644 src/library/class_instance_synth.h diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7a468da0a6..e35bab1682 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -39,7 +39,7 @@ Author: Leonardo de Moura #include "library/choice_iterator.h" #include "library/projection.h" #include "library/pp_options.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/tactic/expr_to_tactic.h" #include "library/error_handling/error_handling.h" #include "library/definitional/equations.h" @@ -293,7 +293,7 @@ expr elaborator::mk_placeholder_meta(optional const & suffix, optional ci_type_inference_ptr; -static name * g_class_unique_class_instances = nullptr; static name * g_class_trace_instances = nullptr; static name * g_class_instance_max_depth = nullptr; static name * g_class_trans_instances = nullptr; @@ -52,10 +50,6 @@ static ci_type_inference_factory * g_default_factory = nullptr; LEAN_THREAD_PTR(ci_type_inference_factory, g_factory); LEAN_THREAD_PTR(io_state, g_ios); -bool get_class_unique_class_instances(options const & o) { - return o.get_bool(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES); -} - bool get_class_trace_instances(options const & o) { return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES); } @@ -85,6 +79,8 @@ public: } }; +ci_type_inference_factory::~ci_type_inference_factory() {} + std::shared_ptr ci_type_inference_factory::operator()(environment const & env) const { return std::shared_ptr(new default_ci_type_inference(env)); } @@ -108,8 +104,8 @@ struct cienv { list m_ctx; buffer> m_local_instances; - unsigned m_next_uvar; - unsigned m_next_mvar; + unsigned m_next_uvar_idx; + unsigned m_next_mvar_idx; struct state { list m_stack; // stack of meta-variables that need to be synthesized; @@ -134,15 +130,14 @@ struct cienv { bool m_displayed_trace_header; // configuration - bool m_unique_instances; unsigned m_max_depth; bool m_trans_instances; bool m_trace_instances; cienv(bool multiple_instances = false): m_ngen(*g_prefix2), - m_next_uvar(0), - m_next_mvar(0), + m_next_uvar_idx(0), + m_next_mvar_idx(0), m_multiple_instances(multiple_instances) {} bool is_not_reducible(name const & n) const { @@ -176,18 +171,15 @@ struct cienv { } void set_options(options const & o) { - bool unique_instances = get_class_unique_class_instances(o); unsigned max_depth = get_class_instance_max_depth(o); bool trans_instances = get_class_trans_instances(o); bool trace_instances = get_class_trace_instances(o); - if (m_unique_instances != unique_instances || - m_max_depth != max_depth || + if (m_max_depth != max_depth || m_trans_instances != trans_instances || m_trace_instances != trace_instances) { reset_cache(); } - m_unique_instances = unique_instances; m_max_depth = max_depth; m_trans_instances = trans_instances; m_trace_instances = trace_instances; @@ -251,7 +243,7 @@ struct cienv { if (!is_constant(f)) return optional(); return constant_is_class(f); - } + } } /** \brief Partial/Quick test for is_class. Result @@ -355,8 +347,8 @@ struct cienv { // Create an internal universal metavariable level mk_uvar() { - unsigned idx = m_next_uvar; - m_next_uvar++; + unsigned idx = m_next_uvar_idx; + m_next_uvar_idx++; return mk_meta_univ(name(*g_prefix2, idx)); } @@ -394,8 +386,8 @@ struct cienv { // Create an internal metavariable. expr mk_mvar(expr const & type) { - unsigned idx = m_next_mvar; - m_next_mvar++; + unsigned idx = m_next_mvar_idx; + m_next_mvar_idx++; return mk_metavar(name(*g_prefix2, idx), type); } @@ -422,6 +414,7 @@ struct cienv { void update_assignment(expr const & m, expr const & v) { m_state.m_eassignment.insert(mvar_idx(m), v); + lean_assert(is_assigned(m)); } // Assign \c v to the metavariable \c m. @@ -625,7 +618,7 @@ struct cienv { } virtual expr visit(expr const & e) { - if (!has_expr_metavar(e) || !has_univ_metavar(e)) + if (!has_expr_metavar(e) && !has_univ_metavar(e)) return e; else return replace_visitor::visit(e); @@ -933,11 +926,6 @@ struct cienv { return empty(m_state.m_stack); } - expr const & next_mvar() const { - lean_assert(!is_done()); - return head(m_state.m_stack); - } - bool mk_choice_point(expr const & mvar) { lean_assert(is_mvar(mvar)); if (m_choices.size() > m_max_depth) { @@ -966,45 +954,46 @@ struct cienv { return true; } - bool process_next_alt_core(list & insts) { + bool process_next_alt_core(expr const & mvar, list & insts) { while (!empty(insts)) { expr inst = head(insts); insts = tail(insts); expr inst_type = infer_type(inst); - if (try_instance(next_mvar(), inst, inst_type)) + if (try_instance(mvar, inst, inst_type)) return true; } return false; } - bool process_next_alt_core(list & inst_names) { + bool process_next_alt_core(expr const & mvar, list & inst_names) { while (!empty(inst_names)) { name inst_name = head(inst_names); inst_names = tail(inst_names); - if (try_instance(next_mvar(), inst_name)) + if (try_instance(mvar, inst_name)) return true; } return false; } - bool process_next_alt() { + bool process_next_alt(expr const & mvar) { lean_assert(!m_choices.empty()); choice & c = m_choices.back(); - if (process_next_alt_core(c.m_local_instances)) + if (process_next_alt_core(mvar, c.m_local_instances)) return true; - if (process_next_alt_core(c.m_trans_instances)) + if (process_next_alt_core(mvar, c.m_trans_instances)) return true; - if (process_next_alt_core(c.m_instances)) + if (process_next_alt_core(mvar, c.m_instances)) return true; return false; } bool process_next_mvar() { lean_assert(!is_done()); - expr mvar = next_mvar(); + expr mvar = head(m_state.m_stack); if (!mk_choice_point(mvar)) return false; - return process_next_alt(); + m_state.m_stack = tail(m_state.m_stack); + return process_next_alt(mvar); } bool backtrack() { @@ -1013,8 +1002,10 @@ struct cienv { m_choices.pop_back(); if (m_choices.empty()) return false; - m_state = m_choices.back().m_state; - if (process_next_alt()) + m_state = m_choices.back().m_state; + expr mvar = head(m_state.m_stack); + m_state.m_stack = tail(m_state.m_stack); + if (process_next_alt(mvar)) return true; } } @@ -1029,6 +1020,20 @@ struct cienv { return some_expr(instantiate_uvars_mvars(m_main_mvar)); } + optional next_solution() { + if (m_choices.empty()) + return none_expr(); + m_state = m_choices.back().m_state; + expr mvar = head(m_state.m_stack); + m_state.m_stack = tail(m_state.m_stack); + if (process_next_alt(mvar)) + return search(); + else if (backtrack()) + return search(); + else + return none_expr(); + } + void init_search(expr const & type) { m_state = state(); m_main_mvar = mk_mvar(type); @@ -1036,37 +1041,42 @@ struct cienv { m_displayed_trace_header = false; } + optional ensure_no_meta(optional r) { + while (true) { + if (!r) + return none_expr(); + if (!has_expr_metavar_relaxed(*r)) { + cache_result(mlocal_type(m_main_mvar), *r); + return r; + } + r = next_solution(); + } + } + optional operator()(environment const & env, options const & o, pos_info_provider const * pip, list const & ctx, expr const & type) { set_env(env); set_options(o); set_ctx(ctx); set_pos_info(pip, type); - if (auto r = check_cache(type)) + if (auto r = check_cache(type)) { + if (m_trace_instances) { + auto out = diagnostic(m_env, *g_ios); + out << "cached instance for " << type << "\n" << *r << "\n"; + } return r; + } init_search(type); - - if (auto r = search()) { - cache_result(type, *r); - return r; - } else { - return none_expr(); - } + auto r = search(); + return ensure_no_meta(r); } optional next() { if (!m_multiple_instances) return none_expr(); - if (m_choices.empty()) - return none_expr(); - m_state = m_choices.back().m_state; - if (process_next_alt()) - return search(); - else if (backtrack()) - return search(); - else - return none_expr(); + auto r = next_solution(); + return ensure_no_meta(r); } }; @@ -1087,27 +1097,100 @@ ci_type_inference_factory_scope::~ci_type_inference_factory_scope() { g_factory = m_old; } -optional mk_class_instance(environment const & env, io_state const & ios, list const & ctx, expr const & e, pos_info_provider * pip) { +optional mk_class_instance(environment const & env, io_state const & ios, list const & ctx, expr const & e, pos_info_provider const * pip) { flet set_ios(g_ios, const_cast(&ios)); return get_cienv()(env, ios.get_options(), pip, ctx, e); } -optional mk_class_instance(environment const & env, list const & ctx, expr const & e, pos_info_provider * pip) { +optional mk_class_instance(environment const & env, list const & ctx, expr const & e, pos_info_provider const * pip) { return mk_class_instance(env, get_dummy_ios(), ctx, e, pip); } +static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, local_context const & _ctx, expr const & m, bool is_strict, + bool use_local_instances, pos_info_provider const * pip) { + justification j = mk_failed_to_synthesize_jst(env, m); + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator &&) { + cienv & cenv = get_cienv(); + cenv.set_env(env); + auto cls_name = cenv.is_class(meta_type); + if (!cls_name) { + // do nothing, since type is not a class. + return lazy_list(constraints()); + } + bool multiple_insts = try_multiple_instances(env, *cls_name); + local_context ctx; + if (use_local_instances) + ctx = _ctx.instantiate(substitution(s)); + pair mj = update_meta(meta, s); + expr new_meta = mj.first; + justification new_j = mj.second; + if (multiple_insts) { + // TODO(Leo) + return lazy_list(); + } else { + if (auto r = mk_class_instance(env, ios, ctx.get_data(), meta_type, pip)) { + constraint c = mk_eq_cnstr(new_meta, *r, new_j); + return lazy_list(constraints(c)); + } else if (is_strict) { + return lazy_list(); + } else { + return lazy_list(constraints()); + } + } + }; + bool owner = false; + delay_factor factor; + return mk_choice_cnstr(m, choice_fn, factor, owner, j); +} + +/** \brief Create a metavariable, and attach choice constraint for generating + solutions using class-instances +*/ +pair mk_class_instance_elaborator( + environment const & env, io_state const & ios, local_context const & ctx, + name const & prefix, optional const & suffix, bool use_local_instances, + bool is_strict, optional const & type, tag g, pos_info_provider const * pip) { + name_generator ngen(prefix); + expr m = ctx.mk_meta(ngen, suffix, type, g); + constraint c = mk_class_instance_root_cnstr(env, ios, ctx, m, is_strict, + use_local_instances, pip); + return mk_pair(m, c); +} + +optional mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances) { + if (use_local_instances) + return mk_class_instance(env, ios, ctx.get_data(), type, nullptr); + else + return mk_class_instance(env, ios, list(), type, nullptr); +} + +optional mk_class_instance(environment const & env, local_context const & ctx, expr const & type) { + return mk_class_instance(env, ctx.get_data(), type, nullptr); +} + +optional mk_hset_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type) { + level lvl = sort_level(tc.ensure_type(type).first); + expr is_hset = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first; + return mk_class_instance(tc.env(), ios, ctx, is_hset); +} + +optional mk_subsingleton_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type) { + level lvl = sort_level(tc.ensure_type(type).first); + expr subsingleton; + if (is_standard(tc.env())) + subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type); + else + subsingleton = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)).first; + return mk_class_instance(tc.env(), ios, ctx, subsingleton); +} + void initialize_class_instance_resolution() { g_prefix1 = new name(name::mk_internal_unique_name()); g_prefix2 = new name(name::mk_internal_unique_name()); - g_class_unique_class_instances = new name{"class", "unique_instances"}; g_class_trace_instances = new name{"class", "trace_instances"}; g_class_instance_max_depth = new name{"class", "instance_max_depth"}; g_class_trans_instances = new name{"class", "trans_instances"}; - register_bool_option(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES, - "(class) generate an error if there is more than one solution " - "for a class-instance resolution problem"); - register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES, "(class) display messages showing the class-instances resolution execution trace"); @@ -1124,7 +1207,6 @@ void finalize_class_instance_resolution() { delete g_default_factory; delete g_prefix1; delete g_prefix2; - delete g_class_unique_class_instances; delete g_class_trace_instances; delete g_class_instance_max_depth; delete g_class_trans_instances; diff --git a/src/library/class_instance_resolution.h b/src/library/class_instance_resolution.h index a6b1c75bfd..e4cabd7782 100644 --- a/src/library/class_instance_resolution.h +++ b/src/library/class_instance_resolution.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "kernel/environment.h" #include "library/io_state.h" +#include "library/local_context.h" namespace lean { class ci_type_inference { @@ -32,6 +33,32 @@ public: optional mk_class_instance(environment const & env, io_state const & ios, list const & ctx, expr const & e, pos_info_provider const * pip = nullptr); optional mk_class_instance(environment const & env, list const & ctx, expr const & e, pos_info_provider const * pip = nullptr); + +// Old API + +/** \brief Create a metavariable, and attach choice constraint for generating + solutions using class-instances. + + \param ctx Local context where placeholder is located + \param prefix Prefix for metavariables that will be created by this procedure + \param suffix If provided, then it is added to the main metavariable created by this procedure. + \param use_local_instances If instances in the local context should be used + in the class-instance resolution + \param is_strict True if constraint should fail if not solution is found, + False if empty solution should be returned if there is no solution + \param type Expected type for the placeholder (if known) + \param tag To be associated with new metavariables and expressions (for error localization). +*/ +pair mk_class_instance_elaborator( + environment const & env, io_state const & ios, local_context const & ctx, + name const & prefix, optional const & suffix, bool use_local_instances, + bool is_strict, optional const & type, tag g, pos_info_provider const * pip); + +optional mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances); +optional mk_class_instance(environment const & env, local_context const & ctx, expr const & type); +optional mk_hset_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type); +optional mk_subsingleton_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type); + void initialize_class_instance_resolution(); void finalize_class_instance_resolution(); } diff --git a/src/library/class_instance_synth.cpp b/src/library/class_instance_synth.cpp deleted file mode 100644 index 5f643ce6e3..0000000000 --- a/src/library/class_instance_synth.cpp +++ /dev/null @@ -1,539 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -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" -#include "kernel/error_msgs.h" -#include "library/unifier.h" -#include "library/reducible.h" -#include "library/metavar_closure.h" -#include "library/error_handling/error_handling.h" -#include "library/class.h" -#include "library/local_context.h" -#include "library/choice_iterator.h" -#include "library/pp_options.h" -#include "library/generic_exception.h" -#include "library/util.h" -#include "library/constants.h" -#include "library/class_instance_synth.h" - -#ifndef LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES -#define LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES false -#endif - -#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES -#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false -#endif - -#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH -#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32 -#endif - -#ifndef LEAN_DEFAULT_CLASS_CONSERVATIVE -#define LEAN_DEFAULT_CLASS_CONSERVATIVE true -#endif - -#ifndef LEAN_DEFAULT_CLASS_TRANS_INSTANCES -#define LEAN_DEFAULT_CLASS_TRANS_INSTANCES true -#endif - -namespace lean { -static name * g_tmp_prefix = nullptr; -static name * g_class_unique_class_instances = nullptr; -static name * g_class_trace_instances = nullptr; -static name * g_class_instance_max_depth = nullptr; -static name * g_class_conservative = nullptr; -static name * g_class_trans_instances = nullptr; - -[[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); } -[[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); } - -void initialize_class_instance_elaborator() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_class_unique_class_instances = new name{"class", "unique_instances"}; - g_class_trace_instances = new name{"class", "trace_instances"}; - g_class_instance_max_depth = new name{"class", "instance_max_depth"}; - g_class_conservative = new name{"class", "conservative"}; - g_class_trans_instances = new name{"class", "trans_instances"}; - - register_bool_option(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES, - "(class) generate an error if there is more than one solution " - "for a class-instance resolution problem"); - - register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES, - "(class) display messages showing the class-instances resolution execution trace"); - - register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, - "(class) max allowed depth in class-instance resolution"); - - register_bool_option(*g_class_conservative, LEAN_DEFAULT_CLASS_CONSERVATIVE, - "(class) use conservative unification (only unfold reducible definitions, and avoid delta-delta case splits)"); - - register_bool_option(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES, - "(class) use automatically derived instances from the transitive closure of the structure instance graph"); -} - -void finalize_class_instance_elaborator() { - delete g_tmp_prefix; - delete g_class_unique_class_instances; - delete g_class_trace_instances; - delete g_class_instance_max_depth; - delete g_class_conservative; - delete g_class_trans_instances; -} - -bool get_class_unique_class_instances(options const & o) { - return o.get_bool(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES); -} - -bool get_class_trace_instances(options const & o) { - return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES); -} - -unsigned get_class_instance_max_depth(options const & o) { - return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH); -} - -bool get_class_conservative(options const & o) { - return o.get_bool(*g_class_conservative, LEAN_DEFAULT_CLASS_CONSERVATIVE); -} - -bool get_class_trans_instances(options const & o) { - return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES); -} - -/** \brief Context for handling class-instance metavariable choice constraint */ -struct class_instance_context { - io_state m_ios; - name_generator m_ngen; - type_checker_ptr m_tc; - expr m_main_meta; - bool m_use_local_instances; - bool m_trace_instances; - bool m_conservative; - unsigned m_max_depth; - bool m_trans_instances; - char const * m_fname; - optional m_pos; - class_instance_context(environment const & env, io_state const & ios, - name const & prefix, bool use_local_instances): - m_ios(ios), - m_ngen(prefix), - m_use_local_instances(use_local_instances) { - m_fname = nullptr; - m_trace_instances = get_class_trace_instances(ios.get_options()); - m_max_depth = get_class_instance_max_depth(ios.get_options()); - m_conservative = get_class_conservative(ios.get_options()); - m_trans_instances = get_class_trans_instances(ios.get_options()); - m_tc = mk_class_type_checker(env, m_ngen.mk_child(), m_conservative); - options opts = m_ios.get_options(); - opts = opts.update_if_undef(get_pp_purify_metavars_name(), false); - opts = opts.update_if_undef(get_pp_implicit_name(), true); - m_ios.set_options(opts); - } - - environment const & env() const { return m_tc->env(); } - io_state const & ios() const { return m_ios; } - bool use_local_instances() const { return m_use_local_instances; } - type_checker & tc() const { return *m_tc; } - bool trace_instances() const { return m_trace_instances; } - void set_main_meta(expr const & meta) { m_main_meta = meta; } - expr const & get_main_meta() const { return m_main_meta; } - void set_pos(char const * fname, optional const & pos) { - m_fname = fname; - m_pos = pos; - } - optional const & get_pos() const { return m_pos; } - char const * get_file_name() const { return m_fname; } - unsigned get_max_depth() const { return m_max_depth; } - bool use_trans_instances() const { return m_trans_instances; } -}; - -static pair mk_class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, - optional const & type, tag g, unsigned depth, bool use_globals); - -/** \brief Choice function \c fn for synthesizing class instances. - - - The function \c fn produces a stream of alternative solutions for ?m. - In this case, \c fn will do the following: - 1) if the elaborated type of ?m is a 'class' C, then the stream will start with - a) all local instances of class C (if elaborator.local_instances == true) - b) all global instances of class C -*/ -struct class_instance_elaborator : public choice_iterator { - std::shared_ptr m_C; - local_context m_ctx; - expr m_meta; - // elaborated type of the metavariable - expr m_meta_type; - // local instances that should also be included in the - // class-instance resolution. - // This information is retrieved from the local context - list m_local_instances; - // global declaration names that are class instances. - // This information is retrieved using #get_class_instances. - list m_trans_instances; - list m_instances; - justification m_jst; - unsigned m_depth; - bool m_displayed_trace_header; - - class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, - expr const & meta, expr const & meta_type, - list const & local_insts, list const & trans_insts, list const & instances, - justification const & j, unsigned depth): - choice_iterator(), m_C(C), m_ctx(ctx), m_meta(meta), m_meta_type(meta_type), - m_local_instances(local_insts), m_trans_instances(trans_insts), m_instances(instances), m_jst(j), m_depth(depth) { - if (m_depth > m_C->get_max_depth()) { - throw_class_exception("maximum class-instance resolution depth has been reached " - "(the limit can be increased by setting option 'class.instance_max_depth') " - "(the class-instance resolution trace can be visualized by setting option 'class.trace_instances')", - C->get_main_meta()); - } - m_displayed_trace_header = false; - } - - constraints mk_constraints(constraint const & c, buffer const & cs) { - return cons(c, to_list(cs.begin(), cs.end())); - } - - void trace(expr const & t, expr const & r) { - if (!m_C->trace_instances()) - return; - auto out = diagnostic(m_C->env(), m_C->ios()); - if (!m_displayed_trace_header && m_depth == 0) { - if (auto fname = m_C->get_file_name()) { - out << fname << ":"; - } - if (auto pos = m_C->get_pos()) { - out << pos->first << ":" << pos->second << ":"; - } - out << " class-instance resolution trace" << endl; - m_displayed_trace_header = true; - } - for (unsigned i = 0; i < m_depth; i++) - out << " "; - if (m_depth > 0) - out << "[" << m_depth << "] "; - out << m_meta << " : " << t << " := " << r << endl; - } - - optional try_instance(expr const & inst, expr const & inst_type, bool use_globals) { - type_checker & tc = m_C->tc(); - name_generator & ngen = m_C->m_ngen; - tag g = inst.get_tag(); - try { - flet scope(m_ctx, m_ctx); - buffer locals; - expr meta_type = m_meta_type; - while (true) { - meta_type = tc.whnf(meta_type).first; - if (!is_pi(meta_type)) - break; - expr local = mk_local(ngen.next(), binding_name(meta_type), - binding_domain(meta_type), binding_info(meta_type)); - m_ctx.add_local(local); - locals.push_back(local); - meta_type = instantiate(binding_body(meta_type), local); - } - expr type = inst_type; - expr r = inst; - buffer cs; - while (true) { - type = tc.whnf(type).first; - if (!is_pi(type)) - break; - expr arg; - if (binding_info(type).is_inst_implicit()) { - pair ac = mk_class_instance_elaborator(m_C, m_ctx, some_expr(binding_domain(type)), - g, m_depth+1, use_globals); - arg = ac.first; - cs.push_back(ac.second); - } else { - arg = m_ctx.mk_meta(m_C->m_ngen, some_expr(binding_domain(type)), g); - } - r = mk_app(r, arg, g); - type = instantiate(binding_body(type), arg); - } - r = Fun(locals, r); - trace(meta_type, r); - constraint c = mk_eq_cnstr(m_meta, r, m_jst); - return optional(mk_constraints(c, cs)); - } catch (exception &) { - return optional(); - } - } - - optional try_instance(name const & inst, bool use_globals) { - environment const & env = m_C->env(); - if (auto decl = env.find(inst)) { - name_generator & ngen = m_C->m_ngen; - buffer ls_buffer; - unsigned num_univ_ps = decl->get_num_univ_params(); - for (unsigned i = 0; i < num_univ_ps; i++) - ls_buffer.push_back(mk_meta_univ(ngen.next())); - levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); - expr inst_cnst = copy_tag(m_meta, mk_constant(inst, ls)); - expr inst_type = instantiate_type_univ_params(*decl, ls); - return try_instance(inst_cnst, inst_type, use_globals); - } else { - return optional(); - } - } - - virtual optional next() { - while (!empty(m_local_instances)) { - expr inst = head(m_local_instances); - m_local_instances = tail(m_local_instances); - if (!is_local(inst)) - continue; - bool use_globals = true; - if (auto r = try_instance(inst, mlocal_type(inst), use_globals)) - return r; - } - while (!empty(m_trans_instances)) { - bool use_globals = false; - name inst = head(m_trans_instances); - m_trans_instances = tail(m_trans_instances); - if (auto cs = try_instance(inst, use_globals)) - return cs; - } - while (!empty(m_instances)) { - bool use_globals = true; - name inst = head(m_instances); - m_instances = tail(m_instances); - if (auto cs = try_instance(inst, use_globals)) - return cs; - } - return optional(); - } -}; - -// Remarks: -// - we only use get_class_instances and get_class_derived_trans_instances when use_globals is true -static constraint mk_class_instance_cnstr(std::shared_ptr const & C, local_context const & ctx, expr const & m, unsigned depth, bool use_globals) { - 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 &, name_generator const &) { - if (auto cls_name_it = is_ext_class(C->tc(), meta_type)) { - name cls_name = *cls_name_it; - list const & ctx_lst = ctx.get_data(); - list local_insts; - if (C->use_local_instances()) - local_insts = get_local_instances(C->tc(), ctx_lst, cls_name); - list trans_insts, insts; - if (use_globals) { - if (depth == 0 && C->use_trans_instances()) - trans_insts = get_class_derived_trans_instances(env, cls_name); - insts = get_class_instances(env, cls_name); - } - if (empty(local_insts) && empty(insts)) - return lazy_list(); // nothing to be done - // we are always strict with placeholders associated with classes - return choose(std::make_shared(C, ctx, meta, meta_type, local_insts, trans_insts, insts, j, depth)); - } else { - // do nothing, type is not a class... - return lazy_list(constraints()); - } - }; - bool owner = false; - return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic), owner, j); -} - -static pair mk_class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, - optional const & type, tag g, unsigned depth, bool use_globals) { - expr m = ctx.mk_meta(C->m_ngen, type, g); - constraint c = mk_class_instance_cnstr(C, ctx, m, depth, use_globals); - return mk_pair(m, c); -} - -static constraint mk_class_instance_root_cnstr(std::shared_ptr const & C, local_context const & _ctx, - expr const & m, bool is_strict, 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 && ngen) { - environment const & env = C->env(); - auto cls_name_it = is_ext_class(C->tc(), meta_type); - if (!cls_name_it) { - // do nothing, since type is not a class. - return lazy_list(constraints()); - } - local_context ctx = _ctx.instantiate(substitution(s)); - pair mj = update_meta(meta, s); - expr new_meta = mj.first; - justification new_j = mj.second; - unsigned depth = 0; - bool use_globals = true; - constraint c = mk_class_instance_cnstr(C, ctx, new_meta, depth, use_globals); - unifier_config new_cfg(cfg); - new_cfg.m_discard = false; - new_cfg.m_use_exceptions = false; - new_cfg.m_pattern = true; - new_cfg.m_kind = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal; - - auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints { - 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); - constraints cs = cls.mk_constraints(new_s, new_j); - return append(cs, postponed); - }; - - auto no_solution_fn = [=]() { - if (is_strict) - return lazy_list(); - else - return lazy_list(constraints()); - }; - - unify_result_seq seq1 = unify(env, 1, &c, std::move(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 solutions (modulo universe metavariables) - return !has_expr_metavar_relaxed(result); - }); - - if (get_class_unique_class_instances(C->m_ios.get_options())) { - optional solution; - substitution subst; - constraints cnstrs; - for_each(seq2, [&](pair const & p) { - subst = p.first; - cnstrs = p.second; - expr next_solution = subst.instantiate(new_meta); - if (solution) { - throw_class_exception(m, [=](formatter const & fmt) { - format r = format("ambiguous class-instance resolution, " - "there is more than one solution"); - r += pp_indent_expr(fmt, *solution); - r += compose(line(), format("and")); - r += pp_indent_expr(fmt, next_solution); - return r; - }); - } else { - solution = next_solution; - } - }); - if (!solution) { - return no_solution_fn(); - } else { - // some constraints may have been postponed (example: universe level constraints) - return lazy_list(to_cnstrs_fn(subst, cnstrs)); - } - } else { - if (try_multiple_instances(env, *cls_name_it)) { - 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())); - } - } else { - auto p = seq2.pull(); - if (!p) - return no_solution_fn(); - else - return lazy_list(to_cnstrs_fn(p->first.first, p->first.second)); - } - } - }; - bool owner = false; - return mk_choice_cnstr(m, choice_fn, factor, owner, j); -} - -/** \brief Create a metavariable, and attach choice constraint for generating - solutions using class-instances -*/ -pair mk_class_instance_elaborator( - environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, optional const & suffix, bool use_local_instances, - bool is_strict, optional const & type, tag g, unifier_config const & cfg, - pos_info_provider const * pip) { - auto C = std::make_shared(env, ios, prefix, use_local_instances); - expr m = ctx.mk_meta(C->m_ngen, suffix, type, g); - C->set_main_meta(m); - if (pip) - C->set_pos(pip->get_file_name(), pip->get_pos_info(m)); - constraint c = mk_class_instance_root_cnstr(C, ctx, m, is_strict, cfg, delay_factor()); - return mk_pair(m, c); -} - -optional mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, expr const & type, bool use_local_instances, - unifier_config const & cfg) { - auto C = std::make_shared(env, ios, prefix, use_local_instances); - if (!is_ext_class(C->tc(), type)) - return none_expr(); - expr meta = ctx.mk_meta(C->m_ngen, some_expr(type), type.get_tag()); - unsigned depth = 0; - bool use_globals = true; - constraint c = mk_class_instance_cnstr(C, ctx, meta, depth, use_globals); - unifier_config new_cfg(cfg); - new_cfg.m_discard = true; - new_cfg.m_use_exceptions = true; - new_cfg.m_pattern = true; - new_cfg.m_kind = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal; - try { - auto seq = unify(env, 1, &c, C->m_ngen.mk_child(), substitution(), new_cfg); - while (true) { - auto p = seq.pull(); - lean_assert(p); - substitution s = p->first.first; - expr r = s.instantiate_all(meta); - expr new_type = s.instantiate_all(type); - if (!has_expr_metavar_relaxed(r) && new_type == type) - return some_expr(r); - seq = p->second; - } - } catch (exception &) { - return none_expr(); - } -} - -optional mk_class_instance(environment const & env, io_state const & ios, list const & ctx, - name const & prefix, expr const & type, bool use_local_instances, - unifier_config const & cfg) { - local_context lctx(ctx); - return mk_class_instance(env, ios, lctx, prefix, type, use_local_instances, cfg); -} - -optional mk_class_instance(environment const & env, local_context const & ctx, expr const & type) { - return mk_class_instance(env, get_dummy_ios(), ctx, *g_tmp_prefix, type); -} - -optional mk_hset_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type) { - level lvl = sort_level(tc.ensure_type(type).first); - expr is_hset = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first; - return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), is_hset); -} - -optional mk_subsingleton_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type) { - level lvl = sort_level(tc.ensure_type(type).first); - expr subsingleton; - if (is_standard(tc.env())) - subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type); - else - subsingleton = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)).first; - return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), subsingleton); -} -} diff --git a/src/library/class_instance_synth.h b/src/library/class_instance_synth.h deleted file mode 100644 index e1c55d5ba1..0000000000 --- a/src/library/class_instance_synth.h +++ /dev/null @@ -1,55 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/expr.h" -#include "library/io_state.h" -#include "library/unifier.h" - -namespace lean { -class local_context; -class type_checker; - -/** \brief Create a metavariable, and attach choice constraint for generating - solutions using class-instances. - - \param ctx Local context where placeholder is located - \param prefix Prefix for metavariables that will be created by this procedure - \param suffix If provided, then it is added to the main metavariable created by this procedure. - \param use_local_instances If instances in the local context should be used - in the class-instance resolution - \param is_strict True if constraint should fail if not solution is found, - False if empty solution should be returned if there is no solution - \param type Expected type for the placeholder (if known) - \param tag To be associated with new metavariables and expressions (for error localization). -*/ -pair mk_class_instance_elaborator( - environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, optional const & suffix, bool use_local_instances, - bool is_strict, optional const & type, tag g, unifier_config const & cfg, - pos_info_provider const * pip); - -/** \brief Create/synthesize a term of the class instance \c type. */ -optional mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, - name const & prefix, expr const & type, bool use_local_instances = true, - unifier_config const & cfg = unifier_config()); - -optional mk_class_instance(environment const & env, io_state const & ios, list const & ctx, - name const & prefix, expr const & type, bool use_local_instances = true, - unifier_config const & cfg = unifier_config()); - -optional mk_class_instance(environment const & env, local_context const & ctx, expr const & type); - -/** \brief Try to synthesize an inhabitant for (is_hset type) using class instance resolution */ -optional mk_hset_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type); - -/** \brief Try to synthesize an inhabitant for (subsingleton type in the standard library, and hprop in the HoTT library) - using class instance resolution */ -optional mk_subsingleton_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type); - -void initialize_class_instance_elaborator(); -void finalize_class_instance_elaborator(); -} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 73971cf872..235830acf4 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -37,13 +37,14 @@ Author: Leonardo de Moura #include "library/abbreviation.h" #include "library/relation_manager.h" #include "library/user_recursors.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/composition_manager.h" #include "library/noncomputable.h" #include "library/aux_recursors.h" #include "library/decl_stats.h" #include "library/meng_paulson.h" #include "library/norm_num.h" +#include "library/class_instance_resolution.h" namespace lean { void initialize_library_module() { @@ -80,22 +81,23 @@ void initialize_library_module() { initialize_abbreviation(); initialize_relation_manager(); initialize_user_recursors(); - initialize_class_instance_elaborator(); initialize_composition_manager(); initialize_noncomputable(); initialize_aux_recursors(); initialize_decl_stats(); initialize_meng_paulson(); initialize_norm_num(); + initialize_class_instance_resolution(); } void finalize_library_module() { + finalize_class_instance_resolution(); + finalize_norm_num(); finalize_meng_paulson(); finalize_decl_stats(); finalize_aux_recursors(); finalize_noncomputable(); finalize_composition_manager(); - finalize_class_instance_elaborator(); finalize_user_recursors(); finalize_relation_manager(); finalize_abbreviation(); @@ -129,6 +131,5 @@ void finalize_library_module() { finalize_print(); finalize_fingerprint(); finalize_constants(); - finalize_norm_num(); } } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 1d90218ec5..99f6ef0565 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -22,7 +22,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/type_util.h" #include "library/local_context.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/apply_tactic.h" @@ -119,7 +119,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const auto mc = mk_class_instance_elaborator( env, ios, ctx, ngen.next(), optional(), use_local_insts, is_strict, - some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), cfg, nullptr); + some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), nullptr); meta = mc.first; cs.push_back(mc.second); } else { diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp index 2bf95e7367..bfc2e14fee 100644 --- a/src/library/tactic/congruence_tactic.cpp +++ b/src/library/tactic/congruence_tactic.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/locals.h" #include "library/constants.h" #include "library/reducible.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/tactic/util.h" #include "library/tactic/intros_tactic.h" #include "library/tactic/subst_tactic.h" diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index fa997d4296..5694ca7219 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -13,7 +13,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/reducible.h" #include "library/locals.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/generalize_tactic.h" @@ -66,11 +66,10 @@ class induction_tac { bool use_local_insts = true; bool is_strict = false; local_context ctx = g.to_local_context(); - unifier_config cfg(m_ios.get_options()); auto mc = mk_class_instance_elaborator( m_env, m_ios, ctx, m_ngen.next(), optional(), use_local_insts, is_strict, - some_expr(type), m_ref.get_tag(), cfg, nullptr); + some_expr(type), m_ref.get_tag(), nullptr); m_cs += mc.second; return mc.first; } diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index a0ad8cbb57..bc290c2f3f 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/constants.h" #include "library/reducible.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/inversion_tactic.h" diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 82fb5a4935..101d48e6d9 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -32,7 +32,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/unfold_macros.h" #include "library/generic_exception.h" -#include "library/class_instance_synth.h" +#include "library/class_instance_resolution.h" #include "library/num.h" #include "library/tactic/clear_tactic.h" #include "library/tactic/trace_tactic.h" @@ -1040,13 +1040,11 @@ class rewrite_fn { } pair mk_class_instance_elaborator(expr const & type) { - unifier_config cfg; - cfg.m_kind = unifier_kind::VeryConservative; bool use_local_instances = true; bool is_strict = false; return ::lean::mk_class_instance_elaborator(m_env, m_ios, m_ctx, m_ngen.next(), optional(), use_local_instances, is_strict, - some_expr(type), m_expr_loc.get_tag(), cfg, nullptr); + some_expr(type), m_expr_loc.get_tag(), nullptr); } // target, new_target, H : represents the rewrite (H : target = new_target) for hypothesis