From e4fd627ae22ba82339952d4e7b71b6f4bf1f6d8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Aug 2016 08:20:37 -0700 Subject: [PATCH] feat(library/attribute_manager): fingerprints The fingerprint changes whenever a new attribute is added. --- library/init/meta/attribute.lean | 1 + src/library/attribute_manager.cpp | 48 ++++++++++++++++++++++++------- src/library/attribute_manager.h | 2 ++ src/library/reducible.cpp | 4 +++ src/library/vm/user_attribute.cpp | 11 +++++++ tests/lean/run/fingerprint.lean | 36 +++++++++++++++++++++++ 6 files changed, 91 insertions(+), 11 deletions(-) create mode 100644 tests/lean/run/fingerprint.lean diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean index a60a0289dc..e4ac433442 100644 --- a/library/init/meta/attribute.lean +++ b/library/init/meta/attribute.lean @@ -7,6 +7,7 @@ prelude import init.meta.tactic meta_constant attribute.get_instances : name → tactic (list name) +meta_constant attribute.fingerprint : name → tactic nat structure user_attribute := (descr : string) diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 414b686f0e..4cfbb3299d 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -92,21 +92,32 @@ struct attr_entry { }; typedef priority_queue attr_records; -typedef name_map attr_state; +typedef name_map> attr_state; struct attr_config { typedef attr_state state; typedef attr_entry entry; + + static unsigned get_entry_hash(entry const & e) { + return hash(hash(e.m_attr.hash(), e.m_record.hash()), e.m_prio); + } + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { attr_records m; - if (auto q = s.find(e.m_attr)) - m = *q; + unsigned h = 0; + if (auto q = s.find(e.m_attr)) { + m = q->first; + h = q->second; + } m.insert(e.m_record, e.m_prio); - s.insert(e.m_attr, m); + h = hash(h, get_entry_hash(e)); + s.insert(e.m_attr, mk_pair(m, h)); } + static std::string const & get_serialization_key() { return *g_key; } + static void write_entry(serializer & s, entry const & e) { s << e.m_attr << e.m_prio << e.m_record.m_decl; lean_assert(e.m_record.m_data); @@ -116,6 +127,7 @@ struct attr_config { // dispatch over the extension, since we can't call get_attribute without an env g_user_attribute_ext->write_entry(s, *e.m_record.m_data); } + static entry read_entry(deserializer & d) { entry e; d >> e.m_attr >> e.m_prio >> e.m_record.m_decl; @@ -126,8 +138,9 @@ struct attr_config { e.m_record.m_data = g_user_attribute_ext->read_entry(d); return e; } + static optional get_fingerprint(entry const & e) { - return optional(hash(hash(e.m_attr.hash(), e.m_record.hash()), e.m_prio)); + return optional(get_entry_hash(e)); } }; @@ -139,22 +152,35 @@ environment attribute::set_core(environment const & env, io_state const & ios, n return attribute_ext::add_entry(env, ios, attr_entry(m_id, prio, attr_record(n, data)), persistent); } attr_data_ptr attribute::get_untyped(environment const & env, name const & n) const { - if (auto records = attribute_ext::get_state(env).find(m_id)) - if (auto record = records->get_key({n, {}})) + if (auto p = attribute_ext::get_state(env).find(m_id)) { + attr_records const & records = p->first; + if (auto record = records.get_key({n, {}})) return record->m_data; + } return {}; } unsigned attribute::get_prio(environment const & env, name const & n) const { - if (auto records = attribute_ext::get_state(env).find(get_name())) - if (auto prio = records->get_prio({n, {}})) + if (auto p = attribute_ext::get_state(env).find(get_name())) { + attr_records const & records = p->first; + if (auto prio = records.get_prio({n, {}})) return prio.value(); + } return LEAN_DEFAULT_PRIORITY; } void attribute::get_instances(environment const & env, buffer & r) const { - if (auto records = attribute_ext::get_state(env).find(m_id)) - records->for_each([&](attr_record const & rec) { r.push_back(rec.m_decl); }); + if (auto p = attribute_ext::get_state(env).find(m_id)) { + attr_records const & records = p->first; + records.for_each([&](attr_record const & rec) { r.push_back(rec.m_decl); }); + } +} + +unsigned attribute::get_fingerprint(environment const & env) const { + if (auto p = attribute_ext::get_state(env).find(m_id)) { + return p->second; + } + return 0; } priority_queue attribute::get_instances_by_prio(environment const & env) const { diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index fd399fe4ad..db44ea7367 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -56,6 +56,8 @@ public: virtual void get_instances(environment const &, buffer &) const; priority_queue get_instances_by_prio(environment const &) const; virtual attr_data_ptr parse_data(abstract_parser &) const; + + virtual unsigned get_fingerprint(environment const & env) const; }; typedef std::shared_ptr attribute_ptr; diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index bfcd8ff196..27ad06b041 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -68,6 +68,10 @@ public: if (is_instance(env, n)) r.push_back(n); } + + virtual unsigned get_fingerprint(environment const & env) const { + return get_reducibility_attribute().get_fingerprint(env); + } }; void initialize_reducible() { diff --git a/src/library/vm/user_attribute.cpp b/src/library/vm/user_attribute.cpp index b309d7e13d..033a22ae87 100644 --- a/src/library/vm/user_attribute.cpp +++ b/src/library/vm/user_attribute.cpp @@ -104,9 +104,20 @@ static vm_obj attribute_register(vm_obj const & vm_n, vm_obj const & vm_s) { LEAN_TACTIC_CATCH(s); } +static vm_obj attribute_fingerprint(vm_obj const & vm_n, vm_obj const & vm_s) { + auto const & s = to_tactic_state(vm_s); + auto const & n = to_name(vm_n); + unsigned h; + LEAN_TACTIC_TRY; + h = get_attribute(s.env(), n).get_fingerprint(s.env()); + LEAN_TACTIC_CATCH(s); + return mk_tactic_success(mk_vm_nat(h), s); +} + void initialize_user_attribute() { DECLARE_VM_BUILTIN(name({"attribute", "get_instances"}), attribute_get_instances); DECLARE_VM_BUILTIN(name({"attribute", "register"}), attribute_register); + DECLARE_VM_BUILTIN(name({"attribute", "fingerprint"}), attribute_fingerprint); g_ext = new user_attr_ext_reg(); g_key = new std::string("USR_ATTR"); diff --git a/tests/lean/run/fingerprint.lean b/tests/lean/run/fingerprint.lean new file mode 100644 index 0000000000..5f0e9c41f3 --- /dev/null +++ b/tests/lean/run/fingerprint.lean @@ -0,0 +1,36 @@ +open tactic + +run_command attribute.fingerprint `reducible >>= trace + +definition ex0 : nat := +by attribute.fingerprint `reducible >>= expr_of_nat >>= exact + +attribute [reducible] +definition f : nat := 10 + +run_command attribute.fingerprint `reducible >>= trace + +definition ex1 : nat := +by attribute.fingerprint `reducible >>= expr_of_nat >>= exact + +vm_eval ex1 + +definition g : nat := 20 + +run_command attribute.fingerprint `reducible >>= trace + +definition ex2 : nat := +by attribute.fingerprint `reducible >>= expr_of_nat >>= exact + +vm_eval ex2 + +example : ex1 = ex2 := +rfl + +definition h : nat := 20 + +definition ex3 : nat := +by attribute.fingerprint `reducible >>= expr_of_nat >>= exact + +example : ex1 = ex3 := +rfl