From: Ferruccio Guidi Date: Tue, 20 Jan 2004 18:10:30 +0000 (+0000) Subject: functor added X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=381006cf8b418cfdeaf145ab7df9e8f2b19ae2e6 functor added --- diff --git a/helm/mathql_test/.depend b/helm/mathql_test/.depend index 851d52dd6..b8d9e578a 100644 --- a/helm/mathql_test/.depend +++ b/helm/mathql_test/.depend @@ -1,3 +1,5 @@ +mqgtop.cmo: mQGTopLexer.cmo mQGTopParser.cmi +mqgtop.cmx: mQGTopLexer.cmx mQGTopParser.cmx mQGTopParser.cmo: mQGTopParser.cmi mQGTopParser.cmx: mQGTopParser.cmi mQGTopLexer.cmo: mQGTopParser.cmi diff --git a/helm/mathql_test/Makefile b/helm/mathql_test/Makefile index 04fea5185..a4a0c181a 100644 --- a/helm/mathql_test/Makefile +++ b/helm/mathql_test/Makefile @@ -1,6 +1,7 @@ BIN_DIR = /usr/local/bin -REQUIRES = unix helm-cic_textual_parser \ - helm-mathql helm-mathql_interpreter helm-mathql_generator +REQUIRES = unix helm-cic_textual_parser helm-cic_proof_checking \ + helm-mathql helm-mathql_interpreter helm-mathql_generator \ + helm-tactics PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index ae06bc752..16a5ea0a9 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -26,6 +26,9 @@ (* AUTOR: Ferruccio Guidi *) +let _ = MQueryStandard.init +let _ = MQueryHELM.init + let query_num = ref 1 let interp_file = ref "interp.cic" @@ -51,6 +54,7 @@ module C3 = CGLocateInductive module C2 = CGSearchPattern module C1 = CGMatchConclusion module GU = MQGUtil +module M = MQueryMisc let get_handle () = C.init (C.flags_of_string ! int_options) @@ -116,16 +120,14 @@ let get_terms interp = in aux () -let pp_type_of uri = - let u = UriManager.uri_of_string uri in - let s = match (CicEnvironment.get_obj u) with - | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty - | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty - | _ -> "Current proof or inductive definition." -(* - | Cic.CurrentProof (_,conjs,te,ty) -> - | C.InductiveDefinition _ -> -*) +let pp_term_of b uri = + let s = try + let body, ty = M.get_object (M.uriref_of_string uri) in + if b then CicPp.ppterm body else CicPp.ppterm ty + with + | M.CurrentProof -> "proof in progress" + | M.InductiveDefinition -> "inductive definition" + | M.IllFormedFragment -> "ill formed fragment identifier" in print_endline s; flush stdout let rec display = function @@ -277,6 +279,7 @@ let prerr_help () = prerr_endline "-o -options STRING sets the interpreter options"; prerr_endline "-c -check checks the database connection"; prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object"; + prerr_endline "-b -bodyof URI outputs the CIC body of the given HELM object"; prerr_endline "-x -execute issues a query given in the input file"; prerr_endline "-i -interp FILE sets the CIC short names interpretation file"; prerr_endline "-d -disply outputs the CIC terms given in the input file"; @@ -297,14 +300,15 @@ let prerr_help () = prerr_endline "NOTES: * current interpreter options are:"; prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)"; prerr_endline " * CIC terms are read with the HELM CIC Textual Parser"; - prerr_endline " * -typeof does not work with inductive types and proofs in progress\n" + prerr_endline " * -typeof / -bodyof do not work with proofs in progress\n" let rec parse = function | [] -> () | ("-h"|"-help") :: rem -> prerr_help (); parse rem | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem - | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem + | ("-t"|"-typeof") :: arg :: rem -> pp_term_of false arg; parse rem + | ("-b"|"-bodyof") :: arg :: rem -> pp_term_of true arg; parse rem | ("-x"|"-execute") :: rem -> execute stdin; parse rem | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem @@ -326,9 +330,9 @@ let rec parse = function let _ = let t = U.start_time () in - Logger.log_callback := +(* Logger.log_callback := (Logger.log_to_html ~print_and_flush:(fun s -> print_string s; flush stdout)) ; - parse (List.tl (Array.to_list Sys.argv)); +*) parse (List.tl (Array.to_list Sys.argv)); prerr_endline ("mqgtop: done in " ^ (U.stop_time t)); exit 0 diff --git a/helm/mathql_test/mqitop.ml b/helm/mathql_test/mqitop.ml index aca13b9cb..4d45740cf 100644 --- a/helm/mathql_test/mqitop.ml +++ b/helm/mathql_test/mqitop.ml @@ -26,13 +26,17 @@ (* AUTOR: Ferruccio Guidi *) -module U = MQueryUtil +let _ = MQueryStandard.init +let _ = MQueryHELM.init + +module P = MQueryUtil +module U = AvsUtil module I = MQueryInterpreter module C = MQIConn module F = MQueryIO let _ = - let t = U.start_time () in + let t = P.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 log s = print_string s; flush stdout in @@ -41,13 +45,13 @@ let _ = print_endline "mqitop: no connection"; flush stdout end; let rec aux () = - let t = U.start_time () in + let t = P.start_time () in let r = I.execute handle (F.query_of_text ich) in (* F.text_of_result log r "\n"; -*) Printf.eprintf "mqitop: query: %s,%i\n" (U.stop_time t) (List.length r); +*) Printf.eprintf "mqitop: query: %s,%i\n" (P.stop_time t) (U.count r); flush stderr; aux() in begin try aux() with End_of_file -> () end; C.close handle; - Printf.eprintf "mqitop: done: %s\n" (U.stop_time t) + Printf.eprintf "mqitop: done: %s\n" (P.stop_time t) diff --git a/helm/mathql_test/mqtop.ml b/helm/mathql_test/mqtop.ml index f0e0dc877..4c54653cd 100644 --- a/helm/mathql_test/mqtop.ml +++ b/helm/mathql_test/mqtop.ml @@ -26,6 +26,9 @@ (* AUTOR: Ferruccio Guidi *) +let _ = MQueryStandard.init +let _ = MQueryHELM.init + let _ = let module U = MQueryUtil in let module F = MQueryIO in diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend index ff5132bcc..6d18bd83c 100644 --- a/helm/ocaml/mathql/.depend +++ b/helm/ocaml/mathql/.depend @@ -1,2 +1,10 @@ +listAvs.cmi: avs.cmo +avsUtil.cmi: mathQL.cmo +listAvs.cmo: avs.cmo listAvs.cmi +listAvs.cmx: avs.cmx listAvs.cmi +mathQL.cmo: avs.cmo listAvs.cmi +mathQL.cmx: avs.cmx listAvs.cmx +avsUtil.cmo: mathQL.cmo avsUtil.cmi +avsUtil.cmx: mathQL.cmx avsUtil.cmi mQueryUtil.cmo: mQueryUtil.cmi mQueryUtil.cmx: mQueryUtil.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index a6a165f0a..30678e429 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -3,11 +3,11 @@ REQUIRES = PREDICATES = -INTERFACE_FILES = mQueryUtil.mli +INTERFACE_FILES = mQueryUtil.mli listAvs.mli avsUtil.mli -IMPLEMENTATION_FILES = mathQL.ml mQueryUtil.ml +IMPLEMENTATION_FILES = mQueryUtil.ml avs.ml listAvs.ml mathQL.ml avsUtil.ml -EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi +EXTRA_OBJECTS_TO_INSTALL = avs.ml avs.cmi mathQL.ml mathQL.cmi EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/mathql/avs.ml b/helm/ocaml/mathql/avs.ml new file mode 100644 index 000000000..485354037 --- /dev/null +++ b/helm/ocaml/mathql/avs.ml @@ -0,0 +1,85 @@ +(* 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 value = string list (* a linearized attribute value *) + +type path = string list (* the name of an attribute *) + +module type Type = sig + + type group (* an group of attribures *) + + type avs (* a set of attributed values *) + + type peek_t = Empty + | Single of (string * group list) + | Many of (string * group list) + + + val grp_empty : group + + val grp_make : path -> string -> group + + val grp_union : group -> group -> group + + val grp_read : group -> path -> avs + + val grps_make : group list -> group -> group list + + val empty : avs + + val make : string -> group -> avs + + val iter : ('a -> string -> bool -> 'a) -> 'a -> avs -> 'a + + val x_iter : ('a -> string -> group list -> bool -> 'a) -> + 'a -> avs -> 'a + + val x_grp_iter : ('a -> path -> value -> bool -> 'a) -> 'a -> group -> 'a + + val single : avs -> string option + + val sub : avs -> avs -> bool + + val meet : avs -> avs -> bool + + val eq : avs -> avs -> bool + + val union : avs -> avs -> avs (* without attr. distribution *) + + val intersect : avs -> avs -> avs (* without attr. distribution *) + + val diff : avs -> avs -> avs + + val append : avs -> avs -> avs + + val d_union : avs -> avs -> avs (* with attr. distribution *) + + val peek : avs -> peek_t + +end diff --git a/helm/ocaml/mathql/avsUtil.ml b/helm/ocaml/mathql/avsUtil.ml new file mode 100644 index 000000000..65bcadb15 --- /dev/null +++ b/helm/ocaml/mathql/avsUtil.ml @@ -0,0 +1,89 @@ +(* 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 I = MathQL.I + +(* strings ******************************************************************) + +let avs_of_string s = I.make s I.grp_empty + +let string_of_avs r = + match I.peek r with + | I.Single (s, _) -> Some s + | _ -> None + +(* boolean constants *******************************************************) + +let bool_of_avs r = r <> I.empty + +let avs_of_bool = function + | true -> I.make "" I.grp_empty + | false -> I.empty + +let val_false = avs_of_bool false + +let val_true = avs_of_bool true + +(* iterators ****************************************************************) + +let grp_iter f al = + List.fold_left (fun s a -> I.grp_union s (f a)) I.grp_empty al + +let grp_iter2 f al bl = + List.fold_left2 (fun s a b -> I.grp_union s (f a b)) I.grp_empty al bl + +let iter f al = List.fold_left (fun s a -> I.union s (f a)) I.empty al + +let append_iter f al = List.fold_left (fun s a -> I.append (f a) s) I.empty al + +(* other ********************************************************************) + +let grp_make_x p vl = grp_iter (I.grp_make p) vl + +let x_grp_make_x p rs = + let aux g s _ = I.grp_make p s in + I.iter aux I.grp_empty rs + +let make_x s gl = iter (I.make s) gl + +let count v = I.iter (fun n _ _ -> succ n) 0 v + +let subj v = iter (fun s -> I.make s I.grp_empty) v + +(* numeric operations *******************************************************) + +exception NumberError of MathQL.result + +let avs_of_int i = I.make (string_of_int i) I.grp_empty + +let int_of_avs r = + try match (I.peek r) with + | I.Empty + | I.Many _ -> raise (Failure "int_of_string") + | I.Single (s, _) -> MQueryUtil.int_of_string s + with Failure "int_of_string" -> raise (NumberError r) diff --git a/helm/ocaml/mathql/avsUtil.mli b/helm/ocaml/mathql/avsUtil.mli new file mode 100644 index 000000000..ac8888c17 --- /dev/null +++ b/helm/ocaml/mathql/avsUtil.mli @@ -0,0 +1,64 @@ +(* 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 + *) + +exception NumberError of MathQL.result + +val val_true : MathQL.result + +val val_false : MathQL.result + +val grp_make_x : MathQL.path -> MathQL.value -> MathQL.group + +val x_grp_make_x : MathQL.path -> MathQL.result -> MathQL.group + +val grp_iter : ('a -> MathQL.group) -> 'a list -> MathQL.group + +val grp_iter2 : ('a -> 'b -> MathQL.group) -> + 'a list -> 'b list -> MathQL.group + +val make_x : string -> MathQL.group list -> MathQL.result + +val iter : ('a -> MathQL.result) -> 'a list -> MathQL.result + +val append_iter : ('a -> MathQL.result) -> 'a list -> MathQL.result + +val count : MathQL.result -> int + +val avs_of_bool : bool -> MathQL.result + +val bool_of_avs : MathQL.result -> bool + +val avs_of_int : int -> MathQL.result + +val int_of_avs : MathQL.result -> int + +val subj : MathQL.value -> MathQL.result + +val avs_of_string : string -> MathQL.result + +val string_of_avs : MathQL.result -> string option diff --git a/helm/ocaml/mathql/listAvs.ml b/helm/ocaml/mathql/listAvs.ml new file mode 100644 index 000000000..e25fc61c7 --- /dev/null +++ b/helm/ocaml/mathql/listAvs.ml @@ -0,0 +1,189 @@ +(* 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 path = Avs.path (* the name of an attribute *) + +type value = Avs.value (* the value of an attribute *) + +type attribute = path * value (* an attribute *) + +type group = attribute list (* a group of attributes *) + +type attribute_set = group list (* the attributes of an URI *) + +type av = string * attribute_set (* an attributed URI *) + +type avs = av list (* the query result *) + +type peek_t = Empty + | Single of (string * group list) + | Many of (string * group list) + + +(* constructors *************************************************************) + +let grp_empty = [] + +let grp_make p v = [(p, [v])] + +let empty = grp_empty + +let make s = function + | [] -> [(s, [])] + | g -> [(s, [g])] + +(* projections **************************************************************) + +let subj v = List.rev (List.rev_map (fun x -> (x, [])) v) + +let grp_read g p = subj (List.assoc p g) + +let single = function + | [s, _] -> Some s + | _ -> None + +(* iterators ****************************************************************) + +let rec iter f a = function + | [] -> a + | [s, _] -> f a s false + | (s, _) :: v -> iter f (f a s true) v + +let rec x_iter f a = function + | [] -> a + | [s, gl] -> f a s gl false + | (s, gl) :: v -> x_iter f (f a s gl true) v + +let rec x_grp_iter f a g = x_iter f a g + +(* tests ********************************************************************) + +let rec sub v1 v2 = + match (v1, v2) with + | [], _ -> true + | _, [] -> false + | (h1, _) :: _, (h2, _) :: _ when h1 < h2 -> false + | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> sub v1 t2 + | _ :: t1, _ :: t2 -> sub t1 t2 + +let rec meet v1 v2 = + match v1, v2 with + | [], _ + | _, [] -> false + | (h1, _) :: t1, (h2, _) :: _ when h1 < h2 -> meet t1 v2 + | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> meet v1 t2 + | _, _ -> true + +let rec eq v1 v2 = + match v1, v2 with + | [], [] -> true + | (h1, _) :: t1, (h2, _) :: t2 when h1 = h2 -> eq t1 t2 + | _, _ -> false + +(* union ********************************************************************) + +let rec set_union v1 v2 = + match v1, v2 with + | [], v -> v + | v, [] -> v + | h1 :: t1, h2 :: t2 when h1 < h2 -> h1 :: set_union t1 v2 + | h1 :: t1, h2 :: t2 when h1 > h2 -> h2 :: set_union v1 t2 + | h1 :: t1, _ :: t2 -> h1 :: set_union t1 t2 + +let set_iter f al = List.fold_left (fun s a -> set_union (f a) s) [] al + +let grps_make l g = set_union l [g] + +let rec union s1 s2 = + match s1, s2 with + | [], s -> s + | s, [] -> s + | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 -> + (r1, g1) :: union t1 s2 + | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 -> + (r2, g2) :: union s1 t2 + | (r1, g1) :: t1, (_, g2) :: t2 -> + (r1, set_union g1 g2) :: union t1 t2 + +let grp_union = union + +let prod g1 g2 = + let aux a = set_iter (fun h -> [union a h]) g2 in + set_iter aux g1 + +let rec d_union s1 s2 = + match s1, s2 with + | [], s -> s + | s, [] -> s + | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 -> + (r1, g1) :: d_union t1 s2 + | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 -> + (r2, g2) :: d_union s1 t2 + | (r1, g1) :: t1, (_, g2) :: t2 -> + (r1, prod g1 g2) :: d_union t1 t2 + +(* intersect ****************************************************************) + +let rec set_intersect v1 v2 = + match v1, v2 with + | [], v -> [] + | v, [] -> [] + | h1 :: t1, h2 :: _ when h1 < h2 -> set_intersect t1 v2 + | h1 :: _, h2 :: t2 when h1 > h2 -> set_intersect v1 t2 + | h1 :: t1, _ :: t2 -> h1 :: set_intersect t1 t2 + +let rec intersect s1 s2 = + match s1, s2 with + | [], s -> [] + | s, [] -> [] + | (r1, _) :: t1, (r2, _) :: _ when r1 < r2 -> intersect t1 s2 + | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> intersect s1 t2 + | (r1, g1) :: t1, (_, g2) :: t2 -> + (r1, set_intersect g1 g2) :: intersect t1 t2 + +(* diff *********************************************************************) + +let rec diff s1 s2 = + match s1, s2 with + | [], _ -> [] + | s, [] -> s + | (r1, g1) :: t1 , (r2, _) ::_ when r1 < r2 -> + (r1, g1) :: (diff t1 s2) + | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> diff s1 t2 + | _ :: t1, _ :: t2 -> diff t1 t2 + +(* concatenation ************************************************************) + +let append v1 v2 = v1 @ v2 + +(* peeking ******************************************************************) + +let peek = function + | [] -> Empty + | [s, gl] -> Single (s, gl) + | (s, gl) :: _ -> Many (s, gl) diff --git a/helm/ocaml/mathql/listAvs.mli b/helm/ocaml/mathql/listAvs.mli new file mode 100644 index 000000000..af387928c --- /dev/null +++ b/helm/ocaml/mathql/listAvs.mli @@ -0,0 +1 @@ +include Avs.Type diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 8ba562ab2..b76bd4ed5 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -28,22 +28,15 @@ (* output data structures ***************************************************) -type path = string list (* the name of an attribute *) +module I : Avs.Type = ListAvs -type value = string list (* the value of an attribute *) +type value = Avs.value (* a linearized attribute value *) -type attribute = path * value (* an attribute *) +type path = Avs.path (* the name of an attribute *) -type attribute_group = attribute list (* a group of attributes *) - -type attribute_set = attribute_group list (* the attributes of an URI *) - -type resource = string * attribute_set (* an attributed URI *) - -type resource_set = resource list (* the query result *) - -type result = resource_set +type group = I.group (* an group of attribures *) +type result = I.avs (* the query result *) (* input data structures ****************************************************) @@ -74,7 +67,7 @@ type source = bool type gen = GenFJoin (* full union - with attr handling *) | GenFMeet (* full intersection - with attr handling *) -type query = Const of result +type query = Const of (string * (path * query) list list) list | SVar of svar | AVar of avar | Dot of avar * path diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index e56a744cd..fd349c8ea 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -44,20 +44,19 @@ let lamp xl = M.Fun (["and"], [], xl) let locate s = let query = - M.Property true M.RefineExact ["objectName"] [] [] [] [] - false (const s) + M.Property (true, M.RefineExact, ["objectName"], [], [], [], [], + false, (const s)) in stat query let unreferred target_pattern source_pattern = let query = diff ( - M.Property false M.RefineExact [] [] [] [] [] - true (const target_pattern) + M.Property (false, M.RefineExact, [], [], [], [], [], + true, (const target_pattern)) ) ( - M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] [] - true (const source_pattern) - + M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"], + [], [], [], true, (const source_pattern)) ) in stat query @@ -91,13 +90,13 @@ let compose cl = con "h:depth" (List.map U.string_of_depth d) in let property_must n c = - M.Property true M.RefineExact [n] [] - (cons false c) [] [] false (const "") + M.Property (true, M.RefineExact, [n], [], + (cons false c), [], [], false, (const "")) in let property_only n cl = let cll = List.map (cons true) cl in - M.Property false M.RefineExact [n] [] - ! univ cll [] false (M.AVar "obj") + M.Property (false, M.RefineExact, [n], [], + ! univ, cll, [], false, (M.AVar "obj")) in let rec aux = function | [] -> () @@ -105,17 +104,17 @@ let compose cl = only := true; let l = List.map U.string_of_position l in univ := [(false, ["h:position"], set_val l)]; aux tail - | T.MustObj r p d :: tail -> + | T.MustObj (r, p, d) :: tail -> must := property_must "refObj" (r, [], p, d) :: ! must; aux tail - | T.MustSort s p d :: tail -> + | T.MustSort (s, p, d) :: tail -> must := property_must "refSort" ([], s, p, d) :: ! must; aux tail - | T.MustRel p d :: tail -> + | T.MustRel (p, d) :: tail -> must := property_must "refRel" ([], [], p, d) :: ! must; aux tail - | T.OnlyObj r p d :: tail -> + | T.OnlyObj (r, p, d) :: tail -> onlyobj := (r, [], p, d) :: ! onlyobj; aux tail - | T.OnlySort s p d :: tail -> + | T.OnlySort (s, p, d) :: tail -> onlysort := ([], s, p, d) :: ! onlysort; aux tail - | T.OnlyRel p d :: tail -> + | T.OnlyRel (p, d) :: tail -> onlyrel := ([], [], p, d) :: ! onlyrel; aux tail in let rec iter f g = function @@ -128,7 +127,8 @@ let compose cl = aux cl; let must_query = if ! must = [] then - M.Property false M.RefineExact [] [] [] [] [] true (const ".*") + M.Property (false, M.RefineExact, [], [], + [], [], [], true, (const ".*")) else intersect ! must in diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 4bad2ad26..739f2f90e 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -9,23 +9,19 @@ 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 +mQILib.cmo: mQIConn.cmi mQILib.cmi +mQILib.cmx: mQIConn.cmx mQILib.cmi +mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIProperty.cmi +mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIProperty.cmi mQueryTParser.cmo: mQILib.cmi mQueryTParser.cmi mQueryTParser.cmx: mQILib.cmx mQueryTParser.cmi mQueryTLexer.cmo: mQueryTParser.cmi mQueryTLexer.cmx: mQueryTParser.cmx mQueryIO.cmo: mQILib.cmi mQueryTLexer.cmo mQueryTParser.cmi 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 -mQueryStandard.cmo: mQIConn.cmi mQILib.cmi mQIUtil.cmi mQueryStandard.cmi -mQueryStandard.cmx: mQIConn.cmx mQILib.cmx mQIUtil.cmx mQueryStandard.cmi +mQueryInterpreter.cmo: mQIConn.cmi mQILib.cmi mQIProperty.cmi mQueryIO.cmi \ + mQueryInterpreter.cmi +mQueryInterpreter.cmx: mQIConn.cmx mQILib.cmx mQIProperty.cmx mQueryIO.cmx \ + mQueryInterpreter.cmi +mQueryStandard.cmo: mQIConn.cmi mQILib.cmi mQueryStandard.cmi +mQueryStandard.cmx: mQIConn.cmx mQILib.cmx mQueryStandard.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index 48859300b..555f16215 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -5,7 +5,7 @@ REQUIRES = postgres helm-mathql PREDICATES = PRE_IFILES = mQIPostgres.mli mQIMap.mli mQIConn.mli \ - mQIUtil.mli mQILib.mli mQIProperty.mli + mQILib.mli mQIProperty.mli POST_IFILES = mQueryIO.mli mQueryInterpreter.mli mQueryStandard.mli diff --git a/helm/ocaml/mathql_interpreter/mQILib.ml b/helm/ocaml/mathql_interpreter/mQILib.ml index b22602445..a474857c5 100644 --- a/helm/ocaml/mathql_interpreter/mQILib.ml +++ b/helm/ocaml/mathql_interpreter/mQILib.ml @@ -29,7 +29,6 @@ module M = MathQL module P = MQueryUtil module C = MQIConn -module U = MQIUtil (* external function specification ******************************************) diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index b32b519a1..357809a74 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -27,9 +27,10 @@ *) module M = MathQL +module I = M.I +module U = AvsUtil module P = MQIPostgres module C = MQIConn -module U = MQIUtil module A = MQIMap let not_supported s = @@ -65,15 +66,22 @@ let pg_query h table cols ct cfl = | [head] -> f head | head :: tail -> f head ^ sep ^ iter f sep tail in + let avs_iter f sep v = + let aux a s = function + | true -> a ^ (f s) ^ sep + | false -> a ^ (f s) + in + I.iter aux "" v + in let pg_cols = iter (fun x -> x) ", " cols in - let pg_msval v = iter (fun s, _ -> P.quote s) ", " v in + let pg_msval v = avs_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 ^ ")" + let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in + if pat then "(" ^ avs_iter f " or " v ^ ")" + else match I.single v with + | Some s -> col ^ " = " ^ (P.quote s) + | None -> col ^ " in (" ^ pg_msval v ^ ")" else "true" in let pg_cons l = iter pg_con " and " l in @@ -101,15 +109,15 @@ let gx_query h table cols ct cfl = not_supported "Galax" (* Common functions ********************************************************) let pg_result distinct subj el res = - let compose = if distinct then List.map else fun f -> U.mql_iter (fun x -> [f x]) in + let res, compose = + if distinct then List.rev res, U.append_iter else res, U.iter + in let get_name = function (p, None) -> p | (_, Some p) -> p in let names = List.map get_name el in - let mk_grp l = - let grp = U.mql_iter2 (fun p s -> [(p, [s])]) names l in - if grp = [] then [] else [grp] - in - let mk_avs l = - if subj = "" then ("", mk_grp l) else (List.hd l, mk_grp (List.tl l)) + let mk_grp l = U.grp_iter2 I.grp_make names l in + let mk_avs l = + if subj = "" then I.make "" (mk_grp l) + else I.make (List.hd l) (mk_grp (List.tl l)) in compose mk_avs res @@ -139,9 +147,9 @@ let exec h refine mc ct cfl el = if refine <> M.RefineExact then not_supported "exec"; let table = get_table h mc ct cfl el in let rec exec_aux ct = match ct with - | (pat, p, v) :: tail when List.length v > deadline -> - let single s = exec_aux ((pat, p, [s]) :: tail) in - U.mql_iter single v + | (pat, p, v) :: tail when U.count v > deadline -> + let single a s _ = I.union a (exec_aux ((pat, p, I.make s I.grp_empty) :: tail)) in + I.iter single U.val_false v | _ -> exec_single h mc ct cfl el table in exec_aux ct @@ -155,3 +163,4 @@ let pg_name h s = | _ -> "" let get_id b = if b then ["B"] else ["F"] + diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml deleted file mode 100644 index 8d5782dea..000000000 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ /dev/null @@ -1,140 +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 - *) - -(* boolean constants *******************************************************) - -let mql_false = [] - -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 - -let rec set_meet v1 v2 = - match v1, v2 with - | [], _ - | _, [] -> 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 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 - | [], v -> v - | v, [] -> v - | h1 :: t1, h2 :: t2 when h1 < h2 -> h1 :: set_union t1 v2 - | h1 :: t1, h2 :: t2 when h1 > h2 -> h2 :: set_union v1 t2 - | h1 :: t1, _ :: t2 -> h1 :: set_union t1 t2 - -let rec set_intersect v1 v2 = - match v1, v2 with - | [], v -> [] - | v, [] -> [] - | h1 :: t1, h2 :: _ when h1 < h2 -> set_intersect t1 v2 - | h1 :: _, h2 :: t2 when h1 > h2 -> set_intersect v1 t2 - | h1 :: t1, _ :: t2 -> h1 :: set_intersect t1 t2 - -let rec iter f = function - | [] -> [] - | head :: tail -> set_union (f head) (iter f tail) - -(* MathQL specific set operations ******************************************) - -let mql_subj v = List.map (fun s -> (s, [])) v - -let rec mql_union s1 s2 = - match s1, s2 with - | [], s -> s - | s, [] -> s - | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 -> - (r1, g1) :: mql_union t1 s2 - | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 -> - (r2, g2) :: mql_union s1 t2 - | (r1, g1) :: t1, (_, g2) :: t2 -> - (r1, set_union g1 g2) :: mql_union t1 t2 - -let rec mql_iter f = function - | [] -> [] - | head :: tail -> mql_union (f head) (mql_iter f tail) - -let rec mql_iter2 f l1 l2 = match l1, l2 with - | [], [] -> [] - | h1 :: t1, h2 :: t2 -> mql_union (f h1 h2) (mql_iter2 f t1 t2) - | _ -> raise (Invalid_argument "mql_iter2") - -let rec mql_prod g1 g2 = - let mql_prod_aux a = iter (fun h -> [mql_union a h]) g2 in - iter mql_prod_aux g1 - -let rec mql_intersect s1 s2 = - match s1, s2 with - | [], s -> [] - | s, [] -> [] - | (r1, _) :: t1, (r2, _) :: _ when r1 < r2 -> mql_intersect t1 s2 - | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_intersect s1 t2 - | (r1, g1) :: t1, (_, g2) :: t2 -> - (r1, set_intersect g1 g2) :: mql_intersect t1 t2 - -let rec mql_diff s1 s2 = - match s1, s2 with - | [], _ -> [] - | s, [] -> s - | (r1, g1) :: t1 , (r2, _) ::_ when r1 < r2 -> - (r1, g1) :: (mql_diff t1 s2) - | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_diff s1 t2 - | _ :: t1, _ :: t2 -> mql_diff t1 t2 - -(* logic operations ********************************************************) - -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 *******************************************************) - -exception NumberError of MathQL.result - -let int_of_set r = - try match r with - | [s, _] -> MQueryUtil.int_of_string s - | _ -> raise (Failure "int_of_string") - with Failure "int_of_string" -> raise (NumberError r) diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli deleted file mode 100644 index f6063ad07..000000000 --- a/helm/ocaml/mathql_interpreter/mQIUtil.mli +++ /dev/null @@ -1,65 +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 mql_true : MathQL.result - -val mql_false : MathQL.result - -val set_sub : MathQL.result -> MathQL.result -> MathQL.result - -val set_meet : MathQL.result -> MathQL.result -> MathQL.result - -val set_eq : MathQL.result -> MathQL.result -> MathQL.result - -val set_union : 'a list -> 'a list -> 'a list - -val mql_subj : MathQL.value -> MathQL.result - -val mql_union : ('a * 'b list) list -> ('a * 'b list) list -> - ('a * 'b list) list - -val mql_prod : MathQL.attribute_set -> MathQL.attribute_set -> - MathQL.attribute_set - -val mql_intersect : MathQL.result -> MathQL.result -> MathQL.result - -val mql_diff : MathQL.result -> MathQL.result -> MathQL.result - -val iter : ('a -> 'b list) -> 'a list -> 'b list - -val mql_iter : ('c -> ('a * 'b list) list) -> 'c list -> - ('a * 'b list) list - -val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list -> - 'd list -> ('a * 'b list) list - -val xor : MathQL.result -> MathQL.result -> MathQL.result - -exception NumberError of MathQL.result - -val int_of_set : MathQL.result -> int diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.ml b/helm/ocaml/mathql_interpreter/mQueryIO.ml index 5af9c7b10..14199e513 100644 --- a/helm/ocaml/mathql_interpreter/mQueryIO.ml +++ b/helm/ocaml/mathql_interpreter/mQueryIO.ml @@ -27,6 +27,7 @@ *) module M = MathQL +module I = M.I module P = MQueryUtil module L = MQILib @@ -51,22 +52,37 @@ let txt_str out s = out ("\"" ^ txt_quote s ^ "\"") let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p -let text_of_result out sep x = - let txt_attr = function - | (p, []) -> txt_path out p - | (p, l) -> txt_path out p; out " = "; - P.flat_list out (txt_str out) ", " l +let text_of_result out sep x = + let txt_attr _ p l b = + txt_path out p; + if l <> [] then begin + out " = "; P.flat_list out (txt_str out) ", " l + end; + if b then out ("; " ^ sep) in + let txt_group l = out "{"; I.x_grp_iter txt_attr () l; out "}" in + let txt_res _ s l b = + txt_str out s; + if l <> [] then begin + out " = "; P.flat_list out txt_group ", " l + end; + if b then out "; " + in + I.x_iter txt_res () x; out sep + +let rec xtext_of_groups out l = + let txt_attr (p, x) = txt_path out p; out " = "; text_of_query out "" x in let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in + P.flat_list out txt_group ", " l + +and xtext_of_result out x = let txt_res = function | (s, []) -> txt_str out s - | (s, l) -> txt_str out s; out " attr "; - P.flat_list out txt_group ", " l + | (s, l) -> txt_str out s; out " attr "; xtext_of_groups out l in - let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in - txt_set x + P.flat_list out txt_res "; " x -let rec text_of_query out sep x = +and text_of_query out sep x = let txt_svar sv = out ("$" ^ sv) in let txt_avar av = out ("@" ^ av) in let txt_inv i = if i then out "inverse " in @@ -103,44 +119,41 @@ let rec text_of_query out sep x = | 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.Attr g -> xtext_of_groups out g | M.From av -> txt_avar av and txt_set = function - | M.Fun p pl xl -> + | M.Fun (p, pl, xl) -> let o = {L.out = out; L.path = txt_path; L.query = text_of_query; L.result = text_of_result } in L.fun_txt_out o 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 -> + | M.Const [s, []] -> txt_str out s + | M.Const r -> xtext_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 (Some sv) x y -> out "let "; txt_svar sv; out " = "; - txt_set x; out " in "; txt_set y - | M.Let None x y -> txt_set x; out " ;; "; 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.While k x y -> out "while "; 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 - | M.Gen p [x] -> out "gen "; txt_path out p; out " in "; txt_set x - | M.Gen p l -> out "gen "; txt_path out p; out " {"; - P.flat_list out txt_set ", " l; out "}" + | M.Let (Some sv, x, y) -> out "let "; txt_svar sv; out " = "; + txt_set x; out " in "; txt_set y + | M.Let (None, x, y) -> txt_set x; out " ;; "; 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.While (k, x, y) -> out "while "; 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 + | M.Gen (p, [x]) -> out "gen "; txt_path out p; out " in "; txt_set x + | M.Gen (p, l) -> out "gen "; txt_path out p; out " {"; + P.flat_list out txt_set ", " l; out "}" in txt_set x; out sep diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index b66228581..cc85c7811 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -28,20 +28,21 @@ exception Found +module U = AvsUtil module M = MathQL +module I = M.I module P = MQueryUtil module C = MQIConn -module U = MQIUtil module L = MQILib module F = MQueryIO (* contexts *****************************************************************) -type svar_context = (M.svar * M.resource_set) list +type svar_context = (M.svar * M.result) list -type avar_context = (M.avar * M.resource) list +type avar_context = (M.avar * (string * M.group list)) list -type group_context = (M.avar * M.attribute_group) list +type group_context = (M.avar * M.group) list type context = {svars: svar_context; avars: avar_context; @@ -58,19 +59,21 @@ let execute h x = F.text_of_query (C.log h) "\n" q end in - let proj v = List.map fst v in let rec eval_query c = function - | M.Const r -> c, r - | M.Dot i p -> + | M.Const r -> + let aux2 s g = I.make s (eval_list c g) in + let aux (s, gl) = U.iter (aux2 s) gl in + c, U.iter aux r + | M.Dot (i, p) -> begin - try c, U.mql_subj (List.assoc p (List.assoc i c.groups)) - with Not_found -> warn (M.Dot i p); c, [] + try c, I.grp_read (List.assoc i c.groups) p + with Not_found -> warn (M.Dot (i, p)); c, I.empty end - | M.Ex l y -> + | M.Ex (l, y) -> let rec ex_aux h = function | [] -> let d = {c with groups = h} in - if snd (eval_query d y) = U.mql_false then () else raise Found + if snd (eval_query d y) = U.val_false then () else raise Found | i :: tail -> begin try @@ -83,55 +86,58 @@ let execute h x = with Not_found -> () end in - begin try ex_aux [] l; c, U.mql_false with Found -> c, U.mql_true end + begin try ex_aux [] l; c, U.val_false with Found -> c, U.val_true end | M.SVar i -> begin try c, List.assoc i c.svars - with Not_found -> warn (M.SVar i); c, [] + with Not_found -> warn (M.SVar i); c, I.empty end | M.AVar i -> begin - try c, [List.assoc i c.avars] - with Not_found -> warn (M.AVar i); c, [] + try + let s, gl = List.assoc i c.avars in + c, U.make_x s gl + with Not_found -> warn (M.AVar i); c, I.empty end - | M.Let (Some i) x1 x2 -> + | M.Let (Some i, x1, x2) -> let d, r = eval_query c x1 in let d = {d with svars = P.add_assoc (i, r) d.svars} in eval_query d x2 - | M.Let None x1 x2 -> + | M.Let (None, x1, x2) -> let d, r = eval_query c x1 in eval_query d x2 - | M.For k i x1 x2 -> + | M.For (k, i, x1, x2) -> let f = match k with - | M.GenFJoin -> U.mql_union - | M.GenFMeet -> U.mql_intersect + | M.GenFJoin -> I.union + | M.GenFMeet -> I.intersect in - let rec for_aux (d, r) = match r with - | [] -> d, [] - | h :: t -> - let d = {d with avars = P.add_assoc (i, h) d.avars} in - let d, r = eval_query d x2 in - let d, s = for_aux (d, t) in - d, f r s - in - for_aux (eval_query c x1) - | M.While k x1 x2 -> + let for_aux (d, r) s gl _ = + let d = {d with avars = P.add_assoc (i, (s, gl)) d.avars} in + let d, s = eval_query d x2 in + d, f r s + in + let d, r = eval_query c x1 in + I.x_iter for_aux (d, I.empty) r + | M.While (k, x1, x2) -> let f = match k with - | M.GenFJoin -> U.mql_union - | M.GenFMeet -> U.mql_intersect + | M.GenFJoin -> I.union + | M.GenFMeet -> I.intersect in let rec while_aux (d, r) = let d, b = eval_query d x1 in - if b = U.mql_false then d, r else + if b = U.val_false then d, r else let d, s = eval_query d x2 in while_aux (d, f r s) in - while_aux (c, U.mql_false) - | M.Add b z x -> - let f = if b then U.mql_prod else U.set_union in - let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in + while_aux (c, U.val_false) + | M.Add (b, z, x) -> + let f = if b then I.d_union else I.union in + let agl = eval_grp c z in + let aux r sj gl _ = + I.append (f (U.make_x sj gl) (U.make_x sj agl)) r + in let _, r = eval_query c x in - c, List.fold_right g r [] - | M.Property q0 q1 q2 mc ct cfl el pat y -> + c, I.x_iter aux I.empty r + | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) -> let _, r = eval_query c y in let subj, mct = if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r) @@ -147,32 +153,32 @@ let execute h x = let r = MQIProperty.exec h q1 subj cons_true cons_false exp in let s = P.stop_time t in if C.set h C.Stat then - C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r)); + C.log h (Printf.sprintf "Property: %s,%i\n" s (U.count r)); c, r - | M.Select i x y -> - let rec select_aux (d, r) = match r with - | [] -> d, [] - | h :: t -> - let d = {d with avars = P.add_assoc (i, h) d.avars} in - let d, r = eval_query d y in - let d, s = select_aux (d, t) in - if r = U.mql_false then d, s else d, (h :: s) + | M.Select (i, x, y) -> + let aux (d, r) sj gl _ = + let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in + let d, s = eval_query d y in + if s = U.val_false then d, r else d, (I.append (U.make_x sj gl) r) in - select_aux (eval_query c x) - | M.Fun p pl xl -> + let d, r = eval_query c x in + I.x_iter aux (d, I.empty) r + | M.Fun (p, pl, xl) -> let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec p pl xl - | M.Gen p xl -> + | M.Gen (p, xl) -> let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in eval_query c (L.gen_eval e p xl) + and eval_list c l = + let aux (p, y) = + let _, r = eval_query c y in + U.x_grp_make_x p r + in + U.grp_iter aux l and eval_grp c = function | M.Attr gs -> - let attr_aux g (p, y) = - let _, r = eval_query c y in - U.mql_union g [p, proj r] - in - let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in + let attr_auxs s l = I.grps_make s (eval_list c l) in List.fold_left attr_auxs [] gs | M.From i -> try snd (List.assoc i c.avars) diff --git a/helm/ocaml/mathql_interpreter/mQueryStandard.ml b/helm/ocaml/mathql_interpreter/mQueryStandard.ml index 4bd251b14..858c28fa0 100644 --- a/helm/ocaml/mathql_interpreter/mQueryStandard.ml +++ b/helm/ocaml/mathql_interpreter/mQueryStandard.ml @@ -26,18 +26,24 @@ (* AUTOR: Ferruccio Guidi *) +module U = AvsUtil +module M = MathQL +module I = M.I module P = MQueryUtil module C = MQIConn -module U = MQIUtil module L = MQILib let init = () +let test f v1 v2 = U.avs_of_bool (f v1 v2) + +let num_test f v1 v2 = U.avs_of_bool (f (U.int_of_avs v1) (U.int_of_avs v2)) + (* FALSE / EMPTY ************************************************************) let false_fun b = let s = if b then "false" else "empty" in - L.fun_arity0 [] s U.mql_false + L.fun_arity0 [] s U.val_false let _ = L.fun_register ["empty"] (false_fun false) @@ -45,14 +51,14 @@ let _ = L.fun_register ["false"] (false_fun true) (* TRUE *********************************************************************) -let true_fun = L.fun_arity0 [] "true" U.mql_true +let true_fun = L.fun_arity0 [] "true" U.val_true let _ = L.fun_register ["true"] true_fun (* NOT **********************************************************************) let not_fun = - let aux r = if r = U.mql_false then U.mql_true else U.mql_false in + let aux r = if r = U.val_false then U.val_true else U.val_false in L.fun_arity1 [] "!" aux let _ = L.fun_register ["not"] not_fun @@ -60,7 +66,7 @@ let _ = L.fun_register ["not"] not_fun (* COUNT ********************************************************************) let count_fun = - let aux r = [string_of_int (List.length r), []] in + let aux r = U.avs_of_int (U.count r) in L.fun_arity1 [] "#" aux let _ = L.fun_register ["count"] count_fun @@ -68,58 +74,61 @@ let _ = L.fun_register ["count"] count_fun (* PEEK *********************************************************************) let peek_fun = - let aux = function [] -> [] | hd :: _ -> [hd] in + let aux r = + match (I.peek r) with + | I.Empty + | I.Single _ -> r + | I.Many (s, gl) -> U.make_x s gl + in L.fun_arity1 [] "peek" aux let _ = L.fun_register ["peek"] peek_fun (* DIFF *********************************************************************) -let diff_fun = L.fun_arity2 [] "diff" U.mql_diff +let diff_fun = L.fun_arity2 [] "diff" I.diff let _ = L.fun_register ["diff"] diff_fun (* XOR **********************************************************************) -let xor_fun = L.fun_arity2 [] "xor" U.xor +let xor_fun = + let aux v1 v2 = + let b = v1 <> U.val_false in + if b && v2 <> U.val_false then U.val_false else + if b then v1 else v2 + in + L.fun_arity2 [] "xor" aux let _ = L.fun_register ["xor"] xor_fun (* SUB **********************************************************************) -let sub_fun = L.fun_arity2 [] "sub" U.set_sub +let sub_fun = L.fun_arity2 [] "sub" (test I.sub) let _ = L.fun_register ["sub"] sub_fun (* MEET *********************************************************************) -let meet_fun = L.fun_arity2 [] "meet" U.set_meet +let meet_fun = L.fun_arity2 [] "meet" (test I.meet) let _ = L.fun_register ["meet"] meet_fun (* EQ ***********************************************************************) -let eq_fun = L.fun_arity2 [] "==" U.set_eq +let eq_fun = L.fun_arity2 [] "==" (test I.eq) let _ = L.fun_register ["eq"] eq_fun (* LE ***********************************************************************) -let le_fun = - let le v1 v2 = - if U.int_of_set v1 <= U.int_of_set v2 then U.mql_true else U.mql_false - in - L.fun_arity2 [] "<=" le +let le_fun = L.fun_arity2 [] "<=" (num_test (<=)) let _ = L.fun_register ["le"] le_fun (* LT ***********************************************************************) -let lt_fun = - let lt v1 v2 = - if U.int_of_set v1 < U.int_of_set v2 then U.mql_true else U.mql_false - in - L.fun_arity2 [] "<" lt +let lt_fun = L.fun_arity2 [] "<" (num_test (<)) let _ = L.fun_register ["lt"] lt_fun @@ -133,7 +142,7 @@ let stat_fun = let t = P.start_time () in let r = (e.L.eval x) in let s = P.stop_time t in - o.L.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); + o.L.out (Printf.sprintf "Stat: %s,%i\n" s (U.count r)); r | _ -> assert false in @@ -190,7 +199,7 @@ let render_fun = let rs = ref "" in let out s = rs := ! rs ^ s in o.L.result out " " (e.L.eval x); - [! rs, []] + I.make ! rs I.grp_empty | _ -> assert false in let txt_out o _ = function @@ -208,12 +217,12 @@ let read_fun = let arity_s = L.Const 1 in let body e o i _ = function | [x] -> - let aux av = - let ich = open_in (fst av) in + let aux avs s _ = + let ich = open_in s in let r = i.L.result_in (Lexing.from_channel ich) in - close_in ich; r + close_in ich; I.union avs r in - U.mql_iter aux (e.L.eval x) + I.iter aux I.empty (e.L.eval x) | _ -> assert false in let txt_out o _ = function @@ -227,16 +236,17 @@ let _ = L.fun_register ["read"] read_fun (* ALIGN ********************************************************************) let align_fun = - let aux l (v, g) = + let aux2 l v = let c = String.length v in - if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g] - in + if c < l then String.make (l - c) ' ' ^ v else v + in + let aux l r s gl _ = I.append r (U.make_x (aux2 l s) gl) in let arity_p = L.Const 0 in let arity_s = L.Const 2 in let body e _ _ _ = function | [y; x] -> - let l = U.int_of_set (e.L.eval y) in - U.mql_iter (aux l) (e.L.eval x) + let l = U.int_of_avs (e.L.eval y) in + I.x_iter (aux l) I.empty (e.L.eval x) | _ -> assert false in let txt_out o _ = function @@ -256,7 +266,7 @@ let if_fun = let arity_s = L.Const 3 in let body e _ _ _ = function | [y; x1; x2] -> - if (e.L.eval y) = U.mql_false then (e.L.eval x2) else (e.L.eval x1) + if U.bool_of_avs (e.L.eval y) then (e.L.eval x1) else (e.L.eval x2) | _ -> assert false in let txt_out o _ = function @@ -276,7 +286,7 @@ let intersect_fun = let rec iter f = function | [] -> assert false | [head] -> f head - | head :: tail -> U.mql_intersect (f head) (iter f tail) + | head :: tail -> I.intersect (f head) (iter f tail) in let arity_p = L.Const 0 in let arity_s = L.Positive in @@ -295,7 +305,7 @@ let _ = L.fun_register ["intersect"] intersect_fun let union_fun = let arity_p = L.Const 0 in let arity_s = L.Any in - let body e _ _ _ xl = U.mql_iter e.L.eval xl in + let body e _ _ _ xl = U.iter e.L.eval xl in let txt_out o _ xl = let o = L.std o in L.out_txt_ o [] xl in {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out} @@ -306,10 +316,10 @@ let _ = L.fun_register ["union"] union_fun let or_fun = let rec iter f = function - | [] -> U.mql_false + | [] -> U.val_false | head :: tail -> let r1 = f head in - if r1 = U.mql_false then (iter f tail) else r1 + if U.bool_of_avs r1 then r1 else (iter f tail) in let arity_p = L.Const 0 in let arity_s = L.Any in @@ -326,10 +336,10 @@ let _ = L.fun_register ["or"] or_fun let and_fun = let rec iter f = function - | [] -> U.mql_true + | [] -> U.val_true | [head] -> f head | head :: tail -> - if f head = U.mql_false then U.mql_false else iter f tail + if U.bool_of_avs (f head) then iter f tail else U.val_false in let arity_p = L.Const 0 in let arity_s = L.Any in @@ -345,14 +355,15 @@ let _ = L.fun_register ["and"] and_fun (* PROJ *********************************************************************) let proj_fun = - let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in - let proj_group p a = U.mql_iter (proj_group_aux p) a in - let proj_set p (_, g) = U.mql_iter (proj_group p) (List.rev g) in + let aux2 p a q v _ = if p = q then I.union a (U.subj v) else a in + let aux p a _ gl _ = + I.union a (U.iter (I.x_grp_iter (aux2 p) I.empty) gl) + in let arity_p = L.Const 1 in let arity_s = L.Const 1 in let body e _ _ pl xl = match pl, xl with - | [p], [x] -> U.mql_iter (proj_set p) (e.L.eval x) + | [p], [x] -> I.x_iter (aux p) I.empty (e.L.eval x) | _ -> assert false in let txt_out o pl xl = @@ -368,15 +379,15 @@ let _ = L.fun_register ["proj"] proj_fun (* KEEP *********************************************************************) -let keep_fun b = - let proj (r, _) = (r, []) in - let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in - let keep_grp l a = List.fold_right (keep_path l) a [] in - let keep_set l a g = - let kg = keep_grp l a in - if kg = [] then g else kg :: g +let keep_fun b = + let aux2 s l a q v _ = + if List.mem q l = b then a else I.union a (I.make s (U.grp_make_x q v)) in - let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in + let aux l a s gl _ = + I.append a ( + if l = [] then I.make s I.grp_empty else + U.iter (I.x_grp_iter (aux2 s l) I.empty) gl) + in let txt_allbut o = if b then o.L.s_out "allbut " in let txt_path_list o l = P.flat_list o.L.s_out o.L.s_path ", " l in let arity_p = L.Any in @@ -384,8 +395,7 @@ let keep_fun b = let body e _ _ pl xl = match b, pl, xl with | true, [], [x] -> e.L.eval x - | false, [], [x] -> List.map proj (e.L.eval x) - | _, l, [x] -> List.map (keep_av l) (e.L.eval x) + | _, l, [x] -> I.x_iter (aux l) I.empty (e.L.eval x) | _ -> assert false in let txt_out o pl xl = diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly index 4945edfc0..54f8f837c 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly +++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly @@ -28,15 +28,17 @@ %{ module M = MathQL + module I = M.I + module U = AvsUtil module L = MQILib let make_fun p pl xl = L.fun_arity p (List.length pl) (List.length xl); - M.Fun p pl xl + M.Fun (p, pl, xl) let make_gen p xl = L.gen_arity p (List.length xl); - M.Gen p xl + M.Gen (p, xl) let analyze x = let rec join l1 l2 = match l1, l2 with @@ -51,26 +53,27 @@ | head :: tail -> join (f head) (iter f tail) in let rec an_set = function - | M.Const _ + | M.Const x -> iter fv x | 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.While _ x y -> iter an_set [x; y] - | M.Fun _ _ l -> iter an_set l - | M.Gen _ l -> iter an_set l - | M.Add _ g x -> join (an_grp g) (an_set x) - | M.Property _ _ _ _ c d _ _ x -> + | M.Ex _ -> [] + | M.Dot (rv, _) -> [rv] + | M.Let (_, x, y) + | M.Select (_, x, y) + | M.For (_, _, x, y) -> iter an_set [x; y] + | M.While (_, x, y) -> iter an_set [x; y] + | M.Fun (_, _, l) -> iter an_set l + | M.Gen (_, l) -> iter an_set l + | M.Add (_, g, x) -> join (an_grp g) (an_set x) + | M.Property (_, _, _, _, c, d, _, _, x) -> 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_set v and an_grp = function | M.Attr g -> iter (iter fg) g - | M.From _ -> [] + | M.From _ -> [] + and fv (_, g) = iter (iter fg) g in an_set x @@ -182,17 +185,6 @@ | PAT { true } | { false } ; - ass: - | set_exp AS path { ($3, $1) } - ; - asss: - | ass CM asss { $1 :: $3 } - | ass { [$1] } - ; - assg: - | asss SC assg { $1 :: $3 } - | asss { [$1] } - ; distr: | DISTR { true } | { false } @@ -213,8 +205,8 @@ | { "text" } ; grp_exp: - | assg { M.Attr $1 } - | avar { M.From $1 } + | x_groups { M.Attr $1 } + | avar { M.From $1 } ; set_exp: | STAT set_exp { make_fun ["stat"] [] [$2] } @@ -247,20 +239,20 @@ | IF set_exp THEN set_exp ELSE set_exp { make_fun ["if"] [] [$2; $4; $6] } | STR { M.Const [$1, []] } - | LB resources RB { M.Const $2 } - | avar FS path { M.Dot $1 $3 } + | LB x_resources RB { M.Const $2 } + | avar FS path { M.Dot ($1, $3) } | LP set_exp RP { $2 } - | EX set_exp { M.Ex (analyze $2) $2 } + | EX set_exp { M.Ex (analyze $2, $2) } | svar { M.SVar $1 } | avar { M.AVar $1 } - | LET svar BE set_exp IN set_exp { M.Let (Some $2) $4 $6 } - | set_exp SEQ set_exp { M.Let None $1 $3 } - | FOR avar IN set_exp gen_op { M.For (fst $5) $2 $4 (snd $5) } - | WHILE set_exp gen_op { M.While (fst $3) $2 (snd $3) } - | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 } + | LET svar BE set_exp IN set_exp { M.Let (Some $2, $4, $6) } + | set_exp SEQ set_exp { M.Let (None, $1, $3) } + | FOR avar IN set_exp gen_op { M.For (fst $5, $2, $4, snd $5) } + | WHILE set_exp gen_op { M.While (fst $3, $2, snd $3) } + | ADD distr grp_exp IN set_exp { M.Add ($2, $3, $5) } | PROP qualif mainc istrue isfalse attrc OF pattern set_exp - { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 } - | SELECT avar FROM set_exp WHERE set_exp { M.Select $2 $4 $6 } + { M.Property (f $2, s $2, t $2, $3, $4, $5, $6, $8, $9) } + | SELECT avar FROM set_exp WHERE set_exp { M.Select ($2, $4, $6) } | GEN path LC sets RC { make_gen $2 $4 } | GEN path IN set_exp { make_gen $2 [$4] } ; @@ -277,13 +269,39 @@ | set_exp error { $1 } | EOF { raise End_of_file } ; + + x_attr: + | path BE set_exp { ($1, $3) } + | path { ($1, make_fun ["empty"] [] []) } + ; + x_attrs: + | x_attr SC x_attrs { $1 :: $3 } + | x_attr { [$1] } + ; + x_group: + LC x_attrs RC { $2 } + ; + x_groups: + | x_group CM x_groups { $1 :: $3 } + | x_group { [$1] } + ; + x_resource: + | STR ATTR x_groups { ($1, $3) } + | STR { ($1, []) } + ; + x_resources: + | x_resource SC x_resources { $1 :: $3 } + | x_resource { [$1] } + | { [] } + ; + attr: - | path BE strs { $1, $3 } - | path { $1, [] } + | path BE strs { U.grp_make_x $1 $3 } + | path { U.grp_make_x $1 [] } ; attrs: - | attr SC attrs { $1 :: $3 } - | attr { [$1] } + | attr SC attrs { I.grp_union $1 $3 } + | attr { $1 } ; group: LC attrs RC { $2 } @@ -293,13 +311,13 @@ | group { [$1] } ; resource: - | STR ATTR groups { ($1, $3) } - | STR { ($1, []) } + | STR ATTR groups { U.make_x $1 $3 } + | STR { U.make_x $1 [] } ; resources: - | resource SC resources { $1 :: $3 } - | resource { [$1] } - | { [] } + | resource SC resources { I.union $1 $3 } + | resource { $1 } + | { U.val_false } ; result: | resources { $1 }