X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=a4908ce7c893141cb040a42e640fb78c7a46e4c3;hb=40a6a2eb15bc50a7fe8f47704ea0244bc9d18ef5;hp=5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf;hpb=04e808fe2e4a18c868af334ad4a2c95b0040e58d;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 5e8ddaf6d..a4908ce7c 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -111,7 +111,7 @@ let add_single_obj uri obj refinement_toolkit =
   let module RT = RefinementTool in
   let obj = 
     if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
-       not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+       not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
     then
       refinement_toolkit.RT.pack_coercion_obj obj
     else
@@ -211,7 +211,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri arity =
+let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -254,14 +254,27 @@ let add_coercion ~add_composites refinement_toolkit uri arity =
         CoercDb.Fun arity
     | _ -> assert false    
   in
-  let already_in = 
+  let already_in_obj src_carr tgt_carr uri obj = 
      List.exists 
       (fun (s,t,ul) -> 
         List.exists 
          (fun u -> 
-           UriManager.eq u uri && 
+           let bo = 
+            match obj with 
+            | Cic.Constant (_, Some bo, _, _, _) -> bo
+            | _ -> assert false
+           in
            CoercDb.eq_carr s src_carr && 
-           CoercDb.eq_carr t tgt_carr) 
+           CoercDb.eq_carr t tgt_carr &&
+           if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+           CicUniv.oblivion_ugraph)
+           then true else
+            (HLog.warn
+              ("Coercions " ^ 
+                UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
+                uri^" are not convertible, but are between the same nodes.\n"^
+                "From now on nification can fail randomly.");
+             false))
          ul)
       (CoercDb.to_list ())
   in
@@ -270,52 +283,46 @@ let add_coercion ~add_composites refinement_toolkit uri arity =
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+       baseuri
+    in
+    let new_coercions = 
+      List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj))
+      new_coercions 
     in
     let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
-    if already_in then
-      (* this if starts here just to be sure the closure function works fine *)
-      begin 
-        assert (new_coercions = []); 
-        HLog.warn
-          (UriManager.string_of_uri uri ^ 
-            " is already declared as a coercion! skipping...");
-        [] 
-      end
-    else
-      begin
-        (* update the DB *)
-        List.iter 
-          (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
-          new_coercions;
-        CoercDb.add_coercion (src_carr, tgt_carr, uri);
-        (* add the composites obj and they eventual lemmas *)
-        let lemmas = 
-          if add_composites then
-            List.fold_left
-              (fun acc (_,_,uri,obj) -> 
-                add_single_obj uri obj refinement_toolkit;
-                uri::acc) 
-              [] new_coercions
-          else
-            []
-        in
-        (* store that composite_uris are related to uri. the first component is
-         * the stuff in the DB while the second is stuff for remove_obj *)
-        (* 
-           prerr_endline ("adding: " ^ 
-             string_of_bool add_composites ^ UriManager.string_of_uri uri);
-           List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-            composite_uris; 
-        *)
-        UriManager.UriHashtbl.add coercion_hashtbl uri 
-          (composite_uris,if add_composites then composite_uris else []);
-        (*
-        prerr_endline ("lemmas:");
-          List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-          lemmas;
-        prerr_endline ("lemmas END");*)
-        lemmas
-      end
+    (* update the DB *)
+    List.iter 
+      (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
+      new_coercions;
+    CoercDb.add_coercion (src_carr, tgt_carr, uri);
+    (* add the composites obj and they eventual lemmas *)
+    let lemmas = 
+      if add_composites then
+        List.fold_left
+          (fun acc (_,tgt,uri,obj) -> 
+            add_single_obj uri obj refinement_toolkit;
+            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+             (uri,arity)::acc) 
+          [] new_coercions
+      else
+        []
+    in
+    (* store that composite_uris are related to uri. the first component is
+     * the stuff in the DB while the second is stuff for remove_obj *)
+    (* 
+       prerr_endline ("adding: " ^ 
+         string_of_bool add_composites ^ UriManager.string_of_uri uri);
+       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+        composite_uris; 
+    *)
+    UriManager.UriHashtbl.add coercion_hashtbl uri 
+      (composite_uris,if add_composites then composite_uris else []);
+    (*
+    prerr_endline ("lemmas:");
+      List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+      lemmas;
+    prerr_endline ("lemmas END");*)
+    lemmas
 ;;
 
 let remove_coercion uri =
@@ -357,14 +364,19 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+              (*CSC: I think there is a bug here. The composite coercions
+                are not remembered in the .moo file. Thus they are re-generated
+                every time. Right? *)
               let x = 
                 add_coercion ~add_composites:true refinement_toolkit uri arity
+		 (UriManager.buri_of_uri uri)
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
   prerr_endline "---";
 *)
-              x
+              (*CSC: I throw the arity away. See comment above *)
+              List.map fst x
             end
           else  
             []