From 2dca68e6450a7a2b4ed5506ada5af742f21f2f92 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Aug 2014 13:50:48 -0700 Subject: [PATCH] chore(util/list): add inline functions for commonly used patterns in list processing code Signed-off-by: Leonardo de Moura --- src/frontends/lean/class.cpp | 7 ++----- src/frontends/lean/local_decls.h | 2 +- src/frontends/lean/notation_cmd.cpp | 16 ++++------------ src/frontends/lean/parse_table.cpp | 4 ++-- src/frontends/lean/tactic_hint.cpp | 5 +---- src/library/aliases.cpp | 9 ++++----- src/library/coercion.cpp | 8 ++++---- src/library/head_map.h | 2 +- src/library/hott_kernel.cpp | 2 +- src/library/module.cpp | 4 ++-- src/library/scoped_ext.cpp | 4 ++-- src/library/scoped_ext.h | 6 +++--- src/library/simplifier/ceq.cpp | 2 +- src/tests/util/serializer.cpp | 2 +- src/util/list.h | 5 +++++ 15 files changed, 34 insertions(+), 44 deletions(-) diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 7a9a8d3c8..19b574b0a 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -24,7 +24,7 @@ struct class_state { void add_instance(name const & c, name const & i) { auto it = m_instances.find(c); if (!it) - m_instances.insert(c, list(i)); + m_instances.insert(c, to_list(i)); else m_instances.insert(c, cons(i, filter(*it, [&](name const & i1) { return i1 != i; }))); } @@ -83,10 +83,7 @@ bool is_class(environment const & env, name const & c) { list get_class_instances(environment const & env, name const & c) { class_state const & s = class_ext::get_state(env); - if (auto it = s.m_instances.find(c)) - return *it; - else - return list(); + return ptr_to_list(s.m_instances.find(c)); } environment add_instance_cmd(parser & p) { diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h index 35b6c8e6c..53dedb61d 100644 --- a/src/frontends/lean/local_decls.h +++ b/src/frontends/lean/local_decls.h @@ -28,7 +28,7 @@ class local_decls { public: local_decls():m_counter(1) {} local_decls(local_decls const & d):m_map(d.m_map), m_counter(d.m_counter), m_scopes(d.m_scopes) {} - void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; m_values = list(v, m_values); } + void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; m_values = cons(v, m_values); } V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; } unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; } bool contains(name const & k) const { return m_map.contains(k); } diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index d160bfec5..d6cf0bc23 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -106,21 +106,13 @@ static std::pair> parse_mixfix_notation(pa char const * tks = tk.c_str(); switch (k) { case mixfix_kind::infixl: - return mk_pair(notation_entry(false, list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(1), Var(0)), overload), - new_token); + return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), mk_app(f, Var(1), Var(0)), overload), new_token); case mixfix_kind::infixr: - return mk_pair(notation_entry(false, list(transition(tks, mk_expr_action(*prec-1))), - mk_app(f, Var(1), Var(0)), overload), - new_token); + return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))), mk_app(f, Var(1), Var(0)), overload), new_token); case mixfix_kind::postfix: - return mk_pair(notation_entry(false, list(transition(tks, mk_skip_action())), - mk_app(f, Var(0)), overload), - new_token); + return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())), mk_app(f, Var(0)), overload), new_token); case mixfix_kind::prefix: - return mk_pair(notation_entry(true, list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(0)), overload), - new_token); + return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))), mk_app(f, Var(0)), overload), new_token); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index b4353cfd5..b3d538da8 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -274,9 +274,9 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons parse_table r(new cell(*m_ptr)); if (num == 0) { if (!overload) - r.m_ptr->m_accept = list(a); + r.m_ptr->m_accept = to_list(a); else - r.m_ptr->m_accept = list(a, remove(r.m_ptr->m_accept, a)); + r.m_ptr->m_accept = cons(a, remove(r.m_ptr->m_accept, a)); } else { auto * it = r.m_ptr->m_children.find(ts->get_token()); parse_table new_child; diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp index 0689ff9eb..63ae1a51d 100644 --- a/src/frontends/lean/tactic_hint.cpp +++ b/src/frontends/lean/tactic_hint.cpp @@ -80,10 +80,7 @@ typedef scoped_ext tactic_hint_ext; list get_tactic_hints(environment const & env, name const & c) { tactic_hint_state const & s = tactic_hint_ext::get_state(env); - if (auto it = s.m_class_tactics.find(c)) - return *it; - else - return list(); + return ptr_to_list(s.m_class_tactics.find(c)); } list get_tactic_hints(environment const & env) { diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 3746c8983..23bd7822d 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -34,9 +34,9 @@ struct aliases_ext : public environment_extension { void add_expr_alias(name const & a, name const & e) { auto it = m_aliases.find(a); if (it) - m_aliases.insert(a, list(e, filter(*it, [&](name const & t) { return t != e; }))); + m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; }))); else - m_aliases.insert(a, list(e)); + m_aliases.insert(a, to_list(e)); m_inv_aliases.insert(e, a); } }; @@ -79,7 +79,7 @@ struct aliases_ext : public environment_extension { } void push(bool in_section) { - m_scopes = list(m_state, m_scopes); + m_scopes = cons(m_state, m_scopes); m_state.m_in_section = in_section; } @@ -151,8 +151,7 @@ optional is_expr_aliased(environment const & env, name const & t) { } list get_expr_aliases(environment const & env, name const & n) { - auto it = get_extension(env).m_state.m_aliases.find(n); - return it ? *it : list(); + return ptr_to_list(get_extension(env).m_state.m_aliases.find(n)); } static void check_no_shadow(environment const & env, name const & a) { diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index c08cc3b75..9aee122a9 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -84,7 +84,7 @@ struct coercion_state { void update_from_to(name const & C, coercion_class const & D, expr const & f, io_state const & ios) { auto it1 = m_from.find(C); if (!it1) { - m_from.insert(C, list>(mk_pair(D, f))); + m_from.insert(C, to_list(mk_pair(D, f))); } else { auto it = it1->begin(); auto end = it1->end(); @@ -98,9 +98,9 @@ struct coercion_state { } auto it2 = m_to.find(D); if (!it2) - m_to.insert(D, list(C)); + m_to.insert(D, to_list(C)); else if (std::find(it2->begin(), it2->end(), C) == it2->end()) - m_to.insert(D, list(C, *it2)); + m_to.insert(D, cons(C, *it2)); } }; @@ -240,7 +240,7 @@ struct add_coercion_fn { } else { list infos = *it; infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; }); - infos = list(coercion_info(f, f_type, ls, num_args, cls), infos); + infos = cons(coercion_info(f, f_type, ls, num_args, cls), infos); m_state.m_coercion_info.insert(C, infos); } if (is_constant(f)) diff --git a/src/library/head_map.h b/src/library/head_map.h index 43dbcd011..0da50d413 100644 --- a/src/library/head_map.h +++ b/src/library/head_map.h @@ -51,7 +51,7 @@ public: if (auto it = m_map.find(h)) m_map.insert(h, cons(v, filter(*it, [&](V const & v2) { return v != v2; }))); else - m_map.insert(h, list(v)); + m_map.insert(h, to_list(v)); } template void for_each(F && f) const { m_map.for_each(f); } template void for_each_entry(F && f) const { diff --git a/src/library/hott_kernel.cpp b/src/library/hott_kernel.cpp index f85394252..ec53b9c4e 100644 --- a/src/library/hott_kernel.cpp +++ b/src/library/hott_kernel.cpp @@ -18,7 +18,7 @@ environment mk_hott_environment(unsigned trust_lvl) { false /* Type.{0} is proof relevant */, true /* Eta */, false /* Type.{0} is predicative */, - list(name("Id")) /* Exact equality types are proof irrelevant */, + to_list(name("Id")) /* Exact equality types are proof irrelevant */, /* builtin support for inductive and record datatypes */ compose(std::unique_ptr(new inductive_normalizer_extension()), std::unique_ptr(new record_normalizer_extension()))); diff --git a/src/library/module.cpp b/src/library/module.cpp index ed60d5d7c..1c9d5fada 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -126,7 +126,7 @@ static std::string g_decl_key("decl"); namespace module { environment add(environment const & env, std::string const & k, std::function const & wr) { module_ext ext = get_extension(env); - ext.m_writers = list(writer(k, wr), ext.m_writers); + ext.m_writers = cons(writer(k, wr), ext.m_writers); return update(env, ext); } @@ -169,7 +169,7 @@ static void inductive_reader(deserializer & d, module_idx, shared_environment & environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params, unsigned num_params, expr const & type, list const & intro_rules) { - return add_inductive(env, level_params, num_params, list(inductive::inductive_decl(ind_name, type, intro_rules))); + return add_inductive(env, level_params, num_params, to_list(inductive::inductive_decl(ind_name, type, intro_rules))); } static register_module_object_reader_fn g_reg_ind_reader(g_inductive, inductive_reader); diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp index d45d2d9d4..792725dbc 100644 --- a/src/library/scoped_ext.cpp +++ b/src/library/scoped_ext.cpp @@ -91,8 +91,8 @@ environment push_scope(environment const & env, io_state const & ios, name const save_ns = true; ext.m_namespace_set.insert(new_n); } - ext.m_namespaces = list(new_n, ext.m_namespaces); - ext.m_in_section = list(n.is_anonymous(), ext.m_in_section); + ext.m_namespaces = cons(new_n, ext.m_namespaces); + ext.m_in_section = cons(n.is_anonymous(), ext.m_in_section); environment r = update(env, ext); for (auto const & t : get_exts()) { r = std::get<2>(t)(r, in_section); diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index b3010673a..0e9fe24a5 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -78,9 +78,9 @@ class scoped_ext : public environment_extension { void register_entry_core(name n, entry const & e) { if (auto it = m_entries.find(n)) - m_entries.insert(n, list(e, *it)); + m_entries.insert(n, cons(e, *it)); else - m_entries.insert(n, list(e)); + m_entries.insert(n, to_list(e)); } void add_entry_core(environment const & env, io_state const & ios, entry const & e) { @@ -118,7 +118,7 @@ public: scoped_ext push() const { scoped_ext r(*this); - r.m_scopes = list(m_state, r.m_scopes); + r.m_scopes = cons(m_state, r.m_scopes); return r; } diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 1ff223397..75ba55032 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -29,7 +29,7 @@ class to_ceqs_fn { unsigned m_idx; static list mk_singleton(expr const & e, expr const & H) { - return list(mk_pair(e, H)); + return to_list(mk_pair(e, H)); } expr lift_free_vars(expr const & e, unsigned d) { diff --git a/src/tests/util/serializer.cpp b/src/tests/util/serializer.cpp index 47732bc06..b1491bfb7 100644 --- a/src/tests/util/serializer.cpp +++ b/src/tests/util/serializer.cpp @@ -49,7 +49,7 @@ public: if (d.read_bool()) { int h = d.read_int(); list t = read(); - return list(h, t); + return cons(h, t); } else { return list(); } diff --git a/src/util/list.h b/src/util/list.h index 74669a908..6849b75ef 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include "util/rc.h" #include "util/debug.h" +#include "util/optional.h" namespace lean { /** @@ -141,6 +142,10 @@ public: template inline list cons(T const & h, list const & t) { return list(h, t); } template inline T const & car(list const & l) { return head(l); } template inline list const & cdr(list const & l) { return tail(l); } +template inline list to_list(T const & v) { return list(v); } +template inline list to_list(optional const & v) { return v ? to_list(*v) : list(); } +template inline list to_list(T const * v) { return v ? to_list(*v) : list(); } +template inline list ptr_to_list(list const * l) { return l ? *l : list(); } template inline std::ostream & operator<<(std::ostream & out, list const & l) { out << "(";