(* Copyright (C) 2000, 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://www.cs.unibo.it/helm/.
 *)

(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
 *)

module T = HxpTypes

module X = HxpXML.Make

let build = ref "EXPORT"

let lib = ref Filename.current_dir_name

let uq s = String.sub s 1 (String.length s - 2)

let rec esc s =
    try 
       let i = String.index s '\'' in
       let l = String.length s in
       String.sub s 0 i ^ "\\\'" ^ esc (String.sub s (succ i) (l - succ i))
    with Not_found -> s

let split_filename f =
   let len = String.length f in 
   let dot = String.rindex f '.' in
   let slash = String.rindex f '/' in
   let path = String.sub f 0 slash in
   let name = String.sub f (succ slash) (dot - succ slash) in
   let ext  = String.sub f (succ dot) (len - succ dot) in 
   (path, (name, ext))

let ins0 name filter =
   let sort = ref "\"\"" in
   let relative = ref 0 in
   let count = ref 0 in
   let max = ref 0 in
   let flags = String.create 3 in
   let set_flags_for = function
      | T.XML_Open "LAMBDA"  -> flags.[0] <- 'L'
      | T.XML_Open "MUTCASE" -> flags.[1] <- 'C'
      | T.XML_Open "FIX"     -> flags.[2] <- 'F'
      | T.XML_Open "COFIX"   -> flags.[2] <- 'F'
      | _                    -> ()
   in
   let rec skip_premises h =
      match X.xnext h with
	 | h, (T.XML_Attribute _, _) -> skip_premises h
	 | h, (T.XML_End, _)         -> skip_premises h
	 | h, (T.XML_Open "PROD", i) ->
	    let h = 
	       if ! sort = "\"\"" then 
	          match X.xnext h with
	             | h, (T.XML_Attribute ("type", str), _) -> sort := str; h
		     | h, _                                  -> sort := ""; h
	       else h
	    in
	    let h = X.scan_for h (T.XML_Close "source", succ i) in
            let h, (obj, i) = X.xnext h in  
	    relative := i + 2; (* XML_Open "target" *)
            skip_premises h	    
         | h, (obj, _)             ->
	    print_string (! sort ^ " " ^ T.string_of_object obj);
	    set_flags_for obj; h
   in
   let rec ins_aux h =
      match X.xnext h with
         | h, (T.XML_Done, _)                 -> h
	 | h, (T.XML_Attribute ("uri", v), i) ->
	    incr count;
	    if i > ! max then max := i;
	    ins_aux h
         | h, (obj, _)                      -> 
	    set_flags_for obj; ins_aux h
   in
   if snd (snd (split_filename name)) = "con" then begin  
      flags.[0] <- '-'; flags.[1] <- '-'; flags.[2] <- '-';   
      let h = X.start (Filename.concat ! lib (name ^ ".xml")) filter in
      let h = X.scan_for h (T.XML_Open "type", 3) in
      X.stop (ins_aux (skip_premises h));
      print_endline (" \"cic:" ^ name ^ "\" " ^ flags ^ 
                     " count " ^ string_of_int ! count ^
                     " max_depth " ^ string_of_int (! max - ! relative) ^ 
		     " <p>");
      flush stdout 
   end

type style_t = HTML | PG | RDF

let ins1 style name filter =
   let maior = ref 0 in
   let minor = ref (-1) in
   let make_uris () =
      let make_ref pre sep post =
         if ! maior > 0 then
            name ^ pre ^ string_of_int ! maior ^ 
	    (if ! minor > 0 then sep ^ string_of_int ! minor else "") ^ post
         else name
      in
      incr minor;
      (make_ref "#xpointer(1/" "/" ")", make_ref "," "," "")
   in 
   let out_alias n =
      match style with
         | HTML -> 
	    print_endline ("\"" ^ n ^ "\" alias of \"cic:" ^
	                   fst (make_uris ()) ^ "\" <p>")
	 | PG ->
	    print_endline ("cic:/" ^ fst (make_uris ()) ^ "\t" ^ n)
         | RDF -> 
	    let uris = make_uris () in
	    let dir = ! build ^ fst (split_filename name) in 
	    let rc = Sys.command ("mkdir -p " ^ esc dir) in 
	    let och = open_out (! build ^ snd uris ^ ".xml") in 
	    output_string och "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n";
            output_string och "<rdf:RDF xml:lang=\"en\"\n";
	    output_string och "         xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\"\n";
	    output_string och "         xmlns:h=\"http://www.cs.unibo.it/helm/schemas/mattone.rdf#\">\n";
	    output_string och ("   <h:Object rdf:about=\"cic:" ^ fst uris ^ "\">\n");
	    output_string och ("      <h:name>" ^ n ^ "</h:name>\n");
            output_string och "   </h:Object>\n";
            output_string och "</rdf:RDF>\n";
	    close_out och;
