Fix minor issues for the translation of hashmap_on_disk

2 files changed, 60 insertions, 12 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 1f59075a..9d96d058 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1192,7 +1192,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)
-    (fwd_def : fun_decl) (def : fun_decl) : unit =
+    (has_state_param : bool) (fwd_def : fun_decl) (def : fun_decl) : unit =
   (* 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
@@ -1279,12 +1279,30 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
        * backward functions have no influence on termination: we thus
        * share the decrease clauses between the forward and the backward
        * functions).
+       * Something annoying is that there may be a state parameter, for
+       * the state-error monad, in which case we need to forget the input
+       * parameter before last:
+       * ```
+       * val f_fwd (x : u32) (st : state) :
+       *   Tot (result (state & u32)) (decreases (f_decreases x st))
+       *
+       *              We ignore this parameter
+       *                       VVV
+       * val f_back (x : u32) (ret : u32) (st : state) :
+       *   Tot (result (state & u32)) (decreases (f_decreases x st))
+       * ```
        * Rk.: if a function has a decreases clause, it is necessarily
        * a transparent function *)
       let inputs_lvs =
-        Collections.List.prefix
-          (List.length (Option.get fwd_def.body).inputs_lvs)
-          (Option.get def.body).inputs_lvs
+        let num_fwd_inputs = List.length (Option.get fwd_def.body).inputs_lvs in
+        let num_fwd_inputs =
+          if has_state_param then num_fwd_inputs - 1 else num_fwd_inputs
+        in
+        let all_inputs = (Option.get def.body).inputs_lvs in
+        let inputs = Collections.List.prefix num_fwd_inputs all_inputs in
+        if has_state_param then
+          inputs @ [ List.nth all_inputs (List.length all_inputs - 1) ]
+        else inputs
       in
       let _ =
         List.fold_left
diff --git a/src/Translate.ml b/src/Translate.ml
index 29f8f5ba..c29dd963 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -347,6 +347,7 @@ type gen_ctx = {
 (** Extraction context *)
 
 type gen_config = {
+  mp_config : Micro.config;
   extract_types : bool;
   extract_decreases_clauses : bool;
   extract_template_decreases_clauses : bool;
@@ -470,13 +471,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          let has_decr_clause =
            has_decreases_clause def && config.extract_decreases_clauses
          in
+         (* Is there an input parameter "visible" for the state used in
+          * the state error monad (if we use a state error monad)? *)
+         let has_state_param =
+           config.mp_config.use_state_monad
+           && config.mp_config.unfold_monadic_let_bindings
+         in
          (* Check if the definition needs to be filtered or not *)
          if
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
          then
            ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
-             has_decr_clause fwd_def def)
+             has_decr_clause has_state_param fwd_def def)
        fls);
     (* Insert unit tests if necessary *)
     if config.test_unit_functions then
@@ -579,7 +586,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   Format.pp_print_newline fmt ();
 
   (* Some logging *)
-  log#linfo (lazy ("Generated: " ^ filename))
+  log#linfo (lazy ("Generated: " ^ filename));
+
+  (* Flush and close the file *)
+  close_out out
 
 (** Translate a module and write the synthesized code to an output file.
     TODO: rename to translate_crate
@@ -665,6 +675,30 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
          trans_funs)
   in
 
+  (* Create the directory, if necessary *)
+  if not (Sys.file_exists dest_dir) then (
+    log#linfo (lazy ("Creating missing directory: " ^ dest_dir));
+    (* Create a directory with *default* permissions *)
+    Core.Unix.mkdir_p dest_dir);
+
+  (* Copy "Primitives.fst" - I couldn't find a "cp" function in the OCaml
+   * libraries... *)
+  let _ =
+    let src = open_in "fstar/Primitives.fst" in
+    let tgt_filename = Filename.concat dest_dir "Primitives.fst" in
+    let tgt = open_out tgt_filename in
+    try
+      while true do
+        (* We copy line by line *)
+        let line = input_line src in
+        Printf.fprintf tgt "%s\n" line
+      done
+    with End_of_file ->
+      close_in src;
+      close_out tgt;
+      log#linfo (lazy ("Copied: " ^ tgt_filename))
+  in
+
   (* Extract the file(s) *)
   let gen_ctx =
     {
@@ -676,18 +710,13 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     }
   in
 
-  (* Create the directory, if necessary *)
-  if not (Sys.file_exists dest_dir) then (
-    log#linfo (lazy ("Creating missing directory: " ^ dest_dir));
-    (* Create a directory with *default* permissions *)
-    Core.Unix.mkdir_p dest_dir);
-
   let use_state = config.mp_config.use_state_monad in
 
   (* Extract one or several files, depending on the configuration *)
   if config.split_files then (
     let base_gen_config =
       {
+        mp_config = config.mp_config;
         extract_types = false;
         extract_decreases_clauses = config.extract_decreases_clauses;
         extract_template_decreases_clauses = false;
@@ -776,6 +805,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   else
     let gen_config =
       {
+        mp_config = config.mp_config;
         extract_types = true;
         extract_decreases_clauses = config.extract_decreases_clauses;
         extract_template_decreases_clauses =