Change .ocamlformat to match aeneas

charon-ml/.ocamlformat

@@ -1,2 +1,5 @@
+break-cases = fit-or-vertical
 doc-comments = before
 exp-grouping = preserve
+parens-tuple = always
+parens-tuple-patterns = multi-line-only

charon-ml/src/Collections.ml

@@ -125,7 +125,9 @@ module List = struct
         match f hd with
         | None -> None
         | Some hd -> (
-            match mmap f tl with None -> None | Some tl -> Some (hd :: tl)))
+            match mmap f tl with
+            | None -> None
+            | Some tl -> Some (hd :: tl)))
 end
 
 module type OrderedType = sig
@@ -212,7 +214,9 @@ module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
 
   let to_string indent_opt a_to_string m =
     let indent, break =
-      match indent_opt with Some indent -> (indent, "\n") | None -> ("", " ")
+      match indent_opt with
+      | Some indent -> (indent, "\n")
+      | None -> ("", " ")
     in
     let sep = "," ^ break in
     let ls =
@@ -314,7 +318,9 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
 
   let to_string indent_opt m =
     let indent, break =
-      match indent_opt with Some indent -> (indent, "\n") | None -> ("", " ")
+      match indent_opt with
+      | Some indent -> (indent, "\n")
+      | None -> ("", " ")
     in
     let sep = "," ^ break in
     let ls = Set.fold (fun v ls -> (indent ^ Ord.to_string v) :: ls) m [] in
@@ -508,7 +514,9 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
   let find k m = Map.find k m.map
 
   let find_with_default k v m =
-    match Map.find_opt k m.map with None -> v | Some v -> v
+    match Map.find_opt k m.map with
+    | None -> v
+    | Some v -> v
 
   let find_opt k m = Map.find_opt k m.map
   let find_first k m = Map.find_first k m.map

charon-ml/src/ExpressionsUtils.ml

@@ -1,11 +1,22 @@
 open Expressions
 
 let unop_can_fail (unop : unop) : bool =
-  match unop with Neg | Cast _ -> true | Not -> false
+  match unop with
+  | Neg | Cast _ -> true
+  | Not -> false
 
 let binop_can_fail (binop : binop) : bool =
   match binop with
-  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt | CheckedAdd
-  | CheckedSub | CheckedMul ->
-      false
+  | BitXor
+  | BitAnd
+  | BitOr
+  | Eq
+  | Lt
+  | Le
+  | Ne
+  | Ge
+  | Gt
+  | CheckedAdd
+  | CheckedSub
+  | CheckedMul -> false
   | Div | Rem | Add | Sub | Mul | Shl | Shr -> true

charon-ml/src/GAstOfJson.ml

@@ -456,7 +456,9 @@ and global_decl_ref_of_json (ctx : of_json_ctx) (js : json) :
 and trait_item_name_of_json (ctx : of_json_ctx) (js : json) :
     (trait_item_name, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> string_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> string_of_json ctx x
+    | _ -> Error "")
 
 and trait_decl_of_json (ctx : of_json_ctx) (js : json) :
     (trait_decl, string) result =
@@ -618,27 +620,37 @@ and assertion_of_json (ctx : of_json_ctx) (js : json) :
 and fun_decl_id_of_json (ctx : of_json_ctx) (js : json) :
     (fun_decl_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> FunDeclId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> FunDeclId.id_of_json ctx x
+    | _ -> Error "")
 
 and type_decl_id_of_json (ctx : of_json_ctx) (js : json) :
     (type_decl_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> TypeDeclId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> TypeDeclId.id_of_json ctx x
+    | _ -> Error "")
 
 and global_decl_id_of_json (ctx : of_json_ctx) (js : json) :
     (global_decl_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> GlobalDeclId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> GlobalDeclId.id_of_json ctx x
+    | _ -> Error "")
 
 and trait_decl_id_of_json (ctx : of_json_ctx) (js : json) :
     (trait_decl_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> TraitDeclId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> TraitDeclId.id_of_json ctx x
+    | _ -> Error "")
 
 and trait_impl_id_of_json (ctx : of_json_ctx) (js : json) :
     (trait_impl_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> TraitImplId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> TraitImplId.id_of_json ctx x
+    | _ -> Error "")
 
 and any_decl_id_of_json (ctx : of_json_ctx) (js : json) :
     (any_decl_id, string) result =
@@ -663,7 +675,9 @@ and any_decl_id_of_json (ctx : of_json_ctx) (js : json) :
 
 and file_id_of_json (ctx : of_json_ctx) (js : json) : (file_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> FileId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> FileId.id_of_json ctx x
+    | _ -> Error "")
 
 and loc_of_json (ctx : of_json_ctx) (js : json) : (loc, string) result =
   combine_error_msgs js __FUNCTION__
@@ -801,7 +815,9 @@ and file_of_json (ctx : of_json_ctx) (js : json) : (file, string) result =
 and disambiguator_of_json (ctx : of_json_ctx) (js : json) :
     (disambiguator, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> Disambiguator.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> Disambiguator.id_of_json ctx x
+    | _ -> Error "")
 
 and path_elem_of_json (ctx : of_json_ctx) (js : json) :
     (path_elem, string) result =
