chore(util/list): add inline functions for commonly used patterns in list processing code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<name>(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<name> 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 ptr_to_list(s.m_instances.find(c));
-        return *it;
-    else
-        return list<name>();
 }
 
 environment add_instance_cmd(parser & p) {

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>(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); }

src/frontends/lean/notation_cmd.cpp

@@ -106,21 +106,13 @@ static std::pair<notation_entry, optional<token_entry>> parse_mixfix_notation(pa
     char const * tks = tk.c_str();
     switch (k) {
     case mixfix_kind::infixl:
-        return mk_pair(notation_entry(false, list<transition>(transition(tks, mk_expr_action(*prec))),
+        return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), mk_app(f, Var(1), Var(0)), overload), new_token);
-                                      mk_app(f, Var(1), Var(0)), overload),
-                       new_token);
     case mixfix_kind::infixr:
-        return mk_pair(notation_entry(false, list<transition>(transition(tks, mk_expr_action(*prec-1))),
+        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);
-                                      mk_app(f, Var(1), Var(0)), overload),
-                       new_token);
     case mixfix_kind::postfix:
-        return mk_pair(notation_entry(false, list<transition>(transition(tks, mk_skip_action())),
+        return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())), mk_app(f, Var(0)), overload), new_token);
-                                      mk_app(f, Var(0)), overload),
-                       new_token);
     case mixfix_kind::prefix:
-        return mk_pair(notation_entry(true, list<transition>(transition(tks, mk_expr_action(*prec))),
+        return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))), mk_app(f, Var(0)), overload), new_token);
-                                      mk_app(f, Var(0)), overload),
-                       new_token);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }

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<expr>(a);
+            r.m_ptr->m_accept = to_list(a);
         else
-            r.m_ptr->m_accept = list<expr>(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;

src/frontends/lean/tactic_hint.cpp

@@ -80,10 +80,7 @@ typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
 
 list<tactic_hint_entry> 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 ptr_to_list(s.m_class_tactics.find(c));
-        return *it;
-    else
-        return list<tactic_hint_entry>();
 }
 
 list<tactic_hint_entry> get_tactic_hints(environment const & env) {

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<name>(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<name>(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<state>(m_state, m_scopes);
+        m_scopes = cons(m_state, m_scopes);
         m_state.m_in_section = in_section;
     }
 
@@ -151,8 +151,7 @@ optional<name> is_expr_aliased(environment const & env, name const & t) {
 }
 
 list<name> get_expr_aliases(environment const & env, name const & n) {
-    auto it = get_extension(env).m_state.m_aliases.find(n);
+    return ptr_to_list(get_extension(env).m_state.m_aliases.find(n));
-    return it ? *it : list<name>();
 }
 
 static void check_no_shadow(environment const & env, name const & a) {

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<std::pair<coercion_class, expr>>(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<name>(C));
+            m_to.insert(D, to_list(C));
         else if (std::find(it2->begin(), it2->end(), C) == it2->end())
-            m_to.insert(D, list<name>(C, *it2));
+            m_to.insert(D, cons(C, *it2));
     }
 };
 
@@ -240,7 +240,7 @@ struct add_coercion_fn {
         } else {
             list<coercion_info> infos = *it;
             infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; });
-            infos = list<coercion_info>(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))

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>(v));
+            m_map.insert(h, to_list(v));
     }
     template<typename F> void for_each(F && f) const { m_map.for_each(f); }
     template<typename F> void for_each_entry(F && f) const {

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>(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<normalizer_extension>(new inductive_normalizer_extension()),
                                           std::unique_ptr<normalizer_extension>(new record_normalizer_extension())));

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<void(serializer &)> const & wr) {
     module_ext ext = get_extension(env);
-    ext.m_writers  = list<writer>(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<inductive::intro_rule> const & intro_rules) {
-    return add_inductive(env, level_params, num_params, list<inductive::inductive_decl>(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);

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<name>(new_n, ext.m_namespaces);
+    ext.m_namespaces = cons(new_n, ext.m_namespaces);
-    ext.m_in_section = list<bool>(n.is_anonymous(), ext.m_in_section);
+    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);

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<entry>(e, *it));
+            m_entries.insert(n, cons(e, *it));
         else
-            m_entries.insert(n, list<entry>(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<state>(m_state, r.m_scopes);
+        r.m_scopes     = cons(m_state, r.m_scopes);
         return r;
     }
 

src/library/simplifier/ceq.cpp

@@ -29,7 +29,7 @@ class to_ceqs_fn {
     unsigned                         m_idx;
 
     static list<expr_pair> mk_singleton(expr const & e, expr const & H) {
-        return list<expr_pair>(mk_pair(e, H));
+        return to_list(mk_pair(e, H));
     }
 
     expr lift_free_vars(expr const & e, unsigned d) {

src/tests/util/serializer.cpp

@@ -49,7 +49,7 @@ public:
                 if (d.read_bool()) {
                     int h       = d.read_int();
                     list<int> t = read();
-                    return list<int>(h, t);
+                    return cons(h, t);
                 } else {
                     return list<int>();
                 }

src/util/list.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <iterator>
 #include "util/rc.h"
 #include "util/debug.h"
+#include "util/optional.h"
 
 namespace lean {
 /**
@@ -141,6 +142,10 @@ public:
 template<typename T> inline list<T>         cons(T const & h, list<T> const & t) { return list<T>(h, t); }
 template<typename T> inline T const &       car(list<T> const & l) { return head(l); }
 template<typename T> inline list<T> const & cdr(list<T> const & l) { return tail(l); }
+template<typename T> inline list<T>         to_list(T const & v) { return list<T>(v); }
+template<typename T> inline list<T>         to_list(optional<T> const & v) { return v ? to_list(*v) : list<T>(); }
+template<typename T> inline list<T>         to_list(T const * v) { return v ? to_list(*v) : list<T>(); }
+template<typename T> inline list<T>         ptr_to_list(list<T> const * l) { return l ? *l : list<T>(); }
 
 template<typename T> inline std::ostream & operator<<(std::ostream & out, list<T> const & l) {
     out << "(";