fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function

src/frontends/lean/pp.cpp

@@ -579,7 +579,7 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul
         }
         if (m_strings) {
             if (auto r = to_string(e)) return pp_string_literal(*r);
-            if (auto r = to_char(e)) return pp_char_literal(*r);
+            if (auto r = to_char(m_ctx, e)) return pp_char_literal(*r);
         }
         expr const & f = app_fn(e);
         if (is_implicit(f)) {
@@ -1195,7 +1195,7 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) ->
         }
         if (m_strings) {
             if (auto r = to_string(e)) return pp_string_literal(*r);
-            if (auto r = to_char(e))   return pp_char_literal(*r);
+            if (auto r = to_char(m_ctx, e))   return pp_char_literal(*r);
         }
         expr const & f = app_fn(e);
         if (is_implicit(f)) {
@@ -1572,8 +1572,8 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
         if (auto n = to_num_core(e)) return pp_num(*n);
     }
     if (m_strings) {
-        if (auto r = to_string(e)) return pp_string_literal(*r);
-        if (auto r = to_char(e))   return pp_char_literal(*r);
+        if (auto r = to_string(e))      return pp_string_literal(*r);
+        if (auto r = to_char(m_ctx, e)) return pp_char_literal(*r);
     }
     if (auto t = is_proof(e)) {
         return pp_proof_type(*t);

src/library/equations_compiler/elim_match.cpp

@@ -285,7 +285,7 @@ struct elim_match_fn {
 
     bool is_value(type_context & ctx, expr const & e) {
         if (!m_use_ite) return false;
-        if (to_char(e) || to_string(e)) return true;
+        if (to_char(ctx, e) || to_string(e)) return true;
         if (is_signed_num(e)) {
             expr type = ctx.infer(e);
             if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type()))

src/library/equations_compiler/util.cpp

@@ -348,13 +348,15 @@ static bool conservative_is_def_eq(type_context & ctx, expr const & a, expr cons
 }
 
 static lbool compare_values(expr const & a, expr const & b) {
+    /* We know 'a' and 'b' are values. So, we don't need
+       to check the type here. */
     if (auto v1 = to_num(a)) {
     if (auto v2 = to_num(b)) {
         return to_lbool(*v1 == *v2);
     }}
 
-    if (auto v1 = to_char(a)) {
-    if (auto v2 = to_char(b)) {
+    if (auto v1 = to_char_core(a)) {
+    if (auto v2 = to_char_core(b)) {
         return to_lbool(*v1 == *v2);
     }}
 

src/library/string.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/kernel_serializer.h"
 #include "library/string.h"
+#include "library/util.h"
 #include "library/constants.h"
 #include "library/num.h"
 #include "library/trace.h"
@@ -173,7 +174,7 @@ expr from_string(std::string const & s) {
     return mk_string_macro(s);
 }
 
-optional<char> to_char(expr const & e) {
+optional<char> to_char_core(expr const & e) {
     buffer<expr> args;
     expr const & fn = get_app_args(e, args);
     if (fn == *g_fin_mk && args.size() == 3) {
@@ -193,12 +194,24 @@ optional<char> to_char(expr const & e) {
     }
 }
 
-bool is_char_value(expr const & e) {
-    return static_cast<bool>(to_char(e));
+bool is_char_value_core(expr const & e) {
+    return static_cast<bool>(to_char_core(e));
+}
+
+optional<char> to_char(abstract_type_context & ctx, expr const & e) {
+    if (auto v = to_char_core(e)) {
+        if (ctx.is_def_eq(ctx.infer(e), mk_char_type()))
+            return v;
+    }
+    return optional<char>();
+}
+
+bool is_char_value(abstract_type_context & ctx, expr const & e) {
+    return is_char_value_core(e) && ctx.is_def_eq(ctx.infer(e), mk_char_type());
 }
 
 static bool append_char(expr const & e, std::string & r) {
-    if (auto c = to_char(e)) {
+    if (auto c = to_char_core(e)) {
         r.push_back(*c);
         return true;
     } else {

src/library/string.h

@@ -22,8 +22,11 @@ bool is_string_macro(expr const & e);
 /** \brief Expand string macro if 'e' is a string macro */
 optional<expr> expand_string_macro(expr const & e);
 
-optional<char> to_char(expr const & e);
-bool is_char_value(expr const & e);
+optional<char> to_char_core(expr const & e);
+bool is_char_value_core(expr const & e);
+
+optional<char> to_char(abstract_type_context & ctx, expr const & e);
+bool is_char_value(abstract_type_context & ctx, expr const & e);
 
 format pp_string_literal(std::string const & s);
 format pp_char_literal(char c);

src/library/tactic/smt/congruence_closure.cpp

@@ -624,13 +624,15 @@ void congruence_closure::mk_entry(expr const & e, bool interpreted) {
 /** Return true if 'e' represents a value (numeral, character, or string).
     TODO(Leo): move this code to a different place. */
 bool congruence_closure::is_value(expr const & e) {
-    return is_signed_num(e) || is_char_value(e) || is_string_value(e);
+    return is_signed_num(e) || is_char_value(m_ctx, e) || is_string_value(e);
 }
 
 /** Return true if 'e' represents a value (nat/int numereal, character, or string).
     TODO(Leo): move this code to a different place. */
 bool congruence_closure::is_interpreted_value(expr const & e) {
-    if (is_char_value(e) || is_string_value(e))
+    if (is_string_value(e))
+        return true;
+    if (is_char_value(m_ctx, e))
         return true;
     if (is_signed_num(e)) {
         expr type = m_ctx.infer(e);

src/library/util.cpp

@@ -502,6 +502,18 @@ static void finalize_int() {
 expr mk_int_type() { return *g_int; }
 bool is_int_type(expr const & e) { return e == *g_int; }
 
+static expr * g_char = nullptr;
+
+expr mk_char_type() { return *g_char; }
+
+static void initialize_char() {
+    g_char = new expr(mk_constant(get_char_name()));
+}
+
+static void finalize_char() {
+    delete g_char;
+}
+
 expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); }
 expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); }
 expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
@@ -979,11 +991,13 @@ void initialize_library_util() {
     g_and_elim_right = new expr(mk_constant(get_and_elim_right_name()));
     initialize_nat();
     initialize_int();
+    initialize_char();
 }
 
 void finalize_library_util() {
     finalize_int();
     finalize_nat();
+    finalize_char();
     delete g_true;
     delete g_true_intro;
     delete g_and;

src/library/util.h

@@ -184,6 +184,8 @@ expr mk_nat_add(expr const & e1, expr const & e2);
 expr mk_int_type();
 bool is_int_type(expr const & e);
 
+expr mk_char_type();
+
 bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f);
 bool is_ite(expr const & e);
 

tests/lean/pp_char_bug.lean

@@ -0,0 +1,6 @@
+check (fin.mk 2 dec_trivial : fin 5)
+check (fin.mk 1 dec_trivial : fin 3)
+check #"a"
+check to_string #"a"
+vm_eval to_string #"a"
+vm_eval #"a"

tests/lean/pp_char_bug.lean.expected.out

@@ -0,0 +1,6 @@
+fin.mk 2 (of_as_true trivial) : fin 5
+fin.mk 1 (of_as_true trivial) : fin 3
+#"a" : char
+to_string #"a" : string
+"#\"a\""
+#"a"