Make minor modifications

6 files changed, 117 insertions, 107 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 06f82ac4..eb88b916 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -314,6 +314,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     String.concat "_" fname
   in
   let global_name (name : global_name) : string =
+    (* Converting to snake case also lowercases the letters (in Rust, global
+     * names are written in capital letters). *)
     let parts = List.map to_snake_case (get_name name) in
     String.concat "_" parts
   in
@@ -326,7 +328,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ suffix
   in
 
-  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string =
+  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string
+      =
     let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
     let suffix = "_decreases" in
@@ -795,8 +798,8 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
   ctx
 
 (** Simply add the global name to the context. *)
-let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl)
-    : extraction_ctx =
+let extract_global_decl_register_names (ctx : extraction_ctx)
+    (def : A.global_decl) : extraction_ctx =
   ctx_add_global_decl_body def ctx
 
 (** The following function factorizes the extraction of ADT values.
@@ -851,7 +854,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 =
+    (id : A.GlobalDeclId.id) : unit =
   F.pp_print_string fmt (ctx_get_global id ctx)
 
 (** [inside]: see [extract_ty].
@@ -921,13 +924,11 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       match qualif.id with
       | Func fun_id ->
           extract_function_call ctx fmt inside fun_id qualif.type_args args
-      | Global global_id ->
-          extract_global ctx fmt global_id
+      | Global global_id -> 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 ->
-          extract_field_projector ctx fmt inside app proj qualif.type_args args
-    )
+          extract_field_projector ctx fmt inside app proj qualif.type_args args)
   | _ ->
       (* "Regular" expression *)
       (* Open parentheses *)
@@ -1493,9 +1494,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
 (** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
 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 =
+    (qualif : fun_decl_qualif) (name : string) (ty : ty)
+    (extract_body : (F.formatter -> unit) Option.t) : unit =
   let is_opaque = Option.is_none extract_body in
 
   (* Open the definition box (depth=0) *)
@@ -1505,7 +1505,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Print "QUALIF NAME " *)
   F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name);
-  F.pp_print_space  fmt ();
+  F.pp_print_space fmt ();
 
   (* Open ": TYPE =" box (depth=2) *)
   F.pp_open_hvbox fmt 0;
@@ -1523,8 +1523,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   if not is_opaque then (
     (* Print " =" *)
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "=";
-  );
+    F.pp_print_string fmt "=");
   (* Close ": TYPE =" box (depth=2) *)
   F.pp_close_box fmt ();
   (* Close "QUALIF NAME : TYPE =" box (depth=1) *)
@@ -1537,8 +1536,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
     (* Print "BODY" *)
     (Option.get extract_body) fmt;
     (* Close "BODY" box (depth=1) *)
-    F.pp_close_box fmt ()
-  );
+    F.pp_close_box fmt ());
   (* Close the definition box (depth=0) *)
   F.pp_close_box fmt ()
 
@@ -1554,39 +1552,37 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
-  assert (body.is_global_body);
+  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.global_name_to_string global.name ^ "] *)");
-  F.pp_print_space  fmt ();
+  F.pp_print_break fmt 0 0;
+  F.pp_print_string fmt
+    ("(** [" ^ Print.global_name_to_string global.name ^ "] *)");
+  F.pp_print_space fmt ();
 
   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
-    if body.signature.info.effect_info.can_fail
-      then (unwrap_result_ty ty, ty)
-      else (ty, mk_result_ty ty)
+    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 ->
       let qualif = if interface then Val else AssumeVal in
       extract_global_decl_body ctx fmt qualif decl_name decl_ty None
   | Some body ->
-      extract_global_decl_body ctx fmt Let body_name body_ty (Some (fun fmt ->
-        extract_texpression ctx fmt false body.body
-      ));
+      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_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
+      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
 
 (** Extract a unit test, if the function is a unit function (takes no
     parameters, returns unit).
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 4598895e..4a4f3353 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -110,14 +110,13 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
     ctx
 
 (** Convert an operand constant operand value to a typed value *)
-let constant_to_typed_value (ty : T.ety)
-    (cv : V.constant_value) : V.typed_value =
+let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value
+    =
   (* Check the type while converting - we actually need some information
-  * contained in the type *)
+     * contained in the type *)
   log#ldebug
     (lazy
-      ("constant_to_typed_value:" ^ "\n- cv: "
-      ^ PV.constant_value_to_string cv));
+      ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv));
   match (ty, cv) with
   (* Scalar, boolean... *)
   | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty }
@@ -128,10 +127,8 @@ let constant_to_typed_value (ty : T.ety)
       assert (int_ty = v.int_ty);
       assert (check_scalar_value_in_range v);
       { V.value = V.Concrete (V.Scalar v); ty }
