From: Ferruccio Guidi Date: Thu, 26 Feb 2004 17:05:53 +0000 (+0000) Subject: - MySQL mode added to the interpreter X-Git-Tag: v0_0_4~63 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e5ad471e2161436f4ff7ff56edce2947350d828;p=helm.git - MySQL mode added to the interpreter - hxp restored --- diff --git a/helm/gTopLevel/gTopLevel.conf.xml.sample b/helm/gTopLevel/gTopLevel.conf.xml.sample index 94fd2874a..1b3836c70 100644 --- a/helm/gTopLevel/gTopLevel.conf.xml.sample +++ b/helm/gTopLevel/gTopLevel.conf.xml.sample @@ -15,7 +15,9 @@ mathql_db_map.txt dbname=mowgli host=mowgli.cs.unibo.it user=helm password=awH21Un - + + + diff --git a/helm/hxp/EXAMPLE.txt b/helm/hxp/EXAMPLE.txt new file mode 100644 index 000000000..83e02a5cb --- /dev/null +++ b/helm/hxp/EXAMPLE.txt @@ -0,0 +1,5 @@ +On mowgli.cs.unibo.it this line outputs the names' list in a format suitable for +Postgres. Each line of this list contains a uri and its short name separated by +a tab character (as produced by pg_dump). see hxp --help for details. + +hxp.opt -l /projects/helm/EXPORT/examples_mowgli/objects -r pg-names diff --git a/helm/hxp/Makefile b/helm/hxp/Makefile new file mode 100644 index 000000000..4c41e6598 --- /dev/null +++ b/helm/hxp/Makefile @@ -0,0 +1,66 @@ +BIN_DIR = /usr/local/bin +REQUIRES = zip +# unix helm-cic_textual_parser \ +# helm-mathql helm-mathql_interpreter helm-mathql_generator +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep +OCAMLYACC = ocamlyacc +OCAMLLEX = ocamllex + +LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) + +HXPTOP = hxpTop.ml + +DEPOBJS = $(HXPTOP) +AUXOBJS = hxpTypes.ml hxpParser.ml hxpParser.mli hxpLexer.ml hxpXML.ml + +all: hxp +opt: hxp.opt + +depend: $(AUXOBJS) + $(OCAMLDEP) $(DEPOBJS) $(AUXOBJS) > .depend + +hxp: hxpParser.cmi $(AUXOBJS:.ml=.cmo) $(HXPTOP:.ml=.cmo) $(LIBRARIES) + $(OCAMLC) -linkpkg -o hxp $(AUXOBJS:.ml=.cmo) $(HXPTOP:.ml=.cmo) + +hxp.opt: $(AUXOBJS:.ml=.cmx) $(HXPTOP:.ml=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -linkpkg -o hxp.opt $(AUXOBJS:.ml=.cmx) $(HXPTOP:.ml=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx .mly .mll +.ml.cmo: $(LIBRARIES) + $(OCAMLC) -c $< +.mli.cmi: $(LIBRARIES) + $(OCAMLC) -c $< +.ml.cmx: $(LIBRARIES_OPT) + $(OCAMLOPT) -c $< +.mly.ml: + $(OCAMLYACC) $< +.mly.mli: + $(OCAMLYACC) $< +.mll.ml: + $(OCAMLLEX) $< + +$(DEPOBJS:%.ml=%.cmo): $(LIBRARIES) +$(DEPOBJS:%.ml=%.cmx): $(LIBRARIES_OPT) + +clean: + rm -f *.cm[iox] *.o hxp hxp.opt \ + hxpParser.ml hxpParser.mli hxpLexer.ml + +install: + cp hxp hxp.opt $(BIN_DIR) + +uninstall: + cd $(BIN_DIR) + rm -f hxp hxp.opt + +.PHONY: install uninstall clean + +ifneq ($(MAKECMDGOALS), depend) + include .depend +endif + diff --git a/helm/hxp/hxpLexer.mll b/helm/hxp/hxpLexer.mll new file mode 100644 index 000000000..fbec4aca7 --- /dev/null +++ b/helm/hxp/hxpLexer.mll @@ -0,0 +1,56 @@ +(* 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 + *) + +{ + open HxpParser +} + +let SPC = [' ' '\t' '\n' '\r' '?' '!']+ +let ALPHA = ['A'-'Z' 'a'-'z']+ +let STR = '"'[^'"']*'"' +let NUM = ['0'-'9' '.']+ +let BEF = [^ '=' '0'-'9' '.' ':' '*']* + +rule xml_token = parse + | SPC { xml_token lexbuf } + | '<' { OPEN } + | '>' { CLOSE } + | '=' { EQ } + | '/' { SL } + | ALPHA { NAME (Lexing.lexeme lexbuf) } + | STR { VAL (Lexing.lexeme lexbuf) } + | eof { DONE } + +and time_token = parse + | BEF { time_token lexbuf } + | NUM { DATA (float_of_string (Lexing.lexeme lexbuf)) } + | '=' { EQ } + | ':' { CLN } + | _ { DONE } + | eof { DONE } + diff --git a/helm/hxp/hxpParser.mly b/helm/hxp/hxpParser.mly new file mode 100644 index 000000000..aed627abf --- /dev/null +++ b/helm/hxp/hxpParser.mly @@ -0,0 +1,56 @@ +/* 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://cs.unibo.it/helm/. + */ + +/* AUTOR: Ferruccio Guidi + */ + +%{ + module T = HxpTypes +%} + %token DONE + %token NAME VAL + %token OPEN CLOSE EQ SL /* < > = / */ + %start xml + %type xml + + %token DATA + %token CLN + %start time + %type time +%% + xml : + OPEN NAME { T.XML_Open $2 } + | NAME EQ VAL { T.XML_Attribute ($1, $3) } + | CLOSE { T.XML_End } + | OPEN SL NAME CLOSE { T.XML_Close $3 } + | SL CLOSE { T.XML_Close "" } + | NAME NAME VAL { T.XML_Attribute ($1 ^ " " ^ $2, $3) } + | DONE { T.XML_Done } + ; + time : + EQ DATA CLN DATA { ($2, $4) } + | DATA EQ DATA CLN DATA { ($3, $5) } + | DONE { (-1., -1.) } + ; diff --git a/helm/hxp/hxpTop.ml b/helm/hxp/hxpTop.ml new file mode 100644 index 000000000..1030c6447 --- /dev/null +++ b/helm/hxp/hxpTop.ml @@ -0,0 +1,345 @@ +(* 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 + *) + +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) ^ + "

