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

feat(frontends/lean/pp): add option to hide binder types

Browse source 
Replace old pp.hide_binder_types option

Conflicts:
        src/frontends/lean/pp.cpp
        src/library/pp_options.cpp
        src/library/pp_options.h
This commit is contained in:
Sebastian Ullrich 2016-05-24 11:42:06 -04:00 • committed by Leonardo de Moura
parent b95bc8ff5b
commit 647078bd40
7 changed files with 61 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -297,7 +297,7 @@ void pretty_fn::set_options_core(options const & _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);
m_binder_types = get_pp_binder_types(o);
m_hide_comp_irrel = get_pp_hide_comp_irrel(o);
m_hide_full_terms = get_formatter_hide_full_terms(o);
m_num_nat_coe = m_numerals && !m_coercion;
@ -679,65 +679,58 @@ auto pretty_fn::pp_app(expr const & e) -> result {
}
format pretty_fn::pp_binder(expr const & local) {
if (m_hide_binder_types) {
return format(local_pp_name(local));
} else {
format r;
auto bi = local_info(local);
if (bi != binder_info())
r += format(open_binder_string(bi, m_unicode));
r += format(local_pp_name(local));
format r;
auto bi = local_info(local);
if (bi != binder_info())
r += format(open_binder_string(bi, m_unicode));
r += format(local_pp_name(local));
if (m_binder_types) {
r += space();
r += compose(colon(), nest(m_indent, compose(line(), pp_child(mlocal_type(local), 0).fmt())));
if (bi != binder_info())
r += format(close_binder_string(bi, m_unicode));
return r;
}
if (bi != binder_info())
r += format(close_binder_string(bi, m_unicode));
return r;
}
format pretty_fn::pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi) {
format r;
r += format(open_binder_string(bi, m_unicode));
if (m_binder_types || bi != binder_info())
r += format(open_binder_string(bi, m_unicode));
for (name const & n : names) {
r += format(n);
r += space();
}
r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt())));
r += format(close_binder_string(bi, m_unicode));
if (m_binder_types) {
r += space();
r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt())));
}
if (m_binder_types || bi != binder_info())
r += format(close_binder_string(bi, m_unicode));
return group(r);
}
format pretty_fn::pp_binders(buffer<expr> const & locals) {
if (m_hide_binder_types) {
format r;
for (auto l : locals) {
r += space();
r += format(local_pp_name(l));
unsigned num = locals.size();
buffer<name> names;
expr local = locals[0];
expr type = mlocal_type(local);
binder_info bi = local_info(local);
names.push_back(local_pp_name(local));
format r;
for (unsigned i = 1; i < num; i++) {
expr local = locals[i];
if (!bi.is_inst_implicit() && mlocal_type(local) == type && local_info(local) == bi) {
names.push_back(local_pp_name(local));
} else {
r += group(compose(line(), pp_binder_block(names, type, bi)));
names.clear();
type = mlocal_type(local);
bi = local_info(local);
names.push_back(local_pp_name(local));
}
return r;
} else {
unsigned num = locals.size();
buffer<name> names;
expr local = locals[0];
expr type = mlocal_type(local);
binder_info bi = local_info(local);
names.push_back(local_pp_name(local));
format r;
for (unsigned i = 1; i < num; i++) {
expr local = locals[i];
if (!bi.is_inst_implicit() && mlocal_type(local) == type && local_info(local) == bi) {
names.push_back(local_pp_name(local));
} else {
r += group(compose(line(), pp_binder_block(names, type, bi)));
names.clear();
type = mlocal_type(local);
bi = local_info(local);
names.push_back(local_pp_name(local));
}
}
r += group(compose(line(), pp_binder_block(names, type, bi)));
return r;
}
r += group(compose(line(), pp_binder_block(names, type, bi)));
return r;
}
auto pretty_fn::pp_lambda(expr const & e) -> result {

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

@ -65,7 +65,6 @@ private:
bool m_metavar_args;
bool m_purify_metavars;
bool m_purify_locals;
bool m_hide_binder_types;
bool m_beta;
bool m_numerals;
bool m_strings;
@ -73,6 +72,7 @@ private:
bool m_hide_full_terms;
bool m_hide_comp_irrel;
bool m_preterm;
bool m_binder_types;
name mk_metavar_name(name const & m);
name mk_local_name(name const & n, name const & suggested);

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

@ -385,7 +385,7 @@ static bool print_constant(parser const & p, char const * kind, declaration cons
out << "protected ";
out << kind << " " << to_user_name(p.env(), d.get_name());
print_attributes(p, d.get_name());
out << " : " << d.get_type();
out.update_options(out.get_options().update((name {"pp", "binder_types"}), true)) << " : " << d.get_type();
if (is_def)
out << " :=";
out << "\n";

20
src/library/pp_options.cpp
View file

@ -83,12 +83,12 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT true
#endif
#ifndef LEAN_DEFAULT_PP_ALL
#define LEAN_DEFAULT_PP_ALL false
#ifndef LEAN_DEFAULT_PP_BINDER_TYPES
#define LEAN_DEFAULT_PP_BINDER_TYPES false
#endif
#ifndef LEAN_DEFAULT_PP_HIDE_BINDER_TYPES
#define LEAN_DEFAULT_PP_HIDE_BINDER_TYPES false
#ifndef LEAN_DEFAULT_PP_ALL
#define LEAN_DEFAULT_PP_ALL false
#endif
@ -111,7 +111,7 @@ static name * g_pp_abbreviations = nullptr;
static name * g_pp_preterm = nullptr;
static name * g_pp_goal_compact = nullptr;
static name * g_pp_goal_max_hyps = nullptr;
static name * g_pp_hide_binder_types = nullptr;
static name * g_pp_binder_types = nullptr;
static name * g_pp_hide_comp_irrel = nullptr;
static name * g_pp_all = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;
@ -133,7 +133,7 @@ void initialize_pp_options() {
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"};
g_pp_binder_types = new name{"pp", "binder_types"};
g_pp_hide_comp_irrel = new name{"pp", "hide_comp_irrelevant"};
g_pp_all = new name{"pp", "all"};
g_pp_goal_compact = new name{"pp", "goal", "compact"};
@ -177,10 +177,10 @@ void initialize_pp_options() {
"(pretty printer) try to display goal in a single line when possible");
register_unsigned_option(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS,
"(pretty printer) maximum number of hypotheses to be displayed");
register_bool_option(*g_pp_hide_binder_types, LEAN_DEFAULT_PP_HIDE_BINDER_TYPES,
"(pretty printer) hide types in binders");
register_bool_option(*g_pp_hide_comp_irrel, LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT,
"(pretty printer) hide terms marked as computationally irrelevant, these marks are introduced by the code generator");
register_bool_option(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES,
"(pretty printer) display types of lambda and Pi parameters");
register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL,
"(pretty printer) display coercions, implicit parameters, fully qualified names, universes, "
"and disable abbreviations, beta reduction and notation during pretty printing");
@ -215,7 +215,7 @@ void finalize_pp_options() {
delete g_pp_beta;
delete g_pp_goal_compact;
delete g_pp_goal_max_hyps;
delete g_pp_hide_binder_types;
delete g_pp_binder_types;
delete g_pp_hide_comp_irrel;
delete g_pp_all;
delete g_distinguishing_pp_options;
@ -253,7 +253,7 @@ bool get_pp_abbreviations(options const & opts) { return opts.get_bool(*
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); }
unsigned get_pp_goal_max_hyps(options const & opts) { return opts.get_unsigned(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS); }
bool get_pp_hide_binder_types(options const & opts) { return opts.get_bool(*g_pp_hide_binder_types, LEAN_DEFAULT_PP_HIDE_BINDER_TYPES); }
bool get_pp_binder_types(options const & opts) { return opts.get_bool(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES); }
bool get_pp_hide_comp_irrel(options const & opts) { return opts.get_bool(*g_pp_hide_comp_irrel, LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT); }
bool get_pp_all(options const & opts) { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); }

2
src/library/pp_options.h
View file

@ -39,7 +39,7 @@ bool get_pp_abbreviations(options const & opts);
bool get_pp_preterm(options const & opts);
bool get_pp_goal_compact(options const & opts);
unsigned get_pp_goal_max_hyps(options const & opts);
bool get_pp_hide_binder_types(options const & opts);
bool get_pp_binder_types(options const & opts);
bool get_pp_hide_comp_irrel(options const & opts);
bool get_pp_all(options const & opts);
list<options> const & get_distinguishing_pp_options();

7
tests/lean/pp_binder_types.lean Normal file
View file

@ -0,0 +1,7 @@
open nat
definition f (n : nat) (H : n = n) := λm, id (n + m)
print f
set_option pp.binder_types true
print f

4
tests/lean/pp_binder_types.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
definition f : Π (n : ℕ), n = n → ℕ → ℕ :=
λ n H m, id (n + m)
definition f : Π (n : ℕ), n = n → ℕ → ℕ :=
λ (n : ℕ) (H : n = n) (m : ℕ), id (n + m)