From 4364b7f92609c02045e1ad81eee2f311ae2b4015 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Feb 2015 12:27:53 -0800 Subject: [PATCH] feat(frontends/lean): pp.beta is true by default Remark: there is one exception (command: print definition). For this command pp.beta is still false. --- src/frontends/lean/builtin_cmds.cpp | 6 +++++- src/frontends/lean/pp.cpp | 29 +++++++++++++++++++++++++++- src/library/pp_options.cpp | 3 ++- src/library/pp_options.h | 1 + tests/lean/pp.lean | 2 +- tests/lean/pp_beta.lean | 7 +++++++ tests/lean/pp_beta.lean.expected.out | 2 ++ 7 files changed, 46 insertions(+), 4 deletions(-) create mode 100644 tests/lean/pp_beta.lean create mode 100644 tests/lean/pp_beta.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 7e7f2440a..89c9ce7ba 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -191,9 +191,13 @@ environment print_cmd(parser & p) { name c = p.check_constant_next("invalid 'print definition', constant expected"); environment const & env = p.env(); declaration d = env.get(c); + io_state_stream out = p.regular_stream(); + options opts = out.get_options(); + opts = opts.update_if_undef(get_pp_beta_name(), false); + io_state_stream new_out = out.update_options(opts); if (!d.is_definition()) throw parser_error(sstream() << "invalid 'print definition', '" << c << "' is not a definition", pos); - p.regular_stream() << d.get_value() << endl; + new_out << d.get_value() << endl; } else if (p.curr_is_token_or_id(get_instances_tk())) { p.next(); name c = p.check_constant_next("invalid 'print instances', constant expected"); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 4503bbce5..44eacffb9 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "library/abbreviation.h" #include "library/pp_options.h" #include "library/constants.h" +#include "library/replace_visitor.h" #include "frontends/lean/pp.h" #include "frontends/lean/token_table.h" #include "frontends/lean/builtin_exprs.h" @@ -1114,10 +1115,36 @@ pretty_fn::pretty_fn(environment const & env, options const & o): m_next_meta_idx = 1; } +// Custom beta reduction procedure for the pretty printer. +// We don't want to reduce application in show annotations. +class pp_beta_reduce_fn : public replace_visitor { + virtual expr visit_meta(expr const & e) { return e; } + virtual expr visit_local(expr const & e) { return e; } + + virtual expr visit_macro(expr const & e) { + if (is_show_annotation(e) && is_app(get_annotation_arg(e))) { + expr const & n = get_annotation_arg(e); + expr new_fn = visit(app_fn(n)); + expr new_arg = visit(app_arg(n)); + return mk_show_annotation(mk_app(new_fn, new_arg)); + } else { + return replace_visitor::visit_macro(e); + } + } + + virtual expr visit_app(expr const & e) { + expr new_e = replace_visitor::visit_app(e); + if (is_head_beta(new_e)) + return visit(head_beta_reduce(new_e)); + else + return new_e; + } +}; + format pretty_fn::operator()(expr const & e) { m_depth = 0; m_num_steps = 0; if (m_beta) - return pp_child(purify(beta_reduce(e)), 0).fmt(); + return pp_child(purify(pp_beta_reduce_fn()(e)), 0).fmt(); else return pp_child(purify(e), 0).fmt(); } diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index f356d87f1..25020cc10 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -52,7 +52,7 @@ Author: Leonardo de Moura #endif #ifndef LEAN_DEFAULT_PP_BETA -#define LEAN_DEFAULT_PP_BETA false +#define LEAN_DEFAULT_PP_BETA true #endif #ifndef LEAN_DEFAULT_PP_NUMERALS @@ -164,6 +164,7 @@ name const & get_pp_notation_option_name() { return *g_pp_notation; } name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; } name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; } name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; } +name const & get_pp_beta_name() { return *g_pp_beta; } unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index 157c734f4..75ee871cc 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -15,6 +15,7 @@ name const & get_pp_notation_option_name(); name const & get_pp_metavar_args_name(); name const & get_pp_purify_metavars_name(); name const & get_pp_purify_locals_name(); +name const & get_pp_beta_name(); unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); diff --git a/tests/lean/pp.lean b/tests/lean/pp.lean index 144942e54..e40742d9b 100644 --- a/tests/lean/pp.lean +++ b/tests/lean/pp.lean @@ -1,4 +1,4 @@ -prelude check λ {A : Type.{1}} (B : Type.{1}) (a : A) (b : B), a +prelude set_option pp.beta false check λ {A : Type.{1}} (B : Type.{1}) (a : A) (b : B), a check λ {A : Type.{1}} {B : Type.{1}} (a : A) (b : B), a check λ (A : Type.{1}) {B : Type.{1}} (a : A) (b : B), a check λ (A : Type.{1}) (B : Type.{1}) (a : A) (b : B), a diff --git a/tests/lean/pp_beta.lean b/tests/lean/pp_beta.lean new file mode 100644 index 000000000..1ff93c06a --- /dev/null +++ b/tests/lean/pp_beta.lean @@ -0,0 +1,7 @@ +open nat + +check (λ x : nat, x) 1 + +set_option pp.beta false + +check (λ x : nat, x) 1 diff --git a/tests/lean/pp_beta.lean.expected.out b/tests/lean/pp_beta.lean.expected.out new file mode 100644 index 000000000..e214e6af9 --- /dev/null +++ b/tests/lean/pp_beta.lean.expected.out @@ -0,0 +1,2 @@ +1 : ℕ +(λ (x : ℕ), x) 1 : ℕ