From acef1efb86bf3e8d4875fc83e3be8d2718624f25 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Jan 2017 22:59:50 -0800 Subject: [PATCH] fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function --- src/frontends/lean/pp.cpp | 8 +++---- src/library/equations_compiler/elim_match.cpp | 2 +- src/library/equations_compiler/util.cpp | 6 ++++-- src/library/string.cpp | 21 +++++++++++++++---- src/library/string.h | 7 +++++-- src/library/tactic/smt/congruence_closure.cpp | 6 ++++-- src/library/util.cpp | 14 +++++++++++++ src/library/util.h | 2 ++ tests/lean/pp_char_bug.lean | 6 ++++++ tests/lean/pp_char_bug.lean.expected.out | 6 ++++++ 10 files changed, 63 insertions(+), 15 deletions(-) create mode 100644 tests/lean/pp_char_bug.lean create mode 100644 tests/lean/pp_char_bug.lean.expected.out diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b014cc3b83..cf23df32c3 100644 --- a/src/frontends/lean/pp.cpp +++ b/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); diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index e5103c2d12..aec311fce8 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/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())) diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index bdf4e5b1e0..e1bdfc56e2 100644 --- a/src/library/equations_compiler/util.cpp +++ b/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); }} diff --git a/src/library/string.cpp b/src/library/string.cpp index f93ab79a90..f862bc4ed9 100644 --- a/src/library/string.cpp +++ b/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 to_char(expr const & e) { +optional to_char_core(expr const & e) { buffer args; expr const & fn = get_app_args(e, args); if (fn == *g_fin_mk && args.size() == 3) { @@ -193,12 +194,24 @@ optional to_char(expr const & e) { } } -bool is_char_value(expr const & e) { - return static_cast(to_char(e)); +bool is_char_value_core(expr const & e) { + return static_cast(to_char_core(e)); +} + +optional 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(); +} + +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 { diff --git a/src/library/string.h b/src/library/string.h index 8078bf0127..b6e77d1123 100644 --- a/src/library/string.h +++ b/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 expand_string_macro(expr const & e); -optional to_char(expr const & e); -bool is_char_value(expr const & e); +optional to_char_core(expr const & e); +bool is_char_value_core(expr const & e); + +optional 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); diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp index 39c4106f4e..93127949ab 100644 --- a/src/library/tactic/smt/congruence_closure.cpp +++ b/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); diff --git a/src/library/util.cpp b/src/library/util.cpp index bb26e933fb..7551c4bbb6 100644 --- a/src/library/util.cpp +++ b/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; diff --git a/src/library/util.h b/src/library/util.h index ab7e2616db..592d602345 100644 --- a/src/library/util.h +++ b/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); diff --git a/tests/lean/pp_char_bug.lean b/tests/lean/pp_char_bug.lean new file mode 100644 index 0000000000..7868eba4a7 --- /dev/null +++ b/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" diff --git a/tests/lean/pp_char_bug.lean.expected.out b/tests/lean/pp_char_bug.lean.expected.out new file mode 100644 index 0000000000..d16fe890c5 --- /dev/null +++ b/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"