diff --git a/src/lib/format_sail.ml b/src/lib/format_sail.ml index 2f48005f7..592f78e93 100644 --- a/src/lib/format_sail.ml +++ b/src/lib/format_sail.ml @@ -77,11 +77,28 @@ let rec map_last f = function let x = f false x in x :: map_last f xs -let line_comment_opt = function Comment (Lexer.Comment_line, _, _, contents, _trailing) -> Some contents | _ -> None let is_comment chunk = match chunk with Comment (_, _, _, _, _) | Doc_comment _ -> true | _ -> false let is_block chunk = match chunk with Block (_, _) -> true | _ -> false +let is_match chunk = match chunk with Match _ -> true | _ -> false let is_let chunk = match chunk with Binder (_, _, _, _) -> true | _ -> false +let rec function_with_only_one_rule ?(ignore_rule = fun chunk -> false) chunks target_rule = + let rec go chunks target_count other_count = + match chunks with + | [] -> (target_count, other_count) + | hd :: tl -> + let target_count, other_count = + if target_rule hd then (target_count + 1, other_count) + else if ignore_rule hd then (target_count, other_count) + else (target_count, other_count + 1) + in + go tl target_count other_count + in + let target, other = go chunks 0 0 in + target = 1 && other = 0 + +let rec chunks_one_block_like chunks = function_with_only_one_rule chunks (fun chunk -> is_block chunk || is_match chunk) + (* Remove additional (> 1) trailing newlines at the end of a string *) let discard_extra_trailing_newlines s = let len = String.length s in @@ -194,8 +211,6 @@ module PPrintWrapper = struct let group doc = Group doc - let group_indent doc n = group (nest n doc) - let space = char ' ' let enclose l r x = l ^^ x ^^ r @@ -217,6 +232,15 @@ module PPrintWrapper = struct let surround n b opening contents closing = opening ^^ Nest (n, break b ^^ contents) ^^ break b ^^ closing + let surround_hardline ?(is_block = true) h n b opening contents closing = + let b = if h then hardline else break b in + group (opening ^^ nest n (b ^^ contents) ^^ (if is_block then b else empty) ^^ closing) + + let group_indent n doc = group (nest n doc) + let prefix_hardline h n b contents = + let b = if h then hardline else break b in + group (nest n (b ^^ contents)) + let repeat n doc = let rec go n acc = if n = 0 then acc else go (n - 1) (doc ^^ acc) in go n empty @@ -383,10 +407,6 @@ let softline = break 0 let prefix_parens n x y = x ^^ ifflat space (space ^^ char '(') ^^ nest n (softline ^^ y) ^^ softline ^^ ifflat empty (char ')') -let surround_hardline ?(is_block = true) h n b opening contents closing = - let b = if h then hardline else break b in - group (opening ^^ nest n (b ^^ contents) ^^ (if is_block then b else empty) ^^ closing) - type config = { indent : int; preserve_structure : bool; line_width : int; ribbon_width : float } let default_config = { indent = 4; preserve_structure = false; line_width = 120; ribbon_width = 1. } @@ -455,6 +475,8 @@ let rec can_chunks_list_wrap cqs = match c with (* Atom *) | Atom _ -> true + (* Xs[unsigned(r)], *) + | App (_, chunks) -> can_chunks_list_wrap chunks (* unit => (), *) | Delim _ | Opt_delim _ -> true (* (v128 >> shift)[64..0] *) @@ -483,25 +505,6 @@ module Make (Config : CONFIG) = struct let indent = Config.config.indent let preserve_structure = Config.config.preserve_structure - let rec function_with_only_one_rule chunks target_rule ignore_rule = - let rec go chunks target_count other_count = - match chunks with - | [] -> (target_count, other_count) - | hd :: tl -> - let target_count, other_count = - if target_rule hd then (target_count + 1, other_count) - else if ignore_rule hd then (target_count, other_count) - else (target_count, other_count + 1) - in - go tl target_count other_count - in - let target, other = go chunks 0 0 in - target = 1 && other = 0 - - let rec function_with_only_one_blcok chunks = function_with_only_one_rule chunks is_block is_comment - - let rec function_with_only_one_let chunks = function_with_only_one_rule chunks is_let is_comment - let rec doc_chunk ?(ungroup_tuple = false) ?(toplevel = false) ?(force_block_comment_end_with_hardline = false) opts = function | Atom s -> string s @@ -548,7 +551,7 @@ module Make (Config : CONFIG) = struct let doc = infix indent spacing (string op) (doc_chunks (opts |> lhs_prec |> expression_like) lhs) - (doc_chunks (opts |> rhs_prec |> expression_like) rhs) + (doc_chunks ~force_block_comment_end_with_hardline:true (opts |> rhs_prec |> expression_like) rhs) in if outer_prec > opts.precedence then parens doc else doc | Ternary (x, op1, y, op2, z) -> @@ -579,8 +582,8 @@ module Make (Config : CONFIG) = struct let doc_i = separate space [string "if"; i] in let doc_t = separate space [string "then"; t] in let doc_e = separate space [string "else"; e] in - let sep = space in - doc_i ^^ sep ^^ doc_t ^^ sep ^^ doc_e ^^ sep |> atomic_parens opts + let sep is_wrap = if is_wrap then space else hardline in + doc_i ^^ sep i_wrap ^^ doc_t ^^ sep t_wrap ^^ doc_e |> atomic_parens opts | If_then (bracing, i, t) -> let i = doc_chunks (opts |> nonatomic |> expression_like) i in let t = @@ -600,7 +603,8 @@ module Make (Config : CONFIG) = struct let exp_doc, exp_wrap = doc_exps (opts |> atomic |> expression_like) exp in let exp_doc = group (empty ^^ nest 4 exp_doc ^^ empty) in let ix_doc, ix_wrap = doc_exps (opts |> nonatomic |> expression_like) ix in - exp_doc ^^ char '[' ^^ ix_doc ^^ char ']' |> subatomic_parens opts + let hl = if ix_wrap then empty else hardline in + exp_doc ^^ char '[' ^^ ix_doc ^^ hl ^^ char ']' |> subatomic_parens opts | Exists ex -> let ex_doc = doc_chunks (atomic opts) ex.vars @@ -723,17 +727,9 @@ module Make (Config : CONFIG) = struct separate space [string (binder_keyword binder); doc_chunks (atomic opts) x; char '='] ^^ nest 4 (hardline ^^ doc_chunks (nonatomic opts) y) | Binder (binder, x, y, z) -> - let doc = - separate space - [ - string (binder_keyword binder); - doc_chunks (atomic opts) x; - char '='; - doc_chunks (nonatomic opts) y; - string "in"; - hardline; - ] - in + let x, _ = doc_exps (atomic opts) x in + let y, _ = doc_exps (atomic opts) y in + let doc = separate space [string (binder_keyword binder); x; char '='; y; string "in"; hardline] in Queue.fold (fun acc chunk -> let doc = doc_chunk ~force_block_comment_end_with_hardline:true opts chunk in @@ -788,16 +784,30 @@ module Make (Config : CONFIG) = struct and doc_exps ?(ungroup_tuple = false) opts exps = let res = Queue.fold (fun doc chunk -> doc ^^ doc_chunk ~ungroup_tuple opts chunk) empty exps in - let is_single_block = function_with_only_one_blcok (List.of_seq (Queue.to_seq exps)) in - if can_chunks_list_wrap [exps] then (res, true) - else ( - Printf.printf "exps_len: %d\n" (Queue.length exps); - ( (* add indent for multi line exps which can't be wrapped *) - (* TODO: add () here, need to handle `,`, like `0b00000 => /**/ EXTZ(0x0),` *) - surround_hardline ~is_block:is_single_block false 4 0 empty res empty, - false - ) - ) + + let no_prefix = chunks_one_block_like (List.of_seq (Queue.to_seq exps)) in + let wrapped = can_chunks_list_wrap [exps] in + let doc = + if wrapped || no_prefix then res + else + (* 1. add indent for multi line exps which can't be wrapped *) + (* 2. add hardline / space + * - if_stmt: + if + let a = 1 in + a + then { + // comment + 1 + } else { 2 } + + - i has no braces, use hardline + - t has braces, use space + - e wraped, use space + *) + prefix_hardline false 4 0 res + in + (doc, wrapped) and doc_pexp_chunks_pair opts pexp = let pat = doc_chunks opts pexp.pat in @@ -821,6 +831,7 @@ module Make (Config : CONFIG) = struct match pexp.guard with | None -> let body_doc, _ = doc_exps opts pexp.body in + (if pexp.funcl_space then space else empty) ^^ group (doc_chunks ~ungroup_tuple:true opts pexp.pat ^^ return_typ) ^^ string "=" ^^ space ^^ body_doc @@ -864,8 +875,10 @@ module Make (Config : CONFIG) = struct let doc = splice_into_doc chunks empty in (group doc, !requires_hardline) - and doc_chunks ?(ungroup_tuple = false) opts chunks = - Queue.fold (fun doc chunk -> doc ^^ doc_chunk ~ungroup_tuple opts chunk) empty chunks + and doc_chunks ?(ungroup_tuple = false) ?(force_block_comment_end_with_hardline = false) opts chunks = + Queue.fold + (fun doc chunk -> doc ^^ doc_chunk ~force_block_comment_end_with_hardline ~ungroup_tuple opts chunk) + empty chunks let to_string doc = let b = Buffer.create 1024 in diff --git a/test/format/default/demo.sail b/test/format/default/demo.sail new file mode 100644 index 000000000..055f38f7b --- /dev/null +++ b/test/format/default/demo.sail @@ -0,0 +1,6 @@ + +function rX r = match r { + _ => + // + Xs[unsigned(r)], +} diff --git a/test/format/default/pat_exps.expect b/test/format/default/pat_exps.expect new file mode 100644 index 000000000..8a692a46f --- /dev/null +++ b/test/format/default/pat_exps.expect @@ -0,0 +1,238 @@ +function one_atom () = + /* comment */ + 0b1 + +function one_binary_op () = + // + a + 1 + +function haveXcheri () -> bool = + /* This is a necessary but not sufficient condition, but should do for now. */ + misa.X == 0b1 + +function one_binary_op () = + // + { + let a = 1; + 1 + } + +function let_in_once_without_trailing_comment () = + let a = 1 in + a + +function let_in_once_with_trailing_comment () = + // comment + let a = 1 in + a + 1 + +function shift_right_arith64(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[63..0] + +function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[63 > 0] + +function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[ + let a = 1 in + 63 > 0 + ] + +function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + let a = + (if + let a = 1 in + a > 1 + then { + let a = 1 in + 63 > 0 + } else { + let a = 1 in + if a > 1 then { 1 } else { + let a = 1 in + a + } + }) in + (v128 >> shift)[ + if + let a = 1 in + a > 1 + then + let a = 1 in + 63 > 0 + else + let a = 1 in + if a > 1 then 1 else + let a = 1 in + a + ] + +function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[ + if + let a = 1 in + a > 1 + then { + let a = 1 in + 63 > 0 + } else { + let a = 1 in + if a > 1 then { 1 } else { + let a = 1 in + a + } + } + ] + +function let_in_once_with_comment () = + // + // 2. commend in a and = + let /**/ a = /**/ /**/ 1 in + /**/ + // + a + 1 + +// 3. multi line should be better? +function let_in_twice () = + // + let a = 1 in + let b = 1 in + a + 1 + +function let_in_three () = + // + let a = 1 in + let b = 1 in + /*let c = 1; is not valid now */ + a + 1 + +function let_in_once2 () = + // + let a = 1 in + a + 1 + +function atom_with_braces () = + // + { 1 } + +function exps_with_braces () = + // + { + let a = 1; + a + 1 + } + +function if_stmt () = if a > 1 then { 1 } else { 2 } + +function if_stmt () = if a > 1 then { + let a = 1 in + 1 // comment +} else { + let a = 1 in + 2 +} + +function if_stmt () = + if + let a = 1 in + if a > 1 then { 2 } else { 3 } + then { 2 } else { 3 } + +function if_stmt () = + if + let a = 1 in + if a > 1 then { + 2 // comment + } else { 3 } + then { + // comment + 2 + } else { + 3 + // comment + } + +function if_stmt () = + if + let a = 1 in + if a > 1 then { + 2 /* comment */ + } else { 3 } + then { + /* comment */ + 2 + } else { + 3 + /* comment */ + } + +function let_with_if_stmt () = + let a = 1 in + if a > 1 then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + /* comment */ + if a > 1 then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + /* comment */ + if + //comment + a > 1 + then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ + then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ + then { + /* comment */ 1 + } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ + then { + /* comment */ 1 /* comment */ + } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ + then { + /* comment */ 1 /* comment */ + } else { + /* comment */ 2 + } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ + then { + /* comment */ 1 /* comment */ + } else { + /* comment */ 2 + } /* comment */ diff --git a/test/format/default/patterns.expect b/test/format/default/patterns.expect index 0e63b877c..dc77c3930 100644 --- a/test/format/default/patterns.expect +++ b/test/format/default/patterns.expect @@ -15,17 +15,16 @@ function foo(ys : bits(6), xs : bits(6)) -> unit = { () } -function rX r = - match r { - 0b00000 => /**/ EXTZ(0x0), - 0b00001 => - /**/ - EXTZ(0x1), - 0b00001 => { - /**/ - EXTZ(0x1) - }, - _ => - // - Xs[unsigned(r)], - } +function rX r = match r { + 0b00000 => /**/ EXTZ(0x0), + 0b00001 => + /**/ + EXTZ(0x1), + 0b00001 => { + /**/ + EXTZ(0x1) + }, + _ => + // + Xs[unsigned(r)], +} diff --git a/test/format/default/wrap_into_oneline.expect b/test/format/default/wrap_into_oneline.expect index c6fbcd8c1..cfab34398 100644 --- a/test/format/default/wrap_into_oneline.expect +++ b/test/format/default/wrap_into_oneline.expect @@ -73,12 +73,26 @@ function f b = /* comment */ if b == bitone then { bitzero } else { bitone } function f b = /* comment */ if b == bitone then { bitzero } else { bitone } // TODO function f b =/* comment */if b == bitone then bitzero else bitone -function f b = if /* comment */ b == bitone then { bitzero } else { bitone } -function f b = if b == /* comment */ bitone then { bitzero } else { bitone } -function f b = if b == /* comment */ bitone then { bitzero } else { bitone } +function f b = + if /* comment */ b == bitone + then { bitzero } else { bitone } +function f b = + if + b == + /* comment */ + bitone + then { bitzero } else { bitone } +function f b = + if + b == + /* comment */ + bitone + then { bitzero } else { bitone } // TODO function f b = if b ==/* comment */bitone then bitzero else bitone -function f b = if b == bitone /* comment */ then { bitzero } else { bitone } +function f b = + if b == bitone /* comment */ + then { bitzero } else { bitone } function f b = if b == bitone then { /* comment */ bitzero } else { bitone } diff --git a/test/format/pat_exps.sail b/test/format/pat_exps.sail index c07894c93..b6b2847e1 100644 --- a/test/format/pat_exps.sail +++ b/test/format/pat_exps.sail @@ -1,143 +1,223 @@ -function one_atom () = /* comment */ -0b1 +function one_atom () = + /* comment */ + 0b1 -function one_binary_op () = // -a + 1 +function one_binary_op () = + // + a + 1 -function haveXcheri () -> bool = /* This is a necessary but not sufficient condition, but should do for now. */ -misa.X == 0b1 +function haveXcheri () -> bool = + /* This is a necessary but not sufficient condition, but should do for now. */ + misa.X == 0b1 -function one_binary_op () = // -{ - let a = 1; - 1 -} +function one_binary_op () = + // + { + let a = 1; + 1 + } -function let_in_once_without_trailing_comment () = let a = 1 in -a -function let_in_once_with_trailing_comment () = // comment -let a = 1 in -a + 1 +function let_in_once_without_trailing_comment () = + let a = 1 in + a -function shift_right_arith64(v : bits(64), shift : bits(6)) -> bits(64) = let v128 : bits(128) = sign_extend(v) in -( - (v128 >> shift))[ - 63..0] +function let_in_once_with_trailing_comment () = + // comment + let a = 1 in + a + 1 -function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = let v128 : bits(128) = sign_extend(v) in -( - (v128 >> shift))[ - 63 > 0] +function shift_right_arith64(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[63..0] -function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = let v128 : bits(128) = sign_extend(v) in -( - (v128 >> shift))[let a = 1 in -63 > 0] +function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[63 > 0] function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = let v128 : bits(128) = sign_extend(v) in (v128 >> shift)[ - if (let a = 1 in a > 1) then - let a = 1 in 63 > 0 - else ( - let a = 1 in - if a > 1 - then 1 - else let a = 1 in a) - ] + let a = 1 in + 63 > 0] function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = let v128 : bits(128) = sign_extend(v) in + let a = if + let a = 1 in + a > 1 + then + let a = 1 in + 63 > 0 + else + let a = 1 in + if a > 1 then 1 else + let a = 1 in + a in (v128 >> shift)[ - if (let a = 1 in a > 1) then - { ( let a = 1 in 63 > 0)} - else {( - let a = 1 in - if a > 1 - then 1 - else let a = 1 in a)} - ] - -function let_in_once_with_comment () = // -// 2. commend in a and = -let /**/ a = /**/ /**/ 1 in -/**/ -// -a + 1 + if + let a = 1 in + a > 1 then + let a = 1 in + 63 > 0 else + let a = 1 in + if a > 1 then 1 else + let a = 1 in + a ] + +function binary_op(v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = sign_extend(v) in + (v128 >> shift)[ + if + let a = 1 in + a > 1 then { + let a = 1 in + 63 > 0 + } else { + let a = 1 in + if a > 1 then { 1 } else { + let a = 1 in + a + } + } ] + +function let_in_once_with_comment () = + // + // 2. commend in a and = + let /**/ a = /**/ /**/ 1 in + /**/ + // + a + 1 // 3. multi line should be better? -function let_in_twice () = // -let a = 1 in -let b = 1 in -a + 1 - -function let_in_three () = // -let a = 1 in -let b = 1 in -/*let c = 1; is not valid now */ a + 1 - -function let_in_once2 () = // -let a = 1 in -a + 1 - -function atom_with_braces () = // -{ 1 } - -function exps_with_braces () = // -{ - let a = 1; +function let_in_twice () = + // + let a = 1 in + let b = 1 in + a + 1 + +function let_in_three () = + // + let a = 1 in + let b = 1 in + /*let c = 1; is not valid now */ a + 1 + +function let_in_once2 () = + // + let a = 1 in + a + 1 + +function atom_with_braces () = + // + { 1 } + + +function exps_with_braces () = + // + { + let a = 1; + a + 1 + } + + +function if_stmt () = if a > 1 then { 1 } else { 2 } + +function if_stmt () = if a > 1 then { + let a = 1 in + 1 // comment +} else { + let a = 1 in + 2 } function if_stmt () = - if a > 1 then { 1 } else { 2 } + if + let a = 1 in + if a > 1 then { 2 } else { 3 } then { 2 } else { 3 } function if_stmt () = - if a > 1 then { + if let a = 1 in - 1 // comment + if a > 1 then { + 2 // comment + } else { 3 } then { + // comment + 2 } else { + 3 + // comment + } + +function if_stmt () = + if let a = 1 in + if a > 1 then { + 2 /* comment */ + } else { 3 } then { + /* comment */ 2 + } else { + 3 + /* comment */ } -function let_with_if_stmt () = let a = 1 in -if a > 1 then { 1 } else { 2 } - -function let_with_if_stmt () = let a = 1 in -/* comment */ /* comment */ if a > 1 then { 1 } else { 2 } - -function let_with_if_stmt () = let a = 1 in -/* comment */ /* comment */ if //comment -a > 1 then { 1 } else { 2 } - -function let_with_if_stmt () = let a = 1 in -/* comment */ if a > 1 then { 1 } else { 2 } - -function let_with_if_stmt () = let a = 1 in -/* comment */ if a > 1 /* comment */ then { 1 } else { 2 } +function let_with_if_stmt () = + let a = 1 in + if a > 1 then { 1 } else { 2 } -function let_with_if_stmt () = let a = 1 in -/* comment */ if a > 1 /* comment */ then { - /* comment */ 1 -} else { 2 } +function let_with_if_stmt () = + let a = 1 in + /* comment */ + /* comment */ + if a > 1 then { 1 } else { 2 } -function let_with_if_stmt () = let a = 1 in -/* comment */ if a > 1 /* comment */ then { - /* comment */ 1 /* comment */ -} else { 2 } +function let_with_if_stmt () = + let a = 1 in + /* comment */ + /* comment */ + if + //comment + a > 1 then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 then { 1 } else { 2 } -function let_with_if_stmt () = let a = 1 in -/* comment */ if a > 1 /* comment */ then { - /* comment */ 1 /* comment */ -} else { - /* comment */ 2 -} +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ then { 1 } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ then { + /* comment */ 1 + } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ then { + /* comment */ 1 /* comment */ + } else { 2 } + +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ then { + /* comment */ 1 /* comment */ + } else { + /* comment */ 2 + } -function let_with_if_stmt () = let a = 1 in -/* comment */ if a > 1 /* comment */ then { - /* comment */ 1 /* comment */ -} else { - /* comment */ 2 -} /* comment */ +function let_with_if_stmt () = + let a = 1 in + /* comment */ + if a > 1 /* comment */ then { + /* comment */ 1 /* comment */ + } else { + /* comment */ 2 + } /* comment */