first snapshot of separate compilation

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

diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml
index 60292515ae11b598856128822507ece6f925c946..eb0c5787d3e0fbaac1d4a01907013385bb12e6b1 100644 (file)
--- a/helm/matita/matitaclean.ml
+++ b/helm/matita/matitaclean.ml
@@ -1,6 +1,7 @@
 module HGT = Http_getter_types;;
 module HG = Http_getter;;
 module UM = UriManager;;
+module TA = TacticAst;;
 
 let _ =
   Helm_registry.load_from "matita.conf.xml";
@@ -13,34 +14,49 @@ let clean_all () =
   exit 0
   
 let dbd = MatitaDb.instance ()
+let cache_of_processed_baseuri = Hashtbl.create 1024
 
 let one_step_depend suri =
-  let dbg_q = 
-    let suri = Mysql.escape suri in
-    (**** FIX FIX FIX ***)
-    (****** let obj_tbl = MetadataTypes.obj_tbl () in  ******)
-    let obj_tbl = MetadataTypes.library_obj_tbl in 
-    (**** FIX FIX FIX ***)
-    Printf.sprintf 
-      "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
+  let buri =
+    try
+      UM.buri_of_uri (UM.uri_of_string suri)
+    with UM.IllFormedUri _ -> suri
   in
-  try 
-    let rc = Mysql.exec dbd dbg_q in
-    let l = ref [] in
-    Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
-    let l = List.sort Pervasives.compare !l in
-    MatitaMisc.list_uniq l
-  with
-    exn -> raise exn (* no errors should be accepted *)
+  if Hashtbl.mem cache_of_processed_baseuri buri then 
+    []
+  else
+    begin
+      Hashtbl.add cache_of_processed_baseuri buri true;
+      let query = 
+        let buri = buri ^ "/" in 
+        let buri = Mysql.escape buri in
+        let obj_tbl = MetadataTypes.obj_tbl () in
+        Printf.sprintf 
+          "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+      in
+      try 
+        let rc = Mysql.exec dbd query in
+        let l = ref [] in
+        Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l);
+        let l = List.sort Pervasives.compare !l in
+        MatitaMisc.list_uniq l
+      with
+        exn -> raise exn (* no errors should be accepted *)
+    end
 
-let cache_of_processed_baseuri = Hashtbl.create 1024
     
+let safe_buri_of_suri suri =
+  try
+    UM.buri_of_uri (UM.uri_of_string suri)
+  with
+    UM.IllFormedUri _ -> 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 
       (List.fast_sort Pervasives.compare 
-        (List.map UM.buri_of_uri uri_to_remove))
+        (List.map safe_buri_of_suri uri_to_remove))
   in
   (* cleand the already visided baseuris *)
   let buri_to_remove = 
@@ -50,9 +66,6 @@ let close_uri_list uri_to_remove =
         else true)
       buri_to_remove
   in
-  List.iter 
-    (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true)
-    buri_to_remove;
   (* now calculate the list of objects that belong to these baseuris *)
   let uri_to_remove = 
     List.fold_left 
@@ -64,7 +77,7 @@ let close_uri_list uri_to_remove =
         in
         let inhabitants = List.map 
             (function 
-             | HGT.Ls_object e -> UM.uri_of_string (buri ^ "/" ^ e.HGT.uri) 
+             | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri 
              | _ -> assert false)
           inhabitants
         in
@@ -74,15 +87,27 @@ let close_uri_list uri_to_remove =
   (* now we want the list of all uri that depend on them *) 
   let depend = 
     List.fold_left
-    (fun acc u -> one_step_depend (UM.string_of_uri u) @ acc) [] 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) 
   in
-  let depend = List.map UM.uri_of_string depend in
   uri_to_remove, depend
 
+let buri_of_file file = 
+  let ic = open_in file in
+  let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
+  close_in ic;
+  let uri = ref "" in
+  List.iter 
+    (function
+    | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
+        uri := MatitaMisc.strip_trailing_slash buri
+    | _ -> ()) 
+    stms;
+  !uri
+
 let main uri_to_remove =
   let rec fix uris next =
     match next with
@@ -96,8 +121,8 @@ let usage () =
   prerr_endline "";
   prerr_endline "usage:";
   prerr_endline "\tmatitaclean all";
-  prerr_endline "\tmatitaclean dry uris...";
-  prerr_endline "\tmatitaclean uris...";
+  prerr_endline "\tmatitaclean dry (uri|file)+";
+  prerr_endline "\tmatitaclean (uri|file)+";
   prerr_endline "";
   exit 1
     
@@ -113,24 +138,31 @@ let _ =
     if Sys.argv.(1) = "dry" then 2, true else 1, false
   in
   let uri_to_remove =ref [] in
-  try 
+  (try 
     for i = start to Array.length Sys.argv - 1 do
       let suri = Sys.argv.(i) in
-      let uri = UM.uri_of_string suri in
+      let uri = 
+        try
+          UM.buri_of_uri (UM.uri_of_string suri)
+        with
+          UM.IllFormedUri _ -> buri_of_file suri
+      in
       uri_to_remove := uri :: !uri_to_remove
     done
   with
-    Invalid_argument _ -> usage ();
+    Invalid_argument _ -> usage ());
   let l = main !uri_to_remove in
   if dry then
     begin
-      List.iter (fun x -> let u = UM.string_of_uri x in prerr_endline u) l;
+      List.iter prerr_endline l;
       exit 0
     end
   else
     List.iter 
       (fun u ->
-        prerr_endline ("Removing " ^ UM.string_of_uri u);
-        MatitaSync.remove u)
+        prerr_endline ("Removing " ^ u);
+        try
+          MatitaSync.remove (UM.uri_of_string u)
+        with Sys_error _ -> ())
     l