helm/hxp/hxpTop.ml

   1 (* Copyright (C) 2000, 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://www.cs.unibo.it/helm/.
  24  *)
  25
  26 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  27  *)
  28
  29 module T = HxpTypes
  30
  31 module X = HxpXML.Make
  32
  33 let build = ref "EXPORT"
  34
  35 let lib = ref Filename.current_dir_name
  36
  37 let uq s = String.sub s 1 (String.length s - 2)
  38
  39 let rec esc s =
  40     try
  41        let i = String.index s '\'' in
  42        let l = String.length s in
  43        String.sub s 0 i ^ "\\\'" ^ esc (String.sub s (succ i) (l - succ i))
  44     with Not_found -> s
  45
  46 let split_filename f =
  47    let len = String.length f in
  48    let dot = String.rindex f '.' in
  49    let slash = String.rindex f '/' in
  50    let path = String.sub f 0 slash in
  51    let name = String.sub f (succ slash) (dot - succ slash) in
  52    let ext  = String.sub f (succ dot) (len - succ dot) in
  53    (path, (name, ext))
  54
  55 let ins0 name filter =
  56    let sort = ref "\"\"" in
  57    let relative = ref 0 in
  58    let count = ref 0 in
  59    let max = ref 0 in
  60    let flags = String.create 3 in
  61    let set_flags_for = function
  62       | T.XML_Open "LAMBDA"  -> flags.[0] <- 'L'
  63       | T.XML_Open "MUTCASE" -> flags.[1] <- 'C'
  64       | T.XML_Open "FIX"     -> flags.[2] <- 'F'
  65       | T.XML_Open "COFIX"   -> flags.[2] <- 'F'
  66       | _                    -> ()
  67    in
  68    let rec skip_premises h =
  69       match X.xnext h with
  70          | h, (T.XML_Attribute _, _) -> skip_premises h
  71          | h, (T.XML_End, _)         -> skip_premises h
  72          | h, (T.XML_Open "PROD", i) ->
  73             let h =
  74                if ! sort = "\"\"" then
  75                   match X.xnext h with
  76                      | h, (T.XML_Attribute ("type", str), _) -> sort := str; h
  77                      | h, _                                  -> sort := ""; h
  78                else h
  79             in
  80             let h = X.scan_for h (T.XML_Close "source", succ i) in
  81             let h, (obj, i) = X.xnext h in
  82             relative := i + 2; (* XML_Open "target" *)
  83             skip_premises h
  84          | h, (obj, _)             ->
  85             print_string (! sort ^ " " ^ T.string_of_object obj);
  86             set_flags_for obj; h
  87    in
  88    let rec ins_aux h =
  89       match X.xnext h with
  90          | h, (T.XML_Done, _)                 -> h
  91          | h, (T.XML_Attribute ("uri", v), i) ->
  92             incr count;
  93             if i > ! max then max := i;
  94             ins_aux h
  95          | h, (obj, _)                      ->
  96             set_flags_for obj; ins_aux h
  97    in
  98    if snd (snd (split_filename name)) = "con" then begin
  99       flags.[0] <- '-'; flags.[1] <- '-'; flags.[2] <- '-';
 100       let h = X.start (Filename.concat ! lib (name ^ ".xml")) filter in
 101       let h = X.scan_for h (T.XML_Open "type", 3) in
 102       X.stop (ins_aux (skip_premises h));
 103       print_endline (" \"cic:" ^ name ^ "\" " ^ flags ^
 104                      " count " ^ string_of_int ! count ^
 105                      " max_depth " ^ string_of_int (! max - ! relative) ^
 106                      " <p>");
 107       flush stdout
 108    end
 109
 110 type style_t = HTML | PG | RDF
 111
 112 let ins1 style name filter =
 113    let maior = ref 0 in
 114    let minor = ref (-1) in
 115    let make_uris () =
 116       let make_ref pre sep post =
 117          if ! maior > 0 then
 118             name ^ pre ^ string_of_int ! maior ^
 119             (if ! minor > 0 then sep ^ string_of_int ! minor else "") ^ post
 120          else name
 121       in
 122       incr minor;
 123       (make_ref "#xpointer(1/" "/" ")", make_ref "," "," "")
 124    in
 125    let out_alias n =
 126       match style with
 127          | HTML ->
 128             print_endline ("\"" ^ n ^ "\" alias of \"cic:" ^
 129                            fst (make_uris ()) ^ "\" <p>")
 130          | PG ->
 131             print_endline ("cic:/" ^ fst (make_uris ()) ^ "\t" ^ n)
 132          | RDF ->
 133             let uris = make_uris () in
 134             let dir = ! build ^ fst (split_filename name) in
 135             let rc = Sys.command ("mkdir -p " ^ esc dir) in
 136             let och = open_out (! build ^ snd uris ^ ".xml") in
 137             output_string och "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n";
 138             output_string och "<rdf:RDF xml:lang=\"en\"\n";
 139             output_string och "         xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\"\n";
 140             output_string och "         xmlns:h=\"http://www.cs.unibo.it/helm/schemas/mattone.rdf#\">\n";
 141             output_string och ("   <h:Object rdf:about=\"cic:" ^ fst uris ^ "\">\n");
 142             output_string och ("      <h:name>" ^ n ^ "</h:name>\n");
 143             output_string och "   </h:Object>\n";
 144             output_string och "</rdf:RDF>\n";
 145             close_out och;
 146 (*          print_endline ("\"" ^ fst uris ^ "\" alias \"" ^ n ^ "\"")
 147 *) in
 148    let rec ins_aux h =
 149       match X.xnext h with
 150          | h, (T.XML_Done, _)                  -> h
 151          | h, (T.XML_Attribute ("name", n), i) ->
 152             if i = 4 then begin incr maior; minor := -1; out_alias (uq n) end else
 153             if i = 5 then out_alias (uq n);
 154             ins_aux h
 155          | h, _                                -> ins_aux h
 156    in
 157    let split = snd (split_filename name) in
 158    if snd split <> "ind" then out_alias (fst split) else
 159       let h = X.start (Filename.concat ! lib (name ^ ".xml")) filter in
 160       X.stop (ins_aux h);
 161    flush stdout
 162
 163 let test s name filter =
 164    if s = "con-info"   then ins0 name filter else
 165    if s = "html-names" then ins1 HTML name filter else
 166    if s = "pg-names"   then ins1 PG name filter else
 167    if s = "rdf-names"  then ins1 RDF name filter else ()
 168
 169 let read_index_txt () =
 170    let uris = ref [] in
 171    let ich = open_in (Filename.concat ! lib "index.txt") in
 172    let rec aux () =
 173       let line = input_line ich in
 174       let p0 = succ (String.index line '/') in
 175       let p1 = succ (String.rindex line '.') in
 176       let uri = String.sub line p0 (p1 - p0) in
 177       let ext = String.sub line p1 (String.length line - p1) in
 178       match ext with
 179          | "con gz" -> uris := (uri ^ "con", true) :: ! uris; aux ()
 180          | "ind gz" -> uris := (uri ^ "ind", true) :: ! uris; aux ()
 181          | "var gz" -> uris := (uri ^ "var", true) :: ! uris; aux ()
 182          | "con"    -> uris := (uri ^ "con", false) :: ! uris; aux ()
 183          | "ind"    -> uris := (uri ^ "ind", false) :: ! uris; aux ()
 184          | "var"    -> uris := (uri ^ "var", false) :: ! uris; aux ()
 185          | _        -> aux ()
 186    in
 187    begin try aux () with End_of_file -> close_in ich end; ! uris
 188
 189 let read_xml s =
 190    let l = read_index_txt () in
 191    let rec loop_on = function
 192       | []                    -> ()
 193       | (uri, filter) :: tail -> test s uri filter; loop_on tail
 194    in loop_on l;
 195    prerr_endline ("total time: " ^ string_of_float (Sys.time ()) ^ " seconds")
 196 (*
 197 let get_timing () =
 198    let lexbuf = Lexing.from_channel stdin in
 199    let tm = ref [] in
 200    let cont = ref true in
 201    while ! cont do
 202       let data = Parser.tm Lexer.tmt lexbuf in
 203       if fst data > 0. then begin
 204          let d = (fst data, snd data, snd data /. fst data) in
 205          tm := d :: ! tm end else
 206       if fst data < 0. then cont := false else
 207          print_endline ("[" ^ string_of_int (1 + List.length ! tm) ^ "] ");
 208    done; print_newline (); ! tm
 209
 210 let compare1 (r1, t1, p1) (r2, t2, p2) =
 211    if r1 > r2 then 1 else
 212    if r1 < r2 then -1 else
 213    if p1 > p2 then 1 else
 214    if p1 < p2 then -1 else 0
 215
 216 let rec count min max = function
 217    | []                -> 0
 218    | (r, _, _) :: tail ->
 219       let p = count min max tail in
 220       if r >= min && r <= max then succ p else p
 221
 222 let mean min max l =
 223    let num = ref 0. in
 224    let sum = ref 0. in
 225    let rec mean_aux = function
 226       | []                -> ! sum /. ! num
 227       | (r, _, p) :: tail ->
 228          if r >= min && r <= max then begin
 229             num := ! num +. 1.; sum := ! sum +. p; mean_aux tail end
 230          else mean_aux tail
 231    in mean_aux l
 232
 233 let variance min max m l =
 234    let num = ref 0. in
 235    let sum = ref 0. in
 236    let rec variance_aux = function
 237       | []                -> ! sum /. ! num
 238       | (r, _, p) :: tail ->
 239          if r >= min && r <= max then begin
 240             num := ! num +. 1.; sum := ! sum +. (p -. m) *. (p -. m);
 241             variance_aux tail end
 242          else variance_aux tail
 243    in sqrt (variance_aux l)
 244
 245 let read_timing min max =
 246    let l = List.sort compare1 (get_timing ()) in
 247    let c = count min max l in
 248    let m = mean min max l in
 249    let v = variance min max m l in
 250    print_timing l;
 251    print_endline (string_of_int c ^ " " ^ string_of_float m ^ " " ^
 252                   string_of_float v);
 253    flush stdout
 254
 255 let diff_timing () =
 256    let rec diff_aux = function
 257       | ((r1, q1, p1) :: t1, (r2, q2, p2) :: t2) when r1 = r2 ->
 258          (r1, q1 -. q2, p1 -. p2) :: diff_aux (t1, t2)
 259       | ([], []) -> print_newline (); []
 260       | (_ :: t1, _ :: t2) ->
 261          print_string ("[" ^ string_of_int (1 + List.length t1) ^ "] ");
 262          diff_aux (t1, t2)
 263       | _ -> assert false
 264    in
 265    let l1 = get_timing () in
 266    let l2 = get_timing () in
 267    print_string (string_of_int (List.length l1) ^ " ");
 268    print_string (string_of_int (List.length l2) ^ "\n");
 269    diff_aux (l1, l2)
 270
 271 let comp_timing min max =
 272    let l = List.sort compare1 (diff_timing ()) in
 273    let c = count min max l in
 274    let m = mean min max l in
 275    let v = variance min max m l in
 276    print_timing l;
 277    print_endline (string_of_int c ^ " " ^ string_of_float m ^ " " ^
 278                   string_of_float v);
 279    flush stdout
 280
 281 let print file =
 282    let rec print_aux () =
 283       let xobj = Xml.xnext() in
 284       if fst xobj = XML_Done then () else
 285       begin print_endline (string_of_xobject xobj); print_aux () end
 286    in Xml.start file false; print_aux (); Xml.stop ()
 287
 288 let count_bytes s =
 289    let mbytes = ref 0.0 in
 290    let num = ref 0 in
 291    let k = 1024.0 ** float (int_of_string s) in
 292    let rec count_bytes_aux () =
 293       try
 294          let s = read_line () in
 295          (* prerr_endline ("*" ^ s ^ "*"); *)
 296          let j = String.rindex s ' ' in
 297          let i =
 298             try succ (String.rindex_from s (pred j) ' ')
 299             with Not_found -> 0 in
 300          (* prerr_endline ("*" ^ String.sub s i (j - i) ^ "*"); *)
 301          let b = int_of_string (String.sub s i (j - i)) in
 302          mbytes := ! mbytes +. float b /. k; incr num;
 303          count_bytes_aux ()
 304       with End_of_file -> ()
 305    in
 306    count_bytes_aux ();
 307    prerr_endline (string_of_int ! num ^ " " ^ string_of_float ! mbytes)
 308 *)
 309
 310 let _ =
 311    let usage = "Usage: hxp [-lx <dir>] [-p <action>]" in
 312
 313    let _l = "    set the path to the index.txt file (default is .)" in
 314    let _x = "    set the path to the RDF export directory (default is EXPORT)" in
 315    let _r = "    read the XML files extracting the specified information
 316          <action>: con-info   produce information about .con files in HTML format
 317                    html-names produce short names' list in HTML format
 318                    pg-names   produce short names' list in Postgres input format
 319                    rdf-names  produce RDF files with short names' metadata"
 320    in
 321
 322    Arg.parse [
 323       ("-l", Arg.String (fun dir -> lib := dir), _l);
 324       ("-x", Arg.String (fun dir -> build := dir), _x);
 325       ("-r", Arg.String read_xml, _r)
 326    ] ignore usage
 327
 328 (*
 329 let parse_args () =
 330    let rec parse = function
 331       | []                                  -> ()
 332       | ("-l"|"-library") :: dir :: rem     -> lib := dir; parse rem
 333       | ("-x"|"-export") :: dir :: rem      -> build := dir; parse rem
 334       | ("-s"|"-stat") :: min :: max :: rem ->
 335          read_timing (float_of_string min) (float_of_string max); parse rem
 336       | ("-c"|"-comp") :: min :: max :: rem ->
 337          comp_timing (float_of_string min) (float_of_string max); parse rem
 338       | ("-i"|"-ins") :: s :: file :: rem   -> test s file false; parse rem
 339       | ("-t"|"-text") :: s :: rem          -> read_xml s false; parse rem
 340       | ("-z"|"-gzip") :: s :: rem          -> read_xml s true; parse rem
 341       | ("-b"|"-bytes") :: s :: rem         -> count_bytes s; parse rem
 342       | _ :: rem                            -> parse rem
 343    in
 344       parse (List.tl (Array.to_list Sys.argv))
 345 *)