feat(library/attribute_manager): fingerprints

The fingerprint changes whenever a new attribute is added.

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)

src/library/attribute_manager.cpp

@@ -92,21 +92,32 @@ struct attr_entry {
 };
 
 typedef priority_queue<attr_record, attr_record_cmp> attr_records;
-typedef name_map<attr_records> attr_state;
+typedef name_map<pair<attr_records, unsigned>> 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<unsigned> get_fingerprint(entry const & e) {
-        return optional<unsigned>(hash(hash(e.m_attr.hash(), e.m_record.hash()), e.m_prio));
+        return optional<unsigned>(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<name> & 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<name, name_quick_cmp> attribute::get_instances_by_prio(environment const & env) const {

src/library/attribute_manager.h

@@ -56,6 +56,8 @@ public:
     virtual void get_instances(environment const &, buffer<name> &) const;
     priority_queue<name, name_quick_cmp> 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 const> attribute_ptr;

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() {

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");

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