Merge pull request #1111 from hacspec/update-ocamlformat

chore(engine): ocamlformat: update: 0.24.1 -> 0.26.2
cryspen · Nov 13, 2024 · 64d1004 · 64d1004
2 parents a8acd9b + 5c148ec
commit 64d1004
Show file tree

Hide file tree

Showing 37 changed files with 342 additions and 330 deletions.
diff --git a/engine/.ocamlformat b/engine/.ocamlformat
@@ -1,2 +1,2 @@
 profile = default
-version = 0.24.1
+version = 0.26.2
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -86,10 +86,11 @@ let hardcoded_coq_headers =
 
 module BasePrinter = Generic_printer.Make (InputLanguage)
 
-module Make (Default : sig
-  val default : string -> string
-end)
-(Attrs : Attrs.WITH_ITEMS) =
+module Make
+    (Default : sig
+      val default : string -> string
+    end)
+    (Attrs : Attrs.WITH_ITEMS) =
 struct
   open PPrint
 
@@ -648,10 +649,10 @@ struct
 
       method trait_item'_TIDefault ~params ~body ~witness:_ =
         (if List.is_empty params then empty
-        else
-          string "fun" ^^ space
-          ^^ separate_map space (fun x -> x#p) params
-          ^^ space ^^ string "=>")
+         else
+           string "fun" ^^ space
+           ^^ separate_map space (fun x -> x#p) params
+           ^^ space ^^ string "=>")
         ^^ nest 2 (break 1 ^^ body#p)
 
       method trait_item'_TIFn x1 = x1#p

diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml
@@ -578,10 +578,10 @@ functor
                       Some
                         ("let" ^ " " ^ name ^ " " ^ ":=" ^ " "
                         ^ (if List.is_empty arguments then ""
-                          else
-                            "fun" ^ " "
-                            ^ params_to_string_typed arguments
-                            ^ " " ^ "=>" ^ " ")
+                           else
+                             "fun" ^ " "
+                             ^ params_to_string_typed arguments
+                             ^ " " ^ "=>" ^ " ")
                         ^ term_to_string_without_paren term 1
                         ^ " " ^ ":" ^ " "
                         ^ ty_to_string_without_paren ty
@@ -601,10 +601,10 @@ functor
                    | InlineDef (name, arguments, term, ty) ->
                        name ^ " " ^ ":=" ^ " " ^ "("
                        ^ (if List.is_empty arguments then ""
-                         else
-                           "fun" ^ " "
-                           ^ params_to_string_typed arguments
-                           ^ " " ^ "=>" ^ " ")
+                          else
+                            "fun" ^ " "
+                            ^ params_to_string_typed arguments
+                            ^ " " ^ "=>" ^ " ")
                        ^ term_to_string_without_paren term 1
                        ^ " " ^ ":" ^ " "
                        ^ ty_to_string_without_paren ty

diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -334,7 +334,7 @@ module SSPExtraDefinitions (* : ANALYSIS *) = struct
                                             ~f:(fun x y ->
                                               SSP.AST.App (SSP.AST.Var x, [ y ]))
                                             ((if Stdlib.(i != 0) then [ "snd" ]
-                                             else [])
+                                              else [])
                                             @ List.init
                                                 (List.length fields - 1 - i)
                                                 ~f:(fun _ -> "fst")),
@@ -437,9 +437,9 @@ module SSPExtraDefinitions (* : ANALYSIS *) = struct
                             [
                               SSP.AST.Value
                                 ( (if Stdlib.(j == i) then SSP.AST.Var "y"
-                                  else
-                                    SSP.AST.App
-                                      (SSP.AST.Var x, [ SSP.AST.Var "x" ])),
+                                   else
+                                     SSP.AST.App
+                                       (SSP.AST.Var x, [ SSP.AST.Var "x" ])),
                                   false,
                                   0 );
                             ] ))
@@ -534,12 +534,12 @@ end
 
 module StaticAnalysis (* : ANALYSIS *) = struct
   module FunctionDependency (* : ANALYSIS *) =
-  [%functor_application
-  Analyses.Function_dependency InputLanguage]
+    [%functor_application
+    Analyses.Function_dependency InputLanguage]
 
   module MutableVariables (* : ANALYSIS *) =
-  [%functor_application
-  Analyses.Mutable_variables InputLanguage]
+    [%functor_application
+    Analyses.Mutable_variables InputLanguage]
 
   type analysis_data = { mut_var : MutableVariables.analysis_data }
 
@@ -1470,16 +1470,16 @@ struct
           let g = pgeneric span generics in
           [
             (if List.is_empty g then
-             SSP.AST.Notation
-               ( "'" ^ pconcrete_ident name ^ "'",
-                 SSP.AST.Type (pty span ty),
-                 None )
-            else
-              SSP.AST.Definition
-                ( pconcrete_ident name,
-                  g,
-                  SSP.AST.Type (pty span ty),
-                  SSP.AST.TypeTy ));
+               SSP.AST.Notation
+                 ( "'" ^ pconcrete_ident name ^ "'",
+                   SSP.AST.Type (pty span ty),
+                   None )
+             else
+               SSP.AST.Definition
+                 ( pconcrete_ident name,
+                   g,
+                   SSP.AST.Type (pty span ty),
+                   SSP.AST.TypeTy ));
           ]
       (* record *)
       | Type
