checker: add eta-expansion

Backport of changes introduced in r13443 and r13494.

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

3 files changed, 35 insertions, 12 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index bd7347134..58c80b521 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -651,6 +651,12 @@ let rec get_args n tys f e stk =
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
+(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
+let rec eta_expand_stack = function
+  | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+      e :: eta_expand_stack s
+  | [] ->
+      [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
 
 (* Iota reduction: extract the arguments to be passed to the Case
    branches *)
diff --git a/checker/closure.mli b/checker/closure.mli
index 8556f26af..707a51f9c 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -120,6 +120,7 @@ type stack_member =
 and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
+val eta_expand_stack : stack -> stack
 
 (* To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
diff --git a/checker/reduction.ml b/checker/reduction.ml
index d8749f072..df3891695 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -268,20 +268,10 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 		    | None -> raise NotConvertible) in
           eqappr univ cv_pb infos app1 app2)
 
-    (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, _)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
-           | None -> raise NotConvertible)
-    | (_, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
-           | None -> raise NotConvertible)
-
     (* other constructors *)
     | (FLambda _, FLambda _) ->
+        (* Inconsistency: we tolerate that v1, v2 contain shift and update but
+           we throw them away *)
         assert (is_empty_stack v1 && is_empty_stack v2);
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
@@ -294,6 +284,32 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
         ccnv univ CONV infos el1 el2 c1 c'1;
         ccnv univ cv_pb infos (el_lift el1) (el_lift el2) c2 c'2
 
+    (* Eta-expansion on the fly *)
+    | (FLambda _, _) ->
+        if v1 <> [] then
+          anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+        eqappr univ CONV infos
+          (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
+    | (_, FLambda _) ->
+        if v2 <> [] then
+          anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+        eqappr univ CONV infos
+          (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
+
+    (* only one constant, defined var or defined rel *)
+    | (FFlex fl1, _)      ->
+        (match unfold_reference infos fl1 with
+           | Some def1 ->
+	       eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
+           | None -> raise NotConvertible)
+    | (_, FFlex fl2)      ->
+        (match unfold_reference infos fl2 with
+           | Some def2 ->
+	       eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
+           | None -> raise NotConvertible)
+
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
      | (FInd ind1, FInd ind2) ->