ocamlformat

hacspec · Apr 24, 2024 · ae7c460 · ae7c460
1 parent fd6eeae
commit ae7c460
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 16 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -1111,7 +1111,8 @@ struct
                            let args =
                              List.map ~f:(pgeneric_value e.span) args
                            in
-                           ( F.id (name ^ "_" ^ impl_ident_name), (* Dodgy concatenation *)
+                           ( F.id (name ^ "_" ^ impl_ident_name),
+                             (* Dodgy concatenation *)
                              None,
                              [],
                              F.mk_e_app base args ))
@@ -1128,16 +1129,23 @@ struct
                     let output = pty e.span output in
                     let ty_pre_post =
                       let inputs = List.map ~f:FStarBinder.to_term inputs in
-		      let add_pre n = n ^ "_pre" in
-		      let pre_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) in
+                      let add_pre n = n ^ "_pre" in
+                      let pre_name_str =
+                        U.Concrete_ident_view.to_definition_name
+                          (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident)
+                      in
                       let pre =
-                        F.mk_e_app (F.term_of_lid [pre_name_str]) inputs in
+                        F.mk_e_app (F.term_of_lid [ pre_name_str ]) inputs
+                      in
                       let result = F.term_of_lid [ "result" ] in
-		      let add_post n = n ^ "_post" in
-		      let post_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) in
+                      let add_post n = n ^ "_post" in
+                      let post_name_str =
+                        U.Concrete_ident_view.to_definition_name
+                          (Concrete_ident.Create.map_last ~f:add_post i.ti_ident)
+                      in
                       let post =
                         F.mk_e_app
-                          (F.term_of_lid [ post_name_str])
+                          (F.term_of_lid [ post_name_str ])
                           (inputs @ [ result ])
                       in
                       let post =

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -1502,15 +1502,12 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                        ii_v =
                          (match (item.kind : Thir.impl_item_kind) with
                          | Fn { body; params; _ } ->
-		             let params =
-			          if List.is_empty params then [ U.make_unit_param span ]
-			          else List.map ~f:(c_param item.span) params
-		             in
-                             IIFn
-                               {
-                                 body = c_expr body;
-                                 params = params;
-                               }
+                             let params =
+                               if List.is_empty params then
+                                 [ U.make_unit_param span ]
+                               else List.map ~f:(c_param item.span) params
+                             in
+                             IIFn { body = c_expr body; params }
                          | Const (_ty, e) ->
                              IIFn { body = c_expr e; params = [] }
                          | Type { ty; parent_bounds } ->