module HGT = Http_getter_types;; module HG = Http_getter;; module UM = UriManager;; module TA = TacticAst;; let cache_of_processed_baseuri = Hashtbl.create 1024 let one_step_depend suri = let buri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> suri in 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 (MatitaDb.instance ()) 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 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 safe_buri_of_suri uri_to_remove)) in (* cleand the already visided baseuris *) let buri_to_remove = List.filter (fun buri -> if Hashtbl.mem cache_of_processed_baseuri buri then false else true) buri_to_remove in (* now calculate the list of objects that belong to these baseuris *) let uri_to_remove = List.fold_left (fun acc buri -> let inhabitants = HG.ls (buri ^ "/") in let inhabitants = List.filter (function HGT.Ls_object _ -> true | _ -> false) inhabitants in let inhabitants = List.map (function | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri | _ -> assert false) inhabitants in inhabitants @ acc) [] buri_to_remove in (* now we want the list of all uri that depend on them *) let depend = List.fold_left (fun acc u -> one_step_depend u @ acc) [] uri_to_remove in let depend = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend let baseuri_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 rec fix uris next = match next with | [] -> uris | l -> let uris, next = close_uri_list l in fix uris next @ uris let clean_baseuris buris = let l = fix [] buris in let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in let l = List.map UriManager.uri_of_string l in List.iter MatitaSync.remove l