X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=a59294aaa73f7eb3173b1d6047809f27061fee76;hb=ae4ac93251c1a7178220d293a2a8ae9dc850fde3;hp=413cc986cbbc6188994a2e13f0c10e407e046b31;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 413cc986c..a59294aaa 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -217,60 +217,75 @@ let add_coercion ~add_composites refinement_toolkit uri =
     in
     aux ty
   in
+  let already_in = 
+     List.exists 
+      (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+      (CoercDb.to_list ())
+  in
   let ty_src, ty_tgt = extract_last_two_p coer_ty in
   let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
   let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
-  let new_coercions = 
-    CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri in
-  let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
-  (* update the DB *)
-  List.iter 
-    (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
-      new_coercions;
-  if 
-    List.exists 
-      (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr)
-      (CoercDb.to_list ())
-  then
-    begin
-      assert (new_coercions = []);
-      []
-    end
+  if not add_composites then
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
-    begin
-      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) 
-            composite_uris 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 []);
-      lemmas
-    end
+    let new_coercions = 
+      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+    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
+;;
 
 let remove_coercion uri =
   try
     let (composites_in_db, composites_in_lib) = 
       UriManager.UriHashtbl.find coercion_hashtbl uri 
     in
-    prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+    (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-      composites_in_db;
+      composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
     CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
     (* remove from the DB *) 
@@ -297,7 +312,15 @@ let generate_projections refinement_toolkit uri fields =
         add_single_obj uri obj refinement_toolkit;
         let composites = 
          if coercion then
-            add_coercion ~add_composites:true refinement_toolkit uri
+            begin
+              prerr_endline ("composite for " ^ UriManager.string_of_uri uri);
+              let x = add_coercion ~add_composites:true refinement_toolkit uri
+              in
+              prerr_endline ("are: ");
+              List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+              prerr_endline "---";
+              x
+            end
           else  
             []
         in
@@ -336,7 +359,7 @@ let add_obj refinement_toolkit uri obj =
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @ 
           generate_elimination_principles uri refinement_toolkit;
-	uris := !uris @ generate_inversion refinement_toolkit uri obj;
+        uris := !uris @ generate_inversion refinement_toolkit uri obj;
         let rec get_record_attrs =
           function
           | [] -> None