From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 23 Oct 2023 13:47:39 +0200
Subject: Remove some assumed types and add more support for builtin
 definitions

---
 compiler/ExtractBuiltin.ml | 468 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 468 insertions(+)
 create mode 100644 compiler/ExtractBuiltin.ml

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
new file mode 100644
index 00000000..cf5cc70d
--- /dev/null
+++ b/compiler/ExtractBuiltin.ml
@@ -0,0 +1,468 @@
+(** This file declares external identifiers that we catch to map them to
+    definitions coming from the standard libraries in our backends. *)
+
+open Names
+open Config
+
+type simple_name = string list [@@deriving show, ord]
+
+let name_to_simple_name (s : name) : simple_name =
+  (* We simply ignore the disambiguators *)
+  List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
+
+(** Small helper which cuts a string at the occurrences of "::" *)
+let string_to_simple_name (s : string) : simple_name =
+  (* No function to split by using string separator?? *)
+  let name = String.split_on_char ':' s in
+  List.filter (fun s -> s <> "") name
+
+module SimpleNameOrd = struct
+  type t = simple_name
+
+  let compare = compare_simple_name
+  let to_string = show_simple_name
+  let pp_t = pp_simple_name
+  let show_t = show_simple_name
+end
+
+module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+
+(** Small utility to memoize some computations *)
+let mk_memoized (f : unit -> 'a) : unit -> 'a =
+  let r = ref None in
+  let g () =
+    match !r with
+    | Some x -> x
+    | None ->
+        let x = f () in
+        r := Some x;
+        x
+  in
+  g
+
+let builtin_globals : (string * string) list =
+  [
+    (* Min *)
+    ("core::num::usize::MIN", "core_usize_min");
+    ("core::num::u8::MIN", "core_u8_min");
+    ("core::num::u16::MIN", "core_u16_min");
+    ("core::num::u32::MIN", "core_u32_min");
+    ("core::num::u64::MIN", "core_u64_min");
+    ("core::num::u128::MIN", "core_u128_min");
+    ("core::num::isize::MIN", "core_isize_min");
+    ("core::num::i8::MIN", "core_i8_min");
+    ("core::num::i16::MIN", "core_i16_min");
+    ("core::num::i32::MIN", "core_i32_min");
+    ("core::num::i64::MIN", "core_i64_min");
+    ("core::num::i128::MIN", "core_i128_min");
+    (* Max *)
+    ("core::num::usize::MAX", "core_usize_max");
+    ("core::num::u8::MAX", "core_u8_max");
+    ("core::num::u16::MAX", "core_u16_max");
+    ("core::num::u32::MAX", "core_u32_max");
+    ("core::num::u64::MAX", "core_u64_max");
+    ("core::num::u128::MAX", "core_u128_max");
+    ("core::num::isize::MAX", "core_isize_max");
+    ("core::num::i8::MAX", "core_i8_max");
+    ("core::num::i16::MAX", "core_i16_max");
+    ("core::num::i32::MAX", "core_i32_max");
+    ("core::num::i64::MAX", "core_i64_max");
+    ("core::num::i128::MAX", "core_i128_max");
+  ]
+
+let builtin_globals_map : string SimpleNameMap.t =
+  SimpleNameMap.of_list
+    (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
+
+type builtin_variant_info = { fields : (string * string) list }
+
+type builtin_enum_variant_info = {
+  rust_variant_name : string;
+  extract_variant_name : string;
+  fields : string list option;
+}
+
+type builtin_type_body_info =
+  | Struct of string * string list
+    (* The constructor name and the map for the field names *)
+  | Enum of builtin_enum_variant_info list
+(* For every variant, a map for the field names *)
+
+type builtin_type_info = {
+  rust_name : string;
+  extract_name : string;
+  keep_params : bool list option;
+      (** We might want to filter some of the type parameters.
+
+          For instance, `Vec` type takes a type parameter for the allocator,
+          which we want to ignore.
+       *)
+  body_info : builtin_type_body_info option;
+}
+
+(** The assumed types.
+
+    The optional list of booleans is filtering information for the type
+    parameters. For instance, in the case of the `Vec` functions, there is
+    a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_types () : builtin_type_info list =
+  [
+    (* Alloc *)
+    {
+      rust_name = "alloc::alloc::Global";
+      extract_name =
+        (match !backend with
+        | Lean -> "AllocGlobal"
+        | Coq | FStar | HOL4 -> "alloc_global");
+      keep_params = None;
+      body_info = None;
+    };
+    (* Vec *)
+    {
+      rust_name = "alloc::vec::Vec";
+      extract_name =
+        (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec");
+      keep_params = Some [ true; false ];
+      body_info = None;
+    };
+    (* Option *)
+    {
+      rust_name = "core::option::Option";
+      extract_name =
+        (match !backend with
+        | Lean -> "Option"
+        | Coq | FStar | HOL4 -> "option");
+      keep_params = None;
+      body_info =
+        Some
+          (Enum
+             [
+               {
+                 rust_variant_name = "None";
+                 extract_variant_name =
+                   (match !backend with
+                   | FStar | Coq -> "None"
+                   | Lean -> "none"
+                   | HOL4 -> "NONE");
+                 fields = None;
+               };
+               {
+                 rust_variant_name = "Some";
+                 extract_variant_name =
+                   (match !backend with
+                   | FStar | Coq -> "Some"
+                   | Lean -> "some"
+                   | HOL4 -> "SOME");
+                 fields = None;
+               };
+             ]);
+    };
+    (* Range *)
+    {
+      rust_name = "core::ops::range::Range";
+      extract_name =
+        (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range");
+      keep_params = None;
+      body_info =
+        Some
+          (Struct
+             ( (match !backend with
+               | Lean -> "Range.mk"
+               | Coq | HOL4 -> "mk_range"
+               | FStar -> "Mkrange"),
+               [ "start"; "end_" ] ));
+    };
+  ]
+
+let mk_builtin_types_map () =
+  SimpleNameMap.of_list
+    (List.map
+       (fun info -> (string_to_simple_name info.rust_name, info))
+       (builtin_types ()))
+
+let builtin_types_map = mk_memoized mk_builtin_types_map
+
+type builtin_fun_info = {
+  rg : Types.RegionGroupId.id option;
+  extract_name : string;
+}
+
+(** The assumed functions.
+
+    The optional list of booleans is filtering information for the type
+    parameters. For instance, in the case of the `Vec` functions, there is
+    a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
+  let rg0 = Some Types.RegionGroupId.zero in
+  [
+    ( "core::mem::replace",
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "mem_replace_fwd"
+            | Lean -> "mem.replace");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "mem_replace_back"
+            | Lean -> "mem.replace_back");
+        };
+      ] );
+    ( "alloc::vec::Vec::new",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_new"
+            | Lean -> "Vec.new");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_new_back"
+            | Lean -> "Vec.new_back");
+        };
+      ] );
+    ( "alloc::vec::Vec::push",
+      Some [ true; false ],
+      [
+        (* The forward function shouldn't be used *)
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_push_fwd"
+            | Lean -> "Vec.push_fwd");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_push_back"
+            | Lean -> "Vec.push");
+        };
+      ] );
+    ( "alloc::vec::Vec::insert",
+      Some [ true; false ],
+      [
+        (* The forward function shouldn't be used *)
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_insert_fwd"
+            | Lean -> "Vec.insert_fwd");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_insert_back"
+            | Lean -> "Vec.insert");
+        };
+      ] );
+    ( "alloc::vec::Vec::len",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_len"
+            | Lean -> "Vec.len");
+        };
+      ] );
+    ( "alloc::vec::Vec::index",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_fwd"
+            | Lean -> "Vec.index_shared");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_back"
+            | Lean -> "Vec.index_shared_back");
+        };
+      ] );
+    ( "alloc::vec::Vec::index_mut",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_mut_fwd"
+            | Lean -> "Vec.index_mut");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_mut_back"
+            | Lean -> "Vec.index_mut_back");
+        };
+      ] );
+  ]
+
+let mk_builtin_funs_map () =
+  SimpleNameMap.of_list
+    (List.map
+       (fun (name, filter, info) ->
+         (string_to_simple_name name, (filter, info)))
+       (builtin_funs ()))
+
+let builtin_funs_map () = mk_memoized mk_builtin_funs_map
+
+type builtin_trait_info = {
+  rust_name : string;
+  extract_name : string;
+  parent_clauses : string list;
+  consts : (string * string) list;
+  types : (string * string * string list) list;
+      (** Every type has:
+          - a Rust name
+          - an extraction name
+          - a list of clauses *)
+  funs : (string * Types.RegionGroupId.id option * string) list;
+}
+
+let builtin_traits () =
+  let rg0 = Some Types.RegionGroupId.zero in
+  [
+    {
+      (* Deref *)
+      rust_name = "core::ops::deref::Deref";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_deref_Deref"
+        | Lean -> "core.ops.deref.Deref");
+      parent_clauses = [];
+      consts = [];
+      types =
+        [
+          ( "Target",
+            (match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
+            | Lean -> "Target"),
+            [] );
+        ];
+      funs =
+        [
+          ( "deref",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
+            | Lean -> "deref" );
+        ];
+    };
+    {
+      (* DerefMut *)
+      rust_name = "core::ops::deref::DerefMut";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut"
+        | Lean -> "core.ops.deref.DerefMut");
+      parent_clauses =
+        [
+          (match !backend with
+          | Coq | FStar | HOL4 -> "deref_inst"
+          | Lean -> "DerefInst");
+        ];
+      consts = [];
+      types = [];
+      funs =
+        [
+          ( "deref_mut",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
+            | Lean -> "deref_mut" );
+          ( "deref_mut",
+            rg0,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
+            | Lean -> "deref_mut_back" );
+        ];
+    };
+    {
+      (* Index *)
+      rust_name = "core::ops::index::Index";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_index_Index"
+        | Lean -> "core.ops.index.Index");
+      parent_clauses = [];
+      consts = [];
+      types =
+        [
+          ( "Output",
+            (match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
+            | Lean -> "Output"),
+            [] );
+        ];
+      funs =
+        [
+          ( "index",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
+            | Lean -> "index" );
+        ];
+    };
+    {
+      (* IndexMut *)
+      rust_name = "core::ops::index::IndexMut";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_index_IndexMut"
+        | Lean -> "core.ops.index.IndexMut");
+      parent_clauses =
+        [
+          (match !backend with
+          | Coq | FStar | HOL4 -> "index_inst"
+          | Lean -> "IndexInst");
+        ];
+      consts = [];
+      types = [];
+      funs =
+        [
+          ( "index_mut",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
+            | Lean -> "index_mut" );
+          ( "index_mut",
+            rg0,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
+            | Lean -> "index_mut_back" );
+        ];
+    };
+  ]
+
+let mk_builtin_traits_map () =
+  SimpleNameMap.of_list
+    (List.map
+       (fun info -> (string_to_simple_name info.rust_name, info))
+       (builtin_traits ()))
+
+let builtin_traits_map () = mk_memoized mk_builtin_traits_map
-- 
cgit v1.2.3