@@ -832,27 +848,37 @@ and impl_elem_of_json (ctx : of_json_ctx) (js : json) :
 
 and name_of_json (ctx : of_json_ctx) (js : json) : (name, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> list_of_json path_elem_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> list_of_json path_elem_of_json ctx x
+    | _ -> Error "")
 
 and type_var_id_of_json (ctx : of_json_ctx) (js : json) :
     (type_var_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> TypeVarId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> TypeVarId.id_of_json ctx x
+    | _ -> Error "")
 
 and variant_id_of_json (ctx : of_json_ctx) (js : json) :
     (variant_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> VariantId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> VariantId.id_of_json ctx x
+    | _ -> Error "")
 
 and field_id_of_json (ctx : of_json_ctx) (js : json) : (field_id, string) result
     =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> FieldId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> FieldId.id_of_json ctx x
+    | _ -> Error "")
 
 and const_generic_var_id_of_json (ctx : of_json_ctx) (js : json) :
     (const_generic_var_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> ConstGenericVarId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> ConstGenericVarId.id_of_json ctx x
+    | _ -> Error "")
 
 and type_var_of_json (ctx : of_json_ctx) (js : json) : (type_var, string) result
     =
@@ -1080,12 +1106,16 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) :
 and existential_predicate_of_json (ctx : of_json_ctx) (js : json) :
     (existential_predicate, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with `Null -> Ok () | _ -> Error "")
+    (match js with
+    | `Null -> Ok ()
+    | _ -> Error "")
 
 and trait_clause_id_of_json (ctx : of_json_ctx) (js : json) :
     (trait_clause_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> TraitClauseId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> TraitClauseId.id_of_json ctx x
+    | _ -> Error "")
 
 and trait_clause_of_json (ctx : of_json_ctx) (js : json) :
     (trait_clause, string) result =
@@ -1404,7 +1434,9 @@ and fun_sig_of_json (ctx : of_json_ctx) (js : json) : (fun_sig, string) result =
 
 and var_id_of_json (ctx : of_json_ctx) (js : json) : (var_id, string) result =
   combine_error_msgs js __FUNCTION__
-    (match js with x -> VarId.id_of_json ctx x | _ -> Error "")
+    (match js with
+    | x -> VarId.id_of_json ctx x
+    | _ -> Error "")
 
 and literal_of_json (ctx : of_json_ctx) (js : json) : (literal, string) result =
   combine_error_msgs js __FUNCTION__
@@ -1579,7 +1611,9 @@ and id_to_file_of_json (js : json) : (of_json_ctx, string) result =
      let files_with_ids =
        List.filter_map
          (fun (i, file) ->
-           match file with None -> None | Some file -> Some (i, file))
+           match file with
+           | None -> None
+           | Some file -> Some (i, file))
          (List.mapi (fun i file -> (FileId.of_int i, file)) files)
      in
      Ok (FileId.Map.of_list files_with_ids))

charon-ml/src/GAstUtils.ml

@@ -42,7 +42,9 @@ let fun_body_get_input_vars (fbody : 'body gexpr_body) : var list =
   locals_get_input_vars fbody.locals
 
 let g_declaration_group_to_list (g : 'a g_declaration_group) : 'a list =
-  match g with RecGroup ids -> ids | NonRecGroup id -> [ id ]
+  match g with
+  | RecGroup ids -> ids
+  | NonRecGroup id -> [ id ]
 
 (** List all the ids in this declaration group. *)
 let declaration_group_to_list (g : declaration_group) : any_decl_id list =

charon-ml/src/Identifiers.ml

@@ -159,7 +159,9 @@ module IdGen () : Id = struct
 
   let mapi_from1 f ls =
     let rec aux i ls =
-      match ls with [] -> [] | x :: ls' -> f i x :: aux (i + 1) ls'
+      match ls with
+      | [] -> []
+      | x :: ls' -> f i x :: aux (i + 1) ls'
     in
     aux 1 ls
 

charon-ml/src/LlbcAstUtils.ml

@@ -46,8 +46,14 @@ let mk_sequence (st1 : statement) (st2 : statement) : statement =
  *)
 let rec chain_statements (st1 : statement) (st2 : statement) : statement =
   match st1.content with
-  | SetDiscriminant _ | Assert _ | Call _ | Assign _ | FakeRead _ | Drop _
-  | Loop _ | Error _ ->
+  | SetDiscriminant _
+  | Assert _
+  | Call _
+  | Assign _
+  | FakeRead _
+  | Drop _
+  | Loop _
+  | Error _ ->
       (* Simply create a sequence *)
       mk_sequence st1 st2
   | Nop -> (* Ignore the nop *) st2
@@ -91,8 +97,7 @@ let compute_fun_decl_groups_map (c : crate) : FunDeclId.Set.t FunDeclId.Map.t =
                 let idset = FunDeclId.Set.of_list ids in
                 Some (List.map (fun id -> (id, idset)) ids)
             | TypeGroup _ | GlobalGroup _ | TraitDeclGroup _ | TraitImplGroup _
-              ->
-                None
+              -> None
             | MixedGroup _ ->
                 raise
                   (Failure

charon-ml/src/MetaUtils.ml

@@ -26,4 +26,6 @@ let combine_span (m0 : span) (m1 : span) : span option =
 (** Safely combine two spans, even if they do not come from the same file -
     if this happens, we simply use the first span. *)
 let safe_combine_span (m0 : span) (m1 : span) : span =
-  match combine_span m0 m1 with None -> m0 | Some m -> m
+  match combine_span m0 m1 with
+  | None -> m0
+  | Some m -> m