Merge pull request #495 from FStarLang/afromher_rust

New round of improvements for Rust backend

lib/Builtin.ml

@@ -434,7 +434,12 @@ let is_model name =
       "C_Compat_String";
       "FStar_String";
       "Steel_SpinLock"
-    ]
+    ] || (
+      Options.rust () &&
+      List.mem name [
+        "Pulse_Lib_Slice"
+      ]
+    )
 
 (* We have several different treatments. *)
 let prepare files =

lib/DataTypes.ml

@@ -203,7 +203,7 @@ let build_scheme_map files =
           Hashtbl.add map lid ToEnum (* logic replicated in Monomorphization *)
         else if List.length branches = 1 then
           Hashtbl.add map lid (ToFlat (List.map fst (snd (List.hd branches))))
-        else if List.length non_constant = 1 then
+        else if List.length non_constant = 1 && not (Options.rust ()) then
           Hashtbl.add map lid (ToFlatTaggedUnion branches)
         else
           Hashtbl.add map lid (ToTaggedUnion branches);

lib/Inlining.ml

@@ -201,7 +201,7 @@ let mk_crate_of files =
     StringMap.find f map
 
 (** This phase is concerned with three whole-program, cross-compilation-unit
-    analyses, performed ina single pass:
+    analyses, performed in a single pass:
     - assign correct visibility to declarations in the presence of bundling,
       static-header, mutually-recursive definitions, stackinline,
       inline_for_extraction, the friend mechanism, and the krmlinit_globals

lib/MiniRust.ml

@@ -1,7 +1,7 @@
 (* A minimalistic representation of Rust *)
 
 module Name = struct
-  type t = string list
+  type t = string list [@@ deriving show ]
   let compare = compare
 end
 
@@ -12,7 +12,7 @@ type borrow_kind = borrow_kind_ [@ opaque ]
 and constant = Constant.t [@ opaque ]
 and width = Constant.width [@ opaque ]
 and op = Constant.op [@ opaque ]
-and name = Name.t [@ opaque ]
+and name = Name.t [@ visitors.opaque ]
 
 (* Some design choices.
    - We don't intend to perform any deep semantic transformations on this Rust
@@ -36,7 +36,7 @@ type typ =
   | Unit [@name "tunit"]
   | Function of int * typ list * typ
   | Name of name * generic_param list [@name "tname"]
-  | Tuple of typ list
+  | Tuple of typ list [@name "ttuple"]
   | App of typ * typ list
   | Bound of db_index
 [@@deriving show,
@@ -62,8 +62,7 @@ let usize = Constant SizeT
 
 type binding = { name: string; typ: typ; mut: bool; ref: bool (* only for pattern variables *) }
 [@@deriving show,
-  visitors { variety = "map"; name = "map_binding";
-    ancestors = [ "map_misc"; "map_typ" ] }]
+  visitors { variety = "map"; name = "map_binding"; ancestors = [ "map_misc"; "map_typ" ] }]
 
 (* Top-level declarations *)
 
@@ -96,8 +95,9 @@ and expr =
   | While of expr * expr
   | MethodCall of expr * name * expr list
   | Range of expr option * expr option * bool (* inclusive? *)
-  | Struct of name * (string * expr) list
+  | Struct of struct_name * (string * expr) list
   | Match of expr * typ * match_arm list
+  | Tuple of expr list
 
   (* Place expressions *)
   | Var of db_index
@@ -120,11 +120,16 @@ and match_arm = binding list * pat * expr
 and pat =
   | Literal of constant
   | Wildcard
-  (* A "struct pattern" per the Rust grammar that covers both Enum and Struct *)
-  | StructP of ([ `Struct of name | `Variant of name * string ] [@ opaque]) * (string * pat) list
+  | TupleP of pat list
+  | StructP of struct_name * (string * pat) list
   | VarP of db_index
   | OpenP of open_var
 
+(* In the Rust grammar, both variants and structs are covered by the struct
+  case. We disambiguate between the two *)
+and struct_name =
+  [ `Struct of name | `Variant of name * string ] [@ opaque]
+
 and open_var = {
   name: string;
   atom: atom_t
@@ -163,6 +168,7 @@ type decl =
     body: expr;
     meta: meta;
     inline: bool;
+    generic_params: generic_param list;
   }
   | Constant of {
     name: name;
@@ -175,10 +181,12 @@ type decl =
     items: item list;
     derives: trait list;
     meta: meta;
+    generic_params: generic_param list;
   }
   | Struct of {
     name: name;
     fields: struct_field list;
+    derives: trait list;
     meta: meta;
     generic_params: generic_param list;
   }

lib/Monomorphization.ml

@@ -147,7 +147,7 @@ module NameGen = struct
         let n = Printf.sprintf "%s_%02x" n (hash land 0xFF) in
         let n = Idents.mk_fresh n (fun n -> Hashtbl.mem seen (m, n)) in
         Hashtbl.add seen (m, n) ();
-        (m, n), [ Common.AutoGenerated; gen_comment lid ts extra ] 
+        (m, n), [ Common.AutoGenerated; gen_comment lid ts extra ]
     else
       let doc =
         separate_map underscore print_typ ts ^^
@@ -432,7 +432,7 @@ let monomorphize_data_types map = object(self)
       if Options.debug "data-types-traversal" then
         KPrint.bprintf "decl %a\n" plid (lid_of_decl d);
       match d with
-      | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not (Hashtbl.mem state (tuple_lid, args, [])) ->
+      | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not !Options.keep_tuples && not (Hashtbl.mem state (tuple_lid, args, [])) ->
           Hashtbl.remove map lid;
           if Options.debug "monomorphization" then
             KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp (TApp (tuple_lid, args));
@@ -514,13 +514,19 @@ let monomorphize_data_types map = object(self)
       super#visit_DType env name flags n d
 
   method! visit_ETuple under_ref es =
-    EFlat (List.mapi (fun i e -> Some (self#field_at i), self#visit_expr under_ref e) es)
+    if not !Options.keep_tuples then
+      EFlat (List.mapi (fun i e -> Some (self#field_at i), self#visit_expr under_ref e) es)
+    else
+      super#visit_ETuple under_ref es
 
   method! visit_PTuple under_ref pats =
-    PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats)
+    if not !Options.keep_tuples then
+      PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats)
+    else
+      super#visit_PTuple under_ref pats
 
   method! visit_TTuple under_ref ts =
-    if not (has_variables ts) && not (has_cg_array ts) then
+    if not !Options.keep_tuples && not (has_variables ts) && not (has_cg_array ts) then
       TQualified (self#visit_node under_ref (tuple_lid, ts, []))
     else
       super#visit_TTuple under_ref ts