diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean index 55f1ce6968..37fbb2c27c 100644 --- a/library/init/meta/attribute.lean +++ b/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 diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean index bbf6e073a7..020ee40fcc 100644 --- a/library/init/meta/rb_map.lean +++ b/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 diff --git a/src/library/vm/vm_rb_map.cpp b/src/library/vm/vm_rb_map.cpp index b8c18f3059..91376cbb68 100644 --- a/src/library/vm/vm_rb_map.cpp +++ b/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(to_external(o)); +} + +name_set const & to_name_set(vm_obj const & o) { + lean_vm_check(dynamic_cast(to_external(o))); + return static_cast(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() {