From c486bd0675f489c5ac917749a68e2c71b55041ae Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 23 Oct 2023 17:29:15 +0200
Subject: Make progress on handling the builtins

---
 compiler/ExtractBuiltin.ml | 93 +++++++++++++++++++++++++---------------------
 1 file changed, 51 insertions(+), 42 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index cf5cc70d..3b4afff6 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -1,5 +1,8 @@
 (** This file declares external identifiers that we catch to map them to
-    definitions coming from the standard libraries in our backends. *)
+    definitions coming from the standard libraries in our backends.
+
+    TODO: there misses trait **implementations**
+ *)
 
 open Names
 open Config
@@ -331,20 +334,20 @@ let mk_builtin_funs_map () =
 
 let builtin_funs_map () = mk_memoized mk_builtin_funs_map
 
-type builtin_trait_info = {
+type builtin_trait_decl_info = {
   rust_name : string;
   extract_name : string;
   parent_clauses : string list;
   consts : (string * string) list;
-  types : (string * string * string list) list;
+  types : (string * (string * string list)) list;
       (** Every type has:
           - a Rust name
           - an extraction name
           - a list of clauses *)
-  funs : (string * Types.RegionGroupId.id option * string) list;
+  funs : (string * (Types.RegionGroupId.id option * string) list) list;
 }
 
-let builtin_traits () =
+let builtin_trait_decls_info () =
   let rg0 = Some Types.RegionGroupId.zero in
   [
     {
@@ -359,18 +362,20 @@ let builtin_traits () =
       types =
         [
           ( "Target",
-            (match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
-            | Lean -> "Target"),
-            [] );
+            ( (match !backend with
+              | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
+              | Lean -> "Target"),
+              [] ) );
         ];
       funs =
         [
           ( "deref",
-            None,
-            match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
-            | Lean -> "deref" );
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
+                | Lean -> "deref" );
+            ] );
         ];
     };
     {
@@ -391,15 +396,16 @@ let builtin_traits () =
       funs =
         [
           ( "deref_mut",
-            None,
-            match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
-            | Lean -> "deref_mut" );
-          ( "deref_mut",
-            rg0,
-            match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
-            | Lean -> "deref_mut_back" );
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
+                | Lean -> "deref_mut" );
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
+                | Lean -> "deref_mut_back" );
+            ] );
         ];
     };
     {
@@ -414,18 +420,20 @@ let builtin_traits () =
       types =
         [
           ( "Output",
-            (match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
-            | Lean -> "Output"),
-            [] );
+            ( (match !backend with
+              | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
+              | Lean -> "Output"),
+              [] ) );
         ];
       funs =
         [
           ( "index",
-            None,
-            match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
-            | Lean -> "index" );
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
+                | Lean -> "index" );
+            ] );
         ];
     };
     {
@@ -446,23 +454,24 @@ let builtin_traits () =
       funs =
         [
           ( "index_mut",
-            None,
-            match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
-            | Lean -> "index_mut" );
-          ( "index_mut",
-            rg0,
-            match !backend with
-            | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
-            | Lean -> "index_mut_back" );
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
+                | Lean -> "index_mut" );
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
+                | Lean -> "index_mut_back" );
+            ] );
         ];
     };
   ]
 
-let mk_builtin_traits_map () =
+let mk_builtin_trait_decls_map () =
   SimpleNameMap.of_list
     (List.map
        (fun info -> (string_to_simple_name info.rust_name, info))
-       (builtin_traits ()))
+       (builtin_trait_decls_info ()))
 
-let builtin_traits_map () = mk_memoized mk_builtin_traits_map
+let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
-- 
cgit v1.2.3


From 63107911c16a9991f7d5cf8c6df621318a03ca3b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 14:32:38 +0200
Subject: Fix various issues with the builtins

---
 compiler/ExtractBuiltin.ml | 82 +++++++++++++++++++++++++++++++++++-----------
 1 file changed, 62 insertions(+), 20 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 3b4afff6..0d591028 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -78,21 +78,24 @@ let builtin_globals_map : string SimpleNameMap.t =
     (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
 
 type builtin_variant_info = { fields : (string * string) list }
+[@@deriving show]
 
 type builtin_enum_variant_info = {
   rust_variant_name : string;
   extract_variant_name : string;
   fields : string list option;
 }
+[@@deriving show]
 
 type builtin_type_body_info =
   | Struct of string * string list
     (* The constructor name and the map for the field names *)
   | Enum of builtin_enum_variant_info list
 (* For every variant, a map for the field names *)
+[@@deriving show]
 
 type builtin_type_info = {
-  rust_name : string;
+  rust_name : string list;
   extract_name : string;
   keep_params : bool list option;
       (** We might want to filter some of the type parameters.
@@ -102,6 +105,7 @@ type builtin_type_info = {
        *)
   body_info : builtin_type_body_info option;
 }
+[@@deriving show]
 
 (** The assumed types.
 
@@ -113,7 +117,7 @@ let builtin_types () : builtin_type_info list =
   [
     (* Alloc *)
     {
-      rust_name = "alloc::alloc::Global";
+      rust_name = [ "alloc"; "alloc"; "Global" ];
       extract_name =
         (match !backend with
         | Lean -> "AllocGlobal"
@@ -123,7 +127,7 @@ let builtin_types () : builtin_type_info list =
     };
     (* Vec *)
     {
-      rust_name = "alloc::vec::Vec";
+      rust_name = [ "alloc"; "vec"; "Vec" ];
       extract_name =
         (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec");
       keep_params = Some [ true; false ];
@@ -131,7 +135,7 @@ let builtin_types () : builtin_type_info list =
     };
     (* Option *)
     {
-      rust_name = "core::option::Option";
+      rust_name = [ "core"; "option"; "Option" ];
       extract_name =
         (match !backend with
         | Lean -> "Option"
@@ -163,7 +167,7 @@ let builtin_types () : builtin_type_info list =
     };
     (* Range *)
     {
-      rust_name = "core::ops::range::Range";
+      rust_name = [ "core"; "ops"; "range"; "Range" ];
       extract_name =
         (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range");
       keep_params = None;
@@ -180,9 +184,7 @@ let builtin_types () : builtin_type_info list =
 
 let mk_builtin_types_map () =
   SimpleNameMap.of_list
-    (List.map
-       (fun info -> (string_to_simple_name info.rust_name, info))
-       (builtin_types ()))
+    (List.map (fun info -> (info.rust_name, info)) (builtin_types ()))
 
 let builtin_types_map = mk_memoized mk_builtin_types_map
 
@@ -190,6 +192,7 @@ type builtin_fun_info = {
   rg : Types.RegionGroupId.id option;
   extract_name : string;
 }
+[@@deriving show]
 
 (** The assumed functions.
 
@@ -197,10 +200,12 @@ type builtin_fun_info = {
     parameters. For instance, in the case of the `Vec` functions, there is
     a type parameter for the allocator to use, which we want to filter.
  *)
-let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
+let builtin_funs () :
+    (string list * bool list option * builtin_fun_info list) list =
   let rg0 = Some Types.RegionGroupId.zero in
+  (* TODO: fix the names below *)
   [
-    ( "core::mem::replace",
+    ( [ "core::mem::replace" ],
       None,
       [
         {
@@ -218,7 +223,7 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "mem.replace_back");
         };
       ] );
-    ( "alloc::vec::Vec::new",
+    ( [ "alloc::vec::Vec::new" ],
       Some [ true; false ],
       [
         {
@@ -236,7 +241,7 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "Vec.new_back");
         };
       ] );
-    ( "alloc::vec::Vec::push",
+    ( [ "alloc::vec::Vec::push" ],
       Some [ true; false ],
       [
         (* The forward function shouldn't be used *)
@@ -255,7 +260,7 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "Vec.push");
         };
       ] );
-    ( "alloc::vec::Vec::insert",
+    ( [ "alloc::vec::Vec::insert" ],
       Some [ true; false ],
       [
         (* The forward function shouldn't be used *)
@@ -274,7 +279,7 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "Vec.insert");
         };
       ] );
-    ( "alloc::vec::Vec::len",
+    ( [ "alloc::vec::Vec::len" ],
       Some [ true; false ],
       [
         {
@@ -285,7 +290,7 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "Vec.len");
         };
       ] );
-    ( "alloc::vec::Vec::index",
+    ( [ "alloc::vec::Vec::index" ],
       Some [ true; false ],
       [
         {
@@ -304,7 +309,7 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "Vec.index_shared_back");
         };
       ] );
-    ( "alloc::vec::Vec::index_mut",
+    ( [ "alloc::vec::Vec::index_mut" ],
       Some [ true; false ],
       [
         {
@@ -323,16 +328,52 @@ let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
             | Lean -> "Vec.index_mut_back");
         };
       ] );
+    ( [ "alloc"; "boxed"; "Box"; "deref" ],
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref"
+            | Lean -> "alloc.boxed.Box.deref");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back"
+            | Lean -> "alloc.boxed.Box.deref_back");
+        };
+      ] );
+    ( [ "alloc"; "boxed"; "Box"; "deref_mut" ],
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut"
+            | Lean -> "alloc.boxed.Box.deref_mut");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut_back"
+            | Lean -> "alloc.boxed.Box.deref_mut_back");
+        };
+      ] );
   ]
 
 let mk_builtin_funs_map () =
   SimpleNameMap.of_list
     (List.map
-       (fun (name, filter, info) ->
-         (string_to_simple_name name, (filter, info)))
+       (fun (name, filter, info) -> (name, (filter, info)))
        (builtin_funs ()))
 
-let builtin_funs_map () = mk_memoized mk_builtin_funs_map
+let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
 type builtin_trait_decl_info = {
   rust_name : string;
@@ -346,6 +387,7 @@ type builtin_trait_decl_info = {
           - a list of clauses *)
   funs : (string * (Types.RegionGroupId.id option * string) list) list;
 }
+[@@deriving show]
 
 let builtin_trait_decls_info () =
   let rg0 = Some Types.RegionGroupId.zero in
@@ -389,7 +431,7 @@ let builtin_trait_decls_info () =
         [
           (match !backend with
           | Coq | FStar | HOL4 -> "deref_inst"
-          | Lean -> "DerefInst");
+          | Lean -> "derefInst");
         ];
       consts = [];
       types = [];
-- 
cgit v1.2.3


From be70eed487b507dc002660a4c891397003165e75 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:01:55 +0200
Subject: Add support for builtin trait implementations

---
 compiler/ExtractBuiltin.ml | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 0d591028..d3cea54e 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -517,3 +517,37 @@ let mk_builtin_trait_decls_map () =
        (builtin_trait_decls_info ()))
 
 let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
