From 71fc35af1ddf6b131eca2835dec8a48172896d07 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Jun 2018 17:32:27 -0700 Subject: [PATCH] chore(library/vm): remove meta rb_map We should use the non-meta rbmap that is implemented in Lean. --- library/init/meta/default.lean | 2 +- library/init/meta/environment.lean | 5 - library/init/meta/expr.lean | 17 +- library/init/meta/interactive.lean | 10 - library/init/meta/rb_map.lean | 209 ----------------- src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 3 - src/library/vm/vm_environment.cpp | 6 - src/library/vm/vm_expr.cpp | 1 - src/library/vm/vm_rb_map.cpp | 217 ------------------ src/library/vm/vm_rb_map.h | 16 -- tests/lean/run/display_hw_term_hack_deps.lean | 2 + 12 files changed, 6 insertions(+), 484 deletions(-) delete mode 100644 library/init/meta/rb_map.lean delete mode 100644 src/library/vm/vm_rb_map.cpp delete mode 100644 src/library/vm/vm_rb_map.h diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 191cb170af..523e0d085c 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.meta.name init.meta.options init.meta.format init.meta.rb_map +import init.meta.name init.meta.options init.meta.format import init.meta.level init.meta.expr init.meta.environment import init.meta.tactic init.meta.interactive diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index 3b6c40ecb3..27de72da24 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -5,7 +5,6 @@ Authors: Leonardo de Moura -/ prelude import init.meta.declaration init.meta.exceptional init.data.option.basic -import init.meta.rb_map meta constant environment : Type @@ -85,10 +84,6 @@ meta constant decl_olean : environment → name → option string meta constant decl_pos : environment → name → option pos /-- Return the fields of the structure with the given name, or `none` if it is not a structure -/ meta constant structure_fields : environment → name → option (list name) -/-- `get_class_attribute_symbols env attr_name` return symbols - occurring in instances of type classes tagged with the attribute `attr_name`. - Example: [algebra] -/ -meta constant get_class_attribute_symbols : environment → name → name_set meta constant fingerprint : environment → nat open expr diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index cc7e094d77..83ade5de52 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.meta.level init.control.monad init.meta.rb_map +import init.meta.level init.control.monad universes u v -open native + structure pos := (line : nat) (column : nat) @@ -346,16 +346,3 @@ meta def mfold {α : Type} {m : Type → Type} [monad m] (e : expr) (a : α) (fn fold e (return a) (λ e n a, a >>= fn e n) end expr - -@[reducible] meta def expr_map (data : Type) := rb_map expr data -namespace expr_map -export native.rb_map (hiding mk) - -meta def mk (data : Type) : expr_map data := rb_map.mk expr data -end expr_map - -meta def mk_expr_map {data : Type} : expr_map data := -expr_map.mk data - -@[reducible] meta def expr_set := rb_set expr -meta def mk_expr_set : expr_set := mk_rb_set diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index eab236a7ea..6bb7f7db19 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -262,16 +262,6 @@ match p.to_expr with precedence `generalizing` : 0 -private meta def collect_hyps_uids : tactic name_set := -do ctx ← local_context, - return $ ctx.foldl (λ r h, r.insert h.fvar_id) mk_name_set - -private meta def revert_new_hyps (input_hyp_uids : name_set) : tactic unit := -do ctx ← local_context, - let to_revert := ctx.foldr (λ h r, if input_hyp_uids.contains h.fvar_id then r else h::r) [], - m ← revert_lst to_revert, - return () - private meta def get_type_name (e : expr) : tactic name := do e_type ← infer_type e >>= whnf, (const I ls) ← return $ get_app_fn e_type, diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean deleted file mode 100644 index 67806fe58f..0000000000 --- a/library/init/meta/rb_map.lean +++ /dev/null @@ -1,209 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Jeremy Avigad --/ -prelude -import init.data.ordering.basic init.function init.meta.name init.meta.format init.control.monad - -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 native -meta constant {u₁ u₂} rb_map : Type u₁ → Type u₂ → Type (max u₁ u₂) - -namespace rb_map -meta constant mk_core {key : Type} (data : Type) : (key → key → ordering) → rb_map key data -meta constant size {key : Type} {data : Type} : rb_map key data → nat -meta constant empty {key : Type} {data : Type} : rb_map key data → bool -meta constant insert {key : Type} {data : Type} : rb_map key data → key → data → rb_map key data -meta constant erase {key : Type} {data : Type} : rb_map key data → key → rb_map key data -meta constant contains {key : Type} {data : Type} : rb_map key data → key → bool -meta constant find {key : Type} {data : Type} : rb_map key data → key → option data -meta constant min {key : Type} {data : Type} : rb_map key data → option data -meta constant max {key : Type} {data : Type} : rb_map key data → option data -meta constant fold {key : Type} {data : Type} {α :Type} : rb_map key data → α → (key → data → α → α) → α - -attribute [inline] -meta def mk (key : Type) [has_lt key] [decidable_rel ((<) : key → key → Prop)] (data : Type) : rb_map key data := -mk_core data cmp - -open list - -section -variables {key data : Type} - -meta def keys (m : rb_map key data) : list key := -fold m [] (λk v ks, k :: ks) - -meta def values {key : Type} {data : Type} (m : rb_map key data) : list data := -fold m [] (λk v vs, v :: vs) - -meta def to_list {key : Type} {data : Type} (m : rb_map key data) : list (key × data) := -fold m [] (λk v res, (k, v) :: res) - -meta def mfold {key data α :Type} {m : Type → Type} [monad m] (mp : rb_map key data) (a : α) (fn : key → data → α → m α) : m α := -mp.fold (return a) (λ k d act, act >>= fn k d) -end - -section - -variables {key data data' : Type} [has_lt key] [decidable_rel ((<) : key → key → Prop)] - -meta def of_list : list (key × data) → rb_map key data -| [] := mk key data -| ((k, v)::ls) := insert (of_list ls) k v - - -meta def set_of_list : list key → rb_map key unit -| [] := mk _ _ -| (x::xs) := insert (set_of_list xs) x () - -meta def map (f : data → data') (m : rb_map key data) : rb_map key data' := -fold m (mk _ _) (λk v res, insert res k (f v)) - -meta def for (m : rb_map key data) (f : data → data') : rb_map key data' := -map f m - -meta def filter (m : rb_map key data) (f : data → Prop) [decidable_pred f] := -fold m (mk _ _) $ λa b m', if f b then insert m' a b else m' - -end - -end rb_map - -meta def mk_rb_map {key data : Type} [has_lt key] [decidable_rel ((<) : key → key → Prop)] : rb_map key data := -rb_map.mk key data - -@[reducible] meta def nat_map (data : Type) := rb_map nat data -namespace nat_map -export rb_map (hiding mk) - -meta def mk (data : Type) : nat_map data := rb_map.mk nat data -end nat_map - -meta def mk_nat_map {data : Type} : nat_map data := -nat_map.mk data - -open rb_map prod -section -variables {key : Type} {data : Type} [has_to_format key] [has_to_format data] -private meta def format_key_data (k : key) (d : data) (first : bool) : format := -(if first then to_fmt "" else to_fmt "," ++ line) ++ to_fmt k ++ space ++ to_fmt "←" ++ space ++ to_fmt d - -meta instance : has_to_format (rb_map key data) := -⟨λ m, group $ to_fmt "⟨" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ k d p, (fst p ++ format_key_data k d (snd p), ff)))) ++ - to_fmt "⟩"⟩ -end - -section -variables {key : Type} {data : Type} [has_to_string key] [has_to_string data] -private meta def key_data_to_string (k : key) (d : data) (first : bool) : string := -(if first then "" else ", ") ++ to_string k ++ " ← " ++ to_string d - -meta instance : has_to_string (rb_map key data) := -⟨λ m, "⟨" ++ (fst (fold m ("", tt) (λ k d p, (fst p ++ key_data_to_string k d (snd p), ff)))) ++ "⟩"⟩ -end - -/-- a variant of rb_maps that stores a list of elements for each key. - `find` returns the list of elements in the opposite order that they were inserted. -/ -meta def rb_lmap (key : Type) (data : Type) : Type := rb_map key (list data) - -namespace rb_lmap - -protected meta def mk (key : Type) [has_lt key] [decidable_rel ((<) : key → key → Prop)] (data : Type) : rb_lmap key data := -rb_map.mk key (list data) - -meta def insert {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) (d : data) : - rb_lmap key data := -match (rb_map.find rbl k) with -| none := rb_map.insert rbl k [d] -| (some l) := rb_map.insert (rb_map.erase rbl k) k (d :: l) - -meta def erase {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) : - rb_lmap key data := -rb_map.erase rbl k - -meta def contains {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) : bool := -rb_map.contains rbl k - -meta def find {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) : list data := -match (rb_map.find rbl k) with -| none := [] -| (some l) := l - -end rb_lmap - -meta def rb_set (key) := rb_map key unit -meta def mk_rb_set {key} [has_lt key] [decidable_rel ((<) : key → key → Prop)] : rb_set key := -mk_rb_map - -namespace rb_set -meta def insert {key} (s : rb_set key) (k : key) : rb_set key := -rb_map.insert s k () - -meta def erase {key} (s : rb_set key) (k : key) : rb_set key := -rb_map.erase s k - -meta def contains {key} (s : rb_set key) (k : key) : bool := -rb_map.contains s k - -meta def size {key} (s : rb_set key) : nat := -rb_map.size s - -meta def empty {key : Type} (s : rb_set key) : bool := -rb_map.empty s - -meta def fold {key α : Type} (s : rb_set key) (a : α) (fn : key → α → α) : α := -rb_map.fold s a (λ k _ a, fn k a) - -meta def mfold {key α :Type} {m : Type → Type} [monad m] (s : rb_set key) (a : α) (fn : key → α → m α) : m α := -s.fold (return a) (λ k act, act >>= fn k) - -meta def to_list {key : Type} (s : rb_set key) : list key := -s.fold [] list.cons - -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 -end native - -open native -@[reducible] meta def name_map (data : Type) := rb_map name data -namespace name_map -export native.rb_map (hiding mk) - -meta def mk (data : Type) : name_map data := rb_map.mk_core data name.cmp -end name_map - -meta def mk_name_map {data : Type} : name_map data := -name_map.mk data - -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 empty : name_set → bool -meta constant fold {α :Type} : name_set → α → (name → α → α) → α - -meta def to_list (s : name_set) : list name := -s.fold [] list.cons - -meta instance : has_to_format name_set := -⟨λ m, group $ to_fmt "{" ++ nest 1 (fold m (to_fmt "", tt) (λ k p, (p.1 ++ format_key k p.2, ff))).1 ++ - to_fmt "}"⟩ - -meta def of_list (l : list name) : name_set := -list.foldl name_set.insert mk_name_set l - -meta def mfold {α :Type} {m : Type → Type} [monad m] (ns : name_set) (a : α) (fn : name → α → m α) : m α := -ns.fold (return a) (λ k act, act >>= fn k) - -end name_set diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 9a44162e4f..5860983903 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp - vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp + vm_options.cpp vm_format.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 2e0d8a53aa..9c88cb9473 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/vm/vm_name.h" #include "library/vm/vm_options.h" #include "library/vm/vm_format.h" -#include "library/vm/vm_rb_map.h" #include "library/vm/vm_level.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_pexpr.h" @@ -35,7 +34,6 @@ void initialize_vm_core_module() { initialize_vm_name(); initialize_vm_options(); initialize_vm_format(); - initialize_vm_rb_map(); initialize_vm_level(); initialize_vm_expr(); initialize_vm_pexpr(); @@ -61,7 +59,6 @@ void finalize_vm_core_module() { finalize_vm_pexpr(); finalize_vm_expr(); finalize_vm_level(); - finalize_vm_rb_map(); finalize_vm_format(); finalize_vm_options(); finalize_vm_name(); diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 3ebb279507..48ecba5824 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -26,7 +26,6 @@ Author: Leonardo de Moura #include "library/vm/vm_exceptional.h" #include "library/vm/vm_list.h" #include "library/vm/vm_pos_info.h" -#include "library/vm/vm_rb_map.h" #include "frontends/lean/structure_cmd.h" namespace lean { @@ -256,10 +255,6 @@ vm_obj environment_unfold_all_macros(vm_obj const & env, vm_obj const & e) { return to_obj(unfold_all_macros(to_env(env), to_expr(e))); } -vm_obj environment_get_class_attribute_symbols(vm_obj const & env, vm_obj const & n) { - return to_obj(get_class_attribute_symbols(to_env(env), to_name(n))); -} - vm_obj environment_fingerprint(vm_obj const & env) { return mk_vm_nat(mpz(get_fingerprint(to_env(env)))); } @@ -294,7 +289,6 @@ void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "unfold_untrusted_macros"}), environment_unfold_untrusted_macros); DECLARE_VM_BUILTIN(name({"environment", "unfold_all_macros"}), environment_unfold_all_macros); DECLARE_VM_BUILTIN(name({"environment", "structure_fields"}), environment_structure_fields); - DECLARE_VM_BUILTIN(name({"environment", "get_class_attribute_symbols"}), environment_get_class_attribute_symbols); DECLARE_VM_BUILTIN(name({"environment", "fingerprint"}), environment_fingerprint); } diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 49fa96bb75..b15f5113ba 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -31,7 +31,6 @@ Author: Leonardo de Moura #include "library/vm/vm_list.h" #include "library/vm/vm_string.h" #include "library/vm/vm_pos_info.h" -#include "library/vm/vm_rb_map.h" #include "library/compiler/simp_inductive.h" #include "library/compiler/nat_value.h" diff --git a/src/library/vm/vm_rb_map.cpp b/src/library/vm/vm_rb_map.cpp deleted file mode 100644 index 9c1d8d9553..0000000000 --- a/src/library/vm/vm_rb_map.cpp +++ /dev/null @@ -1,217 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#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" - -namespace lean { -struct vm_obj_cmp { - vm_obj m_cmp; - int operator()(vm_obj const & o1, vm_obj const & o2) const { - return ordering_to_int(invoke(m_cmp, o1, o2)); - } - vm_obj_cmp() {} - explicit vm_obj_cmp(vm_obj const & cmp):m_cmp(cmp) {} -}; - -typedef rb_map vm_obj_map; - -struct vm_rb_map : public vm_external { - vm_obj_map m_map; - vm_rb_map(vm_obj_map const & m):m_map(m) {} - virtual ~vm_rb_map() {} - virtual void dealloc() override { delete this; } - virtual vm_external * ts_clone(vm_clone_fn const &) override; - virtual vm_external * clone(vm_clone_fn const &) override { lean_unreachable(); } -}; - -/* Auxiliary object used by vm_rb_map::ts_clone. - This is the "thread safe" version used when creating a ts_vm_obj that contains - a nested vm_rb_map. */ -struct vm_rb_map_ts_copy : public vm_external { - vm_obj m_cmp; - std::vector> m_entries; - virtual ~vm_rb_map_ts_copy() { - /* The object ts_vm_obj manages the life cycle of all vm_obj's. - We should prevent this destructor from invoking the destructor of m_cmp and the - vm_obj's nested in m_entries. */ - m_cmp.steal_ptr(); - for (auto & p : m_entries) { - if (p.first.is_ptr()) - p.first.steal_ptr(); - if (p.second.is_ptr()) - p.second.steal_ptr(); - } - } - virtual void dealloc() override { lean_unreachable(); } - virtual vm_external * ts_clone(vm_clone_fn const &) override { lean_unreachable(); } - virtual vm_external * clone(vm_clone_fn const &) override; -}; - -vm_external * vm_rb_map::ts_clone(vm_clone_fn const & fn) { - vm_rb_map_ts_copy * r = new vm_rb_map_ts_copy(); - r->m_cmp = fn(m_map.get_cmp().m_cmp); - m_map.for_each([&](vm_obj const & k, vm_obj const & v) { - r->m_entries.emplace_back(fn(k), fn(v)); - }); - return r; -} - -vm_external * vm_rb_map_ts_copy::clone(vm_clone_fn const & fn) { - vm_obj new_cmp = fn(m_cmp); - vm_obj_map new_map = vm_obj_map(vm_obj_cmp(new_cmp)); - for (auto const & p : m_entries) { - new_map.insert(fn(p.first), fn(p.second)); - } - return new vm_rb_map(new_map); -} - -vm_obj_map const & to_map(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_map; -} - -vm_obj to_obj(vm_rb_map const & n) { - return mk_vm_external(new vm_rb_map(n)); -} - -vm_obj rb_map_mk_core(vm_obj const &, vm_obj const &, vm_obj const & cmp) { - return to_obj(vm_obj_map(vm_obj_cmp(cmp))); -} - -vm_obj rb_map_size(vm_obj const &, vm_obj const &, vm_obj const & m) { - return mk_vm_nat(to_map(m).size()); -} - -vm_obj rb_map_empty(vm_obj const &, vm_obj const &, vm_obj const & m) { - return mk_vm_bool(to_map(m).empty()); -} - -vm_obj rb_map_insert(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k, vm_obj const & d) { - return to_obj(insert(to_map(m), k, d)); -} - -vm_obj rb_map_erase(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k) { - return to_obj(erase(to_map(m), k)); -} - -vm_obj rb_map_contains(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k) { - return mk_vm_bool(to_map(m).contains(k)); -} - -vm_obj rb_map_find(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k) { - if (auto d = to_map(m).find(k)) - return mk_vm_some(*d); - else - return mk_vm_none(); -} - -vm_obj rb_map_min(vm_obj const &, vm_obj const &, vm_obj const & m) { - if (to_map(m).empty()) - return mk_vm_none(); - else - return mk_vm_some(to_map(m).min()); -} - -vm_obj rb_map_max(vm_obj const &, vm_obj const &, vm_obj const & m) { - if (to_map(m).empty()) - return mk_vm_none(); - else - return mk_vm_some(to_map(m).max()); -} - -vm_obj rb_map_fold(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & a, vm_obj const & fn) { - vm_obj r = a; - to_map(m).for_each([&](vm_obj const & k, vm_obj const & d) { - r = invoke(fn, k, d, r); - }); - 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 { delete 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 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 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_empty(vm_obj const & m) { - return mk_vm_bool(to_name_set(m).empty()); -} - -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({"native", "rb_map", "mk_core"}), rb_map_mk_core); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "size"}), rb_map_size); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "empty"}), rb_map_empty); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "insert"}), rb_map_insert); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "erase"}), rb_map_erase); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "contains"}), rb_map_contains); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "find"}), rb_map_find); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "min"}), rb_map_min); - DECLARE_VM_BUILTIN(name({"native", "rb_map", "max"}), rb_map_max); - DECLARE_VM_BUILTIN(name({"native", "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", "empty"}), name_set_empty); - 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() { -} -} diff --git a/src/library/vm/vm_rb_map.h b/src/library/vm/vm_rb_map.h deleted file mode 100644 index 66bf23cfe3..0000000000 --- a/src/library/vm/vm_rb_map.h +++ /dev/null @@ -1,16 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once - -namespace lean { -bool is_name_set(vm_obj const & o); -name_set const & to_name_set(vm_obj const & o); -vm_obj to_obj(name_set const & n); - -void initialize_vm_rb_map(); -void finalize_vm_rb_map(); -} diff --git a/tests/lean/run/display_hw_term_hack_deps.lean b/tests/lean/run/display_hw_term_hack_deps.lean index 9f0da6f740..117f6da51a 100644 --- a/tests/lean/run/display_hw_term_hack_deps.lean +++ b/tests/lean/run/display_hw_term_hack_deps.lean @@ -8,6 +8,8 @@ meta def is_eqn_theorem : name → bool | (name.mk_string (name.mk_string "equations" _) _) := tt | _ := ff +#exit + meta def display_hw_term_hack_dependencies : tactic unit := do env ← get_env, env.fold (return mk_name_set) $ λ d tac, do {