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 = HMysql.exec dbd (SqlStatements.direct_deps tbl uri) in
70 HMysql.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 = HMysql.exec dbd (SqlStatements.inverse_deps tbl uri) in
88 HMysql.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
96 module UriTbl = UriManager.UriHashtbl
99 let fat_increment = fat_value
100 let incomplete_attrs = ["style", "dashed"]
101 let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"]
103 let label_of_uri uri = UriManager.name_of_uri uri
104 (*let label_of_uri uri = UriManager.string_of_uri uri*)
107 { adjacency: UriManager.uri list lazy_t; (* all outgoing edges *)
108 mutable shown: int (* amount of edges to show *)
111 (** <adjacency list of the dependency graph,
113 * generator function,
114 * invert edges on render?>
115 * All dependency graph have a single root, it is kept here to have a
116 * starting point for graph traversals *)
118 neighborhood UriTbl.t * UriManager.uri
119 * (UriManager.uri -> UriManager.uri list) * bool
122 UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
125 let render fmt (adjlist, root, _f, invert) =
126 let is_complete uri =
128 let neighbs = UriTbl.find adjlist uri in
129 Lazy.lazy_is_val neighbs.adjacency
130 && neighbs.shown >= List.length (Lazy.force neighbs.adjacency)
132 (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
135 Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
140 let suri = UriManager.string_of_uri uri in
142 ~attrs:([ "href", UriManager.string_of_uri uri;
143 "label", label_of_uri uri
144 ] @ (if is_complete uri then [] else incomplete_attrs))
146 let new_nodes = ref [] in
148 let neighbs = UriTbl.find adjlist uri in
149 if Lazy.lazy_is_val neighbs.adjacency then begin
151 HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
155 let uri1, uri2 = if invert then dest, uri else uri, dest in
156 Pp.edge (UriManager.string_of_uri uri1)
157 (UriManager.string_of_uri uri2) fmt)
159 new_nodes := adjacency
161 with Not_found -> ());
162 aux (!new_nodes @ tl)
167 let expand uri (adjlist, _root, f, _invert) =
168 (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*)
170 let neighbs = UriTbl.find adjlist uri in
171 if not (Lazy.lazy_is_val neighbs.adjacency) then
172 (* node has never been expanded *)
173 let adjacency = Lazy.force neighbs.adjacency in
174 let weight = min (List.length adjacency) fat_value in
177 (* perform look ahead of 1 edge to avoid making as expandable nodes
178 * which have no outgoing edges *)
179 let next_level = f dest in
181 if List.length next_level = 0 then begin
182 (* no further outgoing edges, "expand" the node right now *)
183 let lazy_val = lazy next_level in
184 ignore (Lazy.force lazy_val);
185 { adjacency = lazy_val; shown = 0 }
187 { adjacency = lazy next_level; shown = 0 }
189 (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*)
190 UriTbl.add adjlist dest neighborhood)
192 neighbs.shown <- weight;
193 fst (HExtlib.split_nth weight adjacency), weight
194 else begin (* nodes has been expanded at least once *)
195 let adjacency = Lazy.force neighbs.adjacency in
196 let total_nodes = List.length adjacency in
197 if neighbs.shown < total_nodes then begin
198 (* some more children to show ... *)
199 let shown_before = neighbs.shown in
200 neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
201 let new_shown = neighbs.shown - shown_before in
202 (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
204 [], 0 (* all children are already shown *)
207 (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*)
210 let collapse uri (adjlist, _root, f, _invert) =
212 let neighbs = UriTbl.find adjlist uri in
213 if Lazy.lazy_is_val neighbs.adjacency then
214 (* do not collapse already collapsed nodes *)
215 if Lazy.force neighbs.adjacency <> [] then
216 (* do not collapse nodes with no outgoing edges *)
217 UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 }
219 (* do not add a collapsed node if it was not part of the graph *)
222 let graph_of_fun ?(invert = false) f ~dbd uri =
224 (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*)
225 let uris = fst (List.split (f ~dbd uri)) in
226 let uriset = List.fold_right UriSet.add uris UriSet.empty in
227 let res = UriSet.elements uriset in
228 (*eprintf "returned uris: %s\n%!"*)
229 (*(String.concat " " (List.map UriManager.string_of_uri res));*)
232 let adjlist = UriTbl.create 17 in
233 let gen_f = f ~dbd in
234 UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 };
235 let dep_graph = adjlist, uri, gen_f, invert in
236 let rec rec_expand weight =
239 | uri :: tl when weight >= fat_value -> ()
241 let new_nodes, increase = expand uri dep_graph in
242 rec_expand (weight + increase) (new_nodes @ tl) in
246 let direct_deps = graph_of_fun direct_deps
247 let inverse_deps = graph_of_fun ~invert:true inverse_deps
249 let expand uri graph =
251 ignore (expand uri graph)