Better codegen for array repeats in Rust -- fixes #137

.ocamlformat

@@ -1,5 +1,5 @@
 profile = default
-version = 0.26.2
+version = 0.27.0
 margin = 100
 
 break-cases = fit-or-vertical

bin/main.ml

@@ -201,7 +201,7 @@ Supported options:|}
   let files = Eurydice.Cleanup2.improve_names files in
   let files = Eurydice.Cleanup2.recognize_asserts#visit_files () files in
   (* Temporary workaround until Aeneas supports nested loops *)
-  let files = Eurydice.Cleanup2.inline_loops #visit_files () files in
+  let files = Eurydice.Cleanup2.inline_loops#visit_files () files in
   let files = Krml.Inlining.inline files in
   let files = Krml.Monomorphization.functions files in
   let files = Krml.Monomorphization.datatypes files in
@@ -221,7 +221,9 @@ Supported options:|}
     fail __FILE__ __LINE__;
   let files = Krml.Inlining.drop_unused files in
   let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in
+  Eurydice.Logging.log "Phase2.25" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_array_repeats#visit_files () files in
+  Eurydice.Logging.log "Phase2.26" "%a" pfiles files;
   let files = Eurydice.Cleanup2.rewrite_slice_to_array#visit_files () files in
   let files = Krml.DataTypes.simplify files in
   let files = Krml.DataTypes.optimize files in
@@ -238,10 +240,10 @@ Supported options:|}
      functions that do not write to memory). *)
   fill_readonly_table files;
   let files = Krml.Simplify.optimize_lets files in
-  (* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)
   let files = Eurydice.Cleanup2.remove_array_from_fn files in
   (* remove_array_from_fn, above, creates further opportunities for removing unused functions. *)
   let files = Krml.Inlining.drop_unused files in
+  Eurydice.Logging.log "Phase2.55" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in
   (* Creates opportunities for removing unused variables *)
   Eurydice.Logging.log "Phase2.6" "%a" pfiles files;

lib/Bundles.ml

@@ -439,16 +439,19 @@ let reassign_monomorphizations (files : Krml.Ast.file list) (config : config) =
                } ->
             (* Monomorphization resulting in exactly this name *)
             find_map (matches monomorphized_lid) monomorphizations_exact
-            ||| (* Monomorphization using given trait name, amongst the arguments *)
+            |||
+            (* Monomorphization using given trait name, amongst the arguments *)
             List.find_map
               (fun e ->
                 match e.node with
                 | EQualified lid' -> find_map (matches lid') monomorphizations_using
                 | _ -> None)
               cgs
-            ||| (* Monomorphization using given type name *)
+            |||
+            (* Monomorphization using given type name *)
             List.find_map (uses monomorphizations_using) ts
-            ||| (* Monomorphization of a given polymorphic name *)
+            |||
+            (* Monomorphization of a given polymorphic name *)
             find_map (matches generic_lid) monomorphizations_of
             |> Option.map (fun vis -> name, inline_static, vis))
           config

lib/Cleanup1.ml

@@ -117,13 +117,14 @@ let remove_assignments =
             @@ close_now_over not_yet_closed
                  ((* We must now bind: *)
                   count e
-                ++ (* whichever variables were in the condition *)
+                ++
+                (* whichever variables were in the condition *)
                 AtomSet.empty)
                  (* unlike below, we are in terminal position, so we do not need to
                     close immediately variables that appear in both branches -- we can simply declare them
                     twice in each branch! is this a better code-gen choice? yes, absolutely -- owing to
                     the structure of MIR, NOT doing this generates awful code *)
-                   (fun not_yet_closed ->
+                 (fun not_yet_closed ->
                    EIfThenElse
                      ( self#visit_expr_w not_yet_closed e,
                        recurse_or_close not_yet_closed e',
@@ -137,10 +138,11 @@ let remove_assignments =
             @@ close_now_over not_yet_closed
                  ((* We must now bind: *)
                   count e
-                ++ (* i.e., whichever variables were in the condition *)
+                ++
+                (* i.e., whichever variables were in the condition *)
                 AtomSet.empty)
                  (* see above *)
-                   (fun not_yet_closed ->
+                 (fun not_yet_closed ->
                    ESwitch
                      ( self#visit_expr_w not_yet_closed e,
                        List.map (fun (p, e) -> p, recurse_or_close not_yet_closed e) branches ))
@@ -149,10 +151,11 @@ let remove_assignments =
             @@ close_now_over not_yet_closed
                  ((* We must now bind: *)
                   count e
-                ++ (* i.e., whichever variables were in the condition *)
+                ++
+                (* i.e., whichever variables were in the condition *)
                 AtomSet.empty)
                  (* see above *)
-                   (fun not_yet_closed ->
+                 (fun not_yet_closed ->
                    EMatch
                      ( c,
                        self#visit_expr_w not_yet_closed e,
@@ -201,12 +204,14 @@ let remove_assignments =
           close_now_over not_yet_closed
             ((* We must now bind: *)
              count e
-            ++ (* whichever variables were in the condition *)
+            ++
+            (* whichever variables were in the condition *)
             AtomSet.inter (count e') (count e'')
-            ++ (* variables that appear in both branches *)
+            ++
+            (* variables that appear in both branches *)
             AtomSet.inter (count e' ++ count e'') (count e2))
             (* variables in either branch *and* used later *)
-              (fun not_yet_closed ->
+            (fun not_yet_closed ->
               ELet
                 ( b,
                   mk e1.typ e1.meta
@@ -232,16 +237,18 @@ let remove_assignments =
           close_now_over not_yet_closed
             ((* We must now bind: *)
              count e
-            ++ (* i.e., whichever variables were in the condition *)
+            ++
+            (* i.e., whichever variables were in the condition *)
             Krml.KList.reduce AtomSet.inter (List.map (fun (_p, e) -> count e) branches)
-            ++ (* i.e., variables that appear in all branches -- note that
+            ++
+            (* i.e., variables that appear in all branches -- note that
                   switches don't bind variables in their branches so it's simpler
                   than the match below*)
             AtomSet.inter
               (Krml.KList.reduce ( ++ ) (List.map (fun (_, e) -> count e) branches))
               (count e2))
             (* i.e., variables in either one of the branches *and* used later *)
-              (fun not_yet_closed ->
+            (fun not_yet_closed ->
               ELet
                 ( b,
                   mk e1.typ e1.meta
@@ -254,15 +261,17 @@ let remove_assignments =
           close_now_over not_yet_closed
             ((* We must now bind: *)
              count e
-            ++ (* i.e., whichever variables were in the condition *)
+            ++
+            (* i.e., whichever variables were in the condition *)
             Krml.KList.reduce AtomSet.inter (List.map (fun (_bs, _p, e) -> count e) branches)
-            ++ (* i.e., variables that appear in all branches -- note that we
+            ++
+            (* i.e., variables that appear in all branches -- note that we
                   don't open _bs meaning that we don't collect bound variables in this branch *)
             AtomSet.inter
               (Krml.KList.reduce ( ++ ) (List.map (fun (_, _, e) -> count e) branches))
               (count e2))
             (* i.e., variables in either one of the branches *and* used later *)
-              (fun not_yet_closed ->
+            (fun not_yet_closed ->
               ELet
                 ( b,
                   mk e1.typ e1.meta