Correct last PR remarks

3 files changed, 20 insertions, 26 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index f2c481c0..7f271f02 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -797,7 +797,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
 (** Simply add the global name to the context. *)
 let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl)
     : extraction_ctx =
-  ctx_add_global_decl def ctx
+  ctx_add_global_decl_body def ctx
 
 (** The following function factorizes the extraction of ADT values.
 
@@ -852,7 +852,7 @@ let extract_adt_g_value
 (* Extract globals in the same way as variables *)
 let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
   	(id : A.GlobalDeclId.id) : unit =
-  F.pp_print_string fmt (ctx_get_global_decl id ctx)
+  F.pp_print_string fmt (ctx_get_global id ctx)
 
 (** [inside]: see [extract_ty].
 
@@ -1491,16 +1491,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
-(* Change the suffix from "_c" to "_body" *)
-let global_decl_to_body_name (decl : string) : string =
-  (* The declaration length without the global suffix *)
-  let base_len = String.length decl - 2 in
-  (* TODO: Use String.ends_with instead when a more recent version of OCaml is used *)
-  assert (String.sub decl base_len 2 = "_c");
-  (String.sub decl 0 base_len) ^ "_body"
-
 (** Extract a global definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
-let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   (qualif : fun_decl_qualif) (name : string) (ty : ty)
   (extract_body : (F.formatter -> unit) Option.t)
     : unit =
@@ -1574,8 +1566,8 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)");
   F.pp_print_space  fmt ();
 
-  let decl_name = ctx_get_global_decl global.def_id ctx in
-  let body_name = ctx_get_global_body global.def_id ctx in
+  let decl_name = ctx_get_global global.def_id ctx in
+  let body_name = ctx_get_function (Regular global.body_id) None ctx in
 
   let decl_ty, body_ty =
     let ty = body.signature.output in
@@ -1586,13 +1578,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   match body.body with
   | None ->
       let qualif = if interface then Val else AssumeVal in
-      extract_global_definition ctx fmt qualif decl_name decl_ty None
+      extract_global_decl_body ctx fmt qualif decl_name decl_ty None
   | Some body ->
-      extract_global_definition ctx fmt Let body_name body_ty (Some (fun fmt ->
+      extract_global_decl_body ctx fmt Let body_name body_ty (Some (fun fmt ->
         extract_texpression ctx fmt false body.body
       ));
       F.pp_print_break fmt 0 0;
-      extract_global_definition ctx fmt Let decl_name decl_ty (Some (fun fmt ->
+      extract_global_decl_body ctx fmt Let decl_name decl_ty (Some (fun fmt ->
         F.pp_print_string fmt ("eval_global " ^ body_name)
       ));
   F.pp_print_break fmt 0 0
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 1dc7eae9..b7d45deb 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -449,12 +449,9 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string =
       log#serror ("Could not find: " ^ id_to_string id ctx);
       raise Not_found
 
-let ctx_get_global_decl (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
-  ctx_get (GlobalId id) ctx ^ "_c"
+let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
+  ctx_get (GlobalId id) ctx
 
-let ctx_get_global_body (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
-  ctx_get (GlobalId id) ctx ^ "_body"
-  
 let ctx_get_function (id : A.fun_id)
     (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
@@ -585,9 +582,14 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) :
   let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
   ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx
 
-let ctx_add_global_decl (def : A.global_decl) (ctx : extraction_ctx) :
+let ctx_add_global_decl_body (def : A.global_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  ctx_add (GlobalId def.def_id) (ctx.fmt.global_name def.name) ctx
+  let name = ctx.fmt.global_name def.name in
+  let decl = GlobalId def.def_id in
+  let body = FunId (Regular def.body_id, None) in
+  let ctx = ctx_add decl (name ^ "_c") ctx in
+  let ctx = ctx_add body (name ^ "_body") ctx in
+  ctx
 
 let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
     (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 5cfb82d6..4a9a0e48 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -31,14 +31,14 @@ let x3_body : result u32 =
 let x3_c : u32 = eval_global x3_body
 
 (** [constants::mk_pair0] *)
-let mk_pair0_fwd (x : u32) (y0 : u32) : result (u32 & u32) = Return (x, y0)
+let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
 
 (** [constants::Pair] *)
 type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
 
 (** [constants::mk_pair1] *)
-let mk_pair1_fwd (x : u32) (y0 : u32) : result (pair_t u32 u32) =
-  Return (Mkpair_t x y0)
+let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
+  Return (Mkpair_t x y)
 
 (** [constants::P0] *)
 let p0_body : result (u32 & u32) =