feat(library/init/meta): add native name_set

library/init/meta/attribute.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 prelude
-import init.meta.tactic
+import init.meta.tactic init.meta.rb_map init.meta.quote
 
 meta constant attribute.get_instances : name → tactic (list name)
 meta constant attribute.fingerprint : name → tactic nat
@@ -22,3 +22,14 @@ meta structure caching_user_attribute (α : Type) extends user_attribute :=
 (dependencies : list _root_.name)
 
 meta constant caching_user_attribute.get_cache : Π {α : Type}, caching_user_attribute α → tactic α
+
+open tactic
+
+meta def mk_name_set_attr (attr_name : name) : command :=
+do t ← to_expr ``(caching_user_attribute name_set),
+   v ← to_expr ``({name     := %%(quote attr_name),
+                   descr    := "name_set attribute",
+                   mk_cache := name_set.of_list,
+                   dependencies := [] } : caching_user_attribute name_set),
+   add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
+   attribute.register attr_name

library/init/meta/rb_map.lean

@@ -142,6 +142,11 @@ meta def rb_set (key) := rb_map key unit
 meta def mk_rb_set {key} [has_ordering key] : rb_set key :=
 mk_rb_map
 
+open format
+
+private meta def format_key {key} [has_to_format key] (k : key) (first : bool) : format :=
+(if first then to_fmt "" else to_fmt "," ++ line) ++ to_fmt k
+
 namespace rb_set
 meta def insert {key} (s : rb_set key) (k : key) : rb_set key :=
 s^.insert k ()
@@ -161,19 +166,28 @@ s^.fold a (λ k _ a, fn k a)
 meta def to_list {key : Type} (s : rb_set key) : list key :=
 s^.fold [] list.cons
 
-open format
-
-private meta def format_key {key} [has_to_format key] (k : key) (first : bool) : format :=
-(if first then to_fmt "" else to_fmt "," ++ line) ++ to_fmt k
-
 meta instance {key} [has_to_format key] : has_to_format (rb_set key) :=
 ⟨λ m, group $ to_fmt "{" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ k p, (fst p ++ format_key k (snd p), ff)))) ++
               to_fmt "}"⟩
 end rb_set
 
-@[reducible] meta def name_set := rb_set name
 @[reducible] meta def expr_set := rb_set expr
-meta def mk_name_set : name_set := mk_rb_set
 meta def mk_expr_set : expr_set := mk_rb_set
 
-vm_eval to_fmt $ (mk_name_set^.insert `a)^.insert `b
+meta constant name_set : Type
+meta constant mk_name_set : name_set
+
+namespace name_set
+meta constant insert         : name_set → name → name_set
+meta constant erase          : name_set → name → name_set
+meta constant contains       : name_set → name → bool
+meta constant size           : name_set → nat
+meta constant fold {α :Type} : name_set → α → (name → α → α) → α
+
+meta instance : has_to_format name_set :=
+⟨λ m, group $ to_fmt "{" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ k p, (fst p ++ format_key k (snd p), ff)))) ++
+              to_fmt "}"⟩
+
+meta def of_list (l : list name) : name_set :=
+list.foldl name_set.insert mk_name_set l
+end name_set

src/library/vm/vm_rb_map.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/rb_map.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
+#include "library/vm/vm_name.h"
 #include "library/vm/vm_option.h"
 #include "library/vm/vm_ordering.h"
 
@@ -130,6 +131,56 @@ vm_obj rb_map_fold(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const
     return r;
 }
 
+struct vm_name_set : public vm_external {
+    name_set m_val;
+    vm_name_set(name_set const & v):m_val(v) {}
+    virtual ~vm_name_set() {}
+    virtual void dealloc() override { this->~vm_name_set(); get_vm_allocator().deallocate(sizeof(vm_name_set), this); }
+    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_name_set(m_val); }
+    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_name_set))) vm_name_set(m_val); }
+};
+
+bool is_name_set(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_name_set*>(to_external(o));
+}
+
+name_set const & to_name_set(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_name_set*>(to_external(o)));
+    return static_cast<vm_name_set*>(to_external(o))->m_val;
+}
+
+vm_obj to_obj(name_set const & n) {
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_name_set))) vm_name_set(n));
+}
+
+vm_obj mk_name_set() {
+    return to_obj(name_set());
+}
+
+vm_obj name_set_size(vm_obj const & m) {
+    return mk_vm_nat(to_name_set(m).size());
+}
+
+vm_obj name_set_insert(vm_obj const & m, vm_obj const & k) {
+    return to_obj(insert(to_name_set(m), to_name(k)));
+}
+
+vm_obj name_set_erase(vm_obj const & m, vm_obj const & k) {
+    return to_obj(erase(to_name_set(m), to_name(k)));
+}
+
+vm_obj name_set_contains(vm_obj const & m, vm_obj const & k) {
+    return mk_vm_bool(to_name_set(m).contains(to_name(k)));
+}
+
+vm_obj name_set_fold(vm_obj const &, vm_obj const & m, vm_obj const & a, vm_obj const & fn) {
+    vm_obj r = a;
+    to_name_set(m).for_each([&](name const & k) {
+            r = invoke(fn, to_obj(k), r);
+        });
+    return r;
+}
+
 void initialize_vm_rb_map() {
     DECLARE_VM_BUILTIN(name({"rb_map", "mk_core"}),        rb_map_mk_core);
     DECLARE_VM_BUILTIN(name({"rb_map", "size"}),           rb_map_size);
@@ -140,6 +191,13 @@ void initialize_vm_rb_map() {
     DECLARE_VM_BUILTIN(name({"rb_map", "min"}),            rb_map_min);
     DECLARE_VM_BUILTIN(name({"rb_map", "max"}),            rb_map_max);
     DECLARE_VM_BUILTIN(name({"rb_map", "fold"}),           rb_map_fold);
+
+    DECLARE_VM_BUILTIN(name({"mk_name_set"}),              mk_name_set);
+    DECLARE_VM_BUILTIN(name({"name_set", "size"}),         name_set_size);
+    DECLARE_VM_BUILTIN(name({"name_set", "insert"}),       name_set_insert);
+    DECLARE_VM_BUILTIN(name({"name_set", "erase"}),        name_set_erase);
+    DECLARE_VM_BUILTIN(name({"name_set", "contains"}),     name_set_contains);
+    DECLARE_VM_BUILTIN(name({"name_set", "fold"}),         name_set_fold);
 }
 
 void finalize_vm_rb_map() {