Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4852)

 This code simplification isn't that important, but it can trigger further
 simplifications elsewhere, see for instance BZ#4852.

 NB: normally, the extraction favors eta-expanded forms, since that's the usual
 way to avoid issues about '_a type variables that cannot be generalized. But
 the atomic eta-reductions done here shouldn't be problematic (no applications
 put outside of functions).

1 files changed, 18 insertions, 0 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a4c2bcd88..b16b430a8 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -769,6 +769,20 @@ let eta_red e =
 	else e
     | _ -> e
 
+(* Performs an eta-reduction when the core is atomic,
+   or otherwise returns None *)
+
+let atomic_eta_red e =
+  let ids,t = collect_lams e in
+  let n = List.length ids in
+  match t with
+  | MLapp (f,a) when test_eta_args_lift 0 n a ->
+     (match f with
+      | MLrel k when k>n -> Some (MLrel (k-n))
+      | MLglob _ | MLexn _ | MLdummy _ -> Some f
+      | _ -> None)
+  | _ -> None
+
 (*s Computes all head linear beta-reductions possible in [(t a)].
   Non-linear head beta-redex become let-in. *)
 
@@ -1053,6 +1067,10 @@ let rec simpl o = function
      simpl o (MLcase(typ,e,br'))
   | MLmagic(MLdummy _ as e) when lang () == Haskell -> e
   | MLmagic(MLexn _ as e) -> e
+  | MLlam _ as e ->
+     (match atomic_eta_red e with
+      | Some e' -> e'
+      | None -> ast_map (simpl o) e)
   | a -> ast_map (simpl o) a
 
 (* invariant : list [a] of arguments is non-empty *)