1 (* Copyright (C) 2006, 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/
30 module Pp = GraphvizPp.Dot
31 module UriSet = UriManager.UriSet
34 let prefix_len = String.length position_prefix in
35 String.sub s prefix_len (String.length s - prefix_len)
40 (match strip_prefix s with
41 | "MainConclusion" -> `MainConclusion (Some (Eq (int_of_string d)))
42 | "MainHypothesis" -> `MainHypothesis (Some (Eq (int_of_string d)))
44 prerr_endline ("Invalid main position: " ^ s);
47 (match strip_prefix s with
48 | "InConclusion" -> `InConclusion
49 | "InHypothesis" -> `InHypothesis
52 prerr_endline ("Invalid position: " ^ s);
56 let unbox_row = function `Obj (uri, pos) -> (uri, pos)
58 let direct_deps ~dbd uri =
59 let obj_metadata_of_row =
61 | [| Some _; Some occurrence; pos; depth |] ->
62 `Obj (UriManager.uri_of_string occurrence, parse_pos (pos, depth))
64 prerr_endline "invalid (direct) refObj metadata row";
68 let res = HSql.exec dbd (SqlStatements.direct_deps tbl uri) in
70 HSql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in
73 do_query (MetadataTypes.obj_tbl ())
74 @ do_query MetadataTypes.library_obj_tbl
76 let inverse_deps ~dbd uri =
77 let inv_obj_metadata_of_row =
79 | [| Some src; Some _; pos; depth |] ->
80 `Obj (UriManager.uri_of_string src, parse_pos (pos, depth))
82 prerr_endline "invalid (inverse) refObj metadata row";
86 let res = HSql.exec dbd (SqlStatements.inverse_deps tbl uri) in
88 HSql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in
91 do_query (MetadataTypes.obj_tbl ())
92 @ do_query MetadataTypes.library_obj_tbl
94 let topological_sort ~dbd uris =
95 let module OrderedUri =
97 type t = UriManager.uri
98 let compare = UriManager.compare
100 let module Topo = HTopoSort.Make(OrderedUri) in
101 Topo.topological_sort uris
102 (fun uri -> fst (List.split (direct_deps ~dbd uri)))
104 let sorted_uris_of_baseuri ~dbd baseuri =
106 Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" baseuri ^ "%"
110 ("SELECT source FROM %s WHERE source LIKE \"%s\" "
111 ^^ HSql.escape_string_for_like ^^ " UNION " ^^
112 "SELECT source FROM %s WHERE source LIKE \"%s\" "
113 ^^ HSql.escape_string_for_like)
114 (MetadataTypes.name_tbl ()) sql_pat
115 MetadataTypes.library_name_tbl sql_pat
117 let result = HSql.exec dbd query in
118 let map cols = match cols.(0) with
119 | Some s -> UriManager.uri_of_string s
122 let uris = HSql.map result map in
123 let sorted_uris = topological_sort ~dbd uris in
126 Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
127 (UriManager.string_of_uri uri)
129 try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None
130 with Not_found -> Some (UriManager.uri_of_string s)
132 HExtlib.filter_map filter_map sorted_uris
136 module UriTbl = UriManager.UriHashtbl
139 let fat_increment = fat_value
140 let incomplete_attrs = ["style", "dashed"]
141 let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"]
143 let label_of_uri uri = UriManager.name_of_uri uri
144 (*let label_of_uri uri = UriManager.string_of_uri uri*)
147 { adjacency: UriManager.uri list lazy_t; (* all outgoing edges *)
148 mutable shown: int (* amount of edges to show *)
151 (** <adjacency list of the dependency graph,
153 * generator function,
154 * invert edges on render?>
155 * All dependency graph have a single root, it is kept here to have a
156 * starting point for graph traversals *)
158 neighborhood UriTbl.t * UriManager.uri
159 * (UriManager.uri -> UriManager.uri list) * bool
162 UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
165 let render fmt (adjlist, root, _f, invert) =
166 let is_complete uri =
168 let neighbs = UriTbl.find adjlist uri in
169 Lazy.lazy_is_val neighbs.adjacency
170 && neighbs.shown >= List.length (Lazy.force neighbs.adjacency)
172 (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
175 Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
180 let suri = UriManager.string_of_uri uri in
182 ~attrs:([ "href", UriManager.string_of_uri uri;
183 "label", label_of_uri uri
184 ] @ (if is_complete uri then [] else incomplete_attrs))
186 let new_nodes = ref [] in
188 let neighbs = UriTbl.find adjlist uri in
189 if Lazy.lazy_is_val neighbs.adjacency then begin
191 HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
195 let uri1, uri2 = if invert then dest, uri else uri, dest in
196 Pp.edge (UriManager.string_of_uri uri1)
197 (UriManager.string_of_uri uri2) fmt)
199 new_nodes := adjacency
201 with Not_found -> ());
202 aux (!new_nodes @ tl)
207 let expand uri (adjlist, _root, f, _invert) =
208 (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*)
210 let neighbs = UriTbl.find adjlist uri in
211 if not (Lazy.lazy_is_val neighbs.adjacency) then
212 (* node has never been expanded *)
213 let adjacency = Lazy.force neighbs.adjacency in
214 let weight = min (List.length adjacency) fat_value in
217 (* perform look ahead of 1 edge to avoid making as expandable nodes
218 * which have no outgoing edges *)
219 let next_level = f dest in
221 if List.length next_level = 0 then begin
222 (* no further outgoing edges, "expand" the node right now *)
223 let lazy_val = lazy next_level in
224 ignore (Lazy.force lazy_val);
225 { adjacency = lazy_val; shown = 0 }
227 { adjacency = lazy next_level; shown = 0 }
229 (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*)
230 UriTbl.add adjlist dest neighborhood)
232 neighbs.shown <- weight;
233 fst (HExtlib.split_nth weight adjacency), weight
234 else begin (* nodes has been expanded at least once *)
235 let adjacency = Lazy.force neighbs.adjacency in
236 let total_nodes = List.length adjacency in
237 if neighbs.shown < total_nodes then begin
238 (* some more children to show ... *)
239 let shown_before = neighbs.shown in
240 neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
241 let new_shown = neighbs.shown - shown_before in
242 (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
244 [], 0 (* all children are already shown *)
247 (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*)
250 let collapse uri (adjlist, _root, f, _invert) =
252 let neighbs = UriTbl.find adjlist uri in
253 if Lazy.lazy_is_val neighbs.adjacency then
254 (* do not collapse already collapsed nodes *)
255 if Lazy.force neighbs.adjacency <> [] then
256 (* do not collapse nodes with no outgoing edges *)
257 UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 }
259 (* do not add a collapsed node if it was not part of the graph *)
262 let graph_of_fun ?(invert = false) f ~dbd uri =
264 (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*)
265 let uris = fst (List.split (f ~dbd uri)) in
266 let uriset = List.fold_right UriSet.add uris UriSet.empty in
267 let res = UriSet.elements uriset in
268 (*eprintf "returned uris: %s\n%!"*)
269 (*(String.concat " " (List.map UriManager.string_of_uri res));*)
272 let adjlist = UriTbl.create 17 in
273 let gen_f = f ~dbd in
274 UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 };
275 let dep_graph = adjlist, uri, gen_f, invert in
276 let rec rec_expand weight =
279 | uri :: tl when weight >= fat_value -> ()
281 let new_nodes, increase = expand uri dep_graph in
282 rec_expand (weight + increase) (new_nodes @ tl) in
286 let direct_deps = graph_of_fun direct_deps
287 let inverse_deps = graph_of_fun ~invert:true inverse_deps
289 let expand uri graph =
291 ignore (expand uri graph)