From 40cd50b1cabad092e223192b1b52bcd562709f8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Sep 2014 17:09:57 -0700 Subject: [PATCH] fix(frontends/lean/pp): add necessary '@' when pp.implicit is true, otherwise produced output will not even type check Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 22 ++++++++++++++++++++-- src/frontends/lean/pp.h | 1 + 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b5682fcbc..94117c8de 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -230,10 +230,28 @@ auto pretty_fn::pp_local(expr const & e) -> result { return mk_result(format(local_pp_name(e))); } +static name g_tmp_prefix = name::mk_internal_unique_name(); +bool pretty_fn::has_implicit_args(expr const & f) { + name_generator ngen(g_tmp_prefix); + expr type = m_tc.whnf(m_tc.infer(f).first).first; + while (is_pi(type)) { + binder_info bi = binding_info(type); + if (bi.is_implicit() || bi.is_strict_implicit()) + return true; + expr local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type)); + type = m_tc.whnf(instantiate(binding_body(type), local)).first; + } + return false; +} + auto pretty_fn::pp_app(expr const & e) -> result { - result res_fn = pp_child(app_fn(e), max_bp()-1); + expr const & fn = app_fn(e); + result res_fn = pp_child(fn, max_bp()-1); + format fn_fmt = res_fn.first; + if (m_implict && !is_app(fn) && has_implicit_args(fn)) + fn_fmt = compose(g_explicit_fmt, fn_fmt); result res_arg = pp_child(app_arg(e), max_bp()); - return mk_result(group(compose(res_fn.first, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1); + return mk_result(group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1); } format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info const & bi) { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index bdcfac8de..afaa75d98 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -52,6 +52,7 @@ private: result mk_result(format const & e) const { return mk_result(e, max_bp()); } bool is_implicit(expr const & f); bool is_prop(expr const & e); + bool has_implicit_args(expr const & f); format pp_binder_block(buffer const & names, expr const & type, binder_info const & bi); format pp_binders(buffer const & locals);