X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=e1b73821bc6176014ca5c55bb30474858b126f30;hb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;hp=a09baafe1a99fe8e3fdc1aeed08451bbc706dd9d;hpb=ba48c24f4edb0701a0aa346466f2a4211f719ab2;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a09baafe1..e1b73821b 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -59,6 +59,12 @@ let paths_and_uris_of_obj uri =
   xmlunivgraphpath, univgraphuri
 
 let save_object_to_disk uri obj ugraph univlist =
+  let write f x =
+    if not (Helm_registry.get_opt_default 
+              Helm_registry.bool "matita.nodisk" ~default:false) 
+    then      
+      f x
+  in
   let ensure_path_exists path =
     let dir = Filename.dirname path in
     HExtlib.mkdir dir
@@ -74,11 +80,11 @@ let save_object_to_disk uri obj ugraph univlist =
       xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri 
   in
-  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
+  write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
-  ensure_path_exists xmlpath;
-  Xml.pp ~gzip:true xml (Some xmlpath);
-  CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
+  write ensure_path_exists xmlpath;
+  write (Xml.pp ~gzip:true xml) (Some xmlpath);
+  write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
   (* we return a list of uri,path we registered/created *)
   (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
@@ -86,8 +92,8 @@ let save_object_to_disk uri obj ugraph univlist =
     (match bodyxml,bodyuri with
        None,_ -> []
      | Some bodyxml,Some bodyuri->
-         ensure_path_exists xmlbodypath;
-         Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+         write ensure_path_exists xmlbodypath;
+         write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
          [bodyuri, xmlbodypath]
      | _-> assert false) 
 
@@ -217,60 +223,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 +318,16 @@ 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 +366,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