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\" ESCAPE \"\\\" UNION "
112 "SELECT source FROM %s WHERE source LIKE \"%s\" ESCAPE \"\\\"")
113 (MetadataTypes.name_tbl ()) sql_pat
114 MetadataTypes.library_name_tbl sql_pat
116 let result = HSql.exec dbd query in
117 let map cols = match cols.(0) with
118 | Some s -> UriManager.uri_of_string s
121 let uris = HSql.map result map in
122 let sorted_uris = topological_sort ~dbd uris in
125 Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
126 (UriManager.string_of_uri uri)
128 try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None
129 with Not_found -> Some (UriManager.uri_of_string s)
131 HExtlib.filter_map filter_map sorted_uris
135 module UriTbl = UriManager.UriHashtbl
138 let fat_increment = fat_value
139 let incomplete_attrs = ["style", "dashed"]
140 let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"]
142 let label_of_uri uri = UriManager.name_of_uri uri
143 (*let label_of_uri uri = UriManager.string_of_uri uri*)
146 { adjacency: UriManager.uri list lazy_t; (* all outgoing edges *)
147 mutable shown: int (* amount of edges to show *)
150 (** <adjacency list of the dependency graph,
152 * generator function,
153 * invert edges on render?>
154 * All dependency graph have a single root, it is kept here to have a
155 * starting point for graph traversals *)
157 neighborhood UriTbl.t * UriManager.uri
158 * (UriManager.uri -> UriManager.uri list) * bool
161 UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
164 let render fmt (adjlist, root, _f, invert) =
165 let is_complete uri =
167 let neighbs = UriTbl.find adjlist uri in
168 Lazy.lazy_is_val neighbs.adjacency
169 && neighbs.shown >= List.length (Lazy.force neighbs.adjacency)
171 (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
174 Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
179 let suri = UriManager.string_of_uri uri in
181 ~attrs:([ "href", UriManager.string_of_uri uri;
182 "label", label_of_uri uri
183 ] @ (if is_complete uri then [] else incomplete_attrs))
185 let new_nodes = ref [] in
187 let neighbs = UriTbl.find adjlist uri in
188 if Lazy.lazy_is_val neighbs.adjacency then begin
190 HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
194 let uri1, uri2 = if invert then dest, uri else uri, dest in
195 Pp.edge (UriManager.string_of_uri uri1)
196 (UriManager.string_of_uri uri2) fmt)
198 new_nodes := adjacency
200 with Not_found -> ());
201 aux (!new_nodes @ tl)
206 let expand uri (adjlist, _root, f, _invert) =
207 (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*)
209 let neighbs = UriTbl.find adjlist uri in
210 if not (Lazy.lazy_is_val neighbs.adjacency) then
211 (* node has never been expanded *)
212 let adjacency = Lazy.force neighbs.adjacency in
213 let weight = min (List.length adjacency) fat_value in
216 (* perform look ahead of 1 edge to avoid making as expandable nodes
217 * which have no outgoing edges *)
218 let next_level = f dest in
220 if List.length next_level = 0 then begin
221 (* no further outgoing edges, "expand" the node right now *)
222 let lazy_val = lazy next_level in
223 ignore (Lazy.force lazy_val);
224 { adjacency = lazy_val; shown = 0 }
226 { adjacency = lazy next_level; shown = 0 }
228 (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*)
229 UriTbl.add adjlist dest neighborhood)
231 neighbs.shown <- weight;
232 fst (HExtlib.split_nth weight adjacency), weight
233 else begin (* nodes has been expanded at least once *)
234 let adjacency = Lazy.force neighbs.adjacency in
235 let total_nodes = List.length adjacency in
236 if neighbs.shown < total_nodes then begin
237 (* some more children to show ... *)
238 let shown_before = neighbs.shown in
239 neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
240 let new_shown = neighbs.shown - shown_before in
241 (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
243 [], 0 (* all children are already shown *)
246 (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*)
249 let collapse uri (adjlist, _root, f, _invert) =
251 let neighbs = UriTbl.find adjlist uri in
252 if Lazy.lazy_is_val neighbs.adjacency then
253 (* do not collapse already collapsed nodes *)
254 if Lazy.force neighbs.adjacency <> [] then
255 (* do not collapse nodes with no outgoing edges *)
256 UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 }
258 (* do not add a collapsed node if it was not part of the graph *)
261 let graph_of_fun ?(invert = false) f ~dbd uri =
263 (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*)
264 let uris = fst (List.split (f ~dbd uri)) in
265 let uriset = List.fold_right UriSet.add uris UriSet.empty in
266 let res = UriSet.elements uriset in
267 (*eprintf "returned uris: %s\n%!"*)
268 (*(String.concat " " (List.map UriManager.string_of_uri res));*)
271 let adjlist = UriTbl.create 17 in
272 let gen_f = f ~dbd in
273 UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 };
274 let dep_graph = adjlist, uri, gen_f, invert in
275 let rec rec_expand weight =
278 | uri :: tl when weight >= fat_value -> ()
280 let new_nodes, increase = expand uri dep_graph in
281 rec_expand (weight + increase) (new_nodes @ tl) in
285 let direct_deps = graph_of_fun direct_deps
286 let inverse_deps = graph_of_fun ~invert:true inverse_deps
288 let expand uri graph =
290 ignore (expand uri graph)