+
+(* TODO: generalize this.
+
+   For now, the key is:
+   - name of the impl (ex.: "alloc.boxed.Boxed")
+   - name of the implemented trait (ex.: "core.ops.deref.Deref"
+*)
+type simple_name_pair = simple_name * simple_name [@@deriving show, ord]
+
+module SimpleNamePairOrd = struct
+  type t = simple_name_pair
+
+  let compare = compare_simple_name_pair
+  let to_string = show_simple_name_pair
+  let pp_t = pp_simple_name_pair
+  let show_t = show_simple_name_pair
+end
+
+module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
+
+let builtin_trait_impls_info () : ((string list * string list) * string) list =
+  [
+    (* core::ops::Deref<alloc::boxed::Box<T>> *)
+    ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
+      "alloc.boxed.Box.coreOpsDerefInst" );
+    (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
+    ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
+      "alloc.boxed.Box.coreOpsDerefMutInst" );
+  ]
+
+let mk_builtin_trait_impls_map () =
+  SimpleNamePairMap.of_list (builtin_trait_impls_info ())
+
+let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map
-- 
cgit v1.2.3


From 9ddd174959970f87658191034b70d0cfa02ff451 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:49:54 +0200
Subject: Filter some type arguments for the builtin types/functions

---
 compiler/ExtractBuiltin.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index d3cea54e..65c18efd 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -203,9 +203,8 @@ type builtin_fun_info = {
 let builtin_funs () :
     (string list * bool list option * builtin_fun_info list) list =
   let rg0 = Some Types.RegionGroupId.zero in
-  (* TODO: fix the names below *)
   [
-    ( [ "core::mem::replace" ],
+    ( [ "core"; "mem"; "replace" ],
       None,
       [
         {
@@ -223,7 +222,7 @@ let builtin_funs () :
             | Lean -> "mem.replace_back");
         };
       ] );
-    ( [ "alloc::vec::Vec::new" ],
+    ( [ "alloc"; "vec"; "Vec"; "new" ],
       Some [ true; false ],
       [
         {
@@ -241,7 +240,7 @@ let builtin_funs () :
             | Lean -> "Vec.new_back");
         };
       ] );
-    ( [ "alloc::vec::Vec::push" ],
+    ( [ "alloc"; "vec"; "Vec"; "push" ],
       Some [ true; false ],
       [
         (* The forward function shouldn't be used *)
@@ -260,7 +259,7 @@ let builtin_funs () :
             | Lean -> "Vec.push");
         };
       ] );
-    ( [ "alloc::vec::Vec::insert" ],
+    ( [ "alloc"; "vec"; "Vec"; "insert" ],
       Some [ true; false ],
       [
         (* The forward function shouldn't be used *)
@@ -279,7 +278,7 @@ let builtin_funs () :
             | Lean -> "Vec.insert");
         };
       ] );
-    ( [ "alloc::vec::Vec::len" ],
+    ( [ "alloc"; "vec"; "Vec"; "len" ],
       Some [ true; false ],
       [
         {
@@ -290,7 +289,7 @@ let builtin_funs () :
             | Lean -> "Vec.len");
         };
       ] );
-    ( [ "alloc::vec::Vec::index" ],
+    ( [ "alloc"; "vec"; "Vec"; "index" ],
       Some [ true; false ],
       [
         {
@@ -309,7 +308,7 @@ let builtin_funs () :
             | Lean -> "Vec.index_shared_back");
         };
       ] );
-    ( [ "alloc::vec::Vec::index_mut" ],
+    ( [ "alloc"; "vec"; "Vec"; "index_mut" ],
       Some [ true; false ],
       [
         {
-- 
cgit v1.2.3


From fb4fe9ec2c00f15a745ee12357e4a8f929a4dfc0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 16:43:00 +0200
Subject: Fix minor issues

---
 compiler/ExtractBuiltin.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 65c18efd..2e46b120 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -211,15 +211,15 @@ let builtin_funs () :
           rg = None;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "mem_replace_fwd"
-            | Lean -> "mem.replace");
+            | FStar | Coq | HOL4 -> "core_mem_replace_fwd"
+            | Lean -> "core.mem.replace");
         };
         {
           rg = rg0;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "mem_replace_back"
-            | Lean -> "mem.replace_back");
+            | FStar | Coq | HOL4 -> "core_mem_replace_back"
+            | Lean -> "core.mem.replace_back");
         };
       ] );
     ( [ "alloc"; "vec"; "Vec"; "new" ],
-- 
cgit v1.2.3


From 6eebc66e34561bc6985b5866d49c8314a6fbaee9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 17:47:39 +0200
Subject: Start taking into account non-fallible functions like
 core::mem::replace

---
 compiler/ExtractBuiltin.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 2e46b120..9cc7c226 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -29,6 +29,7 @@ module SimpleNameOrd = struct
 end
 
 module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+module SimpleNameSet = Collections.MakeSet (SimpleNameOrd)
 
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
@@ -374,6 +375,13 @@ let mk_builtin_funs_map () =
 
 let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
+let builtin_non_fallible_funs =
+  [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ]
+
+let builtin_non_fallible_funs_set =
+  SimpleNameSet.of_list
+    (List.map string_to_simple_name builtin_non_fallible_funs)
+
 type builtin_trait_decl_info = {
   rust_name : string;
   extract_name : string;
-- 
cgit v1.2.3


From 9c230dddebb171ee1b3e0176838441163836b875 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 18:16:53 +0200
Subject: Handle properly the builtin, non fallible functions

---
 compiler/ExtractBuiltin.ml | 34 +++++++++++++++++++++++++++++++++-
 1 file changed, 33 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 9cc7c226..4c6fe014 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -376,7 +376,39 @@ let mk_builtin_funs_map () =
 let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
 let builtin_non_fallible_funs =
-  [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ]
+  let int_names =
+    [
+      "usize";
+      "u8";
+      "u16";
+      "u32";
+      "u64";
+      "u128";
+      "isize";
+      "i8";
+      "i16";
+      "i32";
+      "i64";
+      "i128";
+    ]
+  in
+  let int_ops =
+    [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ]
+  in
+  let int_funs =
+    List.map
+      (fun int_name ->
+        List.map (fun op -> "core::num::" ^ int_name ^ "::" ^ op) int_ops)
+      int_names
+  in
+  let int_funs = List.concat int_funs in
+  [
+    "alloc::boxed::Box::deref";
+    "alloc::boxed::Box::deref_mut";
+    "core::mem::replace";
+    "core::mem::take";
+  ]
+  @ int_funs
 
 let builtin_non_fallible_funs_set =
   SimpleNameSet.of_list
-- 
cgit v1.2.3


From e3cb3646bbe3d50240aa0bf4763f8e816fb9a706 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 15:36:06 +0200
Subject: Fix some issues at extraction and add builtins

---
 compiler/ExtractBuiltin.ml | 304 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 299 insertions(+), 5 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 4c6fe014..c781463e 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -121,7 +121,7 @@ let builtin_types () : builtin_type_info list =
       rust_name = [ "alloc"; "alloc"; "Global" ];
       extract_name =
         (match !backend with
-        | Lean -> "AllocGlobal"
+        | Lean -> "alloc.alloc.Global"
         | Coq | FStar | HOL4 -> "alloc_global");
       keep_params = None;
       body_info = None;
@@ -335,7 +335,7 @@ let builtin_funs () :
           rg = None;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref"
+            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref"
             | Lean -> "alloc.boxed.Box.deref");
         };
         (* The backward function shouldn't be used *)
@@ -343,7 +343,7 @@ let builtin_funs () :
           rg = rg0;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back"
+            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_back"
             | Lean -> "alloc.boxed.Box.deref_back");
         };
       ] );
