resolved comments

3 files changed, 113 insertions, 99 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1fc8a97f..f7d08fdb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1879,102 +1879,104 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
     [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl}
     and {!extract_fun_decl}.
  *)
-let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
+    (global : global_decl) (body : fun_decl) (interface : bool) : unit =
   let meta = body.meta in
   sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
   sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
-  match global with
-  | Some global -> (
-      (* Add a break then the name of the corresponding LLBC declaration *)
+  (* Add a break then the name of the corresponding LLBC declaration *)
+  F.pp_print_break fmt 0 0;
+  let name =
+    if !Config.extract_external_name_patterns && not global.is_local then
+      Some global.llbc_name
+    else None
+  in
+  extract_comment_with_span ctx fmt
+    [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
+    name global.meta.span;
+  F.pp_print_space fmt ();
+
+  let decl_name = ctx_get_global meta global.def_id ctx in
+  let body_name =
+    ctx_get_function meta
+      (FromLlbc (Pure.FunId (FRegular global.body_id), None))
+      ctx
+  in
+  let decl_ty, body_ty =
+    let ty = body.signature.output in
+    if body.signature.fwd_info.effect_info.can_fail then
+      (unwrap_result_ty meta ty, ty)
+    else (ty, mk_result_ty ty)
+  in
+  (* Add the type parameters *)
+  let ctx, type_params, cg_params, trait_clauses =
+    ctx_add_generic_params meta global.llbc_name global.llbc_generics
+      global.generics ctx
+  in
+  match body.body with
+  | None ->
+      (* No body: only generate a [val x_c : u32] declaration *)
+      let kind = if interface then Declared else Assumed in
+      if !backend = HOL4 then
+        extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics
+          decl_ty
+      else
+        extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics
+          type_params cg_params trait_clauses decl_ty None
+  | Some body ->
+      (* There is a body *)
+      (* Generate: [let x_body : result u32 = Return 3] *)
+      extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
+        global.generics type_params cg_params trait_clauses body_ty
+        (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
       F.pp_print_break fmt 0 0;
-      let name =
-        if !Config.extract_external_name_patterns && not global.is_local then
-          Some global.llbc_name
-        else None
-      in
-      extract_comment_with_span ctx fmt
-        [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
-        name global.meta.span;
-      F.pp_print_space fmt ();
+      (* Generate: [let x_c : u32 = eval_global x_body] *)
+      extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
+        global.generics type_params cg_params trait_clauses decl_ty
+        (Some
+           (fun fmt ->
+             let all_params =
+               List.concat [ type_params; cg_params; trait_clauses ]
+             in
+             let extract_params () =
+               List.iter
+                 (fun p ->
+                   F.pp_print_space fmt ();
+                   F.pp_print_string fmt p)
+                 all_params
+             in
+             let use_brackets = all_params <> [] in
+             (* Extract the name *)
+             let before, after =
+               match !backend with
+               | FStar | Lean ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "eval_global";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
+               | Coq ->
+                   ((fun () -> ()), fun () -> F.pp_print_string fmt "%global")
+               | HOL4 ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "get_return_value";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
+             in
+             before ();
+             if use_brackets then F.pp_print_string fmt "(";
+             F.pp_print_string fmt body_name;
+             (* Extract the generic params *)
+             extract_params ();
+             if use_brackets then F.pp_print_string fmt ")";
+             (* *)
+             after ()));
+      (* Add a break to insert lines between declarations *)
+      F.pp_print_break fmt 0 0
 
-      let decl_name = ctx_get_global meta global.def_id ctx in
-      let body_name =
-        ctx_get_function meta
-          (FromLlbc (Pure.FunId (FRegular global.body_id), None))
-          ctx
-      in
-      let decl_ty, body_ty =
-        let ty = body.signature.output in
-        if body.signature.fwd_info.effect_info.can_fail then
-          (unwrap_result_ty meta ty, ty)
-        else (ty, mk_result_ty ty)
-      in
-      (* Add the type parameters *)
-      let ctx, type_params, cg_params, trait_clauses =
-        ctx_add_generic_params meta global.llbc_name global.llbc_generics
-          global.generics ctx
-      in
-      match body.body with
-      | None ->
-          (* No body: only generate a [val x_c : u32] declaration *)
-          let kind = if interface then Declared else Assumed in
-          if !backend = HOL4 then
-            extract_global_decl_hol4_opaque meta ctx fmt decl_name
-              global.generics decl_ty
-          else
-            extract_global_decl_body_gen meta ctx fmt kind decl_name
-              global.generics type_params cg_params trait_clauses decl_ty None
-      | Some body ->
-          (* There is a body *)
-          (* Generate: [let x_body : result u32 = Return 3] *)
-          extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
-            global.generics type_params cg_params trait_clauses body_ty
-            (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
-          F.pp_print_break fmt 0 0;
-          (* Generate: [let x_c : u32 = eval_global x_body] *)
-          extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
-            global.generics type_params cg_params trait_clauses decl_ty
-            (Some
-               (fun fmt ->
-                 let all_params =
-                   List.concat [ type_params; cg_params; trait_clauses ]
-                 in
-                 let extract_params () =
-                   List.iter
-                     (fun p ->
-                       F.pp_print_space fmt ();
-                       F.pp_print_string fmt p)
-                     all_params
-                 in
-                 let use_brackets = all_params <> [] in
-                 (* Extract the name *)
-                 let before, after =
-                   match !backend with
-                   | FStar | Lean ->
-                       ( (fun () ->
-                           F.pp_print_string fmt "eval_global";
-                           F.pp_print_space fmt ()),
-                         fun () -> () )
-                   | Coq ->
-                       ( (fun () -> ()),
-                         fun () -> F.pp_print_string fmt "%global" )
-                   | HOL4 ->
-                       ( (fun () ->
-                           F.pp_print_string fmt "get_return_value";
-                           F.pp_print_space fmt ()),
-                         fun () -> () )
-                 in
-                 before ();
-                 if use_brackets then F.pp_print_string fmt "(";
-                 F.pp_print_string fmt body_name;
-                 (* Extract the generic params *)
-                 extract_params ();
-                 if use_brackets then F.pp_print_string fmt ")";
-                 (* *)
-                 after ()));
-          (* Add a break to insert lines between declarations *)
-          F.pp_print_break fmt 0 0)
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+  match global with
+  | Some global -> extract_global_decl_aux ctx fmt global body interface
   | None -> ()
 
 (** Similar to {!extract_trait_decl_register_names} *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index b4c55d80..eac4adb9 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3865,7 +3865,10 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
     (fun a ->
       try Some (translate_type_decl ctx a)
       with CFailure (meta, _) ->
-        let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+        let () =
+          save_error __FILE__ __LINE__ meta
+            "Could not generate code, see previous error"
+        in
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 28e5531d..c23b2a47 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
     of backward functions, we also provide names for the outputs.
     TODO: maybe we should introduce a record for this.
 *)
-let translate_function_to_pure_hook (trans_ctx : trans_ctx)
+let translate_function_to_pure_aux (trans_ctx : trans_ctx)
     (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
     (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
     pure_fun_translation_no_loops =
@@ -201,9 +201,12 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     pure_fun_translation_no_loops option =
   try
     Some
-      (translate_function_to_pure_hook trans_ctx pure_type_decls fun_dsigs fdef)
+      (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
   with CFailure (meta, _) ->
-    let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+    let () =
+      save_error __FILE__ __LINE__ meta
+        "Could not translate function because of previous error"
+    in
     None
 
 (* TODO: factor out the return type *)
@@ -240,7 +243,8 @@ let translate_crate_to_pure (crate : crate) :
                    trans_ctx fdef )
            with CFailure (meta, _) ->
              let () =
-               save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+               save_error __FILE__ __LINE__ meta
+                 "Could not translate function because of previous error"
              in
              None)
          (FunDeclId.Map.values crate.fun_decls))
@@ -260,7 +264,8 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
         with CFailure (meta, _) ->
           let () =
-            save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+            save_error __FILE__ __LINE__ meta
+              "Could not translate trait decl because of previous error"
           in
           None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
@@ -273,7 +278,8 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
         with CFailure (meta, _) ->
           let () =
-            save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+            save_error __FILE__ __LINE__ meta
+              "Could not translate trait impl because of previous error"
           in
           None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
@@ -504,7 +510,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     let global =
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (meta, _) ->
-        let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+        let () =
+          save_error __FILE__ __LINE__ meta
+            "Could not translate global because of previous error"
+        in
         None
     in
     Extract.extract_global_decl ctx fmt global body config.interface