]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/metadata/metadataDeps.ml
Implemented topological sorting according to the dependencies.
[helm.git] / helm / software / components / metadata / metadataDeps.ml
1 (* Copyright (C) 2006, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 open MetadataTypes
29
30 module Pp = GraphvizPp.Dot
31 module UriSet = UriManager.UriSet
32
33 let strip_prefix s =
34   let prefix_len = String.length position_prefix in
35   String.sub s prefix_len (String.length s - prefix_len)
36
37 let parse_pos =
38   function
39     | Some s, Some d ->
40         (match strip_prefix s with
41         | "MainConclusion" -> `MainConclusion (Some (Eq (int_of_string d)))
42         | "MainHypothesis" -> `MainHypothesis (Some (Eq (int_of_string d)))
43         | s ->
44             prerr_endline ("Invalid main position: " ^ s);
45             assert false)
46     | Some s, None ->
47         (match strip_prefix s with
48         | "InConclusion" -> `InConclusion
49         | "InHypothesis" -> `InHypothesis
50         | "InBody" -> `InBody
51         | s ->
52             prerr_endline ("Invalid position: " ^ s);
53             assert false)
54     | _ -> assert false
55
56 let unbox_row = function `Obj (uri, pos) -> (uri, pos)
57
58 let direct_deps ~dbd uri =
59   let obj_metadata_of_row =
60     function
61       | [| Some _; Some occurrence; pos; depth |] ->
62           `Obj (UriManager.uri_of_string occurrence, parse_pos (pos, depth))
63       | _ ->
64           prerr_endline "invalid (direct) refObj metadata row";
65           assert false 
66   in
67   let do_query tbl =
68     let res = HMysql.exec dbd (SqlStatements.direct_deps tbl uri) in
69     let deps =
70       HMysql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in
71     deps
72   in
73   do_query (MetadataTypes.obj_tbl ())
74     @ do_query MetadataTypes.library_obj_tbl
75
76 let inverse_deps ~dbd uri =
77   let inv_obj_metadata_of_row =
78     function
79       | [| Some src; Some _; pos; depth |] ->
80           `Obj (UriManager.uri_of_string src, parse_pos (pos, depth))
81       | _ ->
82           prerr_endline "invalid (inverse) refObj metadata row";
83           assert false 
84   in
85   let do_query tbl =
86     let res = HMysql.exec dbd (SqlStatements.inverse_deps tbl uri) in
87     let deps =
88       HMysql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in
89     deps
90   in
91   do_query (MetadataTypes.obj_tbl ())
92     @ do_query MetadataTypes.library_obj_tbl
93
94 let topological_sort ~dbd uris =
95  let module OrderedUri =
96   struct
97    type t = UriManager.uri
98    let compare = UriManager.compare
99   end in
100  let module Topo = HTopoSort.Make(OrderedUri) in
101   Topo.topological_sort uris
102    (fun uri -> fst (List.split (direct_deps ~dbd uri)))
103
104 module DepGraph =
105 struct
106   module UriTbl = UriManager.UriHashtbl
107
108   let fat_value = 20
109   let fat_increment = fat_value
110   let incomplete_attrs = ["style", "dashed"]
111   let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"]
112
113   let label_of_uri uri = UriManager.name_of_uri uri
114   (*let label_of_uri uri = UriManager.string_of_uri uri*)
115
116   type neighborhood =
117     { adjacency: UriManager.uri list lazy_t;  (* all outgoing edges *)
118       mutable shown: int                      (* amount of edges to show *)
119     }
120
121     (** <adjacency list of the dependency graph,
122      *   root,
123      *   generator function,
124      *   invert edges on render?>
125      * All dependency graph have a single root, it is kept here to have a
126      * starting point for graph traversals *)
127   type t =
128     neighborhood UriTbl.t * UriManager.uri
129       * (UriManager.uri -> UriManager.uri list) * bool
130
131   let dummy =
132     UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
133       (fun _ -> []), false
134
135   let render fmt (adjlist, root, _f, invert) =
136     let is_complete uri =
137       try
138         let neighbs = UriTbl.find adjlist uri in
139         Lazy.lazy_is_val neighbs.adjacency
140           && neighbs.shown >= List.length (Lazy.force neighbs.adjacency)
141       with Not_found ->
142         (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
143         assert false
144     in
145     Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
146     let rec aux =
147       function
148         | [] -> ()
149         | uri :: tl ->
150             let suri = UriManager.string_of_uri uri in
151             Pp.node suri
152               ~attrs:([ "href", UriManager.string_of_uri uri;
153                         "label", label_of_uri uri
154                 ] @ (if is_complete uri then [] else incomplete_attrs))
155               fmt;
156             let new_nodes = ref [] in
157             (try
158               let neighbs = UriTbl.find adjlist uri in
159               if Lazy.lazy_is_val neighbs.adjacency then begin
160                 let adjacency, _ =
161                   HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
162                 in
163                 List.iter
164                   (fun dest ->
165                     let uri1, uri2 = if invert then dest, uri else uri, dest in
166                     Pp.edge (UriManager.string_of_uri uri1)
167                       (UriManager.string_of_uri uri2) fmt)
168                   adjacency;
169                 new_nodes := adjacency
170               end;
171             with Not_found -> ());
172             aux (!new_nodes @ tl)
173     in
174     aux [root];
175     Pp.trailer fmt
176
177   let expand uri (adjlist, _root, f, _invert) =
178     (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*)
179     try
180       let neighbs = UriTbl.find adjlist uri in
181       if not (Lazy.lazy_is_val neighbs.adjacency) then
182           (* node has never been expanded *)
183         let adjacency = Lazy.force neighbs.adjacency in
184         let weight = min (List.length adjacency) fat_value in
185         List.iter
186           (fun dest ->
187             (* perform look ahead of 1 edge to avoid making as expandable nodes
188              * which have no outgoing edges *)
189             let next_level = f dest in
190             let neighborhood =
191               if List.length next_level = 0 then begin
192                 (* no further outgoing edges, "expand" the node right now *)
193                 let lazy_val = lazy next_level in
194                 ignore (Lazy.force lazy_val);
195                 { adjacency = lazy_val; shown = 0 }
196               end else
197                 { adjacency = lazy next_level; shown = 0 }
198             in
199             (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*)
200             UriTbl.add adjlist dest neighborhood)
201           adjacency;
202         neighbs.shown <- weight;
203         fst (HExtlib.split_nth weight adjacency), weight
204       else begin  (* nodes has been expanded at least once *)
205         let adjacency = Lazy.force neighbs.adjacency in
206         let total_nodes = List.length adjacency in
207         if neighbs.shown < total_nodes then begin
208           (* some more children to show ... *)
209           let shown_before = neighbs.shown in
210           neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
211           let new_shown = neighbs.shown - shown_before in
212           (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
213         end else
214           [], 0 (* all children are already shown *)
215       end
216     with Not_found ->
217       (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*)
218       [], 0
219
220   let collapse uri (adjlist, _root, f, _invert) =
221     try
222       let neighbs = UriTbl.find adjlist uri in
223       if Lazy.lazy_is_val neighbs.adjacency then
224         (* do not collapse already collapsed nodes *)
225         if Lazy.force neighbs.adjacency <> [] then
226           (* do not collapse nodes with no outgoing edges *)
227           UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 }
228     with Not_found ->
229       (* do not add a collapsed node if it was not part of the graph *)
230       ()
231
232   let graph_of_fun ?(invert = false) f ~dbd uri =
233     let f ~dbd uri =
234       (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*)
235       let uris = fst (List.split (f ~dbd uri)) in
236       let uriset = List.fold_right UriSet.add uris UriSet.empty in
237       let res = UriSet.elements uriset in
238       (*eprintf "returned uris: %s\n%!"*)
239         (*(String.concat " " (List.map UriManager.string_of_uri res));*)
240       res
241     in
242     let adjlist = UriTbl.create 17 in
243     let gen_f = f ~dbd in
244     UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 };
245     let dep_graph = adjlist, uri, gen_f, invert in
246     let rec rec_expand weight =
247       function
248         | [] -> ()
249         | uri :: tl when weight >= fat_value -> ()
250         | uri :: tl ->
251             let new_nodes, increase = expand uri dep_graph in
252             rec_expand (weight + increase) (new_nodes @ tl) in
253     rec_expand 1 [uri];
254     dep_graph
255
256   let direct_deps = graph_of_fun direct_deps
257   let inverse_deps = graph_of_fun ~invert:true inverse_deps
258
259   let expand uri graph =
260     try
261       ignore (expand uri graph)
262     with Not_found -> ()
263 end
264