"); + 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 ()) ^ "\"

") + | 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 "\n\n"; + output_string och "\n"; + output_string och (" \n"); + output_string och (" " ^ n ^ "\n"); + output_string och " \n"; + output_string och "\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

] [-p ]" 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 + : 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)) +*) diff --git a/helm/hxp/hxpTypes.ml b/helm/hxp/hxpTypes.ml new file mode 100644 index 000000000..fb8cfeceb --- /dev/null +++ b/helm/hxp/hxpTypes.ml @@ -0,0 +1,57 @@ +(* 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 + *) + +type xml_object = + | XML_Open of string + | XML_Attribute of string * string + | XML_Close of string + | XML_End + | XML_Done + +type xml_xobject = xml_object * int + +type timing = float * float * float + +let string_of_object = function + | XML_Open t -> "OPEN " ^ t + | XML_Close t -> "CLOSE " ^ t + | XML_Attribute (n, v) -> "ATTRIBUTE " ^ n ^ "=" ^ v + | XML_End -> "END" + | XML_Done -> "" + +let string_of_xobject (o, i) = + string_of_object o ^ " [" ^ string_of_int i ^ "]" + +let string_of_timing (r, t, p) = + string_of_float r ^ "," ^ string_of_float t ^ "s, " ^ string_of_float p + +let rec print_timing = function + | [] -> () + | head :: tail -> + print_endline (string_of_timing head); flush stdout; + print_timing tail diff --git a/helm/hxp/hxpXML.ml b/helm/hxp/hxpXML.ml new file mode 100644 index 000000000..7c4dc4cb4 --- /dev/null +++ b/helm/hxp/hxpXML.ml @@ -0,0 +1,91 @@ +(* 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 + *) + +module T = HxpTypes + +module type Type = sig + + type handle + + val start : string -> bool -> handle + + val stop : handle -> unit + + val next : handle -> T.xml_object + + val xnext : handle -> handle * T.xml_xobject + + val scan_for : handle -> T.xml_xobject -> handle + +end + +module Make : Type = struct + + module L = HxpLexer + + module P = HxpParser + + type mode_t = Text of in_channel * Lexing.lexbuf + | GZip of Gzip.in_channel * Lexing.lexbuf + + type handle = {mode : mode_t; level : int} + + let start s filter = + let gread gch s n = Gzip.input gch s 0 n in + if filter then + let gch = Gzip.open_in (s ^ ".gz") in + let glb = Lexing.from_function (gread gch) in + {mode = GZip (gch, glb); level = 0} + else + let ch = open_in s in + let lb = Lexing.from_channel ch in + {mode = Text (ch, lb); level = 0} + + let stop = function + | {mode = GZip (gch, _)} -> Gzip.close_in gch + | {mode = Text (ch, _)} -> close_in ch + + let next h = + let lexbuf = match h.mode with + | GZip (_, glb) -> glb + | Text (_, lb) -> lb + in + P.xml L.xml_token lexbuf + + let xnext h = + let obj = next h in + match obj with + | T.XML_Open _ -> {h with level = succ h.level}, (obj, h.level) + | T.XML_Close _ -> {h with level = pred h.level}, (obj, pred h.level) + | _ -> h, (obj, h.level) + + let rec scan_for h xobj = + let h, curr_xobj = xnext h in + if curr_xobj = xobj then h else scan_for h xobj + +end diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index f6f655d28..2f842bb6b 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -5,7 +5,7 @@ REQUIRES = helm-urimanager helm-mathql mysql postgres PREDICATES = INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \ - mQIDataBase.mli mQIPostgres.mli mQIMySql.mli mQIMap.mli mQIConn.mli \ + mQIPostgres.mli mQIMySql.mli mQIMap.mli mQIConn.mli \ mQIProperty.mli mQueryInterpreter.mli IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \ diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index 4e27c9782..e138109b0 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -26,14 +26,18 @@ (* AUTOR: Ferruccio Guidi *) +type connection = MySQL_C of Mysql.dbd + | Postgres_C of Postgres.connection + | No_C + type flag = Galax | Postgres | Queries | Result | Source | Times | Warn type handle = { - log : string -> unit; (* logging function *) - set : flag list; (* options *) - pgc : MQIDataBase.connection option; (* PG connection *) - pgm : MQIMap.pg_map; (* PG conversion function *) - pga : MQIMap.pg_alias (* PG table aliases *) + log : string -> unit; (* logging function *) + set : flag list; (* options *) + pgc : connection; (* PG connection *) + pgm : MQIMap.pg_map; (* PG conversion function *) + pga : MQIMap.pg_alias (* PG table aliases *) } let tables handle p = MQIMap.get_tables handle.pgm p @@ -54,7 +58,7 @@ let string_of_flag = function | Galax -> "G" | Postgres -> "P" | Queries -> "Q" - | Result -> "R" + | Result -> "R" | Source -> "S" | Times -> "T" | Warn -> "W" @@ -94,21 +98,31 @@ let init ?(flags = []) ?(log = ignore) () = in g () in {log = log; set = flags; - pgc = - if List.mem Galax flags then - None - else - MQIDataBase.init - (Helm_registry.get "mathql_interpreter.postgresql_connection_string"); + pgc = begin + try + if List.mem Galax flags then No_C else + if List.mem Postgres flags then Postgres_C (MQIPostgres.init ()) else + MySQL_C (MQIMySql.init ()) + with Failure "mqi_connection" -> No_C + end; pgm = m; pga = a } let close handle = - if set handle Galax then () else MQIDataBase.close handle.pgc + match pgc handle with + | MySQL_C c -> MQIMySql.close c + | Postgres_C c -> MQIPostgres.close c + | No_C -> () + +let exec handle table cols ct cfl = + match pgc handle with + | MySQL_C c -> MQIMySql.exec c table cols ct cfl + | Postgres_C c -> MQIPostgres.exec c table cols ct cfl + | No_C -> [], "" let connected handle = - if set handle Galax then false else (pgc handle) <> None + pgc handle <> No_C let init_if_connected ?(flags = []) ?(log = ignore) () = let handle = init ~flags:flags ~log:log () in - ignore (pgc handle); handle + if connected handle then handle else raise (Failure "mqi connection failed") diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli index fba3d4263..5e37f180a 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ b/helm/ocaml/mathql_interpreter/mQIConn.mli @@ -36,6 +36,11 @@ type handle val init : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> handle val close : handle -> unit val connected : handle -> bool +val exec : handle -> + string -> string list -> + (bool * string * string list) list -> + (bool * string * string list) list list -> + string list list * string val init_if_connected : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> handle @@ -45,7 +50,6 @@ val init_if_connected : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> h val log : handle -> string -> unit val set : handle -> flag -> bool -val pgc : handle -> MQIDataBase.connection option val flags : handle -> flag list val tables : handle -> MathQL.path -> MQIMap.pg_tables val field : handle -> MathQL.path -> string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIDataBase.mli b/helm/ocaml/mathql_interpreter/mQIDataBase.mli deleted file mode 100644 index 8fa7acc3b..000000000 --- a/helm/ocaml/mathql_interpreter/mQIDataBase.mli +++ /dev/null @@ -1,37 +0,0 @@ -(* 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://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -type connection - -val init : string -> connection option - -val close : connection option -> unit - -val exec : connection option -> string -> string list list - -val quote : string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.ml b/helm/ocaml/mathql_interpreter/mQIMySql.ml index f5d30d1ed..af50af8ff 100644 --- a/helm/ocaml/mathql_interpreter/mQIMySql.ml +++ b/helm/ocaml/mathql_interpreter/mQIMySql.ml @@ -26,31 +26,13 @@ (* AUTOR: Ferruccio Guidi *) -type connection = Mysql.dbd +let init () = + try Mysql.quick_connect + ~host:"mowgli.cs.unibo.it" ~database:"mowgli" ~user:"helm" () + with _ -> raise (Failure "mqi_connecion") -let init connection_string = - try - Some - (Mysql.quick_connect - ~host:"mowgli.cs.unibo.it" ~database:"mowgli" ~user:"helm" ()) - with _ -> raise (Failure ("MQIPostgres.init: " ^ connection_string)) +let close c = Mysql.disconnect c -let close = function - | None -> () - | Some c -> Mysql.disconnect c - -let exec c q = match c with - | None -> [] - | Some c -> - Mysql.map - ~f:(function a -> - List.map - (function - None -> raise (Failure ("NULL found in a table")) - | Some v -> v - ) (Array.to_list a) - ) (Mysql.exec c q) - let quote s = let rec quote_aux s = try @@ -60,3 +42,43 @@ let quote s = with Not_found -> s in "'" ^ quote_aux s ^ "'" + +let exec c q = + let g = function None -> "" | Some v -> v in + let f a = List.map g (Array.to_list a) in + Mysql.map ~f:f (Mysql.exec c q), q + +let exec c table cols ct cfl = + let rec iter f sep = function + | [] -> "" + | [head] -> f head + | head :: tail -> f head ^ sep ^ iter f sep tail + in + let pg_cols = iter (fun x -> x) ", " cols in + let pg_msval v = iter quote ", " v in + let pg_con (pat, col, v) = + if col <> "" then + let f s = col ^ " regexp " ^ quote ("^" ^ s ^ "$") in + if pat then "(" ^ iter f " or " v ^ ")" + else match v with + | [s] -> "binary " ^ col ^ " = " ^ (quote s) + | v -> "binary " ^ col ^ " in (" ^ pg_msval v ^ ")" + else "1" + in + let pg_cons l = iter pg_con " and " l in + let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in + let pg_cons_not_l ll = iter pg_cons_not " and " ll in + let pg_where = match ct, cfl with + | [], [] -> "" + | lt, [] -> " where " ^ pg_cons lt + | [], llf -> " where " ^ pg_cons_not_l llf + | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf + in + if cols = [] then + let r, q = exec c ("select count (source) from " ^ table ^ pg_where) in + match r with + | [[s]] when int_of_string s > 0 -> [[]], q + | _ -> [], q + else + exec c ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ + " order by " ^ List.hd cols ^ " asc") diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.mli b/helm/ocaml/mathql_interpreter/mQIMySql.mli index 8fa7acc3b..3cbae4dc5 100644 --- a/helm/ocaml/mathql_interpreter/mQIMySql.mli +++ b/helm/ocaml/mathql_interpreter/mQIMySql.mli @@ -26,12 +26,13 @@ (* AUTOR: Ferruccio Guidi *) -type connection +val init : unit -> Mysql.dbd -val init : string -> connection option +val close : Mysql.dbd -> unit -val close : connection option -> unit +val exec : Mysql.dbd -> + string -> string list -> + (bool * string * string list) list -> + (bool * string * string list) list list -> + string list list * string -val exec : connection option -> string -> string list list - -val quote : string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml index 0e6d7c2cc..cf82814e9 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.ml +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.ml @@ -26,20 +26,15 @@ (* AUTOR: Ferruccio Guidi *) -type connection = Postgres.connection - -let init connection_string = - try Some (new Postgres.connection connection_string) - with _ -> raise (Failure ("MQIPostgres.init: " ^ connection_string)) +let init () = + let connection_string = + Helm_registry.get "mathql_interpreter.postgresql_connection_string" + in + try new Postgres.connection connection_string + with _ -> raise (Failure "mqi_connecion") -let close = function - | None -> () - | Some c -> c#close +let close c = c#close -let exec c q = match c with - | None -> [] - | Some c -> (c#exec q)#get_list - let quote s = let rec quote_aux s = try @@ -49,3 +44,51 @@ let quote s = with Not_found -> s in "'" ^ quote_aux s ^ "'" + +let exec c q = (c#exec q)#get_list, q + +let exec c table cols ct cfl = + let rec iter f sep = function + | [] -> "" + | [head] -> f head + | head :: tail -> f head ^ sep ^ iter f sep tail + in + let pg_cols = iter (fun x -> x) ", " cols in + let pg_msval v = iter quote ", " v in + let pg_con (pat, col, v) = + if col <> "" then + let f s = col ^ " ~ " ^ quote ("^" ^ s ^ "$") in + if pat then "(" ^ iter f " or " v ^ ")" + else match v with + | [s] -> col ^ " = " ^ (quote s) + | v -> col ^ " in (" ^ pg_msval v ^ ")" + else "true" + in + let pg_cons l = iter pg_con " and " l in + let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in + let pg_cons_not_l ll = iter pg_cons_not " and " ll in + let pg_where = match ct, cfl with + | [], [] -> "" + | lt, [] -> " where " ^ pg_cons lt + | [], llf -> " where " ^ pg_cons_not_l llf + | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf + in + if cols = [] then + let r, q = exec c ("select count (source) from " ^ table ^ pg_where) in + match r with + | [[s]] when int_of_string s > 0 -> [[]], q + | _ -> [], q + else + exec c ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ + " order by " ^ List.hd cols ^ " asc") + +(* funzioni vecchie ********************************************************) +(* +let pg_name h s = + let q = "select id from registry where uri = " ^ quote s in + match exec h q with + | [[id]] -> "t" ^ id + | _ -> "" + +let get_id b = if b then ["B"] else ["F"] +*) diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.mli b/helm/ocaml/mathql_interpreter/mQIPostgres.mli index 8fa7acc3b..63752dfeb 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.mli +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.mli @@ -26,12 +26,17 @@ (* AUTOR: Ferruccio Guidi *) -type connection +val init : unit -> Postgres.connection + +val close : Postgres.connection -> unit + +val exec : Postgres.connection -> + string -> string list -> + (bool * string * string list) list -> + (bool * string * string list) list list -> + string list list * string + -val init : string -> connection option -val close : connection option -> unit -val exec : connection option -> string -> string list list -val quote : string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index 0433afd5e..fa966a06c 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -27,7 +27,6 @@ *) module M = MathQL -module P = MQIDataBase module C = MQIConn module U = MQIUtil module A = MQIMap @@ -53,51 +52,6 @@ let cl_print l = in List.iter c_print l -(* PostgreSQL backend ******************************************************) - -let pg_query h table cols ct cfl = - let exec q = - if C.set h C.Queries then C.log h (q ^ "\n"); - P.exec (C.pgc h) q - in - let rec iter f sep = function - | [] -> "" - | [head] -> f head - | head :: tail -> f head ^ sep ^ iter f sep tail - in - let pg_cols = iter (fun x -> x) ", " cols in - let pg_msval v = iter P.quote ", " v in - let pg_con (pat, col, v) = - if col <> "" then - let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in - if pat then "(" ^ iter f " or " v ^ ")" - else match v with - | [s] -> col ^ " = " ^ (P.quote s) - | v -> col ^ " in (" ^ pg_msval v ^ ")" - else "true" - in - let pg_cons l = iter pg_con " and " l in - let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in - let pg_cons_not_l ll = iter pg_cons_not " and " ll in - let pg_where = match ct, cfl with - | [], [] -> "" - | lt, [] -> " where " ^ pg_cons lt - | [], llf -> " where " ^ pg_cons_not_l llf - | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf - in - if cols = [] then - let r = exec ("select count (source) from " ^ table ^ pg_where) in - match r with - | [[s]] when int_of_string s > 0 -> [[]] - | _ -> [] - else - exec ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ - " order by " ^ List.hd cols ^ " asc") - -(* Galax backend ***********************************************************) - -let gx_query h table cols ct cfl = not_supported "Galax" - (* Common functions ********************************************************) let pg_result distinct subj el res = @@ -129,8 +83,8 @@ let exec_single h mc ct cfl el table = let cons_false = List.map mk_con cfl in let other_cols = List.map (fun (p, _) -> conv p) el in let cols = if first = "" then other_cols else first :: other_cols in - let low_level = if C.set h C.Galax then gx_query else pg_query in - let result = low_level h (C.resolve h table) cols cons_true cons_false in + let result, q = C.exec h (C.resolve h table) cols cons_true cons_false in + if C.set h C.Queries then C.log h (q ^ "\n"); pg_result false first el result let deadline = 100 @@ -145,13 +99,3 @@ let exec h refine mc ct cfl el = | _ -> exec_single h mc ct cfl el table in exec_aux ct - -(* funzioni vecchie ********************************************************) - -let pg_name h s = - let q = "select id from registry where uri = " ^ P.quote s in - match P.exec h q with - | [[id]] -> "t" ^ id - | _ -> "" - -let get_id b = if b then ["B"] else ["F"]