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 = GrafiteAst;;
  34
  35 let baseuri_of_baseuri_decl st =
  36   match st with
  37   | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
  38       Some buri
  39   | _ -> None
  40
  41 let cache_of_processed_baseuri = Hashtbl.create 1024
  42
  43 let one_step_depend suri =
  44   let buri =
  45     try
  46       UM.buri_of_uri (UM.uri_of_string suri)
  47     with UM.IllFormedUri _ -> suri
  48   in
  49   if Hashtbl.mem cache_of_processed_baseuri buri then
  50     []
  51   else
  52     begin
  53       Hashtbl.add cache_of_processed_baseuri buri true;
  54       let query =
  55         let buri = buri ^ "/" in
  56         let buri = Mysql.escape buri in
  57         let obj_tbl = MetadataTypes.obj_tbl () in
  58         Printf.sprintf
  59           "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
  60       in
  61       try
  62         let rc = Mysql.exec (MatitaDb.instance ()) query in
  63         let l = ref [] in
  64         Mysql.iter rc (
  65           fun row ->
  66             match row.(0), row.(1) with
  67             | Some uri, Some occ when Filename.dirname occ = buri ->
  68                 l := uri :: !l
  69             | _ -> ());
  70         let l = List.sort Pervasives.compare !l in
  71         MatitaMisc.list_uniq l
  72       with
  73         exn -> raise exn (* no errors should be accepted *)
  74     end
  75
  76
  77 let safe_buri_of_suri suri =
  78   try
  79     UM.buri_of_uri (UM.uri_of_string suri)
  80   with
  81     UM.IllFormedUri _ -> suri
  82
  83 let close_uri_list uri_to_remove =
  84   (* to remove an uri you have to remove the whole script *)
  85   let buri_to_remove =
  86     MatitaMisc.list_uniq
  87       (List.fast_sort Pervasives.compare
  88         (List.map safe_buri_of_suri uri_to_remove))
  89   in
  90   (* cleand the already visided baseuris *)
  91   let buri_to_remove =
  92     List.filter
  93       (fun buri ->
  94         if Hashtbl.mem cache_of_processed_baseuri buri then false
  95         else true)
  96       buri_to_remove
  97   in
  98   (* now calculate the list of objects that belong to these baseuris *)
  99   let uri_to_remove =
 100     try
 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     with HGT.Invalid_URI u ->
 117       MatitaLog.error ("We were listing an invalid buri: " ^ u);
 118       exit 1
 119   in
 120   (* now we want the list of all uri that depend on them *)
 121   let depend =
 122     List.fold_left
 123     (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
 124   in
 125   let depend =
 126     MatitaMisc.list_uniq
 127       (List.fast_sort Pervasives.compare depend)
 128   in
 129   uri_to_remove, depend
 130
 131 let baseuri_of_file file =
 132   let uri = ref None in
 133   let ic = open_in file in
 134   let istream = Stream.of_channel ic in
 135   (try
 136     while true do
 137       try
 138         let stm = GrafiteParser.parse_statement istream in
 139         match baseuri_of_baseuri_decl stm with
 140         | Some buri ->
 141             let u = MatitaMisc.strip_trailing_slash buri in
 142             if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
 143               MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
 144             (try
 145               ignore(HG.resolve u)
 146             with
 147             | HGT.Unresolvable_URI _ ->
 148                 MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
 149             | HGT.Key_not_found _ -> ());
 150             uri := Some u;
 151             raise End_of_file
 152         | None -> ()
 153       with
 154         CicNotationParser.Parse_error _ as exn ->
 155           prerr_endline ("Unable to parse: " ^ file);
 156           prerr_endline (MatitaExcPp.to_string exn);
 157           ()
 158     done
 159   with End_of_file -> close_in ic);
 160   match !uri with
 161   | Some uri -> uri
 162   | None -> failwith ("No baseuri defined in " ^ file)
 163
 164 let rec fix uris next =
 165   match next with
 166   | [] -> uris
 167   | l -> let uris, next = close_uri_list l in fix uris next @ uris
 168
 169 let cleaned_no = ref 0;;
 170
 171 let clean_baseuris ?(verbose=true) buris =
 172   Hashtbl.clear cache_of_processed_baseuri;
 173   let buris = List.map HGM.strip_trailing_slash buris in
 174   debug_prerr "clean_baseuris called on:";
 175   if debug then
 176     List.iter debug_prerr buris;
 177   let l = fix [] buris in
 178   let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
 179   let l = List.map UriManager.uri_of_string l in
 180   debug_prerr "clean_baseuri will remove:";
 181   if debug then
 182     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
 183   List.iter (MatitaSync.remove ~verbose) l;
 184   cleaned_no := !cleaned_no + List.length l;
 185   if !cleaned_no > 30 then
 186    List.iter
 187     (function table ->
 188       ignore (Mysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
 189     [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
 190      MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
 191      MetadataTypes.count_tbl()]
 192
 193 let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
 194