@@ -354,7 +354,7 @@ let builtin_funs () :
           rg = None;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut"
+            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_mut"
             | Lean -> "alloc.boxed.Box.deref_mut");
         };
         {
@@ -365,6 +365,179 @@ let builtin_funs () :
             | Lean -> "alloc.boxed.Box.deref_mut_back");
         };
       ] );
+    (* TODO: fix the same like "[T]" below *)
+    ( [ "core"; "slice"; "index"; "[T]"; "index" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index"
+            | Lean -> "core.slice.index.Slice.index");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_back"
+            | Lean -> "core.slice.index.Slice.index_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "[T]"; "index_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut"
+            | Lean -> "core.slice.index.Slice.index_mut");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut_back"
+            | Lean -> "core.slice.index.Slice.index_mut_back");
+        };
+      ] );
+    ( [ "core"; "array"; "[T; N]"; "index" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index"
+            | Lean -> "core.array.Array.index");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index_back"
+            | Lean -> "core.array.Array.index_back");
+        };
+      ] );
+    ( [ "core"; "array"; "[T; N]"; "index_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index_mut"
+            | Lean -> "core.array.Array.index_mut");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index_mut_back"
+            | Lean -> "core.array.Array.index_mut_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get"
+            | Lean -> "core.slice.index.Range.get");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_back"
+            | Lean -> "core.slice.index.Range.get_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut"
+            | Lean -> "core.slice.index.Range.get_mut");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut_back"
+            | Lean -> "core.slice.index.Range.get_mut_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "index" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index"
+            | Lean -> "core.slice.index.Range.index");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_back"
+            | Lean -> "core.slice.index.Range.index_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "index_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut"
+            | Lean -> "core.slice.index.Range.index_mut");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut_back"
+            | Lean -> "core.slice.index.Range.index_mut_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get_unchecked" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked"
+            | Lean -> "core.slice.index.Range.get_unchecked");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked_mut"
+            | Lean -> "core.slice.index.Range.get_unchecked_mut");
+        };
+      ] );
   ]
 
 let mk_builtin_funs_map () =
@@ -528,7 +701,7 @@ let builtin_trait_decls_info () =
         [
           (match !backend with
           | Coq | FStar | HOL4 -> "index_inst"
-          | Lean -> "IndexInst");
+          | Lean -> "indexInst");
         ];
       consts = [];
       types = [];
@@ -547,6 +720,104 @@ let builtin_trait_decls_info () =
             ] );
         ];
     };
+    {
+      (* Sealed *)
+      rust_name = "core::slice::index::private_slice_index::Sealed";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_slice_index_sealed"
+        | Lean -> "core.slice.index.private_slice_index.Sealed");
+      parent_clauses = [];
+      consts = [];
+      types = [];
+      funs = [];
+    };
+    {
+      (* SliceIndex *)
+      rust_name = "core::slice::index::SliceIndex";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_SliceIndex"
+        | Lean -> "core.slice.index.SliceIndex");
+      parent_clauses =
+        [
+          (match !backend with
+          | Coq | FStar | HOL4 -> "sealed_inst"
+          | Lean -> "sealedInst");
+        ];
+      consts = [];
+      types =
+        [
+          ( "Output",
+            ( (match !backend with
+              | Coq | FStar | HOL4 -> "core_SliceIndex_Output"
+              | Lean -> "Output"),
+              [] ) );
+        ];
+      funs =
+        [
+          ( "get",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get"
+                | Lean -> "get" );
+              (* The backward function shouldn't be used *)
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_back"
+                | Lean -> "get_back" );
+            ] );
+          ( "get_mut",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut"
+                | Lean -> "get_mut" );
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut_back"
+                | Lean -> "get_mut_back" );
+            ] );
+          ( "get_unchecked",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked"
+                | Lean -> "get_unchecked" );
+            ] );
+          ( "get_unchecked_mut",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked_mut"
+                | Lean -> "get_unchecked_mut" );
+            ] );
+          ( "index",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index"
+                | Lean -> "index" );
+              (* The backward function shouldn't be used *)
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index_back"
+                | Lean -> "index_back" );
+            ] );
+          ( "index_mut",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut"
+                | Lean -> "index_mut" );
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut_back"
+                | Lean -> "index_mut_back" );
+            ] );
+        ];
+    };
   ]
 
 let mk_builtin_trait_decls_map () =
@@ -577,6 +848,7 @@ end
 module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
 
 let builtin_trait_impls_info () : ((string list * string list) * string) list =
+  (* TODO: fix the names like "[T]" below *)
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
     ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
@@ -584,6 +856,28 @@ let builtin_trait_impls_info () : ((string list * string list) * string) list =
     (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
     ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
       "alloc.boxed.Box.coreOpsDerefMutInst" );
+    (* core::ops::index::Index<[T], I> *)
+    ( ([ "core"; "slice"; "index"; "[T]" ], [ "core"; "ops"; "index"; "Index" ]),
+      "core.slice.index.Slice.coreopsindexIndexInst" );
+    (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
+    ( ( [ "core"; "slice"; "index"; "private_slice_index"; "Range" ],
+        [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ),
+      "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst"
+    );
+    (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
+    ( ( [ "core"; "slice"; "index"; "Range" ],
+        [ "core"; "slice"; "index"; "SliceIndex" ] ),
+      "core.slice.index.Range.coresliceindexSliceIndexInst" );
+    (* core::ops::index::IndexMut<[T], I> *)
+    ( ( [ "core"; "slice"; "index"; "[T]" ],
+        [ "core"; "ops"; "index"; "IndexMut" ] ),
+      "core.slice.index.Slice.coreopsindexIndexMutInst" );
+    (* core::ops::index::Index<[T; N], I> *)
+    ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "Index" ]),
+      "core.array.Array.coreopsindexIndexInst" );
+    (* core::ops::index::IndexMut<[T; N], I> *)
+    ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "IndexMut" ]),
+      "core.array.Array.coreopsindexIndexMutInst" );
   ]
 
 let mk_builtin_trait_impls_map () =
-- 
cgit v1.2.3


From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 18:44:28 +0200
Subject: Make the hashmap files typecheck again in Lean

---
 compiler/ExtractBuiltin.ml | 509 +++++++++++++++------------------------------
 1 file changed, 162 insertions(+), 347 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index c781463e..fa873c6a 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -122,7 +122,7 @@ let builtin_types () : builtin_type_info list =
       extract_name =
         (match !backend with
         | Lean -> "alloc.alloc.Global"
-        | Coq | FStar | HOL4 -> "alloc_global");
+        | Coq | FStar | HOL4 -> "alloc_alloc_Global");
       keep_params = None;
       body_info = None;
     };
@@ -130,7 +130,9 @@ let builtin_types () : builtin_type_info list =
     {
       rust_name = [ "alloc"; "vec"; "Vec" ];
       extract_name =
-        (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec");
+        (match !backend with
+        | Lean -> "alloc.vec.Vec"
+        | Coq | FStar | HOL4 -> "alloc_vec_Vec");
       keep_params = Some [ true; false ];
       body_info = None;
     };
@@ -170,15 +172,17 @@ let builtin_types () : builtin_type_info list =
     {
       rust_name = [ "core"; "ops"; "range"; "Range" ];
       extract_name =
-        (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range");
+        (match !backend with
+        | Lean -> "core.ops.range.Range"
+        | Coq | FStar | HOL4 -> "core_ops_range_Range");
       keep_params = None;
       body_info =
         Some
           (Struct
              ( (match !backend with
-               | Lean -> "Range.mk"
-               | Coq | HOL4 -> "mk_range"
-               | FStar -> "Mkrange"),
+               | Lean -> "core.ops.range.Range.mk"
+               | Coq | HOL4 -> "mk_core_ops_range_Range"
+               | FStar -> "Mkcore_ops_range_Range"),
                [ "start"; "end_" ] ));
     };
   ]
