feat(library/tactic/rewrite_tactic): display list of overloads occurring in a failed rewrite step

src/library/choice.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include "util/sstream.h"
+#include "kernel/for_each_fn.h"
 #include "library/choice.h"
 #include "library/kernel_bindings.h"
 #include "library/kernel_serializer.h"
@@ -42,6 +43,46 @@ expr mk_choice(unsigned num_es, expr const * es) {
         return mk_macro(*g_choice, num_es, es);
 }
 
+list<list<name>> collect_choice_symbols(expr const & e) {
+    buffer<list<name>> r;
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_choice(e)) {
+                buffer<name> cs;
+                for (unsigned i = 0; i < get_num_choices(e); i++) {
+                    expr const & c = get_app_fn(get_choice(e, i));
+                    if (is_constant(c))
+                        cs.push_back(const_name(c));
+                    else if (is_local(c))
+                        cs.push_back(local_pp_name(c));
+                }
+                if (cs.size() > 1)
+                    r.push_back(to_list(cs));
+            }
+            return true;
+        });
+    return to_list(r);
+}
+
+format pp_choice_symbols(expr const & e) {
+    list<list<name>> symbols = collect_choice_symbols(e);
+    if (symbols) {
+        format r;
+        bool first = true;
+        for (auto cs : symbols) {
+            format aux("overloads:");
+            for (auto s : cs)
+                aux += space() + format(s);
+            if (!first)
+                r += line();
+            r += aux;
+            first = false;
+        }
+        return r;
+    } else {
+        return format();
+    }
+}
+
 void initialize_choice() {
     g_choice_name   = new name("choice");
     g_choice_opcode = new std::string("Choice");

src/library/choice.h

@@ -34,6 +34,17 @@ unsigned get_num_choices(expr const & e);
    \pre i < get_num_choices(e)
 */
 expr const & get_choice(expr const & e, unsigned i);
+
+/**
+   \brief Collect "choices" occurring in \c e.
+   For example, if \c e contains [choice (f a) (g a)] where f and g are constants,
+   the result contains the list [f, g]. This function is only used for producing nicer
+   error messages.
+*/
+list<list<name>> collect_choice_symbols(expr const & e);
+/** \brief Format the result produced by collect_choice_symbols. */
+format pp_choice_symbols(expr const & e);
+
 void open_choice(lua_State * L);
 void initialize_choice();
 void finalize_choice();

src/library/tactic/rewrite_tactic.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/expr_lt.h"
 #include "library/match.h"
+#include "library/choice.h"
 #include "library/projection.h"
 #include "library/local_context.h"
 #include "library/unifier.h"
@@ -1096,6 +1097,11 @@ class rewrite_fn {
             for (target_trace const & t : m_targets) {
                 r += t.pp(fmt);
             }
+            format cs = pp_choice_symbols(m_lemma);
+            if (!cs.is_nil()) {
+                r += line() + format("rewrite lemma uses the following overloaded symbols");
+                r += nest(get_pp_indent(fmt.get_options()), line() + cs);
+            }
             return r;
         }
     };

src/util/sexpr/format.cpp

@@ -224,7 +224,7 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n
     {
         sexpr list  = sexpr_compose_list(s);
         int len = 0;
-        while (!is_nil(list) && !found_newline) {
+        while (list && !found_newline) {
             sexpr const & h = car(list);
             list = cdr(list);
             len += space_upto_line_break(h, available, found_newline);

src/util/sexpr/format.h

@@ -182,6 +182,7 @@ public:
     format_kind kind() const {
         return sexpr_kind(m_value);
     }
+    bool is_nil() const { return kind() == format_kind::NIL; }
     unsigned hash() const { return m_value.hash(); }
 
     explicit operator bool() const { return static_cast<bool>(m_value); }