feat(util/name_map): add template alias

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/frontend.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/map.h"
 #include "util/sstream.h"
 #include "util/exception.h"
+#include "util/name_map.h"
 #include "kernel/environment.h"
 #include "library/expr_pair.h"
 #include "library/io_state.h"
@@ -30,8 +31,8 @@ static std::vector<bool> g_empty_vector;
 struct lean_extension : public environment_extension {
     typedef std::pair<std::vector<bool>, name> implicit_info;
     // Remark: only named objects are stored in the dictionary.
-    typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
+    typedef name_map<operator_info> operator_table;
-    typedef std::unordered_map<name, implicit_info, name_hash, name_eq> implicit_table;
+    typedef name_map<implicit_info> implicit_table;
     typedef std::unordered_map<expr, list<operator_info>, expr_hash, std::equal_to<expr>> expr_to_operators;
     typedef std::unordered_map<expr_pair, expr, expr_pair_hash, expr_pair_eq> coercion_map;
     typedef std::unordered_map<expr, list<expr_pair>, expr_hash, std::equal_to<expr>> expr_to_coercions;

src/frontends/lean/parser.cpp

@@ -134,7 +134,7 @@ static name g_unused = name::mk_internal_unique_name();
 */
 class parser::imp {
     typedef scoped_map<name, unsigned, name_hash, name_eq> local_decls;
-    typedef std::unordered_map<name, expr, name_hash, name_eq>  builtins;
+    typedef name_map<expr> builtins;
     typedef std::pair<unsigned, unsigned> pos_info;
     typedef expr_map<pos_info> expr_pos_info;
     typedef expr_map<tactic>   tactic_hints; // a mapping from placeholder to tactic

src/kernel/environment.h

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include <set>
 #include "util/lua.h"
 #include "util/shared_mutex.h"
+#include "util/name_map.h"
 #include "kernel/context.h"
 #include "kernel/object.h"
 #include "kernel/level.h"
@@ -28,7 +29,7 @@ class environment_cell {
     friend class read_write_shared_environment;
     friend class read_only_shared_environment;
     // Remark: only named objects are stored in the dictionary.
-    typedef std::unordered_map<name, object, name_hash, name_eq> object_dictionary;
+    typedef name_map<object> object_dictionary;
     typedef std::tuple<level, level, int> constraint;
     std::weak_ptr<environment_cell>         m_this;
     // Universe variable management

src/library/hidden_defs.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <unordered_map>
 #include "util/name.h"
 #include "util/sstream.h"
+#include "util/name_map.h"
 #include "kernel/environment.h"
 #include "kernel/builtin.h"
 #include "library/hidden_defs.h"
@@ -14,7 +15,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct hidden_defs_extension : public environment_extension {
-    typedef std::unordered_map<name, bool, name_hash, name_eq> hidden_defs;
+    typedef name_map<bool> hidden_defs;
     hidden_defs m_hidden_defs;
 
     hidden_defs_extension const * get_parent() const {

src/util/name_map.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <unordered_map>
+#include "util/name.h"
+namespace lean {
+template<typename T> using name_map = std::unordered_map<name, T, name_hash, name_eq>;
+}