compare_stack_shape before ise_stack2 in evar_conv

+ revert r16130

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

3 files changed, 54 insertions, 34 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d6aa6d5d..497c3b9df 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -152,6 +152,12 @@ let ise_and evd l =
    it reaches the end of a list, it returns the remaining elements in
    the other list if there are some.
 *)
+let ise_exact ise x1 x2 =
+  match ise x1 x2 with
+  | None, out -> out
+  | _, (UnifFailure _ as out) -> out
+  | Some _, Success i -> UnifFailure (i,NotSameArgSize)
+
 let generic_ise_list2 i f l1 l2 =
   let rec aux i l1 l2 =
     match l1,l2 with
@@ -166,10 +172,7 @@ let generic_ise_list2 i f l1 l2 =
 
 (* Same but the 2 lists must have the same length *)
 let ise_list2 evd f l1 l2 =
-  match generic_ise_list2 evd f l1 l2 with
-  | None, out -> out
-  | _, (UnifFailure _ as out) -> out
-  | Some _, Success i -> UnifFailure (i,NotSameArgSize)
+  ise_exact (generic_ise_list2 evd f) l1 l2
 
 let ise_array2 evd f v1 v2 =
   let rec allrec i = function
@@ -204,7 +207,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         match ise_and i [
 	  (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
 	  (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
-	  (fun i -> ise_list2 i (fun ii -> f env ii CONV) a1 a2)] with
+	  (fun i -> ise_exact (ise_stack2 false i) a1 a2)] with
         | Success i' -> ise_stack2 true i' q1 q2
         | UnifFailure _ as x -> fail x
       else fail (UnifFailure (i,NotSameHead))
@@ -228,7 +231,9 @@ let ise_stack2 no_app env evd f sk1 sk2 =
 
 (* Make sure that the matching suffix is the all stack *)
 let exact_ise_stack2 env evd f sk1 sk2 =
-  match ise_stack2 false env evd f sk1 sk2 with | None, out -> out | _ -> UnifFailure (evd, NotSameArgSize)
+  if Reductionops.compare_stack_shape sk1 sk2 then
+    ise_exact (ise_stack2 false env evd f) sk1 sk2
+  else UnifFailure (evd, (* Dummy *) NotSameHead)
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -587,17 +592,19 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
 	 (i', ev :: ks, m - 1))
       (evd,[],List.length bs - 1) bs
   in
+  if Reductionops.compare_stack_shape ts ts1 then
   ise_and evd'
     [(fun i ->
-      ise_list2 i
-        (fun i' x1 x -> evar_conv_x trs env i' CONV x1 (substl ks x))
-        params1 params);
-     (fun i ->
        ise_list2 i
-         (fun i' u1 u -> evar_conv_x trs env i' CONV u1 (substl ks u))
-         us2 us);
-     (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
-     (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))))]
+         (fun i' x1 x -> evar_conv_x trs env i' CONV x1 (substl ks x))
+         params1 params);
+    (fun i ->
+      ise_list2 i
+        (fun i' u1 u -> evar_conv_x trs env i' CONV u1 (substl ks u))
+        us2 us);
+    (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))));
+    (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1)]
+  else UnifFailure(evd,(*dummy*)NotSameHead)
 
 (* We assume here |l1| <= |l2| *)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0f8f6434f..7b1a514ed 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -31,11 +31,26 @@ exception Elimconst
 type 'a stack_member =
   | Zapp of 'a list
   | Zcase of case_info * 'a * 'a array * ('a * 'a list) option
-  | Zfix of fixpoint * 'a list * ('a * 'a list) option
+  | Zfix of fixpoint * 'a stack * ('a * 'a list) option
   | Zshift of int
   | Zupdate of 'a
 and 'a stack = 'a stack_member list
 
