From 1e4fa76a47461ae814beadb251003fb585d2625e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Dec 2013 11:34:40 -0800
Subject: [PATCH] feat(util/name_map): add template alias

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend.cpp |  5 +++--
 src/frontends/lean/parser.cpp   |  2 +-
 src/kernel/environment.h        |  3 ++-
 src/library/hidden_defs.cpp     |  3 ++-
 src/util/name_map.h             | 12 ++++++++++++
 5 files changed, 20 insertions(+), 5 deletions(-)
 create mode 100644 src/util/name_map.h

diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 3a3c9cc05..9348ddf23 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/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 std::unordered_map<name, implicit_info, name_hash, name_eq> implicit_table;
+    typedef name_map<operator_info> operator_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;
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c32f9a15d..756a1867a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/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
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 67c858a92..f047cb017 100644
--- a/src/kernel/environment.h
+++ b/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
diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp
index 46640af99..809725900 100644
--- a/src/library/hidden_defs.cpp
+++ b/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 {
diff --git a/src/util/name_map.h b/src/util/name_map.h
new file mode 100644
index 000000000..ac243abce
--- /dev/null
+++ b/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>;
+}