Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplifications

 Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v)
 by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree:
 the argument v should also be magic now, otherwise it might not have
 the same type as x.

 This optimization is now correctly done, and to mitigate the potential inflation
 of Obj.magic, I've added a few simplification rules to avoid redundant magics,
 push them down inside terms, favor the form (Obj.magic f x y z), etc.

1 files changed, 18 insertions, 2 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index eb3046f031..d06583010f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1035,6 +1035,13 @@ let rec simpl o = function
       if ast_occurs_itvl 1 n c.(i) then
 	MLfix (i, ids, Array.map (simpl o) c)
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
+  | MLmagic(MLmagic _ as e) -> simpl o e
+  | MLmagic(MLapp (f,l)) -> simpl o (MLapp (MLmagic f, l))
+  | MLmagic(MLletin(id,c,e)) -> simpl o (MLletin(id,c,MLmagic e))
+  | MLmagic(MLcase(typ,e,br)) ->
+     let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
+     simpl o (MLcase(typ,e,br'))
+  | MLmagic(MLexn _ as e) -> e
   | a -> ast_map (simpl o) a
 
 (* invariant : list [a] of arguments is non-empty *)
@@ -1053,8 +1060,17 @@ and simpl_app o a = function
 	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
   | MLmagic (MLlam (id,t)) ->
       (* When we've at least one argument, we permute the magic
-         and the lambda, to simplify things a bit (see #2795) *)
-      simpl_app o a (MLlam (id,MLmagic t))
+         and the lambda, to simplify things a bit (see #2795).
+         Alas, the 1st argument must also be magic then. *)
+      let a' = match a with
+        | MLmagic _ :: _ -> a
+        | e::a' -> MLmagic e::a'
+        | [] -> assert false
+      in
+      simpl_app o a' (MLlam (id,MLmagic t))
+  | MLmagic _ as e ->
+      (* When the head is magic, no need for magic on args *)
+      MLapp (e, List.map (function MLmagic e -> e | e -> e) a)
   | MLletin (id,e1,e2) when o.opt_let_app ->
       (* Application of a letin: we push arguments inside *)
       MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))