Fix issues with the builtin names

2 files changed, 88 insertions, 51 deletions

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 2c3c8106..f4f34155 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -24,7 +24,11 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
   g
 
 let split_on_separator (s : string) : string list =
-  Str.split (Str.regexp "::") s
+  Str.split (Str.regexp "\\(::\\|\\.\\)") s
+
+let () =
+  assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]);
+  assert (split_on_separator "x.y.z" = [ "x"; "y"; "z" ])
 
 (** Switch between two values depending on the target backend.
 
@@ -243,20 +247,24 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
   in
   [
     mk_fun "core::mem::replace" None None true false;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::new" None None false false;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::push" None
+    mk_fun "core::slice::{[@T]}::len"
+      (Some (backend_choice "slice::len" "Slice::len"))
+      None true false;
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"
+      (Some "alloc::vec::Vec::new") None false false;
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None
       (Some [ true; false ])
       true true;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" None
       (Some [ true; false ])
       true true;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::len" None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None
       (Some [ true; false ])
       true false;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index" None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index" None
       (Some [ true; true; false ])
       true false;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index_mut" None
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut" None
       (Some [ true; true; false ])
       true false;
     mk_fun "alloc::boxed::{Box<@T>}::deref" None
@@ -269,14 +277,19 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
     mk_fun "core::slice::index::{[@T]}::index_mut" None None true false;
     mk_fun "core::array::{[@T; @C]}::index" None None true false;
     mk_fun "core::array::{[@T; @C]}::index_mut" None None true false;
-    mk_fun "core::slice::index::{Range<@T>}::get" None None true false;
-    mk_fun "core::slice::index::{Range<@T>}::get_mut" None None true false;
-    mk_fun "core::slice::index::{Range<@T>}::index" None None true false;
-    mk_fun "core::slice::index::{Range<@T>}::index_mut" None None true false;
-    mk_fun "core::slice::index::{Range<@T>}::get_unchecked" None None false
-      false;
-    mk_fun "core::slice::index::{Range<@T>}::get_unchecked_mut" None None false
-      false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get"
+      (Some "core::slice::index::Range::get") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_mut"
+      (Some "core::slice::index::Range::get_mut") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index"
+      (Some "core::slice::index::Range::index") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index_mut"
+      (Some "core::slice::index::Range::index_mut") None true false;
+    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked"
+      (Some "core::slice::index::Range::get_unchecked") None false false;
+    mk_fun
+      "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked_mut"
+      (Some "core::slice::index::Range::get_unchecked_mut") None false false;
     mk_fun "core::slice::index::{usize}::get" None None true false;
     mk_fun "core::slice::index::{usize}::get_mut" None None true false;
     mk_fun "core::slice::index::{usize}::get_unchecked" None None false false;
@@ -330,9 +343,10 @@ let builtin_fun_effects =
   let int_funs = List.concat int_funs in
   let no_fail_no_state_funs =
     [
-      (* TODO: redundancy with the funs information below *)
-      "alloc::vec::{alloc::vec::Vec<@T>}::new";
-      "alloc::vec::{alloc::vec::Vec<@T>}::len";
+      (* TODO: redundancy with the funs information above *)
+      "core::slice::{[@T]}::len";
+      "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::len";
       "core::mem::replace";
       "core::mem::take";
     ]
@@ -345,11 +359,11 @@ let builtin_fun_effects =
   in
   let no_state_funs =
     [
-      (* TODO: redundancy with the funs information below *)
-      "alloc::vec::{alloc::vec::Vec<@T>}::push";
-      "alloc::vec::{alloc::vec::Vec<@T>}::index";
-      "alloc::vec::{alloc::vec::Vec<@T>}::index_mut";
-      "alloc::vec::{alloc::vec::Vec<@T>}::index_mut_back";
+      (* TODO: redundancy with the funs information above *)
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::push";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut";
+      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut_back";
     ]
   in
   let no_state_funs =
@@ -396,9 +410,13 @@ let builtin_trait_decls_info () =
     let types =
       let mk_type item_name =
         let type_name =
+          if !record_fields_short_names then item_name
+          else extract_name ^ "_" ^ item_name
+        in
+        let type_name =
           match !backend with
-          | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name
-          | Lean -> item_name
+          | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
+          | Lean -> type_name
         in
         let clauses = [] in
         (item_name, (type_name, clauses))
@@ -409,9 +427,8 @@ let builtin_trait_decls_info () =
       let mk_method (item_name, with_back) =
         (* TODO: factor out with builtin_funs_info *)
         let basename =
-          match !backend with
-          | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name
-          | Lean -> item_name
+          if !record_fields_short_names then item_name
+          else extract_name ^ "_" ^ item_name
         in
         let back_no_suffix = false in
         let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
@@ -442,8 +459,7 @@ let builtin_trait_decls_info () =
       ~methods:[ ("deref", true) ]
       ();
     (* DerefMut *)
-    mk_trait "core::ops::deref::DerefMut"
-      ~parent_clauses:[ backend_choice "deref_inst" "derefInst" ]
+    mk_trait "core::ops::deref::DerefMut" ~parent_clauses:[ "derefInst" ]
       ~methods:[ ("deref_mut", true) ]
       ();
     (* Index *)
@@ -451,15 +467,13 @@ let builtin_trait_decls_info () =
       ~methods:[ ("index", true) ]
       ();
     (* IndexMut *)
-    mk_trait "core::ops::index::IndexMut"
-      ~parent_clauses:[ backend_choice "index_inst" "indexInst" ]
+    mk_trait "core::ops::index::IndexMut" ~parent_clauses:[ "indexInst" ]
       ~methods:[ ("index_mut", true) ]
       ();
     (* Sealed *)
     mk_trait "core::slice::index::private_slice_index::Sealed" ();
     (* SliceIndex *)
-    mk_trait "core::slice::index::SliceIndex"
-      ~parent_clauses:[ backend_choice "sealed_inst" "sealedInst" ]
+    mk_trait "core::slice::index::SliceIndex" ~parent_clauses:[ "sealedInst" ]
       ~types:[ "Output" ]
       ~methods:
         [
@@ -482,43 +496,64 @@ let mk_builtin_trait_decls_map () =
 let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
 
 let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
-  let fmt (rust_name : string) ?(filter : bool list option = None) () :
+  let fmt (rust_name : string) ?(extract_name : string option = None)
+      ?(filter : bool list option = None) () :
       pattern * (bool list option * string) =
     let rust_name = parse_pattern rust_name in
     let name =
-      let name = pattern_to_trait_impl_extract_name rust_name in
       let sep = backend_choice "_" "." in
+      let name =
+        match extract_name with
+        | None -> pattern_to_trait_impl_extract_name rust_name
+        | Some name -> split_on_separator name
+      in
       String.concat sep name
     in
     (rust_name, (filter, name))
   in
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
-    fmt "core::ops::deref::Deref<Box<@T>>" ();
+    fmt "core::ops::deref::Deref<Box<@T>>"
+      ~extract_name:(Some "alloc::boxed::Box::coreopsDerefInst") ();
     (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
-    fmt "core::ops::deref::DerefMut<Box<@T>>" ();
+    fmt "core::ops::deref::DerefMut<Box<@T>>"
+      ~extract_name:(Some "alloc::boxed::Box::coreopsDerefMutInst") ();
     (* core::ops::index::Index<[T], I> *)
-    fmt "core::ops::index::Index<[@T], @I>" ();
+    fmt "core::ops::index::Index<[@T], @I>"
+      ~extract_name:(Some "core::ops::index::IndexSliceTIInst") ();
     (* core::ops::index::IndexMut<[T], I> *)
-    fmt "core::ops::index::IndexMut<[@T], @I>" ();
+    fmt "core::ops::index::IndexMut<[@T], @I>"
+      ~extract_name:(Some "core::ops::index::IndexMutSliceTIInst") ();
     (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
-    fmt "core::slice::index::private_slice_index::Sealed<Range<usize>>" ();
+    fmt
+      "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"
+      ~extract_name:
+        (Some "core.slice.index.private_slice_index.SealedRangeUsizeInst") ();
     (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
-    fmt "core::slice::index::SliceIndex<Range<usize>, [@T]>" ();
+    fmt "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T]>"
+      ~extract_name:(Some "core::slice::index::SliceIndexRangeUsizeSliceTInst")
+      ();
     (* core::ops::index::Index<[T; N], I> *)
-    fmt "core::ops::index::Index<[@T; @N], @I>" ();
+    fmt "core::ops::index::Index<[@T; @N], @I>"
+      ~extract_name:(Some "core::ops::index::IndexArrayInst") ();
     (* core::ops::index::IndexMut<[T; N], I> *)
-    fmt "core::ops::index::IndexMut<[@T; @N], @I>" ();
+    fmt "core::ops::index::IndexMut<[@T; @N], @I>"
+      ~extract_name:(Some "core::ops::index::IndexMutArrayIInst") ();
     (* core::slice::index::private_slice_index::Sealed<usize> *)
-    fmt "core::slice::index::private_slice_index::Sealed<usize>" ();
+    fmt "core::slice::index::private_slice_index::Sealed<usize>"
+      ~extract_name:
+        (Some "core::slice::index::private_slice_index::SealedUsizeInst") ();
     (* core::slice::index::SliceIndex<usize, [T]> *)
-    fmt "core::slice::index::SliceIndex<usize, [@T]>" ();
+    fmt "core::slice::index::SliceIndex<usize, [@T]>"
+      ~extract_name:(Some "core::slice::index::SliceIndexUsizeSliceTInst") ();
     (* core::ops::index::Index<alloc::vec::Vec<T>, T> *)
-    fmt "core::ops::index::Index<alloc::vec::Vec<@T>, @T>"
+    fmt "core::ops::index::Index<alloc::vec::Vec<@T, @A>, @T>"
+      ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexInst")
       ~filter:(Some [ true; true; false ])
       ();
     (* core::ops::index::IndexMut<alloc::vec::Vec<T>, T> *)
-    fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T>, @T>"
+    fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, @T>"
+      ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexMutInst")
       ~filter:(Some [ true; true; false ])
       ();
   ]
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 4f5ca0d1..6d50ed73 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -35,7 +35,7 @@ end
  *)
 let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
     string list =
-  let c = { tgt_kind = TkName } in
+  let c = { tgt = TkName } in
   let is_var (g : generic_arg) : bool =
     match g with
     | GExpr (EVar _) -> true
@@ -83,11 +83,13 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
    names we derive from the patterns (for the builtin definitions) are
    consistent with the extraction names we derive from the Rust names *)
 let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
-  pattern_to_extract_name false (name_to_pattern ctx n)
+  let c : to_pat_config = { tgt = TkName } in
+  pattern_to_extract_name false (name_to_pattern ctx c n)
 
 let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name)
     (p : Types.generic_params) (g : Types.generic_args) : string list =
-  pattern_to_extract_name true (name_with_generics_to_pattern ctx n p g)
+  let c : to_pat_config = { tgt = TkName } in
+  pattern_to_extract_name true (name_with_generics_to_pattern ctx c n p g)
 
 (*
   (* Prepare a name.