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

Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-08 11:23:46 -07:00
parent df116f88e0
commit 59a589037e
2 changed files with 21 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/frontends/lean/lean_pp.cpp
View file

@ -856,35 +856,27 @@ class pp_fn {
++it2; ++it2;
bool implicit = is_implicit(implicit_args, arg_pos); bool implicit = is_implicit(implicit_args, arg_pos);
++arg_pos; ++arg_pos;
if (!implicit && !is_lambda(e) && arg_pos > arrow_starting_at) { if (!implicit_args && arg_pos > arrow_starting_at) {
// the rest is an arrow, but we must check if we are not missing implicit annotations. // The rest is an arrow
auto it2_aux = it2; // We do not use arrow pp when implicit_args marks are used.
unsigned arg_pos_aux = arg_pos; format block;
while (it2_aux != end && !is_implicit(implicit_args, arg_pos_aux)) { bool first_domain = true;
++arg_pos_aux; for (; it != end; ++it) {
++it2_aux; result p_domain = pp_arrow_child(it->second, depth);
} r_weight += p_domain.second;
if (it2_aux == end) { if (first_domain) {
// the rest is a sequence of arrows. first_domain = false;
format block; block = p_domain.first;
bool first_domain = true; } else {
for (; it != end; ++it) { block += format{space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_domain.first};
result p_domain = pp_arrow_child(it->second, depth);
r_weight += p_domain.second;
if (first_domain) {
first_domain = false;
block = p_domain.first;
} else {
block += format{space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_domain.first};
}
} }
result p_body = pp_arrow_child(b, depth);
r_weight += p_body.second;
block += format{space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_body.first};
block = group(block);
format r_format = group(nest(head_indent, format{head, space(), group(bindings), body_sep, line(), block}));
return mk_result(r_format, r_weight);
} }
result p_body = pp_arrow_child(b, depth);
r_weight += p_body.second;
block += format{space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_body.first};
block = group(block);
format r_format = group(nest(head_indent, format{head, space(), group(bindings), body_sep, line(), block}));
return mk_result(r_format, r_weight);
} }
// Continue with standard encoding // Continue with standard encoding
while (it2 != end && it2->second == it->second && implicit == is_implicit(implicit_args, arg_pos)) { while (it2 != end && it2->second == it->second && implicit == is_implicit(implicit_args, arg_pos)) {

4
tests/lean/elab4.lean.expected.out
View file

@ -5,9 +5,9 @@
Assumed: R Assumed: R
Proved: R2 Proved: R2
Set: lean::pp::implicit Set: lean::pp::implicit
Variable C {A B : Type} : (A = B) → A → B Variable C {A B : Type} (H : A = B) (a : A) : B
Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a
Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} : ((Π x : A, B x) = (Π x : A', B' x)) → (A = A') Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) : A = A'
Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A = Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A =
A' := A' :=
D H D H