Improve the treatment of abstract, polymorphic functions that are use…

…d with array types

bin/main.ml

@@ -214,7 +214,6 @@ Supported options:|}
   Eurydice.Logging.log "Phase2.2" "%a" pfiles files;
   (* Sanity check for the big rewriting above. *)
   let errors, files = Krml.Checker.check_everything ~warn:true files in
-  Eurydice.Logging.log "Phase2.25" "%a" pfiles files;
   if errors then
     fail __FILE__ __LINE__;
   let files = Krml.Inlining.drop_unused files in
@@ -230,12 +229,11 @@ Supported options:|}
   let files = Eurydice.Cleanup2.remove_trivial_into#visit_files () files in
   let files = Krml.Structs.pass_by_ref files in
   Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
-  let files = Eurydice.Cleanup2.detect_array_returning_builtins#visit_files () files in
+  Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_literals#visit_files () files in
   (* Eurydice does something more involved than krml and performs a conservative
      approximation of functions that are known to be pure readonly (i.e.,
      functions that do not write to memory). *)
-  Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
   fill_readonly_table files;
   let files = Krml.Simplify.optimize_lets files in
   (* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)

lib/Cleanup2.ml

@@ -618,52 +618,6 @@ let resugar_loops =
 end
 [@ocamlformat "disable"]
 
-(* So I'm not entirely clear on the meaning of this phase, but I think two
-   things are simultaneously true:
-   - builtins (externals) have only one signature (duh), so if the pass_by_ref
-     phase rewrites the signature of an external like slice_index, then we're
-     toast! this will be a type error, so we need to undo some of the work of
-     pass_by_ref (this could be conceivably fixed on the krml side)
-   - MIR is aware of what in C is called array decay, and for instance, if x has
-     type &[[T; N]], then let y = &x[0] generates a simple index into x where y
-     has type T* (not type [T; N]) -- if there is a [T; N] involved, this is
-     represented in MIR by an &x[i] followed by an array-assignment, meaning
-     that there is nothing smart to be done here for slice indices, this is
-     already handled.
-   So, that's two good reasons to not bother rewriting the signature of
-   slice_index, even if the type of elements is an array. (Note: a previous
-   version of this wasn't aware of the second point and had a variant called
-   slice_index_outparam. Turns out this isn't necessary.) *)
-let detect_array_returning_builtins =
-  object
-  inherit [_] map as super
-
-  method! visit_ELet ((), _ as env) b e1 e2 =
-    match e1.node, e2.node with
-    (* let ret = $any;
-       Eurydice_slice_index (e_slice, e_index, ret);
-       e2 *)
-    | EAny, ESequence [
-      { node = EApp (
-        { node = ETApp ({ node = EQualified (["Eurydice"], "slice_index"); _ }, [], [], [ t_elements ]) as hd; _ },
-        [ e_slice; e_index; { node = EBound 0; _ } ]); _ };
-      e2
-    ] ->
-        (* ret does not appear in the first two arguments of slice_index --
-           shift them above the ret *)
-        let shift1 = Krml.DeBruijn.subst Krml.Helpers.eunit 0 in
-        let e_slice = shift1 e_slice in
-        let e_index = shift1 e_index in
-        let t_hd = Krml.DeBruijn.subst_t t_elements 0 Builtin.slice_index.typ in
-        let e_slice_index = with_type t_elements (EApp (with_type t_hd hd, [ e_slice; e_index ])) in
-        (* now substitute *)
-        (Krml.DeBruijn.subst e_slice_index 0 e2).node
-
-    | _ ->
-        super#visit_ELet env b e1 e2
-end
-[@ocamlformat "disable"]
-
 let improve_names files =
   let renamed = Hashtbl.create 41 in
   let allocated = Hashtbl.create 41 in