Skip to content

Commit

Permalink
Start multi-line pretty printing
Browse files Browse the repository at this point in the history
  • Loading branch information
Negabinary committed May 3, 2024
1 parent 65a2456 commit 796d23c
Show file tree
Hide file tree
Showing 5 changed files with 70 additions and 9 deletions.
10 changes: 10 additions & 0 deletions src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
Expand Up @@ -435,3 +435,13 @@ let segment_width = (seg: Segment.t): int =>
of_segment(seg).rows,
0,
);

let width_cost = (seg: Segment.t, max_width: int): int =>
IntMap.fold(
(_, {max_col, _}: Rows.shape, acc) => {
let overflow = max(max_col - max_width, 0);
acc + overflow * overflow;
},
of_segment(seg).rows,
0,
);
28 changes: 21 additions & 7 deletions src/haz3lcore/pretty/ExpToSegment.re
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,7 @@ let should_add_space = (s1, s2) =>
| _ when String.starts_with(s2, ~prefix=" ") => false
| _ when String.ends_with(s1, ~suffix="\n") => false
| _ when String.starts_with(s2, ~prefix="\n") => false
| _ =>
print_endline("(\"" ++ s1 ++ "\")(\"" ++ s2 ++ "\")");
true;
| _ => true
};

let text_to_pretty = (id, sort, str): pretty => {
Expand All @@ -39,7 +37,6 @@ let mk_form = (form_name: string, id, children): Piece.t => {
let children =
Aba.map_abas(
((l, child, r)) => {
let _ = print_endline("l: " ++ l ++ " r: " ++ r);
let lspace = should_add_space(l, child |> Segment.first_string);
let rspace = should_add_space(child |> Segment.last_string, r);
(lspace ? [Secondary(Secondary.mk_space(Id.mk()))] : [])
Expand Down Expand Up @@ -106,7 +103,7 @@ let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
let (id, ids) = (exp.ids |> List.hd, exp.ids |> List.tl);
let* x = go(x)
and* xs = xs |> List.map(go) |> all;
p_just([
let form = (x, xs) =>
mk_form(
"list_lit_exp",
id,
Expand All @@ -120,8 +117,25 @@ let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
),
),
],
),
]);
);
p_just([form(x, xs)])
|> p_orif(
!inline,
p_just(
{
let x = [Secondary(Secondary.mk_newline(Id.mk()))] @ x;
let xs =
xs
|> List.map(x =>
[Secondary(Secondary.mk_newline(Id.mk()))] @ x
)
|> ListUtil.map_last_only(x =>
x @ [Secondary(Secondary.mk_newline(Id.mk()))]
);
[form(x, xs)];
},
),
);
| Var(v) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v)
| BinOp(op, l, r) =>
// TODO: Add optional newlines
Expand Down
20 changes: 19 additions & 1 deletion src/haz3lcore/pretty/PrettySegment.re
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,12 @@ let p_concat = (pretty2, pretty1) =>
List.map(piece1 => List.map(piece2 => piece1 @ piece2, pretty2), pretty1)
|> List.flatten;
let p_or = (pretty2, pretty1) => pretty1 @ pretty2;
let p_orif = (cond, pretty2, pretty1) => if (cond) {pretty1} else {pretty2};
let p_orif = (cond, pretty2, pretty1) =>
if (cond) {
pretty1 @ pretty2;
} else {
pretty2;
};
let p_just = segment => [segment];

let p_concat = (pretties: list(pretty)) =>
Expand All @@ -26,3 +31,16 @@ let rec all =
let rest = all(xs);
List.flatten(List.map(x => List.map(rest => [x, ...rest], rest), x));
};

let select: pretty => Segment.t =
seg =>
ListUtil.minimum(
s => {
let u =
Measured.width_cost(s, 80) * 100 + Measured.segment_height(s);
print_endline(string_of_int(u));
u;
},
seg,
)
|> Option.get;
3 changes: 2 additions & 1 deletion src/haz3lweb/view/dhcode/DHCode.re
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,8 @@ let view =
) => {
let parenthesized = ExpToSegment.parenthesize(d);
let options = ExpToSegment.exp_to_pretty(~inline=false, parenthesized);
let option = List.hd(options);
let _ = print_endline("options: " ++ string_of_int(List.length(options)));
let option = PrettySegment.select(options);
let editor = Editor.init(~read_only=true, Zipper.unzip(option));
let code_text_view =
Code.view(~sort=Sort.root, ~font_metrics, ~settings, editor);
Expand Down
18 changes: 18 additions & 0 deletions src/util/ListUtil.re
Original file line number Diff line number Diff line change
Expand Up @@ -547,3 +547,21 @@ let rec split_last = (xs: list('x)): (list('x), 'x) =>
let (prefix, last) = split_last(xs);
([x, ...prefix], last);
};

let minimum = (f: 'a => int, xs: list('a)): option('a) =>
switch (xs) {
| [] => None
| [x, ...xs] =>
let rec loop = (best: 'a, best_f: int, xs: list('a)): option('a) =>
switch (xs) {
| [] => Some(best)
| [x, ...xs] =>
let f_x = f(x);
if (f_x < best_f) {
loop(x, f_x, xs);
} else {
loop(best, best_f, xs);
};
};
loop(x, f(x), xs);
};

0 comments on commit 796d23c

Please sign in to comment.