From cf36105854c9a42960ee4139c6afdaa75ec8f31a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 1 Oct 2014 23:27:09 +0200
Subject: Move eta-expansion after delta reduction in kernel reduction. This
 makes it closer to evarconv/unification's behavior and it is less prone to
 weird failures and successes in case of first-order unification sending
 problems where the two terms have different types.

---
 kernel/reduction.ml | 88 +++++++++++++++++++++++++++++------------------------
 1 file changed, 48 insertions(+), 40 deletions(-)

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 9a7146890..60109b6c6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -285,6 +285,10 @@ let unfold_projection infos p c =
       | None -> None)
   else None
 
+let check_lambda_args = function
+  | [] -> ()
+  | _ -> anomaly (Pp.str "conversion was given unreduced term (FLambda)")
+    
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
   eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -406,53 +410,57 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
         ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
 
+    (* only one constant, defined var or defined rel *)
+    | (FFlex fl1, c2)      ->
+      (match unfold_reference infos fl1 with
+      | Some def1 ->
+	eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+      | None -> 
+	match c2 with
+	| FConstruct ((ind2,j2),u2) ->
+	  (try
+ 	     let v2, v1 =
+ 	       eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+ 	     in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ 	   with Not_found -> raise NotConvertible)
+	| FLambda _ ->
+	  let () = check_lambda_args v2 in
+          let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+	    eqappr CONV l2r infos
+	      (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
+	| _ -> raise NotConvertible)
+
+    | (c1, FFlex fl2)      ->
+      (match unfold_reference infos fl2 with
+      | Some def2 ->
+	eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+      | None -> 
+	match c1 with
+	| FConstruct ((ind1,j1),u1) ->
+ 	  (try let v1, v2 =
+	     	 eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+	       in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	   with Not_found -> raise NotConvertible)
+	| FLambda _ -> 
+	  let () = check_lambda_args v1 in
+	  let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+	    eqappr CONV l2r infos
+	      (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
+	| _ -> raise NotConvertible)
+
     (* Eta-expansion on the fly *)
+
     | (FLambda _, _) ->
-        let () = match v1 with
-        | [] -> ()
-        | _ ->
-          anomaly (Pp.str "conversion was given unreduced term (FLambda)")
-        in
-        let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+      let () = check_lambda_args v1 in
+      let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
 	eqappr CONV l2r infos
 	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
+
     | (_, FLambda _) ->
-        let () = match v2 with
-        | [] -> ()
-        | _ ->
-	  anomaly (Pp.str "conversion was given unreduced term (FLambda)")
-	in
-        let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+      let () = check_lambda_args v2 in
+      let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
 	eqappr CONV l2r infos
 	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
-
-    (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, c2)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
-           | None -> 
-	     match c2 with
-	     | FConstruct ((ind2,j2),u2) ->
-	       (try
- 	     	  let v2, v1 =
- 	     	    eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
- 	     	  in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
- 	     	with Not_found -> raise NotConvertible)
-	     | _ -> raise NotConvertible)
-
-    | (c1, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
-           | None -> 
-	     match c1 with
-	     | FConstruct ((ind1,j1),u1) ->
- 	       (try let v1, v2 =
-	     	      eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-	     	    in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-	     	with Not_found -> raise NotConvertible)
-	     | _ -> raise NotConvertible)
 	  
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
-- 
cgit v1.2.3