@@ -204,340 +208,118 @@ type builtin_fun_info = {
 let builtin_funs () :
     (string list * bool list option * builtin_fun_info list) list =
   let rg0 = Some Types.RegionGroupId.zero in
+  (* Small utility *)
+  let mk_fun (name : string list) (extract_name : string list option)
+      (filter : bool list option) (with_back : bool) (back_no_suffix : bool) :
+      string list * bool list option * builtin_fun_info list =
+    let extract_name =
+      match extract_name with None -> name | Some name -> name
+    in
+    let fwd_name =
+      match !backend with
+      | FStar | Coq | HOL4 -> String.concat "_" extract_name
+      | Lean -> String.concat "." extract_name
+    in
+    let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
+    let fwd = [ { rg = None; extract_name = fwd_name ^ fwd_suffix } ] in
+    let back_suffix = if with_back && back_no_suffix then "" else "_back" in
+    let back =
+      if with_back then [ { rg = rg0; extract_name = fwd_name ^ back_suffix } ]
+      else []
+    in
+    (name, filter, fwd @ back)
+  in
   [
-    ( [ "core"; "mem"; "replace" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_mem_replace_fwd"
-            | Lean -> "core.mem.replace");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_mem_replace_back"
-            | Lean -> "core.mem.replace_back");
-        };
-      ] );
-    ( [ "alloc"; "vec"; "Vec"; "new" ],
-      Some [ true; false ],
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_new"
-            | Lean -> "Vec.new");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_new_back"
-            | Lean -> "Vec.new_back");
-        };
-      ] );
-    ( [ "alloc"; "vec"; "Vec"; "push" ],
-      Some [ true; false ],
-      [
-        (* The forward function shouldn't be used *)
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_push_fwd"
-            | Lean -> "Vec.push_fwd");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_push_back"
-            | Lean -> "Vec.push");
-        };
-      ] );
-    ( [ "alloc"; "vec"; "Vec"; "insert" ],
-      Some [ true; false ],
-      [
-        (* The forward function shouldn't be used *)
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_insert_fwd"
-            | Lean -> "Vec.insert_fwd");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_insert_back"
-            | Lean -> "Vec.insert");
-        };
-      ] );
-    ( [ "alloc"; "vec"; "Vec"; "len" ],
-      Some [ true; false ],
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_len"
-            | Lean -> "Vec.len");
-        };
-      ] );
-    ( [ "alloc"; "vec"; "Vec"; "index" ],
-      Some [ true; false ],
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_index_fwd"
-            | Lean -> "Vec.index_shared");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_index_back"
-            | Lean -> "Vec.index_shared_back");
-        };
-      ] );
-    ( [ "alloc"; "vec"; "Vec"; "index_mut" ],
-      Some [ true; false ],
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_index_mut_fwd"
-            | Lean -> "Vec.index_mut");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "vec_index_mut_back"
-            | Lean -> "Vec.index_mut_back");
-        };
-      ] );
-    ( [ "alloc"; "boxed"; "Box"; "deref" ],
-      Some [ true; false ],
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref"
-            | Lean -> "alloc.boxed.Box.deref");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_back"
-            | Lean -> "alloc.boxed.Box.deref_back");
-        };
-      ] );
-    ( [ "alloc"; "boxed"; "Box"; "deref_mut" ],
-      Some [ true; false ],
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_mut"
-            | Lean -> "alloc.boxed.Box.deref_mut");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut_back"
-            | Lean -> "alloc.boxed.Box.deref_mut_back");
-        };
-      ] );
+    mk_fun [ "core"; "mem"; "replace" ] None None true false;
+    mk_fun [ "alloc"; "vec"; "Vec"; "new" ] None None false false;
+    mk_fun
+      [ "alloc"; "vec"; "Vec"; "push" ]
+      None
+      (Some [ true; false ])
+      true true;
+    mk_fun
+      [ "alloc"; "vec"; "Vec"; "insert" ]
+      None
+      (Some [ true; false ])
+      true true;
+    mk_fun
+      [ "alloc"; "vec"; "Vec"; "len" ]
+      None
+      (Some [ true; false ])
+      true false;
+    mk_fun
+      [ "alloc"; "vec"; "Vec"; "index" ]
+      None
+      (Some [ true; true; false ])
+      true false;
+    mk_fun
+      [ "alloc"; "vec"; "Vec"; "index_mut" ]
+      None
+      (Some [ true; true; false ])
+      true false;
+    mk_fun
+      [ "alloc"; "boxed"; "Box"; "deref" ]
+      None
+      (Some [ true; false ])
+      true false;
+    mk_fun
+      [ "alloc"; "boxed"; "Box"; "deref_mut" ]
+      None
+      (Some [ true; false ])
+      true false;
     (* TODO: fix the same like "[T]" below *)
-    ( [ "core"; "slice"; "index"; "[T]"; "index" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index"
-            | Lean -> "core.slice.index.Slice.index");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_back"
-            | Lean -> "core.slice.index.Slice.index_back");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "[T]"; "index_mut" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut"
-            | Lean -> "core.slice.index.Slice.index_mut");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut_back"
-            | Lean -> "core.slice.index.Slice.index_mut_back");
-        };
-      ] );
-    ( [ "core"; "array"; "[T; N]"; "index" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_array_Array_index"
-            | Lean -> "core.array.Array.index");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_array_Array_index_back"
-            | Lean -> "core.array.Array.index_back");
-        };
-      ] );
-    ( [ "core"; "array"; "[T; N]"; "index_mut" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_array_Array_index_mut"
-            | Lean -> "core.array.Array.index_mut");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_array_Array_index_mut_back"
-            | Lean -> "core.array.Array.index_mut_back");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "Range"; "get" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_get"
-            | Lean -> "core.slice.index.Range.get");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_back"
-            | Lean -> "core.slice.index.Range.get_back");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "Range"; "get_mut" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut"
-            | Lean -> "core.slice.index.Range.get_mut");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut_back"
-            | Lean -> "core.slice.index.Range.get_mut_back");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "Range"; "index" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_index"
-            | Lean -> "core.slice.index.Range.index");
-        };
-        (* The backward function shouldn't be used *)
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_back"
-            | Lean -> "core.slice.index.Range.index_back");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "Range"; "index_mut" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut"
-            | Lean -> "core.slice.index.Range.index_mut");
-        };
-        {
-          rg = rg0;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut_back"
-            | Lean -> "core.slice.index.Range.index_mut_back");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "Range"; "get_unchecked" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked"
-            | Lean -> "core.slice.index.Range.get_unchecked");
-        };
-      ] );
-    ( [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ],
-      None,
-      [
-        {
-          rg = None;
-          extract_name =
-            (match !backend with
-            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked_mut"
-            | Lean -> "core.slice.index.Range.get_unchecked_mut");
-        };
-      ] );
+    mk_fun
+      [ "core"; "slice"; "index"; "[T]"; "index" ]
+      (Some [ "core"; "slice"; "index"; "Slice"; "index" ])
+      None true false;
+    mk_fun
+      [ "core"; "slice"; "index"; "[T]"; "index_mut" ]
+      (Some [ "core"; "slice"; "index"; "Slice"; "index_mut" ])
+      None true false;
+    mk_fun
+      [ "core"; "array"; "[T; N]"; "index" ]
+      (Some [ "core"; "array"; "Array"; "index" ])
+      None true false;
+    mk_fun
+      [ "core"; "array"; "[T; N]"; "index_mut" ]
+      (Some [ "core"; "array"; "Array"; "index_mut" ])
+      None true false;
+    mk_fun [ "core"; "slice"; "index"; "Range"; "get" ] None None true false;
+    mk_fun [ "core"; "slice"; "index"; "Range"; "get_mut" ] None None true false;
+    mk_fun [ "core"; "slice"; "index"; "Range"; "index" ] None None true false;
+    mk_fun
+      [ "core"; "slice"; "index"; "Range"; "index_mut" ]
+      None None true false;
+    mk_fun
+      [ "core"; "slice"; "index"; "Range"; "get_unchecked" ]
+      None None false false;
+    mk_fun
+      [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ]
+      None None false false;
+    mk_fun
+      [ "core"; "slice"; "index"; "usize"; "get" ]
+      (Some [ "core"; "slice"; "index"; "Usize"; "get" ])
+      None true false;
+    mk_fun
+      [ "core"; "slice"; "index"; "usize"; "get_mut" ]
+      (Some [ "core"; "slice"; "index"; "Usize"; "get_mut" ])
+      None true false;
+    mk_fun
+      [ "core"; "slice"; "index"; "usize"; "get_unchecked" ]
+      (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked" ])
+      None false false;
+    mk_fun
+      [ "core"; "slice"; "index"; "usize"; "get_unchecked_mut" ]
+      (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked_mut" ])
+      None false false;
+    mk_fun
+      [ "core"; "slice"; "index"; "usize"; "index" ]
+      (Some [ "core"; "slice"; "index"; "Usize"; "index" ])
+      None true false;
+    mk_fun
+      [ "core"; "slice"; "index"; "usize"; "index_mut" ]
+      (Some [ "core"; "slice"; "index"; "Usize"; "index_mut" ])
+      None true false;
   ]
 
 let mk_builtin_funs_map () =
@@ -576,6 +358,8 @@ let builtin_non_fallible_funs =
   in
   let int_funs = List.concat int_funs in
   [
+    "alloc::vec::Vec::new";
+    "alloc::vec::Vec::len";
     "alloc::boxed::Box::deref";
     "alloc::boxed::Box::deref_mut";
     "core::mem::replace";
@@ -847,37 +631,68 @@ end
 
 module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
 
-let builtin_trait_impls_info () : ((string list * string list) * string) list =
+let builtin_trait_impls_info () :
+    ((string list * string list) * (bool list option * string)) list =
+  let fmt ?(filter : bool list option = None) (name : string) :
+      bool list option * string =
+    let name =
+      match !backend with
+      | Lean -> name
+      | FStar | Coq | HOL4 ->
+          let name = String.split_on_char '.' name in
+          String.concat "_" name
+    in
+    (filter, name)
+  in
   (* TODO: fix the names like "[T]" below *)
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
     ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
-      "alloc.boxed.Box.coreOpsDerefInst" );
+      fmt "alloc.boxed.Box.coreOpsDerefInst" );
     (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
     ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
-      "alloc.boxed.Box.coreOpsDerefMutInst" );
+      fmt "alloc.boxed.Box.coreOpsDerefMutInst" );
     (* core::ops::index::Index<[T], I> *)
     ( ([ "core"; "slice"; "index"; "[T]" ], [ "core"; "ops"; "index"; "Index" ]),
-      "core.slice.index.Slice.coreopsindexIndexInst" );
+      fmt "core.slice.index.Slice.coreopsindexIndexInst" );
     (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
     ( ( [ "core"; "slice"; "index"; "private_slice_index"; "Range" ],
         [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ),
-      "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst"
+      fmt
+        "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst"
     );
     (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
     ( ( [ "core"; "slice"; "index"; "Range" ],
         [ "core"; "slice"; "index"; "SliceIndex" ] ),
-      "core.slice.index.Range.coresliceindexSliceIndexInst" );
+      fmt "core.slice.index.Range.coresliceindexSliceIndexInst" );
     (* core::ops::index::IndexMut<[T], I> *)
     ( ( [ "core"; "slice"; "index"; "[T]" ],
         [ "core"; "ops"; "index"; "IndexMut" ] ),
-      "core.slice.index.Slice.coreopsindexIndexMutInst" );
+      fmt "core.slice.index.Slice.coreopsindexIndexMutInst" );
     (* core::ops::index::Index<[T; N], I> *)
     ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "Index" ]),
