(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) let paths_to_search_in = ref [];; let add_l l = fun s -> l := s :: !l ;; let arg_spec = [ "-I", Arg.String (add_l paths_to_search_in), " Adds path to the list of searched paths for the include command"; ] let usage = Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:" BuildTimeConf.version module TA = GrafiteAst module U = UriManager let deps = Hashtbl.create (Array.length Sys.argv) let baseuri = ref [] let aliases = Hashtbl.create (Array.length Sys.argv) (* let uri_of_alias = function | Ident_alias (_, uri) | Symbol_alias (_, _, uri) | Number_alias (_, uri) -> uri *) let buri alias = U.buri_of_uri (U.uri_of_string alias) let resolve alias = try Some (snd(List.find (fun (u, f) -> u = (buri alias)) !baseuri)) with | Not_found -> None (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****) let find path = let rec aux = function | [] -> close_in (open_in path); path | p :: tl -> try close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path with Sys_error _ -> aux tl in let paths = !paths_to_search_in in try aux paths with Sys_error _ as exc -> MatitaLog.error ("Unable to read " ^ path); MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); raise exc ;; let main () = Helm_registry.load_from BuildTimeConf.matita_conf; CicNotation.load_notation BuildTimeConf.core_notation_script; let files = ref [] in Arg.parse arg_spec (add_l files) usage; List.iter (fun file -> let ic = open_in file in let istream = Stream.of_channel ic in (try while true do try match GrafiteParser.parse_statement istream with | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> let uri = MatitaMisc.strip_trailing_slash uri in baseuri := (uri, file) :: !baseuri | TA.Executable (_, TA.Command (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> Hashtbl.add aliases file uri | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> Hashtbl.add deps file (find path) | _ -> () with CicNotationParser.Parse_error _ as exn -> prerr_endline ("Unable to parse: " ^ file); prerr_endline (MatitaExcPp.to_string exn); () done with | End_of_file -> close_in ic); Hashtbl.iter (fun file alias -> let dep = resolve alias in match dep with | None -> () | Some d -> Hashtbl.add deps file d) aliases) !files; List.iter (fun file -> let deps = Hashtbl.find_all deps file in let deps = List.fast_sort Pervasives.compare deps in let deps = MatitaMisc.list_uniq deps in let deps = List.map (fun x -> Pcre.replace ~pat:"ma$" ~templ:"moo" x) deps in let deps = file :: deps in Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file) (String.concat " " deps)) !files ;; let _ = main ()