-  (* Remaining cases (invalid) - listing as much as we can on purpose
-    (allows to catch errors at compilation if the definitions change) *)
-  | _, _ ->
-      failwith "Improperly typed constant value"
+  (* Remaining cases (invalid) *)
+  | _, _ -> failwith "Improperly typed constant value"
 
 (** Reorganize the environment in preparation for the evaluation of an operand.
 
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 48620439..34310ea1 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -831,8 +831,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
 
         (* Compose and apply *)
         comp cf_eval_rvalue cf_assign cf ctx
-    | A.AssignGlobal { dst; global } ->
-        eval_global config dst global cf ctx
+    | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx
     | A.FakeRead p ->
         let expand_prim_copy = false in
         let cf_prepare cf =
@@ -910,20 +909,27 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
 
-and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.id) : st_cm_fun =
+and eval_global (config : C.config) (dest : V.VarId.id)
+    (gid : LA.GlobalDeclId.id) : st_cm_fun =
  fun cf ctx ->
   let global = C.ctx_lookup_global_decl ctx gid in
   let place = { E.var_id = dest; projection = [] } in
   match config.mode with
   | ConcreteMode ->
-    (* Treat the global as a function without arguments to call *)
-    (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx
+      (* Treat the evaluation of the global as a call to the global body (without arguments) *)
+      (eval_local_function_call_concrete config global.body_id [] [] [] place)
+        cf ctx
   | SymbolicMode ->
-    (* Treat the global as a fresh symbolic value *)
-    let sval = mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) in
-    let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) place in
-    let e = cc (cf Unit) ctx in
-    S.synthesize_global_eval gid sval e
+      (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
+       * defined as equal to the value of the global (see `S.synthesize_global_eval`). *)
+      let sval =
+        mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty)
+      in
+      let cc =
+        assign_to_place config (mk_typed_value_from_symbolic_value sval) place
+      in
+      let e = cc (cf Unit) ctx in
+      S.synthesize_global_eval gid sval e
 
 (** 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 be43ff54..846d7232 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -394,7 +394,7 @@ let constant_value_of_json (js : json) : (V.constant_value, string) result =
         let* v = string_of_json v in
         Ok (V.String v)
     | _ -> Error "")
-  
+
 let operand_of_json (js : json) : (E.operand, string) result =
   combine_error_msgs js "operand_of_json"
     (match js with
@@ -599,10 +599,8 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result =
     | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
         let* int_ty = integer_type_of_json int_ty in
         let* tgts =
-            list_of_json (
-              pair_of_json
-              (list_of_json scalar_value_of_json)
-              statement_of_json)
+          list_of_json
+            (pair_of_json (list_of_json scalar_value_of_json) statement_of_json)
             tgts
         in
         let* otherwise = statement_of_json otherwise in
@@ -633,47 +631,47 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
         let* name = fun_name_of_json name in
         let* signature = fun_sig_of_json signature in
         let* body = option_of_json fun_body_of_json body in
-        Ok { A.def_id; name; signature; body; is_global_body = false; }
+        Ok { A.def_id; name; signature; body; is_global_body = false }
     | _ -> Error "")
 
 (* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
-type global_id_converter = { fun_count : int }
-[@@deriving show]
+type global_id_converter = { fun_count : int } [@@deriving show]
 
 (** Converts a global id to its corresponding function id.
     To do so, it adds the global id to the number of function declarations :
-    We have the bijection `global_id <=> fun_id + fun_id_count`.
+    We have the bijection `global_fun_id <=> global_id + fun_id_count`.
 *)
-let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id =
-  A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count)
+let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) :
+    A.FunDeclId.id =
+  A.FunDeclId.of_int (A.GlobalDeclId.to_int gid + conv.fun_count)
 
 (* Converts a global declaration to a function declaration.
  *)
-let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result =
+let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
+    (A.global_decl * A.fun_decl, string) result =
   combine_error_msgs js "global_decl_of_json"
     (match js with
-    | `Assoc
-        [
-          ("def_id", def_id);
-          ("name", name);
-          ("ty", ty);
-          ("body", body);
-        ] ->
+    | `Assoc [ ("def_id", def_id); ("name", name); ("ty", ty); ("body", body) ]
+      ->
         let* global_id = A.GlobalDeclId.id_of_json def_id in
         let fun_id = global_to_fun_id gid_conv global_id in
         let* name = fun_name_of_json name in
         let* ty = ety_of_json ty in
         let* body = option_of_json fun_body_of_json body in
-        let signature : A.fun_sig = {
-          region_params = [];
-          num_early_bound_regions = 0;
-          regions_hierarchy = [];
-          type_params = [];
-          inputs = [];
-          output = TU.ety_no_regions_to_sty ty;
-        } in
-        Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; },
-            { A.def_id = fun_id; name; signature; body; is_global_body = true; })
+        let signature : A.fun_sig =
+          {
+            region_params = [];
+            num_early_bound_regions = 0;
+            regions_hierarchy = [];
+            type_params = [];
+            inputs = [];
+            output = TU.ety_no_regions_to_sty ty;
+          }
+        in
+        Ok
+          ( { A.def_id = global_id; body_id = fun_id; name; ty },
+            { A.def_id = fun_id; name; signature; body; is_global_body = true }
+          )
     | _ -> Error "")
 
 let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