+let compare_stack_shape stk1 stk2 =
+  let rec compare_rec bal stk1 stk2 =
+  match (stk1,stk2) with
+      ([],[]) -> Int.equal bal 0
+    | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
+    | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
+    | (Zapp l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2
+    | (_, Zapp l2::s2) -> compare_rec (bal-List.length l2) stk1 s2
+    | (Zcase(c1,_,_,_)::s1, Zcase(c2,_,_,_)::s2) ->
+        Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
+    | (Zfix(_,a1,_)::s1, Zfix(_,a2,_)::s2) ->
+        Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
+    | (_,_) -> false in
+  compare_rec 0 stk1 stk2
+
 let empty_stack = []
 let append_stack_app_list l s =
   match (l,s) with
@@ -111,9 +126,9 @@ let rec zip ?(refold=false) = function
   | f, (Zcase (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
   | f, (Zfix (fix,st,Some(cst, params))::s) when refold -> zip ~refold
     (cst, append_stack_app_list (List.rev params)
-      (append_stack_app_list st (append_stack_app_list [f] s)))
+      (st @ (append_stack_app_list [f] s)))
   | f, (Zfix (fix,st,_)::s) -> zip ~refold
-    (mkFix fix, append_stack_app_list st (append_stack_app_list [f] s))
+    (mkFix fix, st @ (append_stack_app_list [f] s))
   | f, (Zshift n::s) -> zip ~refold (lift n f, s)
   | _ -> assert false
 
@@ -395,7 +410,7 @@ let rec whd_state_gen ?csts refold flags env sigma =
     | Fix ((ri,n),_ as f) ->
       (match strip_n_app ri.(n) stack with
       |None -> fold ()
-      |Some (bef,arg,s') -> whrec noth (arg, Zfix(f,bef,Cst_stack.best_cst cst_l)::s'))
+      |Some (bef,arg,s') -> whrec noth (arg, Zfix(f,[Zapp bef],Cst_stack.best_cst cst_l)::s'))
 
     | Construct (ind,c) ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
@@ -405,7 +420,7 @@ let rec whd_state_gen ?csts refold flags env sigma =
 	|args, (Zfix (f,s',cst)::s'') ->
 	  let x' = applist(x,args) in
 	  whrec noth ((if refold then contract_fix ~env f else contract_fix f) cst,
-		      append_stack_app_list s' (append_stack_app_list [x'] s''))
+		      s' @ (append_stack_app_list [x'] s''))
 	|_ -> fold ()
       else fold ()
 
@@ -458,7 +473,7 @@ let local_whd_state_gen flags sigma =
     | Fix ((ri,n),_ as f) ->
       (match strip_n_app ri.(n) stack with
       |None -> s
-      |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s'))
+      |Some (bef,arg,s') -> whrec (arg, Zfix(f,[Zapp bef],None)::s'))
 
     | Evar ev ->
       (match safe_evar_value sigma ev with
@@ -477,7 +492,7 @@ let local_whd_state_gen flags sigma =
 	  whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	|args, (Zfix (f,s',cst)::s'') ->
 	  let x' = applist(x,args) in
-	  whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
+	  whrec (contract_fix f cst, s' @ (append_stack_app_list [x'] s''))
 	|_ -> s
       else s
 
@@ -664,7 +679,7 @@ let whd_betaiota_preserving_vm_cast env sigma t =
 	     whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	   |args, (Zfix (f,s',cst)::s'') ->
 	     let x' = applist(x,args) in
-	     whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
+	     whrec (contract_fix f cst,s' @ (append_stack_app_list [x'] s''))
 	   |_ -> s
        end
 
@@ -960,14 +975,14 @@ let whd_programs_stack env sigma =
       | Fix ((ri,n),_ as f) ->
 	(match strip_n_app ri.(n) stack with
 	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s'))
+	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,[Zapp bef],None)::s'))
       | Construct (ind,c) -> begin
 	match strip_app stack with
 	  |args, (Zcase(ci, _, lf,_)::s') ->
 	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	  |args, (Zfix (f,s',cst)::s'') ->
 	    let x' = applist(x,args) in
-	    whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
+	    whrec (contract_fix f cst,s' @ (append_stack_app_list [x'] s''))
 	  |_ -> s
       end
       | CoFix cofix -> begin
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d4bb9aabf..3ffb73505 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -17,21 +17,19 @@ open Closure
 
 exception Elimconst
 
-(***********************************************************************
-  s A [stack] is a context of arguments, arguments are pushed by
-   [append_stack] one array at a time but popped with [decomp_stack]
-   one by one *)
-
+(** 90% copy-paste of kernel/closure.ml but polymorphic and with extra
+    arguments for storing refold *)
 type 'a stack_member =
-  | Zapp of 'a list
-  | Zcase of case_info * 'a * 'a array * ('a * 'a list) option
-  | Zfix of fixpoint * 'a list * ('a * 'a list) option
-  | Zshift of int
-  | Zupdate of 'a
+| Zapp of 'a list
+| Zcase of case_info * 'a * 'a array * ('a * 'a list) option
+| Zfix of fixpoint * 'a stack * ('a * 'a list) option
+| Zshift of int
+| Zupdate of 'a
 
 and 'a stack = 'a stack_member list
 
 val empty_stack : 'a stack
+val compare_stack_shape : 'a stack -> 'a stack -> bool
 val append_stack_app : 'a array -> 'a stack -> 'a stack
 val append_stack_app_list : 'a list -> 'a stack -> 'a stack