michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/pp): add necessary '@' when pp.implicit is true, otherwise produced output will not even type check

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-02 17:09:57 -07:00
parent 6077b3158c
commit 40cd50b1ca
2 changed files with 21 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<name> const & names, expr const & type, binder_info const & bi) {

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

@ -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<name> const & names, expr const & type, binder_info const & bi);
format pp_binders(buffer<expr> const & locals);