From df04dee24f1c83998aa314382f70e3961def8f10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Mar 2022 13:07:18 +0100
Subject: Finish updating Translate and ExtractToFStar

---
 src/ExtractToFStar.ml | 52 +++++++++++++++++++++++++++++++++------------------
 src/Translate.ml      |  5 ++---
 2 files changed, 36 insertions(+), 21 deletions(-)

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 1d144a40..6bbc21d7 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -637,7 +637,12 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "type TYPE_NAME" *)
-  let qualif = match qualif with Type -> "type" | And -> "and" in
+  let is_opaque, qualif =
+    match qualif with
+    | Type -> (false, "type")
+    | And -> (false, "and")
+    | AssumeType -> (true, "assume type")
+  in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   (* Print the type parameters *)
   if def.type_params <> [] then (
@@ -653,14 +658,18 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_space fmt ();
     F.pp_print_string fmt "Type0)");
   (* Print the "=" *)
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt "=";
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=");
   (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_close_box fmt ();
-  (match def.kind with
-  | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
-  | Enum variants ->
-      extract_type_decl_enum_body ctx_body fmt def def_name type_params variants);
+  (if not is_opaque then
+   match def.kind with
+   | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
+   | Enum variants ->
+       extract_type_decl_enum_body ctx_body fmt def def_name type_params
+         variants
+   | Opaque -> raise (Failure "Unreachable"));
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
@@ -1122,8 +1131,13 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
-  let qualif =
-    match qualif with Let -> "let" | LetRec -> "let rec" | And -> "and"
+  let is_opaque, qualif =
+    match qualif with
+    | Let -> (false, "let")
+    | LetRec -> (false, "let rec")
+    | And -> (false, "and")
+    | Val -> (true, "val")
+    | AssumeVal -> (true, "AssumeVal")
   in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   F.pp_print_space fmt ();
@@ -1198,19 +1212,21 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ()
   in
   (* Print the "=" *)
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt "=";
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=");
   (* Close the box for "(PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
   (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
-  F.pp_print_space fmt ();
-  (* Open a box for the body *)
-  F.pp_open_hvbox fmt 0;
-  (* Extract the body *)
-  let _ = extract_texpression ctx_body fmt false false def.body in
-  (* Close the box for the body *)
-  F.pp_close_box fmt ();
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    (* Open a box for the body *)
+    F.pp_open_hvbox fmt 0;
+    (* Extract the body *)
+    let _ = extract_texpression ctx_body fmt false false def.body in
+    (* Close the box for the body *)
+    F.pp_close_box fmt ());
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
diff --git a/src/Translate.ml b/src/Translate.ml
index 9b748461..7e4e6178 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -657,9 +657,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     (* Extract the opaque functions, if needed *)
     let opaque_funs_module =
       if has_opaque_funs then (
-        let opaque_filename =
-          extract_filebasename ^ ".Opaque" ^ types_filename_ext
-        in
+        let opaque_filename = extract_filebasename ^ ".Opaque.fsti" in
         let opaque_module = module_name ^ ".Opaque" in
         let opaque_config =
           {
@@ -667,6 +665,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
             extract_fun_decls = true;
             extract_transparent = false;
             extract_opaque = true;
+            interface = true;
           }
         in
         extract_file opaque_config gen_ctx opaque_filename m.M.name
-- 
cgit v1.2.3