Fix bug #2989: make unification.ml able to deal with canonical structure in any context

+ reindenting noise

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

4 files changed, 69 insertions, 41 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 52c930e62..2d21fb0e7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -583,27 +583,27 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       end
 
 and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
-  let (evd',ks,_) =
-    List.fold_left
-      (fun (i,ks,m) b ->
-	 if Int.equal m n then (i,t2::ks, m-1) else
-	 let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
-         let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
-	 (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 -> 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)]
+    let (evd',ks,_) =
+      List.fold_left
+	(fun (i,ks,m) b ->
+	  if Int.equal m n then (i,t2::ks, m-1) else
+	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
+            let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
+	    (i', ev :: ks, m - 1))
+	(evd,[],List.length bs - 1) bs
+    in
+    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 -> 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 24ae6c1d0..6a94fa109 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -51,6 +51,31 @@ let compare_stack_shape stk1 stk2 =
     | (_,_) -> false in
   compare_rec 0 stk1 stk2
 
+let fold_stack2 f o sk1 sk2 =
+  let rec aux o lft1 sk1 lft2 sk2 =
+  let fold_array =
+    Array.fold_left2 (fun a x y -> f a (Term.lift lft1 x) (Term.lift lft2 y))
+  in
+  match sk1,sk2 with
+  | [], [] -> o,lft1,lft2
+  | Zshift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2
+  | _, Zshift n :: q2 -> aux o lft1 sk1 (lft2+n) q2
+  | Zapp [] :: q1, _ -> aux o lft1 q1 lft2 sk2
+  | _, Zapp [] :: q2 -> aux o lft1 sk1 lft2 q2
+  | Zapp (t1::l1) :: q1, Zapp (t2::l2) :: q2 ->
+    aux (f o (Term.lift lft1 t1) (Term.lift lft2 t2))
+      lft1 (Zapp l1 :: q1) lft2 (Zapp l2 :: q2)
+  | Zcase (_,t1,a1,_) :: q1, Zcase (_,t2,a2,_) :: q2 ->
+    aux (fold_array
+	   (f o (Term.lift lft1 t1) (Term.lift lft2 t2))
+	   a1 a2) lft1 q1 lft2 q2
+  | Zfix ((_,(_,a1,b1)),s1,_) :: q1, Zfix ((_,(_,a2,b2)),s2,_) :: q2 ->
+    let (o',_,_) = aux (fold_array (fold_array o b1 b2) a1 a2)
+      lft1 s1 lft2 s2 in
+    aux o' lft1 q1 lft2 q2
+  | _, _ -> raise (Invalid_argument "Reductionops.fold_stack2")
+  in aux o 0 (List.rev sk1) 0 (List.rev sk2)
+
 let empty_stack = []
 let append_stack_app_list l s =
   match (l,s) with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 3ffb73505..1914b3b1e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -30,6 +30,10 @@ and 'a stack = 'a stack_member list
 
 val empty_stack : 'a stack
 val compare_stack_shape : 'a stack -> 'a stack -> bool
+(** [fold_stack2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
+@return the result and the lifts to apply on the terms *)
+val fold_stack2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a ->
+  Term.constr stack -> Term.constr stack -> 'a * int * int
 val append_stack_app : 'a array -> 'a stack -> 'a stack
 val append_stack_app_list : 'a list -> 'a stack -> 'a stack
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ec6eeea12..31148ee39 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -617,29 +617,28 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       try Evarconv.check_conv_record f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
-    let (evd,ks,_) =
-      List.fold_left
-	(fun (evd,ks,m) b ->
-	  if Int.equal m n then (evd,t2::ks, m-1) else
-            let mv = new_meta () in
-	    let evd' = meta_declare mv (substl ks b) evd in
+    if Reductionops.compare_stack_shape ts ts1 then
+      let (evd,ks,_) =
+	List.fold_left
+	  (fun (evd,ks,m) b ->
+	    if Int.equal m n then (evd,t2::ks, m-1) else
+              let mv = new_meta () in
+	      let evd' = meta_declare mv (substl ks b) evd in
 	      (evd', mkMeta mv :: ks, m - 1))
-	(sigma,[],List.length bs - 1) bs
-    in
-    let unilist2 f substn l l' =
-      try List.fold_left2 f substn l l'
-      with Invalid_argument "List.fold_left2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
-    in
-    let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
-      (evd,ms,es) us2 us in
-    let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
-      substn params1 params in
-    match Option.lift2 (unilist2 (unirec_rec curenvnb pb b false) substn)
-      (list_of_app_stack ts) (list_of_app_stack ts1) with
-      |Some substn ->
+	  (sigma,[],List.length bs - 1) bs
+      in
+      let unilist2 f substn l l' =
+	try List.fold_left2 f substn l l'
+	with Invalid_argument "List.fold_left2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
+      in
+      let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
+	(evd,ms,es) us2 us in
+      let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
+	substn params1 params in
+	let (substn,_,_) = Reductionops.fold_stack2 (unirec_rec curenvnb pb b false) substn ts ts1 in
 	unirec_rec curenvnb pb b false substn c1 (applist (c,(List.rev ks)))
-      |None -> anomaly (Pp.str "As expected, solve_canonical_projection breaks the term too much")
-  in
+    else error_cannot_unify (fst curenvnb) sigma (cM,cN)
+      in
   let evd = sigma in
     if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n
         || subterm_restriction conv_at_top flags then false