michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(*): use name_map

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-28 10:23:11 -07:00
parent 33fe409dc6
commit 9f6a8827e0
14 changed files with 38 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/calc.cpp
View file

@ -51,8 +51,8 @@ struct calc_entry {
};
struct calc_state {
typedef rb_map<name, pair<name, unsigned>, name_quick_cmp> refl_table;
typedef rb_map<name, pair<name, unsigned>, name_quick_cmp> subst_table;
typedef name_map<pair<name, unsigned>> refl_table;
typedef name_map<pair<name, unsigned>> subst_table;
typedef rb_map<name_pair, std::tuple<name, name, unsigned>, name_pair_quick_cmp> trans_table;
trans_table m_trans_table;
refl_table m_refl_table;

2
src/frontends/lean/class.cpp
View file

@ -26,7 +26,7 @@ struct class_entry {
};
struct class_state {
typedef rb_map<name, list<name>, name_quick_cmp> class_instances;
typedef name_map<list<name>> class_instances;
class_instances m_instances;
void add_class(name const & c) {
auto it = m_instances.find(c);

2
src/frontends/lean/cmd_table.h
View file

@ -30,6 +30,6 @@ public:
};
typedef cmd_info_tmpl<command_fn> cmd_info;
typedef rb_map<name, cmd_info, name_quick_cmp> cmd_table;
typedef name_map<cmd_info> cmd_table;
inline void add_cmd(cmd_table & t, cmd_info const & cmd) { t.insert(cmd.get_name(), cmd); }
}

2
src/frontends/lean/local_decls.h
View file

@ -19,7 +19,7 @@ namespace lean {
*/
template<typename V>
class local_decls {
typedef rb_map<name, pair<V, unsigned>, name_quick_cmp> map;
typedef name_map<pair<V, unsigned>> map;
typedef list<std::tuple<map, unsigned, list<V>>> scopes;
map m_map;
unsigned m_counter;

6
src/frontends/lean/parse_table.cpp
View file

@ -269,9 +269,9 @@ transition replace(transition const & t, std::function<expr(expr const &)> const
}
struct parse_table::cell {
bool m_nud;
list<expr> m_accept;
rb_map<name, pair<action, parse_table>, name_quick_cmp> m_children;
bool m_nud;
list<expr> m_accept;
name_map<pair<action, parse_table>> m_children;
MK_LEAN_RC(); // Declare m_rc counter
void dealloc() { delete this; }
cell(bool nud = true):m_nud(nud), m_rc(1) {}

2
src/frontends/lean/tactic_hint.cpp
View file

@ -21,7 +21,7 @@ namespace lean {
typedef list<tactic_hint_entry> tactic_hint_entries;
struct tactic_hint_state {
typedef rb_map<name, tactic_hint_entries, name_quick_cmp> class_tactics;
typedef name_map<tactic_hint_entries> class_tactics;
class_tactics m_class_tactics;
tactic_hint_entries m_tactics;
};

3
src/kernel/environment.h
View file

@ -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<environment_header const> header;
typedef rb_map<name, declaration, name_quick_cmp> declarations;
typedef name_map<declaration> declarations;
typedef std::shared_ptr<environment_extensions const> extensions;
header m_header;

11
src/kernel/inductive/inductive.cpp
View file

@ -123,15 +123,16 @@ struct inductive_env_ext : public environment_extension {
};
// mapping from introduction rule name to computation rule data
rb_map<name, elim_info, name_quick_cmp> m_elim_info;
rb_map<name, comp_rule, name_quick_cmp> m_comp_rules;
name_map<elim_info> m_elim_info;
name_map<comp_rule> m_comp_rules;
// mapping from intro rule to datatype
rb_map<name, name, name_quick_cmp> m_intro_info;
rb_map<name, inductive_decls, name_quick_cmp> m_inductive_info;
name_map<name> m_intro_info;
name_map<inductive_decls> 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));
}

7
src/kernel/metavar.h
View file

@ -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<name, expr, name_quick_cmp> expr_map;
typedef rb_map<name, level, name_quick_cmp> level_map;
typedef rb_map<name, justification, name_quick_cmp> jst_map;
typedef name_map<expr> expr_map;
typedef name_map<level> level_map;
typedef name_map<justification> jst_map;
expr_map m_expr_subst;
level_map m_level_subst;

10
src/library/aliases.cpp
View file

@ -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, list<name>, name_quick_cmp> m_aliases;
rb_map<name, name, name_quick_cmp> m_inv_aliases;
rb_map<name, name, name_quick_cmp> m_level_aliases;
rb_map<name, name, name_quick_cmp> m_inv_level_aliases;
bool m_in_section_or_context;
name_map<list<name>> m_aliases;
name_map<name> m_inv_aliases;
name_map<name> m_level_aliases;
name_map<name> m_inv_level_aliases;
state():m_in_section_or_context(false) {}
void add_expr_alias(name const & a, name const & e) {

10
src/library/coercion.cpp
View file

@ -56,12 +56,12 @@ struct coercion_info {
};
struct coercion_state {
rb_map<name, list<coercion_info>, name_quick_cmp> m_coercion_info;
name_map<list<coercion_info>> m_coercion_info;
// m_from and m_to contain "direct" coercions
typedef std::tuple<coercion_class, expr, expr> from_data;
rb_map<name, list<from_data>, name_quick_cmp> m_from; // map user-class -> list of (class, coercion-fun)
rb_map<coercion_class, list<name>, coercion_class_cmp_fn> m_to;
rb_map<name, pair<name, unsigned>, name_quick_cmp> m_coercions; // map coercion -> (from-class, num-args)
typedef std::tuple<coercion_class, expr, expr> from_data;
name_map<list<from_data>> m_from; // map user-class -> list of (class, coercion-fun)
rb_map<coercion_class, list<name>, coercion_class_cmp_fn> m_to;
name_map<pair<name, unsigned>> m_coercions; // map coercion -> (from-class, num-args)
template<typename F>
void for_each_info(name const & from, coercion_class const & to, F && f) {

4
src/library/private.cpp
View file

@ -13,8 +13,8 @@ Author: Leonardo de Moura
namespace lean {
struct private_ext : public environment_extension {
unsigned m_counter;
rb_map<name, name, name_quick_cmp> m_inv_map; // map: hidden-name -> user-name
unsigned m_counter;
name_map<name> m_inv_map; // map: hidden-name -> user-name
private_ext():m_counter(0) {}
};

6
src/library/scoped_ext.h
View file

@ -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<state> m_scopes;
rb_map<name, list<entry>, name_quick_cmp> m_entries;
state m_state;
list<state> m_scopes;
name_map<list<entry>> m_entries;
void using_namespace_core(environment const & env, io_state const & ios, name const & n) {
if (auto it = m_entries.find(n)) {

4
src/library/unifier.cpp
View file

@ -290,8 +290,8 @@ struct unifier_fn {
};
typedef rb_tree<cnstr, cnstr_cmp> cnstr_set;
typedef rb_tree<unsigned, unsigned_cmp> cnstr_idx_set;
typedef rb_map<name, cnstr_idx_set, name_quick_cmp> name_to_cnstrs;
typedef rb_map<name, unsigned, name_quick_cmp> owned_map;
typedef name_map<cnstr_idx_set> name_to_cnstrs;
typedef name_map<unsigned> owned_map;
typedef rb_map<expr, pair<expr, justification>, expr_quick_cmp> expr_map;
typedef std::unique_ptr<type_checker> type_checker_ptr;
environment m_env;