1 files changed, 65 insertions, 4 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 987db88b18..e3b8a166c7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -951,16 +951,77 @@ let base_sort_cmp pb s0 s1 =
     | _ -> false
 
 (* eq_constr extended with universe erasure *)
-let rec constr_cmp cv_pb t1 t2 =
+let compare_constr_univ f cv_pb t1 t2 = 
   match kind_of_term t1, kind_of_term t2 with
       Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
     | Prod (_,t1,c1), Prod (_,t2,c2) -> 
-	constr_cmp Reduction.CONV t1 t2 & 
-	  constr_cmp cv_pb c1 c2
-    | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2
+	f Reduction.CONV t1 t2 & f cv_pb c1 c2
+    | _ -> compare_constr (f Reduction.CONV) t1 t2
+
+let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
 
 let eq_constr = constr_cmp Reduction.CONV
 
+(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
+   App(c,[||]) -> ([],c) *)
+let split_app c = match kind_of_term c with
+    App(c,l) -> 
+      let len = Array.length l in
+      if len=0 then ([],c) else
+	let last = Array.get l (len-1) in
+	let prev = Array.sub l 0 (len-1) in
+	c::(Array.to_list prev), last
+  | _ -> assert false
+
+let hdtl l = List.hd l, List.tl l
+
+type subst = (rel_context*constr) Intmap.t
+
+exception CannotFilter
+
+let filtering env cv_pb c1 c2 =
+  let evm = ref Intmap.empty in
+  let define cv_pb e1 ev c1 = 
+    try let (e2,c2) = Intmap.find ev !evm in
+    let shift = List.length e1 - List.length e2 in
+    if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+    with Not_found -> 
+      evm := Intmap.add ev (e1,c1) !evm
+  in
+  let rec aux env cv_pb c1 c2 =
+    match kind_of_term c1, kind_of_term c2 with
+      | App _, App _ -> 
+	  let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+	  aux env cv_pb l1 l2; if p1=[] & p2=[] then () else
+	      aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2))
+      | Prod (n,t1,c1), Prod (_,t2,c2) ->
+	  aux env cv_pb t1 t2;
+	  aux ((n,None,t1)::env) cv_pb c1 c2
+      | _, Evar (ev,_) -> define cv_pb env ev c1
+      | Evar (ev,_), _ -> define cv_pb env ev c2
+      | _ -> 
+	  if compare_constr_univ 
+	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then () 
+	  else raise CannotFilter
+	  (* TODO: le reste des binders *)
+  in
+  aux env cv_pb c1 c2; !evm
+
+let decompose_prod_letin : constr -> int * rel_context * constr = 
+  let rec prodec_rec i l c = match kind_of_term c with
+    | Prod (n,t,c)    -> prodec_rec (succ i) ((n,None,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+    | Cast (c,_,_)    -> prodec_rec i l c
+    | _               -> i,l,c in
+  prodec_rec 0 []
+
+let align_prod_letin c a : rel_context * constr =
+  let (lc,_,_) = decompose_prod_letin c in
+  let (la,l,a) = decompose_prod_letin a in
+  if not (la >= lc) then invalid_arg "align_prod_letin";
+  let (l1,l2) = Util.list_chop lc l in
+  l2,it_mkProd_or_LetIn a l1
+    
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 versions précédentes buggées                  *)