Create global declaration group, address PR changes but introduce bugs

10 files changed, 134 insertions, 83 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 2c53e45b..a2b15ece 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -313,11 +313,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     (* Concatenate the elements *)
     String.concat "_" fname
   in
-  let fun_name (_fid : A.fun_id) (fname : fun_name) (is_global : bool) (num_rgs : int)
+  let global_name (name : global_name) : string =
+    let parts = List.map to_snake_case (get_name name) in
+    String.concat "_" parts
+  in
+  let fun_name (_fid : A.fun_id) (fname : fun_name) (num_rgs : int)
       (rg : region_group_info option) (filter_info : bool * int) : string =
     let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
-    let suffix = default_fun_suffix is_global num_rgs rg filter_info in
+    let suffix = default_fun_suffix num_rgs rg filter_info in
     (* Concatenate *)
     fname ^ suffix
   in
@@ -411,6 +415,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     variant_name;
     struct_constructor;
     type_name;
+    global_name;
     fun_name;
     decreases_clause_name;
     var_basename;
@@ -839,6 +844,11 @@ let extract_adt_g_value
       ctx
   | _ -> raise (Failure "Inconsistent typed 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)
+
 (** [inside]: see [extract_ty].
 
     As an pattern can introduce new variables, we return an extraction context
@@ -907,12 +917,7 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       | Func fun_id ->
           extract_function_call ctx fmt inside fun_id qualif.type_args args
       | Global global_id ->
-          failwith "TODO ExtractToFStar.ml:911"
-          (* Previous code:
-          let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in
-          let fun_id = Regular (A.Regular fid, None) in
-          extract_function_call ctx fmt inside fun_id qualif.type_args args
-          *)
+          extract_global ctx fmt global_id
       | AdtCons adt_cons_id ->
           extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
       | Proj proj ->
@@ -1353,6 +1358,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
     unit =
+  assert (def.is_global_body);
   (* Retrieve the function name *)
   let def_name = ctx_get_local_function def.def_id def.back_id ctx in
   (* (* Add the type parameters - note that we need those bindings only for the
@@ -1551,40 +1557,40 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
     `let x_c : int = eval_global x_body`
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
-  (qualif : fun_decl_qualif) (def : fun_decl)
-    : unit =
-  (* TODO Lookup LLBC decl *)
-  (* Sanity checks for globals *)
-  assert (def.is_global_body);
-  failwith "TODO ExtractToFStar.ml:1559"
-  (* Previous code:
-  assert (Option.is_none def.back_id);
-  assert (List.length def.signature.inputs = 0);
-  assert (List.length def.signature.doutputs = 1);
-  assert (List.length def.signature.type_params = 0);
-  assert (not def.signature.info.effect_info.can_fail);
+    (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
+  assert (body.is_global_body);
+  assert (Option.is_none body.back_id);
+  assert (List.length body.signature.inputs = 0);
+  assert (List.length body.signature.doutputs = 1);
+  assert (List.length body.signature.type_params = 0);
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break  fmt 0 0;
-  F.pp_print_string fmt ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)");
+  F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)");
   F.pp_print_space  fmt ();
 
-  let def_name = ctx_get_local_function def.def_id def.back_id ctx in
-  match def.body with
+  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_ty, body_ty =
+    let ty = body.signature.output in
+    if body.signature.info.effect_info.can_fail
+      then (unwrap_result_ty ty, ty)
+      else (ty, mk_result_ty ty)
+  in
+  match body.body with
   | None ->
-      extract_global_definition ctx fmt qualif def_name def.signature.output None
+      let qualif = if interface then Val else AssumeVal in
+      extract_global_definition ctx fmt qualif decl_name decl_ty None
   | Some body ->
-      let body_name = global_decl_to_body_name def_name in
-      let body_ty = mk_result_ty def.signature.output in
-      extract_global_definition ctx fmt qualif body_name body_ty (Some (fun fmt ->
+      extract_global_definition 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 qualif def_name def.signature.output (Some (fun fmt ->
+      extract_global_definition 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
-  *)
 
 (** Extract a unit test, if the function is a unit function (takes no
     parameters, returns unit).
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 3a6ad542..65a130c8 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -1,7 +1,7 @@
 (** Compute various information, including:
     - can a function fail (by having `Fail` in its body, or transitively
       calling a function which can fail), false for globals
-    - can a function diverge (bu being recursive, containing a loop or
+    - can a function diverge (by being recursive, containing a loop or
       transitively calling a function which can diverge)
     - does a function perform stateful operations (i.e., do we need a state
       to translate it)
@@ -26,7 +26,9 @@ type fun_info = {
 type modules_funs_info = fun_info FunDeclId.Map.t
 (** Various information about a module's functions *)
 
-let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
+let analyze_module (m : llbc_module)
+    (funs_map : fun_decl FunDeclId.Map.t)
+    (globals_map : global_decl GlobalDeclId.Map.t)
     (use_state : bool) : modules_funs_info =
   let infos = ref FunDeclId.Map.empty in
 
@@ -104,7 +106,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
        * syntactically can't fail don't use an error monad. *)
     in
     List.iter visit_fun d;
-    (* Not-failing functions are not handled yet. *)
+    (* Non-failing functions are not handled yet. *)
     can_fail := true;
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
   in
@@ -126,6 +128,11 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
     | Fun decl :: decls' ->
         analyze_fun_decl_group decl;
         analyze_decl_groups decls'
+    | Global id :: decls' ->
+        (* Analyze a global by analyzing its body function *)
+        let global = GlobalDeclId.Map.find id globals_map in
+        analyze_fun_decl_group (NonRec global.body_id);
+        analyze_decl_groups decls'
   in
 
   analyze_decl_groups m.declarations;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3610d486..51144ba2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -15,9 +15,9 @@ let log = L.interpreter_log
 
 let compute_type_fun_contexts (m : M.llbc_module) :
     C.type_context * C.fun_context * C.global_context =
-  let type_decls_list, _ = M.split_declarations m.declarations in
+  let type_decls_list, _, _ = M.split_declarations m.declarations in
   let type_decls, fun_decls, global_decls = M.compute_defs_maps m in
-  let type_decls_groups, _funs_defs_groups =
+  let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
     M.split_declarations_to_group_maps m.declarations
   in
   let type_infos =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 3f6470b9..ffc47741 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -919,11 +919,16 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i
     (* Treat the global as a function without arguments to call *)
     (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx
   | SymbolicMode ->
+    (*
+    let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in
+    (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx
+    *)
+    failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value";
     (* Treat the global as a fresh symbolic value *)
     let rty = ety_no_regions_to_rty global.ty in
     let sval = mk_fresh_symbolic_value V.FunCallRet rty in
     let sval = mk_typed_value_from_symbolic_value sval in
-    assign_to_place config sval place (cf Unit) ctx
+    (assign_to_place config sval place) (cf Unit) ctx
 
 (** Evaluate a switch *)
 and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index f51c15be..be43ff54 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -698,18 +698,18 @@ let fun_declaration_group_of_json (js : json) :
   combine_error_msgs js "fun_declaration_group_of_json"
     (g_declaration_group_of_json A.FunDeclId.id_of_json js)
 
-(* TODO Should a global declaration group be converted to its function bodies ?
-        It does not seems very clean.
-*)
-let global_declaration_group_of_json (js : json) (gid_conv : global_id_converter) :
-    (M.fun_declaration_group, string) result =
+let global_declaration_group_of_json (js : json) :
+    (A.GlobalDeclId.id, string) result =
   combine_error_msgs js "global_declaration_group_of_json"
-    (g_declaration_group_of_json (fun js ->
-        let* id = A.GlobalDeclId.id_of_json js in
-        Ok (global_to_fun_id gid_conv id)
-      ) js)
-
-let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result
+  (match js with
+  | `Assoc [ ("NonRec", `List [ id ]) ] ->
+      let* id = A.GlobalDeclId.id_of_json id in
+      Ok (id)
+  | `Assoc [ ("Rec", `List [ _ ]) ] ->
+      Error "got mutually dependent globals"
+  | _ -> Error "")
+
+let declaration_group_of_json (js : json) : (M.declaration_group, string) result
     =
   combine_error_msgs js "declaration_of_json"
     (match js with
@@ -720,8 +720,8 @@ let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.
         let* decl = fun_declaration_group_of_json decl in
         Ok (M.Fun decl)
     | `Assoc [ ("Global", `List [ decl ]) ] ->
-        let* decl = global_declaration_group_of_json decl gid_conv in
-        Ok (M.Fun decl)
+        let* id = global_declaration_group_of_json decl in
+        Ok (M.Global id)
     | _ -> Error "")
 
 let length_of_json_list (js: json) : (int, string) result =
@@ -741,15 +741,12 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
           ("functions", functions);
           ("globals", globals);
         ] ->
-        let* fun_count = length_of_json_list functions in
-        let gid_conv = { fun_count } in
         let* name = string_of_json name in
-        let* declarations =
-          list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations
-        in
-        let* types     = list_of_json type_decl_of_json types in
+        let* declarations = list_of_json declaration_group_of_json declarations in
+        let* types = list_of_json type_decl_of_json types in
         let* functions = list_of_json fun_decl_of_json functions in
-        let* globals   = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
+        let gid_conv = { fun_count = List.length functions } in
+        let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
         let globals, global_bodies = List.split globals in
         Ok {
           M.name;
diff --git a/src/Modules.ml b/src/Modules.ml
index 2f640636..009e1ba6 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -10,10 +10,11 @@ type type_declaration_group = TypeDeclId.id g_declaration_group
 type fun_declaration_group = FunDeclId.id g_declaration_group
 [@@deriving show]
 
-(** Module declaration *)
+(** Module declaration. Globals cannot be mutually dependent. *)
 type declaration_group =
   | Type of type_declaration_group
   | Fun of fun_declaration_group
+  | Global of GlobalDeclId.id
 [@@deriving show]
 
 type llbc_module = {
@@ -44,26 +45,29 @@ let compute_defs_maps (m : llbc_module) :
   in
   (types_map, funs_map, globals_map)
 
-(** Split a module's declarations between types and functions *)
+(** Split a module's declarations between types, globals and functions *)
 let split_declarations (decls : declaration_group list) :
-    type_declaration_group list * fun_declaration_group list =
+    type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list =
   let rec split decls =
     match decls with
-    | [] -> ([], [])
+    | [] -> ([], [], [])
     | d :: decls' -> (
-        let types, funs = split decls' in
+        let types, funs, globals = split decls' in
         match d with
-        | Type decl -> (decl :: types, funs)
-        | Fun decl -> (types, decl :: funs))
+        | Type decl -> (decl :: types, funs, globals)
+        | Fun decl -> (types, decl :: funs, globals)
+        | Global decl -> (types, funs, decl :: globals)
+      )
   in
   split decls
 
-(** Split a module's declarations into two maps from type/fun ids to
+(** Split a module's declarations into three maps from type/fun/global ids to
     declaration groups.
  *)
 let split_declarations_to_group_maps (decls : declaration_group list) :
     type_declaration_group TypeDeclId.Map.t
-    * fun_declaration_group FunDeclId.Map.t =
+    * fun_declaration_group FunDeclId.Map.t 
+    * GlobalDeclId.Set.t =
   let module G (M : Map.S) = struct
     let add_group (map : M.key g_declaration_group M.t)
         (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
@@ -75,9 +79,10 @@ let split_declarations_to_group_maps (decls : declaration_group list) :
         M.key g_declaration_group M.t =
       List.fold_left add_group M.empty groups
   end in
-  let types, funs = split_declarations decls in
+  let types, funs, globals = split_declarations decls in
   let module TG = G (TypeDeclId.Map) in
   let types = TG.create_map types in
   let module FG = G (FunDeclId.Map) in
   let funs = FG.create_map funs in
-  (types, funs)
+  let globals = GlobalDeclId.Set.of_list globals in
+  (types, funs, globals)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 2d76f348..1dc7eae9 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -32,6 +32,8 @@ type name = Names.name
 
 type type_name = Names.type_name
 
+type global_name = Names.global_name
+
 type fun_name = Names.fun_name
 
 (* TODO: this should a module we give to a functor! *)
@@ -71,10 +73,11 @@ type formatter = {
        *)
   type_name : type_name -> string;
       (** Provided a basename, compute a type name. *)
+  global_name : global_name -> string;
+      (** Provided a basename, compute a global name. *)
   fun_name :
     A.fun_id ->
     fun_name ->
-    bool ->
     int ->
     region_group_info option ->
     bool * int ->
@@ -83,7 +86,6 @@ type formatter = {
           - function id: this is especially useful to identify whether the
             function is an assumed function or a local function
           - function basename
-          - flag indicating if the function is a global
           - number of region groups
           - region group information in case of a backward function
             (`None` if forward function)
@@ -186,6 +188,7 @@ type formatter = {
 
 (** We use identifiers to look for name clashes *)
 type id =
+  | GlobalId of A.GlobalDeclId.id
   | FunId of A.fun_id * RegionGroupId.id option
   | DecreasesClauseId of A.fun_id
       (** The definition which provides the decreases/termination clause.
@@ -342,6 +345,7 @@ type extraction_ctx = {
 
 (** Debugging function *)
 let id_to_string (id : id) (ctx : extraction_ctx) : string =
+  let global_decls = ctx.trans_ctx.global_context.global_decls in
   let fun_decls = ctx.trans_ctx.fun_context.fun_decls in
   let type_decls = ctx.trans_ctx.type_context.type_decls in
   (* TODO: factorize the pretty-printing with what is in PrintPure *)
@@ -354,6 +358,9 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
     | Tuple -> failwith "Unreachable"
   in
   match id with
+  | GlobalId gid ->
+      let name = (A.GlobalDeclId.Map.find gid global_decls).name in
+      "global name: " ^ Print.global_name_to_string name
   | FunId (fid, rg_id) ->
       let fun_name =
         match fid with
@@ -442,6 +449,12 @@ 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_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 =
@@ -572,6 +585,10 @@ 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) :
+    extraction_ctx =
+  ctx_add (GlobalId def.def_id) (ctx.fmt.global_name def.name) ctx
+
 let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
     (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
   (* Lookup the LLBC def to compute the region group information *)
@@ -600,11 +617,12 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   in
   let def_id = A.Regular def_id in
   let name =
-    ctx.fmt.fun_name def_id def.basename def.is_global_body num_rgs rg_info (keep_fwd, num_backs)
+    ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
   in
-  (* Add the function name *)
-  let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in
-  ctx
+  (* Add the function name if it's not a global *)
+  if def.is_global_body
+    then ctx
+    else ctx_add (FunId (def_id, def.back_id)) name ctx
 
 type names_map_init = {
   keywords : string list;
@@ -671,7 +689,6 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
     TODO: move all those helpers.
 *)
 let default_fun_suffix
-    (is_global_body : bool)
     (num_region_groups : int)
     (rg : region_group_info option)
     ((keep_fwd, num_backs) : bool * int)
@@ -691,7 +708,6 @@ let default_fun_suffix
      we could not add the "_fwd" suffix) to prevent name clashes between
      definitions (in particular between type and function definitions).
   *)
-  if is_global_body then "_body" else
   match rg with
   | None -> "_fwd"
   | Some rg ->
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index c63814eb..39fb5073 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -112,11 +112,8 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       check_texpression ctx body
   | Qualif qualif -> (
       match qualif.id with
-      | Func _ -> () (* TODO *)
-      | Global id ->
-        let global = A.GlobalDeclId.Map.find id ctx.global_decls in
-        (* TODO: something like assert (global.ty = e.ty) *)
-        failwith "PureTypeCheck.ml:118"
+      | Func   _ -> () (* TODO *)
+      | Global _ -> () (* TODO *)
       | Proj { adt_id = proj_adt_id; field_id } ->
           (* Note we can only project fields of structures (not enumerations) *)
           (* Deconstruct the projector type *)
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 8d3b5258..8a1c074d 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -399,6 +399,11 @@ let type_decl_is_enum (def : T.type_decl) : bool =
 let mk_state_ty : ty = Adt (Assumed State, [])
 let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
 
+let unwrap_result_ty (ty : ty) : ty =
+  match ty with
+  | Adt (Assumed Result, [ ty ]) -> ty
+  | _ -> failwith "not a result"
+
 let mk_result_fail_texpression (ty : ty) : texpression =
   let type_args = [ ty ] in
   let ty = Adt (Assumed Result, type_args) in
diff --git a/src/Translate.ml b/src/Translate.ml
index a6477e7f..a936d626 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -298,7 +298,7 @@ let translate_module_to_pure (config : C.partial_config)
 
   (* Compute the type and function contexts *)
   let type_context, fun_context, global_context = compute_type_fun_contexts m in
-  let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in
+  let fun_infos = FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls use_state in
   let fun_context = {
     fun_decls = fun_context.fun_decls;
     fun_infos;
@@ -498,9 +498,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          if
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
-         then if def.is_global_body
-          then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def
-          else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def
+         then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def
         )
        fls);
     (* Insert unit tests if necessary *)
@@ -512,6 +510,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         pure_ls
   in
 
+  (* TODO: Check correct behaviour with opaque globals *)
+  let export_global (id : A.GlobalDeclId.id) : unit =
+    let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in
+    let global = A.GlobalDeclId.Map.find id global_decls in
+    let (_, (body, body_backs)) = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+    assert (List.length body_backs = 0);
+    
+    let is_opaque = Option.is_none body.Pure.body in
+    if ((not is_opaque) && config.extract_transparent)
+         || (is_opaque  && config.extract_opaque)
+    then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body config.interface
+  in
+
   let export_state_type () : unit =
     let qualif =
       if config.interface then ExtractToFStar.TypeVal
@@ -547,6 +558,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         in
         (* Translate *)
         export_functions true pure_funs
+    | Global id ->
+        export_global id
   in
 
   (* If we need to export the state type: we try to export it after we defined