Implement ExtractToFStar.mk_name_formatter

2 files changed, 160 insertions, 54 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index e49e7e1a..cd6e7962 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -7,51 +7,155 @@ open PureToExtract
 open StringUtils
 module F = Format
 
-(*let mk_name_formatter =
-    let int_name (int_ty : integer_type)  =
-      match int_ty with
-      | Isize -> "isize"
-      | I8 -> "i8"
-      | I16 -> "i16"
-      | I32 -> "i32"
-      | I64 -> "i64"
-      | I128 -> "i128"
-      | Usize -> "usize"
-      | U8 -> "u8"
-      | U16 -> "u16"
-      | U32 -> "u32"
-      | U64 -> "u64"
-      | U128 -> "u128"
-    in
-    (* For now, we treat only the case where the type name is:
-     * `Module::Type`
-     * *)
-    let type_name name =
-      let name = Collections.List.pop_last name in
-      to_snake_case name
-    in
-    let field_name (def_name : name) (field_id : FieldId.id) (field_name : string option) : string =
-      let def_name = type_name def_name in
-      match field_name with
-      | Some field_name -> def_name ^ "_" ^ field_name
-      | None -> def_name ^ "_f" ^ FieldId.to_string field_id
-    in
-    let variant_name (def_name :name) (variant : string) : string =
-      type_name def_name ^ to_camel_case variant
-    in
-    {
-      bool_name : "bool";
-      char_name : "char";
-      int_name;
-      str_name : "string";
-      field_name;
-      variant_name;
-      type_name;
-      fun_name : A.fun_id -> name -> int -> region_group_info option -> string;
-      var_basename : StringSet.t -> ty -> string;
-      type_var_basename : StringSet.t -> string;
-      append_index : string -> int -> string;
-  }*)
+(**
+ * [ctx]: we use the context to lookup type definitions, to retrieve type names.
+ * This is used to compute variable names, when they have no basenames: in this
+ * case we use the first letter of the type name.
+ *
+ * [variant_concatenate_type_name]: if true, add the type name as a prefix
+ * to the variant names.
+ * Ex.:
+ * In Rust:
+ *   ```
+ *   enum List = {
+ *     Cons(u32, Box<List>),
+ *     Nil,
+ *   }
+ *   ```
+ *
+ * F*, if option activated:
+ *   ```
+ *   type list =
+ *   | ListCons : u32 -> list -> list
+ *   | ListNil : list
+ *   ```
+ *
+ * F*, if option not activated:
+ *   ```
+ *   type list =
+ *   | Cons : u32 -> list -> list
+ *   | Nil : list
+ *   ```
+ *
+ * Rk.: this should be true by default, because in Rust all the variant names
+ * are actively uniquely identifier by the type name `List::Cons(...)`, while
+ * in other languages it is not necessarily the case, and thus clashes can mess
+ * up type checking. Note that some languages actually forbids the name clashes
+ * (it is the case of F* ).
+ *)
+let mk_name_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
+  let int_name (int_ty : integer_type) =
+    match int_ty with
+    | Isize -> "isize"
+    | I8 -> "i8"
+    | I16 -> "i16"
+    | I32 -> "i32"
+    | I64 -> "i64"
+    | I128 -> "i128"
+    | Usize -> "usize"
+    | U8 -> "u8"
+    | U16 -> "u16"
+    | U32 -> "u32"
+    | U64 -> "u64"
+    | U128 -> "u128"
+  in
+  (* For now, we treat only the case where type and function names are of the
+   * form: `Module::Type` and `Module:function`.
+   *)
+  let get_name (name : name) : string =
+    match name with [ _module; name ] -> name | _ -> failwith "Unexpected"
+  in
+  let type_name_to_camel_case name =
+    let name = get_name name in
+    to_snake_case name
+  in
+  let type_name_to_snake_case name =
+    let name = get_name name in
+    to_snake_case name
+  in
+  let type_name name = type_name_to_camel_case name ^ "_t" in
+  let field_name (def_name : name) (field_id : FieldId.id)
+      (field_name : string option) : string =
+    let def_name = type_name_to_snake_case def_name ^ "_" in
+    match field_name with
+    | Some field_name -> def_name ^ "_" ^ field_name
+    | None -> def_name ^ FieldId.to_string field_id
+  in
+  let variant_name (def_name : name) (variant : string) : string =
+    let variant = to_camel_case variant in
+    if variant_concatenate_type_name then
+      type_name_to_camel_case def_name ^ variant
+    else variant
+  in
+  (* For now, we only treat the case where the type name is:
+   * `Module::Type`
+   *)
+  let fun_name (_fid : A.fun_id) (fname : name) (num_rgs : int)
+      (rg : region_group_info option) : string =
+    let fname = get_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
+    (* Compute the suffix *)
+    let suffix = default_fun_suffix num_rgs rg in
+    (* Concatenate *)
+    fname ^ suffix
+  in
+  let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
+      : string =
+    (* If there is a basename, we use it *)
+    match basename with
+    | Some basename ->
+        (* This should be a no-op *)
+        to_snake_case basename
+    | None -> (
+        (* No basename: we use the first letter of the type *)
+        match ty with
+        | Adt (type_id, tys) -> (
+            match type_id with
+            | Tuple ->
+                (* The "pair" case is frequent enough to have its special treatment *)
+                if List.length tys = 2 then "p" else "t"
+            | Assumed Result -> "r"
+            | AdtId adt_id ->
+                let def =
+                  TypeDefId.Map.find adt_id ctx.type_context.type_defs
+                in
+                StringUtils.string_of_chars [ (get_name def.name).[0] ])
+        | TypeVar _ -> "x" (* lacking imagination here... *)
+        | Bool -> "b"
+        | Char -> "c"
+        | Integer _ -> "i"
+        | Str -> "s"
+        | Array _ | Slice _ -> raise Unimplemented)
+  in
+  let type_var_basename (_varset : StringSet.t) (basename : string option) :
+      string =
+    (* If there is a basename, we use it *)
+    match basename with
+    | Some basename ->
+        (* This is *not* a no-op: type variables in Rust often start with
+         * a capital letter *)
+        to_snake_case basename
+    | None ->
+        (* For no, we use "a" *)
+        "a"
+  in
+  let append_index (basename : string) (i : int) : string =
+    basename ^ string_of_int i
+  in
+  {
+    bool_name = "bool";
+    char_name = "char";
+    int_name;
+    str_name = "string";
+    field_name;
+    variant_name;
+    type_name;
+    fun_name;
+    var_basename;
+    type_var_basename;
+    append_index;
+  }
 
 (** [inside] constrols whether we should add parentheses or not around type
     application (if `true` we add parentheses).
@@ -199,7 +303,7 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
     in
     (* Print the fields *)
     let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in
-    let ctx =
+    let _ =
       List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
     in
     (* Print the final type *)
@@ -220,8 +324,8 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the body box *)
   F.pp_close_box fmt ()
 
