Skip to content

Commit

Permalink
[fmt] run dune fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
HadrienRenaud committed Mar 21, 2024
1 parent 76a37b6 commit 6b97140
Show file tree
Hide file tree
Showing 32 changed files with 836 additions and 460 deletions.
1 change: 1 addition & 0 deletions .ocamlformat
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
version = 0.26.1
13 changes: 4 additions & 9 deletions asllib/Interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -208,8 +208,7 @@ module Make (B : Backend.S) (C : Config) = struct
in
let fold = function
| TopoSort.ASTFold.Single d -> process_one_decl d
| TopoSort.ASTFold.Recursive ds ->
List.fold_right process_one_decl ds
| TopoSort.ASTFold.Recursive ds -> List.fold_right process_one_decl ds
in
fun ast -> TopoSort.ASTFold.fold fold ast

Expand Down Expand Up @@ -841,8 +840,7 @@ module Make (B : Backend.S) (C : Config) = struct
List.fold_left2 folder (return_normal env) ldis liv
|: SemanticsRule.LDTuple
(* End *)
| LDI_Var _, None
| LDI_Tuple _, None ->
| LDI_Var _, None | LDI_Tuple _, None ->
(* Should not happen in V1 because of TypingRule.LDUninitialisedTuple *)
fatal_from s Error.TypeInferenceNeeded

Expand Down Expand Up @@ -991,17 +989,14 @@ module Make (B : Backend.S) (C : Config) = struct
let () =
if debug then
let open Format in
let pp_value fmt v =
B.debug_value v |> pp_print_string fmt
in
let pp_value fmt v = B.debug_value v |> pp_print_string fmt in
eprintf "@[@<2>%a:@ @[%a@]@ ->@ %a@]@." PP.pp_pos s
(pp_print_list ~pp_sep:pp_print_space PP.pp_expr)
args
(pp_print_list ~pp_sep:pp_print_space pp_value)
vs
else (
List.map B.debug_value vs
|> String.concat " " |> print_string;
List.map B.debug_value vs |> String.concat " " |> print_string;
print_newline ())
in
return_continue env |: SemanticsRule.SDebug
Expand Down
22 changes: 7 additions & 15 deletions asllib/Typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ let rename_ty_eqs : (AST.identifier * AST.expr) list -> AST.ty -> AST.ty =
T_Int (WellConstrained constraints) |> add_pos_from_st ty
| _ -> ty

