helm/matita/matitacleanLib.ml

   1 module HGT = Http_getter_types;;
   2 module HG = Http_getter;;
   3 module HGM = Http_getter_misc;;
   4 module UM = UriManager;;
   5 module TA = TacticAst;;
   6
   7 let baseuri_of_baseuri_decl st =
   8   let module TA = TacticAst in
   9   match st with
  10   | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
  11       Some buri
  12   | _ -> None
  13
  14 let cache_of_processed_baseuri = Hashtbl.create 1024
  15
  16 let one_step_depend suri =
  17   let buri =
  18     try
  19       UM.buri_of_uri (UM.uri_of_string suri)
  20     with UM.IllFormedUri _ -> suri
  21   in
  22   if Hashtbl.mem cache_of_processed_baseuri buri then
  23     []
  24   else
  25     begin
  26       Hashtbl.add cache_of_processed_baseuri buri true;
  27       let query =
  28         let buri = buri ^ "/" in
  29         let buri = Mysql.escape buri in
  30         let obj_tbl = MetadataTypes.obj_tbl () in
  31         Printf.sprintf
  32           "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
  33       in
  34       try
  35         let rc = Mysql.exec (MatitaDb.instance ()) query in
  36         let l = ref [] in
  37         Mysql.iter rc (
  38           fun row ->
  39             match row.(0), row.(1) with
  40             | Some uri, Some occ when Filename.dirname occ = buri ->
  41                 l := uri :: !l
  42             | _ -> ());
  43         let l = List.sort Pervasives.compare !l in
  44         MatitaMisc.list_uniq l
  45       with
  46         exn -> raise exn (* no errors should be accepted *)
  47     end
  48
  49
  50 let safe_buri_of_suri suri =
  51   try
  52     UM.buri_of_uri (UM.uri_of_string suri)
  53   with
  54     UM.IllFormedUri _ -> suri
  55
  56 let close_uri_list uri_to_remove =
  57   (* to remove an uri you have to remove the whole script *)
  58   let buri_to_remove =
  59     MatitaMisc.list_uniq
  60       (List.fast_sort Pervasives.compare
  61         (List.map safe_buri_of_suri uri_to_remove))
  62   in
  63   (* cleand the already visided baseuris *)
  64   let buri_to_remove =
  65     List.filter
  66       (fun buri ->
  67         if Hashtbl.mem cache_of_processed_baseuri buri then false
  68         else true)
  69       buri_to_remove
  70   in
  71   (* now calculate the list of objects that belong to these baseuris *)
  72   let uri_to_remove =
  73     List.fold_left
  74       (fun acc buri ->
  75         let inhabitants = HG.ls (buri ^ "/") in
  76         let inhabitants = List.filter
  77             (function HGT.Ls_object _ -> true | _ -> false)
  78           inhabitants
  79         in
  80         let inhabitants = List.map
  81             (function
  82              | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
  83              | _ -> assert false)
  84           inhabitants
  85         in
  86         inhabitants @ acc)
  87     [] buri_to_remove
  88   in
  89   (* now we want the list of all uri that depend on them *)
  90   let depend =
  91     List.fold_left
  92     (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
  93   in
  94   let depend =
  95     MatitaMisc.list_uniq
  96       (List.fast_sort Pervasives.compare depend)
  97   in
  98   uri_to_remove, depend
  99
 100 let baseuri_of_file file =
 101   let ic = open_in file in
 102   let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
 103   close_in ic;
 104   let uri = ref "" in
 105   List.iter
 106     (fun stm ->
 107       match baseuri_of_baseuri_decl stm with
 108       | Some buri -> uri := MatitaMisc.strip_trailing_slash buri
 109       | None -> ())
 110     stms;
 111   !uri
 112
 113 let rec fix uris next =
 114   match next with
 115   | [] -> uris
 116   | l -> let uris, next = close_uri_list l in fix uris next @ uris
 117
 118 let clean_baseuris ?(verbose=true) buris =
 119   let buris = List.map HGM.strip_trailing_slash buris in
 120   (* List.iter prerr_endline buris; *)
 121   let l = fix [] buris in
 122   let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
 123   let l = List.map UriManager.uri_of_string l in
 124   (* List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) l; *)
 125   List.iter (MatitaSync.remove ~verbose) l
 126
 127 let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
 128