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, 11 insertions, 6 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2b6261169e..d70ce83a80 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -716,15 +716,14 @@ let strip_update_shift_app head stk =
 
 let get_nth_arg head n stk =
   assert (head.norm <> Red);
-  let rec strip_rec rstk h depth n = function
+  let rec strip_rec rstk h n = function
     | Zshift(k) as e :: s ->
-        strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
+        strip_rec (e::rstk) (lift_fconstr k h) n s
     | Zapp args::s' ->
         let q = Array.length args in
         if n >= q
         then
-          strip_rec (Zapp args::rstk)
-            {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
+          strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s'
         else
           let bef = Array.sub args 0 n in
           let aft = Array.sub args (n+1) (q-n-1) in
@@ -732,9 +731,9 @@ let get_nth_arg head n stk =
             List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
-        strip_rec rstk (update m (h.norm,h.term)) depth n s
+        strip_rec rstk (update m (h.norm,h.term)) n s
     | s -> (None, List.rev rstk @ s) in
-  strip_rec [] head 0 n stk
+  strip_rec [] head n stk
 
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
@@ -757,6 +756,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 *)