(* Begin Lit *)
(* Begin Lit *)
let annotate_literal = function
| L_Int _ as v -> integer_exact' (literal v)
| L_Bool _ -> T_Bool
Expand Down Expand Up @@ -1804,11 +1804,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
(S_Try (s'', catchers', otherwise') |> here, env) |: TypingRule.STry
(* End *)
| S_Print { args; debug } ->
let args' =
List.map (fun e -> annotate_expr env e |> snd) args
in
(S_Print { args = args'; debug } |> here, env)
|: TypingRule.SDebug
let args' = List.map (fun e -> annotate_expr env e |> snd) args in
(S_Print { args = args'; debug } |> here, env) |: TypingRule.SDebug

and annotate_catcher env (name_opt, ty, stmt) =
let+ () = check_structure_exception ty env ty in
Expand Down Expand Up @@ -2019,8 +2016,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
else add_global_storage name ty keyword env

let declare_const loc name t v env =
add_global_storage loc name GDK_Constant env t
|> add_global_constant name v
add_global_storage loc name GDK_Constant env t |> add_global_constant name v

let rec check_is_valid_bitfield loc env width bitfield () =
let slices = bitfield_get_slices bitfield in
Expand Down Expand Up @@ -2182,8 +2178,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
(* Shouldn't happen because of parser construction. *)
Error.fatal_from loc
(Error.NotYetImplemented
"Global storage declaration must have an initial value or \
a type.")
"Global storage declaration must have an initial value or a type.")
(* End *)

let rename_primitive loc env (f : AST.func) =
Expand Down Expand Up @@ -2244,8 +2239,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
match d.desc with
| D_Func ({ body = SB_ASL _; name; _ } as f) ->
let () =
if false then
Format.eprintf "@[Analysing decl %s.@]@." name
if false then Format.eprintf "@[Analysing decl %s.@]@." name
in
D_Func (try_annotate_subprogram d env f) |> add_pos_from d
| D_Func ({ body = SB_Primitive; _ } as f) ->
Expand All @@ -2261,9 +2255,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
| TopoSort.ASTFold.Single d -> type_check_decl d
| TopoSort.ASTFold.Recursive ds -> type_check_mutually_rec ds
in
let fold_topo ast acc =
TopoSort.ASTFold.fold fold ast acc
in
let fold_topo ast acc = TopoSort.ASTFold.fold fold ast acc in
fun ast env ->
let ast_rev, env = fold_topo ast ([], env) in
(List.rev ast_rev, env)
Expand Down
100 changes: 47 additions & 53 deletions asllib/bitvector.ml
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,7 @@ let _pp_data f (length, data) =
pp_print_char f 'x';
String.iter (fun c -> fprintf f "%x" @@ Char.code c) data

let create_data_bytes length =
Bytes.create ((length + 7)/8)
let create_data_bytes length = Bytes.create ((length + 7) / 8)

(** [String.for_all] taken directly out of stdlib version 4.13 . *)
let string_for_all p s =
Expand Down Expand Up @@ -260,8 +259,7 @@ let z64 = Z.shift_left Z.one 64

let printable bv =
let z = to_z_signed bv in
if Z.geq z z63 then Z.sub z z64
else z
if Z.geq z z63 then Z.sub z z64 else z

let of_string s =
let result = Buffer.create ((String.length s / 8) + 1) in
Expand Down Expand Up @@ -434,47 +432,44 @@ let write_slice (length_dst, data_dst) (length_src, data_src) positions =
let () = List.iteri copy_bit_here positions in
remask (length_dst, Bytes.unsafe_to_string result)


(* Retuns length of destination *)
let pp (l,bs) =
Printf.sprintf "%s<%d>"
(to_string (l,Bytes.to_string bs)) l
let pp (l, bs) = Printf.sprintf "%s<%d>" (to_string (l, Bytes.to_string bs)) l

let pp_bytes n dst =
let sz = (n+1)*8 in
pp (sz,dst)
let sz = (n + 1) * 8 in
pp (sz, dst)

(* [mix_chars_start off low_c high_c] return a char,
whose off lower order bits are from low_c and
the 8-off higher order bits are the 8-off lower
order bits of high_c *)
let mix_chars_start off low_c high_c =
let low_bits = (1 lsl off-1) land (Char.code low_c)
and high_bits = (Char.code high_c) lsl off in
low_bits lor high_bits |> (land) 0xff |> Char.chr
let low_bits = ((1 lsl off) - 1) land Char.code low_c
and high_bits = Char.code high_c lsl off in
low_bits lor high_bits |> ( land ) 0xff |> Char.chr

(* [mix_chars_body off low_c high_c] return a char,
whose off lower order bits are the off higher
order bits of low_c and the 8-off higher order bits are the
8-off lower order bits of high_c *)
let mix_chars_body off low_c high_c =
let low_bits = (Char.code low_c) lsr (8-off)
and high_bits = (Char.code high_c) lsl off in
low_bits lor high_bits |> (land) 0xff |> Char.chr
let low_bits = Char.code low_c lsr (8 - off)
and high_bits = Char.code high_c lsl off in
low_bits lor high_bits |> ( land ) 0xff |> Char.chr

(* [mix_chars_final off c] return a char,
whose sz lower order bits are the
sz bits of c at possition off. *)
let mix_char_final off sz c =
(Char.code c lsr off) land (1 lsl sz-1) |> Char.chr
(Char.code c lsr off) land ((1 lsl sz) - 1) |> Char.chr

let copy_into dst (length_src, data_src as b) offset =
let copy_into dst ((length_src, data_src) as b) offset =
let () =
if false then
Printf.eprintf "copy_into %s + %s, offset=%d\n%!"
(to_string b)
(pp (offset,dst))
offset in
Printf.eprintf "copy_into %s + %s, offset=%d\n%!" (to_string b)
(pp (offset, dst))
offset
in
let length_dst = offset + length_src in
if length_src <= 0 then length_dst
else
Expand All @@ -489,11 +484,10 @@ let copy_into dst (length_src, data_src as b) offset =
* copied into the 8-m_off high order_bits of
* dst.[n_off] *)
let prec_c = Bytes.get dst n_off and next_c = String.get data_src 0 in
mix_chars_start m_off prec_c next_c |> Bytes.set dst n_off ;
mix_chars_start m_off prec_c next_c |> Bytes.set dst n_off;
let () =
if false then
Printf.eprintf "Start: %s\n%!"
(pp_bytes n_off dst) in
if false then Printf.eprintf "Start: %s\n%!" (pp_bytes n_off dst)
in
(*
* Now, loop.
* At each step, 8-off bits are taken from
Expand All @@ -502,43 +496,43 @@ let copy_into dst (length_src, data_src as b) offset =
* lower order bits of the next_char
*)
(* Number of bits still to write *)
let rem_bits = length_src - (8-m_off) in
let rem_bits = length_src - (8 - m_off) in
(* Useful string length *)
let src_str_len = (length_src+7) / 8 in
let rec do_rec i_src i_dst rem_bits =
if i_src+1 >= src_str_len then
i_src,i_dst,rem_bits
else begin
let src_str_len = (length_src + 7) / 8 in
let rec do_rec i_src i_dst rem_bits =
if i_src + 1 >= src_str_len then (i_src, i_dst, rem_bits)
else
let prec_c = String.get data_src i_src in
let next_c = String.get data_src (i_src + 1) in
mix_chars_body (m_off) prec_c next_c |> Bytes.set dst i_dst;
mix_chars_body m_off prec_c next_c |> Bytes.set dst i_dst;
let () =
if false then
Printf.eprintf "Body -> %s\n%!" (pp_bytes i_dst dst) in
do_rec (i_src+1) (i_dst+1) (rem_bits-8)
end in
let i_src,i_dst,rem_bits = do_rec 0 (n_off+1) rem_bits in
let () =
if false then
Printf.eprintf "i_src=%d, i_dst=%d, rem_bits=%d\n%!"
i_src i_dst rem_bits in
if rem_bits > 0 then begin
let c = String.get data_src i_src in
mix_char_final (8-m_off) rem_bits c |> Bytes.set dst i_dst
end in
Printf.eprintf "Body -> %s\n%!" (pp_bytes i_dst dst)
in
do_rec (i_src + 1) (i_dst + 1) (rem_bits - 8)
in
let i_src, i_dst, rem_bits = do_rec 0 (n_off + 1) rem_bits in
let () =
if false then
Printf.eprintf "i_src=%d, i_dst=%d, rem_bits=%d\n%!" i_src i_dst
rem_bits
in
if rem_bits > 0 then
let c = String.get data_src i_src in
mix_char_final (8 - m_off) rem_bits c |> Bytes.set dst i_dst
in
let () =
if false then
Printf.eprintf "copy_into %s + %s ->%s\n%!"
(to_string b)
(pp (offset,dst))
(pp (length_dst, dst)) in
Printf.eprintf "copy_into %s + %s ->%s\n%!" (to_string b)
(pp (offset, dst))
(pp (length_dst, dst))
in
length_dst

let concat bvs =
if false then begin
let pp = List.map to_string bvs in
Printf.eprintf "Concat %s\n%!" (String.concat "," pp)
end ;
(if false then
let pp = List.map to_string bvs in
Printf.eprintf "Concat %s\n%!" (String.concat "," pp));
let length = List.fold_left (fun acc bv -> acc + length bv) 0 bvs in
let result = create_data_bytes length in
let _ = List.fold_right (copy_into result) bvs 0 in
Expand Down
28 changes: 18 additions & 10 deletions asllib/dune
Original file line number Diff line number Diff line change
@@ -1,19 +1,28 @@
(rule (copy ../Version.ml Version.ml))
(rule
(copy ../Version.ml Version.ml))

(ocamllex Lexer)

(ocamllex SimpleLexer0)

(ocamllex splitasl)

(menhir (modules Parser))
(menhir (modules Parser0) (flags --unused-tokens --table))
(menhir
(modules Parser))

(menhir
(modules Parser0)
(flags --unused-tokens --table))

(library
(name asllib)
(modules (:standard \ aslref bundler))
(modules
(:standard \ aslref bundler))
(public_name herdtools7.asllib)
(private_modules Parser0 Gparser0 Lexer0 SimpleLexer0 RepeatableLexer)
(modules_without_implementation Backend AST)
(flags (:standard -w -40-42))
(flags
(:standard -w -40-42))
(libraries menhirLib zarith))

(documentation)
Expand All @@ -25,8 +34,7 @@
(modules aslref))

(executable
(public_name aslbundler)
(name bundler)
(libraries asllib)
(modules bundler))

(public_name aslbundler)
(name bundler)
(libraries asllib)
(modules bundler))
61 changes: 35 additions & 26 deletions asllib/tests/dune
Original file line number Diff line number Diff line change
@@ -1,35 +1,44 @@
(library
(name test_helpers)
(modules Helpers)
(libraries asllib))
(name test_helpers)
(modules Helpers)
(libraries asllib))

