X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fmetadata%2FmetadataDeps.ml;fp=components%2Fmetadata%2FmetadataDeps.ml;h=d34bd1c83eb9241bea1549a2f8527d583c27abd1;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/metadata/metadataDeps.ml b/components/metadata/metadataDeps.ml new file mode 100644 index 000000000..d34bd1c83 --- /dev/null +++ b/components/metadata/metadataDeps.ml @@ -0,0 +1,305 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MetadataTypes + +module Pp = GraphvizPp.Dot +module UriSet = UriManager.UriSet + +let strip_prefix s = + let prefix_len = String.length position_prefix in + String.sub s prefix_len (String.length s - prefix_len) + +let parse_pos = + function + | Some s, Some d -> + (match strip_prefix s with + | "MainConclusion" -> `MainConclusion (Some (Eq (int_of_string d))) + | "MainHypothesis" -> `MainHypothesis (Some (Eq (int_of_string d))) + | s -> + prerr_endline ("Invalid main position: " ^ s); + assert false) + | Some s, None -> + (match strip_prefix s with + | "InConclusion" -> `InConclusion + | "InHypothesis" -> `InHypothesis + | "InBody" -> `InBody + | s -> + prerr_endline ("Invalid position: " ^ s); + assert false) + | _ -> assert false + +let unbox_row = function `Obj (uri, pos) -> (uri, pos) + +let direct_deps ~dbd uri = + let obj_metadata_of_row = + function + | [| Some _; Some occurrence; pos; depth |] -> + `Obj (UriManager.uri_of_string occurrence, parse_pos (pos, depth)) + | _ -> + prerr_endline "invalid (direct) refObj metadata row"; + assert false + in + let do_query (dbtype, tbl) = + let res = + HSql.exec dbtype dbd (SqlStatements.direct_deps tbl uri dbtype dbd) + in + let deps = + HSql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in + deps + in + do_query (HSql.User, MetadataTypes.obj_tbl ()) + @ do_query (HSql.Library, MetadataTypes.library_obj_tbl) + @ do_query (HSql.Legacy, MetadataTypes.library_obj_tbl) + +let inverse_deps ~dbd uri = + let inv_obj_metadata_of_row = + function + | [| Some src; Some _; pos; depth |] -> + `Obj (UriManager.uri_of_string src, parse_pos (pos, depth)) + | _ -> + prerr_endline "invalid (inverse) refObj metadata row"; + assert false + in + let do_query (dbtype, tbl) = + let res = + HSql.exec dbtype dbd (SqlStatements.inverse_deps tbl uri dbtype dbd) + in + let deps = + HSql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in + deps + in + do_query (HSql.User, MetadataTypes.obj_tbl ()) + @ do_query (HSql.Library, MetadataTypes.library_obj_tbl) + @ do_query (HSql.Legacy, MetadataTypes.library_obj_tbl) + +let topological_sort ~dbd uris = + let module OrderedUri = + struct + type t = UriManager.uri + let compare = UriManager.compare + end in + let module Topo = HTopoSort.Make(OrderedUri) in + Topo.topological_sort uris + (fun uri -> fst (List.split (direct_deps ~dbd uri))) + +let sorted_uris_of_baseuri ~dbd baseuri = + let sql_pat = + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" baseuri ^ "%" + in + let query dbtype tbl = + Printf.sprintf + ("SELECT source FROM %s WHERE source LIKE \"%s\" " + ^^ HSql.escape_string_for_like dbtype dbd) + tbl sql_pat + in + let map cols = match cols.(0) with + | Some s -> UriManager.uri_of_string s + | _ -> assert false + in + let uris = + List.fold_left + (fun acc (dbtype, table) -> + let result = HSql.exec dbtype dbd (query dbtype table) in + HSql.map result map @ acc) + [] + [HSql.User, MetadataTypes.name_tbl (); + HSql.Library, MetadataTypes.library_name_tbl; + HSql.Legacy, MetadataTypes.library_name_tbl] + in + let sorted_uris = topological_sort ~dbd uris in + let filter_map uri = + let s = + Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" + (UriManager.string_of_uri uri) + in + try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None + with Not_found -> Some (UriManager.uri_of_string s) + in + HExtlib.filter_map filter_map sorted_uris + +module DepGraph = +struct + module UriTbl = UriManager.UriHashtbl + + let fat_value = 20 + let fat_increment = fat_value + let incomplete_attrs = ["style", "dashed"] + let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"] + + let label_of_uri uri = UriManager.name_of_uri uri + (*let label_of_uri uri = UriManager.string_of_uri uri*) + + type neighborhood = + { adjacency: UriManager.uri list lazy_t; (* all outgoing edges *) + mutable shown: int (* amount of edges to show *) + } + + (** + * All dependency graph have a single root, it is kept here to have a + * starting point for graph traversals *) + type t = + neighborhood UriTbl.t * UriManager.uri + * (UriManager.uri -> UriManager.uri list) * bool + + let dummy = + UriTbl.create 0, UriManager.uri_of_string "cic:/a.con", + (fun _ -> []), false + + let render fmt (adjlist, root, _f, invert) = + let is_complete uri = + try + let neighbs = UriTbl.find adjlist uri in + Lazy.lazy_is_val neighbs.adjacency + && neighbs.shown >= List.length (Lazy.force neighbs.adjacency) + with Not_found -> + (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*) + assert false + in + Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt; + let rec aux = + function + | [] -> () + | uri :: tl -> + let suri = UriManager.string_of_uri uri in + Pp.node suri + ~attrs:([ "href", UriManager.string_of_uri uri; + "label", label_of_uri uri + ] @ (if is_complete uri then [] else incomplete_attrs)) + fmt; + let new_nodes = ref [] in + (try + let neighbs = UriTbl.find adjlist uri in + if Lazy.lazy_is_val neighbs.adjacency then begin + let adjacency, _ = + HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency) + in + List.iter + (fun dest -> + let uri1, uri2 = if invert then dest, uri else uri, dest in + Pp.edge (UriManager.string_of_uri uri1) + (UriManager.string_of_uri uri2) fmt) + adjacency; + new_nodes := adjacency + end; + with Not_found -> ()); + aux (!new_nodes @ tl) + in + aux [root]; + Pp.trailer fmt + + let expand uri (adjlist, _root, f, _invert) = + (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*) + try + let neighbs = UriTbl.find adjlist uri in + if not (Lazy.lazy_is_val neighbs.adjacency) then + (* node has never been expanded *) + let adjacency = Lazy.force neighbs.adjacency in + let weight = min (List.length adjacency) fat_value in + List.iter + (fun dest -> + (* perform look ahead of 1 edge to avoid making as expandable nodes + * which have no outgoing edges *) + let next_level = f dest in + let neighborhood = + if List.length next_level = 0 then begin + (* no further outgoing edges, "expand" the node right now *) + let lazy_val = lazy next_level in + ignore (Lazy.force lazy_val); + { adjacency = lazy_val; shown = 0 } + end else + { adjacency = lazy next_level; shown = 0 } + in + (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*) + UriTbl.add adjlist dest neighborhood) + adjacency; + neighbs.shown <- weight; + fst (HExtlib.split_nth weight adjacency), weight + else begin (* nodes has been expanded at least once *) + let adjacency = Lazy.force neighbs.adjacency in + let total_nodes = List.length adjacency in + if neighbs.shown < total_nodes then begin + (* some more children to show ... *) + let shown_before = neighbs.shown in + neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes; + let new_shown = neighbs.shown - shown_before in + (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown + end else + [], 0 (* all children are already shown *) + end + with Not_found -> + (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*) + [], 0 + + let collapse uri (adjlist, _root, f, _invert) = + try + let neighbs = UriTbl.find adjlist uri in + if Lazy.lazy_is_val neighbs.adjacency then + (* do not collapse already collapsed nodes *) + if Lazy.force neighbs.adjacency <> [] then + (* do not collapse nodes with no outgoing edges *) + UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 } + with Not_found -> + (* do not add a collapsed node if it was not part of the graph *) + () + + let graph_of_fun ?(invert = false) f ~dbd uri = + let f ~dbd uri = + (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*) + let uris = fst (List.split (f ~dbd uri)) in + let uriset = List.fold_right UriSet.add uris UriSet.empty in + let res = UriSet.elements uriset in + (*eprintf "returned uris: %s\n%!"*) + (*(String.concat " " (List.map UriManager.string_of_uri res));*) + res + in + let adjlist = UriTbl.create 17 in + let gen_f = f ~dbd in + UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 }; + let dep_graph = adjlist, uri, gen_f, invert in + let rec rec_expand weight = + function + | [] -> () + | uri :: tl when weight >= fat_value -> () + | uri :: tl -> + let new_nodes, increase = expand uri dep_graph in + rec_expand (weight + increase) (new_nodes @ tl) in + rec_expand 1 [uri]; + dep_graph + + let direct_deps = graph_of_fun direct_deps + let inverse_deps = graph_of_fun ~invert:true inverse_deps + + let expand uri graph = + try + ignore (expand uri graph) + with Not_found -> () +end +