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 /plugins/extraction/mlutil.ml | |
| 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.
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -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))) |