diff --git a/src/library/class.cpp b/src/library/class.cpp index 34ac5e21de..fd959a554b 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -19,7 +19,7 @@ Author: Leonardo de Moura #include "library/attribute_manager.h" namespace lean { -enum class class_entry_kind { Class, Multi, Instance, TransInstance, DerivedTransInstance }; +enum class class_entry_kind { Class, Instance, TransInstance, DerivedTransInstance }; struct class_entry { class_entry_kind m_kind; name m_class; @@ -35,8 +35,6 @@ struct class_entry { class_entry(name const & src, name const & tgt, name const & i): m_kind(class_entry_kind::DerivedTransInstance), m_class(tgt), m_instance(i), m_priority(0), m_source(src) {} - class_entry(name const & c, bool): - m_kind(class_entry_kind::Multi), m_class(c) {} static class_entry mk_trans_inst(name const & src, name const & tgt, name const & i, unsigned p) { return class_entry(src, tgt, i, p); @@ -53,7 +51,6 @@ struct class_state { class_instances m_derived_trans_instances; instance_priorities m_priorities; name_set m_derived_trans_instance_set; - name_set m_multiple; // set of classes that allow multiple solutions/instances tc_multigraph m_mgraph; class_state():m_mgraph("transitive instance") {} @@ -73,10 +70,6 @@ struct class_state { return m_derived_trans_instance_set.contains(i); } - bool try_multiple_instances(name const & c) const { - return m_multiple.contains(c); - } - list insert(name const & inst, unsigned priority, list const & insts) const { if (!insts) return to_list(inst); @@ -119,11 +112,6 @@ struct class_state { m_derived_trans_instance_set.insert(i); m_mgraph.add1(env, src, i, tgt); } - - void add_multiple(name const & c) { - add_class(c); - m_multiple.insert(c); - } }; static name * g_class_name = nullptr; @@ -137,9 +125,6 @@ struct class_config { case class_entry_kind::Class: s.add_class(e.m_class); break; - case class_entry_kind::Multi: - s.add_multiple(e.m_class); - break; case class_entry_kind::Instance: s.add_instance(e.m_class, e.m_instance, e.m_priority); break; @@ -161,7 +146,6 @@ struct class_config { s << static_cast(e.m_kind); switch (e.m_kind) { case class_entry_kind::Class: - case class_entry_kind::Multi: s << e.m_class; break; case class_entry_kind::Instance: @@ -181,7 +165,6 @@ struct class_config { e.m_kind = static_cast(k); switch (e.m_kind) { case class_entry_kind::Class: - case class_entry_kind::Multi: d >> e.m_class; break; case class_entry_kind::Instance: @@ -199,7 +182,6 @@ struct class_config { static optional get_fingerprint(entry const & e) { switch (e.m_kind) { case class_entry_kind::Class: - case class_entry_kind::Multi: return some(e.m_class.hash()); case class_entry_kind::Instance: case class_entry_kind::TransInstance: @@ -325,16 +307,6 @@ environment add_trans_instance(environment const & env, name const & n, unsigned return new_env; } -environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent) { - check_class(env, n); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), ns, persistent); -} - -bool try_multiple_instances(environment const & env, name const & n) { - class_state const & s = class_ext::get_state(env); - return s.try_multiple_instances(n); -} - bool is_instance(environment const & env, name const & i) { class_state const & s = class_ext::get_state(env); return s.is_instance(i); @@ -484,12 +456,6 @@ void initialize_class() { }, is_class); - register_attribute("multiple_instances", "a type class where elaborator should consider multiple solutions", - [](environment const & env, io_state const &, name const & d, name const & ns, bool persistent) { - return mark_multiple_instances(env, d, ns, persistent); - }, - try_multiple_instances); - register_prio_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, name const & ns, bool persistent) { diff --git a/src/library/class.h b/src/library/class.h index 4661b0645d..5729b28b5b 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -33,11 +33,6 @@ list get_class_derived_trans_instances(environment const & env, name const void get_classes(environment const & env, buffer & classes); name get_class_name(environment const & env, expr const & e); -/** \brief Mark that multiple instances of class \c n must be explored. */ -environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent); -/** \brief Return true iff multiple instances of class \c n must be explored. */ -bool try_multiple_instances(environment const & env, name const & n); - /** \brief Return true iff \c type is a class or Pi that produces a class. */ optional is_ext_class(type_checker & tc, expr const & type); diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index 8c98b7f4aa..b25919d139 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -25,10 +25,6 @@ Author: Leonardo de Moura #include "library/choice_iterator.h" #include "library/type_context.h" #include "library/class_instance_resolution.h" -// The following include files are need by the old type class resolution procedure -#include "util/lazy_list_fn.h" -#include "library/unifier.h" -#include "library/metavar_closure.h" namespace lean { [[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); } @@ -86,47 +82,6 @@ optional mk_class_instance(environment const & env, list const & ctx return mk_class_instance(env, options(), ctx, e, pip); } -// Auxiliary class for generating a lazy-stream of instances. -class class_multi_instance_iterator : public choice_iterator { - io_state m_ios; - default_type_context m_ti; - type_context::scope_pos_info m_scope_pos_info; - expr m_new_meta; - justification m_new_j; - optional m_first; -public: - class_multi_instance_iterator(environment const & env, io_state const & ios, list const & ctx, - expr const & e, pos_info_provider const * pip, expr const & pos_ref, - expr const & new_meta, justification const & new_j, - bool is_strict): - choice_iterator(!is_strict), - m_ios(ios), - m_ti(env, ios.get_options(), ctx, true), - m_scope_pos_info(m_ti, pip, pos_ref), - m_new_meta(new_meta), - m_new_j(new_j) { - m_first = m_ti.mk_class_instance(e); - } - - virtual ~class_multi_instance_iterator() {} - - virtual optional next() { - optional r; - if (m_first) { - r = m_first; - m_first = none_expr(); - } else { - r = m_ti.next_class_instance(); - } - if (r) { - constraint c = mk_eq_cnstr(m_new_meta, *r, m_new_j); - return optional(constraints(c)); - } else { - return optional(); - } - } -}; - static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, old_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); @@ -141,23 +96,16 @@ static constraint mk_class_instance_root_cnstr(environment const & env, io_state // do nothing, since type is not a class. return lazy_list(constraints()); } - bool multiple_insts = try_multiple_instances(env, *cls_name); pair mj = update_meta(meta, s); expr new_meta = mj.first; justification new_j = mj.second; - if (multiple_insts) { - return choose(std::shared_ptr(new class_multi_instance_iterator(env, ios, ctx.get_data(), - meta_type, pip, meta, - new_meta, new_j, is_strict))); + if (auto r = mk_class_instance(env, ios.get_options(), ctx.get_data(), meta_type, pip, meta)) { + constraint c = mk_eq_cnstr(new_meta, *r, new_j); + return lazy_list(constraints(c)); + } else if (is_strict) { + return lazy_list(); } else { - if (auto r = mk_class_instance(env, ios.get_options(), ctx.get_data(), meta_type, pip, meta)) { - 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()); - } + return lazy_list(constraints()); } }; bool owner = false; @@ -212,369 +160,12 @@ void finalize_class_instance_resolution() { delete g_class_force_new; } -/* - The rest of this module implements the old more powerful and *expensive* type class - resolution procedure. We still have it because the HoTT library contains - type class instances that require full-higher order unification to be solved. - - Example: - - definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A} - (p : x = y) : (is_equiv (transport P p)) := ... -*/ - -static bool get_class_trace_instances(options const & o) { - return o.get_bool(name("trace", "class_instances"), false); -} - -/** \brief Context for handling class-instance metavariable choice constraint */ -struct class_instance_context { - io_state m_ios; - 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, - bool use_local_instances): - m_ios(ios), - 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 = true; // We removed the option class.conservative - m_trans_instances = get_class_trans_instances(ios.get_options()); - m_tc = mk_class_type_checker(env, 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, old_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; - old_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, old_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(), m_C->m_tc->get_type_context()); - 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(); - 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(mk_fresh_name(), 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(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)) { - 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(mk_fresh_name())); - 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, - old_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 &) { - 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, old_local_context const & ctx, - optional const & type, tag g, unsigned depth, bool use_globals) { - expr m = ctx.mk_meta(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, old_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) { - 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()); - } - old_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::Conservative : 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, 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 (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_old_class_instance_elaborator( - environment const & env, io_state const & ios, old_local_context const & ctx, - 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, use_local_instances); - expr m = ctx.mk_meta(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); -} - pair mk_class_instance_elaborator( environment const & env, io_state const & ios, old_local_context const & ctx, optional const & suffix, bool use_local_instances, bool is_strict, optional const & type, tag g, pos_info_provider const * pip) { - if (is_standard(env) || get_class_force_new(ios.get_options())) { - return mk_new_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances, - is_strict, type, g, pip); - } else { - unifier_config cfg(ios.get_options(), true /* use exceptions */, true /* discard */); - return mk_old_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances, - is_strict, type, g, cfg, pip); - } + return mk_new_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances, + is_strict, type, g, pip); } } diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean index 296c2d453c..b6880ba734 100644 --- a/tests/lean/run/div2.lean +++ b/tests/lean/run/div2.lean @@ -49,8 +49,6 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom → (rec_val : dom → (dom → codom) → codom) (x : dom) : codom := rec_measure_aux default measure rec_val (succ (measure x)) x -attribute decidable [multiple_instances] - theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ) (rec_val : dom → (dom → codom) → codom) (rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) → diff --git a/tests/lean/run/mult.lean b/tests/lean/run/mult.lean deleted file mode 100644 index 23e1544ec3..0000000000 --- a/tests/lean/run/mult.lean +++ /dev/null @@ -1,17 +0,0 @@ -structure C [class] := -(val : nat) - -attribute C [multiple_instances] - -definition c1 [instance] : C := C.mk 1 -definition c2 [instance] : C := C.mk 2 - -set_option trace.class_instances true - -definition f [s : C] : nat := C.val - -definition tst1 : f = 1 := -rfl - -definition tst2 : f = 2 := -rfl