-      "core.array.Array.coreopsindexIndexInst" );
+      fmt "core.array.Array.coreopsindexIndexInst" );
     (* core::ops::index::IndexMut<[T; N], I> *)
     ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "IndexMut" ]),
-      "core.array.Array.coreopsindexIndexMutInst" );
+      fmt "core.array.Array.coreopsindexIndexMutInst" );
+    (* core::slice::index::private_slice_index::Sealed<usize> *)
+    ( ( [ "core"; "slice"; "index"; "private_slice_index"; "usize" ],
+        [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ),
+      fmt
+        "core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst"
+    );
+    (* core::slice::index::SliceIndex<usize, [T]> *)
+    ( ( [ "core"; "slice"; "index"; "usize" ],
+        [ "core"; "slice"; "index"; "SliceIndex" ] ),
+      fmt "core.slice.index.usize.coresliceindexSliceIndexInst" );
+    (* core::ops::index::Index<Vec<T>, T> *)
+    ( ([ "alloc"; "vec"; "Vec" ], [ "core"; "ops"; "index"; "Index" ]),
+      let filter = Some [ true; true; false ] in
+      fmt ~filter "alloc.vec.Vec.coreopsindexIndexInst" );
+    (* core::ops::index::IndexMut<Vec<T>, T> *)
+    ( ([ "alloc"; "vec"; "Vec" ], [ "core"; "ops"; "index"; "IndexMut" ]),
+      let filter = Some [ true; true; false ] in
+      fmt ~filter "alloc.vec.Vec.coreopsindexIndexMutInst" );
   ]
 
 let mk_builtin_trait_impls_map () =
-- 
cgit v1.2.3


From 4a164d24f1ecfb04ada3881e200cb9be16e611dc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 11:03:39 +0200
Subject: Fix more issues at extraction and factor out defs in ExtractBuiltin

---
 compiler/ExtractBuiltin.ml | 403 ++++++++++++++++-----------------------------
 1 file changed, 143 insertions(+), 260 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index fa873c6a..510de583 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -44,6 +44,14 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
   in
   g
 
+(** Switch between two values depending on the target backend.
+
+    We often compute the same value (typically: a name) if the target
+    is F*, Coq or HOL4, and a different value if the target is Lean.
+ *)
+let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
+  match !backend with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
+
 let builtin_globals : (string * string) list =
   [
     (* Min *)
@@ -215,16 +223,16 @@ let builtin_funs () :
     let extract_name =
       match extract_name with None -> name | Some name -> name
     in
-    let fwd_name =
+    let basename =
       match !backend with
       | FStar | Coq | HOL4 -> String.concat "_" extract_name
       | Lean -> String.concat "." extract_name
     in
     let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
-    let fwd = [ { rg = None; extract_name = fwd_name ^ fwd_suffix } ] in
+    let fwd = [ { rg = None; extract_name = basename ^ fwd_suffix } ] in
     let back_suffix = if with_back && back_no_suffix then "" else "_back" in
     let back =
-      if with_back then [ { rg = rg0; extract_name = fwd_name ^ back_suffix } ]
+      if with_back then [ { rg = rg0; extract_name = basename ^ back_suffix } ]
       else []
     in
     (name, filter, fwd @ back)
@@ -381,227 +389,102 @@ type builtin_trait_decl_info = {
           - a Rust name
           - an extraction name
           - a list of clauses *)
-  funs : (string * (Types.RegionGroupId.id option * string) list) list;
+  methods : (string * builtin_fun_info list) list;
 }
 [@@deriving show]
 
 let builtin_trait_decls_info () =
   let rg0 = Some Types.RegionGroupId.zero in
+  let mk_trait (rust_name : string list) ?(extract_name : string option = None)
+      ?(parent_clauses : string list = []) ?(types : string list = [])
+      ?(methods : (string * bool) list = []) () : builtin_trait_decl_info =
+    let extract_name =
+      match extract_name with
+      | Some n -> n
+      | None -> (
+          match !backend with
+          | Coq | FStar | HOL4 -> String.concat "_" rust_name
+          | Lean -> String.concat "." rust_name)
+    in
+    let consts = [] in
+    let types =
+      let mk_type item_name =
+        let type_name =
+          match !backend with
+          | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name
+          | Lean -> item_name
+        in
+        let clauses = [] in
+        (item_name, (type_name, clauses))
+      in
+      List.map mk_type types
+    in
+    let methods =
+      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
+        in
+        let back_no_suffix = false in
+        let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
+        let fwd = [ { rg = None; extract_name = basename ^ fwd_suffix } ] in
+        let back_suffix = if with_back && back_no_suffix then "" else "_back" in
+        let back =
+          if with_back then
+            [ { rg = rg0; extract_name = basename ^ back_suffix } ]
+          else []
+        in
+        (item_name, fwd @ back)
+      in
+      List.map mk_method methods
+    in
+    let rust_name = String.concat "::" rust_name in
+    { rust_name; extract_name; parent_clauses; consts; types; methods }
+  in
   [
-    {
-      (* Deref *)
-      rust_name = "core::ops::deref::Deref";
-      extract_name =
-        (match !backend with
-        | Coq | FStar | HOL4 -> "core_ops_deref_Deref"
-        | Lean -> "core.ops.deref.Deref");
-      parent_clauses = [];
-      consts = [];
-      types =
+    (* Deref *)
+    mk_trait
+      [ "core"; "ops"; "deref"; "Deref" ]
+      ~types:[ "Target" ]
+      ~methods:[ ("deref", true) ]
+      ();
+    (* DerefMut *)
+    mk_trait
+      [ "core"; "ops"; "deref"; "DerefMut" ]
+      ~parent_clauses:[ backend_choice "deref_inst" "derefInst" ]
+      ~methods:[ ("deref_mut", true) ]
+      ();
+    (* Index *)
+    mk_trait
+      [ "core"; "ops"; "index"; "Index" ]
+      ~types:[ "Output" ]
+      ~methods:[ ("index", true) ]
+      ();
+    (* IndexMut *)
+    mk_trait
+      [ "core"; "ops"; "index"; "IndexMut" ]
+      ~parent_clauses:[ backend_choice "index_inst" "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" ]
+      ~types:[ "Output" ]
+      ~methods:
         [
-          ( "Target",
-            ( (match !backend with
-              | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
-              | Lean -> "Target"),
-              [] ) );
-        ];
-      funs =
-        [
-          ( "deref",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
-                | Lean -> "deref" );
-            ] );
-        ];
-    };
-    {
-      (* DerefMut *)
-      rust_name = "core::ops::deref::DerefMut";
-      extract_name =
-        (match !backend with
-        | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut"
-        | Lean -> "core.ops.deref.DerefMut");
-      parent_clauses =
-        [
-          (match !backend with
-          | Coq | FStar | HOL4 -> "deref_inst"
-          | Lean -> "derefInst");
-        ];
-      consts = [];
-      types = [];
-      funs =
-        [
-          ( "deref_mut",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
-                | Lean -> "deref_mut" );
-              ( rg0,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
-                | Lean -> "deref_mut_back" );
-            ] );
-        ];
-    };
-    {
-      (* Index *)
-      rust_name = "core::ops::index::Index";
-      extract_name =
-        (match !backend with
-        | Coq | FStar | HOL4 -> "core_ops_index_Index"
-        | Lean -> "core.ops.index.Index");
-      parent_clauses = [];
-      consts = [];
-      types =
-        [
-          ( "Output",
-            ( (match !backend with
-              | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
-              | Lean -> "Output"),
-              [] ) );
-        ];
-      funs =
-        [
-          ( "index",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
-                | Lean -> "index" );
-            ] );
-        ];
-    };
-    {
-      (* IndexMut *)
-      rust_name = "core::ops::index::IndexMut";
-      extract_name =
-        (match !backend with
-        | Coq | FStar | HOL4 -> "core_ops_index_IndexMut"
-        | Lean -> "core.ops.index.IndexMut");
-      parent_clauses =
-        [
-          (match !backend with
-          | Coq | FStar | HOL4 -> "index_inst"
-          | Lean -> "indexInst");
-        ];
-      consts = [];
-      types = [];
-      funs =
-        [
-          ( "index_mut",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
-                | Lean -> "index_mut" );
-              ( rg0,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
-                | Lean -> "index_mut_back" );
-            ] );
-        ];
-    };
-    {
-      (* Sealed *)
-      rust_name = "core::slice::index::private_slice_index::Sealed";
-      extract_name =
-        (match !backend with
-        | Coq | FStar | HOL4 -> "core_slice_index_sealed"
-        | Lean -> "core.slice.index.private_slice_index.Sealed");
-      parent_clauses = [];
-      consts = [];
-      types = [];
-      funs = [];
-    };
-    {
-      (* SliceIndex *)
-      rust_name = "core::slice::index::SliceIndex";
-      extract_name =
-        (match !backend with
-        | Coq | FStar | HOL4 -> "core_SliceIndex"
-        | Lean -> "core.slice.index.SliceIndex");
-      parent_clauses =
-        [
-          (match !backend with
-          | Coq | FStar | HOL4 -> "sealed_inst"
-          | Lean -> "sealedInst");
-        ];
-      consts = [];
-      types =
-        [
-          ( "Output",
-            ( (match !backend with
-              | Coq | FStar | HOL4 -> "core_SliceIndex_Output"
-              | Lean -> "Output"),
-              [] ) );
-        ];
-      funs =
-        [
-          ( "get",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_get"
-                | Lean -> "get" );
-              (* The backward function shouldn't be used *)
-              ( rg0,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_get_back"
-                | Lean -> "get_back" );
-            ] );
-          ( "get_mut",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut"
-                | Lean -> "get_mut" );
-              ( rg0,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut_back"
-                | Lean -> "get_mut_back" );
-            ] );
-          ( "get_unchecked",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked"
-                | Lean -> "get_unchecked" );
-            ] );
-          ( "get_unchecked_mut",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked_mut"
-                | Lean -> "get_unchecked_mut" );
-            ] );
-          ( "index",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_index"
-                | Lean -> "index" );
-              (* The backward function shouldn't be used *)
-              ( rg0,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_index_back"
-                | Lean -> "index_back" );
-            ] );
-          ( "index_mut",
-            [
-              ( None,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut"
-                | Lean -> "index_mut" );
-              ( rg0,
-                match !backend with
-                | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut_back"
-                | Lean -> "index_mut_back" );
-            ] );
-        ];
-    };
+          ("get", true);
+          ("get_mut", true);
+          ("get_unchecked", false);
+          ("get_unchecked_mut", false);
+          ("index", true);
+          ("index_mut", true);
+        ]
+      ();
   ]
 
 let mk_builtin_trait_decls_map () =
