From 7b606a1c77e9059da11d0543e5dfbe2a746604df Mon Sep 17 00:00:00 2001 From: trdthg Date: Sun, 28 Jul 2024 22:08:15 +0800 Subject: [PATCH] Fmt: allow Vector_update nowrap --- src/lib/chunk_ast.ml | 14 +- src/lib/format_sail.ml | 6 +- test/format/default/demo.sail | 13 +- test/format/default/function_quant.sail | 28 --- test/format/default/pat_exps.sail | 257 ------------------------ test/format/default/wrap.expect | 15 ++ test/format/wrap.sail | 20 +- 7 files changed, 61 insertions(+), 292 deletions(-) delete mode 100644 test/format/default/function_quant.sail delete mode 100644 test/format/default/pat_exps.sail diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 536bbc16e..aebb82be2 100644 --- a/src/lib/chunk_ast.ml +++ b/src/lib/chunk_ast.ml @@ -394,7 +394,11 @@ let rec prerr_chunk indent = function Queue.iter (prerr_chunk (indent ^ " ")) exp; Printf.eprintf "%s with:" indent; List.iter (fun exp -> Queue.iter (prerr_chunk (indent ^ " ")) exp) exps - | Vector_updates (_exp, _updates) -> Printf.eprintf "%sVector_updates:\n" indent + | Vector_updates (exp, updates) -> + Printf.eprintf "%sVector_updates:\n" indent; + Queue.iter (prerr_chunk (indent ^ " ")) exp; + Printf.eprintf "%s with:\n" indent; + List.iter (prerr_chunk (indent ^ " ")) updates | Index (exp, ix) -> Printf.eprintf "%sIndex:\n" indent; List.iter @@ -952,6 +956,14 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) = let i_chunks = rec_chunk_exp i in pop_comments ~spacer:false comments i_chunks keywords.then_loc; let t_chunks = rec_chunk_exp t in + if if_format.then_brace then ignore (pop_comments_until_loc_end comments t_chunks keywords.then_loc); + (* + no place to put comment between then_end and else_start + + if foo + then {} /* comment */ + else {} + *) ignore (pop_trailing_comment comments t_chunks (ending_line_num keywords.then_loc)); (match keywords.else_loc with Some l -> pop_comments comments t_chunks l | None -> ()); let e_chunks = rec_chunk_exp e in diff --git a/src/lib/format_sail.ml b/src/lib/format_sail.ml index 6df064656..1c81f1958 100644 --- a/src/lib/format_sail.ml +++ b/src/lib/format_sail.ml @@ -235,6 +235,7 @@ module PPrintWrapper = struct group (opening ^^ nest n (b ^^ contents) ^^ b ^^ 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)) @@ -485,7 +486,7 @@ let rec check_chunks_nowrap ?(opt = default_opt) cqs = else ( non_delim_count := !non_delim_count + 1; (* strict rule, for nested chunks *) - let check_no_wrap c = + let rec check_no_wrap c = match c with | Atom _ | String_literal _ -> (* Atom *) @@ -518,6 +519,9 @@ let rec check_chunks_nowrap ?(opt = default_opt) cqs = | Struct_update (exps, fexps) -> (* struct { variety = AV_exclusive } *) check_chunks_nowrap ~opt [exps] && check_chunks_nowrap ~opt fexps + | Vector_updates (cq, cs) -> + (* [foo with a = 1, b = 2] *) + check_chunks_nowrap ~opt [cq] && List.fold_left (fun res c -> res && check_no_wrap c) true cs | Tuple (_, _, _, cqs) -> (* (1, 2) *) check_chunks_nowrap ~opt cqs | _ -> false in diff --git a/test/format/default/demo.sail b/test/format/default/demo.sail index 055f38f7b..48609955f 100644 --- a/test/format/default/demo.sail +++ b/test/format/default/demo.sail @@ -1,6 +1,11 @@ +function init_pmp () -> unit = { + assert(sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64, "sys_pmp_count() must be 0, 16, or 64"); -function rX r = match r { - _ => - // - Xs[unsigned(r)], + foreach (i from 0 to 63) { + // On reset the PMP register's A and L bits are set to 0 unless the plaform + // mandates a different value. + pmpcfg_n[i] = [pmpcfg_n[i] with + A = pmpAddrMatchType_to_bits(OFF), L = 0b0 + ] + } } diff --git a/test/format/default/function_quant.sail b/test/format/default/function_quant.sail deleted file mode 100644 index 5d0e0501f..000000000 --- a/test/format/default/function_quant.sail +++ /dev/null @@ -1,28 +0,0 @@ -default Order dec - -$include - -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 = { - () -} diff --git a/test/format/default/pat_exps.sail b/test/format/default/pat_exps.sail deleted file mode 100644 index 19447d37c..000000000 --- a/test/format/default/pat_exps.sail +++ /dev/null @@ -1,257 +0,0 @@ -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/wrap.expect b/test/format/default/wrap.expect index cc0ab7454..90ef473a0 100644 --- a/test/format/default/wrap.expect +++ b/test/format/default/wrap.expect @@ -7,3 +7,18 @@ let a = if i + rs1_val < VLMAX then { 1 } else { 2 } function clause execute SINVAL_VMA(rs1, rs2) = { execute(SFENCE_VMA(rs1, rs2)) } + +function init_pmp () -> unit = { + assert(sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64, "sys_pmp_count() must be 0, 16, or 64"); + + foreach (i from 0 to 63) { + // On reset the PMP register's A and L bits are set to 0 unless the plaform + // mandates a different value. + pmpcfg_n[i] = [pmpcfg_n[i] with + A = pmpAddrMatchType_to_bits(OFF), L = 0b0 + ] + } +} + +register mtimecmp : bits(64) // memory-mapped internal clint register. +function not_implemented message = throw Error_not_implemented(message) diff --git a/test/format/wrap.sail b/test/format/wrap.sail index 96fcca9ff..7d703493c 100644 --- a/test/format/wrap.sail +++ b/test/format/wrap.sail @@ -13,4 +13,22 @@ let a = function clause execute SINVAL_VMA(rs1, rs2) = { execute(SFENCE_VMA(rs1, rs2)) -} \ No newline at end of file +} + +function init_pmp () -> unit = { + assert(sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64, "sys_pmp_count() must be 0, 16, or 64"); + + foreach (i from 0 to 63) { + // On reset the PMP register's A and L bits are set to 0 unless the plaform + // mandates a different value. + pmpcfg_n[i] = [pmpcfg_n[i] with + A = pmpAddrMatchType_to_bits(OFF), L = 0b0 + ] + } +} + +register mtimecmp : + bits(64) // memory-mapped internal clint register. + +function not_implemented message = + throw Error_not_implemented(message)