diff options
| author | Pierre Letouzey | 2015-12-14 22:31:41 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-14 22:42:29 +0100 |
| commit | ce395ca02311bbe6ecc1b2782e74312272dd15ec (patch) | |
| tree | 5649f9f2b332288a41b23da93411fc064650c81f | |
| parent | 2ab8455cffef4097a441eb6befaa29f6f3076824 (diff) | |
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.
| -rw-r--r-- | plugins/extraction/mlutil.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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))) |