-let rec extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_def) : extraction_ctx =
+let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def)
+    : extraction_ctx =
   (* Compute and register the type def name *)
   let ctx, def_name = ctx_add_type_def def ctx in
   (* Compute and register:
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index a5619eae..d6e96d3d 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -62,11 +62,12 @@ type name_formatter = {
           - region group information in case of a backward function
             (`None` if forward function)
        *)
-  var_basename : StringSet.t -> ty -> string;
+  var_basename : StringSet.t -> string option -> ty -> string;
       (** Generates a variable basename.
       
           Inputs:
           - the set of names used in the context so far
+          - the basename we got from the symbolic execution, if we have one
           - the type of the variable (can be useful for heuristics, in order
             not to always use "x" for instance, whenever naming anonymous
             variables)
@@ -75,7 +76,7 @@ type name_formatter = {
           if necessary to prevent name clashes: the burden of name clashes checks
           is thus on the caller's side.
        *)
-  type_var_basename : StringSet.t -> string;
+  type_var_basename : StringSet.t -> string option -> string;
       (** Generates a type variable basename. *)
   append_index : string -> int -> string;
       (** Appends an index to a name - we use this to generate unique
@@ -104,16 +105,17 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
     : string =
   (* There are several cases:
      - [rg] is `Some`: this is a forward function:
-       - if there are no region groups (i.e., no backward functions) we don't
-         add any suffix
-       - if there are region gruops, we add "_fwd"
+       - we add "_fwd"
      - [rg] is `None`: this is a backward function:
        - this function has one region group: we add "_back"
        - this function has several backward function: we add "_back" and an
          additional suffix to identify the precise backward function
+     Note that we always add a suffix (in case there are no region groups,
+     we could not add the "_fwd" suffix) to prevent name clashes between
+     definitions (in particular between type and function definitions).
   *)
   match rg with
-  | None -> if num_region_groups = 0 then "" else "_fwd"
+  | None -> "_fwd"
   | Some rg ->
       assert (num_region_groups > 0);
       if num_region_groups = 1 then (* Exactly one backward function *)