term refinement almost done, some functions exported from the kernel since they were...

[helm.git] / helm / software / components / cic_unification / cicUnification.ml

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 54e7fc5f25bd9cfdadd9f01582a25d941ccd4755..36c114d8f8f85fff695a01040ec3185e83934247 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -620,12 +620,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
 (*DEBUGGING ONLY:
 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 *)
-                     let inner_coerced t =
+                     let inner_coerced ?(skip_non_c=false) t =
                       let t = CicMetaSubst.apply_subst subst t in
                       let rec aux c x t =
                         match t with
                         | Cic.Appl l -> 
                             (match CoercGraph.coerced_arg l with
+                            | None when skip_non_c -> 
+                                aux c (HExtlib.list_last l)            
+                                 (HExtlib.list_last l)            
                             | None -> c, x
                             | Some (t,_) -> aux (List.hd l) t t)
                         | _ ->  c, x
@@ -659,6 +662,31 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl
                               (Cic.Appl (bo::args))
                         | _ -> assert false
                       in
+                      let conclude subst metasenv ugraph last_tl1' last_tl2' =
+                       let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline 
+  ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ 
+   " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+                        fo_unif_subst test_equality_only subst context
+                         metasenv last_tl1' last_tl2' ugraph
+                       in
+                       if subst = subst' then raise exn 
+                       else
+(*DEBUGGING ONLY:
+let subst,metasenv,ugrph as res = 
+*)
+                        fo_unif_subst test_equality_only subst' context
+                         metasenv (C.Appl l1) (C.Appl l2) ugraph
+(*DEBUGGING ONLY:
+in
+(prerr_endline 
+  (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+   " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
+                      in
                       if CoercDb.eq_carr car1 car2 then
                          match last_tl1,last_tl2 with
                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
@@ -671,55 +699,35 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl
                             fo_unif_subst test_equality_only subst context
                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
                          | _ when CoercDb.eq_carr head1_c head2_c ->
-                           let l1, l2 = 
                              (* composite VS composition + metas avoiding
                               * coercions not only in coerced position    *)
-                             if c1 = cc1 then 
-                               unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
-                             else if c2 = cc2 then
-                               Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
-                             else raise exn
-                           in
-                            fo_unif_subst test_equality_only subst context
-                             metasenv l1 l2 ugraph
+                             if c1 <> cc1 && c2 <> cc2 then
+                               conclude subst metasenv ugraph
+                                last_tl1 last_tl2
+                             else
+                              let l1, l2 = 
+                               if c1 = cc1 then 
+                                 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+                               else
+                                 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+                              in
+                               fo_unif_subst test_equality_only subst context
+                                metasenv l1 l2 ugraph
                          | _ -> raise exn
                       else
-                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
-                        let subst',metasenv,ugraph =
-(*DEBUGGING ONLY:
-prerr_endline 
-  ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ 
-   " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
-*)
-                         fo_unif_subst test_equality_only subst context
-                          metasenv last_tl1' last_tl2' ugraph
-                        in
-                        if subst = subst' then raise exn 
-                        else
-(*DEBUGGING ONLY:
-let subst,metasenv,ugraph as res = 
-*)
-                         fo_unif_subst test_equality_only subst' context
-                          metasenv (C.Appl l1) (C.Appl l2) ugraph
-(*DEBUGGING ONLY:
-in
-(prerr_endline 
-  (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
-   " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-res)
-*)
-                       in
-                       let grow1 =
-                         match last_tl1 with Cic.Meta _ -> true | _ -> false in
-                       let grow2 =
-                         match last_tl2 with Cic.Meta _ -> true | _ -> false in
-                       if not (grow1 || grow2) then
-                          (* no flexible terminals -> no pullback, but
-                           * we still unify them, in some cases it helps *)
-                          conclude subst metasenv ugraph last_tl1 last_tl2
-                       else
+                      let grow1 =
+                        match last_tl1 with Cic.Meta _ -> true | _ -> false in
+                      let grow2 =
+                        match last_tl2 with Cic.Meta _ -> true | _ -> false in
+                      if not (grow1 || grow2) then
+                        let _,last_tl1 = 
+                          inner_coerced ~skip_non_c:true (Cic.Appl l1) in 
+                        let _,last_tl2 = 
+                          inner_coerced ~skip_non_c:true  (Cic.Appl l2) in
+                        conclude subst metasenv ugraph last_tl1 last_tl2
+                      else
                         let meets = 
-                          CoercGraph.meets 
+                           CoercGraph.meets 
                             metasenv subst context (grow1,car1) (grow2,car2)
                         in
                         (match meets with