mQueryMisc.cmo: mQueryMisc.cmi
mQueryMisc.cmx: mQueryMisc.cmi
+mQueryUtil.cmo: mQueryUtil.cmi
+mQueryUtil.cmx: mQueryUtil.cmi
REQUIRES = helm-cic helm-cic_textual_parser
PREDICATES =
-INTERFACE_FILES = mQueryMisc.mli
+INTERFACE_FILES = mQueryMisc.mli mQueryUtil.mli
-IMPLEMENTATION_FILES = mathQL.ml mQueryMisc.ml
+IMPLEMENTATION_FILES = mQueryMisc.ml mathQL.ml mQueryUtil.ml
EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* time handling ***********************************************************)
+
+type time = float * float
+
+let start_time () =
+ (Sys.time (), Unix.time ())
+
+let stop_time (s0, u0) =
+ let s1 = Sys.time () in
+ let u1 = Unix.time () in
+ Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0)
+
+(* operations on lists *****************************************************)
+
+type 'a comparison = Lt
+ | Gt
+ | Eq of 'a
+
+let list_join f l1 l2 =
+ let rec aux = function
+ | [], v
+ | v, [] -> v
+ | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
+ match f h1 h2 with
+ | Lt -> h1 :: aux (t1, v2)
+ | Gt -> h2 :: aux (v1, t2)
+ | Eq h -> h :: aux (t1, t2)
+ end
+ in aux (l1, l2)
+
+let list_meet f l1 l2 =
+ let rec aux = function
+ | [], v
+ | v, [] -> []
+ | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
+ match f h1 h2 with
+ | Lt -> aux (t1, v2)
+ | Gt -> aux (v1, t2)
+ | Eq h -> h :: aux (t1, t2)
+ end
+ in aux (l1, l2)
+
+let rec flat_list out f s = function
+ | [] -> ()
+ | [a] -> f a
+ | a :: tail -> f a; out s; flat_list out f s tail
+
+let rec add_assoc ap = function
+ | [] -> [ap]
+ | head :: tail when fst head = fst ap -> ap :: tail
+ | head :: tail -> head :: add_assoc ap tail
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+type time
+
+val start_time : unit -> time
+
+val stop_time : time -> string
+
+type 'a comparison = Lt
+ | Gt
+ | Eq of 'a
+
+val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list
+
+val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list
+
+val flat_list : ('a -> unit) -> ('b -> unit) -> 'a -> 'b list -> unit
+
+val add_assoc : 'a * 'b -> ('a * 'b) list -> ('a * 'b) list
type avar = string (* the name of a variable for a resource *)
-type vvar = string (* the name of a variable for an attribute value *)
-
type inverse = bool
type refine = RefineExact
type source = bool
-type bin = BinFJoin (* full union - with attr handling *)
- | BinFMeet (* full intersection - with attr handling *)
- | BinFDiff (* full difference - with attr handling *)
-
type gen = GenFJoin (* full union - with attr handling *)
| GenFMeet (* full intersection - with attr handling *)
-type test = Xor
- | Or
- | And
- | Sub
- | Meet
- | Eq
- | Le
- | Lt
-
-type query = Empty
- | SVar of svar
+type query = Const of result
+ | SVar of svar
| AVar of avar
- | Subj of msval
+ | Dot of avar * path
+ | Ex of avar list * query
+ | Select of avar * query * query
+ | Let of svar * query * query
+ | Fun of path * path list * query list
+ | Add of bool * groups * query
+ | For of gen * avar * query * query
| Property of inverse * refine * path *
main * istrue * isfalse list * exp_list *
- pattern * msval
- | Select of avar * query * msval
- | Bin of bin * query * query
- | LetSVar of svar * query * query
- | LetVVar of vvar * msval * query
- | For of gen * avar * query * query
- | Add of bool * groups * query
- | If of msval * query * query
- | Log of xml * source * query
- | StatQuery of query
- | Keep of allbut * path list * query
-
-and msval = False
- | True
- | Not of msval
- | Ex of avar list * msval
- | Test of test * msval * msval
- | Const of string
- | Set of msval list
- | Proj of path option * query
- | Dot of avar * path
- | VVar of vvar
- | StatVal of msval
- | Count of msval
- | Align of string * msval
-
-and groups = Attr of (path * msval) list list
+ pattern * query
+
+and groups = Attr of (path * query) list list
| From of avar
-and con = pattern * path * msval
+and con = pattern * path * query
and istrue = con list
-*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli
+*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli *.output
mQIConn.cmi: mQIMap.cmi
+mQILib.cmi: mQIConn.cmi
mQIProperty.cmi: mQIConn.cmi
mQueryInterpreter.cmi: mQIConn.cmi
-mQueryTParser.cmo: mQueryTParser.cmi
-mQueryTParser.cmx: mQueryTParser.cmi
-mQueryTLexer.cmo: mQueryTParser.cmi
-mQueryTLexer.cmx: mQueryTParser.cmx
-mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mQueryUtil.cmi
-mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mQueryUtil.cmi
-mQIUtil.cmo: mQIUtil.cmi
-mQIUtil.cmx: mQIUtil.cmi
mQIPostgres.cmo: mQIPostgres.cmi
mQIPostgres.cmx: mQIPostgres.cmi
-mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi
-mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi
+mQIMap.cmo: mQIMap.cmi
+mQIMap.cmx: mQIMap.cmi
mQIConn.cmo: mQIMap.cmi mQIPostgres.cmi mQIConn.cmi
mQIConn.cmx: mQIMap.cmx mQIPostgres.cmx mQIConn.cmi
+mQIUtil.cmo: mQIUtil.cmi
+mQIUtil.cmx: mQIUtil.cmi
+mQILib.cmo: mQIConn.cmi mQIUtil.cmi mQILib.cmi
+mQILib.cmx: mQIConn.cmx mQIUtil.cmx mQILib.cmi
mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIUtil.cmi \
mQIProperty.cmi
mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIUtil.cmx \
mQIProperty.cmi
-mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi mQueryUtil.cmi \
- mQueryInterpreter.cmi
-mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx mQueryUtil.cmx \
- mQueryInterpreter.cmi
+mQueryTParser.cmo: mQILib.cmi
+mQueryTParser.cmx: mQILib.cmx
+mQueryTLexer.cmo: mQueryTParser.cmo
+mQueryTLexer.cmx: mQueryTParser.cmx
+mQueryIO.cmo: mQILib.cmi mQueryTLexer.cmo mQueryTParser.cmo mQueryIO.cmi
+mQueryIO.cmx: mQILib.cmx mQueryTLexer.cmx mQueryTParser.cmx mQueryIO.cmi
+mQueryInterpreter.cmo: mQIConn.cmi mQILib.cmi mQIProperty.cmi mQIUtil.cmi \
+ mQueryIO.cmi mQueryInterpreter.cmi
+mQueryInterpreter.cmx: mQIConn.cmx mQILib.cmx mQIProperty.cmx mQIUtil.cmx \
+ mQueryIO.cmx mQueryInterpreter.cmi
PREDICATES =
-INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \
- mQIPostgres.mli mQIMap.mli mQIConn.mli \
- mQIProperty.mli mQueryInterpreter.mli
+PRE_IFILES = mQIPostgres.mli mQIMap.mli mQIConn.mli \
+ mQIUtil.mli mQILib.mli mQIProperty.mli
-IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \
- $(INTERFACE_FILES:%.mli=%.ml)
+POST_IFILES = mQueryIO.mli mQueryInterpreter.mli
-EXTRA_OBJECTS_TO_INSTALL = mQueryTLexer.cmi \
- mQueryTLexer.mll mQueryTParser.mly
+INTERFACE_FILES = $(PRE_IFILES) $(POST_IFILES)
+
+IMPLEMENTATION_FILES = $(PRE_IFILES:%.mli=%.ml) \
+ mQueryTParser.ml mQueryTLexer.ml \
+ $(POST_IFILES:%.mli=%.ml)
+
+EXTRA_OBJECTS_TO_INSTALL = mQITypes.cmi mQueryTLexer.cmi \
+ mQITypes.ml mQueryTLexer.mll mQueryTParser.mly
EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \
mQueryTLexer.ml
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+module M = MathQL
+module P = MQueryUtil
+module U = MQIUtil
+module C = MQIConn
+
+(* external function specification ******************************************)
+
+type arity_t = Const of int
+ | Positive
+ | Any
+
+type eval_spec = {eval : M.query -> M.result;
+ handle : C.handle
+ }
+
+type txt_out_spec = {out : string -> unit;
+ path : M.path -> unit;
+ query : M.query -> unit;
+ result : M.result -> unit
+ }
+
+type fun_spec = {arity_p : arity_t;
+ arity_s : arity_t;
+ body : eval_spec -> txt_out_spec ->
+ M.path list -> M.query list -> M.result;
+ txt_out : txt_out_spec ->
+ M.path list -> M.query list -> unit
+ }
+
+exception ArityError of M.path * arity_t * int
+
+exception NameError of M.path
+
+exception NumberError of M.result
+
+(* external functions implementation ****************************************)
+
+let int_of_set s =
+ try match s with
+ | [s, _] -> int_of_string s
+ | _ -> raise (Failure "int_of_string")
+ with Failure "int_of_string" -> raise (NumberError s)
+
+let out_txt2 out commit n x1 x2 =
+ out "(" ; commit x1; out (" " ^ n ^ " "); commit x2; out ")"
+
+let out_txt_ out path commit p xl =
+ path p; out " {"; P.flat_list out commit ", " xl; out "}"
+
+let out_txt_full out path commit p pl xl =
+ path p; out " {"; P.flat_list out path ", " pl; out "} {";
+ P.flat_list out commit ", " xl; out "}"
+
+let arity0 n r =
+ let arity_p = Const 0 in
+ let arity_s = Const 0 in
+ let body _ _ _ _ = U.mql_true in
+ let txt_out s _ _ = s.out n in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let arity1 n f =
+ let arity_p = Const 0 in
+ let arity_s = Const 1 in
+ let body eval _ _ = function
+ | [x] -> f (eval x)
+ | _ -> assert false
+ in
+ let txt_out out _ commit _ = function
+ | [x] -> out (n ^ " "); commit x
+ | _ -> assert false
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let arity2 n f =
+ let arity_p = Const 0 in
+ let arity_s = Const 2 in
+ let body eval _ _ = function
+ | [x1; x2] -> f (eval x1) (eval x2)
+ | _ -> assert false
+ in
+ let txt_out out _ commit _ = function
+ | [x1; x2] -> out_txt2 out commit n x1 x2
+ | _ -> assert false
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let false_fun = arity0 "false" U.mql_false
+
+let true_fun = arity0 "true" U.mql_true
+
+let not_fun =
+ let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
+ arity1 "not" aux
+
+let count_fun =
+ let aux r = [string_of_int (List.length r), []] in
+ arity1 "count" aux
+
+let diff_fun = arity2 "diff" U.mql_diff
+
+let xor_fun = arity2 "xor" U.xor
+
+let sub_fun = arity2 "sub" U.set_sub
+
+let meet_fun = arity2 "meet" U.set_meet
+
+let eq_fun = arity2 "eq" U.set_eq
+
+let le_fun =
+ let le v1 v2 =
+ if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false
+ in
+ arity2 "le" le
+
+let lt_fun =
+ let lt v1 v2 =
+ if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false
+ in
+ arity2 "lt" lt
+
+let stat_fun =
+ let arity_p = Const 0 in
+ let arity_s = Const 1 in
+ let body eval h _ = function
+ | [x] ->
+ let t = P.start_time () in
+ let r = (eval x) in
+ let s = P.stop_time t in
+ C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+ r
+ | _ -> assert false
+ in
+ let txt_out out _ commit _ = function
+ | [x] -> out "stat "; commit x
+ | _ -> assert false
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let align_fun =
+ let aux l (v, g) =
+ let c = String.length v in
+ if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g]
+ in
+ let arity_p = Const 0 in
+ let arity_s = Const 2 in
+ let body eval _ _ = function
+ | [y; x] ->
+ let l = int_of_set (eval y) in
+ U.mql_iter (aux l) (eval x)
+ | _ -> assert false
+ in
+ let txt_out out _ commit _ = function
+ | [y; x] -> out "align "; commit y; out " in "; commit x
+ | _ -> assert false
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let if_fun =
+ let arity_p = Const 0 in
+ let arity_s = Const 3 in
+ let body eval _ _ = function
+ | [y; x1; x2] ->
+ if (eval y) = U.mql_false then (eval x2) else (eval x1)
+ | _ -> assert false
+ in
+ let txt_out out _ commit _ = function
+ | [y; x1; x2] ->
+ out "if "; commit y; out " then "; commit x1; out " else "; commit x2
+ | _ -> assert false
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let intersect_fun =
+ let rec iter f = function
+ | [] -> assert false
+ | [head] -> f head
+ | head :: tail -> U.mql_intersect (f head) (iter f tail)
+ in
+ let arity_p = Const 0 in
+ let arity_s = Positive in
+ let body eval _ _ xl = iter eval xl in
+ let txt_out out path commit _ = function
+ | [] -> assert false
+ | [x1; x2] -> out_txt2 out commit "intersect" x1 x2
+ | xl -> out_txt_ out path commit ["intersect"] xl
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let union_fun =
+ let arity_p = Const 0 in
+ let arity_s = Any in
+ let body eval _ _ xl = U.mql_iter eval xl in
+ let txt_out out path commit _ = function
+ | [x1; x2] -> out_txt2 out commit "union" x1 x2
+ | xl -> out_txt_ out path commit ["union"] xl
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let or_fun =
+ let rec iter f = function
+ | [] -> U.mql_false
+ | head :: tail ->
+ let r1 = f head in
+ if r1 = U.mql_false then (iter f tail) else r1
+ in
+ let arity_p = Const 0 in
+ let arity_s = Any in
+ let body eval _ _ xl = iter eval xl in
+ let txt_out out path commit _ = function
+ | [x1; x2] -> out_txt2 out commit "or" x1 x2
+ | xl -> out_txt_ out path commit ["or"] xl
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let and_fun =
+ let rec iter f = function
+ | [] -> U.mql_true
+ | head :: tail ->
+ if f head = U.mql_false then U.mql_false else (iter f tail)
+ in
+ let arity_p = Const 0 in
+ let arity_s = Any in
+ let body eval _ _ xl = iter eval xl in
+ let txt_out out path commit _ = function
+ | [x1; x2] -> out_txt2 out commit "and" x1 x2
+ | xl -> out_txt_ out path commit ["and"] xl
+ in
+ {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+(* external functions interface *********************************************)
+
+let get_spec = function
+ | ["false"] -> false_fun
+ | ["true"] -> true_fun
+ | ["not"] -> not_fun
+ | ["count"] -> count_fun
+ | ["stat"] -> stat_fun
+ | ["diff"] -> diff_fun
+ | ["xor"] -> xor_fun
+ | ["sub"] -> sub_fun
+ | ["meet"] -> meet_fun
+ | ["eq"] -> eq_fun
+ | ["le"] -> le_fun
+ | ["lt"] -> lt_fun
+ | ["align"] -> align_fun
+ | ["if"] -> if_fun
+ | ["intersect"] -> intersect_fun
+ | ["union"] -> union_fun
+ | ["or"] -> or_fun
+ | ["and"] -> and_fun
+ | p -> raise (NameError p)
+
+let check_arity p m n =
+ let aux i = function
+ | Const k when i = k -> ()
+ | Positive when i > 0 -> ()
+ | Any -> ()
+ | a -> raise (ArityError (p, a, i))
+ in
+ aux m (get_spec p).arity_p; aux n (get_spec p).arity_s
+
+let exec eval h p pl xl = (get_spec p).body eval h pl xl
+
+let txt_out out path commit p pl xl =
+ try (get_spec p).txt_out out path commit pl xl
+ with NameError q when q = p -> out_txt_full out path commit p pl xl
+
+(*
+ | M.Proj (Some p) x -> out "proj "; txt_path out p; out "of "; txt_set x
+ | M.Log a b x -> out "log "; txt_log a b; txt_set x
+ | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l;
+ txt_set x
+ let txt_path_list l = P.flat_list out (txt_path out) ", " l in
+ let txt_log a b =
+ if a then out "xml ";
+ if b then out "source "
+ in
+ let txt_allbut b = if b then out "allbut " in
+
+ | M.Proj None x -> List.map (fun (r, _) -> (r, [])) (eval_query c x)
+ | M.Proj (Some p) x ->
+ let proj_group_aux (q, v) = if q = p then subj v else [] in
+ let proj_group a = U.mql_iter proj_group_aux a in
+ let proj_set (_, g) = U.mql_iter proj_group g in
+ U.mql_iter proj_set (eval_query c x)
+
+
+ | M.Log _ b x ->
+ if b then begin
+ let t = P.start_time () in
+ F.text_of_query (C.log h) x "\n";
+ let s = P.stop_time t in
+ if C.set h C.Stat then
+ C.log h (Printf.sprintf "Log source: %s\n" s);
+ eval_query c x
+ end else begin
+ let s = (eval_query c x) in
+ let t = P.start_time () in
+ F.text_of_result (C.log h) s "\n";
+ let r = P.stop_time t in
+ if C.set h C.Stat then
+ C.log h (Printf.sprintf "Log: %s\n" r);
+ s
+ end
+
+ | M.Keep b l x ->
+ let keep_path (p, v) t =
+ if List.mem p l = b then t else (p, v) :: t in
+ let keep_grp a = List.fold_right keep_path a [] in
+ let keep_set a g =
+ let kg = keep_grp a in
+ if kg = [] then g else kg :: g
+ in
+ let keep_av (s, g) = (s, List.fold_right keep_set g []) in
+ List.map keep_av (eval_query c x)
+
+
+*)
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+type arity_t = Const of int
+ | Positive
+ | Any
+
+type eval_spec = {eval : MathQL.query -> MathQL.result;
+ handle : MQIConn.handle
+ }
+
+type txt_out_spec = {out : string -> unit;
+ path : MathQL.path -> unit;
+ query : MathQL.query -> unit;
+ result : MathQL.result -> unit
+ }
+
+val check_arity : MathQL.path -> int -> int -> unit
+
+val eval : eval_spec -> txt_out_spec ->
+ MathQL.path -> MathQL.path list -> MathQL.query list ->
+ MathQL.result
+
+val txt_out : txt_out_spec ->
+ MathQL.path -> MathQL.path list -> MathQL.query list -> unit
+
+exception ArityError of MathQL.path * arity_t * int
+
+exception NameError of MathQL.path
+
+exception NumberError of MathQL.result
| head :: tail -> f head ^ sep ^ iter f sep tail
in
let pg_cols = iter (fun x -> x) ", " cols in
- let pg_msval v = iter P.quote ", " v in
+ let pg_msval v = iter (fun s, _ -> P.quote s) ", " v in
let pg_con (pat, col, v) =
if col <> "" then
- let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in
+ let f (s, _) = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in
if pat then "(" ^ iter f " or " v ^ ")"
else match v with
- | [s] -> col ^ " = " ^ (P.quote s)
+ | [(s,_)] -> col ^ " = " ^ (P.quote s)
| v -> col ^ " in (" ^ pg_msval v ^ ")"
else "true"
in
let mql_false = []
-let mql_true = [""]
+let mql_true = [("", [])]
(* set theoretic operations *************************************************)
let rec set_sub v1 v2 =
- match v1, v2 with
- | [], _ -> mql_true
- | _, [] -> mql_false
- | h1 :: _, h2 :: _ when h1 < h2 -> mql_false
- | h1 :: _, h2 :: t2 when h1 > h2 -> set_sub v1 t2
- | _ :: t1, _ :: t2 -> set_sub t1 t2
+ match (v1, v2) with
+ | [], _ -> mql_true
+ | _, [] -> mql_false
+ | (h1, _) :: _, (h2, _) :: _ when h1 < h2 -> mql_false
+ | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_sub v1 t2
+ | _ :: t1, _ :: t2 -> set_sub t1 t2
let rec set_meet v1 v2 =
match v1, v2 with
- | [], _ -> mql_false
- | _, [] -> mql_false
- | h1 :: t1, h2 :: _ when h1 < h2 -> set_meet t1 v2
- | h1 :: _, h2 :: t2 when h1 > h2 -> set_meet v1 t2
- | _, _ -> mql_true
+ | [], _
+ | _, [] -> mql_false
+ | (h1, _) :: t1, (h2, _) :: _ when h1 < h2 -> set_meet t1 v2
+ | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_meet v1 t2
+ | _, _ -> mql_true
-let set_eq v1 v2 =
- if v1 = v2 then mql_true else mql_false
+let rec set_eq v1 v2 =
+ match v1, v2 with
+ | [], [] -> mql_true
+ | (h1, _) :: t1, (h2, _) :: t2 when h1 = h2 -> set_eq t1 t2
+ | _, _ -> mql_false
let rec set_union v1 v2 =
match v1, v2 with
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
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-val mql_true : MathQL.value
+val mql_true : MathQL.result
-val mql_false : MathQL.value
+val mql_false : MathQL.result
-val set_sub : MathQL.value -> MathQL.value -> MathQL.value
+val set_sub : MathQL.result -> MathQL.result -> MathQL.result
-val set_meet : MathQL.value -> MathQL.value -> MathQL.value
+val set_meet : MathQL.result -> MathQL.result -> MathQL.result
-val set_eq : MathQL.value -> MathQL.value -> MathQL.value
+val set_eq : MathQL.result -> MathQL.result -> MathQL.result
val set_union : 'a list -> 'a list -> 'a list
-
+(*
val set_intersect : 'a list -> 'a list -> 'a list
-
+*)
val mql_union : ('a * 'b list) list -> ('a * 'b list) list ->
('a * 'b list) list
val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list ->
'd list -> ('a * 'b list) list
-val xor : MathQL.value -> MathQL.value -> MathQL.value
-
-val le : MathQL.value -> MathQL.value -> MathQL.value
-
-val lt : MathQL.value -> MathQL.value -> MathQL.value
-
-val align : string -> string -> MathQL.value
+val xor : MathQL.result -> MathQL.result -> MathQL.result
-val set : string * 'a -> (string * 'a) list -> (string * 'a) list
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+module M = MathQL
+module P = MQueryUtil
+module L = MQILib
+
+(* text linearization and parsing *******************************************)
+
+let txt_str out s = out ("\"" ^ s ^ "\"")
+
+let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p
+
+let text_of_result out x sep =
+ let txt_attr = function
+ | (p, []) -> txt_path out p
+ | (p, l) -> txt_path out p; out " = ";
+ P.flat_list out (txt_str out) ", " l
+ in
+ let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in
+ let txt_res = function
+ | (s, []) -> txt_str out s
+ | (s, l) -> txt_str out s; out " attr ";
+ P.flat_list out txt_group ", " l
+ in
+ let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in
+ txt_set x
+
+let text_of_query out x sep =
+ let txt_svar sv = out ("%" ^ sv) in
+ let txt_avar av = out ("@" ^ av) in
+ let txt_inv i = if i then out "inverse " in
+ let txt_ref = function
+ | M.RefineExact -> ()
+ | M.RefineSub -> out "sub "
+ | M.RefineSuper -> out "super "
+ in
+ let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in
+ let main = function
+ | [] -> ()
+ | p -> out " main "; txt_path out p
+ in
+ let txt_exp = function
+ | (pl, None) -> txt_path out pl
+ | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr
+ in
+ let txt_exp_list = function
+ | [] -> ()
+ | l -> out " attr "; P.flat_list out txt_exp ", " l
+ in
+ let pattern b = if b then out "pattern " in
+ let txt_distr d = if d then out "distr " in
+ let txt_gen = function
+ | M.GenFJoin -> out " sup "
+ | M.GenFMeet -> out " inf "
+ in
+ let rec txt_con (pat, p, x) =
+ txt_path out p;
+ if pat then out " match " else out " in ";
+ txt_set x
+ and txt_con_list s = function
+ | [] -> ()
+ | l -> out s; P.flat_list out txt_con ", " l
+ and txt_istrue lt = txt_con_list " istrue " lt
+ and txt_isfalse lf = txt_con_list " isfalse " lf
+ and txt_ass (p, x) = txt_set x; out " as "; txt_path out p
+ and txt_ass_list l = P.flat_list out txt_ass ", " l
+ and txt_assg_list g = P.flat_list out txt_ass_list "; " g
+ and txt_grp = function
+ | M.Attr g -> txt_assg_list g
+ | M.From av -> txt_avar av
+ and txt_set = function
+ | M.Fun p pl xl ->
+ L.txt_out out (txt_path out) txt_set p pl xl
+ | M.Const [s, []] -> txt_str out s
+ | M.Const r -> text_of_result out r " "
+ | M.Dot av p -> txt_avar av; out "."; txt_path out p
+ | M.Ex b x -> out "ex "; txt_set x
+(* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b;
+ out "] "; txt_set x
+*) | M.SVar sv -> txt_svar sv
+ | M.AVar av -> txt_avar av
+ | M.Property q0 q1 q2 mc ct cfl xl b x ->
+ out "property "; txt_qualif q0 q1 q2; main mc;
+ txt_istrue ct; P.flat_list out txt_isfalse "" cfl; txt_exp_list xl;
+ out " of "; pattern b; txt_set x
+ | M.Let sv x y -> out "let "; txt_svar sv; out " be ";
+ txt_set x; out " in "; txt_set y
+ | M.Select av x y -> out "select "; txt_avar av; out " from ";
+ txt_set x; out " where "; txt_set y
+ | M.For k av x y -> out "for "; txt_avar av; out " in ";
+ txt_set x; txt_gen k; txt_set y
+ | M.Add d g x -> out "add "; txt_distr d; txt_grp g;
+ out " in "; txt_set x
+ in
+ txt_set x; out sep
+
+let query_of_text lexbuf =
+ MQueryTParser.query MQueryTLexer.query_token lexbuf
+
+let result_of_text lexbuf =
+ MQueryTParser.result MQueryTLexer.result_token lexbuf
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val text_of_query : (string -> unit) -> MathQL.query -> string -> unit
+
+val text_of_result : (string -> unit) -> MathQL.result -> string -> unit
+
+val query_of_text : Lexing.lexbuf -> MathQL.query
+
+val result_of_text : Lexing.lexbuf -> MathQL.result
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-(* contexts *****************************************************************)
+exception Found
-type svar_context = (MathQL.svar * MathQL.resource_set) list
+module M = MathQL
+module P = MQueryUtil
+module C = MQIConn
+module U = MQIUtil
+module L = MQILib
+module F = MQueryIO
-type avar_context = (MathQL.avar * MathQL.resource) list
+(* contexts *****************************************************************)
-type group_context = (MathQL.avar * MathQL.attribute_group) list
+type svar_context = (M.svar * M.resource_set) list
-type vvar_context = (MathQL.vvar * MathQL.value) list
+type avar_context = (M.avar * M.resource) list
+
+type group_context = (M.avar * M.attribute_group) list
type context = {svars: svar_context;
avars: avar_context;
- groups: group_context; (* auxiliary context *)
- vvars: vvar_context
+ groups: group_context (* auxiliary context *)
}
-
-(* execute *****************************************************************)
-
-exception Found
-
-module M = MathQL
-module P = MQueryUtil
-module C = MQIConn
-module U = MQIUtil
+
+(* execute ******************************************************************)
let execute h x =
let warn q =
if C.set h C.Warn then
begin
C.log h "MQIExecute: waring: reference to undefined variables: ";
- P.text_of_query (C.log h) q "\n"
+ F.text_of_query (C.log h) q "\n"
end
in
- let rec eval_val c = function
- | M.False -> U.mql_false
- | M.True -> U.mql_true
- | M.Const s -> [s]
- | M.Set l -> U.iter (eval_val c) l
- | M.Test k y1 y2 ->
- let cand y1 y2 =
- if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2
- in
- let cor y1 y2 =
- let v1 = eval_val c y1 in
- if v1 = U.mql_false then eval_val c y2 else v1
- in
- let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in
- let f = match k with
- | M.And -> cand
- | M.Or -> cor
- | M.Xor -> h U.xor
- | M.Sub -> h U.set_sub
- | M.Meet -> h U.set_meet
- | M.Eq -> h U.set_eq
- | M.Le -> h U.le
- | M.Lt -> h U.lt
- in
- f y1 y2
- | M.Not y ->
- if eval_val c y = U.mql_false then U.mql_true else U.mql_false
- | M.VVar i -> begin
- try List.assoc i c.vvars
- with Not_found -> warn (M.Subj (M.VVar i)); [] end
+ let subj v = List.map (fun s -> (s, [])) v in
+ let proj v = List.map fst v in
+ let rec eval_query c = function
+ | M.Const r -> r
| M.Dot i p -> begin
- try List.assoc p (List.assoc i c.groups)
- with Not_found -> warn (M.Subj (M.Dot i p)); [] end
- | M.Proj None x -> List.map (fun (r, _) -> r) (eval_query c x)
- | M.Proj (Some p) x ->
- let proj_group_aux (q, v) = if q = p then v else [] in
- let proj_group a = U.iter proj_group_aux a in
- let proj_set (_, g) = U.iter proj_group g in
- U.iter proj_set (eval_query c x)
+ try subj (List.assoc p (List.assoc i c.groups))
+ with Not_found -> warn (M.Dot i p); [] end
| M.Ex l y ->
let rec ex_aux h = function
| [] ->
let d = {c with groups = h} in
- if eval_val d y = U.mql_false then () else raise Found
+ if eval_query d y = U.mql_false then () else raise Found
| i :: tail ->
begin
try
end
in
(try ex_aux [] l; U.mql_false with Found -> U.mql_true)
- | M.StatVal y ->
- let t = P.start_time () in
- let r = (eval_val c y) in
- let s = P.stop_time t in
- C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
- r
- | M.Count y -> [string_of_int (List.length (eval_val c y))]
- | M.Align s y -> U.iter (U.align s) (eval_val c y)
- and eval_query c = function
- | M.Empty -> []
- | M.Subj x ->
- List.map (fun s -> (s, [])) (eval_val c x)
- | M.Log _ b x ->
- if b then begin
- let t = P.start_time () in
- P.text_of_query (C.log h) x "\n";
- let s = P.stop_time t in
- if C.set h C.Stat then
- C.log h (Printf.sprintf "Log source: %s\n" s);
- eval_query c x
- end else begin
- let s = (eval_query c x) in
- let t = P.start_time () in
- P.text_of_result (C.log h) s "\n";
- let r = P.stop_time t in
- if C.set h C.Stat then
- C.log h (Printf.sprintf "Log: %s\n" r);
- s
- end
- | M.If y x1 x2 ->
- if (eval_val c y) = U.mql_false
- then (eval_query c x2) else (eval_query c x1)
- | M.Bin k x1 x2 ->
- let f = match k with
- | M.BinFJoin -> U.mql_union
- | M.BinFMeet -> U.mql_intersect
- | M.BinFDiff -> U.mql_diff
- in
- f (eval_query c x1) (eval_query c x2)
| M.SVar i -> begin
try List.assoc i c.svars
with Not_found -> warn (M.SVar i); [] end
| M.AVar i -> begin
try [List.assoc i c.avars]
with Not_found -> warn (M.AVar i); [] end
- | M.LetSVar i x1 x2 ->
- let d = {c with svars = U.set (i, eval_query c x1) c.svars} in
+ | M.Let i x1 x2 ->
+ let d = {c with svars = P.add_assoc (i, eval_query c x1) c.svars} in
eval_query d x2
- | M.LetVVar i y x ->
- let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in
- eval_query d x
| M.For k i x1 x2 ->
let f = match k with
| M.GenFJoin -> U.mql_union
let rec for_aux = function
| [] -> []
| h :: t ->
- let d = {c with avars = U.set (i, h) c.avars} in
+ let d = {c with avars = P.add_assoc (i, h) c.avars} in
f (eval_query d x2) (for_aux t)
in
for_aux (eval_query c x1)
List.fold_right g (eval_query c x) []
| M.Property q0 q1 q2 mc ct cfl el pat y ->
let subj, mct =
- if q0 then [], (pat, q2 @ mc, eval_val c y)
- else (q2 @ mc), (pat, [], eval_val c y)
+ if q0 then [], (pat, q2 @ mc, eval_query c y)
+ else (q2 @ mc), (pat, [], eval_query c y)
in
- let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in
+ let eval_cons (pat, p, y) = (pat, q2 @ p, eval_query c y) in
let cons_true = mct :: List.map eval_cons ct in
let cons_false = List.map (List.map eval_cons) cfl in
let eval_exp (p, po) = (q2 @ p, po) in
if C.set h C.Stat then
C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
r
- | M.StatQuery x ->
- let t = P.start_time () in
- let r = (eval_query c x) in
- let s = P.stop_time t in
- C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
- r
| M.Select i x y ->
let rec select_aux = function
| [] -> []
| h :: t ->
- let d = {c with avars = U.set (i, h) c.avars} in
- if eval_val d y = U.mql_false
+ let d = {c with avars = P.add_assoc (i, h) c.avars} in
+ if eval_query d y = U.mql_false
then select_aux t else h :: select_aux t
in
select_aux (eval_query c x)
- | M.Keep b l x ->
- let keep_path (p, v) t =
- if List.mem p l = b then t else (p, v) :: t in
- let keep_grp a = List.fold_right keep_path a [] in
- let keep_set a g =
- let kg = keep_grp a in
- if kg = [] then g else kg :: g
- in
- let keep_av (s, g) = (s, List.fold_right keep_set g []) in
- List.map keep_av (eval_query c x)
+ | M.Fun p pl xl -> L.exec (eval_query c) h p pl xl
and eval_grp c = function
| M.Attr gs ->
- let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] in
+ let attr_aux g (p, y) = U.mql_union g [p, proj (eval_query c y)] in
let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
List.fold_left attr_auxs [] gs
| M.From i ->
try snd (List.assoc i c.avars)
with Not_found -> warn (M.AVar i); []
in
- let c = {svars = []; avars = []; groups = []; vvars = []} in
+ let c = {svars = []; avars = []; groups = []} in
let t = P.start_time () in
let r = eval_query c x in
let s = P.stop_time t in
out ("STR " ^ str); STR str }
| '(' { out "LP"; LP }
| ')' { out "RP"; RP }
+ | '[' { out "LB"; LB }
+ | ']' { out "RB"; RB }
| '{' { out "LC"; LC }
| '}' { out "RC"; RC }
| '@' { out "AT"; AT }
| '%' { out "PC"; PC }
- | '$' { out "DL"; DL }
| '.' { out "FS"; FS }
| ',' { out "CM"; CM }
| ';' { out "SC"; SC }
| "source" { out "SOURCE"; SOURCE }
| "stat" { out "STAT" ; STAT }
| "sub" { out "SUB" ; SUB }
- | "subj" { out "SUBJ" ; SUBJ }
| "sup" { out "SUP" ; SUP }
| "super" { out "SUPER" ; SUPER }
| "then" { out "THEN" ; THEN }
%{
module M = MathQL
+ module L = MQILib
+
+ let make_fun p pl xl =
+ L.check_arity p (List.length pl) (List.length xl);
+ M.Fun p pl xl
let analyze x =
let rec join l1 l2 = match l1, l2 with
| [] -> []
| head :: tail -> join (f head) (iter f tail)
in
- let rec an_val = function
- | M.True -> []
- | M.False -> []
- | M.Const _ -> []
- | M.VVar _ -> []
- | M.Ex _ -> []
- | M.Dot rv _ -> [rv]
- | M.Not x -> an_val x
- | M.StatVal x -> an_val x
- | M.Count x -> an_val x
- | M.Align _ x -> an_val x
- | M.Proj _ x -> an_set x
- | M.Test _ x y -> iter an_val [x; y]
- | M.Set l -> iter an_val l
- and an_set = function
- | M.Empty -> []
- | M.SVar _ -> []
- | M.AVar _ -> []
- | M.Subj x -> an_val x
- | M.Keep _ _ x -> an_set x
- | M.Log _ _ x -> an_set x
- | M.StatQuery x -> an_set x
- | M.Bin _ x y -> iter an_set [x; y]
- | M.LetSVar _ x y -> iter an_set [x; y]
+ let rec an_set = function
+ | M.Const _
+ | M.SVar _
+ | M.AVar _
+ | M.Ex _ -> []
+ | M.Dot rv _ -> [rv]
+ | M.Let _ x y
+ | M.Select _ x y
| M.For _ _ x y -> iter an_set [x; y]
+ | M.Fun _ _ l -> iter an_set l
| M.Add _ g x -> join (an_grp g) (an_set x)
- | M.LetVVar _ x y -> join (an_val x) (an_set y)
- | M.Select _ x y -> join (an_set x) (an_val y)
| M.Property _ _ _ _ c d _ _ x ->
- join (an_val x) (iter an_con [c; List.concat d])
- | M.If x y z -> join (an_val x) (iter an_set [y; z])
- and fc (_, _, v) = an_val v
+ join (an_set x) (iter an_con [c; List.concat d])
+ and fc (_, _, v) = an_set v
and an_con c = iter fc c
- and fg (_, v) = an_val v
+ and fg (_, v) = an_set v
and an_grp = function
| M.Attr g -> iter (iter fg) g
| M.From _ -> []
in
- an_val x
+ an_set x
let f (x, y, z) = x
let s (x, y, z) = y
let t (x, y, z) = z
%}
%token <string> ID STR
- %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF
+ %token LB RB SL IS LC RC CM SC LP RP AT PC FS DQ EOF
%token ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX
%token FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT
%token MAIN MATCH MEET NOT OF OR PAT PROJ PROP SELECT SOURCE STAT SUB
- %token SUBJ SUP SUPER THEN TRUE UNION WHERE XOR
- %nonassoc IN SUP INF ELSE LOG STAT
+ %token SUP SUPER THEN TRUE UNION WHERE XOR
+ %nonassoc IN SUP INF ELSE LOG STAT KEEP
%left DIFF
%left UNION
%left INTER
%left AND
%nonassoc NOT
%nonassoc SUB MEET EQ LT LE
- %nonassoc SUBJ OF PROJ COUNT ALIGN
+ %nonassoc OF PROJ COUNT ALIGN
%start qstr query result
%type <string> qstr
avar:
| AT ID { $2 }
;
- vvar:
- | DL ID { $2 }
- ;
strs:
| STR CM strs { $1 :: $3 }
| STR { [$1] }
| STR { [$1] }
;
path:
- | subpath { $1 }
| SL subpath { $2 }
| SL { [] }
;
| inv ref path { $1, $2, $3 }
;
cons:
- | path IN val_exp { (false, $1, $3) }
- | path MATCH val_exp { (true, $1, $3) }
+ | path IN set_exp { (false, $1, $3) }
+ | path MATCH set_exp { (true, $1, $3) }
;
conss:
| cons CM conss { $1 :: $3 }
| PAT { true }
| { false }
;
- opt_path:
- | path { Some $1 }
- | { None }
- ;
ass:
- | val_exp AS path { ($3, $1) }
+ | set_exp AS path { ($3, $1) }
;
asss:
| ass CM asss { $1 :: $3 }
| { false }
;
allbut:
- | BUT { true }
- | { false }
- ;
- bin_op:
- | set_exp DIFF set_exp { M.BinFDiff, $1, $3 }
- | set_exp UNION set_exp { M.BinFJoin, $1, $3 }
- | set_exp INTER set_exp { M.BinFMeet, $1, $3 }
+ | BUT { "allbut" }
+ | { "these" }
;
gen_op:
| SUP set_exp { M.GenFJoin, $2 }
| INF set_exp { M.GenFMeet, $2 }
;
- test_op:
- | val_exp XOR val_exp { M.Xor, $1, $3 }
- | val_exp OR val_exp { M.Or, $1, $3 }
- | val_exp AND val_exp { M.And, $1, $3 }
- | val_exp SUB val_exp { M.Sub, $1, $3 }
- | val_exp MEET val_exp { M.Meet, $1, $3 }
- | val_exp EQ val_exp { M.Eq, $1, $3 }
- | val_exp LE val_exp { M.Le, $1, $3 }
- | val_exp LT val_exp { M.Lt, $1, $3 }
- ;
source:
- | SOURCE { true }
- | { false }
+ | SOURCE { "source" }
+ | { "result" }
;
xml:
- | { false}
+ | { "text" }
;
grp_exp:
| assg { M.Attr $1 }
| avar { M.From $1 }
;
- val_exp:
- | TRUE { M.True }
- | FALSE { M.False }
- | STR { M.Const $1 }
- | avar FS path { M.Dot $1 $3 }
- | vvar { M.VVar $1 }
- | LC vals RC { M.Set $2 }
- | LC RC { M.Set [] }
- | LP val_exp RP { $2 }
- | STAT val_exp { M.StatVal $2 }
- | EX val_exp { M.Ex (analyze $2) $2 }
- | NOT val_exp { M.Not $2 }
- | test_op { M.Test (f $1) (s $1) (t $1) }
- | PROJ opt_path set_exp { M.Proj $2 $3 }
- | COUNT val_exp { M.Count $2 }
- | ALIGN STR IN val_exp { M.Align $2 $4 }
- ;
- vals:
- | val_exp CM vals { $1 :: $3 }
- | val_exp { [$1] }
- ;
set_exp:
- | EMPTY { M.Empty }
- | LP set_exp RP { $2 }
- | svar { M.SVar $1 }
- | avar { M.AVar $1 }
- | LET svar BE set_exp IN set_exp { M.LetSVar $2 $4 $6 }
- | LET vvar BE val_exp IN set_exp { M.LetVVar $2 $4 $6 }
+ | FALSE
+ { make_fun ["false"] [] [] }
+ | TRUE
+ { make_fun ["true"] [] [] }
+ | STR
+ { M.Const [$1, []] }
+ | LB resources RB
+ { M.Const $2 }
+ | avar FS path
+ { M.Dot $1 $3 }
+ | LC sets RC
+ { make_fun ["union"] [] $2 }
+ | LC RC
+ { make_fun ["union"] [] [] }
+ | LP set_exp RP
+ { $2 }
+ | STAT set_exp
+ { make_fun ["stat"] [] [$2] }
+ | EX set_exp
+ { M.Ex (analyze $2) $2 }
+ | NOT set_exp
+ { make_fun ["not"] [] [$2] }
+ | PROJ path OF set_exp
+ { make_fun ["proj"] [$2] [$4] }
+ | COUNT set_exp
+ { make_fun ["count"] [] [$2] }
+ | ALIGN set_exp IN set_exp
+ { make_fun ["align"] [] [$2; $4] }
+ | EMPTY
+ { make_fun ["false"] [] [] }
+ | svar
+ { M.SVar $1 }
+ | avar
+ { M.AVar $1 }
+ | LET svar BE set_exp IN set_exp
+ { M.Let $2 $4 $6 }
| FOR avar IN set_exp gen_op
{ M.For (fst $5) $2 $4 (snd $5) }
- | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 }
- | IF val_exp THEN set_exp ELSE set_exp { M.If $2 $4 $6 }
- | PROP qualif mainc istrue isfalse attrc OF pattern val_exp
+ | ADD distr grp_exp IN set_exp
+ { M.Add $2 $3 $5 }
+ | IF set_exp THEN set_exp ELSE set_exp
+ { make_fun ["diff"] [] [$2; $4; $6] }
+ | PROP qualif mainc istrue isfalse attrc OF pattern set_exp
{ M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 }
- | LOG xml source set_exp { M.Log $2 $3 $4 }
- | STAT set_exp { M.StatQuery $2 }
- | KEEP allbut paths IN set_exp { M.Keep $2 $3 $5 }
- | KEEP allbut IN set_exp { M.Keep $2 [] $4 }
- | bin_op
- { M.Bin (f $1) (s $1) (t $1) }
- | SELECT avar FROM set_exp WHERE val_exp { M.Select $2 $4 $6 }
- | SUBJ val_exp { M.Subj $2 }
+ | LOG xml source set_exp
+ { make_fun ["log"; $2; $3] [] [$4] }
+ | KEEP allbut paths IN set_exp
+ { make_fun ["keep"; $2] $3 [$5] }
+ | KEEP allbut set_exp
+ { make_fun ["keep"; $2] [] [$3] }
+ | SELECT avar FROM set_exp WHERE set_exp
+ { M.Select $2 $4 $6 }
+ | path LC paths RC LC sets RC
+ { make_fun $1 $3 $6 }
+ | path LC sets RC
+ { make_fun $1 [] $3 }
+ | path LC RC
+ { make_fun $1 [] [] }
+ | set_exp DIFF set_exp
+ { make_fun ["diff"] [] [$1; $3] }
+ | set_exp UNION set_exp
+ { make_fun ["union"] [] [$1; $3] }
+ | set_exp INTER set_exp
+ { make_fun ["intersect"] [] [$1; $3] }
+ | set_exp XOR set_exp
+ { make_fun ["xor"] [] [$1; $3] }
+ | set_exp OR set_exp
+ { make_fun ["or"] [] [$1; $3] }
+ | set_exp AND set_exp
+ { make_fun ["and"] [] [$1; $3] }
+ | set_exp SUB set_exp
+ { make_fun ["sub"] [] [$1; $3] }
+ | set_exp MEET set_exp
+ { make_fun ["meet"] [] [$1; $3] }
+ | set_exp EQ set_exp
+ { make_fun ["eq"] [] [$1; $3] }
+ | set_exp LE set_exp
+ { make_fun ["le"] [] [$1; $3] }
+ | set_exp LT set_exp
+ { make_fun ["lt"] [] [$1; $3] }
+ ;
+ sets:
+ | set_exp CM sets { $1 :: $3 }
+ | set_exp { [$1] }
;
query:
| set_exp { $1 }
| { [] }
;
result:
- | resources { $1 }
- | EOF { raise End_of_file }
+ | resources { $1 }
+ | resources error { $1 }
+ | EOF { raise End_of_file }
+++ /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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* text linearization and parsing *******************************************)
-
-let rec txt_list out f s = function
- | [] -> ()
- | [a] -> f a
- | a :: tail -> f a; out s; txt_list out f s tail
-
-let txt_str out s = out ("\"" ^ s ^ "\"")
-
-let txt_path out p = out "/"; txt_list out (txt_str out) "/" p
-
-let text_of_query out x sep =
- let module M = MathQL in
- let txt_path_list l = txt_list out (txt_path out) ", " l in
- let txt_svar sv = out ("%" ^ sv) in
- let txt_avar av = out ("@" ^ av) in
- let txt_vvar vv = out ("$" ^ vv) in
- let txt_inv i = if i then out "inverse " in
- let txt_ref = function
- | M.RefineExact -> ()
- | M.RefineSub -> out "sub "
- | M.RefineSuper -> out "super "
- in
- let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in
- let main = function
- | [] -> ()
- | p -> out " main "; txt_path out p
- in
- let txt_exp = function
- | (pl, None) -> txt_path out pl
- | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr
- in
- let txt_exp_list = function
- | [] -> ()
- | l -> out " attr "; txt_list out txt_exp ", " l
- in
- let pattern b = if b then out "pattern " in
- let txt_opt_path = function
- | None -> ()
- | Some p -> txt_path out p; out " "
- in
- let txt_distr d = if d then out "distr " in
- let txt_bin = function
- | M.BinFJoin -> out " union "
- | M.BinFMeet -> out " intersect "
- | M.BinFDiff -> out " diff "
- in
- let txt_gen = function
- | M.GenFJoin -> out " sup "
- | M.GenFMeet -> out " inf "
- in
- let txt_test = function
- | M.Xor -> out " xor "
- | M.Or -> out " or "
- | M.And -> out " and "
- | M.Sub -> out " sub "
- | M.Meet -> out " meet "
- | M.Eq -> out " eq "
- | M.Le -> out " le "
- | M.Lt -> out " lt "
- in
- let txt_log a b =
- if a then out "xml ";
- if b then out "source "
- in
- let txt_allbut b = if b then out "allbut " in
- let rec txt_con (pat, p, x) =
- txt_path out p;
- if pat then out " match " else out " in ";
- txt_val x
- and txt_con_list s = function
- | [] -> ()
- | l -> out s; txt_list out txt_con ", " l
- and txt_istrue lt = txt_con_list " istrue " lt
- and txt_isfalse lf = txt_con_list " isfalse " lf
- and txt_ass (p, x) = txt_val x; out " as "; txt_path out p
- and txt_ass_list l = txt_list out txt_ass ", " l
- and txt_assg_list g = txt_list out txt_ass_list "; " g
- and txt_val_list = function
- | [v] -> txt_val v
- | l -> out "{"; txt_list out txt_val ", " l; out "}"
- and txt_grp = function
- | M.Attr g -> txt_assg_list g
- | M.From av -> txt_avar av
- and txt_val = function
- | M.True -> out "true"
- | M.False -> out "false"
- | M.Const s -> txt_str out s
- | M.Set l -> txt_val_list l
- | M.VVar vv -> txt_vvar vv
- | M.Dot av p -> txt_avar av; out "."; txt_path out p
- | M.Proj op x -> out "proj "; txt_opt_path op; txt_set x
- | M.Ex b x -> out "ex "; txt_val x
-(* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x
-*) | M.Not x -> out "not "; txt_val x
- | M.Test k x y -> out "("; txt_val x; txt_test k; txt_val y; out ")"
- | M.StatVal x -> out "stat "; txt_val x
- | M.Count x -> out "count "; txt_val x
- | M.Align s x -> out "align "; txt_str out s; out " in "; txt_val x
- and txt_set = function
- | M.Empty -> out "empty"
- | M.SVar sv -> txt_svar sv
- | M.AVar av -> txt_avar av
- | M.Property q0 q1 q2 mc ct cfl xl b x ->
- out "property "; txt_qualif q0 q1 q2; main mc;
- txt_istrue ct; txt_list out txt_isfalse "" cfl; txt_exp_list xl;
- out " of "; pattern b; txt_val x
- | M.Bin k x y -> out "("; txt_set x; txt_bin k; txt_set y;
- out ")"
- | M.LetSVar sv x y -> out "let "; txt_svar sv; out " be ";
- txt_set x; out " in "; txt_set y
- | M.LetVVar vv x y -> out "let "; txt_vvar vv; out " be ";
- txt_val x; out " in "; txt_set y
- | M.Select av x y -> out "select "; txt_avar av; out " from ";
- txt_set x; out " where "; txt_val y
- | M.Subj x -> out "subj "; txt_val x
- | M.For k av x y -> out "for "; txt_avar av; out " in ";
- txt_set x; txt_gen k; txt_set y
- | M.If x y z -> out "if "; txt_val x; out " then ";
- txt_set y; out " else "; txt_set z
- | M.Add d g x -> out "add "; txt_distr d; txt_grp g;
- out " in "; txt_set x
- | M.Log a b x -> out "log "; txt_log a b; txt_set x
- | M.StatQuery x -> out "stat "; txt_set x
- | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l;
- txt_set x
- in
- txt_set x; out sep
-
-let text_of_result out x sep =
- let txt_attr = function
- | (p, []) -> txt_path out p
- | (p, l) -> txt_path out p; out " = "; txt_list out (txt_str out) ", " l
- in
- let txt_group l = out "{"; txt_list out txt_attr "; " l; out "}" in
- let txt_res = function
- | (s, []) -> txt_str out s
- | (s, l) -> txt_str out s; out " attr "; txt_list out txt_group ", " l
- in
- let txt_set l = txt_list out txt_res ("; " ^ sep) l; out sep in
- txt_set x
-
-let query_of_text lexbuf =
- MQueryTParser.query MQueryTLexer.query_token lexbuf
-
-let result_of_text lexbuf =
- MQueryTParser.result MQueryTLexer.result_token lexbuf
-
-(* time handling ***********************************************************)
-
-type time = float * float
-
-let start_time () =
- (Sys.time (), Unix.time ())
-
-let stop_time (s0, u0) =
- let s1 = Sys.time () in
- let u1 = Unix.time () in
- Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0)
-
-(* operations on lists *****************************************************)
-
-type 'a comparison = Lt
- | Gt
- | Eq of 'a
-
-let list_join f l1 l2 =
- let rec aux = function
- | [], v
- | v, [] -> v
- | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
- match f h1 h2 with
- | Lt -> h1 :: aux (t1, v2)
- | Gt -> h2 :: aux (v1, t2)
- | Eq h -> h :: aux (t1, t2)
- end
- in aux (l1, l2)
-
-let list_meet f l1 l2 =
- let rec aux = function
- | [], v
- | v, [] -> []
- | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
- match f h1 h2 with
- | Lt -> aux (t1, v2)
- | Gt -> aux (v1, t2)
- | Eq h -> h :: aux (t1, t2)
- end
- in aux (l1, l2)
-
+++ /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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val text_of_query : (string -> unit) -> MathQL.query -> string -> unit
-
-val text_of_result : (string -> unit) -> MathQL.result -> string -> unit
-
-val query_of_text : Lexing.lexbuf -> MathQL.query
-
-val result_of_text : Lexing.lexbuf -> MathQL.result
-
-type time
-
-val start_time : unit -> time
-
-val stop_time : time -> string
-
-type 'a comparison = Lt
- | Gt
- | Eq of 'a
-
-val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list
-
-val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list
projects / helm.git / commitdiff