diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2cefa6f76b..7b5194d16e 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -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 cache; + expr_map cache; std::function convert = [&](expr const & e) { return replace(e, [&](expr const e, unsigned) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0445d1ef3c..b81639978c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1507,7 +1507,7 @@ struct to_pattern_fn { parser & m_parser; buffer & m_new_locals; name_map m_locals_map; // local variable name --> its interpretation - expr_struct_map m_anonymous_vars; // for _ + expr_map m_anonymous_vars; // for _ to_pattern_fn(parser & p, buffer & new_locals): diff --git a/src/kernel/equiv_manager.h b/src/kernel/equiv_manager.h index 76e0491a5a..be440eabc8 100644 --- a/src/kernel/equiv_manager.h +++ b/src/kernel/equiv_manager.h @@ -17,9 +17,9 @@ class equiv_manager { unsigned m_rank; }; - std::vector m_nodes; - expr_struct_map m_to_node; - bool m_use_hash; + std::vector m_nodes; + expr_map m_to_node; + bool m_use_hash; node_ref mk_node(); node_ref find(node_ref n); diff --git a/src/kernel/expr_maps.h b/src/kernel/expr_maps.h index 33c6285981..8b81b7bb80 100644 --- a/src/kernel/expr_maps.h +++ b/src/kernel/expr_maps.h @@ -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 -using expr_struct_map = typename std::unordered_map>; +using expr_map = typename std::unordered_map>; // The following map also takes into account binder information template -using expr_bi_struct_map = typename std::unordered_map; +using expr_bi_map = typename std::unordered_map; template -class expr_cond_bi_struct_map : public std::unordered_map { +class expr_cond_bi_map : public std::unordered_map { public: - expr_cond_bi_struct_map(bool use_bi = false): + expr_cond_bi_map(bool use_bi = false): std::unordered_map(10, expr_hash(), is_cond_bi_equal_proc(use_bi)) {} }; }; diff --git a/src/kernel/expr_sets.h b/src/kernel/expr_sets.h index 125d0d08f9..897ba160f9 100644 --- a/src/kernel/expr_sets.h +++ b/src/kernel/expr_sets.h @@ -12,5 +12,5 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { -typedef std::unordered_set> expr_struct_set; +typedef std::unordered_set> expr_set; } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 970874f5dc..f06b4cfb91 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -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 cache; + typedef expr_bi_map cache; typedef std::unordered_set 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 m_whnf_core_cache; - expr_struct_map m_whnf_cache; + expr_map m_whnf_core_cache; + expr_map m_whnf_cache; equiv_manager m_eqv_manager; expr_pair_set m_failure_cache; level_param_names const * m_params; diff --git a/src/library/check.cpp b/src/library/check.cpp index 51af1bc022..4d5f42def7 100644 --- a/src/library/check.cpp +++ b/src/library/check.cpp @@ -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)); diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp index 1f89a6f28c..3cff1862fd 100644 --- a/src/library/compiler/cse.cpp +++ b/src/library/compiler/cse.cpp @@ -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 m_num_occs; + expr_set const & m_candidates; + expr_map 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 const & get_num_occs() const { return m_num_occs; } + collect_num_occs_fn(expr_set const & cs):m_candidates(cs) {} + expr_map const & get_num_occs() const { return m_num_occs; } }; void collect_common_subexprs(buffer 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 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 m_common_subexpr_to_local; + unsigned & m_counter; + expr_set const & m_common_subexprs; + expr_map 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 m_new_locals; + buffer 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); diff --git a/src/library/compiler/extract_values.cpp b/src/library/compiler/extract_values.cpp index 22767925f5..63b9643d98 100644 --- a/src/library/compiler/extract_values.cpp +++ b/src/library/compiler/extract_values.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura namespace lean { class extract_values_fn : public compiler_step_visitor { name m_prefix; - expr_struct_map m_cache; + expr_map m_cache; unsigned m_idx{1}; buffer m_new_procs; expr m_root; diff --git a/src/library/context_cache.h b/src/library/context_cache.h index 8a75776639..bf06ebb47c 100644 --- a/src/library/context_cache.h +++ b/src/library/context_cache.h @@ -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 infer_cache; - typedef expr_struct_map whnf_cache; - typedef expr_struct_map> instance_cache; - typedef expr_struct_map> subsingleton_cache; + typedef expr_cond_bi_map infer_cache; + typedef expr_map whnf_cache; + typedef expr_map> instance_cache; + typedef expr_map> subsingleton_cache; typedef std::unordered_set 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 fi_cache; + typedef expr_map fi_cache; typedef expr_unsigned_map fi_cache_nargs; - typedef expr_struct_map ss_cache; + typedef expr_map ss_cache; typedef expr_unsigned_map ss_cache_nargs; typedef expr_unsigned_map prefix_cache; fi_cache m_fi_cache[LEAN_NUM_TRANSPARENCY_MODES]; diff --git a/src/library/export.cpp b/src/library/export.cpp index def60cd72e..762cdd0825 100644 --- a/src/library/export.cpp +++ b/src/library/export.cpp @@ -28,7 +28,7 @@ class exporter { std::unordered_set m_exported; name_hmap m_name2idx; level_map m_level2idx; - expr_bi_struct_map m_expr2idx; + expr_bi_map m_expr2idx; bool m_quotient_exported = false; unsigned export_name(name const & n) { diff --git a/src/library/locals.cpp b/src/library/locals.cpp index 0fc1cdf86f..a6d033d1f1 100644 --- a/src/library/locals.cpp +++ b/src/library/locals.cpp @@ -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 visit = [&](expr const & e) { if (!has_local(e)) return; diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index cc632b319e..06ed9c14ee 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -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())) { diff --git a/src/library/replace_visitor.h b/src/library/replace_visitor.h index a6f451e79c..6edaa7aec8 100644 --- a/src/library/replace_visitor.h +++ b/src/library/replace_visitor.h @@ -15,7 +15,7 @@ namespace lean { redefine the visit_* methods. */ class replace_visitor { protected: - typedef expr_bi_struct_map cache; + typedef expr_bi_map cache; cache m_cache; expr save_result(expr const & e, expr && r, bool shared); virtual expr visit_sort(expr const &); diff --git a/src/library/tactic/ac_tactics.cpp b/src/library/tactic/ac_tactics.cpp index 14faf06bb3..ec1cec811c 100644 --- a/src/library/tactic/ac_tactics.cpp +++ b/src/library/tactic/ac_tactics.cpp @@ -20,9 +20,9 @@ Author: Leonardo de Moura namespace lean { struct ac_manager_old::cache { - environment m_env; - expr_struct_map> m_assoc_cache[2]; - expr_struct_map> m_comm_cache[2]; + environment m_env; + expr_map> m_assoc_cache[2]; + expr_map> m_comm_cache[2]; cache(environment const & env): m_env(env) { } diff --git a/src/library/tactic/algebraic_normalizer.h b/src/library/tactic/algebraic_normalizer.h index 68a3d9a7f6..6026f731c5 100644 --- a/src/library/tactic/algebraic_normalizer.h +++ b/src/library/tactic/algebraic_normalizer.h @@ -93,7 +93,7 @@ public: local_context m_lctx; name_set m_symbols; head_map> m_head_info; - expr_struct_map m_op_info; + expr_map m_op_info; }; typedef std::shared_ptr data_ptr; diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h index a5d53d33c8..81f589adbc 100644 --- a/src/library/tactic/dsimplify.h +++ b/src/library/tactic/dsimplify.h @@ -48,7 +48,7 @@ class dsimplify_core_fn { protected: type_context_old & m_ctx; defeq_canonizer m_defeq_canonizer; - expr_struct_map m_cache; + expr_map m_cache; unsigned m_num_steps; bool m_need_restart; dsimp_config m_cfg; diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index 7bc19e3d49..d1ac738b19 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -74,9 +74,9 @@ struct simp_config { */ class simplify_core_fn { protected: - typedef expr_struct_map simplify_cache; + typedef expr_map simplify_cache; - type_context_old & m_ctx; + type_context_old & m_ctx; defeq_canonizer m_defeq_canonizer; name m_rel; simp_lemmas m_slss;