From: Stefano Zacchiroli Date: Wed, 19 Jul 2006 17:32:43 +0000 (+0000) Subject: New module to extract from the Db direct and inverse dependencies starting from X-Git-Tag: 0.4.95@7852~1174 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0084c5ce13f5a2ab9622adbcaa5b3b41202d17e;p=helm.git New module to extract from the Db direct and inverse dependencies starting from a given URI. Both single step and recursive (in graph form) dependencies are supported. --- diff --git a/components/metadata/.depend b/components/metadata/.depend index 04197957b..492a34e3a 100644 --- a/components/metadata/.depend +++ b/components/metadata/.depend @@ -2,6 +2,7 @@ metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi metadataDb.cmi: metadataTypes.cmi +metadataDeps.cmi: metadataTypes.cmi sqlStatements.cmo: sqlStatements.cmi sqlStatements.cmx: sqlStatements.cmi metadataTypes.cmo: metadataTypes.cmi @@ -18,3 +19,5 @@ metadataDb.cmo: metadataTypes.cmi metadataPp.cmi metadataExtractor.cmi \ metadataConstraints.cmi metadataDb.cmi metadataDb.cmx: metadataTypes.cmx metadataPp.cmx metadataExtractor.cmx \ metadataConstraints.cmx metadataDb.cmi +metadataDeps.cmo: sqlStatements.cmi metadataTypes.cmi metadataDeps.cmi +metadataDeps.cmx: sqlStatements.cmx metadataTypes.cmx metadataDeps.cmi diff --git a/components/metadata/Makefile b/components/metadata/Makefile index 6c9aa763c..9943237dd 100644 --- a/components/metadata/Makefile +++ b/components/metadata/Makefile @@ -7,7 +7,9 @@ INTERFACE_FILES = \ metadataExtractor.mli \ metadataPp.mli \ metadataConstraints.mli \ - metadataDb.mli + metadataDb.mli \ + metadataDeps.mli \ + $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/components/metadata/metadataDeps.ml b/components/metadata/metadataDeps.ml new file mode 100644 index 000000000..c6dcd1e90 --- /dev/null +++ b/components/metadata/metadataDeps.ml @@ -0,0 +1,243 @@ +(* 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 tbl = + let res = HMysql.exec dbd (SqlStatements.direct_deps tbl uri) in + let deps = + HMysql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in + deps + in + do_query (MetadataTypes.obj_tbl ()) + @ do_query 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 tbl = + let res = HMysql.exec dbd (SqlStatements.inverse_deps tbl uri) in + let deps = + HMysql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in + deps + in + do_query (MetadataTypes.obj_tbl ()) + @ do_query MetadataTypes.library_obj_tbl + +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", "9"; "width", ".4"; "height", ".4"] + + 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_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", UriManager.name_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 (* 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 = shown_before - neighbs.shown in + (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown + end else + [], 0 (* all children are already shown *) + with Not_found -> + (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*) + [], 0 + + let collapse uri (adjlist, _root, f, _invert) = + (* do not add a collapsed node if it was not part of the graph *) + if UriTbl.mem adjlist uri then + UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 } + + 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 + diff --git a/components/metadata/metadataDeps.mli b/components/metadata/metadataDeps.mli new file mode 100644 index 000000000..ee0954d05 --- /dev/null +++ b/components/metadata/metadataDeps.mli @@ -0,0 +1,56 @@ +(* 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/ + *) + + (** @return the one step direct dependencies of an object, specified by URI + * (that is, the list of objects on which an given one depends) *) +val direct_deps: + dbd:HMysql.dbd -> + UriManager.uri -> (UriManager.uri * MetadataTypes.position) list + + (** @return the one step inverse dependencies of an objects, specified by URI + * (that is, the list of objects which depends on a given object) *) +val inverse_deps: + dbd:HMysql.dbd -> + UriManager.uri -> (UriManager.uri * MetadataTypes.position) list + + (** Representation of a (lazy) dependency graph. + * Imperative data structure. *) +module DepGraph: +sig + type t + + val dummy: t + + val expand: UriManager.uri -> t -> unit (** ignores uri not found *) + val collapse: UriManager.uri -> t -> unit (** ignores uri not found *) + val render: Format.formatter -> t -> unit + + (** @return the transitive closure of direct_deps *) + val direct_deps: dbd:HMysql.dbd -> UriManager.uri -> t + + (** @return the transitive closure of inverse_deps *) + val inverse_deps: dbd:HMysql.dbd -> UriManager.uri -> t +end +