Update the name definition to use path_elem

5 files changed, 114 insertions, 57 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 2bf7cd7c..6f53c302 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -247,22 +247,28 @@ let assumed_infos : assumed_info list =
   let vec_pre = [ "alloc"; "vec"; "Vec" ] in
   let index_pre = [ "core"; "ops"; "index" ] in
   [
-    (Replace, Sig.mem_replace_sig, false, [ "core"; "mem"; "replace" ]);
-    (BoxNew, Sig.box_new_sig, false, [ "alloc"; "boxed"; "Box"; "new" ]);
-    (BoxDeref, Sig.box_deref_shared_sig, false, deref_pre @ [ "Deref"; "deref" ]);
+    (A.Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]);
+    (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]);
+    ( BoxDeref,
+      Sig.box_deref_shared_sig,
+      false,
+      to_name (deref_pre @ [ "Deref"; "deref" ]) );
     ( BoxDerefMut,
       Sig.box_deref_mut_sig,
       false,
-      deref_pre @ [ "DerefMut"; "deref_mut" ] );
-    (VecNew, Sig.vec_new_sig, false, vec_pre @ [ "new" ]);
-    (VecPush, Sig.vec_push_sig, true, vec_pre @ [ "push" ]);
-    (VecInsert, Sig.vec_insert_sig, true, vec_pre @ [ "insert" ]);
-    (VecLen, Sig.vec_len_sig, false, vec_pre @ [ "len" ]);
-    (VecIndex, Sig.vec_index_shared_sig, true, index_pre @ [ "Index"; "index" ]);
+      to_name (deref_pre @ [ "DerefMut"; "deref_mut" ]) );
+    (VecNew, Sig.vec_new_sig, false, to_name (vec_pre @ [ "new" ]));
+    (VecPush, Sig.vec_push_sig, true, to_name (vec_pre @ [ "push" ]));
+    (VecInsert, Sig.vec_insert_sig, true, to_name (vec_pre @ [ "insert" ]));
+    (VecLen, Sig.vec_len_sig, false, to_name (vec_pre @ [ "len" ]));
+    ( VecIndex,
+      Sig.vec_index_shared_sig,
+      true,
+      to_name (index_pre @ [ "Index"; "index" ]) );
     ( VecIndexMut,
       Sig.vec_index_mut_sig,
       true,
-      index_pre @ [ "IndexMut"; "index_mut" ] );
+      to_name (index_pre @ [ "IndexMut"; "index_mut" ]) );
   ]
 
 let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
@@ -274,7 +280,7 @@ let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
 
 let get_assumed_name (id : A.assumed_fun_id) : fun_name =
   let _, _, _, name = get_assumed_info id in
-  Regular name
+  name
 
 let assumed_is_monadic (id : A.assumed_fun_id) : bool =
   let _, _, b, _ = get_assumed_info id in
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index d1108913..43ca1074 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -21,21 +21,22 @@ module A = CfimAst
 (* The default logger *)
 let log = Logging.cfim_of_json_logger
 
+let path_elem_of_json (js : json) : (path_elem, string) result =
+  combine_error_msgs js "path_elem_of_json"
+    (match js with
+    | `Assoc [ ("Ident", name) ] ->
+        let* name = string_of_json name in
+        Ok (Ident name)
+    | `Assoc [ ("Disambiguator", d) ] ->
+        let* d = Disambiguator.id_of_json d in
+        Ok (Disambiguator d)
+    | _ -> Error "")
+
 let name_of_json (js : json) : (name, string) result =
-  combine_error_msgs js "name_of_json" (list_of_json string_of_json js)
+  combine_error_msgs js "name_of_json" (list_of_json path_elem_of_json js)
 
 let fun_name_of_json (js : json) : (fun_name, string) result =
