X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=716aa04d29f2c6f34e4280cfca3bdf49c2583333;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=3d9d74dccb76ce526869a13404e786b2fa53ea33;hpb=b12aa2f7dc56d9915603339e9a1e1ba23d834b4a;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3d9d74dcc..716aa04d2 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -43,10 +43,22 @@ let alias_diff ~from status =
     status.aliases []
 
 let alias_diff =
- let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status
+ let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 let set_proof_aliases status new_aliases =
+ let commands_of_aliases =
+   List.map
+    (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias))
+ in
+ let deps_of_aliases =
+   HExtlib.filter_map
+    (function
+    | GrafiteAst.Ident_alias (_, suri) ->
+        let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
+        Some (GrafiteAst.Dependency buri)
+    | _ -> None)
+ in
  let aliases =
   List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
    status.aliases new_aliases in
@@ -59,12 +71,15 @@ let set_proof_aliases status new_aliases =
  if new_aliases = [] then
    new_status
  else
-   add_moo_content
-    (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases)
-    new_status
+   let aliases = 
+     DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+   in
+   let status = add_moo_content (commands_of_aliases aliases) new_status in
+   let status = add_moo_metadata (deps_of_aliases aliases) status in
+   status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
- *  (name,uri) that is used to generate authomatic aliases **)
+ *  (name,uri) that is used to generate automatic aliases **)
 let extract_alias types uri = 
   fst(List.fold_left (
     fun (acc,i) (name, _, _, cl) -> 
@@ -106,6 +121,7 @@ let paths_and_uris_of_obj uri status =
   let basedir = get_string_option status "basedir" ^ "/xml" in
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
   let bodyuri = UriManager.bodyuri_of_uri uri in
+  let univgraphuri = UriManager.univgraphuri_of_uri uri in
   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
         (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
   let innertypespath = basedir ^ "/" ^ innertypesfilename in
@@ -115,12 +131,16 @@ let paths_and_uris_of_obj uri status =
   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
         (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
-  xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
+  let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
+        (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
+  let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
+  xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
+  xmlunivgraphpath, univgraphuri
 
-let save_object_to_disk status uri obj =
+let save_object_to_disk status uri obj ugraph univlist =
   let ensure_path_exists path =
     let dir = Filename.dirname path in
-    MatitaMisc.mkdir dir
+    HExtlib.mkdir dir
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj = Cic2acic.plain_acic_object_of_cic_object obj in 
@@ -129,17 +149,19 @@ let save_object_to_disk status uri obj =
    Cic2Xml.print_object
     uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
   in
-  let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = 
+  let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
+      xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri status 
   in
   let path_scheme_of path = "file://" ^ path in
-  List.iter MatitaMisc.mkdir
-    (List.map Filename.dirname [innertypespath; xmlpath]);
+  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
   ensure_path_exists xmlpath;
-  Xml.pp ~gzip:true xml (Some xmlpath) ;
+  Xml.pp ~gzip:true xml (Some xmlpath);
+  CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
   (* we return a list of uri,path we registered/created *)
   (uri,xmlpath) ::
+  (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
        None,None -> []
@@ -150,18 +172,13 @@ let save_object_to_disk status uri obj =
      | _-> assert false) 
 
 let typecheck_obj =
- let profiler = CicUtil.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj
+ let profiler = HExtlib.profile "add_obj.typecheck_obj" in
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
- let profiler = CicUtil.profile "add_obj.index_obj" in
+ let profiler = HExtlib.profile "add_obj.index_obj" in
   fun ~dbd ~uri ->
-   profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-
-let save_object_to_disk =
- let profiler = CicUtil.profile "add_obj.save_object_to_disk" in
-  fun status uri obj ->
-   profiler.CicUtil.profile (save_object_to_disk status uri) obj
+   profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 
 let add_obj uri obj status =
   let dbd = MatitaDb.instance () in
@@ -170,10 +187,12 @@ let add_obj uri obj status =
     command_error (sprintf "%s already defined" suri)
   else begin
     typecheck_obj uri obj; (* 1 *)
+    let _, ugraph, univlist = 
+      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       try
-        let new_stuff = save_object_to_disk status uri obj in (* 3 *)
+        let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*)
         try 
           MatitaLog.message (sprintf "%s defined" suri);
           let status = add_aliases_for_object status suri obj in
@@ -187,12 +206,12 @@ let add_obj uri obj status =
         raise exc
     with exc ->
       CicEnvironment.remove_obj uri; (* -1 *)
-      raise exc
+    raise exc
   end
 
 let add_obj =
- let profiler = CicUtil.profile "add_obj" in
-  fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status
+ let profiler = HExtlib.profile "add_obj" in
+  fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
    
 module OrderedUri =
 struct
@@ -210,13 +229,20 @@ module UriSet = Set.Make (OrderedUri)
 module IdSet  = Set.Make (OrderedId)
 
   (** @return l2 \ l1 *)
-let uri_list_diff l2 l1 =
+let urixstring_list_diff l2 l1 =
   let module S = UriSet in
   let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
   let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
   let diff = S.diff s2 s1 in
   S.fold (fun uri uris -> uri :: uris) diff []
 
+let uri_list_diff l2 l1 =
+  let module S = UriManager.UriSet in
+  let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+  let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+  let diff = S.diff s2 s1 in
+  S.fold (fun uri uris -> uri :: uris) diff []
+
   (** @return l2 \ l1 *)
 let id_list_diff l2 l1 =
   let module S = IdSet in
@@ -229,15 +255,16 @@ let remove_coercion uri =
   CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
   
 let time_travel ~present ~past =
-  let objs_to_remove = uri_list_diff present.objects past.objects in
+  let objs_to_remove = urixstring_list_diff present.objects past.objects in
+  let coercions_to_remove = uri_list_diff present.coercions past.coercions in
   let notation_to_remove =
     id_list_diff present.notation_ids past.notation_ids
   in
   let debug_list = ref [] in
+  List.iter remove_coercion coercions_to_remove;
   List.iter
     (fun (uri,p) -> 
       MatitaMisc.safe_remove p;
-      remove_coercion uri;
       (try 
         CicEnvironment.remove_obj uri
       with CicEnvironment.Object_not_found _ -> 
@@ -276,12 +303,15 @@ let time_travel ~present ~past =
       List.iter MatitaLog.debug l2
       *)
     
-let remove ~verbose uri =
+let last_baseuri = ref ""
+
+let remove ?(verbose=false) uri =
   let derived_uris_of_uri uri =
     UriManager.innertypesuri_of_uri uri ::
+    UriManager.univgraphuri_of_uri uri ::
     (match UriManager.bodyuri_of_uri uri with
     | None -> []
-    | Some u -> [u])
+    | Some u -> [u]) 
   in
   let to_remove =
     uri :: 
@@ -291,9 +321,17 @@ let remove ~verbose uri =
   List.iter 
     (fun uri -> 
       (try
+        (* WARNING: non reentrant debugging code *)
         if verbose then
-         MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri);
-        MatitaMisc.safe_remove (Http_getter.resolve' uri)
+         let baseuri = UriManager.buri_of_uri uri in
+          if !last_baseuri <> baseuri then
+           begin
+            MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
+            last_baseuri := baseuri
+           end;
+           let file = Http_getter.resolve' uri in
+           MatitaMisc.safe_remove file;
+           MatitaMisc.rmdir_descend (Filename.dirname file)
       with Http_getter_types.Key_not_found _ -> ());
       remove_coercion uri; 
       ignore (MatitaDb.remove_uri uri);