@@ -633,66 +516,66 @@ module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
 
 let builtin_trait_impls_info () :
     ((string list * string list) * (bool list option * string)) list =
-  let fmt ?(filter : bool list option = None) (name : string) :
-      bool list option * string =
+  let fmt (type_name : string list) (trait_name : string list)
+      ?(filter : bool list option = None) () :
+      (string list * string list) * (bool list option * string) =
     let name =
-      match !backend with
-      | Lean -> name
-      | FStar | Coq | HOL4 ->
-          let name = String.split_on_char '.' name in
-          String.concat "_" name
+      let trait_name = String.concat "" trait_name ^ "Inst" in
+      let sep = backend_choice "_" "." in
+      String.concat sep type_name ^ sep ^ trait_name
     in
-    (filter, name)
+    ((type_name, trait_name), (filter, name))
   in
   (* TODO: fix the names like "[T]" below *)
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
-    ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
-      fmt "alloc.boxed.Box.coreOpsDerefInst" );
+    fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "Deref" ] ();
     (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
-    ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
-      fmt "alloc.boxed.Box.coreOpsDerefMutInst" );
+    fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "DerefMut" ] ();
     (* core::ops::index::Index<[T], I> *)
-    ( ([ "core"; "slice"; "index"; "[T]" ], [ "core"; "ops"; "index"; "Index" ]),
-      fmt "core.slice.index.Slice.coreopsindexIndexInst" );
+    fmt
+      [ "core"; "slice"; "index"; "[T]" ]
+      [ "core"; "ops"; "index"; "Index" ]
+      ();
     (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
-    ( ( [ "core"; "slice"; "index"; "private_slice_index"; "Range" ],
-        [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ),
-      fmt
-        "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst"
-    );
+    fmt
+      [ "core"; "slice"; "index"; "private_slice_index"; "Range" ]
+      [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
+      ();
     (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
-    ( ( [ "core"; "slice"; "index"; "Range" ],
-        [ "core"; "slice"; "index"; "SliceIndex" ] ),
-      fmt "core.slice.index.Range.coresliceindexSliceIndexInst" );
+    fmt
+      [ "core"; "slice"; "index"; "Range" ]
+      [ "core"; "slice"; "index"; "SliceIndex" ]
+      ();
     (* core::ops::index::IndexMut<[T], I> *)
-    ( ( [ "core"; "slice"; "index"; "[T]" ],
-        [ "core"; "ops"; "index"; "IndexMut" ] ),
-      fmt "core.slice.index.Slice.coreopsindexIndexMutInst" );
+    fmt
+      [ "core"; "slice"; "index"; "[T]" ]
+      [ "core"; "ops"; "index"; "IndexMut" ]
+      ();
     (* core::ops::index::Index<[T; N], I> *)
-    ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "Index" ]),
-      fmt "core.array.Array.coreopsindexIndexInst" );
+    fmt [ "core"; "array"; "[T; N]" ] [ "core"; "ops"; "index"; "Index" ] ();
     (* core::ops::index::IndexMut<[T; N], I> *)
-    ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "IndexMut" ]),
-      fmt "core.array.Array.coreopsindexIndexMutInst" );
+    fmt [ "core"; "array"; "[T; N]" ] [ "core"; "ops"; "index"; "IndexMut" ] ();
     (* core::slice::index::private_slice_index::Sealed<usize> *)
-    ( ( [ "core"; "slice"; "index"; "private_slice_index"; "usize" ],
-        [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ),
-      fmt
-        "core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst"
-    );
+    fmt
+      [ "core"; "slice"; "index"; "private_slice_index"; "usize" ]
+      [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
+      ();
     (* core::slice::index::SliceIndex<usize, [T]> *)
-    ( ( [ "core"; "slice"; "index"; "usize" ],
-        [ "core"; "slice"; "index"; "SliceIndex" ] ),
-      fmt "core.slice.index.usize.coresliceindexSliceIndexInst" );
+    fmt
+      [ "core"; "slice"; "index"; "usize" ]
+      [ "core"; "slice"; "index"; "SliceIndex" ]
+      ();
     (* core::ops::index::Index<Vec<T>, T> *)
-    ( ([ "alloc"; "vec"; "Vec" ], [ "core"; "ops"; "index"; "Index" ]),
-      let filter = Some [ true; true; false ] in
-      fmt ~filter "alloc.vec.Vec.coreopsindexIndexInst" );
+    fmt [ "alloc"; "vec"; "Vec" ]
+      [ "core"; "ops"; "index"; "Index" ]
+      ~filter:(Some [ true; true; false ])
+      ();
     (* core::ops::index::IndexMut<Vec<T>, T> *)
-    ( ([ "alloc"; "vec"; "Vec" ], [ "core"; "ops"; "index"; "IndexMut" ]),
-      let filter = Some [ true; true; false ] in
-      fmt ~filter "alloc.vec.Vec.coreopsindexIndexMutInst" );
+    fmt [ "alloc"; "vec"; "Vec" ]
+      [ "core"; "ops"; "index"; "IndexMut" ]
+      ~filter:(Some [ true; true; false ])
+      ();
   ]
 
 let mk_builtin_trait_impls_map () =
-- 
cgit v1.2.3


From 7a65b74fb889e87a071b1cc2f0dbd355ebd3c1e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 13:52:38 +0200
Subject: Improve ExtractBuiltin.ml

---
 compiler/ExtractBuiltin.ml | 86 ++++++++++++++++++++++++++--------------------
 1 file changed, 49 insertions(+), 37 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 510de583..8fcdea56 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -97,7 +97,7 @@ type builtin_enum_variant_info = {
 [@@deriving show]
 
 type builtin_type_body_info =
-  | Struct of string * string list
+  | Struct of string * (string * string) list
     (* The constructor name and the map for the field names *)
   | Enum of builtin_enum_variant_info list
 (* For every variant, a map for the field names *)
@@ -116,6 +116,19 @@ type builtin_type_info = {
 }
 [@@deriving show]
 
+type type_variant_kind =
+  | KOpaque
+  | KStruct of (string * string) list
+  (* TODO: handle the tuple case *)
+  | KEnum (* TODO *)
+
+let mk_struct_constructor (type_name : string) : string =
+  let prefix =
+    match !backend with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+  in
+  let suffix = match !backend with FStar | Coq | HOL4 -> "" | Lean -> ".mk" in
+  prefix ^ type_name ^ suffix
+
 (** The assumed types.
 
     The optional list of booleans is filtering information for the type
@@ -123,28 +136,44 @@ type builtin_type_info = {
     a type parameter for the allocator to use, which we want to filter.
  *)
 let builtin_types () : builtin_type_info list =
+  let mk_type (rust_name : string list) ?(keep_params : bool list option = None)
+      ?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
+    let extract_name =
+      let sep = backend_choice "_" "." in
+      String.concat sep rust_name
+    in
+    let body_info : builtin_type_body_info option =
+      match kind with
+      | KOpaque -> None
+      | KStruct fields ->
+          let fields =
+            List.map
+              (fun (rname, name) ->
+                (rname, backend_choice (extract_name ^ name) name))
+              fields
+          in
+          let constructor = mk_struct_constructor extract_name in
+          Some (Struct (constructor, fields))
+      | KEnum -> raise (Failure "TODO")
+    in
+    { rust_name; extract_name; keep_params; body_info }
+  in
+
   [
     (* Alloc *)
-    {
-      rust_name = [ "alloc"; "alloc"; "Global" ];
-      extract_name =
-        (match !backend with
-        | Lean -> "alloc.alloc.Global"
-        | Coq | FStar | HOL4 -> "alloc_alloc_Global");
-      keep_params = None;
-      body_info = None;
-    };
+    mk_type [ "alloc"; "alloc"; "Global" ] ();
     (* Vec *)
-    {
-      rust_name = [ "alloc"; "vec"; "Vec" ];
-      extract_name =
-        (match !backend with
-        | Lean -> "alloc.vec.Vec"
-        | Coq | FStar | HOL4 -> "alloc_vec_Vec");
-      keep_params = Some [ true; false ];
-      body_info = None;
-    };
-    (* Option *)
+    mk_type [ "alloc"; "vec"; "Vec" ] ~keep_params:(Some [ true; false ]) ();
+    (* Range *)
+    mk_type
+      [ "core"; "ops"; "range"; "Range" ]
+      ~kind:(KStruct [ ("start", "start"); ("end", "end_") ])
+      ();
+    (* Option
+
+       This one is more custom because we use the standard "option" type from
+       the target backend.
+    *)
     {
       rust_name = [ "core"; "option"; "Option" ];
       extract_name =
@@ -176,23 +205,6 @@ let builtin_types () : builtin_type_info list =
                };
              ]);
     };
-    (* Range *)
-    {
-      rust_name = [ "core"; "ops"; "range"; "Range" ];
-      extract_name =
-        (match !backend with
-        | Lean -> "core.ops.range.Range"
-        | Coq | FStar | HOL4 -> "core_ops_range_Range");
-      keep_params = None;
-      body_info =
-        Some
-          (Struct
-             ( (match !backend with
-               | Lean -> "core.ops.range.Range.mk"
-               | Coq | HOL4 -> "mk_core_ops_range_Range"
-               | FStar -> "Mkcore_ops_range_Range"),
-               [ "start"; "end_" ] ));
-    };
   ]
 
 let mk_builtin_types_map () =