@@ -701,13 +699,12 @@ let fun_declaration_group_of_json (js : json) :
 let global_declaration_group_of_json (js : json) :
     (A.GlobalDeclId.id, string) result =
   combine_error_msgs js "global_declaration_group_of_json"
-  (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 "")
+    (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
     =
@@ -724,11 +721,11 @@ let declaration_group_of_json (js : json) : (M.declaration_group, string) result
         Ok (M.Global id)
     | _ -> Error "")
 
-let length_of_json_list (js: json) : (int, string) result =
+let length_of_json_list (js : json) : (int, string) result =
   combine_error_msgs js "get_json_list_len"
     (match js with
-      | `List jsl -> Ok (List.length jsl)
-      | _ -> Error ("not a list: " ^ show js))
+    | `List jsl -> Ok (List.length jsl)
+    | _ -> Error ("not a list: " ^ show js))
 
 let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
   combine_error_msgs js "llbc_module_of_json"
@@ -741,18 +738,30 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
           ("functions", functions);
           ("globals", globals);
         ] ->
+        (* We first deserialize the declaration groups (which simply contain ids)
+         * and all the declarations *butù* the globals *)
         let* name = string_of_json name in
-        let* declarations = list_of_json declaration_group_of_json declarations 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
+        (* When deserializing the globals, we split the global declarations
+         * between the globals themselves and their bodies, which are simply
+         * functions with no arguments. We add the global bodies to the list
+         * of function declarations: the (fresh) ids we use for those bodies
+         * are simply given by: `num_functions + global_id` *)
         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 =
+          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;
-          declarations;
-          types;
-          functions = functions @ global_bodies;
-          globals;
-        }
+        Ok
+          {
+            M.name;
+            declarations;
+            types;
+            functions = functions @ global_bodies;
+            globals;
+          }
     | _ -> Error "")
diff --git a/src/Modules.ml b/src/Modules.ml
index 009e1ba6..7f372d09 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -7,10 +7,9 @@ type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
 type type_declaration_group = TypeDeclId.id g_declaration_group
 [@@deriving show]
 
-type fun_declaration_group = FunDeclId.id g_declaration_group
-[@@deriving show]
+type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
 
-(** Module declaration. Globals cannot be mutually dependent. *)
+(** Module declaration. Globals cannot be mutually recursive. *)
 type declaration_group =
   | Type of type_declaration_group
   | Fun of fun_declaration_group
@@ -27,7 +26,9 @@ type llbc_module = {
 (** LLBC module - TODO: rename to crate *)
 
 let compute_defs_maps (m : llbc_module) :
-    type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t =
+    type_decl TypeDeclId.Map.t
+    * fun_decl FunDeclId.Map.t
+    * global_decl GlobalDeclId.Map.t =
   let types_map =
     List.fold_left
       (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
@@ -45,9 +46,11 @@ let compute_defs_maps (m : llbc_module) :
   in
   (types_map, funs_map, globals_map)
 
-(** Split a module's declarations between types, globals and functions *)
+(** Split a module's declarations between types, functions and globals *)
 let split_declarations (decls : declaration_group list) :
-    type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list =
+    type_declaration_group list
+    * fun_declaration_group list
+    * GlobalDeclId.id list =
   let rec split decls =
     match decls with
     | [] -> ([], [], [])
@@ -56,8 +59,7 @@ let split_declarations (decls : declaration_group list) :
         match d with
         | Type decl -> (decl :: types, funs, globals)
         | Fun decl -> (types, decl :: funs, globals)
-        | Global decl -> (types, funs, decl :: globals)
-      )
+        | Global decl -> (types, funs, decl :: globals))
   in
   split decls
 
@@ -66,7 +68,7 @@ let split_declarations (decls : declaration_group list) :
  *)
 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)
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 8a1c074d..e72ff9d7 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -402,7 +402,7 @@ 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"
+  | _ -> failwith "not a result type"
 
 let mk_result_fail_texpression (ty : ty) : texpression =
   let type_args = [ ty ] in