fix(frontends/lean/pp): when formatting a coercion to function-class

that contains implicit arguments
This commit is contained in:
Leonardo de Moura 2014-09-20 09:56:46 -07:00
parent fd5daa8fda
commit 8fe7465ade
4 changed files with 42 additions and 4 deletions

View file

@ -152,17 +152,41 @@ bool pretty_fn::is_prop(expr const & e) {
}
}
auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz) -> result {
if (sz == 1) {
return pp_child(app_arg(e), max_bp()-1);
} else if (is_app(e) && is_implicit(app_fn(e))) {
return pp_coercion_fn(app_fn(e), sz-1);
} else {
expr const & fn = app_fn(e);
result res_fn = pp_coercion_fn(fn, sz-1);
format fn_fmt = res_fn.first;
if (m_implict && sz == 2 && 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(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1);
}
}
auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result {
buffer<expr> args;
expr const & f = get_app_args(e, args);
optional<pair<name, unsigned>> r = is_coercion(m_env, f);
lean_assert(r);
if (r->second >= args.size())
if (r->second >= args.size()) {
return pp_child_core(e, bp);
else if (r->second == args.size() - 1)
} else if (r->second == args.size() - 1) {
return pp_child(args.back(), bp);
else
return pp_child(mk_app(args.size() - r->second, args.data() + r->second), bp);
} else {
unsigned sz = args.size() - r->second;
lean_assert(sz >= 2);
auto r = pp_coercion_fn(e, sz);
if (r.second < bp) {
return mk_result(paren(r.first));
} else {
return r;
}
}
}
auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {

View file

@ -59,6 +59,7 @@ private:
format pp_binders(buffer<expr> const & locals);
format pp_level(level const & l);
result pp_coercion_fn(expr const & e, unsigned sz);
result pp_coercion(expr const & e, unsigned bp);
result pp_child_core(expr const & e, unsigned bp);
result pp_child(expr const & e, unsigned bp);

12
tests/lean/coe.lean Normal file
View file

@ -0,0 +1,12 @@
import logic
set_option pp.notation false
inductive Functor :=
mk : (Π (A B : Type), A → B) → Functor
definition Functor.to_fun [coercion] (f : Functor) {A B : Type} : A → B :=
Functor.rec (λ f, f) f A B
variable f : Functor
check f 0 = 0

View file

@ -0,0 +1 @@
eq (f 0) 0 : Prop