Update ocamlformat and format code

formalsec · Dec 4, 2024 · 542f203 · 542f203
1 parent df5f3fd
commit 542f203
Show file tree

Hide file tree

Showing 9 changed files with 50 additions and 52 deletions.
diff --git a/.ocamlformat b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.26.2
+version=0.27.0
 assignment-operator=end-line
 break-cases=fit
 break-fun-decl=wrap

diff --git a/bench/runner/multi_query.ml b/bench/runner/multi_query.ml
@@ -42,8 +42,7 @@ let make_data_frames results =
       let provers, benchmark, rtime =
         List.fold_left
           (fun (prover_acc, bench_acc, rtime_acc) (prover, benchmark, rtime) ->
-            (prover :: prover_acc, benchmark :: bench_acc, rtime :: rtime_acc)
-            )
+            (prover :: prover_acc, benchmark :: bench_acc, rtime :: rtime_acc) )
           ([], [], []) prover_results
       in
       let df =

diff --git a/bench/runner/single_query.ml b/bench/runner/single_query.ml
@@ -36,7 +36,7 @@ let summarize results =
         ( prover
         , List.fold_left
             (fun (total, sat, unsat, unknown, time)
-               (_, _, stdout, _, rtime, _rusage) ->
+                 (_, _, stdout, _, rtime, _rusage) ->
               let sat, unsat, unknown =
                 match parse_status stdout with
                 | `Sat -> (succ sat, unsat, unknown)
@@ -50,7 +50,7 @@ let summarize results =
   let solver, total, sat, unsat, unknwon, rtime =
     List.fold_left
       (fun (solver, total, sat, unsat, unknown, rtime)
-         (prover, (p_total, p_sat, p_unsat, p_unknown, p_rtime)) ->
+           (prover, (p_total, p_sat, p_unsat, p_unknown, p_rtime)) ->
         ( Tool.prover_to_string prover :: solver
         , p_total :: total
         , p_sat :: sat
@@ -84,7 +84,8 @@ let make_data_frames results =
                , rtime_acc
                , utime_acc
                , stime_acc
-               , maxrss_acc ) (_status, benchmark, stdout, stderr, rtime, rusage) ->
+               , maxrss_acc )
+               (_status, benchmark, stdout, stderr, rtime, rusage) ->
             ( Tool.prover_to_string prover :: prover_acc
             , Fmt.str "%a" Fpath.pp benchmark :: bench_acc
             , Fmt.str "%a" pp_status (parse_status stdout) :: res_acc

diff --git a/bench/runner/tool.ml b/bench/runner/tool.ml
@@ -77,11 +77,11 @@ let fork_and_run ?timeout ?from_file prover file =
   let prog, argv = cmd ?from_file prover file in
   let pid =
     Unix.fork_exec ~prog ~argv () ~preexec_fn:(fun () ->
-        Unix.close stdout_read;
-        Unix.close stderr_read;
-        dup2 ~src:stdout_write ~dst:Unix.stdout;
-        dup2 ~src:stderr_write ~dst:Unix.stderr;
-        Option.iter limit_cpu timeout )
+      Unix.close stdout_read;
+      Unix.close stderr_read;
+      dup2 ~src:stdout_write ~dst:Unix.stdout;
+      dup2 ~src:stderr_write ~dst:Unix.stderr;
+      Option.iter limit_cpu timeout )
   in
   Unix.close stdout_write;
   Unix.close stderr_write;

diff --git a/bin/main.ml b/bin/main.ml
@@ -38,8 +38,7 @@ let parse_file filename =
       (fun acc line ->
         let line = String.trim line in
         (* Assume '#' at the start of a line is a comment *)
-        if String.starts_with ~prefix:"#" line then acc else Fpath.v line :: acc
-        )
+        if String.starts_with ~prefix:"#" line then acc else Fpath.v line :: acc )
       [] lines
   in
   List.rev files
@@ -58,10 +57,10 @@ let run debug solver prover_mode dry print_statistics from_file files =
     incr total_tests;
     let start_t = Unix.gettimeofday () in
     Fun.protect ~finally:(fun () ->
-        if print_statistics then (
-          let exec_t = Unix.gettimeofday () -. start_t in
-          total_t := !total_t +. exec_t;
-          Log.app (fun m -> m "Run %a in %.06f" Fpath.pp file exec_t) ) )
+      if print_statistics then (
+        let exec_t = Unix.gettimeofday () -. start_t in
+        total_t := !total_t +. exec_t;
+        Log.app (fun m -> m "Run %a in %.06f" Fpath.pp file exec_t) ) )
     @@ fun () ->
     let ast =
       try Ok (Compile.until_rewrite file)

diff --git a/src/colibri2_mappings.default.ml b/src/colibri2_mappings.default.ml
@@ -92,26 +92,24 @@ module Fresh = struct
              (fun a -> DExpr.Term.apply_cst f [ a.DExpr.term_ty ] [ a ]) )
       in
       Colibri2_core.Expr.add_builtins (fun env s ->
-          match s with
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToInt" } ->
-            term_app1 env s string_to_int
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "RealToString" }
-            ->
-            term_app1 env s real_to_string
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToReal" }
-            ->
-            term_app1 env s string_to_real
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "TrimString" } ->
-            term_app1 env s trim_string
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "F32ToString" } ->
-            term_app1 env s f32_to_string
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToF32" } ->
-            term_app1 env s string_to_f32
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "F64ToString" } ->
-            term_app1 env s f64_to_string
-          | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToF64" } ->
-            term_app1 env s string_to_f64
-          | _ -> `Not_found )
+        match s with
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToInt" } ->
+          term_app1 env s string_to_int
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "RealToString" } ->
+          term_app1 env s real_to_string
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToReal" } ->
+          term_app1 env s string_to_real
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "TrimString" } ->
+          term_app1 env s trim_string
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "F32ToString" } ->
+          term_app1 env s f32_to_string
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToF32" } ->
+          term_app1 env s string_to_f32
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "F64ToString" } ->
+          term_app1 env s f64_to_string
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToF64" } ->
+          term_app1 env s string_to_f64
+        | _ -> `Not_found )
 
     let satisfiability s = function
       | `Sat d ->
