From: Ferruccio Guidi Date: Wed, 23 Apr 2003 11:05:32 +0000 (+0000) Subject: - New interface for the MathQL interpreter (1.3 version) X-Git-Tag: before_refactoring~9 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03dee221bd1f2c9a6e7f74d9abf88be14aac7763;p=helm.git - New interface for the MathQL interpreter (1.3 version) - Two toplevels committed in ocaml/mathql_test (new directory) --- diff --git a/helm/Makefile b/helm/Makefile index a7fa0f905..fb0fac994 100644 --- a/helm/Makefile +++ b/helm/Makefile @@ -1,4 +1,4 @@ -DIRS = ocaml hbugs gTopLevel +DIRS = ocaml hbugs gTopLevel searchEngine DIRS_BYTE = $(patsubst %,%.byte,$(DIRS)) DIRS_OPT = $(patsubst %,%.opt,$(DIRS)) diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index 0893c195f..4790ab88a 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -4,6 +4,13 @@ open Printf;; exception Empty_must;; +module MQICallbacks = + struct + let log s = prerr_string s + end + +module MQI = MQueryInterpreter.Make(MQICallbacks) + let broker_id = ref None let my_own_id = Hbugs_tutors_common.init_tutor () let my_own_addr, my_own_port = "127.0.0.1", 50011 @@ -103,25 +110,18 @@ let callback (req: Http_types.request) outchan = (Exception ("parse_error", reason))) outchan -let postgresqlconnectionstring = - try - Sys.getenv "POSTGRESQL_CONNECTION_STRING" - with - Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" -;; - let main () = + let mqi_options = "" in (* default MathQL interpreter options *) try Sys.catch_break true; at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id); broker_id := Some (Hbugs_tutors_common.register_to_broker my_own_id my_own_url "FOO" "Search_pattern_apply tutor"); - Mqint.set_database Mqint.postgres_db ; - Mqint.init postgresqlconnectionstring ; + ignore (MQI.init mqi_options) ; Http_daemon.start' ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback; - Mqint.close () + MQI.close mqi_options with Sys.Break -> () (* exit nicely, invoking at_exit functions *) ;; diff --git a/helm/ocaml/META.helm-mathql_test.src b/helm/ocaml/META.helm-mathql_test.src new file mode 100644 index 000000000..e69de29bb diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index e41e3bbc2..a700bb5ac 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -1,5 +1,5 @@ PACKAGE = mathql -REQUIRES = helm-urimanager helm-cic helm-cic_textual_parser +REQUIRES = helm-urimanager helm-cic helm-cic_textual_parser PREDICATES = INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli mQueryMisc.mli diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml index bb5bb74ae..928050679 100644 --- a/helm/ocaml/mathql/mQueryMisc.ml +++ b/helm/ocaml/mathql/mQueryMisc.ml @@ -100,3 +100,14 @@ let term_of_cic_textual_parser_uri uri = | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) ;; +(* time handling ***********************************************************) + +type time = float * float + +let start_time () = + (Sys.time (), Unix.time ()) + +let stop_time (s0, u0) = + let s1 = Sys.time () in + let u1 = Unix.time () in + Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) diff --git a/helm/ocaml/mathql/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli index d775e989d..2605fe286 100644 --- a/helm/ocaml/mathql/mQueryMisc.mli +++ b/helm/ocaml/mathql/mQueryMisc.mli @@ -40,3 +40,6 @@ val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string +type time +val start_time : unit -> time +val stop_time : time -> string diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index ecb037346..42a0b04df 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -20,7 +20,9 @@ property.cmo: dbconn.cmi intersect.cmi utility.cmi property.cmi property.cmx: dbconn.cmx intersect.cmx utility.cmx property.cmi pattern.cmo: dbconn.cmi utility.cmi pattern.cmi pattern.cmx: dbconn.cmx utility.cmx pattern.cmi -mqint.cmo: context.cmo dbconn.cmi diff.cmi func.cmi intersect.cmi meet.cmi \ - pattern.cmi property.cmi relation.cmi sub.cmi union.cmi mqint.cmi -mqint.cmx: context.cmx dbconn.cmx diff.cmx func.cmx intersect.cmx meet.cmx \ - pattern.cmx property.cmx relation.cmx sub.cmx union.cmx mqint.cmi +mQueryInterpreter.cmo: context.cmo dbconn.cmi diff.cmi func.cmi intersect.cmi \ + meet.cmi pattern.cmi property.cmi relation.cmi sub.cmi union.cmi \ + mQueryInterpreter.cmi +mQueryInterpreter.cmx: context.cmx dbconn.cmx diff.cmx func.cmx intersect.cmx \ + meet.cmx pattern.cmx property.cmx relation.cmx sub.cmx union.cmx \ + mQueryInterpreter.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index 4bd667625..8efbe582f 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -1,10 +1,10 @@ PACKAGE = mathql_interpreter -REQUIRES = helm-urimanager postgres unix natile-galax helm-mathql +REQUIRES = helm-urimanager postgres natile-galax helm-mathql PREDICATES = -INTERFACE_FILES = dbconn.mli utility.mli union.mli relation.mli diff.mli meet.mli sub.mli intersect.mli func.mli property.mli pattern.mli mqint.mli +INTERFACE_FILES = dbconn.mli utility.mli union.mli relation.mli diff.mli meet.mli sub.mli intersect.mli func.mli property.mli pattern.mli mQueryInterpreter.mli -IMPLEMENTATION_FILES = dbconn.ml utility.ml union.ml relation.ml diff.ml meet.ml sub.ml intersect.ml context.ml func.ml property.ml pattern.ml mqint.ml +IMPLEMENTATION_FILES = dbconn.ml utility.ml union.ml relation.ml diff.ml meet.ml sub.ml intersect.ml context.ml func.ml property.ml pattern.ml mQueryInterpreter.ml # $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml new file mode 100644 index 000000000..f320ebba6 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -0,0 +1,264 @@ +(* 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/. + *) + +open Dbconn;; +open Union;; +open Intersect;; +open Meet;; +open Property;; +open Sub;; +open Context;; +open Diff;; +open Relation;; +open Func;; +open Pattern;; + +exception SVarUnbound of string;; +exception RVarUnbound of string;; +exception VVarUnbound of string;; +exception PathUnbound of (string * string list);; + +exception InvalidConnection +exception ConnectionFailed of string + +exception BooleExpTrue + +(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *) + +let galax_char = 'G' +let stat_char = 'S' + +let execute_aux log m x = + let module M = MathQL in + let module X = MQueryMisc in +let rec exec_set_exp c = function + M.SVar svar -> + (try + List.assoc svar c.svars + with Not_found -> + raise (SVarUnbound svar)) + | M.RVar rvar -> + (try + [List.assoc rvar c.rvars] + with Not_found -> + raise (RVarUnbound rvar)) + | M.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp) + | M.Pattern vexp -> pattern_ex (exec_val_exp c vexp) + | M.Intersect (sexp1, sexp2) -> + let before = X.start_time() in + let rs1 = exec_set_exp c sexp1 in + let rs2 = exec_set_exp c sexp2 in + let res = intersect_ex rs1 rs2 in + let diff = X.stop_time before in + let ll1 = string_of_int (List.length rs1) in + let ll2 = string_of_int (List.length rs2) in + if String.contains m stat_char then + log ("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ + ": " ^ diff ^ "\n"); + res + | M.Union (sexp1, sexp2) -> + let before = X.start_time () in + let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in + let diff = X.stop_time before in + if String.contains m stat_char then log ("UNION: " ^ diff ^ "\n"); + res + | M.LetSVar (svar, sexp1, sexp2) -> + let before = X.start_time() in + let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in + let res = exec_set_exp c1 sexp2 in + if String.contains m stat_char then begin + log ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": "); + log (X.stop_time before ^ "\n"); + end; + res + | M.LetVVar (vvar, vexp, sexp) -> + let before = X.start_time() in + let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in + let res = exec_set_exp c1 sexp in + if String.contains m stat_char then begin + log ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": "); + log (X.stop_time before ^ "\n"); + end; + res + | M.Relation (inv, rop, path, sexp, assl) -> + let before = X.start_time() in + if String.contains m galax_char then begin + let res = relation_galax_ex inv rop path (exec_set_exp c sexp) assl in + if String.contains m stat_char then begin + log ("RELATION-GALAX " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); + log (X.stop_time before ^ "\n") + end; + res + end else begin + let res = relation_ex inv rop path (exec_set_exp c sexp) assl in + if String.contains m stat_char then begin + log ("RELATION " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); + log (X.stop_time before ^ "\n") + end; + res + end + | M.Select (rvar, sexp, bexp) -> + let before = X.start_time() in + let rset = (exec_set_exp c sexp) in + let rec select_ex = + function + [] -> [] + | r::tl -> + let c1 = upd_rvars c ((rvar,r)::c.rvars) in + if (exec_boole_exp c1 bexp) then + r::(select_ex tl) + else + select_ex tl + in + let res = select_ex rset in + if String.contains m stat_char then begin + log ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": "); + log (X.stop_time before ^ "\n"); + end; + res + | M.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) + +(* valuta una MathQL.boole_exp e ritorna un boole *) + +and exec_boole_exp c = + function + M.False -> false + | M.True -> true + | M.Not x -> not (exec_boole_exp c x) + | M.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y) + | M.Or (x, y) -> (exec_boole_exp c x) || (exec_boole_exp c y) + | M.Sub (vexp1, vexp2) -> + sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) + | M.Meet (vexp1, vexp2) -> + meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) + | M.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2) + | M.Ex l bexp -> + if l = [] then + (exec_boole_exp c bexp) + else + let latt = + List.map + (fun uri -> + let (r,attl) = + (try + List.assoc uri c.rvars + with Not_found -> assert false) + in + (uri,attl) + ) l (*latt = l + attributi*) + in + try + let rec prod c = + function + [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue + | (uri,attl)::tail1 -> + (*per ogni el. di attl devo andare in ric. su tail1*) + let rec sub_prod attl = + match attl with + [] -> () + | att::tail2 -> + let c1 = upd_groups c ((uri,att)::c.groups) in + prod c1 tail1; sub_prod tail2 + in + sub_prod attl + in + prod c latt; + false + with BooleExpTrue -> true + +(* valuta una MathQL.val_exp e ritorna un MathQL.value *) + +and exec_val_exp c = function + M.Const x -> let + ol = List.sort compare x in + let rec edup = function + + [] -> [] + | s::tl -> if tl <> [] then + if s = (List.hd tl) then edup tl + else s::(edup tl) + else s::[] + in + edup ol + | M.Record (rvar, path) -> + (try + List.assoc path + (try + List.assoc rvar c.groups + with Not_found -> + raise (RVarUnbound rvar)) + with Not_found -> + raise (PathUnbound path)) + | M.VVar s -> + (try + List.assoc s c.vvars + with Not_found -> + raise (VVarUnbound s)) + | M.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp) + | M.Fun (s, vexp) -> fun_ex s (exec_val_exp c vexp) + | M.Property (inv, rop, path, vexp) -> property_ex rop path inv (exec_val_exp c vexp) + +(* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *) +in + exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x + +(* new interface ***********************************************************) + +module type Callbacks = + sig + val log : string -> unit (* logging function *) + end + +module Make (C: Callbacks) = + struct + + let postgres = "P" + let galax = "G" + let stat = "S" + let quiet = "Q" + let warn = "W" + + let execute m x = execute_aux C.log m x + + let init m = + let default_connection_string = + "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" + in + let connection_string = + try Sys.getenv "POSTGRESQL_CONNECTION_STRING" + with Not_found -> default_connection_string + in + if String.contains m galax_char then true else + try Dbconn.init connection_string; true + with ConnectionFailed s -> false + + let close m = + if String.contains m galax_char then () else Dbconn.close () + + let check m = + if String.contains m galax_char then false else + try ignore (Dbconn.pgc ()); true with InvalidConnection -> false + + end diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli b/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli new file mode 100644 index 000000000..4400c45dd --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli @@ -0,0 +1,53 @@ +(* 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 06/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +module type Callbacks = + sig + val log : string -> unit (* logging function *) + end + +module Make (C: Callbacks) : + sig + val postgres : string + val galax : string + val stat : string + val quiet : string + val warn : string + + val execute : string -> MathQL.query -> MathQL.result + val init : string -> bool + val close : string -> unit + val check : string -> bool + end diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml deleted file mode 100644 index 5755aa3a6..000000000 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ /dev/null @@ -1,259 +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/. - *) - - - - -(* - * implementazione del'interprete MathQL - *) - - - - -open Dbconn;; -open Union;; -open Intersect;; -open Meet;; -open Property;; -open Sub;; -open Context;; -open Diff;; -open Relation;; -open Func;; -open Pattern;; - -exception SVarUnbound of string;; -exception RVarUnbound of string;; -exception VVarUnbound of string;; -exception PathUnbound of (string * string list);; - -exception BooleExpTrue - -let init connection_param = Dbconn.init connection_param - -let close () = Dbconn.close () - -let check () = - let status = Dbconn.pgc () - in () - -let stat = ref true - -let set_stat b = stat := b - -let get_stat () = ! stat - -let postgres_db = "postgres" - -let galax_db = "galax" - -let dbname = ref galax_db - -let set_database s = - if s = postgres_db || s = galax_db then dbname := s - else raise (Invalid_argument s) - -let get_database () = ! dbname - -(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *) - -let rec exec_set_exp c = function - MathQL.SVar svar -> - (try - List.assoc svar c.svars - with Not_found -> - raise (SVarUnbound svar)) - | MathQL.RVar rvar -> - (try - [List.assoc rvar c.rvars] - with Not_found -> - raise (RVarUnbound rvar)) - | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp) - | MathQL.Pattern vexp -> pattern_ex (exec_val_exp c vexp) - | MathQL.Intersect (sexp1, sexp2) -> - let before = Sys.time() in - let rs1 = exec_set_exp c sexp1 in - let rs2 = exec_set_exp c sexp2 in - let res = intersect_ex rs1 rs2 in - let after = Sys.time() in - let ll1 = string_of_int (List.length rs1) in - let ll2 = string_of_int (List.length rs2) in - let diff = string_of_float (after -. before) in - if !stat then - (prerr_endline("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ - ": " ^ diff ^ "s"); - flush stdout); - res - | MathQL.Union (sexp1, sexp2) -> - let before = Sys.time () in - let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in - let after = Sys.time() in - let diff = string_of_float (after -. before) in - if !stat then - (prerr_endline ("UNION: " ^ diff ^ "s"); - flush stdout); - res - | MathQL.LetSVar (svar, sexp1, sexp2) -> - let before = Sys.time() in - let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in - let res = exec_set_exp c1 sexp2 in - if ! stat then - (prerr_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": "); - prerr_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.LetVVar (vvar, vexp, sexp) -> - let before = Sys.time() in - let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in - let res = exec_set_exp c1 sexp in - if ! stat then - (prerr_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": "); - prerr_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.Relation (inv, rop, path, sexp, assl) -> - let before = Sys.time() in - if ! dbname = postgres_db then - (let res = relation_ex inv rop path (exec_set_exp c sexp) assl in - if ! stat then - (prerr_string ("RELATION " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); - prerr_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res) - - else - (let res = relation_galax_ex inv rop path (exec_set_exp c sexp) assl in - if !stat then - (prerr_string ("RELATION-GALAX " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); - prerr_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res) - - - | MathQL.Select (rvar, sexp, bexp) -> - let before = Sys.time() in - let rset = (exec_set_exp c sexp) in - let rec select_ex = - function - [] -> [] - | r::tl -> - let c1 = upd_rvars c ((rvar,r)::c.rvars) in - if (exec_boole_exp c1 bexp) then - r::(select_ex tl) - else - select_ex tl - in - let res = select_ex rset in - if ! stat then - (prerr_string ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": "); - prerr_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) - -(* valuta una MathQL.boole_exp e ritorna un boole *) - -and exec_boole_exp c = - function - MathQL.False -> false - | MathQL.True -> true - | MathQL.Not x -> not (exec_boole_exp c x) - | MathQL.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y) - | MathQL.Or (x, y) -> (exec_boole_exp c x) || (exec_boole_exp c y) - | MathQL.Sub (vexp1, vexp2) -> - sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) - | MathQL.Meet (vexp1, vexp2) -> - meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) - | MathQL.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2) - | MathQL.Ex l bexp -> - if l = [] then - (exec_boole_exp c bexp) - else - let latt = - List.map - (fun uri -> - let (r,attl) = - (try - List.assoc uri c.rvars - with Not_found -> assert false) - in - (uri,attl) - ) l (*latt = l + attributi*) - in - try - let rec prod c = - function - [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue - | (uri,attl)::tail1 -> - (*per ogni el. di attl devo andare in ric. su tail1*) - let rec sub_prod attl = - match attl with - [] -> () - | att::tail2 -> - let c1 = upd_groups c ((uri,att)::c.groups) in - prod c1 tail1; sub_prod tail2 - in - sub_prod attl - in - prod c latt; - false - with BooleExpTrue -> true - -(* valuta una MathQL.val_exp e ritorna un MathQL.value *) - -and exec_val_exp c = function - MathQL.Const x -> let - ol = List.sort compare x in - let rec edup = function - - [] -> [] - | s::tl -> if tl <> [] then - if s = (List.hd tl) then edup tl - else s::(edup tl) - else s::[] - in - edup ol - | MathQL.Record (rvar, path) -> - (try - List.assoc path - (try - List.assoc rvar c.groups - with Not_found -> - raise (RVarUnbound rvar)) - with Not_found -> - raise (PathUnbound path)) - | MathQL.VVar s -> - (try - List.assoc s c.vvars - with Not_found -> - raise (VVarUnbound s)) - | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp) - | MathQL.Fun (s, vexp) -> fun_ex s (exec_val_exp c vexp) - | MathQL.Property (inv, rop, path, vexp) -> property_ex rop path inv (exec_val_exp c vexp) - -(* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *) -and execute x = - exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x diff --git a/helm/ocaml/mathql_interpreter/mqint.mli b/helm/ocaml/mathql_interpreter/mqint.mli deleted file mode 100644 index 414515308..000000000 --- a/helm/ocaml/mathql_interpreter/mqint.mli +++ /dev/null @@ -1,46 +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/. - *) - -val init : string -> unit (* open database *) - -val execute : MathQL.query -> MathQL.result (* execute query *) - -val close : unit -> unit (* close database *) - -val check : unit -> unit (* check connection *) - -val set_stat : bool -> unit (* set stat emission *) - -val get_stat : unit -> bool (* check stat emission *) - -val postgres_db : string (* postgres *) - -val galax_db : string (* galax *) - -val set_database : string -> unit (* switch postgres/galax *) - -val get_database : unit -> string (* check db used *) - - diff --git a/helm/ocaml/mathql_test/.cvsignore b/helm/ocaml/mathql_test/.cvsignore new file mode 100644 index 000000000..fa6e35041 --- /dev/null +++ b/helm/ocaml/mathql_test/.cvsignore @@ -0,0 +1 @@ +*.cm[aiox] *.cmxa *.opt mqtop mqitop diff --git a/helm/ocaml/mathql_test/.depend b/helm/ocaml/mathql_test/.depend new file mode 100644 index 000000000..e69de29bb diff --git a/helm/ocaml/mathql_test/Makefile b/helm/ocaml/mathql_test/Makefile new file mode 100644 index 000000000..f6f41aaa4 --- /dev/null +++ b/helm/ocaml/mathql_test/Makefile @@ -0,0 +1,61 @@ +BIN_DIR = /usr/local/bin +REQUIRES = unix helm-cic helm-cic_textual_parser helm-mathql helm-mathql_interpreter +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +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)) + +MQTOP = mqtop.ml +MQITOP = mqitop.ml + +DEPOBJS = $(MQTOP) $(MQITOP) + +all: $(DEPOBJS:.ml=) +opt: $(DEPOBJS:.ml=.opt) + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +mqtop: $(MQTOP:.ml=.cmo) $(LIBRARIES) + $(OCAMLC) -linkpkg -o mqtop $(MQTOP:.ml=.cmo) + +mqtop.opt: $(MQTOP:.ml=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -linkpkg -o mqtop.opt $(MQTOP:.ml=.cmx) + +mqitop: $(MQITOP:.ml=.cmo) $(LIBRARIES) + $(OCAMLC) -linkpkg -o mqitop $(MQITOP:.ml=.cmo) + +mqitop.opt: $(MQITOP:.ml=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -linkpkg -o mqitop.opt $(MQITOP:.ml=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: $(LIBRARIES) + $(OCAMLC) -c $< +.mli.cmi: $(LIBRARIES) + $(OCAMLC) -c $< +.ml.cmx: $(LIBRARIES_OPT) + $(OCAMLOPT) -c $< + +$(DEPOBJS:%.ml=%.cmo): $(LIBRARIES) +$(DEPOBJS:%.ml=%.cmx): $(LIBRARIES_OPT) + +clean: + rm -f *.cm[iox] *.o $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) + +install: + cp $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) $(BIN_DIR) + +uninstall: + cd $(BIN_DIR) + rm -f $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) + +.PHONY: install uninstall clean + +ifneq ($(MAKECMDGOALS), depend) + include .depend +endif + diff --git a/helm/ocaml/mathql_test/mqitop.ml b/helm/ocaml/mathql_test/mqitop.ml new file mode 100644 index 000000000..fc206c68d --- /dev/null +++ b/helm/ocaml/mathql_test/mqitop.ml @@ -0,0 +1,25 @@ +module MQICallbacks = + struct + let log s = print_string s; flush stdout + end + +let _ = + let module U = MQueryUtil in + let module X = MQueryMisc in + let module I = MQueryInterpreter.Make(MQICallbacks) in + let t = X.start_time () in + let ich = Lexing.from_channel stdin in + let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in + let rec aux () = + let t = X.start_time () in + let r = I.execute flags (U.query_of_text ich) in + Printf.printf "mqitop: query: %s,%i\n" (X.stop_time t) (List.length r); + flush stdout; aux() + + in + if not (I.init flags) then begin + print_endline "mqitop: no connection"; flush stdout + end; + begin try aux() with End_of_file -> () end; + I.close flags; + Printf.printf "mqitop: done: %s\n" (X.stop_time t) diff --git a/helm/ocaml/mathql_test/mqtop.ml b/helm/ocaml/mathql_test/mqtop.ml new file mode 100644 index 000000000..d601d65f9 --- /dev/null +++ b/helm/ocaml/mathql_test/mqtop.ml @@ -0,0 +1,13 @@ +let _ = + let module U = MQueryUtil in + let module X = MQueryMisc in + let t = X.start_time () in + let ich = Lexing.from_channel stdin in + let rec aux () = + let t = X.start_time () in + U.text_of_query print_string (U.query_of_text ich) "\n"; + Printf.printf "mqtop: query: %s\n" (X.stop_time t); + flush stdout; aux() + in + begin try aux() with End_of_file -> () end; + Printf.printf "mqtop: done: %s\n" (X.stop_time t)