diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index 5b4b8ff61..4b00a294b 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -195,17 +195,10 @@ optional mk_hset_instance(type_checker & tc, io_state const & ios, list mk_subsingleton_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type) { +optional mk_subsingleton_instance(environment const & env, io_state const & ios, list const & ctx, expr const & type) { cienv & cenv = get_cienv(); - cenv.ensure_compatible(tc.env(), ios, ctx); - flet set(cenv.m_ti_ptr->get_ignore_if_zero(), true); - 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 cenv.m_ti_ptr->mk_class_instance(subsingleton); + cenv.ensure_compatible(env, ios, ctx); + return cenv.m_ti_ptr->mk_subsingleton_instance(type); } void initialize_class_instance_resolution() { diff --git a/src/library/class_instance_resolution.h b/src/library/class_instance_resolution.h index 4455ce1a0..c74a39a06 100644 --- a/src/library/class_instance_resolution.h +++ b/src/library/class_instance_resolution.h @@ -38,7 +38,7 @@ pair mk_class_instance_elaborator( 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); +optional mk_subsingleton_instance(environment const & env, 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/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp index bfc2e14fe..53c1bc7c2 100644 --- a/src/library/tactic/congruence_tactic.cpp +++ b/src/library/tactic/congruence_tactic.cpp @@ -50,7 +50,7 @@ optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios if (prop.back()) { ss.push_back(true); } else { - ss.push_back(static_cast(mk_subsingleton_instance(tc, ios, ctx, mlocal_type(d)))); + ss.push_back(static_cast(mk_subsingleton_instance(tc.env(), ios, ctx, mlocal_type(d)))); } codomain_deps_on.push_back(depends_on(codomain, d)); ctx = cons(d, ctx); @@ -145,7 +145,7 @@ optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios return none_expr(); buffer hyps; g.get_hyps(hyps); - auto spr = mk_subsingleton_instance(tc, ios, to_list(hyps), mlocal_type(new_lhs)); + auto spr = mk_subsingleton_instance(tc.env(), ios, to_list(hyps), mlocal_type(new_lhs)); if (!spr) return none_expr(); expr new_eq = mk_local(get_unused_name(name(h, eqidx), hyps), mk_eq(tc, new_rhs, new_lhs)); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index fd37bf929..4c573d658 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/generic_exception.h" #include "library/class.h" +#include "library/constants.h" #ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES #define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false @@ -1610,6 +1611,19 @@ optional type_context::mk_class_instance(expr const & type) { return r; } +optional type_context::mk_subsingleton_instance(expr const & type) { + expr Type = whnf(infer(type)); + if (!is_sort(Type)) + return none_expr(); + level lvl = sort_level(Type); + expr subsingleton; + if (is_standard(m_env)) + subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type); + else + subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)); + return mk_class_instance(subsingleton); +} + optional type_context::next_class_instance() { if (!m_ci_multiple_instances) return none_expr(); @@ -1751,6 +1765,11 @@ expr default_type_context::mk_mvar(expr const & type) { return mk_metavar(name(*g_prefix, idx), type); } +optional default_type_context::mk_subsingleton_instance(expr const & type) { + flet set(m_ignore_if_zero, true); + return type_context::mk_subsingleton_instance(type); +} + bool default_type_context::ignore_universe_def_eq(level const & l1, level const & l2) const { if (is_meta(l1) || is_meta(l2)) { // The unifier may invoke this module before universe metavariables in the class diff --git a/src/library/type_context.h b/src/library/type_context.h index 70e631693..177c5b037 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -409,6 +409,10 @@ public: /** \brief Try to synthesize an instance of the type class \c type */ optional mk_class_instance(expr const & type); optional next_class_instance(); + /** \brief Try to synthesize an instance of (subsingleton type) + \remark This method is virtual because we need a refinement + at default_type_context to workaround an integration problem with the elaborator. */ + virtual optional mk_subsingleton_instance(expr const & type); /** \brief Given \c ma of the form ?m t_1 ... t_n, (try to) assign ?m to (an abstraction of) v. Return true if success and false otherwise. @@ -511,6 +515,8 @@ public: virtual void push() { m_trail.push_back(m_assignment); } virtual void pop() { lean_assert(!m_trail.empty()); m_assignment = m_trail.back(); m_trail.pop_back(); } virtual void commit() { lean_assert(!m_trail.empty()); m_trail.pop_back(); } + virtual optional mk_subsingleton_instance(expr const & type); + // TODO(REMOVE) bool & get_ignore_if_zero() { return m_ignore_if_zero; } };