Merge pull request #462 from FStarLang/afromher_rust

Do not generate (); in Rust backends

lib/OptimizeMiniRust.ml

@@ -787,3 +787,72 @@ let infer_mut_borrows files =
     | x -> x
     ) decls
   ) (List.rev files)
+
+
+(* Transformations occuring on the MiniRust AST, after translation and mutability inference *)
+
+(* Loop unrolling introduces an implicit binder that does not interact well
+   with the substitutions occurring in mutability inference.
+   We perform it after the translation *)
+let unroll_loops = object
+  inherit [_] map_expr as super
+  method! visit_For _ b e1 e2 =
+    let e2 = super#visit_expr () e2 in
+
+    match e1 with
+    | Range (Some (Constant (UInt32, init as k_init) as e_init), Some (Constant (UInt32, max)), false)
+      when (
+        let init = int_of_string init in
+        let max = int_of_string max in
+        let n_loops = max - init in
+        n_loops <= !Options.unroll_loops
+      ) ->
+        let init = int_of_string init in
+        let max = int_of_string max in
+        let n_loops = max - init in
+
+        if n_loops = 0 then Unit
+
+        else if n_loops = 1 then subst e_init 0 e2
+
+        else Call (Name ["krml"; "unroll_for!"], [], [
+          Constant (CInt, string_of_int n_loops);
+          ConstantString b.name;
+          Constant k_init;
+          Constant (UInt32, "1");
+          e2
+        ])
+
+    | _ -> For (b, e1, e2)
+end
+
+let remove_trailing_unit = object
+  inherit [_] map_expr as super
+  method! visit_Let _ b e1 e2 =
+    let e1 = super#visit_expr () e1 in
+    let e2 = super#visit_expr () e2 in
+    match e2 with
+    | Unit -> e1
+    | _ -> Let (b, e1, e2)
+end
+
+let map_funs f_map files =
+  let files =
+    List.fold_left (fun files (filename, decls) ->
+      let decls = List.fold_left (fun decls decl ->
+        match decl with
+        | Function ({ body; _ } as f) ->
+          let body = f_map () body in
+          Function {f with body} :: decls
+        | _ -> decl :: decls
+      ) [] decls in
+      let decls = List.rev decls in
+      (filename, decls) :: files
+    ) [] files
+  in
+  List.rev files
+
+let simplify_minirust files =
+  let files = map_funs unroll_loops#visit_expr files in
+  let files = map_funs remove_trailing_unit#visit_expr files in
+  files

lib/PrintMiniRust.ml

@@ -236,6 +236,9 @@ and print_expression_with_block env (e: expr): document =
 
 and print_statements env (e: expr): document =
   match e with
+  | Let ({ typ = Unit; _ }, Unit, e2) ->
+      (* Special-case: if we have a unit (probably due to an erased node), we omit it *)
+      print_statements (push env (`GoneUnit)) e2
   | Let ({ typ = Unit; _ }, e1, e2) ->
       print_expr env max_int e1 ^^ semi ^^ hardline ^^
       print_statements (push env (`GoneUnit)) e2

lib/SimplifyRust.ml

@@ -9,6 +9,7 @@ let remove_push_pop_frame = object
   method! visit_EPopFrame _ = EUnit
 end
 
-let simplify files =
+let simplify_ast files =
   let files = remove_push_pop_frame#visit_files () files in
   files
+

src/Karamel.ml

@@ -681,7 +681,7 @@ Supported options:|}
   let ifdefs = AstToCStar.mk_ifdefs_set files in
   let macros = AstToCStar.mk_macros_set files in
 
-  let files = if Options.rust () then SimplifyRust.simplify files else files in
+  let files = if Options.rust () then SimplifyRust.simplify_ast files else files in
   let files = Simplify.simplify2 ifdefs files in
   let files = Inlining.mark_possibly_unused ifdefs files in
   let files = if Options.(!merge_variables <> No) then SimplifyMerge.simplify files else files in
@@ -751,7 +751,7 @@ Supported options:|}
       print PrintAst.print_files files;
     let files = AstToMiniRust.translate_files files in
     let files = OptimizeMiniRust.infer_mut_borrows files in
-    let files = RustMacroize.macroize files in
+    let files = OptimizeMiniRust.simplify_minirust files in
     OutputRust.write_all files
 
   else