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", "9"; "width", ".4"; "height", ".4"]
104 { adjacency: UriManager.uri list lazy_t; (* all outgoing edges *)
105 mutable shown: int (* amount of edges to show *)
108 (** <adjacency list of the dependency graph,
110 * generator function,
111 * invert edges on render?>
112 * All dependency graph have a single root, it is kept here to have a
113 * starting point for graph traversals *)
115 neighborhood UriTbl.t * UriManager.uri
116 * (UriManager.uri -> UriManager.uri list) * bool
119 UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
122 let render fmt (adjlist, root, _f, invert) =
123 let is_complete uri =
125 let neighbs = UriTbl.find adjlist uri in
126 Lazy.lazy_is_val neighbs.adjacency
127 && neighbs.shown >= List.length (Lazy.force neighbs.adjacency)
129 (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
132 Pp.header ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
137 let suri = UriManager.string_of_uri uri in
139 ~attrs:([ "href", UriManager.string_of_uri uri;
140 (*"label", UriManager.name_of_uri uri*)
141 ] @ (if is_complete uri then [] else incomplete_attrs))
143 let new_nodes = ref [] in
145 let neighbs = UriTbl.find adjlist uri in
146 if Lazy.lazy_is_val neighbs.adjacency then begin
148 HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
152 let uri1, uri2 = if invert then dest, uri else uri, dest in
153 Pp.edge (UriManager.string_of_uri uri1)
154 (UriManager.string_of_uri uri2) fmt)
156 new_nodes := adjacency
158 with Not_found -> ());
159 aux (!new_nodes @ tl)
164 let expand uri (adjlist, _root, f, _invert) =
165 (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*)
167 let neighbs = UriTbl.find adjlist uri in
168 if not (Lazy.lazy_is_val neighbs.adjacency) then
169 (* node has never been expanded *)
170 let adjacency = Lazy.force neighbs.adjacency in
171 let weight = min (List.length adjacency) fat_value in
174 (* perform look ahead of 1 edge to avoid making as expandable nodes
175 * which have no outgoing edges *)
176 let next_level = f dest in
178 if List.length next_level = 0 then begin
179 (* no further outgoing edges, "expand" the node right now *)
180 let lazy_val = lazy next_level in
181 ignore (Lazy.force lazy_val);
182 { adjacency = lazy_val; shown = 0 }
184 { adjacency = lazy next_level; shown = 0 }
186 (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*)
187 UriTbl.add adjlist dest neighborhood)
189 neighbs.shown <- weight;
190 fst (HExtlib.split_nth weight adjacency), weight
191 else begin (* nodes has been expanded at least once *)
192 let adjacency = Lazy.force neighbs.adjacency in
193 let total_nodes = List.length adjacency in
194 if neighbs.shown < total_nodes then begin
195 (* some more children to show ... *)
196 let shown_before = neighbs.shown in
197 neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
198 let new_shown = neighbs.shown - shown_before in
199 (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
201 [], 0 (* all children are already shown *)
204 (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*)
207 let collapse uri (adjlist, _root, f, _invert) =
209 let neighbs = UriTbl.find adjlist uri in
210 if Lazy.lazy_is_val neighbs.adjacency then
211 (* do not collapse already collapsed nodes *)
212 if Lazy.force neighbs.adjacency <> [] then
213 (* do not collapse nodes with no outgoing edges *)
214 UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 }
216 (* do not add a collapsed node if it was not part of the graph *)
219 let graph_of_fun ?(invert = false) f ~dbd uri =
221 (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*)
222 let uris = fst (List.split (f ~dbd uri)) in
223 let uriset = List.fold_right UriSet.add uris UriSet.empty in
224 let res = UriSet.elements uriset in
225 (*eprintf "returned uris: %s\n%!"*)
226 (*(String.concat " " (List.map UriManager.string_of_uri res));*)
229 let adjlist = UriTbl.create 17 in
230 let gen_f = f ~dbd in
231 UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 };
232 let dep_graph = adjlist, uri, gen_f, invert in
233 let rec rec_expand weight =
236 | uri :: tl when weight >= fat_value -> ()
238 let new_nodes, increase = expand uri dep_graph in
239 rec_expand (weight + increase) (new_nodes @ tl) in
243 let direct_deps = graph_of_fun direct_deps
244 let inverse_deps = graph_of_fun ~invert:true inverse_deps
246 let expand uri graph =
248 ignore (expand uri graph)