From 0c60735279301d22ac3e03f862f86997cb85bce0 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 16 Dec 2015 00:59:38 +0100
Subject: 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.
---
 plugins/extraction/mlutil.ml | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

(limited to 'plugins')

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)))
-- 
cgit v1.2.3