Added eta-expansion in kernel, type inference and tactic unification,

governed in the latter case by a flag since (useful e.g. for setoid
rewriting which otherwise loops as it is implemented).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 46 insertions, 10 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c26e92fd2d..df0fc161ad 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -174,6 +174,8 @@ let rec evar_conv_x env evd pbty term1 term2 =
   match ground_test with
       Some b -> (evd,b)
     | None ->
+	(* Until pattern-unification is used consistently, use nohdbeta to not
+	   destroy beta-redexes that can be used for 1st-order unification *)
         let term1 = apprec_nohdbeta env evd term1 in
         let term2 = apprec_nohdbeta env evd term2 in
         if is_undefined_evar evd term1 then
@@ -241,13 +243,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                   (fun i -> evar_conv_x env i CONV) l1 rest2);
                (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
           else (i,false)
-	and f4 i =
+	and f2 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f4]
+	ise_try evd [f1; f2]
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
@@ -273,13 +275,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                   (fun i -> evar_conv_x env i CONV) rest1 l2);
                (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
           else (i,false)
-	and f4 i =
+	and f2 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f4]
+	ise_try evd [f1; f2]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f1 i =
@@ -319,6 +321,25 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in
 	ise_try evd [f1; f2; f3]
 
+    (* Eta-expansion *)
+    | Rigid c1, (Flexible _ | MaybeFlexible _) when isLambda c1 ->
+	assert (l1 = []);
+	let (na,c1,c'1) = destLambda c1 in
+        let c = nf_evar evd c1 in
+	let env' = push_rel (na,None,c) env in
+        let appr1 = evar_apprec env' evd [] c'1 in
+	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
+	evar_eqappr_x env' evd CONV appr1 appr2
+
+    | (Flexible _ | MaybeFlexible _), Rigid c2 when isLambda c2 ->
+	assert (l2 = []);
+	let (na,c2,c'2) = destLambda c2 in
+        let c = nf_evar evd c2 in
+	let env' = push_rel (na,None,c) env in
+	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
+        let appr2 = evar_apprec env' evd [] c'2 in
+	evar_eqappr_x env' evd CONV appr1 appr2
+
     | Flexible ev1, Rigid _ ->
 	if
 	  is_unification_pattern_evar env ev1 l1 (applist appr2) &
@@ -384,7 +405,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
             (evd,base_sort_cmp pbty s1 s2)
 
-	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] ->
+	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) ->
+	    assert (l1=[] & l2=[]);
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
@@ -464,11 +486,25 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
             else (evd,false)
 
-	| (Meta _ | Lambda _), _ -> (evd,false)
-	| _, (Meta _ | Lambda _) -> (evd,false)
-
-	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
-	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
+	(* Eta-expansion *)
+	| Lambda (na,c1,c'1), _ ->
+	    assert (l1 = []);
+            let c = nf_evar evd c1 in
+	    let env' = push_rel (na,None,c) env in
+            let appr1 = evar_apprec env' evd [] c'1 in
+	    let appr2 = (lift 1 c2, List.map (lift 1) l2 @ [mkRel 1]) in
+	    evar_eqappr_x env' evd CONV appr1 appr2
+
+	| _, Lambda (na,c2,c'2) ->
+	    assert (l2 = []);
+            let c = nf_evar evd c2 in
+	    let env' = push_rel (na,None,c) env in
+	    let appr1 = (lift 1 c1, List.map (lift 1) l1 @ [mkRel 1]) in
+            let appr2 = evar_apprec env' evd [] c'2 in
+	    evar_eqappr_x env' evd CONV appr1 appr2
+
+	| (Meta _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
+	| _, (Meta _ | Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
 
 	| (App _ | Case _ | Fix _ | CoFix _),
 	  (App _ | Case _ | Fix _ | CoFix _) -> (evd,false)