-  combine_error_msgs js "fun_name_of_json"
-    (match js with
-    | `Assoc [ ("Regular", name) ] ->
-        let* name = name_of_json name in
-        Ok (Regular name)
-    | `Assoc [ ("Impl", `List [ type_name; impl_id; ident ]) ] ->
-        let* type_name = name_of_json type_name in
-        let* impl_id = ImplId.id_of_json impl_id in
-        let* ident = string_of_json ident in
-        Ok (Impl (type_name, impl_id, ident))
-    | _ -> Error "")
+  combine_error_msgs js "fun_name_of_json" (name_of_json js)
 
 let type_var_of_json (js : json) : (T.type_var, string) result =
   combine_error_msgs js "type_var_of_json"
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index d8d14ddf..8bf02bd0 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -221,7 +221,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
    *)
   let get_type_name (name : name) : string =
     match name with
-    | [ _module; name ] -> name
+    | [ Ident _module; Ident name ] -> name
     | _ ->
         raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
   in
@@ -258,8 +258,9 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
    *)
   let get_fun_name (name : fun_name) : string =
     match name with
-    | Regular [ _module; name ] -> name
-    | Impl ([ _module; ty ], _, name) -> to_snake_case ty ^ "_" ^ name
+    | [ 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))
@@ -1098,8 +1099,8 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     it is useful for the decrease clause.
  *)
 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 =
+    (qualif : fun_decl_qualif) (has_decreases_clause : 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
diff --git a/src/Names.ml b/src/Names.ml
index fff98be9..054c84ad 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -1,39 +1,86 @@
 open Identifiers
 
-type name = string list [@@deriving show, ord]
+module Disambiguator = IdGen ()
+
+(** See the comments for [Name] *)
+type path_elem = Ident of string | Disambiguator of Disambiguator.id
+[@@deriving show, ord]
+
+type name = path_elem list [@@deriving show, ord]
 (** A name such as: `std::collections::vector` (which would be represented as
-    [["std"; "collections"; "vector"]]) *)
+    [[Ident "std"; Ident "collections"; Ident "vector"]])
+
 
-(* TODO: remove? *)
-module NameOrderedType : C.OrderedType with type t = name = struct
-  type t = name
+    A name really is a list of strings. However, we sometimes need to
+    introduce unique indices to disambiguate. This mostly happens because
+    of "impl" blocks in Rust:
+      ```
+      impl<T> List<T> {
+        ...
+      }
+      ```
+   
+    A type in Rust can have several "impl" blocks, and those blocks can
+    contain items with similar names. For this reason, we need to disambiguate
+    them with unique indices. Rustc calls those "disambiguators". In rustc, this
+    gives names like this:
+    - `betree_main::betree::NodeIdCounter{impl#0}::new`
+    - note that impl blocks can be nested, and macros sometimes generate
+      weird names (which require disambiguation):
+      `betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}`
+   
+    Finally, the paths used by rustc are a lot more precise and explicit than
+    those we expose in LLBC: for instance, every identifier belongs to a specific
+    namespace (value namespace, type namespace, etc.), and is coupled with a
+    disambiguator.
+   
+    On our side, we want to stay high-level and simple: we use string identifiers
+    as much as possible, insert disambiguators only when necessary (whenever
+    we find an "impl" block, typically) and check that the disambiguator is useless
+    in the other situations (i.e., the disambiguator is always equal to 0).
+   
+    Moreover, the items are uniquely disambiguated by their (integer) ids
+    (`TypeDeclId.id`, etc.), and when extracting the code we have to deal with
+    name clashes anyway. Still, we might want to be more precise in the future.
+   
+    Also note that the first path element in the name is always the crate name.
+ *)
 
-  let compare = compare_name
+let to_name (ls : string list) : name = List.map (fun s -> Ident s) ls
 
-  let to_string = String.concat "::"
+(*(* TODO: remove? *)
+  module NameOrderedType : C.OrderedType with type t = name = struct
+    type t = name
 
-  let pp_t = pp_name
+    let compare = compare_name
 
-  let show_t = show_name
-end
+    let to_string = String.concat "::"
 
-module NameMap = C.MakeMap (NameOrderedType)
-module NameSet = C.MakeSet (NameOrderedType)
+    let pp_t = pp_name
+
+    let show_t = show_name
+  end
+
+  module NameMap = C.MakeMap (NameOrderedType)
+  module NameSet = C.MakeSet (NameOrderedType)
+*)
 
 type module_name = name [@@deriving show, ord]
 
 type type_name = name [@@deriving show, ord]
 
-module ImplId = IdGen ()
+type fun_name = name [@@deriving show, ord]
 
-(** A function name *)
-type fun_name =
-  | Regular of name  (** "Regular" function name *)
-  | Impl of type_name * ImplId.id * string
-      (** The function comes from an "impl" block.
+(*module ImplId = IdGen ()
 
-          As we may have several "impl" blocks for one type, we need to use
-          a block id to disambiguate the functions (in rustc, this identifier
-          is called a "disambiguator").
-       *)
-[@@deriving show, ord]
+  (** A function name *)
+  type fun_name =
+    | Regular of name  (** "Regular" function name *)
+    | Impl of type_name * ImplId.id * string
+        (** The function comes from an "impl" block.
+
+            As we may have several "impl" blocks for one type, we need to use
+            a block id to disambiguate the functions (in rustc, this identifier
+            is called a "disambiguator").
+         *)
+  [@@deriving show, ord]*)
diff --git a/src/Print.ml b/src/Print.ml
index f8b8ff85..e03efd94 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -11,13 +11,15 @@ module M = Modules
 let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
   match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
 
-let name_to_string (name : name) : string = String.concat "::" name
+let path_elem_to_string (pe : path_elem) : string =
+  match pe with
+  | Ident s -> s
+  | Disambiguator d -> "{" ^ Disambiguator.to_string d ^ "}"
 
-let fun_name_to_string (name : fun_name) : string =
-  match name with
-  | Regular name -> name_to_string name
-  | Impl (type_name, impl_id, ident) ->
-      name_to_string type_name ^ "{" ^ ImplId.to_string impl_id ^ "}::" ^ ident
+let name_to_string (name : name) : string =
+  String.concat "::" (List.map path_elem_to_string name)
+
+let fun_name_to_string (name : fun_name) : string = name_to_string name
 
 (** Pretty-printing for types *)
 module Types = struct