Apply small changes from the PR

4 files changed, 12 insertions, 9 deletions

diff --git a/src/Expressions.ml b/src/Expressions.ml
index 6645a77f..bf06dd1e 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -72,7 +72,6 @@ let all_binops =
     Shr;
   ]
 
-(* TODO: symplify the operand constant values *)
 type operand =
   | Copy of place
   | Move of place
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 20b06bfa..5b39b0b7 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -26,7 +26,7 @@ type type_decl_qualif =
  *)
 type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
 
-let fun_decl_qualif_name (qualif : fun_decl_qualif) : string =
+let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string =
   match qualif with
   | Let -> "let"
   | LetRec -> "let rec"
@@ -1368,7 +1368,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
   let is_opaque = Option.is_none def.body in
-  let qualif = fun_decl_qualif_name qualif in
+  let qualif = fun_decl_qualif_keyword qualif in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   F.pp_print_space fmt ();
   (* Open a box for "(PARAMS) : EFFECT =" *)
@@ -1498,7 +1498,7 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Print "QUALIF NAME " *)
-  F.pp_print_string fmt (fun_decl_qualif_name qualif ^ " " ^ name);
+  F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name);
   F.pp_print_space  fmt ();
 
   (* Open ": TYPE =" box (depth=2) *)
@@ -1558,7 +1558,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   assert (List.length def.signature.type_params = 0);
   assert (not def.signature.info.effect_info.can_fail);
 
-  (* Add a break then the corresponding Rust definition *)
+  (* 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_space  fmt ();
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 5a623450..b1b8ccc2 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -58,6 +58,8 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
           method may_fail b =
             (* The fail flag is disabled for globals : the global body is
              * normalised into its declaration, which is always successful.
+             * (we check that it is successful in the extracted code: if it is
+             *  not, it leads to a type-checking error in the generated files)
              *)
             if f.is_global then () else
             can_fail := !can_fail || b
@@ -96,6 +98,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
             super#visit_Loop env loop
         end
       in
+      assert (not f.is_global || not use_state);
       (match f.body with
       | None ->
           (* Opaque function *)
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 04ad1b3c..4598895e 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -110,13 +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 typecheck_constant_value (ty : T.ety)
+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 *)
   log#ldebug
     (lazy
-      ("typecheck_constant_value:" ^ "\n- cv: "
+      ("constant_to_typed_value:" ^ "\n- cv: "
       ^ PV.constant_value_to_string cv));
   match (ty, cv) with
   (* Scalar, boolean... *)
@@ -175,7 +175,8 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
    fun cf ctx ->
     match op with
     | Expressions.Constant (ty, cv) ->
-        typecheck_constant_value ty cv |> ignore;
+        (* No need to reorganize the context *)
+        constant_to_typed_value ty cv |> ignore;
         cf ctx
     | Expressions.Copy p ->
         (* Access the value *)
@@ -203,7 +204,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
      ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | Expressions.Constant (ty, cv) -> cf (typecheck_constant_value ty cv) ctx
+  | Expressions.Constant (ty, cv) -> cf (constant_to_typed_value ty cv) ctx
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in