chore(*): remove unification hints
This commit is contained in:
Leonardo de Moura
parent
10ddfdafbd
commit
ce0467638e
16 changed files with 10 additions and 554 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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") {
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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<unification_hint> & 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,
|
||||
|
|
|
|||
|
|
@ -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<declaration> 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<unification_hint> & hints) = 0;
|
||||
|
||||
/* Cache support for type_context_old module */
|
||||
|
||||
|
|
@ -298,7 +296,6 @@ public:
|
|||
virtual optional<declaration> 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<unification_hint> & hints) override;
|
||||
|
||||
/* Cache support for type_context_old module */
|
||||
|
||||
|
|
|
|||
|
|
@ -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<unification_hint> & hints) {
|
||||
if (!m_uhints)
|
||||
m_uhints = ::lean::get_unification_hints(ctx.env());
|
||||
::lean::get_unification_hints(*m_uhints, f1, f2, hints);
|
||||
}
|
||||
|
||||
template<typename R, typename C, typename K>
|
||||
optional<R> find_at(C const & c, K const & e) {
|
||||
auto it = c.find(e);
|
||||
|
|
|
|||
|
|
@ -89,8 +89,6 @@ class context_cache : public context_cacheless {
|
|||
instance_cache m_instance_cache;
|
||||
subsingleton_cache m_subsingleton_cache;
|
||||
|
||||
optional<unification_hints> m_uhints;
|
||||
|
||||
/* Cache datastructures for fun_info */
|
||||
|
||||
typedef expr_map<fun_info> fi_cache;
|
||||
|
|
@ -118,7 +116,6 @@ public:
|
|||
virtual optional<declaration> 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<unification_hint> & hints) override;
|
||||
|
||||
/* Cache support for type_context_old module */
|
||||
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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<unification_hint> & hints) {
|
||||
return m_cache_ptr->get_unification_hints(ctx, f1, f2, hints);
|
||||
}
|
||||
|
||||
optional<expr> persistent_context_cache::get_infer(expr const & e) {
|
||||
return m_cache_ptr->get_infer(e);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -46,7 +46,6 @@ public:
|
|||
virtual optional<declaration> 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<unification_hint> & hints) override;
|
||||
|
||||
/* Cache support for type_context_old module */
|
||||
|
||||
|
|
|
|||
|
|
@ -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<bool> 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<unification_hint> 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"}));
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<pair<expr, expr>> 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<unsigned> to_small_num(expr const & e);
|
||||
|
|
|
|||
|
|
@ -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 <string>
|
||||
#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<expr_pair> 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<unsigned> 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<expr> 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<expr_pair> 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<unsigned> get_fingerprint(entry const & e) {
|
||||
return some(hash(e.m_decl_name.hash(), e.m_priority));
|
||||
}
|
||||
};
|
||||
|
||||
typedef scoped_ext<unification_hint_config> 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<unification_hint> & 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<unification_hint> & 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<optional<expr>> m_assignment;
|
||||
|
||||
expr apply_assignment(expr const & e) {
|
||||
return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
|
||||
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<expr> 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<unsigned> 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<expr_pair> 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();
|
||||
}
|
||||
}
|
||||
|
|
@ -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<expr_pair> m_constraints;
|
||||
unsigned m_num_vars;
|
||||
public:
|
||||
expr get_lhs() const { return m_lhs; }
|
||||
expr get_rhs() const { return m_rhs; }
|
||||
list<expr_pair> 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<expr_pair> 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, unification_hint_cmp> unification_hint_queue;
|
||||
typedef rb_map<name_pair, unification_hint_queue, name_pair_quick_cmp> 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<unification_hint> & uhints);
|
||||
|
||||
void get_unification_hints(environment const & env, name const & n1, name const & n2, buffer<unification_hint> & 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();
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue