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

3 files changed, 60 insertions, 12 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c26e92fd2..df0fc161a 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)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5b8fc591e..b45d23098 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -169,7 +169,8 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
-  use_evars_pattern_unification : bool
+  use_evars_pattern_unification : bool;
+  modulo_eta : bool
 }
 
 let default_unify_flags = {
@@ -178,6 +179,7 @@ let default_unify_flags = {
   modulo_delta = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_eta = true
 }
 
 let default_no_delta_unify_flags = {
@@ -186,6 +188,7 @@ let default_no_delta_unify_flags = {
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
+  modulo_eta = true
 }
 
 let use_evars_pattern_unification flags =
@@ -259,6 +262,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b substn (subst1 a c) cN
 	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b substn cM (subst1 a c)
 
+        (* eta-expansion *)
+	| Lambda (na,t1,c1), _ when flags.modulo_eta ->
+	    unirec_rec (push (na,t1) curenvnb) topconv true substn
+	      c1 (mkApp (lift 1 cN,[|mkRel 1|]))
+	| _, Lambda (na,t2,c2) when flags.modulo_eta ->
+	    unirec_rec (push (na,t2) curenvnb) topconv true substn
+	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
+
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             array_fold_left2 (unirec_rec curenvnb topconv true)
 	      (unirec_rec curenvnb topconv true
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index fa34b428c..cc3040a9e 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,7 +15,8 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
-  use_evars_pattern_unification : bool
+  use_evars_pattern_unification : bool;
+  modulo_eta : bool
 }
 
 val default_unify_flags : unify_flags