@@ -188,13 +186,13 @@ module Fresh = struct
 
       let add s es =
         Scheduler.add_assertion s.scheduler (fun d ->
-            let es' =
-              List.map
-                (encode_expr ~record_sym:(fun c ->
-                     s.decls <- ConstSet.add c s.decls ) )
-                es
-            in
-            List.iter (fun e -> new_assertion d e) es' )
+          let es' =
+            List.map
+              (encode_expr ~record_sym:(fun c ->
+                 s.decls <- ConstSet.add c s.decls ) )
+              es
+          in
+          List.iter (fun e -> new_assertion d e) es' )
 
       let check s ~assumptions =
         match assumptions with

diff --git a/src/smtml_prelude.ml b/src/smtml_prelude.ml
@@ -31,9 +31,9 @@ module Result = struct
       | [] -> k (Ok [])
       | hd :: tl ->
         list_map_cps f tl (fun rest ->
-            let* rest in
-            let* hd' = f hd in
-            k (Ok (hd' :: rest)) )
+          let* rest in
+          let* hd' = f hd in
+          k (Ok (hd' :: rest)) )
     in
     list_map_cps f v Fun.id
 
@@ -43,9 +43,9 @@ module Result = struct
       | [] -> k (Ok [])
       | hd :: tl ->
         list_filter_map_cps f tl (fun rest ->
-            let* rest in
-            let* v = f hd in
-            k (Ok (match v with None -> rest | Some v -> v :: rest)) )
+          let* rest in
+          let* v = f hd in
+          k (Ok (match v with None -> rest | Some v -> v :: rest)) )
     in
     list_filter_map_cps f v Fun.id
 end
diff --git a/src/solvers/solver_intf.ml b/src/solvers/solver_intf.ml
@@ -103,7 +103,8 @@ module type Intf = sig
 
   (** {1 Incremental Model}
 
-      (Experimental) Like the Batch mode described above, but queries are cached *)
+      (Experimental) Like the Batch mode described above, but queries are cached
+  *)
   module Cached (_ : Mappings_intf.S) : sig
     include S
 

diff --git a/test/solver/test_optimizer.ml b/test/solver/test_optimizer.ml
@@ -10,6 +10,6 @@ module Make (M : Mappings_intf.S) = struct
     let x = symbol "x" Ty_int in
     Optimizer.add opt Int.[ x >= int 0; x < int 5 ];
     Optimizer.protect opt (fun () ->
-        assert (Stdlib.(Some (Value.Int 0) = Optimizer.minimize opt x)) );
+      assert (Stdlib.(Some (Value.Int 0) = Optimizer.minimize opt x)) );
     assert (Stdlib.(Some (Value.Int 4) = Optimizer.maximize opt x))
 end