From 47c7bb1bdebc8a4f285a2a4813e839904be67f2d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Dec 2013 11:42:43 -0800 Subject: [PATCH] refactor(*): uses aliases for unordered_map and unordered_set Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.cpp | 16 +++++++++------- src/frontends/lean/parser.cpp | 1 - src/kernel/environment.cpp | 2 -- src/kernel/environment.h | 1 - src/kernel/expr_maps.h | 6 +++++- src/kernel/expr_sets.h | 4 ++++ src/kernel/normalizer.cpp | 4 ++-- src/kernel/replace_visitor.h | 4 ++-- src/kernel/type_checker.cpp | 4 ++-- src/library/expr_pair_maps.h | 15 +++++++++++++++ src/library/hidden_defs.cpp | 1 - src/library/type_inferer.cpp | 4 ++-- src/util/freset.h | 2 +- 13 files changed, 42 insertions(+), 22 deletions(-) create mode 100644 src/library/expr_pair_maps.h diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 9348ddf23d..5b84aaa344 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include #include #include @@ -14,7 +13,10 @@ Author: Leonardo de Moura #include "util/exception.h" #include "util/name_map.h" #include "kernel/environment.h" +#include "kernel/expr_maps.h" +#include "kernel/expr_sets.h" #include "library/expr_pair.h" +#include "library/expr_pair_maps.h" #include "library/io_state.h" #include "library/all/all.h" #include "frontends/lean/operator_info.h" @@ -31,12 +33,12 @@ static std::vector g_empty_vector; struct lean_extension : public environment_extension { typedef std::pair, name> implicit_info; // Remark: only named objects are stored in the dictionary. - typedef name_map operator_table; - typedef name_map implicit_table; - typedef std::unordered_map, expr_hash, std::equal_to> expr_to_operators; - typedef std::unordered_map coercion_map; - typedef std::unordered_map, expr_hash, std::equal_to> expr_to_coercions; - typedef std::unordered_set> coercion_set; + typedef name_map operator_table; + typedef name_map implicit_table; + typedef expr_struct_map> expr_to_operators; + typedef expr_pair_struct_map coercion_map; + typedef expr_struct_map> expr_to_coercions; + typedef expr_struct_set coercion_set; operator_table m_nud; // nud table for Pratt's parser operator_table m_led; // led table for Pratt's parser diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 756a1867a8..505fc42171 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include #include #endif -#include #include #include #include diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 9cdf1f888b..cc993eb6d2 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -8,8 +8,6 @@ Author: Leonardo de Moura #include #include #include -#include -#include #include "util/thread.h" #include "util/safe_arith.h" #include "util/realpath.h" diff --git a/src/kernel/environment.h b/src/kernel/environment.h index f047cb017d..30da363cd5 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include #include -#include #include #include "util/lua.h" #include "util/shared_mutex.h" diff --git a/src/kernel/expr_maps.h b/src/kernel/expr_maps.h index 50e1d429b2..2050eed321 100644 --- a/src/kernel/expr_maps.h +++ b/src/kernel/expr_maps.h @@ -6,10 +6,11 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "kernel/expr.h" namespace lean { - +// Maps based on pointer equality. That is, two keys are equal iff they are pointer equal template using expr_map = typename std::unordered_map; @@ -22,4 +23,7 @@ using expr_cell_map = typename std::unordered_map using expr_cell_offset_map = typename std::unordered_map; +// Maps based on structural equality. That is, two keys are equal iff they are structurally equal +template +using expr_struct_map = typename std::unordered_map>; }; diff --git a/src/kernel/expr_sets.h b/src/kernel/expr_sets.h index ff8a525b7b..c3b9b7a53d 100644 --- a/src/kernel/expr_sets.h +++ b/src/kernel/expr_sets.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include #include "util/hash.h" #include "kernel/expr.h" @@ -48,4 +49,7 @@ struct expr_cell_pair_eqp { }; typedef std::unordered_set expr_cell_pair_set; // ======================================= + +// Similar to expr_set, but using structural equality +typedef std::unordered_set> expr_struct_set; } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index abffc17523..d2043f2cc5 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include -#include #include "util/list.h" #include "util/flet.h" #include "util/freset.h" @@ -15,6 +14,7 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" #include "kernel/normalizer.h" #include "kernel/expr.h" +#include "kernel/expr_maps.h" #include "kernel/context.h" #include "kernel/environment.h" #include "kernel/builtin.h" @@ -73,7 +73,7 @@ closure const & to_closure(expr const & e) { lean_assert(is_closure(e)); retur /** \brief Expression normalizer. */ class normalizer::imp { - typedef std::unordered_map cache; + typedef expr_map cache; ro_environment::weak_ref m_env; context m_ctx; diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index f00b82469b..f3f139040b 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "kernel/expr_maps.h" #include "kernel/replace_fn.h" #include "kernel/context.h" @@ -21,7 +21,7 @@ namespace lean { */ class replace_visitor { protected: - typedef std::unordered_map cache; + typedef expr_map cache; cache m_cache; context m_ctx; expr save_result(expr const & e, expr && r, bool shared); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b5f1f75178..9796596b0a 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include "util/freset.h" #include "util/flet.h" #include "util/interrupt.h" #include "kernel/type_checker.h" +#include "kernel/expr_maps.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" #include "kernel/normalizer.h" @@ -21,7 +21,7 @@ namespace lean { static name g_x_name("x"); /** \brief Auxiliary functional object used to implement infer_type. */ class type_checker::imp { - typedef std::unordered_map cache; + typedef expr_map cache; typedef buffer unification_constraints; ro_environment::weak_ref m_env; diff --git a/src/library/expr_pair_maps.h b/src/library/expr_pair_maps.h new file mode 100644 index 0000000000..d145b012e2 --- /dev/null +++ b/src/library/expr_pair_maps.h @@ -0,0 +1,15 @@ +/* +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 +#include "kernel/expr.h" +#include "library/expr_pair.h" +namespace lean { +// Map based on structural equality +template +using expr_pair_struct_map = std::unordered_map; +} diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp index 8097259004..1ddeb19138 100644 --- a/src/library/hidden_defs.cpp +++ b/src/library/hidden_defs.cpp @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include "util/name.h" #include "util/sstream.h" #include "util/name_map.h" diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index cfab991b41..ab1b755b6f 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include "util/flet.h" #include "util/freset.h" #include "util/interrupt.h" #include "kernel/environment.h" +#include "kernel/expr_maps.h" #include "kernel/normalizer.h" #include "kernel/builtin.h" #include "kernel/kernel_exception.h" @@ -22,7 +22,7 @@ Author: Leonardo de Moura namespace lean { static name g_x_name("x"); class type_inferer::imp { - typedef std::unordered_map cache; + typedef expr_map cache; typedef buffer unification_constraints; ro_environment m_env; diff --git a/src/util/freset.h b/src/util/freset.h index 8d7e783c49..e4a80a499e 100644 --- a/src/util/freset.h +++ b/src/util/freset.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once - +#include namespace lean { /** \brief Template for simulating "fluid-resets".