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

fix(frontends/lean/pp): insert line breaks in notations

Browse source
This commit is contained in:
Gabriel Ebner 2017-04-28 19:54:15 +02:00
parent 701b51a882
commit 8554b8eac1
5 changed files with 51 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1336,6 +1336,16 @@ static bool is_atomic_notation(notation_entry const & entry) {
return head(ts).get_action().kind() == notation::action_kind::Skip;
}
static format mk_tk_fmt(name const & tkn) {
auto tk = tkn.to_string();
if (!tk.empty() && tk.back() == ' ') {
tk.pop_back();
return format(tk) + line();
} else {
return format(tk);
}
}
auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>> & args) -> optional<result> {
if (entry.is_numeral()) {
return some(result(format(entry.get_num().to_string())));
@ -1357,7 +1367,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
format curr;
notation::action const & a = ts[i].get_action();
name const & tk = ts[i].get_token();
format tk_fmt = format(ts[i].get_pp_token());
format tk_fmt = mk_tk_fmt(ts[i].get_pp_token());
switch (a.kind()) {
case notation::action_kind::Skip:
curr = tk_fmt;
@ -1502,7 +1512,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
format e_fmt = pp_notation_child(e, token_lbp, 0).fmt();
fmt = e_fmt + fmt;
}
return optional<result>(result(first_lbp, last_rbp, fmt));
return optional<result>(result(first_lbp, last_rbp, group(nest(m_indent, fmt))));
}
}

10
tests/lean/elab13.lean.expected.out
View file

@ -1,6 +1,8 @@
λ (c : name),
get_env >>= λ (env : environment),
returnex (environment.get env c) >>= λ (decl : declaration),
return (length (declaration.univ_params decl)) >>= λ (num : ℕ),
mk_num_meta_univs 2 >>= λ (ls : list level), return (expr.const c ls) :
get_env >>=
λ (env : environment),
returnex (environment.get env c) >>=
λ (decl : declaration),
return (length (declaration.univ_params decl)) >>=
λ (num : ℕ), mk_num_meta_univs 2 >>= λ (ls : list level), return (expr.const c ls) :
name → tactic expr

18
tests/lean/long_term.lean Normal file
View file

@ -0,0 +1,18 @@
def long_term :=
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1) =
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)+
(1+1+1+1+1+1+1+1+1)
#print long_term

12
tests/lean/long_term.lean.expected.out Normal file
View file

@ -0,0 +1,12 @@
def long_term : Prop :=
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) =
1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1)

5
tests/lean/print_meta.lean.expected.out
View file

@ -1,4 +1,5 @@
meta def tactic.intro : name → tactic expr :=
λ (n : name),
tactic.target >>= λ (t : expr),
ite (↑(expr.is_pi t) ∨ ↑(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)
tactic.target >>=
λ (t : expr),
ite (↑(expr.is_pi t) ∨ ↑(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)