(test
(name asltests)
(modes native)
(modules asltests)
(libraries asllib test_helpers)
(deps (glob_files asl/required/*.asl) asltests.ml ../libdir/stdlib.asl)
(action
(setenv ASL_LIBDIR %{project_root}/asllib/libdir/
(run %{test} asl/required))))
(name asltests)
(modes native)
(modules asltests)
(libraries asllib test_helpers)
(deps
(glob_files asl/required/*.asl)
asltests.ml
../libdir/stdlib.asl)
(action
(setenv
ASL_LIBDIR
%{project_root}/asllib/libdir/
(run %{test} asl/required))))

(test
(name toposort)
(modes native)
(enabled_if %{lib-available:qcheck})
(libraries asllib qcheck)
(modules toposort))
(name toposort)
(modes native)
(enabled_if %{lib-available:qcheck})
(libraries asllib qcheck)
(modules toposort))

(tests
(names static bitvector types)
(modules static bitvector types)
(modes native)
(deps (:standard ../libdir/stdlib.asl))
(libraries asllib test_helpers zarith)
(flags (:standard -w -40-42))
(action
(setenv ASL_LIBDIR %{project_root}/asllib/libdir/
(run %{test} -e))))
(names static bitvector types)
(modules static bitvector types)
(modes native)
(deps
(:standard ../libdir/stdlib.asl))
(libraries asllib test_helpers zarith)
(flags
(:standard -w -40-42))
(action
(setenv
ASL_LIBDIR
%{project_root}/asllib/libdir/
(run %{test} -e))))

(cram
(deps %{bin:aslref}))
(deps %{bin:aslref}))
Loading

0 comments on commit 6b97140

Please sign in to comment.