parameter sintax added to axiom statement

[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 36c114d8f8f85fff695a01040ec3185e83934247..fca316fa3a6a238eae3c1c4d52206ec0d7226da4 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -302,21 +302,25 @@ and beta_expand_many test_equality_only metasenv subst context t args ugraph =
   in
     subst,metasenv,hd,ugraph
 
-and warn_if_not_unique xxx to1 to2 carr car1 car2 =
+and warn_if_not_unique xxx car1 car2 =
+  let unopt = 
+    function 
+    | Some (_,Cic.Appl(Cic.Const(u,_)::_)) -> UriManager.string_of_uri u 
+    | Some (_,t) -> CicPp.ppterm t 
+    | None -> "id"
+  in
   match xxx with
   | [] -> ()
-  | (m2,_,c2,c2')::_ ->
-     let m1,c1,c1' = carr,to1,to2 in
-     let unopt = 
-       function Some (_,t) -> CicPp.ppterm t 
-       | None -> "id"
-     in
+  | _ -> 
      HLog.warn 
-       ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
-       CoercDb.string_of_carr car2^": " ^ 
-       CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
-       unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
-       unopt c2^" + "^unopt c2')
+       ("There are "^string_of_int (List.length xxx + 1)^
+        " minimal joins of "^ CoercDb.string_of_carr car1^" and "^
+       CoercDb.string_of_carr car2^": " ^
+     String.concat " and "
+       (List.map 
+          (fun (m2,_,c2,c2') ->
+          " via "^CoercDb.string_of_carr m2^" via "^unopt c2^" + "^unopt c2')
+          xxx))
 
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a
@@ -666,7 +670,7 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl
                        let subst',metasenv,ugraph =
 (*DEBUGGING ONLY:
 prerr_endline 
-  ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ 
+  ("conclude: " ^ 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
@@ -674,19 +678,33 @@ prerr_endline
                        in
                        if subst = subst' then raise exn 
                        else
-(*DEBUGGING ONLY:
+(*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:
+(*DEBUGGING ONLY: 
 in
 (prerr_endline 
-  (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+  ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
    " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 res)
 *)
                       in
+(*DEBUGGING ONLY: 
+prerr_endline (Printf.sprintf 
+"Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s
+last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n"
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context)
+(CoercDb.string_of_carr car1)
+(CoercDb.string_of_carr car2)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context)
+(CoercDb.string_of_carr head1_c)
+(CoercDb.string_of_carr head2_c)
+);
+*)
                       if CoercDb.eq_carr car1 car2 then
                          match last_tl1,last_tl2 with
                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
@@ -730,10 +748,10 @@ res)
                            CoercGraph.meets 
                             metasenv subst context (grow1,car1) (grow2,car2)
                         in
-                        (match meets with
-                        | [] -> raise exn
-                        | (carr,metasenv,to1,to2)::xxx -> 
-                           warn_if_not_unique xxx to1 to2 carr car1 car2;
+                        (match
+                        HExtlib.list_findopt
+                          (fun (carr,metasenv,to1,to2) meet_no ->
+                             try
                            let last_tl1',(subst,metasenv,ugraph) =
                             match grow1,to1 with
                              | true,Some (last,coerced) -> 
@@ -750,7 +768,18 @@ res)
                                   metasenv coerced last_tl2 ugraph
                              | _ -> last_tl2,(subst,metasenv,ugraph)
                            in
-                           conclude subst metasenv ugraph last_tl1' last_tl2')
+                           if meet_no > 0 then
+                             HLog.warn ("Using pullback number " ^ string_of_int
+                               meet_no);
+                           Some 
+                            (conclude subst metasenv ugraph last_tl1' last_tl2')
+                             with
+                             | UnificationFailure _ 
+                             | Uncertain _ -> None)
+                          meets
+                        with
+                        | Some x -> x
+                        | None -> raise exn)
                         (* }}} pullback *)
                   (* {{{ CSC: This is necessary because of the "elim H" tactic
                          where the type of H is only reducible to an
@@ -953,7 +982,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppcontext ~metasenv subst context)
-    (CicMetaSubst.ppmetasenv subst metasenv)
+    ("OMITTED" (*CicMetaSubst.ppmetasenv subst metasenv*))
     (Lazy.force msg)
  )