+++ /dev/null
-(* 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))
-*)
projects / helm.git / blobdiff