module HGT = Http_getter_types;; module HG = Http_getter;; module HGM = Http_getter_misc;; module UM = UriManager;; module TA = TacticAst;; let baseuri_of_baseuri_decl st = let module TA = TacticAst in match st with | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> Some buri | _ -> None 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, h_occurrence 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 row -> match row.(0), row.(1) with | Some uri, Some occ when Filename.dirname occ = buri -> l := uri :: !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 (fun stm -> match baseuri_of_baseuri_decl stm with | Some buri -> uri := MatitaMisc.strip_trailing_slash buri | None -> ()) 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 ?(verbose=true) buris = let buris = List.map HGM.strip_trailing_slash buris in (* List.iter prerr_endline 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 (fun u -> prerr_endline (UriManager.string_of_uri u)) l; *) List.iter (MatitaSync.remove ~verbose) l let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []