From ce395ca02311bbe6ecc1b2782e74312272dd15ec Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 22:31:41 +0100
Subject: Extraction: allow basic beta-reduction even through a MLmagic (fix
 #2795)

 This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
 to properly investigate the interaction between all the other optimizations
 and MLmagic. But well, at least this precise bug is fixed now.
---
 plugins/extraction/mlutil.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 70249193e5..bfd0794de2 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -987,6 +987,10 @@ and simpl_app o a = function
 	 | _ ->
 	     let a' = List.map (ast_lift 1) (List.tl a) in
 	     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))
   | 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