-- 
cgit v1.2.3


From 442f0aede5da127b4828a90bcbade73a345340e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 14:10:57 +0200
Subject: Make progress on fixing the extraction

---
 compiler/ExtractBuiltin.ml | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 8fcdea56..afa0dd6f 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -528,12 +528,18 @@ module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
 
 let builtin_trait_impls_info () :
     ((string list * string list) * (bool list option * string)) list =
-  let fmt (type_name : string list) (trait_name : string list)
-      ?(filter : bool list option = None) () :
+  let fmt (type_name : string list)
+      ?(extract_type_name : string list option = None)
+      (trait_name : string list) ?(filter : bool list option = None) () :
       (string list * string list) * (bool list option * string) =
     let name =
       let trait_name = String.concat "" trait_name ^ "Inst" in
       let sep = backend_choice "_" "." in
+      let type_name =
+        match extract_type_name with
+        | Some type_name -> type_name
+        | None -> type_name
+      in
       String.concat sep type_name ^ sep ^ trait_name
     in
     ((type_name, trait_name), (filter, name))
@@ -547,8 +553,15 @@ let builtin_trait_impls_info () :
     (* core::ops::index::Index<[T], I> *)
     fmt
       [ "core"; "slice"; "index"; "[T]" ]
+      ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ])
       [ "core"; "ops"; "index"; "Index" ]
       ();
+    (* core::ops::index::IndexMut<[T], I> *)
+    fmt
+      [ "core"; "slice"; "index"; "[T]" ]
+      ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ])
+      [ "core"; "ops"; "index"; "IndexMut" ]
+      ();
     (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
     fmt
       [ "core"; "slice"; "index"; "private_slice_index"; "Range" ]
@@ -559,15 +572,18 @@ let builtin_trait_impls_info () :
       [ "core"; "slice"; "index"; "Range" ]
       [ "core"; "slice"; "index"; "SliceIndex" ]
       ();
-    (* core::ops::index::IndexMut<[T], I> *)
+    (* core::ops::index::Index<[T; N], I> *)
     fmt
-      [ "core"; "slice"; "index"; "[T]" ]
-      [ "core"; "ops"; "index"; "IndexMut" ]
+      [ "core"; "array"; "[T; N]" ]
+      ~extract_type_name:(Some [ "core"; "array"; "Array" ])
+      [ "core"; "ops"; "index"; "Index" ]
       ();
-    (* core::ops::index::Index<[T; N], I> *)
-    fmt [ "core"; "array"; "[T; N]" ] [ "core"; "ops"; "index"; "Index" ] ();
     (* core::ops::index::IndexMut<[T; N], I> *)
-    fmt [ "core"; "array"; "[T; N]" ] [ "core"; "ops"; "index"; "IndexMut" ] ();
+    fmt
+      [ "core"; "array"; "[T; N]" ]
+      ~extract_type_name:(Some [ "core"; "array"; "Array" ])
+      [ "core"; "ops"; "index"; "IndexMut" ]
+      ();
     (* core::slice::index::private_slice_index::Sealed<usize> *)
     fmt
       [ "core"; "slice"; "index"; "private_slice_index"; "usize" ]
-- 
cgit v1.2.3


From 005ad3cc03745bc9211defa481d5e45738a6d832 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 14:37:34 +0200
Subject: Improve the handling of saved function effects in ExtractBuiltin.ml

---
 compiler/ExtractBuiltin.ml | 40 +++++++++++++++++++++++++++-------------
 1 file changed, 27 insertions(+), 13 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index afa0dd6f..363955bf 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -350,7 +350,9 @@ let mk_builtin_funs_map () =
 
 let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
-let builtin_non_fallible_funs =
+type effect_info = { can_fail : bool; stateful : bool }
+
+let builtin_fun_effects =
   let int_names =
     [
       "usize";
@@ -377,19 +379,31 @@ let builtin_non_fallible_funs =
       int_names
   in
   let int_funs = List.concat int_funs in
-  [
-    "alloc::vec::Vec::new";
-    "alloc::vec::Vec::len";
-    "alloc::boxed::Box::deref";
-    "alloc::boxed::Box::deref_mut";
-    "core::mem::replace";
-    "core::mem::take";
-  ]
-  @ int_funs
+  let no_fail_no_state_funs =
+    [
+      "alloc::vec::Vec::new";
+      "alloc::vec::Vec::len";
+      "alloc::boxed::Box::deref";
+      "alloc::boxed::Box::deref_mut";
+      "core::mem::replace";
+      "core::mem::take";
+    ]
+    @ int_funs
+  in
+  let no_fail_no_state_funs =
+    List.map
+      (fun n -> (n, { can_fail = false; stateful = false }))
+      no_fail_no_state_funs
+  in
+  let no_state_funs = [ "alloc::vec::Vec::push" ] in
+  let no_state_funs =
+    List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs
+  in
+  no_fail_no_state_funs @ no_state_funs
 
-let builtin_non_fallible_funs_set =
-  SimpleNameSet.of_list
-    (List.map string_to_simple_name builtin_non_fallible_funs)
+let builtin_fun_effects_map =
+  SimpleNameMap.of_list
+    (List.map (fun (n, x) -> (string_to_simple_name n, x)) builtin_fun_effects)
 
 type builtin_trait_decl_info = {
   rust_name : string;
-- 
cgit v1.2.3


From 7ffcb8e9c5c03f198362fd27bd42f30064541509 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 15:06:36 +0200
Subject: Fix some issues and regenerate the HashmapMain example for Lean

---
 compiler/ExtractBuiltin.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 363955bf..2dbacce3 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -381,6 +381,7 @@ 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::Vec::new";
       "alloc::vec::Vec::len";
       "alloc::boxed::Box::deref";
@@ -395,7 +396,15 @@ let builtin_fun_effects =
       (fun n -> (n, { can_fail = false; stateful = false }))
       no_fail_no_state_funs
   in
-  let no_state_funs = [ "alloc::vec::Vec::push" ] in
+  let no_state_funs =
+    [
+      (* TODO: redundancy with the funs information below *)
+      "alloc::vec::Vec::push";
+      "alloc::vec::Vec::index";
+      "alloc::vec::Vec::index_mut";
+      "alloc::vec::Vec::index_mut_back";
+    ]
+  in
   let no_state_funs =
     List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs
   in
-- 
cgit v1.2.3


From 1110b3da85e93ba0755a665edd5b8c986c54cef0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 16:15:35 +0200
Subject: Make minor modifications and update the array test for F*

---
 compiler/ExtractBuiltin.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 2dbacce3..c6bde9c2 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -149,7 +149,10 @@ let builtin_types () : builtin_type_info list =
           let fields =
             List.map
               (fun (rname, name) ->
-                (rname, backend_choice (extract_name ^ name) name))
+                ( rname,
+                  match !backend with
+                  | FStar | Lean -> name
+                  | Coq | HOL4 -> extract_name ^ "_" ^ name ))
               fields
           in
           let constructor = mk_struct_constructor extract_name in
-- 
cgit v1.2.3


From 3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 16:22:09 +0100
Subject: Make the traits work for Coq

---
 compiler/ExtractBuiltin.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index c6bde9c2..a54ab604 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -420,6 +420,7 @@ let builtin_fun_effects_map =
 type builtin_trait_decl_info = {
   rust_name : string;
   extract_name : string;
+  constructor : string;
   parent_clauses : string list;
   consts : (string * string) list;
   types : (string * (string * string list)) list;
@@ -444,6 +445,7 @@ let builtin_trait_decls_info () =
           | Coq | FStar | HOL4 -> String.concat "_" rust_name
           | Lean -> String.concat "." rust_name)
     in
+    let constructor = mk_struct_constructor extract_name in
     let consts = [] in
     let types =
       let mk_type item_name =
@@ -479,7 +481,15 @@ let builtin_trait_decls_info () =
       List.map mk_method methods
     in
     let rust_name = String.concat "::" rust_name in
-    { rust_name; extract_name; parent_clauses; consts; types; methods }
+    {
+      rust_name;
+      extract_name;
+      constructor;
+      parent_clauses;
+      consts;
+      types;
+      methods;
+    }
   in
   [
     (* Deref *)
-- 
cgit v1.2.3