helm/matita/matitacleanLib.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 let debug = false
  27 let debug_prerr = if debug then prerr_endline else ignore
  28
  29 module HGT = Http_getter_types;;
  30 module HG = Http_getter;;
  31 module HGM = Http_getter_misc;;
  32 module UM = UriManager;;
  33 module TA = TacticAst;;
  34
  35 let baseuri_of_baseuri_decl st =
  36   let module TA = TacticAst in
  37   match st with
  38   | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
  39       Some buri
  40   | _ -> None
  41
  42 let cache_of_processed_baseuri = Hashtbl.create 1024
  43
  44 let one_step_depend suri =
  45   let buri =
  46     try
  47       UM.buri_of_uri (UM.uri_of_string suri)
  48     with UM.IllFormedUri _ -> suri
  49   in
  50   if Hashtbl.mem cache_of_processed_baseuri buri then
  51     []
  52   else
  53     begin
  54       Hashtbl.add cache_of_processed_baseuri buri true;
  55       let query =
  56         let buri = buri ^ "/" in
  57         let buri = Mysql.escape buri in
  58         let obj_tbl = MetadataTypes.obj_tbl () in
  59         Printf.sprintf
  60           "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
  61       in
  62       try
  63         let rc = Mysql.exec (MatitaDb.instance ()) query in
  64         let l = ref [] in
  65         Mysql.iter rc (
  66           fun row ->
  67             match row.(0), row.(1) with
  68             | Some uri, Some occ when Filename.dirname occ = buri ->
  69                 l := uri :: !l
  70             | _ -> ());
  71         let l = List.sort Pervasives.compare !l in
  72         MatitaMisc.list_uniq l
  73       with
  74         exn -> raise exn (* no errors should be accepted *)
  75     end
  76
  77
  78 let safe_buri_of_suri suri =
  79   try
  80     UM.buri_of_uri (UM.uri_of_string suri)
  81   with
  82     UM.IllFormedUri _ -> suri
  83
  84 let close_uri_list uri_to_remove =
  85   (* to remove an uri you have to remove the whole script *)
  86   let buri_to_remove =
  87     MatitaMisc.list_uniq
  88       (List.fast_sort Pervasives.compare
  89         (List.map safe_buri_of_suri uri_to_remove))
  90   in
  91   (* cleand the already visided baseuris *)
  92   let buri_to_remove =
  93     List.filter
  94       (fun buri ->
  95         if Hashtbl.mem cache_of_processed_baseuri buri then false
  96         else true)
  97       buri_to_remove
  98   in
  99   (* now calculate the list of objects that belong to these baseuris *)
 100   let uri_to_remove =
 101     List.fold_left
 102       (fun acc buri ->
 103         let inhabitants = HG.ls (buri ^ "/") in
 104         let inhabitants = List.filter
 105             (function HGT.Ls_object _ -> true | _ -> false)
 106           inhabitants
 107         in
 108         let inhabitants = List.map
 109             (function
 110              | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
 111              | _ -> assert false)
 112           inhabitants
 113         in
 114         inhabitants @ acc)
 115     [] buri_to_remove
 116   in
 117   (* now we want the list of all uri that depend on them *)
 118   let depend =
 119     List.fold_left
 120     (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
 121   in
 122   let depend =
 123     MatitaMisc.list_uniq
 124       (List.fast_sort Pervasives.compare depend)
 125   in
 126   uri_to_remove, depend
 127
 128 let baseuri_of_file file =
 129   let ic = open_in file in
 130   let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
 131   close_in ic;
 132   let uri = ref "" in
 133   List.iter
 134     (fun stm ->
 135       match baseuri_of_baseuri_decl stm with
 136       | Some buri -> uri := MatitaMisc.strip_trailing_slash buri
 137       | None -> ())
 138     stms;
 139   !uri
 140
 141 let rec fix uris next =
 142   match next with
 143   | [] -> uris
 144   | l -> let uris, next = close_uri_list l in fix uris next @ uris
 145
 146 let clean_baseuris ?(verbose=true) buris =
 147   Hashtbl.clear cache_of_processed_baseuri;
 148   let buris = List.map HGM.strip_trailing_slash buris in
 149   debug_prerr "clean_baseuris called on:";
 150   if debug then
 151     List.iter debug_prerr buris;
 152   let l = fix [] buris in
 153   let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
 154   let l = List.map UriManager.uri_of_string l in
 155   debug_prerr "clean_baseuri will remove:";
 156   if debug then
 157     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
 158   List.iter (MatitaSync.remove ~verbose) l
 159
 160 let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
 161