max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library,frontends/lean/pp): add support for new string encoding

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-24 16:20:43 -07:00
parent cf5e7e4185
commit 6a9e5079c9
18 changed files with 226 additions and 151 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/.project
View file

@ -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/

6
library/init/char.lean
View file

@ -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

6
library/init/string.lean
View file

@ -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

16
src/frontends/lean/parser.cpp
View file

@ -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<expr> 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<expr> 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<bool> set(m_in_backtick, true);

2
src/frontends/lean/parser.h
View file

@ -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<bool> m_has_num;
optional<bool> m_has_string;
optional<bool> m_has_tactic_decls;
// We process theorems in parallel
theorem_queue m_theorem_queue;

15
src/frontends/lean/pp.cpp
View file

@ -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))

1
src/frontends/lean/pp.h
View file

@ -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;

2
src/frontends/lean/token_table.cpp
View file

@ -90,7 +90,7 @@ static char const * g_decreasing_unicode = "↓";
void init_token_table(token_table & t) {
pair<char const *, unsigned> 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},

32
src/library/constants.cpp
View file

@ -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; }

8
src/library/constants.h
View file

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

8
src/library/constants.txt
View file

@ -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

3
src/library/init_module.cpp
View file

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

49
src/library/num.cpp
View file

@ -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;
}
}

7
src/library/num.h
View file

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

11
src/library/pp_options.cpp
View file

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

2
src/library/pp_options.h
View file

@ -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);

191
src/library/string.cpp
View file

@ -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<expr> 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<std::string>()(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<expr> 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<char> & tmp) {
bool to_char_core(expr const & e, std::string & r) {
buffer<expr> 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<char> & 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<expr> 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<std::string> to_string(expr const & e) {
if (is_string_macro(e)) {
return optional<std::string>(to_string_macro(e).get_value());
} else {
buffer<char> 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<std::string>(r);
return optional<std::string>(tmp);
} else {
return optional<std::string>();
}

14
src/library/string.h
View file

@ -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<std::string> to_string(expr const & e);
format pp_string_literal(std::string const & s);
void initialize_string();
void finalize_string();
}