Fix minor mistakes with regards to extraction of external declarations

5 files changed, 68 insertions, 45 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 2e0568c8..2389d444 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -213,26 +213,42 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
  * up type checking. Note that some languages actually forbids the name clashes
  * (it is the case of F* ).
  *)
-let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
-    formatter =
+let mk_formatter (ctx : trans_ctx) (crate_name : string)
+    (variant_concatenate_type_name : bool) : formatter =
   let int_name = fstar_int_name in
 
-  (* For now, we treat only the case where type names are of the
-   * form: `Module::Type`
+  (* Prepare a name.
+   * The first id elem is always the crate: if it is the local crate,
+   * we remove it.
+   * We also remove all the disambiguators which are 0, then convert
+   * everything to strings.
    *)
-  let get_type_name (name : name) : string =
+  let get_name (name : name) : string list =
+    let name = Names.filter_disambiguators_zero name in
     match name with
-    | [ Ident _module; Ident name ] -> name
+    | Ident crate :: name ->
+        let name = if crate = crate_name then name else Ident crate :: name in
+        let name =
+          List.map
+            (function
+              | Names.Ident s -> s
+              | Disambiguator d -> Names.Disambiguator.to_string d)
+            name
+        in
+        name
     | _ ->
         raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
   in
+  let get_type_name = get_name in
   let type_name_to_camel_case name =
     let name = get_type_name name in
-    to_camel_case name
+    let name = List.map to_camel_case name in
+    String.concat "" name
   in
   let type_name_to_snake_case name =
     let name = get_type_name name in
-    to_snake_case name
+    let name = List.map to_snake_case name in
+    String.concat "_" name
   in
   let type_name name = type_name_to_snake_case name ^ "_t" in
   let field_name (def_name : name) (field_id : FieldId.id)
@@ -252,25 +268,17 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
     let tname = type_name basename in
     "Mk" ^ tname
   in
-  (* For now, we treat only the case where function names are of the
-   * form:
-   * `module::function` (if top function)
-   * `module::Type::function` (for implementations)
-   *)
-  let get_fun_name (name : fun_name) : string =
-    match name with
-    | [ Ident _module_name; Ident name ] -> name
-    | [ Ident _module_name; Ident ty; Disambiguator _; Ident name ] ->
-        to_snake_case ty ^ "_" ^ name
-    | _ ->
-        raise
-          (Failure ("Unexpected name shape: " ^ Print.fun_name_to_string name))
+  let get_fun_name = get_name in
+  let fun_name_to_snake_case (fname : fun_name) : string =
+    let fname = get_fun_name fname in
+    (* Converting to snake case should be a no-op, but it doesn't cost much *)
+    let fname = List.map to_snake_case fname in
+    (* Concatenate the elements *)
+    String.concat "_" fname
   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 = get_fun_name fname in
-    (* Converting to snake case should be a no-op, but it doesn't cost much *)
-    let fname = to_snake_case fname in
+    let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
     let suffix = default_fun_suffix num_rgs rg filter_info in
     (* Concatenate *)
@@ -278,9 +286,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
   in
 
   let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string =
-    let fname = get_fun_name fname in
-    (* Converting to snake case should be a no-op, but it doesn't cost much *)
-    let fname = to_snake_case fname in
+    let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
     let suffix = "_decreases" in
     (* Concatenate *)
@@ -311,12 +317,11 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
                   TypeDeclId.Map.find adt_id ctx.type_context.type_decls
                 in
                 (* We do the following:
-                 * - convert to snake_case
+                 * - compute the type name converted_to_snake_case
                  * - take the first letter of every "letter group"
                  * Ex.: "TypeVar" -> "type_var" -> "tv"
                  *)
-                let cl = get_type_name def.name in
-                let cl = StringUtils.to_snake_case cl in
+                let cl = type_name_to_snake_case def.name in
                 let cl = String.split_on_char '_' cl in
                 let cl = List.filter (fun s -> String.length s > 0) cl in
                 assert (List.length cl > 0);
@@ -637,11 +642,16 @@ 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 is_opaque, qualif =
+  let is_opaque =
+    match def.kind with Struct _ | Enum _ -> false | Opaque -> true
+  in
+  let qualif =
     match qualif with
-    | Type -> (false, "type")
-    | And -> (false, "and")
-    | AssumeType -> (true, "assume type")
+    | Type -> "type"
+    | And -> "and"
+    | AssumeType ->
+        assert is_opaque;
+        "assume type"
   in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   (* Print the type parameters *)
@@ -1134,13 +1144,14 @@ 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 is_opaque, qualif =
+  let is_opaque = Option.is_none def.body in
+  let qualif =
     match qualif with
-    | Let -> (false, "let")
-    | LetRec -> (false, "let rec")
-    | And -> (false, "and")
-    | Val -> (true, "val")
-    | AssumeVal -> (true, "AssumeVal")
+    | Let -> "let"
+    | LetRec -> "let rec"
+    | And -> "and"
+    | Val -> "val"
+    | AssumeVal -> "AssumeVal"
   in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   F.pp_print_space fmt ();
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 93ba7696..19ffc279 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -178,6 +178,7 @@ let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result =
     | `Assoc [ ("Enum", variants) ] ->
         let* variants = list_of_json variant_of_json variants in
         Ok (T.Enum variants)
+    | `String "Opaque" -> Ok T.Opaque
     | _ -> Error "")
 
 let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
diff --git a/src/Names.ml b/src/Names.ml
index a8e6be59..41177c37 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -53,3 +53,10 @@ type module_name = name [@@deriving show, ord]
 type type_name = name [@@deriving show, ord]
 
 type fun_name = name [@@deriving show, ord]
+
+(** Filter the disambiguators equal to 0 in a name *)
+let filter_disambiguators_zero (n : name) : name =
+  let pred (pe : path_elem) : bool =
+    match pe with Ident _ -> true | Disambiguator d -> d <> Disambiguator.zero
+  in
+  List.filter pred n
diff --git a/src/OfJsonBasic.ml b/src/OfJsonBasic.ml
index 6e7bb4e9..9dbd521d 100644
--- a/src/OfJsonBasic.ml
+++ b/src/OfJsonBasic.ml
@@ -11,7 +11,7 @@ let ( let* ) o f = match o with Error e -> Error e | Ok x -> f x
 let combine_error_msgs js msg res : ('a, string) result =
   match res with
   | Ok x -> Ok x
-  | Error e -> Error (msg ^ " failed on: " ^ show js ^ "\n" ^ e)
+  | Error e -> Error ("[" ^ msg ^ "]" ^ " failed on: " ^ show js ^ "\n\n" ^ e)
 
 let bool_of_json (js : json) : (bool, string) result =
   match js with
diff --git a/src/Translate.ml b/src/Translate.ml
index 5812dc89..a440cacd 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -368,13 +368,17 @@ type gen_config = {
 (** Returns the pair: (has opaque type decls, has opaque fun decls) *)
 let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
   let has_opaque_types =
-    T.TypeDeclId.Map.exists
+    Pure.TypeDeclId.Map.exists
       (fun _ (d : Pure.type_decl) ->
         match d.kind with Opaque -> true | _ -> false)
       ctx.trans_types
   in
-  (* TODO: *)
-  let has_opaque_funs = false in
+  let has_opaque_funs =
+    Pure.FunDeclId.Map.exists
+      (fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) ->
+        Option.is_none t_fwd.body)
+      ctx.trans_funs
+  in
   (has_opaque_types, has_opaque_funs)
 
 (** A generic utility to generate the extracted definitions: as we may want to
@@ -560,7 +564,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   in
   let variant_concatenate_type_name = true in
   let fstar_fmt =
-    ExtractToFStar.mk_formatter trans_ctx variant_concatenate_type_name
+    ExtractToFStar.mk_formatter trans_ctx m.name variant_concatenate_type_name
   in
   let ctx =
     { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }