helm/matita/matitacleanLib.ml

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