From 9f6a8827e02afae00b14197d8021817bd0fc0cb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Sep 2014 10:23:11 -0700 Subject: [PATCH] refactor(*): use name_map --- src/frontends/lean/calc.cpp | 4 ++-- src/frontends/lean/class.cpp | 2 +- src/frontends/lean/cmd_table.h | 2 +- src/frontends/lean/local_decls.h | 2 +- src/frontends/lean/parse_table.cpp | 6 +++--- src/frontends/lean/tactic_hint.cpp | 2 +- src/kernel/environment.h | 3 ++- src/kernel/inductive/inductive.cpp | 11 ++++++----- src/kernel/metavar.h | 7 ++++--- src/library/aliases.cpp | 10 +++++----- src/library/coercion.cpp | 10 +++++----- src/library/private.cpp | 4 ++-- src/library/scoped_ext.h | 6 +++--- src/library/unifier.cpp | 4 ++-- 14 files changed, 38 insertions(+), 35 deletions(-) diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index 7d39e2d75..dac8aca3c 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -51,8 +51,8 @@ struct calc_entry { }; struct calc_state { - typedef rb_map, name_quick_cmp> refl_table; - typedef rb_map, name_quick_cmp> subst_table; + typedef name_map> refl_table; + typedef name_map> subst_table; typedef rb_map, name_pair_quick_cmp> trans_table; trans_table m_trans_table; refl_table m_refl_table; diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 9ce195df9..610fad622 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -26,7 +26,7 @@ struct class_entry { }; struct class_state { - typedef rb_map, name_quick_cmp> class_instances; + typedef name_map> class_instances; class_instances m_instances; void add_class(name const & c) { auto it = m_instances.find(c); diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h index a8cb78535..1be2be626 100644 --- a/src/frontends/lean/cmd_table.h +++ b/src/frontends/lean/cmd_table.h @@ -30,6 +30,6 @@ public: }; typedef cmd_info_tmpl cmd_info; -typedef rb_map cmd_table; +typedef name_map cmd_table; inline void add_cmd(cmd_table & t, cmd_info const & cmd) { t.insert(cmd.get_name(), cmd); } } diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h index ccaea4299..56df2dea6 100644 --- a/src/frontends/lean/local_decls.h +++ b/src/frontends/lean/local_decls.h @@ -19,7 +19,7 @@ namespace lean { */ template class local_decls { - typedef rb_map, name_quick_cmp> map; + typedef name_map> map; typedef list>> scopes; map m_map; unsigned m_counter; diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index d6abf303b..bd2525fa7 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -269,9 +269,9 @@ transition replace(transition const & t, std::function const } struct parse_table::cell { - bool m_nud; - list m_accept; - rb_map, name_quick_cmp> m_children; + bool m_nud; + list m_accept; + name_map> m_children; MK_LEAN_RC(); // Declare m_rc counter void dealloc() { delete this; } cell(bool nud = true):m_nud(nud), m_rc(1) {} diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp index d8f73e39e..516204586 100644 --- a/src/frontends/lean/tactic_hint.cpp +++ b/src/frontends/lean/tactic_hint.cpp @@ -21,7 +21,7 @@ namespace lean { typedef list tactic_hint_entries; struct tactic_hint_state { - typedef rb_map class_tactics; + typedef name_map class_tactics; class_tactics m_class_tactics; tactic_hint_entries m_tactics; }; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 590201a02..b08c1fb40 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "util/list.h" #include "util/rb_map.h" #include "util/name_set.h" +#include "util/name_map.h" #include "kernel/expr.h" #include "kernel/constraint.h" #include "kernel/declaration.h" @@ -101,7 +102,7 @@ public: */ class environment { typedef std::shared_ptr header; - typedef rb_map declarations; + typedef name_map declarations; typedef std::shared_ptr extensions; header m_header; diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 32071973b..30a94c749 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -123,15 +123,16 @@ struct inductive_env_ext : public environment_extension { }; // mapping from introduction rule name to computation rule data - rb_map m_elim_info; - rb_map m_comp_rules; + name_map m_elim_info; + name_map m_comp_rules; // mapping from intro rule to datatype - rb_map m_intro_info; - rb_map m_inductive_info; + name_map m_intro_info; + name_map m_inductive_info; inductive_env_ext() {} - void add_elim(name const & n, name const & id_name, level_param_names const & ls, unsigned num_ps, unsigned num_ace, unsigned num_indices) { + void add_elim(name const & n, name const & id_name, level_param_names const & ls, + unsigned num_ps, unsigned num_ace, unsigned num_indices) { m_elim_info.insert(n, elim_info(id_name, ls, num_ps, num_ace, num_indices)); } diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index cf723183d..da9c57846 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -9,14 +9,15 @@ Author: Leonardo de Moura #include "util/rb_map.h" #include "util/optional.h" #include "util/name_set.h" +#include "util/name_map.h" #include "kernel/expr.h" #include "kernel/justification.h" namespace lean { class substitution { - typedef rb_map expr_map; - typedef rb_map level_map; - typedef rb_map jst_map; + typedef name_map expr_map; + typedef name_map level_map; + typedef name_map jst_map; expr_map m_expr_subst; level_map m_level_subst; diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 81e57edd5..2552c9ecd 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -25,11 +25,11 @@ static environment update(environment const & env, aliases_ext const & ext); struct aliases_ext : public environment_extension { struct state { - bool m_in_section_or_context; - rb_map, name_quick_cmp> m_aliases; - rb_map m_inv_aliases; - rb_map m_level_aliases; - rb_map m_inv_level_aliases; + bool m_in_section_or_context; + name_map> m_aliases; + name_map m_inv_aliases; + name_map m_level_aliases; + name_map m_inv_level_aliases; state():m_in_section_or_context(false) {} void add_expr_alias(name const & a, name const & e) { diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 55cd7de3e..eaee2a240 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -56,12 +56,12 @@ struct coercion_info { }; struct coercion_state { - rb_map, name_quick_cmp> m_coercion_info; + name_map> m_coercion_info; // m_from and m_to contain "direct" coercions - typedef std::tuple from_data; - rb_map, name_quick_cmp> m_from; // map user-class -> list of (class, coercion-fun) - rb_map, coercion_class_cmp_fn> m_to; - rb_map, name_quick_cmp> m_coercions; // map coercion -> (from-class, num-args) + typedef std::tuple from_data; + name_map> m_from; // map user-class -> list of (class, coercion-fun) + rb_map, coercion_class_cmp_fn> m_to; + name_map> m_coercions; // map coercion -> (from-class, num-args) template void for_each_info(name const & from, coercion_class const & to, F && f) { diff --git a/src/library/private.cpp b/src/library/private.cpp index ec412e656..65ce0564c 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -13,8 +13,8 @@ Author: Leonardo de Moura namespace lean { struct private_ext : public environment_extension { - unsigned m_counter; - rb_map m_inv_map; // map: hidden-name -> user-name + unsigned m_counter; + name_map m_inv_map; // map: hidden-name -> user-name private_ext():m_counter(0) {} }; diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 02640f5c3..b72213437 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -69,9 +69,9 @@ class scoped_ext : public environment_extension { static name const & get_class_name() { return Config::get_class_name(); } static std::string const & get_serialization_key() { return Config::get_serialization_key(); } - state m_state; - list m_scopes; - rb_map, name_quick_cmp> m_entries; + state m_state; + list m_scopes; + name_map> m_entries; void using_namespace_core(environment const & env, io_state const & ios, name const & n) { if (auto it = m_entries.find(n)) { diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 4de1d0b7a..6a646f8a7 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -290,8 +290,8 @@ struct unifier_fn { }; typedef rb_tree cnstr_set; typedef rb_tree cnstr_idx_set; - typedef rb_map name_to_cnstrs; - typedef rb_map owned_map; + typedef name_map name_to_cnstrs; + typedef name_map owned_map; typedef rb_map, expr_quick_cmp> expr_map; typedef std::unique_ptr type_checker_ptr; environment m_env;