Update the name registration for globals

2 files changed, 12 insertions, 6 deletions

diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 255d4e1b..07a1732c 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -585,6 +585,9 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
 
 let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
     (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
+  (* Sanity check: the function should not be a global body - those are handled
+   * separately *)
+  assert (not def.is_global_decl_body);
   (* Lookup the LLBC def to compute the region group information *)
   let def_id = def.def_id in
   let llbc_def =
@@ -613,9 +616,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   let name =
     ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
   in
-  (* Add the function name if it's not a global *)
-  if def.is_global_decl_body then ctx
-  else ctx_add (FunId (def_id, def.back_id)) name ctx
+  ctx_add (FunId (def_id, def.back_id)) name ctx
 
 type names_map_init = {
   keywords : string list;
diff --git a/src/Translate.ml b/src/Translate.ml
index c9dc7943..61300ed8 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -670,12 +670,17 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   let ctx =
     List.fold_left
       (fun ctx (keep_fwd, def) ->
-        (* Note that we generate a decrease clause for all the recursive functions *)
+        (* We generate a decrease clause for all the recursive functions *)
         let gen_decr_clause =
           A.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
         in
-        ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
-          gen_decr_clause def)
+        (* Register the names, only if the function is not a global body -
+         * those are handled later *)
+        let is_global = (fst def).Pure.is_global_decl_body in
+        if is_global then ctx
+        else
+          ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
+            gen_decr_clause def)
       ctx trans_funs
   in