(*          print_endline ("\"" ^ fst uris ^ "\" alias \"" ^ n ^ "\"")
*) in
   let rec ins_aux h =
      match X.xnext h with
         | h, (T.XML_Done, _)                  -> h	   
	 | h, (T.XML_Attribute ("name", n), i) ->
            if i = 4 then begin incr maior; minor := -1; out_alias (uq n) end else
	    if i = 5 then out_alias (uq n);
	    ins_aux h
	 | h, _                                -> ins_aux h  
   in
   let split = snd (split_filename name) in
   if snd split <> "ind" then out_alias (fst split) else 
      let h = X.start (Filename.concat ! lib (name ^ ".xml")) filter in
      X.stop (ins_aux h);
   flush stdout 

let test s name filter =
   if s = "con-info"   then ins0 name filter else
   if s = "html-names" then ins1 HTML name filter else
   if s = "pg-names"   then ins1 PG name filter else 
   if s = "rdf-names"  then ins1 RDF name filter else ()

let read_index_txt () =
   let uris = ref [] in
   let ich = open_in (Filename.concat ! lib "index.txt") in
   let rec aux () =
      let line = input_line ich in
      let p0 = succ (String.index line '/') in
      let p1 = succ (String.rindex line '.') in
      let uri = String.sub line p0 (p1 - p0) in
      let ext = String.sub line p1 (String.length line - p1) in
      match ext with 
         | "con gz" -> uris := (uri ^ "con", true) :: ! uris; aux ()
	 | "ind gz" -> uris := (uri ^ "ind", true) :: ! uris; aux ()
	 | "var gz" -> uris := (uri ^ "var", true) :: ! uris; aux ()
         | "con"    -> uris := (uri ^ "con", false) :: ! uris; aux ()
	 | "ind"    -> uris := (uri ^ "ind", false) :: ! uris; aux ()
	 | "var"    -> uris := (uri ^ "var", false) :: ! uris; aux ()
	 | _        -> aux ()
   in 
   begin try aux () with End_of_file -> close_in ich end; ! uris

let read_xml s =
   let l = read_index_txt () in
   let rec loop_on = function
      | []                    -> ()
      | (uri, filter) :: tail -> test s uri filter; loop_on tail
   in loop_on l;
   prerr_endline ("total time: " ^ string_of_float (Sys.time ()) ^ " seconds")
