From 6a9e5079c9c10ac1d3b730addfccca39aadd25bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 May 2016 16:20:43 -0700 Subject: [PATCH] feat(library,frontends/lean/pp): add support for new string encoding --- library/.project | 4 +- library/init/char.lean | 6 +- library/init/string.lean | 6 +- src/frontends/lean/parser.cpp | 16 +-- src/frontends/lean/parser.h | 2 - src/frontends/lean/pp.cpp | 15 +++ src/frontends/lean/pp.h | 1 + src/frontends/lean/token_table.cpp | 2 +- src/library/constants.cpp | 32 ++++- src/library/constants.h | 8 +- src/library/constants.txt | 8 +- src/library/init_module.cpp | 3 + src/library/num.cpp | 49 ++++++-- src/library/num.h | 7 +- src/library/pp_options.cpp | 11 ++ src/library/pp_options.h | 2 + src/library/string.cpp | 191 ++++++++++++++--------------- src/library/string.h | 14 +-- 18 files changed, 226 insertions(+), 151 deletions(-) diff --git a/library/.project b/library/.project index 1841071bc7..5eb55ae000 100644 --- a/library/.project +++ b/library/.project @@ -19,10 +19,10 @@ - matrix.lean - squash.lean - stream.lean -- string.lean +- old_string.lean - uprod.lean - tuple.lean -- fin.lean +- old_fin.lean - pnat.lean - hf.lean - data/vector/ diff --git a/library/init/char.lean b/library/init/char.lean index 9b7ca797fe..ac0a9f2a18 100644 --- a/library/init/char.lean +++ b/library/init/char.lean @@ -9,5 +9,9 @@ open nat definition char := fin 256 -definition char.of_nat (n : nat) : char := +namespace char + +definition of_nat [coercion] (n : nat) : char := if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial + +end char diff --git a/library/init/string.lean b/library/init/string.lean index b108395655..a56c87e979 100644 --- a/library/init/string.lean +++ b/library/init/string.lean @@ -8,5 +8,7 @@ import init.char definition string := list char -definition string.empty : string := list.nil -definition string.str : char → string → string := list.cons +namespace string +definition empty : string := list.nil +definition str : char → string → string := list.cons +end string diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f3cefc8bc5..af40bd651d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1611,21 +1611,14 @@ expr parser::parse_numeral_expr(bool user_notation) { auto p = pos(); mpz n = get_num_val().get_numerator(); next(); - if (!m_has_num) - m_has_num = has_num_decls(m_env); list vals; if (user_notation) vals = get_mpz_notation(m_env, n); - if (!*m_has_num && !vals) { - throw parser_error("numeral cannot be encoded as expression, environment does not contain " - "the auxiliary declarations zero, one, bit0 and bit1", p); - } if (!vals) { return save_pos(mk_prenum(n), p); } else { buffer cs; - if (*m_has_num) - cs.push_back(save_pos(mk_prenum(n), p)); + cs.push_back(save_pos(mk_prenum(n), p)); for (expr const & c : vals) cs.push_back(copy_with_new_pos(c, p)); if (cs.size() == 1) @@ -1650,18 +1643,11 @@ expr parser::parse_decimal_expr() { } expr parser::parse_string_expr() { - auto p = pos(); std::string v = get_str_val(); next(); - if (!m_has_string) - m_has_string = has_string_decls(m_env); - if (!*m_has_string) - throw parser_error("string cannot be encoded as expression, environment does not contain the type 'string' " - "(solution: use 'import string')", p); return from_string(v); } - expr parser::parse_backtick_expr_core() { next(); flet set(m_in_backtick, true); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index cab006739b..011036f011 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -118,8 +118,6 @@ class parser { // When the following flag is true, it creates a constant. // This flag is when we are trying to parse mutually recursive declarations. undef_id_behavior m_undef_id_behavior; - optional m_has_num; - optional m_has_string; optional m_has_tactic_decls; // We process theorems in parallel theorem_queue m_theorem_queue; diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 0c859f7032..3b86d2599b 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/constants.h" #include "library/replace_visitor.h" +#include "library/string.h" #include "library/definitional/equations.h" #include "library/compiler/comp_irrelevant.h" #include "library/compiler/erase_irrelevant.h" @@ -274,6 +275,7 @@ void pretty_fn::set_options_core(options const & _o) { o = o.update_if_undef(get_pp_full_names_name(), true); o = o.update_if_undef(get_pp_beta_name(), false); o = o.update_if_undef(get_pp_numerals_name(), false); + o = o.update_if_undef(get_pp_strings_name(), false); o = o.update_if_undef(get_pp_abbreviations_name(), false); } m_options = o; @@ -292,6 +294,7 @@ void pretty_fn::set_options_core(options const & _o) { m_purify_locals = get_pp_purify_locals(o); m_beta = get_pp_beta(o); m_numerals = get_pp_numerals(o); + m_strings = get_pp_strings(o); m_abbreviations = get_pp_abbreviations(o); m_preterm = get_pp_preterm(o); m_hide_binder_types = get_pp_hide_binder_types(o); @@ -506,6 +509,9 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul if (auto n = to_num(e)) return pp_num(*n); 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); + } expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { return pp_abbreviation(e, *it, true, bp, ignore_hide); @@ -840,6 +846,9 @@ auto pretty_fn::pp_macro(expr const & e) -> result { return m_unicode ? format("◾") : format("irrel"); else return pp(get_annotation_arg(e)); + } else if (!m_strings && to_string(e)) { + expr n = *macro_def(e).expand(e, m_ctx); + return pp(n); } else if (is_annotation(e)) { return pp(get_annotation_arg(e)); } else if (is_rec_fn_macro(e)) { @@ -1030,6 +1039,9 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> if (auto n = to_num(e)) return pp_num(*n); 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); + } expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { return pp_abbreviation(e, *it, true, rbp); @@ -1284,6 +1296,9 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { if (auto n = to_num(e)) return pp_num(*n); 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 n = is_abbreviated(e)) return pp_abbreviation(e, *n, false); if (auto r = pp_notation(e)) diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 16c19163b6..0034356078 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -68,6 +68,7 @@ private: bool m_hide_binder_types; bool m_beta; bool m_numerals; + bool m_strings; bool m_abbreviations; bool m_hide_full_terms; bool m_hide_comp_irrel; diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 03558f648e..495051d9f2 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -90,7 +90,7 @@ static char const * g_decreasing_unicode = "↓"; void init_token_table(token_table & t) { pair builtin[] = {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0}, - {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0}, + {"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0}, diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d5ed66b07d..ba67964903 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -23,7 +23,7 @@ name const * g_cast = nullptr; name const * g_cast_eq = nullptr; name const * g_cast_heq = nullptr; name const * g_char = nullptr; -name const * g_char_mk = nullptr; +name const * g_char_of_nat = nullptr; name const * g_classical = nullptr; name const * g_congr = nullptr; name const * g_congr_arg = nullptr; @@ -55,6 +55,8 @@ name const * g_false = nullptr; name const * g_false_of_true_iff_false = nullptr; name const * g_false_rec = nullptr; name const * g_field = nullptr; +name const * g_fin = nullptr; +name const * g_fin_mk = nullptr; name const * g_funext = nullptr; name const * g_has_add = nullptr; name const * g_has_div = nullptr; @@ -96,6 +98,7 @@ name const * g_lift_down = nullptr; name const * g_lift_up = nullptr; name const * g_linear_ordered_ring = nullptr; name const * g_linear_ordered_semiring = nullptr; +name const * g_list = nullptr; name const * g_list_nil = nullptr; name const * g_list_cons = nullptr; name const * g_monoid = nullptr; @@ -120,6 +123,9 @@ name const * g_nat_cases_on = nullptr; name const * g_nat_rec_on = nullptr; name const * g_nat_no_confusion = nullptr; name const * g_nat_no_confusion_type = nullptr; +name const * g_nat_has_zero = nullptr; +name const * g_nat_has_one = nullptr; +name const * g_nat_has_add = nullptr; name const * g_ne = nullptr; name const * g_neg = nullptr; name const * g_norm_num_add1 = nullptr; @@ -315,7 +321,7 @@ void initialize_constants() { g_cast_eq = new name{"cast_eq"}; g_cast_heq = new name{"cast_heq"}; g_char = new name{"char"}; - g_char_mk = new name{"char", "mk"}; + g_char_of_nat = new name{"char", "of_nat"}; g_classical = new name{"classical"}; g_congr = new name{"congr"}; g_congr_arg = new name{"congr_arg"}; @@ -347,6 +353,8 @@ void initialize_constants() { g_false_of_true_iff_false = new name{"false_of_true_iff_false"}; g_false_rec = new name{"false", "rec"}; g_field = new name{"field"}; + g_fin = new name{"fin"}; + g_fin_mk = new name{"fin", "mk"}; g_funext = new name{"funext"}; g_has_add = new name{"has_add"}; g_has_div = new name{"has_div"}; @@ -388,6 +396,7 @@ void initialize_constants() { g_lift_up = new name{"lift", "up"}; g_linear_ordered_ring = new name{"linear_ordered_ring"}; g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; + g_list = new name{"list"}; g_list_nil = new name{"list", "nil"}; g_list_cons = new name{"list", "cons"}; g_monoid = new name{"monoid"}; @@ -412,6 +421,9 @@ void initialize_constants() { g_nat_rec_on = new name{"nat", "rec_on"}; g_nat_no_confusion = new name{"nat", "no_confusion"}; g_nat_no_confusion_type = new name{"nat", "no_confusion_type"}; + g_nat_has_zero = new name{"nat_has_zero"}; + g_nat_has_one = new name{"nat_has_one"}; + g_nat_has_add = new name{"nat_has_add"}; g_ne = new name{"ne"}; g_neg = new name{"neg"}; g_norm_num_add1 = new name{"norm_num", "add1"}; @@ -608,7 +620,7 @@ void finalize_constants() { delete g_cast_eq; delete g_cast_heq; delete g_char; - delete g_char_mk; + delete g_char_of_nat; delete g_classical; delete g_congr; delete g_congr_arg; @@ -640,6 +652,8 @@ void finalize_constants() { delete g_false_of_true_iff_false; delete g_false_rec; delete g_field; + delete g_fin; + delete g_fin_mk; delete g_funext; delete g_has_add; delete g_has_div; @@ -681,6 +695,7 @@ void finalize_constants() { delete g_lift_up; delete g_linear_ordered_ring; delete g_linear_ordered_semiring; + delete g_list; delete g_list_nil; delete g_list_cons; delete g_monoid; @@ -705,6 +720,9 @@ void finalize_constants() { delete g_nat_rec_on; delete g_nat_no_confusion; delete g_nat_no_confusion_type; + delete g_nat_has_zero; + delete g_nat_has_one; + delete g_nat_has_add; delete g_ne; delete g_neg; delete g_norm_num_add1; @@ -900,7 +918,7 @@ name const & get_cast_name() { return *g_cast; } name const & get_cast_eq_name() { return *g_cast_eq; } name const & get_cast_heq_name() { return *g_cast_heq; } name const & get_char_name() { return *g_char; } -name const & get_char_mk_name() { return *g_char_mk; } +name const & get_char_of_nat_name() { return *g_char_of_nat; } name const & get_classical_name() { return *g_classical; } name const & get_congr_name() { return *g_congr; } name const & get_congr_arg_name() { return *g_congr_arg; } @@ -932,6 +950,8 @@ name const & get_false_name() { return *g_false; } name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; } name const & get_false_rec_name() { return *g_false_rec; } name const & get_field_name() { return *g_field; } +name const & get_fin_name() { return *g_fin; } +name const & get_fin_mk_name() { return *g_fin_mk; } name const & get_funext_name() { return *g_funext; } name const & get_has_add_name() { return *g_has_add; } name const & get_has_div_name() { return *g_has_div; } @@ -973,6 +993,7 @@ name const & get_lift_down_name() { return *g_lift_down; } name const & get_lift_up_name() { return *g_lift_up; } name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; } name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; } +name const & get_list_name() { return *g_list; } name const & get_list_nil_name() { return *g_list_nil; } name const & get_list_cons_name() { return *g_list_cons; } name const & get_monoid_name() { return *g_monoid; } @@ -997,6 +1018,9 @@ name const & get_nat_cases_on_name() { return *g_nat_cases_on; } name const & get_nat_rec_on_name() { return *g_nat_rec_on; } name const & get_nat_no_confusion_name() { return *g_nat_no_confusion; } name const & get_nat_no_confusion_type_name() { return *g_nat_no_confusion_type; } +name const & get_nat_has_zero_name() { return *g_nat_has_zero; } +name const & get_nat_has_one_name() { return *g_nat_has_one; } +name const & get_nat_has_add_name() { return *g_nat_has_add; } name const & get_ne_name() { return *g_ne; } name const & get_neg_name() { return *g_neg; } name const & get_norm_num_add1_name() { return *g_norm_num_add1; } diff --git a/src/library/constants.h b/src/library/constants.h index 85f052a342..ce6fc92c67 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -25,7 +25,7 @@ name const & get_cast_name(); name const & get_cast_eq_name(); name const & get_cast_heq_name(); name const & get_char_name(); -name const & get_char_mk_name(); +name const & get_char_of_nat_name(); name const & get_classical_name(); name const & get_congr_name(); name const & get_congr_arg_name(); @@ -57,6 +57,8 @@ name const & get_false_name(); name const & get_false_of_true_iff_false_name(); name const & get_false_rec_name(); name const & get_field_name(); +name const & get_fin_name(); +name const & get_fin_mk_name(); name const & get_funext_name(); name const & get_has_add_name(); name const & get_has_div_name(); @@ -98,6 +100,7 @@ name const & get_lift_down_name(); name const & get_lift_up_name(); name const & get_linear_ordered_ring_name(); name const & get_linear_ordered_semiring_name(); +name const & get_list_name(); name const & get_list_nil_name(); name const & get_list_cons_name(); name const & get_monoid_name(); @@ -122,6 +125,9 @@ name const & get_nat_cases_on_name(); name const & get_nat_rec_on_name(); name const & get_nat_no_confusion_name(); name const & get_nat_no_confusion_type_name(); +name const & get_nat_has_zero_name(); +name const & get_nat_has_one_name(); +name const & get_nat_has_add_name(); name const & get_ne_name(); name const & get_neg_name(); name const & get_norm_num_add1_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index c085aaa32b..41449f7717 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -18,7 +18,7 @@ cast cast_eq cast_heq char -char.mk +char.of_nat classical congr congr_arg @@ -50,6 +50,8 @@ false false_of_true_iff_false false.rec field +fin +fin.mk funext has_add has_div @@ -91,6 +93,7 @@ lift.down lift.up linear_ordered_ring linear_ordered_semiring +list list.nil list.cons monoid @@ -115,6 +118,9 @@ nat.cases_on nat.rec_on nat.no_confusion nat.no_confusion_type +nat_has_zero +nat_has_one +nat_has_add ne neg norm_num.add1 diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 7899eca090..8d5b2fc72d 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/typed_expr.h" #include "library/choice.h" #include "library/class.h" +#include "library/num.h" #include "library/string.h" #include "library/annotation.h" #include "library/explicit.h" @@ -90,6 +91,7 @@ void initialize_library_module() { initialize_typed_expr(); initialize_choice(); initialize_string(); + initialize_num(); initialize_annotation(); initialize_explicit(); initialize_module(); @@ -157,6 +159,7 @@ void finalize_library_module() { finalize_module(); finalize_explicit(); finalize_annotation(); + finalize_num(); finalize_string(); finalize_choice(); finalize_typed_expr(); diff --git a/src/library/num.cpp b/src/library/num.cpp index 2ce89cdf7f..1b05f130fb 100644 --- a/src/library/num.cpp +++ b/src/library/num.cpp @@ -9,14 +9,6 @@ Author: Leonardo de Moura #include "library/constants.h" namespace lean { -bool has_num_decls(environment const & env) { - return - env.find(get_zero_name()) && - env.find(get_one_name()) && - env.find(get_bit0_name()) && - env.find(get_bit1_name()); -} - bool is_const_app(expr const & e, name const & n, unsigned nargs) { expr const & f = get_app_fn(e); return is_constant(f) && const_name(f) == n && get_app_num_args(e) == nargs; @@ -128,4 +120,45 @@ bool is_num_leaf_constant(name const & n) { n == get_has_zero_zero_name() || n == get_has_one_one_name(); } + +static expr * g_bit0_nat = nullptr; +static expr * g_bit1_nat = nullptr; +static expr * g_zero_nat = nullptr; +static expr * g_one_nat = nullptr; + +expr to_nat_expr_core(mpz const & n) { + lean_assert(n >= 0); + if (n == 1) + return *g_one_nat; + else if (n % mpz(2) == 0) + return mk_app(*g_bit0_nat, to_nat_expr(n / 2)); + else + return mk_app(*g_bit1_nat, to_nat_expr(n / 2)); +} + +expr to_nat_expr(mpz const & n) { + if (n == 0) + return *g_zero_nat; + else + return to_nat_expr_core(n); +} + +void initialize_num() { + expr nat = Const(get_nat_name()); + expr nat_has_add = Const(get_nat_has_add_name()); + expr nat_has_one = Const(get_nat_has_one_name()); + expr nat_has_zero = Const(get_nat_has_zero_name()); + + g_bit0_nat = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_one()}), nat, nat_has_add)); + g_bit1_nat = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_one()}), nat, nat_has_one, nat_has_add)); + g_one_nat = new expr(mk_app(mk_constant(get_one_name(), {mk_level_one()}), nat, nat_has_one)); + g_zero_nat = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_one()}), nat, nat_has_zero)); +} + +void finalize_num() { + delete g_bit0_nat; + delete g_bit1_nat; + delete g_zero_nat; + delete g_one_nat; +} } diff --git a/src/library/num.h b/src/library/num.h index 4b347297e6..918ace2947 100644 --- a/src/library/num.h +++ b/src/library/num.h @@ -8,10 +8,6 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { -/** \brief Return true iff the given environment contains the declarations needed to encode numerals: - zero, one, bit0, bit1 */ -bool has_num_decls(environment const & env); - bool is_const_app(expr const &, name const &, unsigned); /** \brief Return true iff the given expression encodes a numeral. */ @@ -42,6 +38,9 @@ optional to_num_core(expr const & e); annotation to let user mark constants that should be treated in a different way by some tactics. */ bool is_num_leaf_constant(name const & n); +/** \brief Encode \c n as an expression using bit0/bit1/one/zero constants */ +expr to_nat_expr(mpz const & n); + void initialize_num(); void finalize_num(); } diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index ab3e3e00cf..be99e80caa 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -59,6 +59,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_NUMERALS true #endif +#ifndef LEAN_DEFAULT_PP_STRINGSS +#define LEAN_DEFAULT_PP_STRINGS true +#endif + #ifndef LEAN_DEFAULT_PP_ABBREVIATIONS #define LEAN_DEFAULT_PP_ABBREVIATIONS true #endif @@ -102,6 +106,7 @@ static name * g_pp_purify_metavars = nullptr; static name * g_pp_purify_locals = nullptr; static name * g_pp_beta = nullptr; static name * g_pp_numerals = nullptr; +static name * g_pp_strings = nullptr; static name * g_pp_abbreviations = nullptr; static name * g_pp_preterm = nullptr; static name * g_pp_goal_compact = nullptr; @@ -125,6 +130,7 @@ void initialize_pp_options() { g_pp_purify_locals = new name{"pp", "purify_locals"}; g_pp_beta = new name{"pp", "beta"}; g_pp_numerals = new name{"pp", "numerals"}; + g_pp_strings = new name{"pp", "strings"}; g_pp_abbreviations = new name{"pp", "abbreviations"}; g_pp_preterm = new name{"pp", "preterm"}; g_pp_hide_binder_types = new name{"pp", "hide_binder_types"}; @@ -161,6 +167,8 @@ void initialize_pp_options() { "(pretty printer) apply beta-reduction when pretty printing"); register_bool_option(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS, "(pretty printer) display nat/num numerals in decimal notation"); + register_bool_option(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS, + "(pretty printer) pretty print string literals"); register_bool_option(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS, "(pretty printer) display abbreviations (i.e., revert abbreviation expansion when pretty printing)"); register_bool_option(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM, @@ -192,6 +200,7 @@ void finalize_pp_options() { delete g_pp_preterm; delete g_pp_abbreviations; delete g_pp_numerals; + delete g_pp_strings; delete g_pp_max_depth; delete g_pp_max_steps; delete g_pp_notation; @@ -223,6 +232,7 @@ name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; } name const & get_pp_beta_name() { return *g_pp_beta; } name const & get_pp_preterm_name() { return *g_pp_preterm; } name const & get_pp_numerals_name() { return *g_pp_numerals; } +name const & get_pp_strings_name() { return *g_pp_strings; } name const & get_pp_abbreviations_name() { return *g_pp_abbreviations; } unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } @@ -238,6 +248,7 @@ bool get_pp_purify_metavars(options const & opts) { return opts.get_bool(* bool get_pp_purify_locals(options const & opts) { return opts.get_bool(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS); } bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); } +bool get_pp_strings(options const & opts) { return opts.get_bool(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS); } bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*g_pp_abbreviations, LEAN_DEFAULT_PP_ABBREVIATIONS); } bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } bool get_pp_goal_compact(options const & opts) { return opts.get_bool(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index f7acae5452..0999ff24ef 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -18,6 +18,7 @@ name const & get_pp_purify_locals_name(); name const & get_pp_beta_name(); name const & get_pp_preterm_name(); name const & get_pp_numerals_name(); +name const & get_pp_strings_name(); name const & get_pp_abbreviations_name(); unsigned get_pp_max_depth(options const & opts); @@ -33,6 +34,7 @@ bool get_pp_beta(options const & opts); bool get_pp_purify_metavars(options const & opts); bool get_pp_purify_locals(options const & opts); bool get_pp_numerals(options const & opts); +bool get_pp_strings(options const & opts); bool get_pp_abbreviations(options const & opts); bool get_pp_preterm(options const & opts); bool get_pp_goal_compact(options const & opts); diff --git a/src/library/string.cpp b/src/library/string.cpp index 8ec2276579..63ffa5a7e8 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -10,20 +10,50 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/string.h" #include "library/constants.h" +#include "library/num.h" +#include "library/trace.h" namespace lean { static name * g_string_macro = nullptr; static std::string * g_string_opcode = nullptr; -static expr * g_bool = nullptr; -static expr * g_ff = nullptr; -static expr * g_tt = nullptr; +static expr * g_nat = nullptr; static expr * g_char = nullptr; -static expr * g_ascii = nullptr; +static expr * g_char_of_nat = nullptr; static expr * g_string = nullptr; static expr * g_empty = nullptr; static expr * g_str = nullptr; +static expr * g_fin_mk = nullptr; +static expr * g_list_char = nullptr; +static expr * g_list_cons = nullptr; +static expr * g_list_nil_char = nullptr; -expr from_string_core(unsigned i, std::string const & s); +expr from_string_core(std::string const & s); + +static void display_string_literal(std::ostream & out, std::string const & s) { + out << "\""; + for (unsigned i = 0; i < s.size(); i++) { + char c = s[i]; + if (c == '\n') + out << "\\n"; + else if (c == '\t') + out << "\\t"; + else if (c == '\r') + out << "\\r"; + else if (c == 0) + out << "\\0"; + else if (c == '\"') + out << "\\\""; + else + out << c; + } + out << "\""; +} + +format pp_string_literal(std::string const & s) { + std::ostringstream out; + display_string_literal(out, s); + return format(out.str()); +} /** \brief The string macro is a compact way of encoding strings inside Lean expressions. */ class string_macro : public macro_definition_cell { @@ -38,7 +68,7 @@ public: return *g_string; } virtual optional expand(expr const &, abstract_type_context &) const { - return some_expr(from_string_core(0, m_value)); + return some_expr(from_string_core(m_value)); } virtual unsigned trust_level() const { return 0; } virtual bool operator==(macro_definition_cell const & other) const { @@ -46,28 +76,10 @@ public: return other_ptr && m_value == other_ptr->m_value; } virtual void display(std::ostream & out) const { - out << "\""; - for (unsigned i = 0; i < m_value.size(); i++) { - char c = m_value[i]; - if (c == '\n') - out << "\\n"; - else if (c == '\t') - out << "\\t"; - else if (c == '\r') - out << "\\r"; - else if (c == 0) - out << "\\0"; - else if (c == '\"') - out << "\\\""; - else - out << c; - } - out << "\""; + display_string_literal(out, m_value); } virtual format pp(formatter const &) const { - std::ostringstream out; - display(out); - return format(out.str()); + return pp_string_literal(m_value); } virtual bool is_atomic_pp(bool, bool) const { return true; } virtual unsigned hash() const { return std::hash()(m_value); } @@ -89,16 +101,18 @@ string_macro const & to_string_macro(expr const & e) { } void initialize_string() { - g_string_macro = new name("string_macro"); - g_string_opcode = new std::string("Str"); - g_bool = new expr(Const(get_bool_name())); - g_ff = new expr(Const(get_bool_ff_name())); - g_tt = new expr(Const(get_bool_tt_name())); - g_char = new expr(Const(get_char_name())); - g_ascii = new expr(Const(get_char_mk_name())); - g_string = new expr(Const(get_string_name())); - g_empty = new expr(Const(get_string_empty_name())); - g_str = new expr(Const(get_string_str_name())); + g_string_macro = new name("string_macro"); + g_string_opcode = new std::string("Str"); + g_nat = new expr(Const(get_nat_name())); + g_char = new expr(Const(get_char_name())); + g_char_of_nat = new expr(Const(get_char_of_nat_name())); + g_string = new expr(Const(get_string_name())); + g_empty = new expr(Const(get_string_empty_name())); + g_str = new expr(Const(get_string_str_name())); + g_fin_mk = new expr(Const(get_fin_mk_name())); + g_list_char = new expr(mk_app(mk_constant(get_list_name(), {mk_level_one()}), *g_char)); + g_list_cons = new expr(mk_constant(get_list_cons_name(), {mk_level_one()})); + g_list_nil_char = new expr(mk_app(mk_constant(get_list_nil_name(), {mk_level_one()}), *g_char)); register_macro_deserializer(*g_string_opcode, [](deserializer & d, unsigned num, expr const *) { if (num != 0) @@ -109,85 +123,72 @@ void initialize_string() { } void finalize_string() { + delete g_nat; delete g_str; delete g_empty; delete g_string; - delete g_ascii; + delete g_char_of_nat; delete g_char; - delete g_tt; - delete g_ff; - delete g_bool; delete g_string_opcode; delete g_string_macro; + delete g_list_char; + delete g_list_cons; + delete g_list_nil_char; + delete g_fin_mk; } -bool has_string_decls(environment const & env) { - try { - type_checker tc(env); - return - tc.infer(*g_ff) == *g_bool && - tc.infer(*g_tt) == *g_bool && - tc.infer(*g_ascii) == *g_bool >> (*g_bool >> (*g_bool >> (*g_bool >> (*g_bool >> (*g_bool >> (*g_bool >> (*g_bool >> *g_char))))))) && - tc.infer(*g_empty) == *g_string && - tc.infer(*g_str) == *g_char >> (*g_string >> *g_string); - } catch (exception &) { - return false; +expr from_string_core(std::string const & s) { + expr r = *g_empty; + for (unsigned i = 0; i < s.size(); i++) { + expr n = to_nat_expr(mpz(s[i])); + expr c = mk_app(*g_char_of_nat, n); + r = mk_app(*g_str, c, r); } -} - -expr from_char(unsigned char c) { - buffer bits; - while (c != 0) { - if (c % 2 == 1) - bits.push_back(*g_tt); - else - bits.push_back(*g_ff); - c /= 2; - } - while (bits.size() < 8) - bits.push_back(*g_ff); - return mk_rev_app(*g_ascii, bits.size(), bits.data()); -} - -expr from_string_core(unsigned i, std::string const & s) { - if (i == s.size()) - return *g_empty; - else - return mk_app(*g_str, from_char(s[i]), from_string_core(i+1, s)); + return r; } expr from_string(std::string const & s) { return mk_string_macro(s); } -bool to_char_core(expr const & e, buffer & tmp) { +bool to_char_core(expr const & e, std::string & r) { buffer args; - if (get_app_rev_args(e, args) == *g_ascii && args.size() == 8) { - unsigned v = 0; - for (unsigned i = 0; i < args.size(); i++) { - v *= 2; - if (args[i] == *g_tt) - v++; - else if (args[i] != *g_ff) - return false; + expr const & fn = get_app_args(e, args); + if (fn == *g_fin_mk && args.size() == 3) { + if (auto n = to_num(args[1])) { + r.push_back(n->get_unsigned_int()); + return true; + } else { + return false; + } + } else if (fn == *g_char_of_nat && args.size() == 1) { + if (auto n = to_num(args[0])) { + r.push_back(n->get_unsigned_int()); + return true; + } else { + return false; } - tmp.push_back(v); - return true; } else { return false; } } -bool to_string_core(expr const & e, buffer & tmp) { - if (e == *g_empty) { +bool to_string_core(expr const & e, std::string & r) { + if (e == *g_empty || e == *g_list_nil_char) { + return true; + } else if (is_string_macro(e)) { + r = to_string_macro(e).get_value(); return true; } else { buffer args; - return - get_app_args(e, args) == *g_str && - args.size() == 2 && - to_char_core(args[0], tmp) && - to_string_core(args[1], tmp); + expr const & fn = get_app_args(e, args); + if (fn == *g_str && args.size() == 2) { + return to_string_core(args[1], r) && to_char_core(args[0], r); + } else if (fn == *g_list_cons && args.size() == 3 && args[0] == *g_char) { + return to_string_core(args[2], r) && to_char_core(args[1], r); + } else { + return false; + } } } @@ -195,15 +196,9 @@ optional to_string(expr const & e) { if (is_string_macro(e)) { return optional(to_string_macro(e).get_value()); } else { - buffer tmp; + std::string tmp; if (to_string_core(e, tmp)) { - std::string r; - unsigned i = tmp.size(); - while (i > 0) { - --i; - r += tmp[i]; - } - return optional(r); + return optional(tmp); } else { return optional(); } diff --git a/src/library/string.h b/src/library/string.h index 251843594e..6da63dfa5a 100644 --- a/src/library/string.h +++ b/src/library/string.h @@ -8,18 +8,6 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { -/** - \brief Return true iff the environment \c env contains the following declarations - in the namespace 'bit' - b0 : bit - b1 : bit - and the following ones in the namespace 'string' - ascii : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> char - empty : string - str : char -> string -> string -*/ -bool has_string_decls(environment const & env); - /** \brief Return an expression that encodes the given string using the declarations ascii, empty and str. @@ -37,6 +25,8 @@ expr from_string(std::string const & s); */ optional to_string(expr const & e); +format pp_string_literal(std::string const & s); + void initialize_string(); void finalize_string(); }