Reformat the code

AeneasVerif · Sep 9, 2024 · 53a07ee · 53a07ee
1 parent c95a328
commit 53a07ee
Show file tree

Hide file tree

Showing 2 changed files with 65 additions and 56 deletions.
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
@@ -2661,57 +2661,64 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     + List.length decl.generics.trait_clauses
   in
   let params = Collections.List.repeat num_prefix_params Implicit in
-  (
-    (* The constructor *)
-    let cons_name =
-      ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx
-    in
-    extract_coq_arguments_instruction ctx fmt cons_name params;
-    (* Add the record itself as a parameter for the projectors *)
-    let params = params @ [Explicit] in
-    (* The constants *)
-    List.iter
-      (fun (name, _) ->
-        let item_name =
-          ctx_get_trait_const decl.item_meta.span decl.def_id name ctx
-        in
-        extract_coq_arguments_instruction ctx fmt item_name params)
-      decl.consts;
-    (* The types *)
-    List.iter
-      (fun name ->
-        (* The type *)
-        let item_name =
-          ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
-        in
-        extract_coq_arguments_instruction ctx fmt item_name params)
-      decl.types;
-    (* The parent clauses *)
-    List.iter
-      (fun clause ->
-        let item_name =
-          ctx_get_trait_parent_clause decl.item_meta.span decl.def_id
-            clause.clause_id ctx
-        in
-        extract_coq_arguments_instruction ctx fmt item_name params)
-      decl.parent_clauses;
-    (* The required methods *)
-    List.iter
-      (fun (item_name, id) ->
-        (* Lookup the definition to retrieve the information about the explicit/implicit parameters *)
-        let trans = A.FunDeclId.Map.find id ctx.trans_funs in
-        let f = trans.f in
-        let explicit_info = explicit_info_drop_prefix decl.generics f.signature.explicit_info
-        in
-        let params = params @ List.concat [explicit_info.explicit_types; explicit_info.explicit_const_generics] in
-        (* Extract *)
-        let item_name =
-          ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
-        in
-        extract_coq_arguments_instruction ctx fmt item_name params)
-      decl.required_methods;
-    (* Add a space *)
-    F.pp_print_space fmt ())
+  (* The constructor *)
+  let cons_name =
+    ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx
+  in
+  extract_coq_arguments_instruction ctx fmt cons_name params;
+  (* Add the record itself as a parameter for the projectors *)
+  let params = params @ [ Explicit ] in
+  (* The constants *)
+  List.iter
+    (fun (name, _) ->
+      let item_name =
+        ctx_get_trait_const decl.item_meta.span decl.def_id name ctx
+      in
+      extract_coq_arguments_instruction ctx fmt item_name params)
+    decl.consts;
+  (* The types *)
+  List.iter
+    (fun name ->
+      (* The type *)
+      let item_name =
+        ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
+      in
+      extract_coq_arguments_instruction ctx fmt item_name params)
+    decl.types;
+  (* The parent clauses *)
+  List.iter
+    (fun clause ->
+      let item_name =
+        ctx_get_trait_parent_clause decl.item_meta.span decl.def_id
+          clause.clause_id ctx
+      in
+      extract_coq_arguments_instruction ctx fmt item_name params)
+    decl.parent_clauses;
+  (* The required methods *)
+  List.iter
+    (fun (item_name, id) ->
+      (* Lookup the definition to retrieve the information about the explicit/implicit parameters *)
+      let trans = A.FunDeclId.Map.find id ctx.trans_funs in
+      let f = trans.f in
+      let explicit_info =
+        explicit_info_drop_prefix decl.generics f.signature.explicit_info
+      in
+      let params =
+        params
+        @ List.concat
+            [
+              explicit_info.explicit_types;
+              explicit_info.explicit_const_generics;
+            ]
+      in
+      (* Extract *)
+      let item_name =
+        ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
+      in
+      extract_coq_arguments_instruction ctx fmt item_name params)
+    decl.required_methods;
+  (* Add a space *)
+  F.pp_print_space fmt ()
 
 (** See {!extract_trait_decl_coq_arguments} *)
 let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
@@ -1706,10 +1706,12 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_space fmt ();
   F.pp_print_string fmt cons_name;
   (* Print the type/const params and the trait clauses (`{T}`) *)
-  List.iter (fun e ->
-    F.pp_print_space fmt ();
-    if e = Implicit then F.pp_print_string fmt "{ _ }" else
-    F.pp_print_string fmt "_") params;
+  List.iter
+    (fun e ->
+      F.pp_print_space fmt ();
+      if e = Implicit then F.pp_print_string fmt "{ _ }"
+      else F.pp_print_string fmt "_")
+    params;
   F.pp_print_string fmt ".";
 
   (* Close the box *)
@@ -1731,7 +1733,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
   if num_params = 0 then ()
   else
     (* Generate the [Arguments] instruction *)
-    let params = (Collections.List.repeat num_params Implicit) in
+    let params = Collections.List.repeat num_params Implicit in
     match decl.kind with
     | Opaque -> ()
     | Struct fields ->