dump_moo added

[helm.git] / helm / matita / matitacleanLib.ml

diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index 51268acef0c8084216a7107346308b23813f3416..e8a1fd29a301bf1141f4ae2739929664aa2f9426 100644 (file)
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 let debug = false
 let debug_prerr = if debug then prerr_endline else ignore
 
@@ -49,8 +51,10 @@ let one_step_depend suri =
         let buri = buri ^ "/" in 
         let buri = HMysql.escape buri in
         let obj_tbl = MetadataTypes.obj_tbl () in
-        Printf.sprintf 
-          "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+        sprintf 
+        ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
+         "h_occurrence REGEXP '^%s[^/]*$'")
+            obj_tbl buri
       in
       try 
         let rc = HMysql.exec (MatitaDb.instance ()) query in
@@ -62,11 +66,10 @@ let one_step_depend suri =
                 l := uri :: !l
             | _ -> ());
         let l = List.sort Pervasives.compare !l in
-        MatitaMisc.list_uniq l
+        HExtlib.list_uniq l
       with
         exn -> raise exn (* no errors should be accepted *)
     end
-
     
 let safe_buri_of_suri suri =
   try
@@ -77,7 +80,7 @@ let safe_buri_of_suri suri =
 let close_uri_list uri_to_remove =
   (* to remove an uri you have to remove the whole script *)
   let buri_to_remove = 
-    MatitaMisc.list_uniq 
+    HExtlib.list_uniq 
       (List.fast_sort Pervasives.compare 
         (List.map safe_buri_of_suri uri_to_remove))
   in
@@ -117,34 +120,100 @@ let close_uri_list uri_to_remove =
     (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
   in
   let depend = 
-    MatitaMisc.list_uniq 
-      (List.fast_sort Pervasives.compare depend) 
+    HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) 
   in
   uri_to_remove, depend
 
-let rec close uris next =
+let rec close_using_db uris next =
   match next with
   | [] -> uris
-  | l -> let uris, next = close_uri_list l in close uris next @ uris
+  | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
   
 let cleaned_no = ref 0;;
 
+  (** TODO repellent code ... *)
+let moo_root_dir = lazy (
+  let url =
+    List.assoc "cic:/matita/"
+      (List.map
+        (fun pair ->
+          match
+            Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
+          with
+          | [a;b] -> a, b
+          | _ -> assert false)
+        (Helm_registry.get_list Helm_registry.string "getter.prefix"))
+  in
+  String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
+)
+
+let close_using_moos buris =
+  let rev_deps = Hashtbl.create 97 in
+  let all_moos =
+    HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
+      (Lazy.force moo_root_dir)
+  in
+  List.iter
+    (fun path -> 
+      let _, metadata = MatitaMoo.load_moo ~fname:path in
+      let baseuri_of_current_moo = 
+        let rec aux = function 
+          | [] -> assert false
+          | GrafiteAst.Baseuri buri::_ -> buri
+          | _ :: tl -> aux tl
+        in
+        aux metadata
+      in
+      let deps = 
+        HExtlib.filter_map 
+          (function 
+          | GrafiteAst.Dependency buri -> Some buri
+          | _ -> None ) 
+        metadata
+      in
+      List.iter 
+        (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
+  all_moos;
+  let buris_to_remove = 
+    HExtlib.list_uniq  
+      (List.fast_sort Pervasives.compare 
+        (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
+  in
+  let objects_to_remove = 
+    let objs_of_buri buri =
+      HExtlib.filter_map 
+        (function 
+        | Http_getter_types.Ls_object o ->
+            Some (buri ^ "/" ^ o.Http_getter_types.uri)
+        | _ -> None) 
+      (Http_getter.ls buri)
+    in
+    List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
+  in
+  objects_to_remove
+
 let clean_baseuris ?(verbose=true) buris =
   Hashtbl.clear cache_of_processed_baseuri;
   let buris = List.map HGM.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
   if debug then
     List.iter debug_prerr buris; 
-  let l = close [] buris in
-  let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
+  let l = 
+    if Helm_registry.get_bool "db.nodb" then
+      close_using_moos buris
+    else
+      close_using_db [] buris 
+  in
+  let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
   debug_prerr "clean_baseuri will remove:";
   if debug then
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
-  Hashtbl.iter
-   (fun buri _ ->
+  List.iter
+   (fun buri ->
      MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) 
-   cache_of_processed_baseuri;
+   (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+     (List.map (UriManager.buri_of_uri) l)));
   List.iter (MatitaSync.remove ~verbose) l;
   cleaned_no := !cleaned_no + List.length l;
   if !cleaned_no > 30 then
@@ -157,3 +226,4 @@ let clean_baseuris ?(verbose=true) buris =
       MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
       MetadataTypes.count_tbl()]
    end
+