--- /dev/null
+(* 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
--- /dev/null
+(* 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 <fguidi@cs.unibo.it> *)
+(* 06/01/2003 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+val execute : (string -> unit) -> string -> MathQL.query -> MathQL.result
--- /dev/null
+(* 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 ^ "'"
--- /dev/null
+(* 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 <fguidi@cs.unibo.it> *)
+(* 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
--- /dev/null
+
+(* 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"]
--- /dev/null
+(* 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
--- /dev/null
+(* 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 <fguidi@cs.unibo.it> *)
+(* 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)
--- /dev/null
+(* 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 <fguidi@cs.unibo.it> *)
+(* 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
-*.cm[aiox] *.cmxa *.opt mqtop mqitop examples*
+*.cm[aiox] *.cmxa *.opt mqtop mqitop mqgtop examples*
+mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
+mqgtop.cmo: mQGTopParser.cmi
+mqgtop.cmx: mQGTopParser.cmx
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)
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)
--- /dev/null
+(* 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 }
--- /dev/null
+/* 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 <string> ID
+ %token <UriManager.uri> CONURI
+ %token <UriManager.uri> VARURI
+ %token <UriManager.uri * int> INDTYURI
+ %token <UriManager.uri * int * int> INDCONURI
+ %token ALIAS EOF
+
+ %start interp
+ %type <CicTextualParser0.interpretation_domain_item -> CicTextualParser0.interpretation_codomain_item option> interp
+
+ %token <string> STR
+ %token DL DQ LC RC CM NOT
+ %token MOBJ MSORT MREL SOBJ SSORT OREL WOBJ WSORT
+
+ %start qstr
+ %type <string> 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 { [] }
+ ;
+*/
--- /dev/null
+(* 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 = " <p>\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
projects / helm.git / commitdiff