@@ -1741,11 +1741,11 @@ struct
                             (if include_extra_loc then [ loc_name ] else [])
                         in
                         (if include_extra_loc then
-                         [
-                           SSP.AST.Named
-                             (loc_name, SSP.AST.NameTy "{fset Location}");
-                         ]
-                        else [])
+                           [
+                             SSP.AST.Named
+                               (loc_name, SSP.AST.NameTy "{fset Location}");
+                           ]
+                         else [])
                         @ [
                             SSP.AST.Named
                               ( pconcrete_ident x.ti_ident,

diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml
@@ -348,12 +348,12 @@ let translate _ (bo : BackendOptions.t) ~(bundles : AST.item list list)
 open Phase_utils
 
 module TransformToInputLanguage =
-[%functor_application
-Phases.Reject.RawOrMutPointer Features.Rust |> Phases.Reject.Unsafe
-|> Phases.And_mut_defsite |> Phases.Reconstruct_asserts
-|> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks
-|> Phases.Reject.Continue |> Phases.Drop_references |> Phases.Bundle_cycles
-|> RejectNotEC]
+  [%functor_application
+  Phases.Reject.RawOrMutPointer Features.Rust |> Phases.Reject.Unsafe
+  |> Phases.And_mut_defsite |> Phases.Reconstruct_asserts
+  |> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks
+  |> Phases.Reject.Continue |> Phases.Drop_references |> Phases.Bundle_cycles
+  |> RejectNotEC]
 
 let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) :
     AST.item list =

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -104,7 +104,8 @@ let module_name (ns : string * string list) : string =
     (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns))
 
 module Make
-    (Attrs : Attrs.WITH_ITEMS) (Ctx : sig
+    (Attrs : Attrs.WITH_ITEMS)
+    (Ctx : sig
       val ctx : Context.t
     end) =
 struct
@@ -1174,11 +1175,9 @@ struct
                     (* in *)
                     (F.id name, None, [], t)
                     :: List.map
-                         ~f:
-                           (fun {
-                                  goal = { trait; args };
-                                  name = impl_ident_name;
-                                } ->
+                         ~f:(fun
+                             { goal = { trait; args }; name = impl_ident_name }
+                           ->
                            let base =
                              F.term @@ F.AST.Name (pconcrete_ident trait)
                            in

diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
@@ -38,14 +38,14 @@ module SubtypeToInputLanguage
              and type macro = Features.On.macro
              and type quote = Features.On.quote
              and type construct_base = Features.On.construct_base
-    (* and type as_pattern = Features.Off.as_pattern *)
-    (* and type nontrivial_lhs = Features.Off.nontrivial_lhs *)
-    (* and type arbitrary_lhs = Features.Off.arbitrary_lhs *)
-    (* and type lifetime = Features.Off.lifetime *)
-    (* and type construct_base = Features.Off.construct_base *)
-    (* and type monadic_action = Features.Off.monadic_action *)
-    (* and type monadic_binding = Features.Off.monadic_binding *)
-    (* and type block = Features.Off.block *)) =
+(* and type as_pattern = Features.Off.as_pattern *)
+(* and type nontrivial_lhs = Features.Off.nontrivial_lhs *)
+(* and type arbitrary_lhs = Features.Off.arbitrary_lhs *)
+(* and type lifetime = Features.Off.lifetime *)
+(* and type construct_base = Features.Off.construct_base *)
+(* and type monadic_action = Features.Off.monadic_action *)
+(* and type monadic_binding = Features.Off.monadic_binding *)
+(* and type block = Features.Off.block *)) =
 struct
   module FB = InputLanguage
 

diff --git a/engine/lib/analyses/mutable_variables.ml b/engine/lib/analyses/mutable_variables.ml
@@ -39,11 +39,10 @@ module%inlined_contents Make (F : Features.T) = struct
     include W
     include Set.M (W)
 
-    class type ['s] monoid =
-      object
-        method zero : 's
-        method plus : 's -> 's -> 's
-      end
+    class type ['s] monoid = object
+      method zero : 's
+      method plus : 's -> 's -> 's
+    end
 
     class ['s, 't] prod_monoid (fst : 's monoid)
       (snd : 't monoid) (* : ['s * 't] monoid *) =
@@ -153,8 +152,8 @@ module%inlined_contents Make (F : Features.T) = struct
   end
 
   let rec analyse (func_dep : pre_data) (items : A.item list) : analysis_data =
-    let (mut_var_list, _)
-          : (concrete_ident * (U.TypedLocalIdent.t * id_order) list) list * _ =
+    let (mut_var_list, _) :
+        (concrete_ident * (U.TypedLocalIdent.t * id_order) list) list * _ =
       List.fold_left ~init:([], 0)
         ~f:(fun (y, count) (name, body) ->
           let items, count = analyse_function_body body count in