Skip to content

Commit

Permalink
basic code
Browse files Browse the repository at this point in the history
  • Loading branch information
trdthg committed Jul 5, 2024
1 parent 68c11d7 commit 5f5a769
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 25 deletions.
29 changes: 28 additions & 1 deletion src/lib/format_sail.ml
Original file line number Diff line number Diff line change
Expand Up @@ -440,6 +440,27 @@ module type CONFIG = sig
val config : config
end

let rec can_shrink_to_oneline cqs =
match cqs with
| [] -> true
| [cq] -> (
match List.of_seq (Queue.to_seq cq) with
| [] -> true
| [c] -> (
match c with
(* Atom is ok *)
| Atom _ -> true
(* {{{ Atom }}} is ok *)
| Block (_, exps) -> can_shrink_to_oneline exps
| If_then_else (_, i, t, e) -> can_shrink_to_oneline [t; e]
| _ -> false
)
| c :: cq ->
can_shrink_to_oneline [Queue.of_seq (List.to_seq [c])]
&& can_shrink_to_oneline [Queue.of_seq (List.to_seq cq)]
)
| cq :: cqs -> can_shrink_to_oneline [cq] && can_shrink_to_oneline cqs

module Make (Config : CONFIG) = struct
let indent = Config.config.indent
let preserve_structure = Config.config.preserve_structure
Expand Down Expand Up @@ -636,14 +657,20 @@ module Make (Config : CONFIG) = struct
)
| Pragma (pragma, arg) -> char '$' ^^ string pragma ^^ space ^^ string arg ^^ hardline
| Block (always_hardline, exps) ->
let always_hardline, indent, padding =
match exps with
| x :: [xs] -> (always_hardline, indent, 1)
| [x] -> if can_shrink_to_oneline exps then (false, 4, 1) else (always_hardline, indent, 1)
| _ -> (always_hardline, indent, 1)
in
let exps =
map_last
(fun no_semi chunks -> doc_block_exp_chunks (opts |> nonatomic |> statement_like) no_semi chunks)
exps
in
let sep = if always_hardline || List.exists snd exps then hardline else break 1 in
let exps = List.map fst exps in
surround_hardline always_hardline indent 1 (char '{') (separate sep exps) (char '}') |> atomic_parens opts
surround_hardline always_hardline indent padding (char '{') (separate sep exps) (char '}') |> atomic_parens opts
| Block_binder (binder, x, y) ->
if can_hang y then
separate space
Expand Down
16 changes: 4 additions & 12 deletions test/format/default/function_quant.expect
Original file line number Diff line number Diff line change
Expand Up @@ -3,24 +3,16 @@ default Order dec
$include <prelude.sail>

function foo forall 'n 'm, 'n >= 0.
(x : int('n), y : int('m)) -> unit = {
()
}
(x : int('n), y : int('m)) -> unit = { () }

function foo /* c */ forall 'n 'm, 'n >= 0.
(x : int('n), y : int('m)) -> unit = {
()
}
(x : int('n), y : int('m)) -> unit = { () }

function foo forall /* c */ 'n 'm, 'n >= 0.
(x : int('n), y : int('m)) -> unit = {
()
}
(x : int('n), y : int('m)) -> unit = { () }

function foo forall 'n 'm, /* c */ 'n >= 0.
(x : int('n), y : int('m)) -> unit = {
()
}
(x : int('n), y : int('m)) -> unit = { () }

function foo forall 'very_long_identifier_that_will_cause_a_line_break 'm, 'n >= 0.
(x : int('very_long_identifier_that_will_cause_a_line_break), y : int('m)) -> unit = {
Expand Down
18 changes: 18 additions & 0 deletions test/format/default/function_quant.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
default Order dec

$include <prelude.sail>

function foo forall 'n 'm, 'n >= 0.
(x : int('n), y : int('m)) -> unit = { () }

function foo /* c */ forall 'n 'm, 'n >= 0.
(x : int('n), y : int('m)) -> unit = { () }

function foo forall /* c */ 'n 'm, 'n >= 0.
(x : int('n), y : int('m)) -> unit = { () }

function foo forall 'n 'm, /* c */ 'n >= 0.
(x : int('n), y : int('m)) -> unit = { () }

function foo forall 'very_long_identifier_that_will_cause_a_line_break 'm, 'n >= 0.
(x : int('very_long_identifier_that_will_cause_a_line_break), y : int('m)) -> unit = { () }
16 changes: 4 additions & 12 deletions test/format/default/struct_update.expect
Original file line number Diff line number Diff line change
Expand Up @@ -44,22 +44,14 @@ enum E with f -> very_long_type_that_will_trigger_a_linebreak,
}

function has_loops () = {
foreach (n from 1 to 3) {
()
};
foreach (n from 3 downto 1) {
()
};
foreach (n from 0 to 4 by 2) {
()
};
foreach (n from 1 to 3) { () };
foreach (n from 3 downto 1) { () };
foreach (n from 0 to 4 by 2) { () };
foreach (n from 10000000000000000000000000000000 to 444444444444444444444444444444444444444444444444444444444444) {
()
};
while true do ();
while true do {
()
};
while true do { () };
repeat termination_measure { foo } () until true
}

Expand Down

0 comments on commit 5f5a769

Please sign in to comment.