(*
let get_timing () =
   let lexbuf = Lexing.from_channel stdin in
   let tm = ref [] in
   let cont = ref true in
   while ! cont do
      let data = Parser.tm Lexer.tmt lexbuf in
      if fst data > 0. then begin
         let d = (fst data, snd data, snd data /. fst data) in
         tm := d :: ! tm end else
      if fst data < 0. then cont := false else
         print_endline ("[" ^ string_of_int (1 + List.length ! tm) ^ "] ");
   done; print_newline (); ! tm

let compare1 (r1, t1, p1) (r2, t2, p2) =
   if r1 > r2 then 1 else
   if r1 < r2 then -1 else
   if p1 > p2 then 1 else
   if p1 < p2 then -1 else 0

let rec count min max = function
   | []                -> 0
   | (r, _, _) :: tail -> 
      let p = count min max tail in
      if r >= min && r <= max then succ p else p 

let mean min max l =
   let num = ref 0. in
   let sum = ref 0. in
   let rec mean_aux = function
      | []                -> ! sum /. ! num
      | (r, _, p) :: tail ->
         if r >= min && r <= max then begin 
	    num := ! num +. 1.; sum := ! sum +. p; mean_aux tail end
	 else mean_aux tail
   in mean_aux l

let variance min max m l =
   let num = ref 0. in
   let sum = ref 0. in
   let rec variance_aux = function
      | []                -> ! sum /. ! num
      | (r, _, p) :: tail ->
         if r >= min && r <= max then begin 
	    num := ! num +. 1.; sum := ! sum +. (p -. m) *. (p -. m);
	    variance_aux tail end
	 else variance_aux tail
   in sqrt (variance_aux l)

let read_timing min max =
   let l = List.sort compare1 (get_timing ()) in
   let c = count min max l in
   let m = mean min max l in
   let v = variance min max m l in
   print_timing l;
   print_endline (string_of_int c ^ " " ^ string_of_float m ^ " " ^ 
                  string_of_float v);
   flush stdout

let diff_timing () =
   let rec diff_aux = function 
      | ((r1, q1, p1) :: t1, (r2, q2, p2) :: t2) when r1 = r2 ->
         (r1, q1 -. q2, p1 -. p2) :: diff_aux (t1, t2)
      | ([], []) -> print_newline (); []
      | (_ :: t1, _ :: t2) -> 
         print_string ("[" ^ string_of_int (1 + List.length t1) ^ "] ");
	 diff_aux (t1, t2)
      | _ -> assert false
   in
   let l1 = get_timing () in
   let l2 = get_timing () in
   print_string (string_of_int (List.length l1) ^ " ");
   print_string (string_of_int (List.length l2) ^ "\n");
   diff_aux (l1, l2)

let comp_timing min max =
   let l = List.sort compare1 (diff_timing ()) in
   let c = count min max l in
   let m = mean min max l in
   let v = variance min max m l in
   print_timing l;
   print_endline (string_of_int c ^ " " ^ string_of_float m ^ " " ^ 
                  string_of_float v);
   flush stdout

let print file =
   let rec print_aux () =
      let xobj = Xml.xnext() in
      if fst xobj = XML_Done then () else
      begin print_endline (string_of_xobject xobj); print_aux () end
   in Xml.start file false; print_aux (); Xml.stop ()

let count_bytes s =
   let mbytes = ref 0.0 in
   let num = ref 0 in
   let k = 1024.0 ** float (int_of_string s) in
   let rec count_bytes_aux () =
      try 
         let s = read_line () in
         (* prerr_endline ("*" ^ s ^ "*"); *)
         let j = String.rindex s ' ' in
         let i = 
	    try succ (String.rindex_from s (pred j) ' ') 
	    with Not_found -> 0 in
         (* prerr_endline ("*" ^ String.sub s i (j - i) ^ "*"); *)
         let b = int_of_string (String.sub s i (j - i)) in
         mbytes := ! mbytes +. float b /. k; incr num; 
         count_bytes_aux ()
      with End_of_file -> ()
   in
   count_bytes_aux ();
   prerr_endline (string_of_int ! num ^ " " ^ string_of_float ! mbytes)
*)

let _ = 
   let usage = "Usage: hxp [-lx <dir>] [-p <action>]" in

   let _l = "    set the path to the index.txt file (default is .)" in
   let _x = "    set the path to the RDF export directory (default is EXPORT)" in
   let _r = "    read the XML files extracting the specified information
         <action>: con-info   produce information about .con files in HTML format
                   html-names produce short names' list in HTML format
                   pg-names   produce short names' list in Postgres input format
		   rdf-names  produce RDF files with short names' metadata"
   in

   Arg.parse [
      ("-l", Arg.String (fun dir -> lib := dir), _l);
      ("-x", Arg.String (fun dir -> build := dir), _x);
      ("-r", Arg.String read_xml, _r)
   ] ignore usage

(*
let parse_args () =
   let rec parse = function
      | []                                  -> () 
      | ("-l"|"-library") :: dir :: rem     -> lib := dir; parse rem
      | ("-x"|"-export") :: dir :: rem      -> build := dir; parse rem
      | ("-s"|"-stat") :: min :: max :: rem ->
         read_timing (float_of_string min) (float_of_string max); parse rem
      | ("-c"|"-comp") :: min :: max :: rem -> 
         comp_timing (float_of_string min) (float_of_string max); parse rem
      | ("-i"|"-ins") :: s :: file :: rem   -> test s file false; parse rem 
      | ("-t"|"-text") :: s :: rem          -> read_xml s false; parse rem
      | ("-z"|"-gzip") :: s :: rem          -> read_xml s true; parse rem
      | ("-b"|"-bytes") :: s :: rem         -> count_bytes s; parse rem
      | _ :: rem                            -> parse rem
   in  
      parse (List.tl (Array.to_list Sys.argv))
*)