From: Ferruccio Guidi Date: Tue, 20 May 2003 14:52:11 +0000 (+0000) Subject: MathQL query generator: new interface X-Git-Tag: submitted~42 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48b9bb5e9504aba97cff28a9d7e2797feb42972e;p=helm.git MathQL query generator: new interface --- diff --git a/helm/ocaml/mathql_interpreter/mQIExecute.ml b/helm/ocaml/mathql_interpreter/mQIExecute.ml new file mode 100644 index 000000000..7bd7bd8b9 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIExecute.ml @@ -0,0 +1,248 @@ +(* 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/. + *) + +(* modifiers ***************************************************************) + +let galax_char = 'G' + +let stat_char = 'S' + +let warn_char = 'W' + +(* contexts *****************************************************************) + +type svar_context = (MathQL.svar * MathQL.resource_set) list + +type avar_context = (MathQL.avar * MathQL.resource) list + +type group_context = (MathQL.avar * MathQL.attribute_group) list + +type vvar_context = (MathQL.vvar * MathQL.value) list + +type context = {svars: svar_context; + avars: avar_context; + groups: group_context; (* auxiliary context *) + vvars: vvar_context + } + +(* execute *****************************************************************) + +exception Found + +module M = MathQL +module P = MQueryUtil +module U = MQIUtil + +let execute out m x = + let warn q = + if String.contains m warn_char then + begin + out "MQIExecute: waring: reference to undefined variables: "; + P.text_of_query out 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 + | 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) + | 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 + | i :: tail -> + begin + try + let (_, a) = List.assoc i c.avars in + let rec add_group = function + | [] -> () + | g :: t -> ex_aux ((i, g) :: h) tail; add_group t + in + add_group a + with Not_found -> () + end + in + (try ex_aux [] l; U.mql_false with Found -> U.mql_true) + | M.StatVal y -> + let t = U.start_time () in + let r = (eval_val c y) in + let s = U.stop_time t in + out (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 = U.start_time () in + P.text_of_query out x "\n"; + let s = U.stop_time t in + if String.contains m stat_char then + out (Printf.sprintf "Log source: %s\n" s); + eval_query c x + end else begin + let s = (eval_query c x) in + let t = U.start_time () in + P.text_of_result out s "\n"; + let r = U.stop_time t in + if String.contains m stat_char then + out (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 + 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 + | M.GenFMeet -> U.mql_intersect + in + let rec for_aux = function + | [] -> [] + | h :: t -> + let d = {c with avars = U.set (i, h) c.avars} in + f (eval_query d x2) (for_aux t) + in + for_aux (eval_query c x1) + | 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 + List.fold_right g (eval_query c x) [] + | M.Property q0 q1 q2 mc ct cf el pat y -> + let subj, mct = + if q0 then [], (pat, q2 @ mc, eval_val c y) + else (q2 @ mc), (pat, [], eval_val c y) + in + let f = if String.contains m galax_char + then MQIProperty.galax else MQIProperty.postgres + in + let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in + let cons_true = mct :: List.map eval_cons ct in + let cons_false = List.map eval_cons cf in + let eval_exp (p, po) = (q2 @ p, po) in + let exp = List.map eval_exp el in + let t = U.start_time () in + let r = f q1 subj cons_true cons_false exp in + let s = U.stop_time t in + if String.contains m stat_char then + out (Printf.sprintf "Property: %s,%i\n" s (List.length r)); + r + | M.StatQuery x -> + let t = U.start_time () in + let r = (eval_query c x) in + let s = U.stop_time t in + out (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 + 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) + and eval_grp c = function + | M.Attr l -> + let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] in + [List.fold_left attr_aux [] l] + | 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 t = U.start_time () in + let r = eval_query c x in + let s = U.stop_time t in + if String.contains m stat_char then + out (Printf.sprintf "MQIExecute: %s,%s\n" s m); + r diff --git a/helm/ocaml/mathql_interpreter/mQIExecute.mli b/helm/ocaml/mathql_interpreter/mQIExecute.mli new file mode 100644 index 000000000..536e489c1 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIExecute.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 06/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +val execute : (string -> unit) -> string -> MathQL.query -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml new file mode 100644 index 000000000..fe4e3f6f9 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.ml @@ -0,0 +1,57 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let default_connection_string = + "dbname=mowgli_test user=helm" + +let connection = ref None + +let connection_string = + try Sys.getenv "POSTGRESQL_CONNECTION_STRING" + with Not_found -> default_connection_string + +let init () = + try connection := Some (new Postgres.connection connection_string); + with _ -> raise (Failure ("MQIPostgres.init: " ^ connection_string)) + +let close () = match ! connection with + | None -> () + | Some c -> c#close + +let check () = ! connection <> None + +let exec q = match ! connection with + | None -> [] + | Some c -> (c#exec q)#get_list + +let quote s = + let rec quote_aux s = + try + let l = String.length s in + let i = String.index s '\'' in + String.sub s 0 i ^ "\\'" ^ quote_aux (String.sub s (succ i) (l - (succ i))) + with Not_found -> s + in + "'" ^ quote_aux s ^ "'" diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.mli b/helm/ocaml/mathql_interpreter/mQIPostgres.mli new file mode 100644 index 000000000..8906a4985 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 06/01/2003 *) +(* *) +(* *) +(******************************************************************************) + + +val init : unit -> unit + +val close : unit -> unit + +val check : unit -> bool + +val exec : string -> string list list + +val quote : string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml new file mode 100644 index 000000000..c30c18d47 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -0,0 +1,167 @@ + +(* 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/. + *) + +module M = MathQL +module P = MQIPostgres +module U = MQIUtil + +let not_supported s = + raise (Failure ("MQIProperty: feature not supported: " ^ s)) + +(* debugging ***************************************************************) + +let pg_print l = + let rec pg_record = function + | [] -> prerr_newline () + | head :: tail -> prerr_string (head ^ " "); pg_record tail + in + List.iter pg_record l + +let cl_print l = + let c_print (b, p, v) = + prerr_string (if b then "match " else "in "); + List.iter (fun x -> prerr_string ("/" ^ x)) p; + prerr_newline (); + List.iter prerr_endline v + in + List.iter c_print l + +(* PostgreSQL backend ******************************************************) + +let pg_query table cols ct cf = + let rec iter f sep = function + | [] -> "" + | [head] -> f head + | head :: tail -> f head ^ sep ^ iter f sep tail + in + let pg_cols = iter (fun x -> x) ", " cols in + let pg_msval v = iter P.quote ", " v in + let pg_con (pat, col, v) = + if col <> "" then + let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in + if pat then "(" ^ iter f " or " v ^ ")" + else col ^ " in (" ^ pg_msval v ^ ")" + else "true" + in + let pg_cons l = iter pg_con " and " l in + let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in + let pg_where = match ct, cf with + | [], [] -> "" + | lt, [] -> " where " ^ pg_cons lt + | [], lf -> " where " ^ pg_cons_not lf + | lt, lf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not lf + in + if cols = [] then [] else begin + let q = "select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ + " order by " ^ List.hd cols ^ " asc" in + prerr_endline q; + P.exec q end + +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 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)) + in + compose mk_avs res + +let get_table mc ct cf el = + let fst = function + | [] -> None + | head :: tail -> Some head + in + let comp n1 n2 = match n1, n2 with + | None, _ -> n2 + | Some h, Some k when h = k -> n2 + | _, None -> n1 + | _ -> not_supported "comp" + in + let rec get_c prev = function + | [] -> prev + | (_, p, _) :: tail -> get_c (comp prev (fst p)) tail + in + let rec get_e prev = function + | [] -> prev + | (p, _) :: tail -> get_e (comp prev (fst p)) tail + in + get_e (get_c (get_c (fst mc) ct) cf) el + +let rec decolon s = + let l = String.length s in + try + let i = String.index s ':' in + String.sub s 0 i ^ "_" ^ decolon (String.sub s (succ i) (l - succ i)) + with Not_found -> s + +let conv = function + | [] -> "source" + | ["objectname"] -> "value" + | [t] -> "" + | [_; t] -> decolon t + | _ -> not_supported "conv" + +let postgres_single mc ct cf el t = + let table = match t with Some t -> decolon t | None -> "objectname" in + let first = conv mc in + let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in + let cons_true = mk_con ct in + let cons_false = mk_con cf in + let other_cols = List.map (fun (p, _) -> conv p) el in + let cols = if first = "" then other_cols else first :: other_cols in + pg_result false first el (pg_query table cols cons_true cons_false) + +let deadline = 100 + +let postgres refine mc ct cf el = + if refine <> M.RefineExact then not_supported "postgres"; + cl_print ct; + let table = get_table mc ct cf el in + let rec postgres_aux ct = match ct with + | (pat, p, v) :: tail when List.length v > deadline -> + let single s = postgres_aux ((pat, p, [s]) :: tail) in + U.mql_iter single v + | _ -> + postgres_single mc ct cf el table + in postgres_aux ct + +(* Galax backend ***********************************************************) + +let galax refine mc ct cf el = not_supported "Galax" + +(* funzioni vecchie ********************************************************) + +let pg_name s = + let q = "select id from registry where uri = " ^ P.quote s in + match P.exec q with + | [[id]] -> "t" ^ id + | _ -> "" + +let get_id b = if b then ["B"] else ["F"] diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.mli b/helm/ocaml/mathql_interpreter/mQIProperty.mli new file mode 100644 index 000000000..90ac3cba6 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIProperty.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open MathQL + +val postgres: refine -> path -> + (bool * path * value) list -> (bool * path * value) list -> + exp_list -> result + +val galax: refine -> path -> + (bool * path * value) list -> (bool * path * value) list -> + exp_list -> result diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml new file mode 100644 index 000000000..537e32d77 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml @@ -0,0 +1,165 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 06/01/2003 *) +(* *) +(* *) +(******************************************************************************) + + +(* 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 + | _, [] -> 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_union v1 v2 = + match v1, v2 with + | [], v -> v + | v, [] -> v (* (zz h1 ">" h2); *) + | 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 iter f = function + | [] -> [] + | head :: tail -> set_union (f head) (iter f tail) + +(* MathQL specific set operations ******************************************) + +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_itwr2") + +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, mql_prod 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 ******************************************************) + +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 + +(* time handling ***********************************************************) + +type time = float * float + +let start_time () = + (Sys.time (), Unix.time ()) + +let stop_time (s0, u0) = + let s1 = Sys.time () in + let u1 = Unix.time () in + Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli new file mode 100644 index 000000000..38ca8f380 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIUtil.mli @@ -0,0 +1,81 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 06/01/2003 *) +(* *) +(* *) +(******************************************************************************) + + +val mql_true : MathQL.value + +val mql_false : MathQL.value + +val set_sub : MathQL.value -> MathQL.value -> MathQL.value + +val set_meet : MathQL.value -> MathQL.value -> MathQL.value + +val set_eq : MathQL.value -> MathQL.value -> MathQL.value + +val set_union : 'a list -> 'a list -> 'a list + +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.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 set : string * 'a -> (string * 'a) list -> (string * 'a) list + +type time + +val start_time : unit -> time + +val stop_time : time -> string diff --git a/helm/ocaml/mathql_test/.cvsignore b/helm/ocaml/mathql_test/.cvsignore index 6e9e9c2c2..180760238 100644 --- a/helm/ocaml/mathql_test/.cvsignore +++ b/helm/ocaml/mathql_test/.cvsignore @@ -1 +1,2 @@ -*.cm[aiox] *.cmxa *.opt mqtop mqitop examples* +*.cm[aiox] *.cmxa *.opt mqtop mqitop mqgtop examples* +mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml diff --git a/helm/ocaml/mathql_test/.depend b/helm/ocaml/mathql_test/.depend index e69de29bb..6974b7052 100644 --- a/helm/ocaml/mathql_test/.depend +++ b/helm/ocaml/mathql_test/.depend @@ -0,0 +1,2 @@ +mqgtop.cmo: mQGTopParser.cmi +mqgtop.cmx: mQGTopParser.cmx diff --git a/helm/ocaml/mathql_test/Makefile b/helm/ocaml/mathql_test/Makefile index f6f41aaa4..cd902ab3e 100644 --- a/helm/ocaml/mathql_test/Makefile +++ b/helm/ocaml/mathql_test/Makefile @@ -1,23 +1,27 @@ BIN_DIR = /usr/local/bin -REQUIRES = unix helm-cic helm-cic_textual_parser helm-mathql helm-mathql_interpreter +REQUIRES = unix helm-cic helm-cic_textual_parser helm-mathql helm-mathql_interpreter helm-mquery_generator PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) OCAMLDEP = ocamldep +OCAMLYACC = ocamlyacc +OCAMLLEX = ocamllex LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) MQTOP = mqtop.ml MQITOP = mqitop.ml +MQGTOP = mqgtop.ml -DEPOBJS = $(MQTOP) $(MQITOP) +DEPOBJS = $(MQTOP) $(MQITOP) $(MQGTOP) +AUXOBJS = mQGTopParser.ml mQGTopLexer.ml all: $(DEPOBJS:.ml=) opt: $(DEPOBJS:.ml=.opt) -depend: +depend: $(AUXOBJS) $(OCAMLDEP) $(DEPOBJS) > .depend mqtop: $(MQTOP:.ml=.cmo) $(LIBRARIES) @@ -32,19 +36,32 @@ mqitop: $(MQITOP:.ml=.cmo) $(LIBRARIES) mqitop.opt: $(MQITOP:.ml=.cmx) $(LIBRARIES_OPT) $(OCAMLOPT) -linkpkg -o mqitop.opt $(MQITOP:.ml=.cmx) -.SUFFIXES: .ml .mli .cmo .cmi .cmx +mqgtop: mQGTopParser.cmi $(AUXOBJS:.ml=.cmo) $(MQGTOP:.ml=.cmo) $(LIBRARIES) + $(OCAMLC) -linkpkg -o mqgtop $(AUXOBJS:.ml=.cmo) $(MQGTOP:.ml=.cmo) + +mqgtop.opt: $(AUXOBJS:.ml=.cmx) $(MQGTOP:.ml=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -linkpkg -o mqgtop.opt $(AUXOBJS:.ml=.cmx) $(MQGTOP:.ml=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx .mly .mll .ml.cmo: $(LIBRARIES) $(OCAMLC) -c $< .mli.cmi: $(LIBRARIES) $(OCAMLC) -c $< .ml.cmx: $(LIBRARIES_OPT) $(OCAMLOPT) -c $< +.mly.ml: + $(OCAMLYACC) $< +.mly.mli: + $(OCAMLYACC) $< +.mll.ml: + $(OCAMLLEX) $< $(DEPOBJS:%.ml=%.cmo): $(LIBRARIES) $(DEPOBJS:%.ml=%.cmx): $(LIBRARIES_OPT) clean: - rm -f *.cm[iox] *.o $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) + rm -f *.cm[iox] *.o $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) \ + mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml install: cp $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) $(BIN_DIR) diff --git a/helm/ocaml/mathql_test/mQGTopLexer.mll b/helm/ocaml/mathql_test/mQGTopLexer.mll new file mode 100644 index 000000000..cf116641b --- /dev/null +++ b/helm/ocaml/mathql_test/mQGTopLexer.mll @@ -0,0 +1,70 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +{ + open MQGTopParser + + let debug = false + + let out s = if debug then prerr_endline s +} + +let SPC = [' ' '\t' '\n']+ +let ALPHA = ['A'-'Z' 'a'-'z' '_'] +let NUM = ['0'-'9'] +let IDEN = ALPHA (NUM | ALPHA)* +let QSTR = [^ '"' '\\']+ + +rule comm_token = parse + | "(*" { comm_token lexbuf; comm_token lexbuf } + | "*)" { () } + | ['*' '('] { comm_token lexbuf } + | [^ '*' '(']* { comm_token lexbuf } +and string_token = parse + | '"' { DQ } + | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } + | QSTR { STR (Lexing.lexeme lexbuf) } + | eof { EOF } +and spec_token = parse + | "(*" { comm_token lexbuf; spec_token lexbuf } + | SPC { spec_token lexbuf } + | '"' { let str = qstr string_token lexbuf in + out ("STR " ^ str); STR str } + | '{' { out "LC"; LC } + | '}' { out "RC"; RC } + | ',' { out "CM"; CM } + | '$' { out "DL"; DL } + | "not" { out "NOT" ; NOT } + | "mustobj" { out "MOBJ" ; MOBJ } + | "mustsort" { out "MSORT" ; MSORT } + | "mustrel" { out "MREL" ; MREL } + | "sonlyobj" { out "SOBJ" ; SOBJ } + | "sonlysort" { out "SSORT" ; SSORT } + | "onlyrel" { out "OREL" ; OREL } + | "wonlyobj" { out "WOBJ" ; WOBJ } + | "wonlysort" { out "WSORT" ; WSORT } + | IDEN { let id = Lexing.lexeme lexbuf in + out ("ID " ^ id); ID id } + | eof { EOF } diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly new file mode 100644 index 000000000..9fd70a033 --- /dev/null +++ b/helm/ocaml/mathql_test/mQGTopParser.mly @@ -0,0 +1,103 @@ +/* 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/. + */ + +%{ + let f (x, y, z) = x + let s (x, y, z) = y + let t (x, y, z) = z + + module G = MQueryGenerator +%} + %token ID + %token CONURI + %token VARURI + %token INDTYURI + %token INDCONURI + %token ALIAS EOF + + %start interp + %type CicTextualParser0.interpretation_codomain_item option> interp + + %token STR + %token DL DQ LC RC CM NOT + %token MOBJ MSORT MREL SOBJ SSORT OREL WOBJ WSORT + + %start qstr + %type qstr +%% + uri: + | CONURI { CicTextualParser0.ConUri $1 } + | VARURI { CicTextualParser0.VarUri $1 } + | INDTYURI { CicTextualParser0.IndTyUri ((fst $1), (snd $1)) } + | INDCONURI { CicTextualParser0.IndConUri ((f $1), (s $1), (t $1)) } + ; + alias: + | ALIAS ID uri { ($2, CicTextualParser0.Uri $3) } + ; + aliases: + | alias aliases { $1 :: $2 } + | EOF { [] } + ; + interp: + | aliases { function CicTextualParser0.Id s -> (try Some (List.assoc s $1) + with Not_found -> None) + | _ -> None } + ; + + qstr: + | DQ { "" } + | STR qstr { $1 ^ $2 } + ; +/* str: + | STR { $1 } + | DL ID { try G.builtin $2 with _ -> "" } + ; + strs: + | str CM strs { $1 :: $3 } + | str { [$1] } + | { [] } + ; + list: + | LC strs RC { $2 } + ; + not: + | NOT { true } + | { false } + ; + spec: + | MOBJ not list list list { G.MustObj ($2, $3, $4, $5) } + | MSORT not list list list { G.MustSort ($2, $3, $4, $5) } + | MREL not list list { G.MustRel ($2, $3, $4) } + | SOBJ not list list list { G.SOnlyObj ($2, $3, $4, $5) } + | SSORT not list list list { G.SOnlySort ($2, $3, $4, $5) } + | OREL not list list { G.OnlyRel ($2, $3, $4) } + | WOBJ not list list list { G.WOnlyObj ($2, $3, $4, $5) } + | WSORT not list list list { G.WOnlySort ($2, $3, $4, $5) } + ; + specs: + | spec specs { $1 :: $2 } + | EOF { [] } + ; +*/ diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml new file mode 100644 index 000000000..6304a65f5 --- /dev/null +++ b/helm/ocaml/mathql_test/mqgtop.ml @@ -0,0 +1,298 @@ +(* 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/. + *) + +let query_num = ref 1 + +let interp_file = ref "interp.cic" + +let log_file = ref "MQGenLog.htm" + +let show_queries = ref false + +let int_options = ref "" + +let nl = "

\n" + +module MQI = MQueryInterpreter +module MQIC = MQIConn +module MQG = MQueryGenerator + +let get_handle () = + MQIC.init (MQIC.flags_of_string ! int_options) + (fun s -> print_string s; flush stdout) + +let issue handle q = + let module U = MQueryUtil in + let mode = [Open_wronly; Open_append; Open_creat; Open_text] in + let perm = 64 * 6 + 8 * 6 + 4 in + let time () = + let lt = Unix.localtime (Unix.time ()) in + "NEW LOG: " ^ + string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_year + 1900) ^ " " ^ + string_of_int (lt.Unix.tm_hour) ^ ":" ^ + string_of_int (lt.Unix.tm_min) ^ ":" ^ + string_of_int (lt.Unix.tm_sec) + in + let log q r = + let och = open_out_gen mode perm ! log_file in + let out = output_string och in + if ! query_num = 1 then out (time () ^ nl); + out ("Query: " ^ string_of_int ! query_num ^ nl); + U.text_of_query out q nl; + out ("Result: " ^ nl); + U.text_of_result out r nl; + close_out och + in + if ! show_queries then U.text_of_query (output_string stdout) q nl; + let r = MQI.execute handle q in + U.text_of_result (output_string stdout) r nl; + if ! log_file <> "" then log q r; + incr query_num; + flush stdout + +let get_interp () = + let module L = CicTextualLexer in + let module T = CicTextualParser in + let module P = MQGTopParser in + let lexer = function + | T.ID s -> P.ID s + | T.CONURI u -> P.CONURI u + | T.VARURI u -> P.VARURI u + | T.INDTYURI (u, p) -> P.INDTYURI (u, p) + | T.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s) + | T.LETIN -> P.ALIAS + | T.EOF -> P.EOF + | _ -> assert false + in + let ich = open_in ! interp_file in + let lexbuf = Lexing.from_channel ich in + let f = P.interp (fun x -> lexer (L.token x)) lexbuf in + close_in ich; f + +let get_terms interp = + let interp = get_interp () in + let lexbuf = Lexing.from_channel stdin in + let rec aux () = + try + let dom, mk_term = + CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf + in + (snd (mk_term interp)) :: aux () + with + CicTextualParser0.Eof -> [] + 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 _ -> +*) + in print_endline s; flush stdout + +let rec display = function + | [] -> () + | term :: tail -> + display tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + flush stdout + +let execute ich = + let module U = MQueryUtil in + let lexbuf = Lexing.from_channel ich in + let handle = get_handle () in + let rec execute_aux () = + try + let q = U.query_of_text lexbuf in + issue handle q; execute_aux () + with End_of_file -> () + in + execute_aux (); + MQIC.close handle +(* +let compose () = + let module P = MQGTopParser in + let module L = MQGTopLexer in + let module G = MQueryGeneratorNew in + let cl = P.specs L.spec_token (Lexing.from_channel stdin) in + issue (G.compose cl) +*) +let locate name = + let handle = get_handle () in + issue handle (MQG.locate name); + MQIC.close handle + +let mpattern n m l = + let module C = MQueryLevels2 in + let queries = ref [] in + let handle = get_handle () in + let rec pattern level = function + | [] -> () + | term :: tail -> + pattern level tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.time () in + let om,rm,sm = C.get_constraints term in + let oml,rml,sml = List.length om, List.length rm, List.length sm in + let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in + let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in + let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in + let q = MQG.searchPattern (om,rm,sm) (oo,ro,so) in + if not (List.mem q ! queries) then + begin + issue handle q; + let t1 = Sys.time () -. t0 in + Printf.eprintf "[%i] " (pred ! query_num); flush stderr; + Printf.printf "%i GEN = %i: %.2fs%s" + (pred ! query_num) (oml + rml + sml + ool + rol + sol) t1 nl; + flush stdout; queries := q :: ! queries + end + in + for level = max m n downto min m n do + Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level; + flush stderr; pattern level l + done; + Printf.eprintf "\nmqgtop: pattern: %i queries issued\n" + (List.length ! queries); + flush stderr; + MQIC.close handle +(* +let mbackward n m l = + let module C = MQueryLevels in + let module G = MQueryGenerator in + let queries = ref [] in + let torigth_restriction (u, b) = + let p = if b + then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" + in + (u, p, None) + in + let rec backward level = function + | [] -> () + | term :: tail -> + backward level tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.time () in + let list_of_must, only = C.out_restr [] [] term in + let max_level = pred (List.length list_of_must) in + let must = List.nth list_of_must (min level max_level) in + let rigth_must = List.map torigth_restriction must in + let rigth_only = Some (List.map torigth_restriction only) in + let q = G.searchPattern (rigth_must, [], []) (rigth_only , None, None) in + if not (List.mem q ! queries) then + begin + issue q; + let t1 = Sys.time () -. t0 in + Printf.eprintf "[%i] " (pred ! query_num); flush stderr; + Printf.printf "%i GEN = %i: %.2fs%s" + (pred ! query_num) (List.length must) t1 nl; + flush stdout; queries := q :: ! queries + end + in + for level = max m n downto min m n do + Printf.eprintf "\nmqgtop: backward: trying level %i\n" level; + flush stderr; backward level l + done; + Printf.eprintf "\nmqgtop: backward: %i queries issued\n" + (List.length ! queries); + flush stderr +*) + +let set_options s = int_options := s + +let check () = + let handle = get_handle () in + Printf.eprintf + "mqgtop: current options: %s, connection: %s\n" + ! int_options (if MQIC.connected handle then "on" else "off"); + MQIC.close handle + +let prerr_help () = + prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n"; + prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for"; + prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output"; + prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n"; + prerr_endline "OPTIONS:\n"; + prerr_endline "-h -help shows this help message"; + prerr_endline "-q -show-queries outputs generated queries"; + 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 "-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"; + prerr_endline "-C -compose issues the \"Compose\" query reading its specifications"; + prerr_endline " from the input file"; + prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; + prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all"; + prerr_endline " CIC terms in the input file"; + prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0"; + prerr_endline " on all CIC terms in the input file"; + prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all"; + prerr_endline " CIC terms in the input file"; + prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0"; + prerr_endline " on all CIC terms in the input file\n"; + 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" + +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 + | ("-x"|"-execute") :: rem -> execute stdin; parse rem + | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem + | ("-o"|"-options") :: arg :: rem -> set_options arg; parse rem + | ("-c"|"-check") :: rem -> check (); parse rem +(* | ("-C"|"-compose") :: rem -> compose (); parse rem +*) | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem +(* | ("-M"|"-backward") :: arg :: rem -> + let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem + | ("-MB"|"-multi-backward") :: arg :: rem -> + let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem +*) | ("-P"|"-pattern") :: arg :: rem -> + let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem + | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem + | _ :: rem -> parse rem + +let _ = + Logger.log_callback := + (Logger.log_to_html + ~print_and_flush:(function s -> print_string s ; flush stdout)) ; + parse (List.tl (Array.to_list Sys.argv)); + prerr_endline ("mqgtop: done in " ^ string_of_float (Sys.time ()) ^ + " seconds"); + exit 0