From ce0467638e40d7f0cfef0f1c8dfa6ca9596d32ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Apr 2018 16:29:04 -0700 Subject: [PATCH] chore(*): remove unification hints --- library/init/core.lean | 15 - library/init/data/nat/lemmas.lean | 8 +- src/frontends/lean/print_cmd.cpp | 7 - src/library/CMakeLists.txt | 6 +- src/library/abstract_context_cache.cpp | 4 - src/library/abstract_context_cache.h | 3 - src/library/context_cache.cpp | 6 - src/library/context_cache.h | 3 - src/library/eval_helper.cpp | 1 + src/library/init_module.cpp | 3 - src/library/persistent_context_cache.cpp | 4 - src/library/persistent_context_cache.h | 1 - src/library/type_context.cpp | 35 --- src/library/type_context.h | 16 +- src/library/unification_hint.cpp | 380 ----------------------- src/library/unification_hint.h | 72 ----- 16 files changed, 10 insertions(+), 554 deletions(-) delete mode 100644 src/library/unification_hint.cpp delete mode 100644 src/library/unification_hint.h diff --git a/library/init/core.lean b/library/init/core.lean index 63cd26c9f7..a1c1528c58 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -297,16 +297,6 @@ inductive nat | zero : nat | succ (n : nat) : nat -structure unification_constraint := -{α : Type u} (lhs : α) (rhs : α) - -infix ` ≟ `:50 := unification_constraint.mk -infix ` =?= `:50 := unification_constraint.mk - -structure unification_hint := -(pattern : unification_constraint) -(constraints : list unification_constraint) - /- Declare builtin and reserved notation -/ class has_zero (α : Type u) := (zero : α) @@ -560,10 +550,5 @@ inductive bin_tree (α : Type u) attribute [elab_simple] bin_tree.node bin_tree.leaf -/- Basic unification hints -/ -@[unify] def add_succ_defeq_succ_add_hint (x y z : nat) : unification_hint := -{ pattern := x + nat.succ y ≟ nat.succ z, - constraints := [z ≟ x + y] } - /-- Like `by apply_instance`, but not dependent on the tactic framework. -/ @[reducible] def infer_instance {α : Type u} [i : α] : α := i diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 3e5ec52600..df7b7637d4 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -17,7 +17,7 @@ protected lemma add_comm : ∀ n m : ℕ, n + m = m + n protected lemma add_assoc : ∀ n m k : ℕ, (n + m) + k = n + (m + k) | n m 0 := rfl -| n m (succ k) := by rw [add_succ, add_succ, add_assoc] +| n m (succ k) := by rw [add_succ, add_succ, add_succ, add_assoc] protected lemma add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k) := left_comm nat.add nat.add_comm nat.add_assoc @@ -959,7 +959,11 @@ protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 := let t := add_div_right 0 H in by rwa [nat.zero_add, nat.zero_div] at t theorem add_mul_div_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) / y = x / y + z := -by {induction z with z ih, simp [nat.mul_zero, nat.add_zero], rw [mul_succ, ← nat.add_assoc, nat.add_div_right _ H, ih]} +begin + induction z with z ih, + { simp [nat.mul_zero, nat.add_zero] }, + { rw [mul_succ, ← nat.add_assoc, nat.add_div_right _ H, ih, add_succ] } +end theorem add_mul_div_right (x y : ℕ) {z : ℕ} (H : z > 0) : (x + y * z) / z = x / z + y := by rw [nat.mul_comm, add_mul_div_left _ _ H] diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index ddabc4e21e..e847229e44 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -23,7 +23,6 @@ Author: Leonardo de Moura #include "library/user_recursors.h" #include "library/noncomputable.h" #include "library/type_context.h" -#include "library/unification_hint.h" #include "library/reducible.h" #include "library/tactic/simp_lemmas.h" #include "library/tactic/kabstract.h" @@ -450,10 +449,6 @@ void print_polymorphic(parser & p, message_builder & out) { print_id_info(p, out, id, show_value, pos); } -static void print_unification_hints(parser & p, message_builder & out) { - out << pp_unification_hints(get_unification_hints(p.env()), out.get_formatter()); -} - static void print_simp_rules(parser & p, message_builder & out) { name attr = p.check_id_next("invalid '#print [simp]' command, identifier expected"); simp_lemmas slss = get_simp_lemmas(p.env(), attr); @@ -603,8 +598,6 @@ environment print_cmd(parser & p) { if (name == "recursor") { print_recursor_info(p, out); - } else if (name == "unify") { - print_unification_hints(p, out); } else if (name == "simp") { print_simp_rules(p, out); } else if (name == "congr") { diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 1a7cb51c38..79aa8bf148 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -10,15 +10,13 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp unfold_macros.cpp app_builder.cpp projection.cpp relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp aux_recursors.cpp trace.cpp - attribute_manager.cpp unification_hint.cpp - local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp + attribute_manager.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp replace_visitor_with_tc.cpp aux_definition.cpp inverse.cpp pattern_attribute.cpp choice.cpp locals.cpp normalize.cpp discr_tree.cpp mt_task_queue.cpp st_task_queue.cpp library_task_builder.cpp - eval_helper.cpp - messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp + eval_helper.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp context_cache.cpp unique_id.cpp persistent_context_cache.cpp elab_context.cpp) diff --git a/src/library/abstract_context_cache.cpp b/src/library/abstract_context_cache.cpp index 24ba38941a..2d49a04c45 100644 --- a/src/library/abstract_context_cache.cpp +++ b/src/library/abstract_context_cache.cpp @@ -109,10 +109,6 @@ bool context_cacheless::get_aux_recursor(type_context_old & ctx, name const & n) return ::lean::is_aux_recursor(ctx.env(), n); } -void context_cacheless::get_unification_hints(type_context_old & ctx, name const & f1, name const & f2, buffer & hints) { - return ::lean::get_unification_hints(ctx.env(), f1, f2, hints); -} - void initialize_abstract_context_cache() { g_class_instance_max_depth = new name{"class", "instance_max_depth"}; register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h index f0d89376d0..ce5b726bdf 100644 --- a/src/library/abstract_context_cache.h +++ b/src/library/abstract_context_cache.h @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/projection.h" #include "library/fun_info.h" #include "library/local_instances.h" -#include "library/unification_hint.h" namespace lean { #define LEAN_NUM_TRANSPARENCY_MODES 5 @@ -182,7 +181,6 @@ public: virtual optional get_decl(type_context_old &, transparency_mode, name const &) = 0; virtual projection_info const * get_proj_info(type_context_old &, name const &) = 0; virtual bool get_aux_recursor(type_context_old &, name const &) = 0; - virtual void get_unification_hints(type_context_old &, name const & f1, name const & f2, buffer & hints) = 0; /* Cache support for type_context_old module */ @@ -298,7 +296,6 @@ public: virtual optional get_decl(type_context_old &, transparency_mode, name const &) override; virtual projection_info const * get_proj_info(type_context_old &, name const &) override; virtual bool get_aux_recursor(type_context_old &, name const &) override; - virtual void get_unification_hints(type_context_old &, name const & f1, name const & f2, buffer & hints) override; /* Cache support for type_context_old module */ diff --git a/src/library/context_cache.cpp b/src/library/context_cache.cpp index 57efae6115..ec39a4d3c1 100644 --- a/src/library/context_cache.cpp +++ b/src/library/context_cache.cpp @@ -44,12 +44,6 @@ bool context_cache::get_aux_recursor(type_context_old & ctx, name const & n) { return r; } -void context_cache::get_unification_hints(type_context_old & ctx, name const & f1, name const & f2, buffer & hints) { - if (!m_uhints) - m_uhints = ::lean::get_unification_hints(ctx.env()); - ::lean::get_unification_hints(*m_uhints, f1, f2, hints); -} - template optional find_at(C const & c, K const & e) { auto it = c.find(e); diff --git a/src/library/context_cache.h b/src/library/context_cache.h index bf06ebb47c..74427c20ed 100644 --- a/src/library/context_cache.h +++ b/src/library/context_cache.h @@ -89,8 +89,6 @@ class context_cache : public context_cacheless { instance_cache m_instance_cache; subsingleton_cache m_subsingleton_cache; - optional m_uhints; - /* Cache datastructures for fun_info */ typedef expr_map fi_cache; @@ -118,7 +116,6 @@ public: virtual optional get_decl(type_context_old &, transparency_mode, name const &) override; virtual projection_info const * get_proj_info(type_context_old &, name const &) override; virtual bool get_aux_recursor(type_context_old &, name const &) override; - virtual void get_unification_hints(type_context_old &, name const & f1, name const & f2, buffer & hints) override; /* Cache support for type_context_old module */ diff --git a/src/library/eval_helper.cpp b/src/library/eval_helper.cpp index b493d8c000..3671af3745 100644 --- a/src/library/eval_helper.cpp +++ b/src/library/eval_helper.cpp @@ -7,6 +7,7 @@ Author: Gabriel Ebner #include "kernel/instantiate.h" #include "library/util.h" #include "library/eval_helper.h" +#include "library/io_state.h" #include "library/tactic/tactic_state.h" namespace lean { diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 4b28e16f9b..b7c5d044d0 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -39,7 +39,6 @@ Author: Leonardo de Moura #include "library/local_context.h" #include "library/metavar_context.h" #include "library/attribute_manager.h" -#include "library/unification_hint.h" #include "library/delayed_abstraction.h" #include "library/app_builder.h" #include "library/fun_info.h" @@ -106,7 +105,6 @@ void initialize_library_module() { initialize_aux_recursors(); initialize_app_builder(); initialize_fun_info(); - initialize_unification_hint(); initialize_abstract_context_cache(); initialize_type_context(); initialize_delayed_abstraction(); @@ -134,7 +132,6 @@ void finalize_library_module() { finalize_delayed_abstraction(); finalize_type_context(); finalize_abstract_context_cache(); - finalize_unification_hint(); finalize_fun_info(); finalize_app_builder(); finalize_aux_recursors(); diff --git a/src/library/persistent_context_cache.cpp b/src/library/persistent_context_cache.cpp index ae68c5de26..cbb0d9ee28 100644 --- a/src/library/persistent_context_cache.cpp +++ b/src/library/persistent_context_cache.cpp @@ -63,10 +63,6 @@ bool persistent_context_cache::get_aux_recursor(type_context_old & ctx, name con return m_cache_ptr->get_aux_recursor(ctx, n); } -void persistent_context_cache::get_unification_hints(type_context_old & ctx, name const & f1, name const & f2, buffer & hints) { - return m_cache_ptr->get_unification_hints(ctx, f1, f2, hints); -} - optional persistent_context_cache::get_infer(expr const & e) { return m_cache_ptr->get_infer(e); } diff --git a/src/library/persistent_context_cache.h b/src/library/persistent_context_cache.h index 813128188d..c38fdee387 100644 --- a/src/library/persistent_context_cache.h +++ b/src/library/persistent_context_cache.h @@ -46,7 +46,6 @@ public: virtual optional get_decl(type_context_old &, transparency_mode, name const &) override; virtual projection_info const * get_proj_info(type_context_old &, name const &) override; virtual bool get_aux_recursor(type_context_old &, name const &) override; - virtual void get_unification_hints(type_context_old &, name const & f1, name const & f2, buffer & hints) override; /* Cache support for type_context_old module */ diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 116e09bda7..df69123e74 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -27,7 +27,6 @@ Author: Leonardo de Moura #include "library/locals.h" #include "library/aux_recursors.h" #include "library/attribute_manager.h" -#include "library/unification_hint.h" #include "library/delayed_abstraction.h" #include "library/fun_info.h" #include "library/num.h" @@ -3241,8 +3240,6 @@ bool type_context_old::is_def_eq_core_core(expr t, expr s) { s = s_n; } - if (try_unification_hints(t, s)) return l_true; - r = try_nat_offset_cnstrs(t, s); if (r != l_undef) return r == l_true; @@ -3323,37 +3320,6 @@ bool type_context_old::relaxed_is_def_eq(expr const & e1, expr const & e2) { return is_def_eq(e1, e2); } -bool type_context_old::try_unification_hint(unification_hint const & hint, expr const & e1, expr const & e2) { - scope S(*this); - flet disable_smart_unfolding(m_smart_unfolding, false); - if (::lean::try_unification_hint(*this, hint, e1, e2) && process_postponed(S)) { - S.commit(); - return true; - } else { - return false; - } -} - -bool type_context_old::try_unification_hints(expr const & e1, expr const & e2) { - expr e1_fn = get_app_fn(e1); - expr e2_fn = get_app_fn(e2); - if (is_constant(e1_fn) && is_constant(e2_fn)) { - buffer hints; - m_cache->get_unification_hints(*this, const_name(e1_fn), const_name(e2_fn), hints); - for (unification_hint const & hint : hints) { - lean_trace(name({"type_context", "unification_hint"}), - scope_trace_env scope(env(), *this); - tout() << e1 << " =?= " << e2 - << ", pattern: " << hint.get_lhs() << " =?= " << hint.get_rhs() << "\n";); - if (try_unification_hint(hint, e1, e2) || - try_unification_hint(hint, e2, e1)) { - return true; - } - } - } - return false; -} - /* ------------- Type classes ------------- */ @@ -4212,7 +4178,6 @@ mk_pp_ctx(type_context_old const & ctx) { void initialize_type_context() { register_trace_class("class_instances"); - register_trace_class(name({"type_context", "unification_hint"})); register_trace_class(name({"type_context", "is_def_eq"})); register_trace_class(name({"type_context", "is_def_eq_detail"})); register_trace_class(name({"type_context", "univ_is_def_eq"})); diff --git a/src/library/type_context.h b/src/library/type_context.h index 954cffc7bb..6fe1784ad0 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -17,7 +17,7 @@ Author: Leonardo de Moura #include "library/metavar_context.h" #include "library/abstract_context_cache.h" #include "library/exception.h" -#include "library/unification_hint.h" +#include "library/expr_pair.h" namespace lean { /* Return `f._sunfold` */ @@ -351,17 +351,6 @@ public: only fresh new temporary metavariables. So, no offsets are needed since we don't use pre-allocated temporary metavars. Thus, we use `(tmp-unify) lctx | t =?= s` where `lctx` is the local context for `?m`. - - - (Internal) Unification hints. For versions <= 3.3, we used a - custom and very basic matching procedure to implement - this feature. This created several stability problems - and counterintuitive behavior. We use temporary - metavariables and matching. - We also use `(nested-tmp-match) lctx | (k, t) =?= s`. - This case is very similar to the previous one. - - Remark: only the two last applications require offsets. Moreover, `k` is `0` if - the `type_context_old` is not already in TMP mode. */ /* This class supports temporary meta-variables "mode". In this "tmp" mode, @@ -967,13 +956,10 @@ private: bool is_def_eq_proof_irrel(expr const & e1, expr const & e2); optional elim_delayed_abstraction(expr const & e); lbool quick_is_def_eq(expr const & e1, expr const & e2); - bool try_unification_hint(unification_hint const & h, expr const & e1, expr const & e2); - bool try_unification_hints(expr const & e1, expr const & e2); lbool is_def_eq_delta(expr const & t, expr const & s); lbool is_def_eq_proj(expr t, expr s); optional> find_unsynth_metavar(expr const & e); bool mk_nested_instance(expr const & m, expr const & m_type); - friend class unification_hint_fn; /* Support for solving offset constraints, see issue #1226 */ optional to_small_num(expr const & e); diff --git a/src/library/unification_hint.cpp b/src/library/unification_hint.cpp deleted file mode 100644 index 32c3d26592..0000000000 --- a/src/library/unification_hint.cpp +++ /dev/null @@ -1,380 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Daniel Selsam, Leonardo de Moura -*/ -#include -#include "util/sexpr/format.h" -#include "kernel/expr.h" -#include "kernel/instantiate.h" -#include "kernel/replace_fn.h" -#include "kernel/error_msgs.h" -#include "library/attribute_manager.h" -#include "library/constants.h" -#include "library/unification_hint.h" -#include "library/util.h" -#include "library/trace.h" -#include "library/expr_lt.h" -#include "library/scoped_ext.h" -#include "library/fun_info.h" -#include "library/annotation.h" -#include "library/type_context.h" - -namespace lean { -unification_hint::unification_hint(expr const & lhs, expr const & rhs, list const & constraints, unsigned num_vars): - m_lhs(lhs), m_rhs(rhs), m_constraints(constraints), m_num_vars(num_vars) {} - -int unification_hint_cmp::operator()(unification_hint const & uh1, unification_hint const & uh2) const { - if (uh1.get_lhs() != uh2.get_lhs()) { - return expr_quick_cmp()(uh1.get_lhs(), uh2.get_lhs()); - } else if (uh1.get_rhs() != uh2.get_rhs()) { - return expr_quick_cmp()(uh1.get_rhs(), uh2.get_rhs()); - } else { - auto it1 = uh1.get_constraints().begin(); - auto it2 = uh2.get_constraints().begin(); - auto end1 = uh1.get_constraints().end(); - auto end2 = uh2.get_constraints().end(); - for (; it1 != end1 && it2 != end2; ++it1, ++it2) { - if (unsigned cmp = expr_pair_quick_cmp()(*it1, *it2)) return cmp; - } - return 0; - } -} - -struct unification_hint_state { - unification_hints m_hints; - name_map m_decl_names_to_prio; // Note: redundant but convenient - - void validate_type(expr const & decl_type) { - expr type = decl_type; - while (is_pi(type)) type = binding_body(type); - if (!is_app_of(type, get_unification_hint_name(), 0)) { - throw exception("invalid unification hint, must return element of type `unification hint`"); - } - } - - void register_hint(environment const & env, name const & decl_name, expr const & value, unsigned priority) { - m_decl_names_to_prio.insert(decl_name, priority); - type_context_old _ctx(env, options(), transparency_mode::All); - tmp_type_context ctx(_ctx); - expr e_hint = value; - unsigned num_vars = 0; - buffer tmp_mvars; - while (is_lambda(e_hint)) { - expr d = instantiate_rev(binding_domain(e_hint), tmp_mvars.size(), tmp_mvars.data()); - tmp_mvars.push_back(ctx.mk_tmp_mvar(d)); - e_hint = binding_body(e_hint); - num_vars++; - } - - if (!is_app_of(e_hint, get_unification_hint_mk_name(), 2)) { - throw exception("invalid unification hint, body must be application of 'unification_hint.mk' to two arguments"); - } - - // e_hint := unification_hint.mk pattern constraints - expr e_pattern = app_arg(app_fn(e_hint)); - expr e_constraints = app_arg(e_hint); - - // pattern := unification_constraint.mk _ lhs rhs - expr e_pattern_lhs = app_arg(app_fn(e_pattern)); - expr e_pattern_rhs = app_arg(e_pattern); - - expr e_pattern_lhs_fn = get_app_fn(e_pattern_lhs); - expr e_pattern_rhs_fn = get_app_fn(e_pattern_rhs); - - if (!is_constant(e_pattern_lhs_fn) || !is_constant(e_pattern_rhs_fn)) { - throw exception("invalid unification hint, the heads of both sides of pattern must be constants"); - } - - if (quick_cmp(const_name(e_pattern_lhs_fn), const_name(e_pattern_rhs_fn)) > 0) { - swap(e_pattern_lhs_fn, e_pattern_rhs_fn); - swap(e_pattern_lhs, e_pattern_rhs); - } - - name_pair key = mk_pair(const_name(e_pattern_lhs_fn), const_name(e_pattern_rhs_fn)); - - buffer constraints; - unsigned eqidx = 1; - while (is_app_of(e_constraints, get_list_cons_name(), 3)) { - // e_constraints := cons _ constraint rest - expr e_constraint = app_arg(app_fn(e_constraints)); - expr e_constraint_lhs = app_arg(app_fn(e_constraint)); - expr e_constraint_rhs = app_arg(e_constraint); - constraints.push_back(mk_pair(e_constraint_lhs, e_constraint_rhs)); - e_constraints = app_arg(e_constraints); - - if (!ctx.is_def_eq(instantiate_rev(e_constraint_lhs, tmp_mvars.size(), tmp_mvars.data()), - instantiate_rev(e_constraint_rhs, tmp_mvars.size(), tmp_mvars.data()))) { - throw exception(sstream() << "invalid unification hint, failed to unify constraint #" << eqidx); - } - eqidx++; - } - - if (!is_app_of(e_constraints, get_list_nil_name(), 1)) { - throw exception("invalid unification hint, must provide list of constraints explicitly"); - } - - if (!ctx.is_def_eq(instantiate_rev(e_pattern_lhs, tmp_mvars.size(), tmp_mvars.data()), - instantiate_rev(e_pattern_rhs, tmp_mvars.size(), tmp_mvars.data()))) { - throw exception("invalid unification hint, failed to unify pattern after unifying constraints"); - } - - unification_hint hint(e_pattern_lhs, e_pattern_rhs, to_list(constraints), num_vars); - unification_hint_queue q; - if (auto const & q_ptr = m_hints.find(key)) q = *q_ptr; - q.insert(hint, priority); - m_hints.insert(key, q); - } -}; - -struct unification_hint_entry { - name m_decl_name; - unsigned m_priority; - unification_hint_entry(name const & decl_name, unsigned priority): - m_decl_name(decl_name), m_priority(priority) {} -}; - -struct unification_hint_config { - typedef unification_hint_entry entry; - typedef unification_hint_state state; - - static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { - declaration decl = env.get(e.m_decl_name); - s.validate_type(decl.get_type()); - s.register_hint(env, e.m_decl_name, decl.get_value(), e.m_priority); - } - static const char * get_serialization_key() { return "UNIFICATION_HINT"; } - static void write_entry(serializer & s, entry const & e) { - s << e.m_decl_name << e.m_priority; - } - static entry read_entry(deserializer & d) { - name decl_name; unsigned prio; - d >> decl_name >> prio; - return entry(decl_name, prio); - } - static optional get_fingerprint(entry const & e) { - return some(hash(e.m_decl_name.hash(), e.m_priority)); - } -}; - -typedef scoped_ext unification_hint_ext; - -environment add_unification_hint(environment const & env, io_state const & ios, name const & decl_name, unsigned prio, - bool persistent) { - if (!env.get(decl_name).is_definition()) - throw exception(sstream() << "invalid unification hint, '" << decl_name << "' must be a definition"); - return unification_hint_ext::add_entry(env, ios, unification_hint_entry(decl_name, prio), persistent); -} - -unification_hints get_unification_hints(environment const & env) { - return unification_hint_ext::get_state(env).m_hints; -} - -void get_unification_hints(unification_hints const & hints, name const & n1, name const & n2, buffer & uhints) { - if (quick_cmp(n1, n2) > 0) { - if (auto const * q_ptr = hints.find(mk_pair(n2, n1))) - q_ptr->to_buffer(uhints); - } else { - if (auto const * q_ptr = hints.find(mk_pair(n1, n2))) - q_ptr->to_buffer(uhints); - } -} - -void get_unification_hints(environment const & env, name const & n1, name const & n2, buffer & uhints) { - unification_hints hints = unification_hint_ext::get_state(env).m_hints; - get_unification_hints(hints, n1, n2, uhints); -} - -/* Pretty-printing */ - -// TODO(dhs): I may not be using all the formatting functions correctly. -format unification_hint::pp(unsigned prio, formatter const & fmt) const { - format r; - if (prio != LEAN_DEFAULT_PRIORITY) - r += paren(format(prio)) + space(); - format r1 = fmt(get_lhs()) + space() + format("=?=") + pp_indent_expr(fmt, get_rhs()); - r1 += space() + lcurly(); - r += group(r1); - bool first = true; - for (expr_pair const & p : m_constraints) { - if (first) { - first = false; - } else { - r += comma() + space(); - } - r += fmt(p.first) + space() + format("=?=") + space() + fmt(p.second); - } - r += rcurly(); - return r; -} - -format pp_unification_hints(unification_hints const & hints, formatter const & fmt) { - format r; - r += format("unification hints") + colon() + line(); - hints.for_each([&](name_pair const & names, unification_hint_queue const & q) { - q.for_each([&](unification_hint const & hint) { - r += lp() + format(names.first) + comma() + space() + format(names.second) + rp() + space(); - r += hint.pp(*q.get_prio(hint), fmt) + line(); - }); - }); - return r; -} - -class unification_hint_fn { - type_context_old & m_owner; - unification_hint const & m_hint; - buffer> m_assignment; - - expr apply_assignment(expr const & e) { - return replace(e, [=](expr const & m, unsigned offset) -> optional { - if (offset >= get_free_var_range(m)) - return some_expr(m); // expression m does not contain free variables with idx >= s1 - if (is_var(m)) { - unsigned vidx = var_idx(m); - if (vidx >= offset) { - unsigned h = offset + m_assignment.size(); - if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) { - if (auto v = m_assignment[vidx - offset]) - return some_expr(*v); - } - return some_expr(m); - } - } - return none_expr(); - }); - } - - bool match_app(expr const & p, expr const & e) { - buffer p_args, e_args; - expr const & p_fn = get_app_args(p, p_args); - expr const & e_fn = get_app_args(e, e_args); - if (p_args.size() != e_args.size()) - return false; - fun_info finfo = get_fun_info(m_owner, e_fn, e_args.size()); - unsigned i = 0; - buffer postponed; - for (param_info const & pinfo : finfo.get_params_info()) { - if (!pinfo.is_implicit() && !pinfo.is_inst_implicit()) { - if (!match(p_args[i], e_args[i])) { - return false; - } - } else { - postponed.push_back(i); - } - i++; - } - for (; i < p_args.size(); i++) { - if (!match(p_args[i], e_args[i])) { - return false; - } - } - if (!match(p_fn, e_fn)) - return false; - for (unsigned i : postponed) { - expr new_p_arg = apply_assignment(p_args[i]); - if (closed(new_p_arg)) { - if (!m_owner.is_def_eq(new_p_arg, e_args[i])) { - return false; - } - } else { - if (!match(new_p_arg, e_args[i])) - return false; - } - } - return true; - } - - bool match(expr const & pattern, expr const & e) { - if (m_owner.is_mvar(e) && m_owner.is_assigned(e)) { - return match(pattern, m_owner.instantiate_mvars(e)); - } - if (is_annotation(e)) { - return match(pattern, get_annotation_arg(e)); - } - unsigned idx; - switch (pattern.kind()) { - case expr_kind::Var: - idx = var_idx(pattern); - if (!m_assignment[idx]) { - m_assignment[idx] = some_expr(e); - return true; - } else { - return m_owner.is_def_eq(*m_assignment[idx], e); - } - case expr_kind::Constant: - return - is_constant(e) && - const_name(pattern) == const_name(e) && - m_owner.is_def_eq(const_levels(pattern), const_levels(e)); - case expr_kind::Sort: - return is_sort(e) && m_owner.is_def_eq(sort_level(pattern), sort_level(e)); - case expr_kind::Pi: case expr_kind::Lambda: - case expr_kind::Macro: case expr_kind::Let: - // Remark: we do not traverse inside of binders. - return pattern == e; - case expr_kind::App: - return - is_app(e) && - match(app_fn(pattern), app_fn(e)) && - match(app_arg(pattern), app_arg(e)); - case expr_kind::Local: case expr_kind::Meta: - lean_unreachable(); - } - lean_unreachable(); - } - -public: - unification_hint_fn(type_context_old & o, unification_hint const & hint): - m_owner(o), m_hint(hint) { - m_assignment.resize(m_hint.get_num_vars()); - } - - bool operator()(expr const & lhs, expr const & rhs) { - if (!match(m_hint.get_lhs(), lhs)) { - lean_trace(name({"type_context", "unification_hint"}), tout() << "LHS does not match\n";); - return false; - } else if (!match(m_hint.get_rhs(), rhs)) { - lean_trace(name({"type_context", "unification_hint"}), tout() << "RHS does not match\n";); - return false; - } else { - auto instantiate_assignment_fn = [&](expr const & e, unsigned offset) { - if (is_var(e)) { - unsigned idx = var_idx(e) + offset; - if (idx < m_assignment.size() && m_assignment[idx]) - return m_assignment[idx]; - } - return none_expr(); - }; - buffer constraints; - to_buffer(m_hint.get_constraints(), constraints); - for (expr_pair const & p : constraints) { - expr new_lhs = replace(p.first, instantiate_assignment_fn); - expr new_rhs = replace(p.second, instantiate_assignment_fn); - bool success = m_owner.is_def_eq(new_lhs, new_rhs); - lean_trace(name({"type_context", "unification_hint"}), - scope_trace_env scope(m_owner.env(), m_owner); - tout() << new_lhs << " =?= " << new_rhs << "..." - << (success ? "success" : "failed") << "\n";); - if (!success) return false; - } - lean_trace(name({"type_context", "unification_hint"}), - tout() << "hint successfully applied\n";); - return true; - } - } -}; - -bool try_unification_hint(type_context_old & o, unification_hint const & hint, expr const & lhs, expr const & rhs) { - return unification_hint_fn(o, hint)(lhs, rhs); -} - -void initialize_unification_hint() { - unification_hint_ext::initialize(); - - register_system_attribute(basic_attribute("unify", "unification hint", add_unification_hint)); -} - -void finalize_unification_hint() { - unification_hint_ext::finalize(); -} -} diff --git a/src/library/unification_hint.h b/src/library/unification_hint.h deleted file mode 100644 index 59a94150d3..0000000000 --- a/src/library/unification_hint.h +++ /dev/null @@ -1,72 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#pragma once -#include "kernel/environment.h" -#include "library/expr_pair.h" -#include "library/io_state.h" -#include "library/head_map.h" -#include "util/priority_queue.h" - -namespace lean { - -/* -Users can declare unification hints using the following structures: - -structure unification_constraint := {A : Type} (lhs : A) (rhs : A) -structure unification_hint := (pattern : unification_constraint) (constraints : list unification_constraint) - -Example: - -definition both_zero_of_add_eq_zero [unify] (n₁ n₂ : ℕ) (s₁ : has_add ℕ) (s₂ : has_zero ℕ) : unification_hint := - unification_hint.mk (unification_constraint.mk (@has_add.add ℕ s₁ n₁ n₂) (@has_zero.zero ℕ s₂)) - [unification_constraint.mk n₁ (@has_zero.zero ℕ s₂), - unification_constraint.mk n₂ (@has_zero.zero ℕ s₂)] - -creates the following unification hint: -m_lhs: add nat #1 #3 #2 -m_rhs: zero nat #0 -m_constraints: [(#3, zero nat #0), (#2, zero nat #0)] -m_num_vars: #4 - -Note that once we have an assignment to all variables from matching, we must substitute the assignments in the constraints. -*/ -class unification_hint { - expr m_lhs; - expr m_rhs; - - list m_constraints; - unsigned m_num_vars; -public: - expr get_lhs() const { return m_lhs; } - expr get_rhs() const { return m_rhs; } - list get_constraints() const { return m_constraints; } - unsigned get_num_vars() const { return m_num_vars; } - - unification_hint() {} - unification_hint(expr const & lhs, expr const & rhs, list const & constraints, unsigned num_vars); - format pp(unsigned priority, formatter const & fmt) const; -}; - -struct unification_hint_cmp { - int operator()(unification_hint const & uh1, unification_hint const & uh2) const; -}; - -typedef priority_queue unification_hint_queue; -typedef rb_map unification_hints; - -unification_hints get_unification_hints(environment const & env); -void get_unification_hints(unification_hints const & hints, name const & n1, name const & n2, buffer & uhints); - -void get_unification_hints(environment const & env, name const & n1, name const & n2, buffer & hints); - -format pp_unification_hints(unification_hints const & hints, formatter const & fmt); - -class type_context_old; -bool try_unification_hint(type_context_old & o, unification_hint const & hint, expr const & lhs, expr const & rhs); - -void initialize_unification_hint(); -void finalize_unification_hint(); -}