From 3444a295e7c12f4ec60e07309ca39b6be048056f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Feb 2019 12:57:46 -0800 Subject: [PATCH] feat(library/compiler,runtime): builtin support for `lean.name` --- src/kernel/expr.cpp | 2 +- src/kernel/expr.h | 2 +- src/kernel/expr_sets.h | 2 +- src/kernel/level.cpp | 2 +- src/library/annotation.cpp | 3 ++- src/library/compiler/builtin.cpp | 7 +++++- src/library/compiler/csimp.cpp | 13 +++++------ src/library/compiler/elim_dead_let.cpp | 4 ++-- src/library/compiler/lambda_lifting.cpp | 2 +- src/library/compiler/llnf.cpp | 10 ++++---- src/library/compiler/util.cpp | 8 +++++-- src/library/compiler/util.h | 4 ++-- src/library/context_cache.h | 5 ++-- src/library/expr_pair.h | 2 +- src/library/module.cpp | 2 +- src/library/phash_map.h | 2 +- src/library/private.cpp | 2 +- src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 3 +++ src/library/vm/vm.cpp | 13 +++++++---- src/library/vm/vm_name.cpp | 25 ++++++++++++++++++++ src/library/vm/vm_name.h | 11 +++++++++ src/runtime/CMakeLists.txt | 2 +- src/{util => runtime}/hash.cpp | 0 src/{util => runtime}/hash.h | 0 src/runtime/object.cpp | 31 +++++++++++++++++++++++++ src/runtime/object.h | 13 +++++++++++ src/tests/util/hash.cpp | 2 +- src/util/CMakeLists.txt | 2 +- src/util/name.cpp | 23 ++++-------------- src/util/name.h | 2 +- src/util/name_hash_map.h | 2 +- src/util/name_hash_set.h | 2 +- src/util/sexpr/format.cpp | 2 +- src/util/sexpr/sexpr.cpp | 2 +- 35 files changed, 147 insertions(+), 62 deletions(-) create mode 100644 src/library/vm/vm_name.cpp create mode 100644 src/library/vm/vm_name.h rename src/{util => runtime}/hash.cpp (100%) rename src/{util => runtime}/hash.h (100%) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 9190d6ce16..a7588800ed 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -10,8 +10,8 @@ Author: Leonardo de Moura #include #include #include +#include "runtime/hash.h" #include "util/list_fn.h" -#include "util/hash.h" #include "util/buffer.h" #include "kernel/expr.h" #include "kernel/expr_eq_fn.h" diff --git a/src/kernel/expr.h b/src/kernel/expr.h index d05ac071da..d18de6a0c7 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -14,10 +14,10 @@ Author: Leonardo de Moura #include "runtime/optional.h" #include "runtime/thread.h" #include "runtime/serializer.h" +#include "runtime/hash.h" #include "util/rc.h" #include "util/name.h" #include "util/nat.h" -#include "util/hash.h" #include "util/buffer.h" #include "util/kvmap.h" #include "util/list_fn.h" diff --git a/src/kernel/expr_sets.h b/src/kernel/expr_sets.h index 897ba160f9..c9459f35a9 100644 --- a/src/kernel/expr_sets.h +++ b/src/kernel/expr_sets.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include -#include "util/hash.h" +#include "runtime/hash.h" #include "kernel/expr.h" namespace lean { diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index d760a018b0..fbe119dbfb 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -10,11 +10,11 @@ Author: Leonardo de Moura #include #include "runtime/debug.h" #include "runtime/interrupt.h" +#include "runtime/hash.h" #include "util/safe_arith.h" #include "util/buffer.h" #include "util/rc.h" #include "util/list.h" -#include "util/hash.h" #include "kernel/level.h" #include "kernel/environment.h" diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index ea2b7efdc8..e8f250dba7 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "runtime/sstream.h" +#include "util/name_hash_map.h" #include "library/abstract_type_context.h" #include "library/annotation.h" #include "library/pos_info_provider.h" @@ -19,7 +20,7 @@ kvmap mk_annotation_kvmap(name const & k) { return set_name(kvmap(), *g_annotation, k); } -typedef std::unordered_map annotation_maps; +typedef name_hash_map annotation_maps; static annotation_maps * g_annotation_maps = nullptr; void register_annotation(name const & kind) { diff --git a/src/library/compiler/builtin.cpp b/src/library/compiler/builtin.cpp index 61ce665d5c..f0b0f76404 100644 --- a/src/library/compiler/builtin.cpp +++ b/src/library/compiler/builtin.cpp @@ -24,7 +24,7 @@ struct builtin_decl { } }; -typedef std::unordered_map builtin_map; +typedef std::unordered_map builtin_map; static builtin_map * g_builtin_decls = nullptr; @@ -316,6 +316,11 @@ void initialize_builtin() { register_builtin(name({"thunk", "get"}), o_o_o, "lean::thunk_get", bb, xu); register_builtin(name({"thunk", "bind"}), o_o_o_o_o, "lean::thunk_get", bb, xu); register_builtin(name({"thunk", "map"}), o_o_o_o_o, "lean::thunk_bind", bbcc, xxuu); + + /* name builtin functions */ + register_builtin(name({"lean", "name", "hash"}), o_us, "lean::name_hash_usize", b); + register_builtin(name({"lean", "name", "mk_string"}), o_o_o, "lean::name_mk_string"); + register_builtin(name({"lean", "name", "mk_numeral"}), o_o_o, "lean::name_mk_numeral"); } void finalize_builtin() { diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 3731c00523..862ea81659 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -67,7 +67,6 @@ class csimp_fn { */ typedef rb_map, expr, pair_cmp> proj2var; proj2var m_proj2var; - typedef std::unordered_set name_set; environment const & env() const { return m_st.env(); } @@ -333,7 +332,7 @@ class csimp_fn { unsigned m_num_branches{0}; /* The number of branches that return a constructor application. */ unsigned m_num_cnstr_results{0}; - name_set m_visited_jps; + name_hash_set m_visited_jps; }; void collect_cases_info(expr e, cases_info_result & result) { @@ -689,7 +688,7 @@ class csimp_fn { } /* Return true iff `e` contains a free variable in `s` */ - bool depends_on(expr const & e, name_set const & s) { + bool depends_on(expr const & e, name_hash_set const & s) { if (!has_fvar(e)) return false; bool found = false; for_each(e, [&](expr const & e, unsigned) { @@ -722,7 +721,7 @@ class csimp_fn { buffer> & entries_ndep_x) { if (entries.empty()) return; - name_set deps; + name_hash_set deps; deps.insert(fvar_name(x)); /* Recall that `entries` are in reverse order. That is, pos 0 is the inner most variable. */ unsigned i = entries.size(); @@ -785,7 +784,7 @@ class csimp_fn { /* Copy `src_entries` and the new joint points that depend on them to `entries`, and update `entries_fvars`. This method is used after we perform a `float_cases_on`. */ - void move_to_entries(buffer const & src_entries, buffer & entries, name_set & entries_fvars) { + void move_to_entries(buffer const & src_entries, buffer & entries, name_hash_set & entries_fvars) { buffer todo; for (unsigned i = 0; i < src_entries.size(); i++) { expr_pair const & entry = src_entries[i]; @@ -842,8 +841,8 @@ class csimp_fn { We simplify the value of some let-declarations in this method, but we don't want to create a new temporary declaration just for this. */ buffer entries; - name_set e_fvars; /* Set of free variables names used in `e` */ - name_set entries_fvars; /* Set of free variable names used in `entries` */ + name_hash_set e_fvars; /* Set of free variables names used in `e` */ + name_hash_set entries_fvars; /* Set of free variable names used in `entries` */ collect_used(e, e_fvars); bool e_is_cases = is_cases_on_app(env(), e); /* diff --git a/src/library/compiler/elim_dead_let.cpp b/src/library/compiler/elim_dead_let.cpp index 9a751201dc..18f420e0a3 100644 --- a/src/library/compiler/elim_dead_let.cpp +++ b/src/library/compiler/elim_dead_let.cpp @@ -15,8 +15,8 @@ namespace lean { static name * g_elim_dead_let_fresh = nullptr; class elim_dead_let_fn { - std::unordered_set m_used; - name_generator m_ngen; + std::unordered_set m_used; + name_generator m_ngen; void mark_fvar(expr const & e) { m_used.insert(fvar_name(e)); diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 364bc7dba1..793585d802 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -22,7 +22,7 @@ class lambda_lifting_fn { name m_base_name; unsigned m_next_idx{1}; - typedef std::unordered_set name_set; + typedef std::unordered_set name_set; environment const & env() { return m_env; } diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index b353c9c1ac..b16f5e6245 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -10,6 +10,8 @@ Author: Leonardo de Moura #include #include "runtime/flet.h" #include "runtime/sstream.h" +#include "util/name_hash_set.h" +#include "util/name_hash_map.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" @@ -244,9 +246,9 @@ class to_llnf_fn { TODO(Leo): we must track which variables are marked as borrowed here. Reason: the `reuse` instruction is just overhead for variables marked as borrowed. */ - typedef std::unordered_set name_set; - typedef std::unordered_map cnstr_info_cache; - typedef std::unordered_map, name_hash> enum_cache; + typedef name_hash_set name_set; + typedef name_hash_map cnstr_info_cache; + typedef name_hash_map> enum_cache; type_checker::state m_st; bool m_unboxed; local_ctx m_lctx; @@ -401,7 +403,7 @@ class to_llnf_fn { if (saved_fvars_size == m_fvars.size()) return r; buffer used; - name_set used_fvars; + name_hash_set used_fvars; collect_used(r, used_fvars); while (m_fvars.size() > saved_fvars_size) { expr x = m_fvars.back(); diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index 7a45478039..27f7008114 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/name_hash_set.h" #include "kernel/type_checker.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" @@ -394,6 +395,7 @@ bool is_runtime_builtin_type(name const & n) { n == get_uint64_name() || n == get_usize_name() || n == get_thunk_name() || + n == get_lean_name_name() || // n == get_task_name() || TODO(Leo): enable // n == get_array_name() || TODO(Leo): enable n == get_nat_name() || @@ -420,7 +422,9 @@ bool is_runtime_builtin_cnstr(name const & n) { n == get_string_mk_name() || n == get_string_iterator_mk_name() || n == get_int_of_nat_name() || - n == get_int_neg_succ_of_nat_name(); + n == get_int_neg_succ_of_nat_name() || + n == get_lean_name_mk_numeral_name() || + n == get_lean_name_mk_string_name(); } bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type) { @@ -438,7 +442,7 @@ bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & t return false; } -void collect_used(expr const & e, std::unordered_set & S) { +void collect_used(expr const & e, name_hash_set & S) { if (!has_fvar(e)) return; for_each(e, [&](expr const & e, unsigned) { if (!has_fvar(e)) return false; diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h index 0dddb6eb16..33495b750a 100644 --- a/src/library/compiler/util.h +++ b/src/library/compiler/util.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include #include "util/pair_ref.h" #include "util/list_ref.h" +#include "util/name_hash_set.h" #include "kernel/expr.h" #include "kernel/type_checker.h" #include "library/constants.h" @@ -151,7 +151,7 @@ bool is_runtime_builtin_cnstr(name const & n); bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type); -void collect_used(expr const & e, std::unordered_set & S); +void collect_used(expr const & e, name_hash_set & S); environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v); environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v); diff --git a/src/library/context_cache.h b/src/library/context_cache.h index 776092eec0..13b223b683 100644 --- a/src/library/context_cache.h +++ b/src/library/context_cache.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include "util/name_hash_map.h" #include "kernel/expr_maps.h" #include "kernel/equiv_manager.h" #include "library/expr_unsigned_map.h" @@ -15,8 +16,8 @@ Author: Leonardo de Moura namespace lean { class context_cache : public context_cacheless { - typedef std::unordered_map, name_hash> transparency_cache; - typedef std::unordered_map name2bool; + typedef name_hash_map> transparency_cache; + typedef name_hash_map name2bool; /** We use expr_cond_bi_struct_map because sometimes we want the inferred type to contain precise binder information (e.g., in the elaborator). diff --git a/src/library/expr_pair.h b/src/library/expr_pair.h index bbbf819ab4..b53660febd 100644 --- a/src/library/expr_pair.h +++ b/src/library/expr_pair.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include -#include "util/hash.h" +#include "runtime/hash.h" #include "library/expr_lt.h" namespace lean { diff --git a/src/library/module.cpp b/src/library/module.cpp index dde7de3d0a..7f6ee33347 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -15,7 +15,7 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include "runtime/thread.h" #include "runtime/interrupt.h" #include "runtime/sstream.h" -#include "util/hash.h" +#include "runtime/hash.h" #include "util/lean_path.h" #include "util/buffer.h" #include "util/name_map.h" diff --git a/src/library/phash_map.h b/src/library/phash_map.h index 5c8d85a628..20ef9ea2d0 100644 --- a/src/library/phash_map.h +++ b/src/library/phash_map.h @@ -119,5 +119,5 @@ public: }; template -using name_hash_map = phash_map; +using name_hash_map = phash_map; } diff --git a/src/library/private.cpp b/src/library/private.cpp index 72fa63c126..2493b12ec1 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #include #include "runtime/sstream.h" -#include "util/hash.h" +#include "runtime/hash.h" #include "library/private.h" #include "library/module.h" diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index c27214a96c..46e2d4f857 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,2 +1,2 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp - vm_int.cpp vm_uint.cpp vm_thunk.cpp init_module.cpp) + vm_int.cpp vm_uint.cpp vm_thunk.cpp vm_name.cpp init_module.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index bf1164220a..7875dfe5e1 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/vm/vm_io.h" #include "library/vm/vm_string.h" #include "library/vm/vm_thunk.h" +#include "library/vm/vm_name.h" namespace lean { void initialize_vm_core_module() { @@ -23,9 +24,11 @@ void initialize_vm_core_module() { initialize_vm_string(); initialize_vm_uint(); initialize_vm_thunk(); + initialize_vm_name(); } void finalize_vm_core_module() { + finalize_vm_name(); finalize_vm_thunk(); finalize_vm_uint(); finalize_vm_string(); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 315d067881..d80b32b03b 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -15,7 +15,10 @@ Author: Leonardo de Moura #include "runtime/sstream.h" #include "runtime/memory.h" #include "runtime/flet.h" +#include "util/name_hash_map.h" +#include "util/name_hash_set.h" #include "util/timeit.h" +#include "util/name_hash_map.h" #include "util/sexpr/option_declarations.h" #include "util/shared_mutex.h" #include "library/constants.h" @@ -3442,14 +3445,14 @@ auto vm_state::profiler::get_snapshots() -> snapshots { stop(); snapshots r; r.m_total_time = chrono::milliseconds(0); - std::unordered_map, name_hash> timings; + name_hash_map> timings; for (snapshot_core const & s : m_snapshots) { snapshot new_s; new_s.m_duration = s.m_duration; new_s.m_perf_counters = s.m_perf_counters; r.m_total_time += s.m_duration; auto & new_stack = new_s.m_stack; - std::unordered_set decl_already_seen_in_this_stack; + name_hash_set decl_already_seen_in_this_stack; for (unsigned i = 0; i < s.m_stack.size(); i++) { auto const & p = s.m_stack[i]; vm_decl const * decl = m_state.m_decl_map.find(p.first); @@ -3575,9 +3578,9 @@ unsigned get_vm_builtin_arity(name const & fn) { } class vm_index_manager { - shared_mutex m_mutex; - std::unordered_map m_name2idx; - std::vector m_idx2name; + shared_mutex m_mutex; + name_hash_map m_name2idx; + std::vector m_idx2name; public: unsigned get_index(name const & n) { diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp new file mode 100644 index 0000000000..ed6b6c879c --- /dev/null +++ b/src/library/vm/vm_name.cpp @@ -0,0 +1,25 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/vm/vm.h" +namespace lean { +static vm_obj dummy_unary_op(vm_obj const &) { + throw exception("name object support has not been implemented in the old VM"); +} + +static vm_obj dummy_binary_op(vm_obj const &, vm_obj const &) { + throw exception("name object support has not been implemented in the old VM"); +} + +void initialize_vm_name() { + DECLARE_VM_BUILTIN(name({"lean", "name", "hash"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"lean", "name", "mk_string"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"lean", "name", "mk_numeral"}), dummy_binary_op); +} + +void finalize_vm_name() { +} +} diff --git a/src/library/vm/vm_name.h b/src/library/vm/vm_name.h new file mode 100644 index 0000000000..996c34e1a4 --- /dev/null +++ b/src/library/vm/vm_name.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2019 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 { +void initialize_vm_name(); +void finalize_vm_name(); +} diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index bd4fdd2c6d..4baccd511c 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -1,6 +1,6 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp mpq.cpp utf8.cpp object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp -serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp) +serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp) add_library(runtime OBJECT ${RUNTIME_OBJS}) add_library(leanruntime ${RUNTIME_OBJS}) diff --git a/src/util/hash.cpp b/src/runtime/hash.cpp similarity index 100% rename from src/util/hash.cpp rename to src/runtime/hash.cpp diff --git a/src/util/hash.h b/src/runtime/hash.h similarity index 100% rename from src/util/hash.h rename to src/runtime/hash.h diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 0a8e7acb65..9006ced70a 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "runtime/apply.h" #include "runtime/flet.h" #include "runtime/interrupt.h" +#include "runtime/hash.h" namespace lean { size_t obj_byte_size(object * o) { @@ -1521,6 +1522,36 @@ obj_res string_iterator_snd(b_obj_arg it) { return r; } +// ======================================= +// name + +/* +inductive name +| anonymous : name +| mk_string : name → string → name +| mk_numeral : name → nat → name +*/ +obj_res name_mk_string(obj_arg p, obj_arg s) { + object * r = alloc_cnstr(1, 2, sizeof(unsigned)); + size_t sz = string_size(s); + unsigned h = hash_str(sz, string_cstr(s), name_hash(p)); + cnstr_set(r, 0, p); + cnstr_set(r, 1, s); + cnstr_set_scalar(r, 2*sizeof(object*), h); + return r; +} + +obj_res name_mk_numeral(obj_arg p, obj_arg n) { + object * r = alloc_cnstr(2, 2, sizeof(unsigned)); + unsigned h1 = is_scalar(n) ? unbox(n) : mpz_value(n).hash(); + unsigned h2 = name_hash(p); + unsigned h = hash(h1, h2); + cnstr_set(r, 0, p); + cnstr_set(r, 1, n); + cnstr_set_scalar(r, 2*sizeof(object*), h); + return r; +} + // ======================================= // Debugging helper functions diff --git a/src/runtime/object.h b/src/runtime/object.h index 253d4b05ea..f31b574f34 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -1256,4 +1256,17 @@ inline usize usize_modn(usize a1, b_obj_arg a2) { inline obj_res usize_dec_eq(usize a1, usize a2) { return box(a1 == a2); } inline obj_res usize_dec_lt(usize a1, usize a2) { return box(a1 < a2); } inline obj_res usize_dec_le(usize a1, usize a2) { return box(a1 <= a2); } + +// ======================================= +// name +inline unsigned name_hash(b_obj_arg n) { + if (lean::is_scalar(n)) return 11; + else return lean::cnstr_get_scalar(n, sizeof(void*)*2); +} + +inline size_t name_hash_usize(b_obj_arg n) { return name_hash(n); } + +obj_res name_mk_string(obj_arg p, obj_arg s); +obj_res name_mk_numeral(obj_arg p, obj_arg n); +inline obj_res name_mk_string(obj_arg p, char const * s) { return name_mk_string(p, mk_string(s)); } } diff --git a/src/tests/util/hash.cpp b/src/tests/util/hash.cpp index 2113fcfd97..c66078cb33 100644 --- a/src/tests/util/hash.cpp +++ b/src/tests/util/hash.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/test.h" -#include "util/hash.h" +#include "runtime/hash.h" using namespace lean; static void tst1() { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b19aa37196..6a9388fe40 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(util OBJECT object_ref.cpp name.cpp name_set.cpp fresh_name.cpp hash.cpp +add_library(util OBJECT object_ref.cpp name.cpp name_set.cpp fresh_name.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp shared_mutex.cpp path.cpp lean_path.cpp lbool.cpp bitap_fuzzy_search.cpp init_module.cpp name_map.cpp list_fn.cpp file_lock.cpp diff --git a/src/util/name.cpp b/src/util/name.cpp index 83c76094e3..924d682936 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -14,9 +14,9 @@ Author: Leonardo de Moura #include "runtime/debug.h" #include "runtime/sstream.h" #include "runtime/utf8.h" +#include "runtime/hash.h" #include "util/name.h" #include "util/buffer.h" -#include "util/hash.h" #include "util/ascii.h" namespace lean { @@ -94,38 +94,25 @@ static void display_name(std::ostream & out, name const & n, bool escape, char c } name::name(name const & prefix, char const * n): - object_ref(mk_cnstr(static_cast(name_kind::STRING), - prefix.raw(), mk_string(n), sizeof(unsigned))) { + object_ref(name_mk_string(prefix.raw(), n)) { inc(prefix.raw()); - size_t sz = strlen(n); - unsigned h = hash_str(static_cast(sz), n, prefix.hash()); - cnstr_set_scalar(raw(), 2*sizeof(object*), h); // NOLINT } name::name(name const & prefix, unsigned k): - object_ref(mk_cnstr(static_cast(name_kind::NUMERAL), - prefix.raw(), mk_nat_obj(k), sizeof(unsigned))) { + object_ref(name_mk_numeral(prefix.raw(), mk_nat_obj(k))) { inc(prefix.raw()); - unsigned h = ::lean::hash(k, prefix.hash()); - cnstr_set_scalar(raw(), 2*sizeof(object*), h); // NOLINT } name::name(name const & prefix, string_ref const & s): - object_ref(mk_cnstr(static_cast(name_kind::STRING), - prefix.raw(), s.raw(), sizeof(unsigned))) { + object_ref(name_mk_string(prefix.raw(), s.raw())) { inc(prefix.raw()); inc(s.raw()); - unsigned h = hash_str(static_cast(s.num_bytes()), s.data(), prefix.hash()); - cnstr_set_scalar(raw(), 2*sizeof(object*), h); // NOLINT } name::name(name const & prefix, nat const & k): - object_ref(mk_cnstr(static_cast(name_kind::NUMERAL), - prefix.raw(), k.raw(), sizeof(unsigned))) { + object_ref(name_mk_numeral(prefix.raw(), k.raw())) { inc(prefix.raw()); inc(k.raw()); - unsigned h = ::lean::hash(k.hash(), prefix.hash()); - cnstr_set_scalar(raw(), 2*sizeof(object*), h); // NOLINT } name::name(std::initializer_list const & l):name() { diff --git a/src/util/name.h b/src/util/name.h index f3522b4cb4..aabc1404c2 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -203,7 +203,7 @@ public: name string_to_name(std::string const & str); -struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } }; +struct name_hash_fn { unsigned operator()(name const & n) const { return n.hash(); } }; struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } }; struct name_cmp { typedef name type; diff --git a/src/util/name_hash_map.h b/src/util/name_hash_map.h index b6d3ec543f..b69946c98e 100644 --- a/src/util/name_hash_map.h +++ b/src/util/name_hash_map.h @@ -8,5 +8,5 @@ Author: Leonardo de Moura #include #include "util/name.h" namespace lean { -template using name_hash_map = std::unordered_map; +template using name_hash_map = std::unordered_map; } diff --git a/src/util/name_hash_set.h b/src/util/name_hash_set.h index 3abdb17f4f..1ac7be582a 100644 --- a/src/util/name_hash_set.h +++ b/src/util/name_hash_set.h @@ -8,5 +8,5 @@ Author: Daniel Selsam #include #include "util/name.h" namespace lean { -typedef std::unordered_set name_hash_set; +typedef std::unordered_set name_hash_set; } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 4457d0bde8..7da70a4462 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -12,7 +12,7 @@ #include #include "runtime/interrupt.h" #include "runtime/sstream.h" -#include "util/hash.h" +#include "runtime/hash.h" #include "util/escaped.h" #include "util/sexpr/sexpr.h" #include "util/sexpr/format.h" diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index a2ed8e70a8..735c12e976 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include #include #include "runtime/sstream.h" +#include "runtime/hash.h" #include "util/rc.h" -#include "util/hash.h" #include "util/name.h" #include "util/escaped.h" #include "util/buffer.h"