From c5aca4005faf74d99091ef29257cbed6a53a12d4 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Sat, 5 Aug 2017 10:42:56 +0200
Subject: 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).
---
 plugins/extraction/mlutil.ml  | 18 +++++++++++++++
 test-suite/bugs/closed/4852.v | 54 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 72 insertions(+)
 create mode 100644 test-suite/bugs/closed/4852.v

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 *)
diff --git a/test-suite/bugs/closed/4852.v b/test-suite/bugs/closed/4852.v
new file mode 100644
index 000000000..5068ed9b9
--- /dev/null
+++ b/test-suite/bugs/closed/4852.v
@@ -0,0 +1,54 @@
+(** BZ 4852 : unsatisfactory Extraction Implicit for a fixpoint defined via wf *)
+
+Require Import Coq.Lists.List.
+Import ListNotations.
+Require Import Omega.
+
+Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.
+
+Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) :=
+  let R := fresh in
+  let E := fresh in
+  remember term as R eqn:E;
+  revert E; revert Hs;
+  induction R as [R H] using wfi_lt;
+  intros; subst R.
+
+Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws.
+
+Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega.
+
+Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'").
+
+Definition split_acc (ls : list nat) : forall acc1 acc2,
+    (|acc1| = |acc2| \/ |acc1| = S (|acc2|)) ->
+    { lss : list nat * list nat |
+      let '(ls1, ls2) := lss in |ls1++ls2| = |ls++acc1++acc2| /\ (|ls1| = |ls2| \/ |ls1| = S (|ls2|))}.
+Proof.
+  induction ls as [|a ls IHls]. all:intros acc1 acc2 H.
+  { exists (acc1, acc2). cbn. intuition reflexivity. }
+  destruct (IHls (a::acc2) acc1) as [[ls1 ls2] (H1 & H2)]. 1:solve_nat.
+  exists (ls1, ls2). cbn. intuition solve_nat.
+Defined.
+
+Definition join(ls : list nat) : { rls : list nat | |rls| = |ls| }.
+Proof.
+  wfinduction (|ls|) on ls as IH.
+  case (split_acc ls [] []). 1:solve_nat.
+  intros (ls1 & ls2) (H1 & H2).
+  destruct ls2 as [|a ls2].
+  - exists ls1. solve_nat.
+  - unshelve eelim (IH _ _ ls1 eq_refl). 1:solve_nat. intros rls1 H3.
+    unshelve eelim (IH _ _ ls2 eq_refl). 1:solve_nat. intros rls2 H4.
+    exists (a :: rls1 ++ rls2). solve_nat.
+Defined.
+
+Require Import ExtrOcamlNatInt.
+Extract Inlined Constant length => "List.length".
+Extract Inlined Constant app => "List.append".
+
+Extraction Inline wfi_lt.
+Extraction Implicit wfi_lt [1 3].
+Recursive Extraction join. (* was: Error: An implicit occurs after extraction *)
+Extraction TestCompile join.
+
-- 
cgit v1.2.3