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 (dbtype, tbl) =
  68     let res =
  69       HSql.exec dbtype dbd (SqlStatements.direct_deps tbl uri dbtype dbd)
  70     in
  71     let deps =
  72       HSql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in
  73     deps
  74   in
  75   do_query (HSql.User, MetadataTypes.obj_tbl ())
  76     @ do_query (HSql.Library, MetadataTypes.library_obj_tbl)
  77     @ do_query (HSql.Legacy, MetadataTypes.library_obj_tbl)
  78
  79 let inverse_deps ~dbd uri =
  80   let inv_obj_metadata_of_row =
  81     function
  82       | [| Some src; Some _; pos; depth |] ->
  83           `Obj (UriManager.uri_of_string src, parse_pos (pos, depth))
  84       | _ ->
  85           prerr_endline "invalid (inverse) refObj metadata row";
  86           assert false
  87   in
  88   let do_query (dbtype, tbl) =
  89     let res =
  90       HSql.exec dbtype dbd (SqlStatements.inverse_deps tbl uri dbtype dbd)
  91     in
  92     let deps =
  93       HSql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in
  94     deps
  95   in
  96   do_query (HSql.User, MetadataTypes.obj_tbl ())
  97     @ do_query (HSql.Library, MetadataTypes.library_obj_tbl)
  98     @ do_query (HSql.Legacy, MetadataTypes.library_obj_tbl)
  99
 100 let topological_sort ~dbd uris =
 101  let module OrderedUri =
 102   struct
 103    type t = UriManager.uri
 104    let compare = UriManager.compare
 105   end in
 106  let module Topo = HTopoSort.Make(OrderedUri) in
 107   Topo.topological_sort uris
 108    (fun uri -> fst (List.split (direct_deps ~dbd uri)))
 109
 110 let sorted_uris_of_baseuri ~dbd baseuri =
 111    let sql_pat =
 112      Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" baseuri ^ "%"
 113    in
 114    let query dbtype tbl =
 115       Printf.sprintf
 116          ("SELECT source FROM %s WHERE source LIKE \"%s\" "
 117           ^^ HSql.escape_string_for_like dbtype dbd)
 118          tbl sql_pat
 119    in
 120    let map cols = match cols.(0) with
 121       | Some s -> UriManager.uri_of_string s
 122       | _ -> assert false
 123    in
 124    let uris =
 125      List.fold_left
 126        (fun acc (dbtype, table) ->
 127           let result = HSql.exec dbtype dbd (query dbtype table) in
 128             HSql.map result map @ acc)
 129        []
 130        [HSql.User, MetadataTypes.name_tbl ();
 131        HSql.Library, MetadataTypes.library_name_tbl;
 132        HSql.Legacy, MetadataTypes.library_name_tbl]
 133    in
 134    let sorted_uris = topological_sort ~dbd uris in
 135    let filter_map uri =
 136       let s =
 137          Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
 138                       (UriManager.string_of_uri uri)
 139       in
 140       try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None
 141       with Not_found -> Some (UriManager.uri_of_string s)
 142    in
 143    HExtlib.filter_map filter_map sorted_uris
 144
 145 module DepGraph =
 146 struct
 147   module UriTbl = UriManager.UriHashtbl
 148
 149   let fat_value = 20
 150   let fat_increment = fat_value
 151   let incomplete_attrs = ["style", "dashed"]
 152   let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"]
 153
 154   let label_of_uri uri = UriManager.name_of_uri uri
 155   (*let label_of_uri uri = UriManager.string_of_uri uri*)
 156
 157   type neighborhood =
 158     { adjacency: UriManager.uri list lazy_t;  (* all outgoing edges *)
 159       mutable shown: int                      (* amount of edges to show *)
 160     }
 161
 162     (** <adjacency list of the dependency graph,
 163      *   root,
 164      *   generator function,
 165      *   invert edges on render?>
 166      * All dependency graph have a single root, it is kept here to have a
 167      * starting point for graph traversals *)
 168   type t =
 169     neighborhood UriTbl.t * UriManager.uri
 170       * (UriManager.uri -> UriManager.uri list) * bool
 171
 172   let dummy =
 173     UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
 174       (fun _ -> []), false
 175
 176   let render fmt (adjlist, root, _f, invert) =
 177     let is_complete uri =
 178       try
 179         let neighbs = UriTbl.find adjlist uri in
 180         Lazy.lazy_is_val neighbs.adjacency
 181           && neighbs.shown >= List.length (Lazy.force neighbs.adjacency)
 182       with Not_found ->
 183         (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
 184         assert false
 185     in
 186     Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
 187     let rec aux =
 188       function
 189         | [] -> ()
 190         | uri :: tl ->
 191             let suri = UriManager.string_of_uri uri in
 192             Pp.node suri
 193               ~attrs:([ "href", UriManager.string_of_uri uri;
 194                         "label", label_of_uri uri
 195                 ] @ (if is_complete uri then [] else incomplete_attrs))
 196               fmt;
 197             let new_nodes = ref [] in
 198             (try
 199               let neighbs = UriTbl.find adjlist uri in
 200               if Lazy.lazy_is_val neighbs.adjacency then begin
 201                 let adjacency, _ =
 202                   HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
 203                 in
 204                 List.iter
 205                   (fun dest ->
 206                     let uri1, uri2 = if invert then dest, uri else uri, dest in
 207                     Pp.edge (UriManager.string_of_uri uri1)
 208                       (UriManager.string_of_uri uri2) fmt)
 209                   adjacency;
 210                 new_nodes := adjacency
 211               end;
 212             with Not_found -> ());
 213             aux (!new_nodes @ tl)
 214     in
 215     aux [root];
 216     Pp.trailer fmt
 217
 218   let expand uri (adjlist, _root, f, _invert) =
 219     (*eprintf "expanding uri %s\n%!" (UriManager.string_of_uri uri);*)
 220     try
 221       let neighbs = UriTbl.find adjlist uri in
 222       if not (Lazy.lazy_is_val neighbs.adjacency) then
 223           (* node has never been expanded *)
 224         let adjacency = Lazy.force neighbs.adjacency in
 225         let weight = min (List.length adjacency) fat_value in
 226         List.iter
 227           (fun dest ->
 228             (* perform look ahead of 1 edge to avoid making as expandable nodes
 229              * which have no outgoing edges *)
 230             let next_level = f dest in
 231             let neighborhood =
 232               if List.length next_level = 0 then begin
 233                 (* no further outgoing edges, "expand" the node right now *)
 234                 let lazy_val = lazy next_level in
 235                 ignore (Lazy.force lazy_val);
 236                 { adjacency = lazy_val; shown = 0 }
 237               end else
 238                 { adjacency = lazy next_level; shown = 0 }
 239             in
 240             (*UriTbl.add adjlist dest { adjacency = lazy (f dest); shown = 0 }*)
 241             UriTbl.add adjlist dest neighborhood)
 242           adjacency;
 243         neighbs.shown <- weight;
 244         fst (HExtlib.split_nth weight adjacency), weight
 245       else begin  (* nodes has been expanded at least once *)
 246         let adjacency = Lazy.force neighbs.adjacency in
 247         let total_nodes = List.length adjacency in
 248         if neighbs.shown < total_nodes then begin
 249           (* some more children to show ... *)
 250           let shown_before = neighbs.shown in
 251           neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
 252           let new_shown = neighbs.shown - shown_before in
 253           (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
 254         end else
 255           [], 0 (* all children are already shown *)
 256       end
 257     with Not_found ->
 258       (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*)
 259       [], 0
 260
 261   let collapse uri (adjlist, _root, f, _invert) =
 262     try
 263       let neighbs = UriTbl.find adjlist uri in
 264       if Lazy.lazy_is_val neighbs.adjacency then
 265         (* do not collapse already collapsed nodes *)
 266         if Lazy.force neighbs.adjacency <> [] then
 267           (* do not collapse nodes with no outgoing edges *)
 268           UriTbl.replace adjlist uri { adjacency = lazy (f uri); shown = 0 }
 269     with Not_found ->
 270       (* do not add a collapsed node if it was not part of the graph *)
 271       ()
 272
 273   let graph_of_fun ?(invert = false) f ~dbd uri =
 274     let f ~dbd uri =
 275       (*eprintf "invoking graph fun on %s...\n%!" (UriManager.string_of_uri uri);*)
 276       let uris = fst (List.split (f ~dbd uri)) in
 277       let uriset = List.fold_right UriSet.add uris UriSet.empty in
 278       let res = UriSet.elements uriset in
 279       (*eprintf "returned uris: %s\n%!"*)
 280         (*(String.concat " " (List.map UriManager.string_of_uri res));*)
 281       res
 282     in
 283     let adjlist = UriTbl.create 17 in
 284     let gen_f = f ~dbd in
 285     UriTbl.add adjlist uri { adjacency = lazy (gen_f uri); shown = 0 };
 286     let dep_graph = adjlist, uri, gen_f, invert in
 287     let rec rec_expand weight =
 288       function
 289         | [] -> ()
 290         | uri :: tl when weight >= fat_value -> ()
 291         | uri :: tl ->
 292             let new_nodes, increase = expand uri dep_graph in
 293             rec_expand (weight + increase) (new_nodes @ tl) in
 294     rec_expand 1 [uri];
 295     dep_graph
 296
 297   let direct_deps = graph_of_fun direct_deps
 298   let inverse_deps = graph_of_fun ~invert:true inverse_deps
 299
 300   let expand uri graph =
 301     try
 302       ignore (expand uri graph)
 303     with Not_found -> ()
 304 end
 305