max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): rename expr_struct_* to expr_*

Browse source 
We don't need to modifier `_struct` anymore since we don't use the
pointer equality based hashtables anymore.
This commit is contained in:
Leonardo de Moura 2018-04-09 12:55:48 -07:00
parent faf8e025e7
commit 8dd53cd94f
18 changed files with 50 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -394,7 +394,7 @@ static environment init_quotient_cmd(parser & p) {
After we convert the frontend to type_context_old, we will not need to use this procedure.
*/
static expr convert_metavars(metavar_context & mctx, expr const & e) {
expr_struct_map<expr> cache;
expr_map<expr> cache;
std::function<expr(expr const & e)> convert = [&](expr const & e) {
return replace(e, [&](expr const e, unsigned) {

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

@ -1507,7 +1507,7 @@ struct to_pattern_fn {
parser & m_parser;
buffer<expr> & m_new_locals;
name_map<expr> m_locals_map; // local variable name --> its interpretation
expr_struct_map<expr> m_anonymous_vars; // for _
expr_map<expr> m_anonymous_vars; // for _
to_pattern_fn(parser & p, buffer<expr> & new_locals):

6
src/kernel/equiv_manager.h
View file

@ -17,9 +17,9 @@ class equiv_manager {
unsigned m_rank;
};
std::vector<node> m_nodes;
expr_struct_map<node_ref> m_to_node;
bool m_use_hash;
std::vector<node> m_nodes;
expr_map<node_ref> m_to_node;
bool m_use_hash;
node_ref mk_node();
node_ref find(node_ref n);

8
src/kernel/expr_maps.h
View file

@ -12,15 +12,15 @@ Author: Leonardo de Moura
namespace lean {
// Maps based on structural equality. That is, two keys are equal iff they are structurally equal
template<typename T>
using expr_struct_map = typename std::unordered_map<expr, T, expr_hash, std::equal_to<expr>>;
using expr_map = typename std::unordered_map<expr, T, expr_hash, std::equal_to<expr>>;
// The following map also takes into account binder information
template<typename T>
using expr_bi_struct_map = typename std::unordered_map<expr, T, expr_hash, is_bi_equal_proc>;
using expr_bi_map = typename std::unordered_map<expr, T, expr_hash, is_bi_equal_proc>;
template<typename T>
class expr_cond_bi_struct_map : public std::unordered_map<expr, T, expr_hash, is_cond_bi_equal_proc> {
class expr_cond_bi_map : public std::unordered_map<expr, T, expr_hash, is_cond_bi_equal_proc> {
public:
expr_cond_bi_struct_map(bool use_bi = false):
expr_cond_bi_map(bool use_bi = false):
std::unordered_map<expr, T, expr_hash, is_cond_bi_equal_proc>(10, expr_hash(), is_cond_bi_equal_proc(use_bi)) {}
};
};

2
src/kernel/expr_sets.h
View file

@ -12,5 +12,5 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
typedef std::unordered_set<expr, expr_hash, std::equal_to<expr>> expr_struct_set;
typedef std::unordered_set<expr, expr_hash, std::equal_to<expr>> expr_set;
}

6
src/kernel/type_checker.h
View file

@ -27,15 +27,15 @@ class type_checker : public abstract_type_context {
Examples:
The type of (lambda x : A, t) is (Pi x : A, typeof(t))
The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t)) */
typedef expr_bi_struct_map<expr> cache;
typedef expr_bi_map<expr> cache;
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
environment m_env;
name_generator m_name_generator;
bool m_memoize;
bool m_trusted_only;
cache m_infer_type_cache[2];
expr_struct_map<expr> m_whnf_core_cache;
expr_struct_map<expr> m_whnf_cache;
expr_map<expr> m_whnf_core_cache;
expr_map<expr> m_whnf_cache;
equiv_manager m_eqv_manager;
expr_pair_set m_failure_cache;
level_param_names const * m_params;

2
src/library/check.cpp
View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
namespace lean {
struct check_fn {
type_context_old & m_ctx;
expr_struct_set m_visited;
expr_set m_visited;
void visit_constant(expr const & e) {
declaration d = m_ctx.env().get(const_name(e));

36
src/library/compiler/cse.cpp
View file

@ -23,7 +23,7 @@ class cse_fn : public compiler_step_visitor {
class visitor_fn {
protected:
expr_struct_set m_visited; /* do we need this? */
expr_set m_visited; /* do we need this? */
bool check_visited(expr const & e) {
if (m_visited.find(e) != m_visited.end())
@ -65,7 +65,7 @@ class cse_fn : public compiler_step_visitor {
class collect_candidates_fn : public visitor_fn {
environment const & m_env;
expr_struct_set m_candidates;
expr_set m_candidates;
void add_candidate(expr const & e) {
if (!closed(e)) return;
@ -94,12 +94,12 @@ class cse_fn : public compiler_step_visitor {
}
public:
collect_candidates_fn(environment const & env):m_env(env) {}
expr_struct_set const & get_candidates() const { return m_candidates; }
expr_set const & get_candidates() const { return m_candidates; }
};
class collect_num_occs_fn : public visitor_fn {
expr_struct_set const & m_candidates;
expr_struct_map<unsigned> m_num_occs;
expr_set const & m_candidates;
expr_map<unsigned> m_num_occs;
void add_occ(expr const & e) {
if (!closed(e)) return;
@ -127,12 +127,12 @@ class cse_fn : public compiler_step_visitor {
visit(arg);
}
public:
collect_num_occs_fn(expr_struct_set const & cs):m_candidates(cs) {}
expr_struct_map<unsigned> const & get_num_occs() const { return m_num_occs; }
collect_num_occs_fn(expr_set const & cs):m_candidates(cs) {}
expr_map<unsigned> const & get_num_occs() const { return m_num_occs; }
};
void collect_common_subexprs(buffer<expr> const & let_values, expr const & body,
expr_struct_set & r) {
expr_set & r) {
/* first pass */
collect_candidates_fn candidate_collector(m_ctx.env());
for (expr const & v : let_values) candidate_collector(v);
@ -149,20 +149,20 @@ class cse_fn : public compiler_step_visitor {
}
}
void collect_common_subexprs(expr const & e, expr_struct_set & r) {
void collect_common_subexprs(expr const & e, expr_set & r) {
buffer<expr> tmp;
collect_common_subexprs(tmp, e, r);
}
/* Helper functor for converting common subexpressions into fresh let-decls */
struct cse_processor {
unsigned & m_counter;
expr_struct_set const & m_common_subexprs;
expr_struct_map<expr> m_common_subexpr_to_local;
unsigned & m_counter;
expr_set const & m_common_subexprs;
expr_map<expr> m_common_subexpr_to_local;
type_context_old::tmp_locals m_all_locals; /* new local declarations, it also include let-decls for common-subexprs */
local_context const & m_lctx;
local_context const & m_lctx;
cse_processor(unsigned & counter, type_context_old & ctx, expr_struct_set const & s):
cse_processor(unsigned & counter, type_context_old & ctx, expr_set const & s):
m_counter(counter),
m_common_subexprs(s),
m_all_locals(ctx),
@ -198,9 +198,9 @@ class cse_fn : public compiler_step_visitor {
/* Similar to cse_processor, but has support for binding exprs (lambda and let) */
struct cse_processor_for_binding : public cse_processor {
type_context_old::tmp_locals const & m_locals;
buffer<expr> m_new_locals;
buffer<expr> m_new_locals;
cse_processor_for_binding(unsigned & counter, type_context_old & ctx, type_context_old::tmp_locals const & locals, expr_struct_set const & s):
cse_processor_for_binding(unsigned & counter, type_context_old & ctx, type_context_old::tmp_locals const & locals, expr_set const & s):
cse_processor(counter, ctx, s),
m_locals(locals) {
}
@ -250,7 +250,7 @@ class cse_fn : public compiler_step_visitor {
t = instantiate_rev(t, locals.size(), locals.data());
t = visit(t);
expr_struct_set common_subexprs;
expr_set common_subexprs;
collect_common_subexprs(let_values, t, common_subexprs);
if (common_subexprs.empty())
return copy_tag(e, locals.mk_lambda(t));
@ -279,7 +279,7 @@ class cse_fn : public compiler_step_visitor {
args[i] = visit(m);
} else {
m = visit(m);
expr_struct_set common_subexprs;
expr_set common_subexprs;
collect_common_subexprs(m, common_subexprs);
if (!common_subexprs.empty()) {
cse_processor proc(m_counter, m_ctx, common_subexprs);

2
src/library/compiler/extract_values.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
namespace lean {
class extract_values_fn : public compiler_step_visitor {
name m_prefix;
expr_struct_map<expr> m_cache;
expr_map<expr> m_cache;
unsigned m_idx{1};
buffer<procedure> m_new_procs;
expr m_root;

12
src/library/context_cache.h
View file

@ -30,10 +30,10 @@ class context_cache : public context_cacheless {
So, when we create a type_context_old_cache object we can specify whether this extra
level of precision is required or not. */
typedef expr_cond_bi_struct_map<expr> infer_cache;
typedef expr_struct_map<expr> whnf_cache;
typedef expr_struct_map<optional<expr>> instance_cache;
typedef expr_struct_map<optional<expr>> subsingleton_cache;
typedef expr_cond_bi_map<expr> infer_cache;
typedef expr_map<expr> whnf_cache;
typedef expr_map<optional<expr>> instance_cache;
typedef expr_map<optional<expr>> subsingleton_cache;
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> failure_cache;
/* Remark: we only cache inferred types if the metavariable assignment was not accessed.
@ -93,9 +93,9 @@ class context_cache : public context_cacheless {
/* Cache datastructures for fun_info */
typedef expr_struct_map<fun_info> fi_cache;
typedef expr_map<fun_info> fi_cache;
typedef expr_unsigned_map<fun_info> fi_cache_nargs;
typedef expr_struct_map<ss_param_infos> ss_cache;
typedef expr_map<ss_param_infos> ss_cache;
typedef expr_unsigned_map<ss_param_infos> ss_cache_nargs;
typedef expr_unsigned_map<unsigned> prefix_cache;
fi_cache m_fi_cache[LEAN_NUM_TRANSPARENCY_MODES];

2
src/library/export.cpp
View file

@ -28,7 +28,7 @@ class exporter {
std::unordered_set<name, name_hash> m_exported;
name_hmap<unsigned> m_name2idx;
level_map<unsigned> m_level2idx;
expr_bi_struct_map<unsigned> m_expr2idx;
expr_bi_map<unsigned> m_expr2idx;
bool m_quotient_exported = false;
unsigned export_name(name const & n) {

2
src/library/locals.cpp
View file

@ -62,7 +62,7 @@ void collected_locals::insert(expr const & l) {
void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
if (!has_local(e))
return;
expr_struct_set visited;
expr_set visited;
std::function<void(expr const & e)> visit = [&](expr const & e) {
if (!has_local(e))
return;

2
src/library/noncomputable.cpp
View file

@ -116,7 +116,7 @@ struct get_noncomputable_reason_fn {
type_checker & m_tc;
noncomputable_ext const & m_ext;
expr_struct_set m_cache;
expr_set m_cache;
get_noncomputable_reason_fn(type_checker & tc):
m_tc(tc), m_ext(get_extension(tc.env())) {

2
src/library/replace_visitor.h
View file

@ -15,7 +15,7 @@ namespace lean {
redefine the visit_* methods. */
class replace_visitor {
protected:
typedef expr_bi_struct_map<expr> cache;
typedef expr_bi_map<expr> cache;
cache m_cache;
expr save_result(expr const & e, expr && r, bool shared);
virtual expr visit_sort(expr const &);

6
src/library/tactic/ac_tactics.cpp
View file

@ -20,9 +20,9 @@ Author: Leonardo de Moura
namespace lean {
struct ac_manager_old::cache {
environment m_env;
expr_struct_map<optional<expr>> m_assoc_cache[2];
expr_struct_map<optional<expr>> m_comm_cache[2];
environment m_env;
expr_map<optional<expr>> m_assoc_cache[2];
expr_map<optional<expr>> m_comm_cache[2];
cache(environment const & env):
m_env(env) {
}

2
src/library/tactic/algebraic_normalizer.h
View file

@ -93,7 +93,7 @@ public:
local_context m_lctx;
name_set m_symbols;
head_map<pair<expr, algebraic_info_ref>> m_head_info;
expr_struct_map<algebraic_info_ref> m_op_info;
expr_map<algebraic_info_ref> m_op_info;
};
typedef std::shared_ptr<data> data_ptr;

2
src/library/tactic/dsimplify.h
View file

@ -48,7 +48,7 @@ class dsimplify_core_fn {
protected:
type_context_old & m_ctx;
defeq_canonizer m_defeq_canonizer;
expr_struct_map<expr> m_cache;
expr_map<expr> m_cache;
unsigned m_num_steps;
bool m_need_restart;
dsimp_config m_cfg;

4
src/library/tactic/simplify.h
View file

@ -74,9 +74,9 @@ struct simp_config {
*/
class simplify_core_fn {
protected:
typedef expr_struct_map<simp_result> simplify_cache;
typedef expr_map<simp_result> simplify_cache;
type_context_old & m_ctx;
type_context_old & m_ctx;
defeq_canonizer m_defeq_canonizer;
name m_rel;
simp_lemmas m_slss;