From: Ferruccio Guidi Date: Wed, 1 Oct 2003 14:53:04 +0000 (+0000) Subject: first version X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5bef9ac5a9bfe07b11ce0e44fab51ea4b6eb4057 first version --- diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend index 30dbaa280..8acbe7bca 100644 --- a/helm/ocaml/mathql/.depend +++ b/helm/ocaml/mathql/.depend @@ -1,2 +1,4 @@ mQueryMisc.cmo: mQueryMisc.cmi mQueryMisc.cmx: mQueryMisc.cmi +mQueryUtil.cmo: mQueryUtil.cmi +mQueryUtil.cmx: mQueryUtil.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index 6554bf698..f3030e882 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -2,9 +2,9 @@ PACKAGE = mathql REQUIRES = helm-cic helm-cic_textual_parser PREDICATES = -INTERFACE_FILES = mQueryMisc.mli +INTERFACE_FILES = mQueryMisc.mli mQueryUtil.mli -IMPLEMENTATION_FILES = mathQL.ml mQueryMisc.ml +IMPLEMENTATION_FILES = mQueryMisc.ml mathQL.ml mQueryUtil.ml EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml new file mode 100644 index 000000000..22d1f91e5 --- /dev/null +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -0,0 +1,79 @@ +(* 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 + *) + +(* 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) + +(* operations on lists *****************************************************) + +type 'a comparison = Lt + | Gt + | Eq of 'a + +let list_join f l1 l2 = + let rec aux = function + | [], v + | v, [] -> v + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> h1 :: aux (t1, v2) + | Gt -> h2 :: aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) + +let list_meet f l1 l2 = + let rec aux = function + | [], v + | v, [] -> [] + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> aux (t1, v2) + | Gt -> aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) + +let rec flat_list out f s = function + | [] -> () + | [a] -> f a + | a :: tail -> f a; out s; flat_list out f s tail + +let rec add_assoc ap = function + | [] -> [ap] + | head :: tail when fst head = fst ap -> ap :: tail + | head :: tail -> head :: add_assoc ap tail diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli new file mode 100644 index 000000000..fbfb3f793 --- /dev/null +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -0,0 +1,45 @@ +(* 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 time + +val start_time : unit -> time + +val stop_time : time -> string + +type 'a comparison = Lt + | Gt + | Eq of 'a + +val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list + +val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list + +val flat_list : ('a -> unit) -> ('b -> unit) -> 'a -> 'b list -> unit + +val add_assoc : 'a * 'b -> ('a * 'b) list -> ('a * 'b) list diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 7e82fe547..9c19f4a50 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -51,8 +51,6 @@ type svar = string (* the name of a variable for a resource set *) type avar = string (* the name of a variable for a resource *) -type vvar = string (* the name of a variable for an attribute value *) - type inverse = bool type refine = RefineExact @@ -73,58 +71,27 @@ type xml = bool type source = bool -type bin = BinFJoin (* full union - with attr handling *) - | BinFMeet (* full intersection - with attr handling *) - | BinFDiff (* full difference - with attr handling *) - type gen = GenFJoin (* full union - with attr handling *) | GenFMeet (* full intersection - with attr handling *) -type test = Xor - | Or - | And - | Sub - | Meet - | Eq - | Le - | Lt - -type query = Empty - | SVar of svar +type query = Const of result + | SVar of svar | AVar of avar - | Subj of msval + | Dot of avar * path + | Ex of avar list * query + | Select of avar * query * query + | Let of svar * query * query + | Fun of path * path list * query list + | Add of bool * groups * query + | For of gen * avar * query * query | Property of inverse * refine * path * main * istrue * isfalse list * exp_list * - pattern * msval - | Select of avar * query * msval - | Bin of bin * query * query - | LetSVar of svar * query * query - | LetVVar of vvar * msval * query - | For of gen * avar * query * query - | Add of bool * groups * query - | If of msval * query * query - | Log of xml * source * query - | StatQuery of query - | Keep of allbut * path list * query - -and msval = False - | True - | Not of msval - | Ex of avar list * msval - | Test of test * msval * msval - | Const of string - | Set of msval list - | Proj of path option * query - | Dot of avar * path - | VVar of vvar - | StatVal of msval - | Count of msval - | Align of string * msval - -and groups = Attr of (path * msval) list list + pattern * query + +and groups = Attr of (path * query) list list | From of avar -and con = pattern * path * msval +and con = pattern * path * query and istrue = con list diff --git a/helm/ocaml/mathql_interpreter/.cvsignore b/helm/ocaml/mathql_interpreter/.cvsignore index cd9b591e3..55b492aab 100644 --- a/helm/ocaml/mathql_interpreter/.cvsignore +++ b/helm/ocaml/mathql_interpreter/.cvsignore @@ -1 +1 @@ -*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli +*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli *.output diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 7d9b3c625..fa6401505 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,25 +1,28 @@ mQIConn.cmi: mQIMap.cmi +mQILib.cmi: mQIConn.cmi mQIProperty.cmi: mQIConn.cmi mQueryInterpreter.cmi: mQIConn.cmi -mQueryTParser.cmo: mQueryTParser.cmi -mQueryTParser.cmx: mQueryTParser.cmi -mQueryTLexer.cmo: mQueryTParser.cmi -mQueryTLexer.cmx: mQueryTParser.cmx -mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mQueryUtil.cmi -mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mQueryUtil.cmi -mQIUtil.cmo: mQIUtil.cmi -mQIUtil.cmx: mQIUtil.cmi mQIPostgres.cmo: mQIPostgres.cmi mQIPostgres.cmx: mQIPostgres.cmi -mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi -mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi +mQIMap.cmo: mQIMap.cmi +mQIMap.cmx: mQIMap.cmi mQIConn.cmo: mQIMap.cmi mQIPostgres.cmi mQIConn.cmi mQIConn.cmx: mQIMap.cmx mQIPostgres.cmx mQIConn.cmi +mQIUtil.cmo: mQIUtil.cmi +mQIUtil.cmx: mQIUtil.cmi +mQILib.cmo: mQIConn.cmi mQIUtil.cmi mQILib.cmi +mQILib.cmx: mQIConn.cmx mQIUtil.cmx mQILib.cmi mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIUtil.cmi \ mQIProperty.cmi mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIUtil.cmx \ mQIProperty.cmi -mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi mQueryUtil.cmi \ - mQueryInterpreter.cmi -mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx mQueryUtil.cmx \ - mQueryInterpreter.cmi +mQueryTParser.cmo: mQILib.cmi +mQueryTParser.cmx: mQILib.cmx +mQueryTLexer.cmo: mQueryTParser.cmo +mQueryTLexer.cmx: mQueryTParser.cmx +mQueryIO.cmo: mQILib.cmi mQueryTLexer.cmo mQueryTParser.cmo mQueryIO.cmi +mQueryIO.cmx: mQILib.cmx mQueryTLexer.cmx mQueryTParser.cmx mQueryIO.cmi +mQueryInterpreter.cmo: mQIConn.cmi mQILib.cmi mQIProperty.cmi mQIUtil.cmi \ + mQueryIO.cmi mQueryInterpreter.cmi +mQueryInterpreter.cmx: mQIConn.cmx mQILib.cmx mQIProperty.cmx mQIUtil.cmx \ + mQueryIO.cmx mQueryInterpreter.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index 88c66ac8e..c82572648 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -4,15 +4,19 @@ REQUIRES = helm-urimanager helm-mathql postgres PREDICATES = -INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \ - mQIPostgres.mli mQIMap.mli mQIConn.mli \ - mQIProperty.mli mQueryInterpreter.mli +PRE_IFILES = mQIPostgres.mli mQIMap.mli mQIConn.mli \ + mQIUtil.mli mQILib.mli mQIProperty.mli -IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \ - $(INTERFACE_FILES:%.mli=%.ml) +POST_IFILES = mQueryIO.mli mQueryInterpreter.mli -EXTRA_OBJECTS_TO_INSTALL = mQueryTLexer.cmi \ - mQueryTLexer.mll mQueryTParser.mly +INTERFACE_FILES = $(PRE_IFILES) $(POST_IFILES) + +IMPLEMENTATION_FILES = $(PRE_IFILES:%.mli=%.ml) \ + mQueryTParser.ml mQueryTLexer.ml \ + $(POST_IFILES:%.mli=%.ml) + +EXTRA_OBJECTS_TO_INSTALL = mQITypes.cmi mQueryTLexer.cmi \ + mQITypes.ml mQueryTLexer.mll mQueryTParser.mly EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ mQueryTLexer.ml diff --git a/helm/ocaml/mathql_interpreter/mQILib.ml b/helm/ocaml/mathql_interpreter/mQILib.ml new file mode 100644 index 000000000..f816590d1 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQILib.ml @@ -0,0 +1,346 @@ +(* 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 M = MathQL +module P = MQueryUtil +module U = MQIUtil +module C = MQIConn + +(* external function specification ******************************************) + +type arity_t = Const of int + | Positive + | Any + +type eval_spec = {eval : M.query -> M.result; + handle : C.handle + } + +type txt_out_spec = {out : string -> unit; + path : M.path -> unit; + query : M.query -> unit; + result : M.result -> unit + } + +type fun_spec = {arity_p : arity_t; + arity_s : arity_t; + body : eval_spec -> txt_out_spec -> + M.path list -> M.query list -> M.result; + txt_out : txt_out_spec -> + M.path list -> M.query list -> unit + } + +exception ArityError of M.path * arity_t * int + +exception NameError of M.path + +exception NumberError of M.result + +(* external functions implementation ****************************************) + +let int_of_set s = + try match s with + | [s, _] -> int_of_string s + | _ -> raise (Failure "int_of_string") + with Failure "int_of_string" -> raise (NumberError s) + +let out_txt2 out commit n x1 x2 = + out "(" ; commit x1; out (" " ^ n ^ " "); commit x2; out ")" + +let out_txt_ out path commit p xl = + path p; out " {"; P.flat_list out commit ", " xl; out "}" + +let out_txt_full out path commit p pl xl = + path p; out " {"; P.flat_list out path ", " pl; out "} {"; + P.flat_list out commit ", " xl; out "}" + +let arity0 n r = + let arity_p = Const 0 in + let arity_s = Const 0 in + let body _ _ _ _ = U.mql_true in + let txt_out s _ _ = s.out n in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let arity1 n f = + let arity_p = Const 0 in + let arity_s = Const 1 in + let body eval _ _ = function + | [x] -> f (eval x) + | _ -> assert false + in + let txt_out out _ commit _ = function + | [x] -> out (n ^ " "); commit x + | _ -> assert false + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let arity2 n f = + let arity_p = Const 0 in + let arity_s = Const 2 in + let body eval _ _ = function + | [x1; x2] -> f (eval x1) (eval x2) + | _ -> assert false + in + let txt_out out _ commit _ = function + | [x1; x2] -> out_txt2 out commit n x1 x2 + | _ -> assert false + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let false_fun = arity0 "false" U.mql_false + +let true_fun = arity0 "true" U.mql_true + +let not_fun = + let aux r = if r = U.mql_false then U.mql_true else U.mql_false in + arity1 "not" aux + +let count_fun = + let aux r = [string_of_int (List.length r), []] in + arity1 "count" aux + +let diff_fun = arity2 "diff" U.mql_diff + +let xor_fun = arity2 "xor" U.xor + +let sub_fun = arity2 "sub" U.set_sub + +let meet_fun = arity2 "meet" U.set_meet + +let eq_fun = arity2 "eq" U.set_eq + +let le_fun = + let le v1 v2 = + if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false + in + arity2 "le" le + +let lt_fun = + let lt v1 v2 = + if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false + in + arity2 "lt" lt + +let stat_fun = + let arity_p = Const 0 in + let arity_s = Const 1 in + let body eval h _ = function + | [x] -> + let t = P.start_time () in + let r = (eval x) in + let s = P.stop_time t in + C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); + r + | _ -> assert false + in + let txt_out out _ commit _ = function + | [x] -> out "stat "; commit x + | _ -> assert false + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let align_fun = + let aux l (v, g) = + let c = String.length v in + if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g] + in + let arity_p = Const 0 in + let arity_s = Const 2 in + let body eval _ _ = function + | [y; x] -> + let l = int_of_set (eval y) in + U.mql_iter (aux l) (eval x) + | _ -> assert false + in + let txt_out out _ commit _ = function + | [y; x] -> out "align "; commit y; out " in "; commit x + | _ -> assert false + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let if_fun = + let arity_p = Const 0 in + let arity_s = Const 3 in + let body eval _ _ = function + | [y; x1; x2] -> + if (eval y) = U.mql_false then (eval x2) else (eval x1) + | _ -> assert false + in + let txt_out out _ commit _ = function + | [y; x1; x2] -> + out "if "; commit y; out " then "; commit x1; out " else "; commit x2 + | _ -> assert false + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let intersect_fun = + let rec iter f = function + | [] -> assert false + | [head] -> f head + | head :: tail -> U.mql_intersect (f head) (iter f tail) + in + let arity_p = Const 0 in + let arity_s = Positive in + let body eval _ _ xl = iter eval xl in + let txt_out out path commit _ = function + | [] -> assert false + | [x1; x2] -> out_txt2 out commit "intersect" x1 x2 + | xl -> out_txt_ out path commit ["intersect"] xl + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let union_fun = + let arity_p = Const 0 in + let arity_s = Any in + let body eval _ _ xl = U.mql_iter eval xl in + let txt_out out path commit _ = function + | [x1; x2] -> out_txt2 out commit "union" x1 x2 + | xl -> out_txt_ out path commit ["union"] xl + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let or_fun = + let rec iter f = function + | [] -> U.mql_false + | head :: tail -> + let r1 = f head in + if r1 = U.mql_false then (iter f tail) else r1 + in + let arity_p = Const 0 in + let arity_s = Any in + let body eval _ _ xl = iter eval xl in + let txt_out out path commit _ = function + | [x1; x2] -> out_txt2 out commit "or" x1 x2 + | xl -> out_txt_ out path commit ["or"] xl + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +let and_fun = + let rec iter f = function + | [] -> U.mql_true + | head :: tail -> + if f head = U.mql_false then U.mql_false else (iter f tail) + in + let arity_p = Const 0 in + let arity_s = Any in + let body eval _ _ xl = iter eval xl in + let txt_out out path commit _ = function + | [x1; x2] -> out_txt2 out commit "and" x1 x2 + | xl -> out_txt_ out path commit ["and"] xl + in + {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} + +(* external functions interface *********************************************) + +let get_spec = function + | ["false"] -> false_fun + | ["true"] -> true_fun + | ["not"] -> not_fun + | ["count"] -> count_fun + | ["stat"] -> stat_fun + | ["diff"] -> diff_fun + | ["xor"] -> xor_fun + | ["sub"] -> sub_fun + | ["meet"] -> meet_fun + | ["eq"] -> eq_fun + | ["le"] -> le_fun + | ["lt"] -> lt_fun + | ["align"] -> align_fun + | ["if"] -> if_fun + | ["intersect"] -> intersect_fun + | ["union"] -> union_fun + | ["or"] -> or_fun + | ["and"] -> and_fun + | p -> raise (NameError p) + +let check_arity p m n = + let aux i = function + | Const k when i = k -> () + | Positive when i > 0 -> () + | Any -> () + | a -> raise (ArityError (p, a, i)) + in + aux m (get_spec p).arity_p; aux n (get_spec p).arity_s + +let exec eval h p pl xl = (get_spec p).body eval h pl xl + +let txt_out out path commit p pl xl = + try (get_spec p).txt_out out path commit pl xl + with NameError q when q = p -> out_txt_full out path commit p pl xl + +(* + | M.Proj (Some p) x -> out "proj "; txt_path out p; out "of "; txt_set x + | M.Log a b x -> out "log "; txt_log a b; txt_set x + | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l; + txt_set x + let txt_path_list l = P.flat_list out (txt_path out) ", " l in + let txt_log a b = + if a then out "xml "; + if b then out "source " + in + let txt_allbut b = if b then out "allbut " in + + | M.Proj None x -> List.map (fun (r, _) -> (r, [])) (eval_query c x) + | M.Proj (Some p) x -> + let proj_group_aux (q, v) = if q = p then subj v else [] in + let proj_group a = U.mql_iter proj_group_aux a in + let proj_set (_, g) = U.mql_iter proj_group g in + U.mql_iter proj_set (eval_query c x) + + + | M.Log _ b x -> + if b then begin + let t = P.start_time () in + F.text_of_query (C.log h) x "\n"; + let s = P.stop_time t in + if C.set h C.Stat then + C.log h (Printf.sprintf "Log source: %s\n" s); + eval_query c x + end else begin + let s = (eval_query c x) in + let t = P.start_time () in + F.text_of_result (C.log h) s "\n"; + let r = P.stop_time t in + if C.set h C.Stat then + C.log h (Printf.sprintf "Log: %s\n" r); + s + end + + | M.Keep b l x -> + let keep_path (p, v) t = + if List.mem p l = b then t else (p, v) :: t in + let keep_grp a = List.fold_right keep_path a [] in + let keep_set a g = + let kg = keep_grp a in + if kg = [] then g else kg :: g + in + let keep_av (s, g) = (s, List.fold_right keep_set g []) in + List.map keep_av (eval_query c x) + + +*) diff --git a/helm/ocaml/mathql_interpreter/mQILib.mli b/helm/ocaml/mathql_interpreter/mQILib.mli new file mode 100644 index 000000000..69bd3c04e --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQILib.mli @@ -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 + *) + +type arity_t = Const of int + | Positive + | Any + +type eval_spec = {eval : MathQL.query -> MathQL.result; + handle : MQIConn.handle + } + +type txt_out_spec = {out : string -> unit; + path : MathQL.path -> unit; + query : MathQL.query -> unit; + result : MathQL.result -> unit + } + +val check_arity : MathQL.path -> int -> int -> unit + +val eval : eval_spec -> txt_out_spec -> + MathQL.path -> MathQL.path list -> MathQL.query list -> + MathQL.result + +val txt_out : txt_out_spec -> + MathQL.path -> MathQL.path list -> MathQL.query list -> unit + +exception ArityError of MathQL.path * arity_t * int + +exception NameError of MathQL.path + +exception NumberError of MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index be559adc7..b32b519a1 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -66,13 +66,13 @@ let pg_query h table cols ct cfl = | 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_msval v = iter (fun s, _ -> P.quote s) ", " v in let pg_con (pat, col, v) = if col <> "" then - let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in + let f (s, _) = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in if pat then "(" ^ iter f " or " v ^ ")" else match v with - | [s] -> col ^ " = " ^ (P.quote s) + | [(s,_)] -> col ^ " = " ^ (P.quote s) | v -> col ^ " in (" ^ pg_msval v ^ ")" else "true" in diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml index 00f5390b5..f80fefeec 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml @@ -30,28 +30,31 @@ let mql_false = [] -let mql_true = [""] +let mql_true = [("", [])] (* set theoretic operations *************************************************) let rec set_sub v1 v2 = - match v1, v2 with - | [], _ -> mql_true - | _, [] -> mql_false - | h1 :: _, h2 :: _ when h1 < h2 -> mql_false - | h1 :: _, h2 :: t2 when h1 > h2 -> set_sub v1 t2 - | _ :: t1, _ :: t2 -> set_sub t1 t2 + match (v1, v2) with + | [], _ -> mql_true + | _, [] -> mql_false + | (h1, _) :: _, (h2, _) :: _ when h1 < h2 -> mql_false + | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_sub v1 t2 + | _ :: t1, _ :: t2 -> set_sub t1 t2 let rec set_meet v1 v2 = match v1, v2 with - | [], _ -> mql_false - | _, [] -> mql_false - | h1 :: t1, h2 :: _ when h1 < h2 -> set_meet t1 v2 - | h1 :: _, h2 :: t2 when h1 > h2 -> set_meet v1 t2 - | _, _ -> mql_true + | [], _ + | _, [] -> mql_false + | (h1, _) :: t1, (h2, _) :: _ when h1 < h2 -> set_meet t1 v2 + | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_meet v1 t2 + | _, _ -> mql_true -let set_eq v1 v2 = - if v1 = v2 then mql_true else mql_false +let rec set_eq v1 v2 = + match v1, v2 with + | [], [] -> mql_true + | (h1, _) :: t1, (h2, _) :: t2 when h1 = h2 -> set_eq t1 t2 + | _, _ -> mql_false let rec set_union v1 v2 = match v1, v2 with @@ -123,31 +126,3 @@ let xor v1 v2 = let b = v1 <> mql_false in if b && v2 <> mql_false then mql_false else if b then v1 else v2 - -(* numeric operations ******************************************************) - -let int_of_list = function - | [s] -> int_of_string s - | _ -> raise (Failure "int_of_list") - -let le v1 v2 = - try if int_of_list v1 <= int_of_list v2 then mql_true else mql_false - with _ -> mql_false - -let lt v1 v2 = - try if int_of_list v1 < int_of_list v2 then mql_true else mql_false - with _ -> mql_false - -let align n v = - let c = String.length v in - try - let l = int_of_list [n] in - if c < l then [(String.make (l - c) ' ') ^ v] else [v] - with _ -> [v] - -(* context handling ********************************************************) - -let rec set ap = function - | [] -> [ap] - | head :: tail when fst head = fst ap -> ap :: tail - | head :: tail -> head :: set ap tail diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli index 76735a863..32e0d78dc 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.mli +++ b/helm/ocaml/mathql_interpreter/mQIUtil.mli @@ -26,20 +26,20 @@ (* AUTOR: Ferruccio Guidi *) -val mql_true : MathQL.value +val mql_true : MathQL.result -val mql_false : MathQL.value +val mql_false : MathQL.result -val set_sub : MathQL.value -> MathQL.value -> MathQL.value +val set_sub : MathQL.result -> MathQL.result -> MathQL.result -val set_meet : MathQL.value -> MathQL.value -> MathQL.value +val set_meet : MathQL.result -> MathQL.result -> MathQL.result -val set_eq : MathQL.value -> MathQL.value -> MathQL.value +val set_eq : MathQL.result -> MathQL.result -> MathQL.result val set_union : 'a list -> 'a list -> 'a list - +(* val set_intersect : 'a list -> 'a list -> 'a list - +*) val mql_union : ('a * 'b list) list -> ('a * 'b list) list -> ('a * 'b list) list @@ -58,12 +58,5 @@ val mql_iter : ('c -> ('a * 'b list) list) -> 'c list -> val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list -> 'd list -> ('a * 'b list) list -val xor : MathQL.value -> MathQL.value -> MathQL.value - -val le : MathQL.value -> MathQL.value -> MathQL.value - -val lt : MathQL.value -> MathQL.value -> MathQL.value - -val align : string -> string -> MathQL.value +val xor : MathQL.result -> MathQL.result -> MathQL.result -val set : string * 'a -> (string * 'a) list -> (string * 'a) list diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.ml b/helm/ocaml/mathql_interpreter/mQueryIO.ml new file mode 100644 index 000000000..d59b2f2b7 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryIO.ml @@ -0,0 +1,127 @@ +(* 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 M = MathQL +module P = MQueryUtil +module L = MQILib + +(* text linearization and parsing *******************************************) + +let txt_str out s = out ("\"" ^ s ^ "\"") + +let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p + +let text_of_result out x sep = + let txt_attr = function + | (p, []) -> txt_path out p + | (p, l) -> txt_path out p; out " = "; + P.flat_list out (txt_str out) ", " l + in + let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in + let txt_res = function + | (s, []) -> txt_str out s + | (s, l) -> txt_str out s; out " attr "; + P.flat_list out txt_group ", " l + in + let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in + txt_set x + +let text_of_query out x sep = + let txt_svar sv = out ("%" ^ sv) in + let txt_avar av = out ("@" ^ av) in + let txt_inv i = if i then out "inverse " in + let txt_ref = function + | M.RefineExact -> () + | M.RefineSub -> out "sub " + | M.RefineSuper -> out "super " + in + let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in + let main = function + | [] -> () + | p -> out " main "; txt_path out p + in + let txt_exp = function + | (pl, None) -> txt_path out pl + | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr + in + let txt_exp_list = function + | [] -> () + | l -> out " attr "; P.flat_list out txt_exp ", " l + in + let pattern b = if b then out "pattern " in + let txt_distr d = if d then out "distr " in + let txt_gen = function + | M.GenFJoin -> out " sup " + | M.GenFMeet -> out " inf " + in + let rec txt_con (pat, p, x) = + txt_path out p; + if pat then out " match " else out " in "; + txt_set x + and txt_con_list s = function + | [] -> () + | l -> out s; P.flat_list out txt_con ", " l + and txt_istrue lt = txt_con_list " istrue " lt + and txt_isfalse lf = txt_con_list " isfalse " lf + and txt_ass (p, x) = txt_set x; out " as "; txt_path out p + and txt_ass_list l = P.flat_list out txt_ass ", " l + and txt_assg_list g = P.flat_list out txt_ass_list "; " g + and txt_grp = function + | M.Attr g -> txt_assg_list g + | M.From av -> txt_avar av + and txt_set = function + | M.Fun p pl xl -> + L.txt_out out (txt_path out) txt_set p pl xl + | M.Const [s, []] -> txt_str out s + | M.Const r -> text_of_result out r " " + | M.Dot av p -> txt_avar av; out "."; txt_path out p + | M.Ex b x -> out "ex "; txt_set x +(* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b; + out "] "; txt_set x +*) | M.SVar sv -> txt_svar sv + | M.AVar av -> txt_avar av + | M.Property q0 q1 q2 mc ct cfl xl b x -> + out "property "; txt_qualif q0 q1 q2; main mc; + txt_istrue ct; P.flat_list out txt_isfalse "" cfl; txt_exp_list xl; + out " of "; pattern b; txt_set x + | M.Let sv x y -> out "let "; txt_svar sv; out " be "; + txt_set x; out " in "; txt_set y + | M.Select av x y -> out "select "; txt_avar av; out " from "; + txt_set x; out " where "; txt_set y + | M.For k av x y -> out "for "; txt_avar av; out " in "; + txt_set x; txt_gen k; txt_set y + | M.Add d g x -> out "add "; txt_distr d; txt_grp g; + out " in "; txt_set x + in + txt_set x; out sep + +let query_of_text lexbuf = + MQueryTParser.query MQueryTLexer.query_token lexbuf + +let result_of_text lexbuf = + MQueryTParser.result MQueryTLexer.result_token lexbuf diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.mli b/helm/ocaml/mathql_interpreter/mQueryIO.mli new file mode 100644 index 000000000..d74bdd280 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryIO.mli @@ -0,0 +1,35 @@ +(* 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 + *) + +val text_of_query : (string -> unit) -> MathQL.query -> string -> unit + +val text_of_result : (string -> unit) -> MathQL.result -> string -> unit + +val query_of_text : Lexing.lexbuf -> MathQL.query + +val result_of_text : Lexing.lexbuf -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index 58fb7b87e..7c7ef8a56 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -26,83 +26,50 @@ (* AUTOR: Ferruccio Guidi *) -(* contexts *****************************************************************) +exception Found -type svar_context = (MathQL.svar * MathQL.resource_set) list +module M = MathQL +module P = MQueryUtil +module C = MQIConn +module U = MQIUtil +module L = MQILib +module F = MQueryIO -type avar_context = (MathQL.avar * MathQL.resource) list +(* contexts *****************************************************************) -type group_context = (MathQL.avar * MathQL.attribute_group) list +type svar_context = (M.svar * M.resource_set) list -type vvar_context = (MathQL.vvar * MathQL.value) list +type avar_context = (M.avar * M.resource) list + +type group_context = (M.avar * M.attribute_group) list type context = {svars: svar_context; avars: avar_context; - groups: group_context; (* auxiliary context *) - vvars: vvar_context + groups: group_context (* auxiliary context *) } - -(* execute *****************************************************************) - -exception Found - -module M = MathQL -module P = MQueryUtil -module C = MQIConn -module U = MQIUtil + +(* execute ******************************************************************) let execute h x = let warn q = if C.set h C.Warn then begin C.log h "MQIExecute: waring: reference to undefined variables: "; - P.text_of_query (C.log h) q "\n" + F.text_of_query (C.log h) q "\n" end in - let rec eval_val c = function - | M.False -> U.mql_false - | M.True -> U.mql_true - | M.Const s -> [s] - | M.Set l -> U.iter (eval_val c) l - | M.Test k y1 y2 -> - let cand y1 y2 = - if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2 - in - let cor y1 y2 = - let v1 = eval_val c y1 in - if v1 = U.mql_false then eval_val c y2 else v1 - in - let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in - let f = match k with - | M.And -> cand - | M.Or -> cor - | M.Xor -> h U.xor - | M.Sub -> h U.set_sub - | M.Meet -> h U.set_meet - | M.Eq -> h U.set_eq - | M.Le -> h U.le - | M.Lt -> h U.lt - in - f y1 y2 - | M.Not y -> - if eval_val c y = U.mql_false then U.mql_true else U.mql_false - | M.VVar i -> begin - try List.assoc i c.vvars - with Not_found -> warn (M.Subj (M.VVar i)); [] end + let subj v = List.map (fun s -> (s, [])) v in + let proj v = List.map fst v in + let rec eval_query c = function + | M.Const r -> r | M.Dot i p -> begin - try List.assoc p (List.assoc i c.groups) - with Not_found -> warn (M.Subj (M.Dot i p)); [] end - | M.Proj None x -> List.map (fun (r, _) -> r) (eval_query c x) - | M.Proj (Some p) x -> - let proj_group_aux (q, v) = if q = p then v else [] in - let proj_group a = U.iter proj_group_aux a in - let proj_set (_, g) = U.iter proj_group g in - U.iter proj_set (eval_query c x) + try subj (List.assoc p (List.assoc i c.groups)) + with Not_found -> warn (M.Dot i p); [] end | M.Ex l y -> let rec ex_aux h = function | [] -> let d = {c with groups = h} in - if eval_val d y = U.mql_false then () else raise Found + if eval_query d y = U.mql_false then () else raise Found | i :: tail -> begin try @@ -116,57 +83,15 @@ let execute h x = end in (try ex_aux [] l; U.mql_false with Found -> U.mql_true) - | M.StatVal y -> - let t = P.start_time () in - let r = (eval_val c y) in - let s = P.stop_time t in - C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); - r - | M.Count y -> [string_of_int (List.length (eval_val c y))] - | M.Align s y -> U.iter (U.align s) (eval_val c y) - and eval_query c = function - | M.Empty -> [] - | M.Subj x -> - List.map (fun s -> (s, [])) (eval_val c x) - | M.Log _ b x -> - if b then begin - let t = P.start_time () in - P.text_of_query (C.log h) x "\n"; - let s = P.stop_time t in - if C.set h C.Stat then - C.log h (Printf.sprintf "Log source: %s\n" s); - eval_query c x - end else begin - let s = (eval_query c x) in - let t = P.start_time () in - P.text_of_result (C.log h) s "\n"; - let r = P.stop_time t in - if C.set h C.Stat then - C.log h (Printf.sprintf "Log: %s\n" r); - s - end - | M.If y x1 x2 -> - if (eval_val c y) = U.mql_false - then (eval_query c x2) else (eval_query c x1) - | M.Bin k x1 x2 -> - let f = match k with - | M.BinFJoin -> U.mql_union - | M.BinFMeet -> U.mql_intersect - | M.BinFDiff -> U.mql_diff - in - f (eval_query c x1) (eval_query c x2) | M.SVar i -> begin try List.assoc i c.svars with Not_found -> warn (M.SVar i); [] end | M.AVar i -> begin try [List.assoc i c.avars] with Not_found -> warn (M.AVar i); [] end - | M.LetSVar i x1 x2 -> - let d = {c with svars = U.set (i, eval_query c x1) c.svars} in + | M.Let i x1 x2 -> + let d = {c with svars = P.add_assoc (i, eval_query c x1) c.svars} in eval_query d x2 - | M.LetVVar i y x -> - let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in - eval_query d x | M.For k i x1 x2 -> let f = match k with | M.GenFJoin -> U.mql_union @@ -175,7 +100,7 @@ let execute h x = let rec for_aux = function | [] -> [] | h :: t -> - let d = {c with avars = U.set (i, h) c.avars} in + let d = {c with avars = P.add_assoc (i, h) c.avars} in f (eval_query d x2) (for_aux t) in for_aux (eval_query c x1) @@ -185,10 +110,10 @@ let execute h x = List.fold_right g (eval_query c x) [] | M.Property q0 q1 q2 mc ct cfl el pat y -> let subj, mct = - if q0 then [], (pat, q2 @ mc, eval_val c y) - else (q2 @ mc), (pat, [], eval_val c y) + if q0 then [], (pat, q2 @ mc, eval_query c y) + else (q2 @ mc), (pat, [], eval_query c y) in - let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in + let eval_cons (pat, p, y) = (pat, q2 @ p, eval_query c y) in let cons_true = mct :: List.map eval_cons ct in let cons_false = List.map (List.map eval_cons) cfl in let eval_exp (p, po) = (q2 @ p, po) in @@ -199,41 +124,26 @@ let execute h x = if C.set h C.Stat then C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r)); r - | M.StatQuery x -> - let t = P.start_time () in - let r = (eval_query c x) in - let s = P.stop_time t in - C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); - r | M.Select i x y -> let rec select_aux = function | [] -> [] | h :: t -> - let d = {c with avars = U.set (i, h) c.avars} in - if eval_val d y = U.mql_false + let d = {c with avars = P.add_assoc (i, h) c.avars} in + if eval_query d y = U.mql_false then select_aux t else h :: select_aux t in select_aux (eval_query c x) - | M.Keep b l x -> - let keep_path (p, v) t = - if List.mem p l = b then t else (p, v) :: t in - let keep_grp a = List.fold_right keep_path a [] in - let keep_set a g = - let kg = keep_grp a in - if kg = [] then g else kg :: g - in - let keep_av (s, g) = (s, List.fold_right keep_set g []) in - List.map keep_av (eval_query c x) + | M.Fun p pl xl -> L.exec (eval_query c) h p pl xl and eval_grp c = function | M.Attr gs -> - let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] in + let attr_aux g (p, y) = U.mql_union g [p, proj (eval_query c y)] in let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in List.fold_left attr_auxs [] gs | M.From i -> try snd (List.assoc i c.avars) with Not_found -> warn (M.AVar i); [] in - let c = {svars = []; avars = []; groups = []; vvars = []} in + let c = {svars = []; avars = []; groups = []} in let t = P.start_time () in let r = eval_query c x in let s = P.stop_time t in diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll index abccb4626..6969fcb3e 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll +++ b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll @@ -57,11 +57,12 @@ and query_token = parse out ("STR " ^ str); STR str } | '(' { out "LP"; LP } | ')' { out "RP"; RP } + | '[' { out "LB"; LB } + | ']' { out "RB"; RB } | '{' { out "LC"; LC } | '}' { out "RC"; RC } | '@' { out "AT"; AT } | '%' { out "PC"; PC } - | '$' { out "DL"; DL } | '.' { out "FS"; FS } | ',' { out "CM"; CM } | ';' { out "SC"; SC } @@ -108,7 +109,6 @@ and query_token = parse | "source" { out "SOURCE"; SOURCE } | "stat" { out "STAT" ; STAT } | "sub" { out "SUB" ; SUB } - | "subj" { out "SUBJ" ; SUBJ } | "sup" { out "SUP" ; SUP } | "super" { out "SUPER" ; SUPER } | "then" { out "THEN" ; THEN } diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly index 313636c80..1025cf316 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly +++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly @@ -28,6 +28,11 @@ %{ module M = MathQL + module L = MQILib + + let make_fun p pl xl = + L.check_arity p (List.length pl) (List.length xl); + M.Fun p pl xl let analyze x = let rec join l1 l2 = match l1, l2 with @@ -41,57 +46,39 @@ | [] -> [] | head :: tail -> join (f head) (iter f tail) in - let rec an_val = function - | M.True -> [] - | M.False -> [] - | M.Const _ -> [] - | M.VVar _ -> [] - | M.Ex _ -> [] - | M.Dot rv _ -> [rv] - | M.Not x -> an_val x - | M.StatVal x -> an_val x - | M.Count x -> an_val x - | M.Align _ x -> an_val x - | M.Proj _ x -> an_set x - | M.Test _ x y -> iter an_val [x; y] - | M.Set l -> iter an_val l - and an_set = function - | M.Empty -> [] - | M.SVar _ -> [] - | M.AVar _ -> [] - | M.Subj x -> an_val x - | M.Keep _ _ x -> an_set x - | M.Log _ _ x -> an_set x - | M.StatQuery x -> an_set x - | M.Bin _ x y -> iter an_set [x; y] - | M.LetSVar _ x y -> iter an_set [x; y] + let rec an_set = function + | M.Const _ + | M.SVar _ + | M.AVar _ + | M.Ex _ -> [] + | M.Dot rv _ -> [rv] + | M.Let _ x y + | M.Select _ x y | M.For _ _ x y -> iter an_set [x; y] + | M.Fun _ _ l -> iter an_set l | M.Add _ g x -> join (an_grp g) (an_set x) - | M.LetVVar _ x y -> join (an_val x) (an_set y) - | M.Select _ x y -> join (an_set x) (an_val y) | M.Property _ _ _ _ c d _ _ x -> - join (an_val x) (iter an_con [c; List.concat d]) - | M.If x y z -> join (an_val x) (iter an_set [y; z]) - and fc (_, _, v) = an_val v + join (an_set x) (iter an_con [c; List.concat d]) + and fc (_, _, v) = an_set v and an_con c = iter fc c - and fg (_, v) = an_val v + and fg (_, v) = an_set v and an_grp = function | M.Attr g -> iter (iter fg) g | M.From _ -> [] in - an_val x + an_set x let f (x, y, z) = x let s (x, y, z) = y let t (x, y, z) = z %} %token ID STR - %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF + %token LB RB SL IS LC RC CM SC LP RP AT PC FS DQ EOF %token ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX %token FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT %token MAIN MATCH MEET NOT OF OR PAT PROJ PROP SELECT SOURCE STAT SUB - %token SUBJ SUP SUPER THEN TRUE UNION WHERE XOR - %nonassoc IN SUP INF ELSE LOG STAT + %token SUP SUPER THEN TRUE UNION WHERE XOR + %nonassoc IN SUP INF ELSE LOG STAT KEEP %left DIFF %left UNION %left INTER @@ -100,7 +87,7 @@ %left AND %nonassoc NOT %nonassoc SUB MEET EQ LT LE - %nonassoc SUBJ OF PROJ COUNT ALIGN + %nonassoc OF PROJ COUNT ALIGN %start qstr query result %type qstr @@ -117,9 +104,6 @@ avar: | AT ID { $2 } ; - vvar: - | DL ID { $2 } - ; strs: | STR CM strs { $1 :: $3 } | STR { [$1] } @@ -129,7 +113,6 @@ | STR { [$1] } ; path: - | subpath { $1 } | SL subpath { $2 } | SL { [] } ; @@ -149,8 +132,8 @@ | inv ref path { $1, $2, $3 } ; cons: - | path IN val_exp { (false, $1, $3) } - | path MATCH val_exp { (true, $1, $3) } + | path IN set_exp { (false, $1, $3) } + | path MATCH set_exp { (true, $1, $3) } ; conss: | cons CM conss { $1 :: $3 } @@ -184,12 +167,8 @@ | PAT { true } | { false } ; - opt_path: - | path { Some $1 } - | { None } - ; ass: - | val_exp AS path { ($3, $1) } + | set_exp AS path { ($3, $1) } ; asss: | ass CM asss { $1 :: $3 } @@ -204,81 +183,109 @@ | { false } ; allbut: - | BUT { true } - | { false } - ; - bin_op: - | set_exp DIFF set_exp { M.BinFDiff, $1, $3 } - | set_exp UNION set_exp { M.BinFJoin, $1, $3 } - | set_exp INTER set_exp { M.BinFMeet, $1, $3 } + | BUT { "allbut" } + | { "these" } ; gen_op: | SUP set_exp { M.GenFJoin, $2 } | INF set_exp { M.GenFMeet, $2 } ; - test_op: - | val_exp XOR val_exp { M.Xor, $1, $3 } - | val_exp OR val_exp { M.Or, $1, $3 } - | val_exp AND val_exp { M.And, $1, $3 } - | val_exp SUB val_exp { M.Sub, $1, $3 } - | val_exp MEET val_exp { M.Meet, $1, $3 } - | val_exp EQ val_exp { M.Eq, $1, $3 } - | val_exp LE val_exp { M.Le, $1, $3 } - | val_exp LT val_exp { M.Lt, $1, $3 } - ; source: - | SOURCE { true } - | { false } + | SOURCE { "source" } + | { "result" } ; xml: - | { false} + | { "text" } ; grp_exp: | assg { M.Attr $1 } | avar { M.From $1 } ; - val_exp: - | TRUE { M.True } - | FALSE { M.False } - | STR { M.Const $1 } - | avar FS path { M.Dot $1 $3 } - | vvar { M.VVar $1 } - | LC vals RC { M.Set $2 } - | LC RC { M.Set [] } - | LP val_exp RP { $2 } - | STAT val_exp { M.StatVal $2 } - | EX val_exp { M.Ex (analyze $2) $2 } - | NOT val_exp { M.Not $2 } - | test_op { M.Test (f $1) (s $1) (t $1) } - | PROJ opt_path set_exp { M.Proj $2 $3 } - | COUNT val_exp { M.Count $2 } - | ALIGN STR IN val_exp { M.Align $2 $4 } - ; - vals: - | val_exp CM vals { $1 :: $3 } - | val_exp { [$1] } - ; set_exp: - | EMPTY { M.Empty } - | LP set_exp RP { $2 } - | svar { M.SVar $1 } - | avar { M.AVar $1 } - | LET svar BE set_exp IN set_exp { M.LetSVar $2 $4 $6 } - | LET vvar BE val_exp IN set_exp { M.LetVVar $2 $4 $6 } + | FALSE + { make_fun ["false"] [] [] } + | TRUE + { make_fun ["true"] [] [] } + | STR + { M.Const [$1, []] } + | LB resources RB + { M.Const $2 } + | avar FS path + { M.Dot $1 $3 } + | LC sets RC + { make_fun ["union"] [] $2 } + | LC RC + { make_fun ["union"] [] [] } + | LP set_exp RP + { $2 } + | STAT set_exp + { make_fun ["stat"] [] [$2] } + | EX set_exp + { M.Ex (analyze $2) $2 } + | NOT set_exp + { make_fun ["not"] [] [$2] } + | PROJ path OF set_exp + { make_fun ["proj"] [$2] [$4] } + | COUNT set_exp + { make_fun ["count"] [] [$2] } + | ALIGN set_exp IN set_exp + { make_fun ["align"] [] [$2; $4] } + | EMPTY + { make_fun ["false"] [] [] } + | svar + { M.SVar $1 } + | avar + { M.AVar $1 } + | LET svar BE set_exp IN set_exp + { M.Let $2 $4 $6 } | FOR avar IN set_exp gen_op { M.For (fst $5) $2 $4 (snd $5) } - | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 } - | IF val_exp THEN set_exp ELSE set_exp { M.If $2 $4 $6 } - | PROP qualif mainc istrue isfalse attrc OF pattern val_exp + | ADD distr grp_exp IN set_exp + { M.Add $2 $3 $5 } + | IF set_exp THEN set_exp ELSE set_exp + { make_fun ["diff"] [] [$2; $4; $6] } + | PROP qualif mainc istrue isfalse attrc OF pattern set_exp { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 } - | LOG xml source set_exp { M.Log $2 $3 $4 } - | STAT set_exp { M.StatQuery $2 } - | KEEP allbut paths IN set_exp { M.Keep $2 $3 $5 } - | KEEP allbut IN set_exp { M.Keep $2 [] $4 } - | bin_op - { M.Bin (f $1) (s $1) (t $1) } - | SELECT avar FROM set_exp WHERE val_exp { M.Select $2 $4 $6 } - | SUBJ val_exp { M.Subj $2 } + | LOG xml source set_exp + { make_fun ["log"; $2; $3] [] [$4] } + | KEEP allbut paths IN set_exp + { make_fun ["keep"; $2] $3 [$5] } + | KEEP allbut set_exp + { make_fun ["keep"; $2] [] [$3] } + | SELECT avar FROM set_exp WHERE set_exp + { M.Select $2 $4 $6 } + | path LC paths RC LC sets RC + { make_fun $1 $3 $6 } + | path LC sets RC + { make_fun $1 [] $3 } + | path LC RC + { make_fun $1 [] [] } + | set_exp DIFF set_exp + { make_fun ["diff"] [] [$1; $3] } + | set_exp UNION set_exp + { make_fun ["union"] [] [$1; $3] } + | set_exp INTER set_exp + { make_fun ["intersect"] [] [$1; $3] } + | set_exp XOR set_exp + { make_fun ["xor"] [] [$1; $3] } + | set_exp OR set_exp + { make_fun ["or"] [] [$1; $3] } + | set_exp AND set_exp + { make_fun ["and"] [] [$1; $3] } + | set_exp SUB set_exp + { make_fun ["sub"] [] [$1; $3] } + | set_exp MEET set_exp + { make_fun ["meet"] [] [$1; $3] } + | set_exp EQ set_exp + { make_fun ["eq"] [] [$1; $3] } + | set_exp LE set_exp + { make_fun ["le"] [] [$1; $3] } + | set_exp LT set_exp + { make_fun ["lt"] [] [$1; $3] } + ; + sets: + | set_exp CM sets { $1 :: $3 } + | set_exp { [$1] } ; query: | set_exp { $1 } @@ -310,5 +317,6 @@ | { [] } ; result: - | resources { $1 } - | EOF { raise End_of_file } + | resources { $1 } + | resources error { $1 } + | EOF { raise End_of_file } diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml deleted file mode 100644 index 30e6688ee..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.ml +++ /dev/null @@ -1,218 +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 - *) - -(* text linearization and parsing *******************************************) - -let rec txt_list out f s = function - | [] -> () - | [a] -> f a - | a :: tail -> f a; out s; txt_list out f s tail - -let txt_str out s = out ("\"" ^ s ^ "\"") - -let txt_path out p = out "/"; txt_list out (txt_str out) "/" p - -let text_of_query out x sep = - let module M = MathQL in - let txt_path_list l = txt_list out (txt_path out) ", " l in - let txt_svar sv = out ("%" ^ sv) in - let txt_avar av = out ("@" ^ av) in - let txt_vvar vv = out ("$" ^ vv) in - let txt_inv i = if i then out "inverse " in - let txt_ref = function - | M.RefineExact -> () - | M.RefineSub -> out "sub " - | M.RefineSuper -> out "super " - in - let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in - let main = function - | [] -> () - | p -> out " main "; txt_path out p - in - let txt_exp = function - | (pl, None) -> txt_path out pl - | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr - in - let txt_exp_list = function - | [] -> () - | l -> out " attr "; txt_list out txt_exp ", " l - in - let pattern b = if b then out "pattern " in - let txt_opt_path = function - | None -> () - | Some p -> txt_path out p; out " " - in - let txt_distr d = if d then out "distr " in - let txt_bin = function - | M.BinFJoin -> out " union " - | M.BinFMeet -> out " intersect " - | M.BinFDiff -> out " diff " - in - let txt_gen = function - | M.GenFJoin -> out " sup " - | M.GenFMeet -> out " inf " - in - let txt_test = function - | M.Xor -> out " xor " - | M.Or -> out " or " - | M.And -> out " and " - | M.Sub -> out " sub " - | M.Meet -> out " meet " - | M.Eq -> out " eq " - | M.Le -> out " le " - | M.Lt -> out " lt " - in - let txt_log a b = - if a then out "xml "; - if b then out "source " - in - let txt_allbut b = if b then out "allbut " in - let rec txt_con (pat, p, x) = - txt_path out p; - if pat then out " match " else out " in "; - txt_val x - and txt_con_list s = function - | [] -> () - | l -> out s; txt_list out txt_con ", " l - and txt_istrue lt = txt_con_list " istrue " lt - and txt_isfalse lf = txt_con_list " isfalse " lf - and txt_ass (p, x) = txt_val x; out " as "; txt_path out p - and txt_ass_list l = txt_list out txt_ass ", " l - and txt_assg_list g = txt_list out txt_ass_list "; " g - and txt_val_list = function - | [v] -> txt_val v - | l -> out "{"; txt_list out txt_val ", " l; out "}" - and txt_grp = function - | M.Attr g -> txt_assg_list g - | M.From av -> txt_avar av - and txt_val = function - | M.True -> out "true" - | M.False -> out "false" - | M.Const s -> txt_str out s - | M.Set l -> txt_val_list l - | M.VVar vv -> txt_vvar vv - | M.Dot av p -> txt_avar av; out "."; txt_path out p - | M.Proj op x -> out "proj "; txt_opt_path op; txt_set x - | M.Ex b x -> out "ex "; txt_val x -(* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x -*) | M.Not x -> out "not "; txt_val x - | M.Test k x y -> out "("; txt_val x; txt_test k; txt_val y; out ")" - | M.StatVal x -> out "stat "; txt_val x - | M.Count x -> out "count "; txt_val x - | M.Align s x -> out "align "; txt_str out s; out " in "; txt_val x - and txt_set = function - | M.Empty -> out "empty" - | M.SVar sv -> txt_svar sv - | M.AVar av -> txt_avar av - | M.Property q0 q1 q2 mc ct cfl xl b x -> - out "property "; txt_qualif q0 q1 q2; main mc; - txt_istrue ct; txt_list out txt_isfalse "" cfl; txt_exp_list xl; - out " of "; pattern b; txt_val x - | M.Bin k x y -> out "("; txt_set x; txt_bin k; txt_set y; - out ")" - | M.LetSVar sv x y -> out "let "; txt_svar sv; out " be "; - txt_set x; out " in "; txt_set y - | M.LetVVar vv x y -> out "let "; txt_vvar vv; out " be "; - txt_val x; out " in "; txt_set y - | M.Select av x y -> out "select "; txt_avar av; out " from "; - txt_set x; out " where "; txt_val y - | M.Subj x -> out "subj "; txt_val x - | M.For k av x y -> out "for "; txt_avar av; out " in "; - txt_set x; txt_gen k; txt_set y - | M.If x y z -> out "if "; txt_val x; out " then "; - txt_set y; out " else "; txt_set z - | M.Add d g x -> out "add "; txt_distr d; txt_grp g; - out " in "; txt_set x - | M.Log a b x -> out "log "; txt_log a b; txt_set x - | M.StatQuery x -> out "stat "; txt_set x - | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l; - txt_set x - in - txt_set x; out sep - -let text_of_result out x sep = - let txt_attr = function - | (p, []) -> txt_path out p - | (p, l) -> txt_path out p; out " = "; txt_list out (txt_str out) ", " l - in - let txt_group l = out "{"; txt_list out txt_attr "; " l; out "}" in - let txt_res = function - | (s, []) -> txt_str out s - | (s, l) -> txt_str out s; out " attr "; txt_list out txt_group ", " l - in - let txt_set l = txt_list out txt_res ("; " ^ sep) l; out sep in - txt_set x - -let query_of_text lexbuf = - MQueryTParser.query MQueryTLexer.query_token lexbuf - -let result_of_text lexbuf = - MQueryTParser.result MQueryTLexer.result_token lexbuf - -(* 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) - -(* operations on lists *****************************************************) - -type 'a comparison = Lt - | Gt - | Eq of 'a - -let list_join f l1 l2 = - let rec aux = function - | [], v - | v, [] -> v - | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin - match f h1 h2 with - | Lt -> h1 :: aux (t1, v2) - | Gt -> h2 :: aux (v1, t2) - | Eq h -> h :: aux (t1, t2) - end - in aux (l1, l2) - -let list_meet f l1 l2 = - let rec aux = function - | [], v - | v, [] -> [] - | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin - match f h1 h2 with - | Lt -> aux (t1, v2) - | Gt -> aux (v1, t2) - | Eq h -> h :: aux (t1, t2) - end - in aux (l1, l2) - diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.mli b/helm/ocaml/mathql_interpreter/mQueryUtil.mli deleted file mode 100644 index 2a3c80b83..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.mli +++ /dev/null @@ -1,49 +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 - *) - -val text_of_query : (string -> unit) -> MathQL.query -> string -> unit - -val text_of_result : (string -> unit) -> MathQL.result -> string -> unit - -val query_of_text : Lexing.lexbuf -> MathQL.query - -val result_of_text : Lexing.lexbuf -> MathQL.result - -type time - -val start_time : unit -> time - -val stop_time : time -> string - -type 'a comparison = Lt - | Gt - | Eq of 'a - -val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list - -val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list