1 (* Copyright (C) 2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module GA = GrafiteAst
31 let obj_file_of_baseuri writable baseuri =
33 LibraryMisc.obj_file_of_baseuri
34 ~must_exist:true ~baseuri ~writable
36 | Http_getter_types.Unresolvable_URI _
37 | Http_getter_types.Key_not_found _ ->
38 LibraryMisc.obj_file_of_baseuri
39 ~must_exist:false ~baseuri ~writable:true
43 (* all are maps from "file" to "something" *)
44 let include_deps = Hashtbl.create (Array.length Sys.argv) in
45 let include_deps_dot = Hashtbl.create (Array.length Sys.argv) in
46 let baseuri_of = Hashtbl.create (Array.length Sys.argv) in
47 let baseuri_of_inv = Hashtbl.create (Array.length Sys.argv) in
48 let uri_deps = Hashtbl.create (Array.length Sys.argv) in
49 let buri alias = U.buri_of_uri (U.uri_of_string alias) in
50 let resolve alias current_buri =
51 let buri = buri alias in
52 if buri <> current_buri then Some buri else None in
53 let dot_file = ref "" in
54 MatitaInit.add_cmdline_spec
55 ["-dot", Arg.Set_string dot_file,
56 "<file> Save dependency graph in dot format to the given file"];
57 MatitaInit.parse_cmdline_and_configuration_file ();
59 Helm_registry.get_list Helm_registry.string "matita.includes" in
60 let args = Helm_registry.get_list Helm_registry.string "matita.args" in
63 prerr_endline "At least one .ma file must be specified";
66 let ma_files = args in
67 let bof = Hashtbl.create 10 in
68 let baseuri_of_script s =
69 try Hashtbl.find bof s
71 let b,_ = DependenciesParser.baseuri_of_script ~include_paths s in
72 Hashtbl.add bof s b; b
76 let ic = open_in ma_file in
77 let istream = Ulexing.from_utf8_channel ic in
78 let dependencies = DependenciesParser.parse_dependencies istream in
82 | DependenciesParser.UriDep uri ->
83 let uri = UriManager.string_of_uri uri in
84 if not (Http_getter_storage.is_legacy uri) then
85 Hashtbl.add uri_deps ma_file uri
86 | DependenciesParser.BaseuriDep uri ->
87 let uri = Http_getter_misc.strip_trailing_slash uri in
88 Hashtbl.add baseuri_of ma_file uri;
89 Hashtbl.add baseuri_of_inv uri ma_file
90 | DependenciesParser.IncludeDep path ->
92 let baseuri = baseuri_of_script path in
93 if not (Http_getter_storage.is_legacy baseuri) then
94 (let moo_file = obj_file_of_baseuri false baseuri in
95 Hashtbl.add include_deps ma_file moo_file;
96 Hashtbl.add include_deps_dot ma_file baseuri)
99 ("Unable to find " ^ path ^ " that is included in " ^ ma_file))
105 let dep = resolve alias (Hashtbl.find baseuri_of file) in
109 Hashtbl.add include_deps file (obj_file_of_baseuri false u)
111 prerr_endline ("File "^ file^" has no baseuri. Use set baseuri");
115 (* explode and implode from the OCaml Expert FAQ. *)
118 if i < 0 then l else exp (i - 1) (s.[i] :: l) in
119 exp (String.length s - 1) []
122 let res = String.create (List.length l) in
123 let rec imp i = function
125 | c :: l -> res.[i] <- c; imp (i + 1) l in
128 let rec aux = function
129 | x::tl1,y::tl2 when x = y -> x::(aux (tl1,tl2))
132 implode (aux (explode x,explode y))
134 let max_path = List.hd ma_files in
135 let max_path = List.fold_left gcp max_path ma_files in
136 let short x = Pcre.replace ~pat:("^"^max_path) x in
137 if !dot_file <> "" then (* generate dependency graph if required *)
139 let oc = open_out !dot_file in
140 let fmt = Format.formatter_of_out_channel oc in
141 GraphvizPp.Dot.header (* ~graph_attrs:["rankdir","LR"] *) fmt;
144 let deps = Hashtbl.find_all include_deps_dot ma_file in
148 try Some (Hashtbl.find baseuri_of_inv u)
149 with Not_found -> None)
152 let deps = List.fast_sort Pervasives.compare deps in
153 let deps = HExtlib.list_uniq deps in
154 GraphvizPp.Dot.node (short ma_file) fmt;
155 List.iter (fun dep -> GraphvizPp.Dot.edge (short ma_file) (short dep) fmt) deps)
157 GraphvizPp.Dot.trailer fmt;
160 List.iter (* (always) generate regular .depend output *)
163 let deps = Hashtbl.find_all include_deps ma_file in
164 let deps = List.fast_sort Pervasives.compare deps in
165 let deps = HExtlib.list_uniq deps in
166 let deps = ma_file :: deps in
167 let baseuri = Hashtbl.find baseuri_of ma_file in
168 let moo = obj_file_of_baseuri true baseuri in
169 Printf.printf "%s: %s\n%s: %s\n%s: %s\n%s: %s\n"
170 moo (String.concat " " deps)
171 (Filename.basename(Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file)) moo
172 (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo
173 (Pcre.replace ~pat:"ma$" ~templ:"mo" (short ma_file)) moo
175 prerr_endline ("File "^ma_file^" has no baseuri. Use set baseuri");