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

feat(src/frontends/lean/pp): option to print theorem statements instead of proof terms

Browse source 
Conflicts:
	src/frontends/lean/pp.cpp
	src/library/pp_options.cpp
This commit is contained in:
Daniel Selsam 2016-04-16 16:37:35 -07:00 • committed by Leonardo de Moura
parent 533d1ab130
commit 4d77f5ab2d
6 changed files with 63 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -283,6 +283,7 @@ void pretty_fn::set_options_core(options const & _o) {
bool all = get_pp_all(o);
if (all) {
o = o.update_if_undef(get_pp_implicit_name(), true);
o = o.update_if_undef(get_pp_proofs_name(), true);
o = o.update_if_undef(get_pp_coercions_name(), true);
o = o.update_if_undef(get_pp_notation_name(), false);
o = o.update_if_undef(get_pp_universes_name(), true);
@ -298,6 +299,7 @@ void pretty_fn::set_options_core(options const & _o) {
m_max_depth = get_pp_max_depth(o);
m_max_steps = get_pp_max_steps(o);
m_implict = get_pp_implicit(o);
m_proofs = get_pp_proofs(o);
m_unicode = get_pp_unicode(o);
m_coercion = get_pp_coercions(o);
m_notation = get_pp_notation(o);
@ -329,6 +331,25 @@ format pretty_fn::pp_level(level const & l) {
return ::lean::pp(l, m_unicode, m_indent);
}
// Returns the theorem type if `f` has a Pi type with binding domain a Prop,
// and `m_proofs` is set to false.
optional<expr> pretty_fn::arg_is_proof(expr const & f) {
if (m_proofs)
return none_expr(); // showing proof terms
if (!closed(f))
// the Lean type checker assumes expressions are closed.
return none_expr();
try {
expr t = m_ctx.relaxed_whnf(m_ctx.infer(f));
if (is_pi(t) && is_prop(binding_domain(t)))
return some_expr(binding_domain(t));
else
return none_expr();
} catch (exception &) {
return none_expr();
}
}
bool pretty_fn::is_implicit(expr const & f) {
// Remark: we assume preterms do not have implicit arguments,
// since they have not been elaborated yet.
@ -533,6 +554,8 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul
return pp_abbreviation(e, *it, true, bp, ignore_hide);
} else if (is_implicit(f)) {
return pp_child(f, bp, ignore_hide);
} else if (auto thm = arg_is_proof(f)) {
return pp_child_core(mk_app(f, mk_inaccessible(*thm)), bp, ignore_hide);
} else if (!m_coercion && is_coercion(m_env, f)) {
return pp_coercion(e, bp, ignore_hide);
}

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

@ -55,6 +55,7 @@ private:
unsigned m_max_depth;
unsigned m_max_steps;
bool m_implict; //!< if true show implicit arguments
bool m_proofs; //!< if true show proof terms
bool m_unicode; //!< if true use unicode chars
bool m_coercion; //!< if true show coercions
bool m_num_nat_coe; //!< truen when !m_coercion && env has coercion from num -> nat
@ -80,6 +81,7 @@ private:
level purify(level const & l);
expr purify(expr const & e);
bool is_implicit(expr const & f);
optional<expr> arg_is_proof(expr const & f);
bool is_prop(expr const & e);
bool has_implicit_args(expr const & f);
optional<name> is_aliased(name const & n) const;

16
src/library/pp_options.cpp
View file

@ -23,6 +23,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_IMPLICIT false
#endif
#ifndef LEAN_DEFAULT_PP_PROOFS
#define LEAN_DEFAULT_PP_PROOFS true
#endif
#ifndef LEAN_DEFAULT_PP_COERCIONS
#define LEAN_DEFAULT_PP_COERCIONS false
#endif
@ -101,6 +105,7 @@ static name * g_pp_max_depth = nullptr;
static name * g_pp_max_steps = nullptr;
static name * g_pp_notation = nullptr;
static name * g_pp_implicit = nullptr;
static name * g_pp_proofs = nullptr;
static name * g_pp_coercions = nullptr;
static name * g_pp_universes = nullptr;
static name * g_pp_full_names = nullptr;
@ -126,6 +131,7 @@ void initialize_pp_options() {
g_pp_max_steps = new name{"pp", "max_steps"};
g_pp_notation = new name{"pp", "notation"};
g_pp_implicit = new name{"pp", "implicit"};
g_pp_proofs = new name{"pp", "proofs"};
g_pp_coercions = new name{"pp", "coercions"};
g_pp_universes = new name{"pp", "universes"};
g_pp_full_names = new name{"pp", "full_names"};
@ -153,6 +159,8 @@ void initialize_pp_options() {
"(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
register_bool_option(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT,
"(pretty printer) display implicit parameters");
register_bool_option(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS,
"(pretty printer) display proof terms");
register_bool_option(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS,
"(pretty printer) display coercionss");
register_bool_option(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES,
@ -190,17 +198,18 @@ void initialize_pp_options() {
register_bool_option(*g_pp_lazy_abstraction, LEAN_DEFAULT_PP_LAZY_ABSTRACTION,
"(pretty printer) display lazy-abstraction macros (for debugging purposes)");
register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL,
"(pretty printer) display coercions, implicit parameters, fully qualified names, universes, "
"(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, "
"and disable abbreviations, beta reduction and notation during pretty printing");
options universes_true(*g_pp_universes, true);
options full_names_true(*g_pp_full_names, true);
options implicit_true(*g_pp_implicit, true);
options proofs_true(*g_pp_proofs, true);
options coercions_true(*g_pp_coercions, true);
options notation_false(*g_pp_notation, false);
options binder_types_true(*g_pp_binder_types, true);
options implicit_coercions = join(coercions_true, implicit_true);
options implicit_notation = join(notation_false, implicit_true);
options all = universes_true + implicit_true + coercions_true + notation_false + full_names_true + binder_types_true;
options all = universes_true + implicit_true + proofs_true + coercions_true + notation_false + full_names_true + binder_types_true;
g_distinguishing_pp_options = new list<options>({implicit_true, full_names_true, coercions_true, implicit_coercions,
implicit_notation, universes_true, all});
}
@ -214,6 +223,7 @@ void finalize_pp_options() {
delete g_pp_max_steps;
delete g_pp_notation;
delete g_pp_implicit;
delete g_pp_proofs;
delete g_pp_coercions;
delete g_pp_universes;
delete g_pp_full_names;
@ -232,6 +242,7 @@ void finalize_pp_options() {
}
name const & get_pp_implicit_name() { return *g_pp_implicit; }
name const & get_pp_proofs_name() { return *g_pp_proofs; }
name const & get_pp_coercions_name() { return *g_pp_coercions; }
name const & get_pp_full_names_name() { return *g_pp_full_names; }
name const & get_pp_universes_name() { return *g_pp_universes; }
@ -250,6 +261,7 @@ unsigned get_pp_max_depth(options const & opts) { return opts.get_unsign
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
bool get_pp_notation(options const & opts) { return opts.get_bool(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
bool get_pp_implicit(options const & opts) { return opts.get_bool(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
bool get_pp_proofs(options const & opts) { return opts.get_bool(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS); }
bool get_pp_coercions(options const & opts) { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
bool get_pp_universes(options const & opts) { return opts.get_bool(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
bool get_pp_full_names(options const & opts) { return opts.get_bool(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }

2
src/library/pp_options.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "util/sexpr/options.h"
namespace lean {
name const & get_pp_implicit_name();
name const & get_pp_proofs_name();
name const & get_pp_coercions_name();
name const & get_pp_full_names_name();
name const & get_pp_universes_name();
@ -26,6 +27,7 @@ unsigned get_pp_max_depth(options const & opts);
unsigned get_pp_max_steps(options const & opts);
bool get_pp_notation(options const & opts);
bool get_pp_implicit(options const & opts);
bool get_pp_proofs(options const & opts);
bool get_pp_coercions(options const & opts);
bool get_pp_universes(options const & opts);
bool get_pp_full_names(options const & opts);

16
tests/lean/pp_no_proofs.lean Normal file
View file

@ -0,0 +1,16 @@
import data.nat
open nat
constants (P : ∀ {t:true}, ℕ → Prop) (P0 : @P trivial 0)
(Ps : ∀ {n}, @P trivial n → @P trivial (succ n))
(f : Π {n}, @P trivial n → ℕ)
definition messy := f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
eval messy
set_option pp.proofs false
eval messy
set_option pp.implicit true
eval messy
set_option pp.proofs true
eval messy

6
tests/lean/pp_no_proofs.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
f ⌞P 6⌟
@f 6 ⌞@P ⌞true⌟ 6⌟
@f 6
(@Ps (succ (succ (succ (succ (succ 0)))))
(@Ps (succ (succ (succ (succ 0)))) (@Ps (succ (succ (succ 0))) (@Ps (succ (succ 0)) (@Ps (succ 0) (@Ps 0 P0))))))