+mqgtop.cmo: mQGTopLexer.cmo mQGTopParser.cmi
+mqgtop.cmx: mQGTopLexer.cmx mQGTopParser.cmx
mQGTopParser.cmo: mQGTopParser.cmi
mQGTopParser.cmx: mQGTopParser.cmi
mQGTopLexer.cmo: mQGTopParser.cmi
BIN_DIR = /usr/local/bin
-REQUIRES = unix helm-cic_textual_parser \
- helm-mathql helm-mathql_interpreter helm-mathql_generator
+REQUIRES = unix helm-cic_textual_parser helm-cic_proof_checking \
+ helm-mathql helm-mathql_interpreter helm-mathql_generator \
+ helm-tactics
PREDICATES =
OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+let _ = MQueryStandard.init
+let _ = MQueryHELM.init
+
let query_num = ref 1
let interp_file = ref "interp.cic"
module C2 = CGSearchPattern
module C1 = CGMatchConclusion
module GU = MQGUtil
+module M = MQueryMisc
let get_handle () =
C.init (C.flags_of_string ! int_options)
in
aux ()
-let pp_type_of uri =
- let u = UriManager.uri_of_string uri in
- let s = match (CicEnvironment.get_obj u) with
- | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
- | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
- | _ -> "Current proof or inductive definition."
-(*
- | Cic.CurrentProof (_,conjs,te,ty) ->
- | C.InductiveDefinition _ ->
-*)
+let pp_term_of b uri =
+ let s = try
+ let body, ty = M.get_object (M.uriref_of_string uri) in
+ if b then CicPp.ppterm body else CicPp.ppterm ty
+ with
+ | M.CurrentProof -> "proof in progress"
+ | M.InductiveDefinition -> "inductive definition"
+ | M.IllFormedFragment -> "ill formed fragment identifier"
in print_endline s; flush stdout
let rec display = function
prerr_endline "-o -options STRING sets the interpreter options";
prerr_endline "-c -check checks the database connection";
prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object";
+ prerr_endline "-b -bodyof URI outputs the CIC body of the given HELM object";
prerr_endline "-x -execute issues a query given in the input file";
prerr_endline "-i -interp FILE sets the CIC short names interpretation file";
prerr_endline "-d -disply outputs the CIC terms given in the input file";
prerr_endline "NOTES: * current interpreter options are:";
prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)";
prerr_endline " * CIC terms are read with the HELM CIC Textual Parser";
- prerr_endline " * -typeof does not work with inductive types and proofs in progress\n"
+ prerr_endline " * -typeof / -bodyof do not work with proofs in progress\n"
let rec parse = function
| [] -> ()
| ("-h"|"-help") :: rem -> prerr_help (); parse rem
| ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
| ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
- | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
+ | ("-t"|"-typeof") :: arg :: rem -> pp_term_of false arg; parse rem
+ | ("-b"|"-bodyof") :: arg :: rem -> pp_term_of true arg; parse rem
| ("-x"|"-execute") :: rem -> execute stdin; parse rem
| ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
| ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
let _ =
let t = U.start_time () in
- Logger.log_callback :=
+(* Logger.log_callback :=
(Logger.log_to_html
~print_and_flush:(fun s -> print_string s; flush stdout)) ;
- parse (List.tl (Array.to_list Sys.argv));
+*) parse (List.tl (Array.to_list Sys.argv));
prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
exit 0
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-module U = MQueryUtil
+let _ = MQueryStandard.init
+let _ = MQueryHELM.init
+
+module P = MQueryUtil
+module U = AvsUtil
module I = MQueryInterpreter
module C = MQIConn
module F = MQueryIO
let _ =
- let t = U.start_time () in
+ let t = P.start_time () in
let ich = Lexing.from_channel stdin in
let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in
let log s = print_string s; flush stdout in
print_endline "mqitop: no connection"; flush stdout
end;
let rec aux () =
- let t = U.start_time () in
+ let t = P.start_time () in
let r = I.execute handle (F.query_of_text ich) in
(* F.text_of_result log r "\n";
-*) Printf.eprintf "mqitop: query: %s,%i\n" (U.stop_time t) (List.length r);
+*) Printf.eprintf "mqitop: query: %s,%i\n" (P.stop_time t) (U.count r);
flush stderr; aux()
in
begin try aux() with End_of_file -> () end;
C.close handle;
- Printf.eprintf "mqitop: done: %s\n" (U.stop_time t)
+ Printf.eprintf "mqitop: done: %s\n" (P.stop_time t)
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+let _ = MQueryStandard.init
+let _ = MQueryHELM.init
+
let _ =
let module U = MQueryUtil in
let module F = MQueryIO in
+listAvs.cmi: avs.cmo
+avsUtil.cmi: mathQL.cmo
+listAvs.cmo: avs.cmo listAvs.cmi
+listAvs.cmx: avs.cmx listAvs.cmi
+mathQL.cmo: avs.cmo listAvs.cmi
+mathQL.cmx: avs.cmx listAvs.cmx
+avsUtil.cmo: mathQL.cmo avsUtil.cmi
+avsUtil.cmx: mathQL.cmx avsUtil.cmi
mQueryUtil.cmo: mQueryUtil.cmi
mQueryUtil.cmx: mQueryUtil.cmi
PREDICATES =
-INTERFACE_FILES = mQueryUtil.mli
+INTERFACE_FILES = mQueryUtil.mli listAvs.mli avsUtil.mli
-IMPLEMENTATION_FILES = mathQL.ml mQueryUtil.ml
+IMPLEMENTATION_FILES = mQueryUtil.ml avs.ml listAvs.ml mathQL.ml avsUtil.ml
-EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi
+EXTRA_OBJECTS_TO_INSTALL = avs.ml avs.cmi mathQL.ml mathQL.cmi
EXTRA_OBJECTS_TO_CLEAN =
--- /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://www.cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+type value = string list (* a linearized attribute value *)
+
+type path = string list (* the name of an attribute *)
+
+module type Type = sig
+
+ type group (* an group of attribures *)
+
+ type avs (* a set of attributed values *)
+
+ type peek_t = Empty
+ | Single of (string * group list)
+ | Many of (string * group list)
+
+
+ val grp_empty : group
+
+ val grp_make : path -> string -> group
+
+ val grp_union : group -> group -> group
+
+ val grp_read : group -> path -> avs
+
+ val grps_make : group list -> group -> group list
+
+ val empty : avs
+
+ val make : string -> group -> avs
+
+ val iter : ('a -> string -> bool -> 'a) -> 'a -> avs -> 'a
+
+ val x_iter : ('a -> string -> group list -> bool -> 'a) ->
+ 'a -> avs -> 'a
+
+ val x_grp_iter : ('a -> path -> value -> bool -> 'a) -> 'a -> group -> 'a
+
+ val single : avs -> string option
+
+ val sub : avs -> avs -> bool
+
+ val meet : avs -> avs -> bool
+
+ val eq : avs -> avs -> bool
+
+ val union : avs -> avs -> avs (* without attr. distribution *)
+
+ val intersect : avs -> avs -> avs (* without attr. distribution *)
+
+ val diff : avs -> avs -> avs
+
+ val append : avs -> avs -> avs
+
+ val d_union : avs -> avs -> avs (* with attr. distribution *)
+
+ val peek : avs -> peek_t
+
+end
--- /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 I = MathQL.I
+
+(* strings ******************************************************************)
+
+let avs_of_string s = I.make s I.grp_empty
+
+let string_of_avs r =
+ match I.peek r with
+ | I.Single (s, _) -> Some s
+ | _ -> None
+
+(* boolean constants *******************************************************)
+
+let bool_of_avs r = r <> I.empty
+
+let avs_of_bool = function
+ | true -> I.make "" I.grp_empty
+ | false -> I.empty
+
+let val_false = avs_of_bool false
+
+let val_true = avs_of_bool true
+
+(* iterators ****************************************************************)
+
+let grp_iter f al =
+ List.fold_left (fun s a -> I.grp_union s (f a)) I.grp_empty al
+
+let grp_iter2 f al bl =
+ List.fold_left2 (fun s a b -> I.grp_union s (f a b)) I.grp_empty al bl
+
+let iter f al = List.fold_left (fun s a -> I.union s (f a)) I.empty al
+
+let append_iter f al = List.fold_left (fun s a -> I.append (f a) s) I.empty al
+
+(* other ********************************************************************)
+
+let grp_make_x p vl = grp_iter (I.grp_make p) vl
+
+let x_grp_make_x p rs =
+ let aux g s _ = I.grp_make p s in
+ I.iter aux I.grp_empty rs
+
+let make_x s gl = iter (I.make s) gl
+
+let count v = I.iter (fun n _ _ -> succ n) 0 v
+
+let subj v = iter (fun s -> I.make s I.grp_empty) v
+
+(* numeric operations *******************************************************)
+
+exception NumberError of MathQL.result
+
+let avs_of_int i = I.make (string_of_int i) I.grp_empty
+
+let int_of_avs r =
+ try match (I.peek r) with
+ | I.Empty
+ | I.Many _ -> raise (Failure "int_of_string")
+ | I.Single (s, _) -> MQueryUtil.int_of_string s
+ with Failure "int_of_string" -> raise (NumberError r)
--- /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>
+ *)
+
+exception NumberError of MathQL.result
+
+val val_true : MathQL.result
+
+val val_false : MathQL.result
+
+val grp_make_x : MathQL.path -> MathQL.value -> MathQL.group
+
+val x_grp_make_x : MathQL.path -> MathQL.result -> MathQL.group
+
+val grp_iter : ('a -> MathQL.group) -> 'a list -> MathQL.group
+
+val grp_iter2 : ('a -> 'b -> MathQL.group) ->
+ 'a list -> 'b list -> MathQL.group
+
+val make_x : string -> MathQL.group list -> MathQL.result
+
+val iter : ('a -> MathQL.result) -> 'a list -> MathQL.result
+
+val append_iter : ('a -> MathQL.result) -> 'a list -> MathQL.result
+
+val count : MathQL.result -> int
+
+val avs_of_bool : bool -> MathQL.result
+
+val bool_of_avs : MathQL.result -> bool
+
+val avs_of_int : int -> MathQL.result
+
+val int_of_avs : MathQL.result -> int
+
+val subj : MathQL.value -> MathQL.result
+
+val avs_of_string : string -> MathQL.result
+
+val string_of_avs : MathQL.result -> string option
--- /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://www.cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+type path = Avs.path (* the name of an attribute *)
+
+type value = Avs.value (* the value of an attribute *)
+
+type attribute = path * value (* an attribute *)
+
+type group = attribute list (* a group of attributes *)
+
+type attribute_set = group list (* the attributes of an URI *)
+
+type av = string * attribute_set (* an attributed URI *)
+
+type avs = av list (* the query result *)
+
+type peek_t = Empty
+ | Single of (string * group list)
+ | Many of (string * group list)
+
+
+(* constructors *************************************************************)
+
+let grp_empty = []
+
+let grp_make p v = [(p, [v])]
+
+let empty = grp_empty
+
+let make s = function
+ | [] -> [(s, [])]
+ | g -> [(s, [g])]
+
+(* projections **************************************************************)
+
+let subj v = List.rev (List.rev_map (fun x -> (x, [])) v)
+
+let grp_read g p = subj (List.assoc p g)
+
+let single = function
+ | [s, _] -> Some s
+ | _ -> None
+
+(* iterators ****************************************************************)
+
+let rec iter f a = function
+ | [] -> a
+ | [s, _] -> f a s false
+ | (s, _) :: v -> iter f (f a s true) v
+
+let rec x_iter f a = function
+ | [] -> a
+ | [s, gl] -> f a s gl false
+ | (s, gl) :: v -> x_iter f (f a s gl true) v
+
+let rec x_grp_iter f a g = x_iter f a g
+
+(* tests ********************************************************************)
+
+let rec sub v1 v2 =
+ match (v1, v2) with
+ | [], _ -> true
+ | _, [] -> false
+ | (h1, _) :: _, (h2, _) :: _ when h1 < h2 -> false
+ | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> sub v1 t2
+ | _ :: t1, _ :: t2 -> sub t1 t2
+
+let rec meet v1 v2 =
+ match v1, v2 with
+ | [], _
+ | _, [] -> false
+ | (h1, _) :: t1, (h2, _) :: _ when h1 < h2 -> meet t1 v2
+ | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> meet v1 t2
+ | _, _ -> true
+
+let rec eq v1 v2 =
+ match v1, v2 with
+ | [], [] -> true
+ | (h1, _) :: t1, (h2, _) :: t2 when h1 = h2 -> eq t1 t2
+ | _, _ -> false
+
+(* union ********************************************************************)
+
+let rec set_union v1 v2 =
+ match v1, v2 with
+ | [], v -> v
+ | v, [] -> v
+ | h1 :: t1, h2 :: t2 when h1 < h2 -> h1 :: set_union t1 v2
+ | h1 :: t1, h2 :: t2 when h1 > h2 -> h2 :: set_union v1 t2
+ | h1 :: t1, _ :: t2 -> h1 :: set_union t1 t2
+
+let set_iter f al = List.fold_left (fun s a -> set_union (f a) s) [] al
+
+let grps_make l g = set_union l [g]
+
+let rec union s1 s2 =
+ match s1, s2 with
+ | [], s -> s
+ | s, [] -> s
+ | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 ->
+ (r1, g1) :: union t1 s2
+ | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 ->
+ (r2, g2) :: union s1 t2
+ | (r1, g1) :: t1, (_, g2) :: t2 ->
+ (r1, set_union g1 g2) :: union t1 t2
+
+let grp_union = union
+
+let prod g1 g2 =
+ let aux a = set_iter (fun h -> [union a h]) g2 in
+ set_iter aux g1
+
+let rec d_union s1 s2 =
+ match s1, s2 with
+ | [], s -> s
+ | s, [] -> s
+ | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 ->
+ (r1, g1) :: d_union t1 s2
+ | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 ->
+ (r2, g2) :: d_union s1 t2
+ | (r1, g1) :: t1, (_, g2) :: t2 ->
+ (r1, prod g1 g2) :: d_union t1 t2
+
+(* intersect ****************************************************************)
+
+let rec set_intersect v1 v2 =
+ match v1, v2 with
+ | [], v -> []
+ | v, [] -> []
+ | h1 :: t1, h2 :: _ when h1 < h2 -> set_intersect t1 v2
+ | h1 :: _, h2 :: t2 when h1 > h2 -> set_intersect v1 t2
+ | h1 :: t1, _ :: t2 -> h1 :: set_intersect t1 t2
+
+let rec intersect s1 s2 =
+ match s1, s2 with
+ | [], s -> []
+ | s, [] -> []
+ | (r1, _) :: t1, (r2, _) :: _ when r1 < r2 -> intersect t1 s2
+ | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> intersect s1 t2
+ | (r1, g1) :: t1, (_, g2) :: t2 ->
+ (r1, set_intersect g1 g2) :: intersect t1 t2
+
+(* diff *********************************************************************)
+
+let rec diff s1 s2 =
+ match s1, s2 with
+ | [], _ -> []
+ | s, [] -> s
+ | (r1, g1) :: t1 , (r2, _) ::_ when r1 < r2 ->
+ (r1, g1) :: (diff t1 s2)
+ | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> diff s1 t2
+ | _ :: t1, _ :: t2 -> diff t1 t2
+
+(* concatenation ************************************************************)
+
+let append v1 v2 = v1 @ v2
+
+(* peeking ******************************************************************)
+
+let peek = function
+ | [] -> Empty
+ | [s, gl] -> Single (s, gl)
+ | (s, gl) :: _ -> Many (s, gl)
--- /dev/null
+include Avs.Type
(* output data structures ***************************************************)
-type path = string list (* the name of an attribute *)
+module I : Avs.Type = ListAvs
-type value = string list (* the value of an attribute *)
+type value = Avs.value (* a linearized attribute value *)
-type attribute = path * value (* an attribute *)
+type path = Avs.path (* the name of an attribute *)
-type attribute_group = attribute list (* a group of attributes *)
-
-type attribute_set = attribute_group list (* the attributes of an URI *)
-
-type resource = string * attribute_set (* an attributed URI *)
-
-type resource_set = resource list (* the query result *)
-
-type result = resource_set
+type group = I.group (* an group of attribures *)
+type result = I.avs (* the query result *)
(* input data structures ****************************************************)
type gen = GenFJoin (* full union - with attr handling *)
| GenFMeet (* full intersection - with attr handling *)
-type query = Const of result
+type query = Const of (string * (path * query) list list) list
| SVar of svar
| AVar of avar
| Dot of avar * path
let locate s =
let query =
- M.Property true M.RefineExact ["objectName"] [] [] [] []
- false (const s)
+ M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
+ false, (const s))
in stat query
let unreferred target_pattern source_pattern =
let query =
diff
(
- M.Property false M.RefineExact [] [] [] [] []
- true (const target_pattern)
+ M.Property (false, M.RefineExact, [], [], [], [], [],
+ true, (const target_pattern))
) (
- M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
- true (const source_pattern)
-
+ M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
+ [], [], [], true, (const source_pattern))
)
in stat query
con "h:depth" (List.map U.string_of_depth d)
in
let property_must n c =
- M.Property true M.RefineExact [n] []
- (cons false c) [] [] false (const "")
+ M.Property (true, M.RefineExact, [n], [],
+ (cons false c), [], [], false, (const ""))
in
let property_only n cl =
let cll = List.map (cons true) cl in
- M.Property false M.RefineExact [n] []
- ! univ cll [] false (M.AVar "obj")
+ M.Property (false, M.RefineExact, [n], [],
+ ! univ, cll, [], false, (M.AVar "obj"))
in
let rec aux = function
| [] -> ()
only := true;
let l = List.map U.string_of_position l in
univ := [(false, ["h:position"], set_val l)]; aux tail
- | T.MustObj r p d :: tail ->
+ | T.MustObj (r, p, d) :: tail ->
must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
- | T.MustSort s p d :: tail ->
+ | T.MustSort (s, p, d) :: tail ->
must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
- | T.MustRel p d :: tail ->
+ | T.MustRel (p, d) :: tail ->
must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
- | T.OnlyObj r p d :: tail ->
+ | T.OnlyObj (r, p, d) :: tail ->
onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
- | T.OnlySort s p d :: tail ->
+ | T.OnlySort (s, p, d) :: tail ->
onlysort := ([], s, p, d) :: ! onlysort; aux tail
- | T.OnlyRel p d :: tail ->
+ | T.OnlyRel (p, d) :: tail ->
onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
in
let rec iter f g = function
aux cl;
let must_query =
if ! must = [] then
- M.Property false M.RefineExact [] [] [] [] [] true (const ".*")
+ M.Property (false, M.RefineExact, [], [],
+ [], [], [], true, (const ".*"))
else
intersect ! must
in
mQIMap.cmx: mQIMap.cmi
mQIConn.cmo: mQIMap.cmi mQIPostgres.cmi mQIConn.cmi
mQIConn.cmx: mQIMap.cmx mQIPostgres.cmx mQIConn.cmi
-mQIUtil.cmo: mQIUtil.cmi
-mQIUtil.cmx: mQIUtil.cmi
-mQILib.cmo: mQIConn.cmi mQIUtil.cmi mQILib.cmi
-mQILib.cmx: mQIConn.cmx mQIUtil.cmx mQILib.cmi
-mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIUtil.cmi \
- mQIProperty.cmi
-mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIUtil.cmx \
- mQIProperty.cmi
+mQILib.cmo: mQIConn.cmi mQILib.cmi
+mQILib.cmx: mQIConn.cmx mQILib.cmi
+mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIProperty.cmi
+mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIProperty.cmi
mQueryTParser.cmo: mQILib.cmi mQueryTParser.cmi
mQueryTParser.cmx: mQILib.cmx mQueryTParser.cmi
mQueryTLexer.cmo: mQueryTParser.cmi
mQueryTLexer.cmx: mQueryTParser.cmx
mQueryIO.cmo: mQILib.cmi mQueryTLexer.cmo mQueryTParser.cmi mQueryIO.cmi
mQueryIO.cmx: mQILib.cmx mQueryTLexer.cmx mQueryTParser.cmx mQueryIO.cmi
-mQueryInterpreter.cmo: mQIConn.cmi mQILib.cmi mQIProperty.cmi mQIUtil.cmi \
- mQueryIO.cmi mQueryInterpreter.cmi
-mQueryInterpreter.cmx: mQIConn.cmx mQILib.cmx mQIProperty.cmx mQIUtil.cmx \
- mQueryIO.cmx mQueryInterpreter.cmi
-mQueryStandard.cmo: mQIConn.cmi mQILib.cmi mQIUtil.cmi mQueryStandard.cmi
-mQueryStandard.cmx: mQIConn.cmx mQILib.cmx mQIUtil.cmx mQueryStandard.cmi
+mQueryInterpreter.cmo: mQIConn.cmi mQILib.cmi mQIProperty.cmi mQueryIO.cmi \
+ mQueryInterpreter.cmi
+mQueryInterpreter.cmx: mQIConn.cmx mQILib.cmx mQIProperty.cmx mQueryIO.cmx \
+ mQueryInterpreter.cmi
+mQueryStandard.cmo: mQIConn.cmi mQILib.cmi mQueryStandard.cmi
+mQueryStandard.cmx: mQIConn.cmx mQILib.cmx mQueryStandard.cmi
PREDICATES =
PRE_IFILES = mQIPostgres.mli mQIMap.mli mQIConn.mli \
- mQIUtil.mli mQILib.mli mQIProperty.mli
+ mQILib.mli mQIProperty.mli
POST_IFILES = mQueryIO.mli mQueryInterpreter.mli mQueryStandard.mli
module M = MathQL
module P = MQueryUtil
module C = MQIConn
-module U = MQIUtil
(* external function specification ******************************************)
*)
module M = MathQL
+module I = M.I
+module U = AvsUtil
module P = MQIPostgres
module C = MQIConn
-module U = MQIUtil
module A = MQIMap
let not_supported s =
| [head] -> f head
| head :: tail -> f head ^ sep ^ iter f sep tail
in
+ let avs_iter f sep v =
+ let aux a s = function
+ | true -> a ^ (f s) ^ sep
+ | false -> a ^ (f s)
+ in
+ I.iter aux "" v
+ in
let pg_cols = iter (fun x -> x) ", " cols in
- let pg_msval v = iter (fun s, _ -> P.quote s) ", " v in
+ let pg_msval v = avs_iter P.quote ", " v in
let pg_con (pat, col, v) =
if col <> "" then
- let f (s, _) = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in
- if pat then "(" ^ iter f " or " v ^ ")"
- else match v with
- | [(s,_)] -> col ^ " = " ^ (P.quote s)
- | v -> col ^ " in (" ^ pg_msval v ^ ")"
+ let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in
+ if pat then "(" ^ avs_iter f " or " v ^ ")"
+ else match I.single v with
+ | Some s -> col ^ " = " ^ (P.quote s)
+ | None -> col ^ " in (" ^ pg_msval v ^ ")"
else "true"
in
let pg_cons l = iter pg_con " and " l in
(* Common functions ********************************************************)
let pg_result distinct subj el res =
- let compose = if distinct then List.map else fun f -> U.mql_iter (fun x -> [f x]) in
+ let res, compose =
+ if distinct then List.rev res, U.append_iter else res, U.iter
+ in
let get_name = function (p, None) -> p | (_, Some p) -> p in
let names = List.map get_name el in
- let mk_grp l =
- let grp = U.mql_iter2 (fun p s -> [(p, [s])]) names l in
- if grp = [] then [] else [grp]
- in
- let mk_avs l =
- if subj = "" then ("", mk_grp l) else (List.hd l, mk_grp (List.tl l))
+ let mk_grp l = U.grp_iter2 I.grp_make names l in
+ let mk_avs l =
+ if subj = "" then I.make "" (mk_grp l)
+ else I.make (List.hd l) (mk_grp (List.tl l))
in
compose mk_avs res
if refine <> M.RefineExact then not_supported "exec";
let table = get_table h mc ct cfl el in
let rec exec_aux ct = match ct with
- | (pat, p, v) :: tail when List.length v > deadline ->
- let single s = exec_aux ((pat, p, [s]) :: tail) in
- U.mql_iter single v
+ | (pat, p, v) :: tail when U.count v > deadline ->
+ let single a s _ = I.union a (exec_aux ((pat, p, I.make s I.grp_empty) :: tail)) in
+ I.iter single U.val_false v
| _ ->
exec_single h mc ct cfl el table
in exec_aux ct
| _ -> ""
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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* boolean constants *******************************************************)
-
-let mql_false = []
-
-let mql_true = ["", []]
-
-(* set theoretic operations *************************************************)
-
-let rec set_sub v1 v2 =
- match (v1, v2) with
- | [], _ -> mql_true
- | _, [] -> mql_false
- | (h1, _) :: _, (h2, _) :: _ when h1 < h2 -> mql_false
- | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_sub v1 t2
- | _ :: t1, _ :: t2 -> set_sub t1 t2
-
-let rec set_meet v1 v2 =
- match v1, v2 with
- | [], _
- | _, [] -> mql_false
- | (h1, _) :: t1, (h2, _) :: _ when h1 < h2 -> set_meet t1 v2
- | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_meet v1 t2
- | _, _ -> mql_true
-
-let rec set_eq v1 v2 =
- match v1, v2 with
- | [], [] -> mql_true
- | (h1, _) :: t1, (h2, _) :: t2 when h1 = h2 -> set_eq t1 t2
- | _, _ -> mql_false
-
-let rec set_union v1 v2 =
- match v1, v2 with
- | [], v -> v
- | v, [] -> v
- | h1 :: t1, h2 :: t2 when h1 < h2 -> h1 :: set_union t1 v2
- | h1 :: t1, h2 :: t2 when h1 > h2 -> h2 :: set_union v1 t2
- | h1 :: t1, _ :: t2 -> h1 :: set_union t1 t2
-
-let rec set_intersect v1 v2 =
- match v1, v2 with
- | [], v -> []
- | v, [] -> []
- | h1 :: t1, h2 :: _ when h1 < h2 -> set_intersect t1 v2
- | h1 :: _, h2 :: t2 when h1 > h2 -> set_intersect v1 t2
- | h1 :: t1, _ :: t2 -> h1 :: set_intersect t1 t2
-
-let rec iter f = function
- | [] -> []
- | head :: tail -> set_union (f head) (iter f tail)
-
-(* MathQL specific set operations ******************************************)
-
-let mql_subj v = List.map (fun s -> (s, [])) v
-
-let rec mql_union s1 s2 =
- match s1, s2 with
- | [], s -> s
- | s, [] -> s
- | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 ->
- (r1, g1) :: mql_union t1 s2
- | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 ->
- (r2, g2) :: mql_union s1 t2
- | (r1, g1) :: t1, (_, g2) :: t2 ->
- (r1, set_union g1 g2) :: mql_union t1 t2
-
-let rec mql_iter f = function
- | [] -> []
- | head :: tail -> mql_union (f head) (mql_iter f tail)
-
-let rec mql_iter2 f l1 l2 = match l1, l2 with
- | [], [] -> []
- | h1 :: t1, h2 :: t2 -> mql_union (f h1 h2) (mql_iter2 f t1 t2)
- | _ -> raise (Invalid_argument "mql_iter2")
-
-let rec mql_prod g1 g2 =
- let mql_prod_aux a = iter (fun h -> [mql_union a h]) g2 in
- iter mql_prod_aux g1
-
-let rec mql_intersect s1 s2 =
- match s1, s2 with
- | [], s -> []
- | s, [] -> []
- | (r1, _) :: t1, (r2, _) :: _ when r1 < r2 -> mql_intersect t1 s2
- | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_intersect s1 t2
- | (r1, g1) :: t1, (_, g2) :: t2 ->
- (r1, set_intersect g1 g2) :: mql_intersect t1 t2
-
-let rec mql_diff s1 s2 =
- match s1, s2 with
- | [], _ -> []
- | s, [] -> s
- | (r1, g1) :: t1 , (r2, _) ::_ when r1 < r2 ->
- (r1, g1) :: (mql_diff t1 s2)
- | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_diff s1 t2
- | _ :: t1, _ :: t2 -> mql_diff t1 t2
-
-(* logic operations ********************************************************)
-
-let xor v1 v2 =
- let b = v1 <> mql_false in
- if b && v2 <> mql_false then mql_false else
- if b then v1 else v2
-
-(* numeric operations *******************************************************)
-
-exception NumberError of MathQL.result
-
-let int_of_set r =
- try match r with
- | [s, _] -> MQueryUtil.int_of_string s
- | _ -> raise (Failure "int_of_string")
- with Failure "int_of_string" -> raise (NumberError r)
+++ /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 mql_true : MathQL.result
-
-val mql_false : MathQL.result
-
-val set_sub : MathQL.result -> MathQL.result -> MathQL.result
-
-val set_meet : MathQL.result -> MathQL.result -> MathQL.result
-
-val set_eq : MathQL.result -> MathQL.result -> MathQL.result
-
-val set_union : 'a list -> 'a list -> 'a list
-
-val mql_subj : MathQL.value -> MathQL.result
-
-val mql_union : ('a * 'b list) list -> ('a * 'b list) list ->
- ('a * 'b list) list
-
-val mql_prod : MathQL.attribute_set -> MathQL.attribute_set ->
- MathQL.attribute_set
-
-val mql_intersect : MathQL.result -> MathQL.result -> MathQL.result
-
-val mql_diff : MathQL.result -> MathQL.result -> MathQL.result
-
-val iter : ('a -> 'b list) -> 'a list -> 'b list
-
-val mql_iter : ('c -> ('a * 'b list) list) -> 'c list ->
- ('a * 'b list) list
-
-val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list ->
- 'd list -> ('a * 'b list) list
-
-val xor : MathQL.result -> MathQL.result -> MathQL.result
-
-exception NumberError of MathQL.result
-
-val int_of_set : MathQL.result -> int
*)
module M = MathQL
+module I = M.I
module P = MQueryUtil
module L = MQILib
let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p
-let text_of_result out sep x =
- let txt_attr = function
- | (p, []) -> txt_path out p
- | (p, l) -> txt_path out p; out " = ";
- P.flat_list out (txt_str out) ", " l
+let text_of_result out sep x =
+ let txt_attr _ p l b =
+ txt_path out p;
+ if l <> [] then begin
+ out " = "; P.flat_list out (txt_str out) ", " l
+ end;
+ if b then out ("; " ^ sep)
in
+ let txt_group l = out "{"; I.x_grp_iter txt_attr () l; out "}" in
+ let txt_res _ s l b =
+ txt_str out s;
+ if l <> [] then begin
+ out " = "; P.flat_list out txt_group ", " l
+ end;
+ if b then out "; "
+ in
+ I.x_iter txt_res () x; out sep
+
+let rec xtext_of_groups out l =
+ let txt_attr (p, x) = txt_path out p; out " = "; text_of_query out "" x in
let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in
+ P.flat_list out txt_group ", " l
+
+and xtext_of_result out x =
let txt_res = function
| (s, []) -> txt_str out s
- | (s, l) -> txt_str out s; out " attr ";
- P.flat_list out txt_group ", " l
+ | (s, l) -> txt_str out s; out " attr "; xtext_of_groups out l
in
- let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in
- txt_set x
+ P.flat_list out txt_res "; " x
-let rec text_of_query out sep x =
+and text_of_query out sep x =
let txt_svar sv = out ("$" ^ sv) in
let txt_avar av = out ("@" ^ av) in
let txt_inv i = if i then out "inverse " in
| l -> out s; P.flat_list out txt_con ", " l
and txt_istrue lt = txt_con_list " istrue " lt
and txt_isfalse lf = txt_con_list " isfalse " lf
- and txt_ass (p, x) = txt_set x; out " as "; txt_path out p
- and txt_ass_list l = P.flat_list out txt_ass ", " l
- and txt_assg_list g = P.flat_list out txt_ass_list "; " g
and txt_grp = function
- | M.Attr g -> txt_assg_list g
+ | M.Attr g -> xtext_of_groups out g
| M.From av -> txt_avar av
and txt_set = function
- | M.Fun p pl xl ->
+ | M.Fun (p, pl, xl) ->
let o = {L.out = out; L.path = txt_path;
L.query = text_of_query; L.result = text_of_result
}
in
L.fun_txt_out o p pl xl
- | M.Const [s, []] -> txt_str out s
- | M.Const r -> text_of_result out " " r
- | M.Dot av p -> txt_avar av; out "."; txt_path out p
- | M.Ex b x -> out "ex "; txt_set x
-(* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b;
- out "] "; txt_set x
-*) | M.SVar sv -> txt_svar sv
- | M.AVar av -> txt_avar av
- | M.Property q0 q1 q2 mc ct cfl xl b x ->
+ | M.Const [s, []] -> txt_str out s
+ | M.Const r -> xtext_of_result out r
+ | M.Dot (av, p) -> txt_avar av; out "."; txt_path out p
+ | M.Ex (b, x) -> out "ex "; txt_set x
+(* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b;
+ out "] "; txt_set x
+*) | M.SVar sv -> txt_svar sv
+ | M.AVar av -> txt_avar av
+ | M.Property (q0, q1, q2, mc, ct, cfl, xl, b, x) ->
out "property "; txt_qualif q0 q1 q2; main mc;
txt_istrue ct; P.flat_list out txt_isfalse "" cfl; txt_exp_list xl;
out " of "; pattern b; txt_set x
- | M.Let (Some sv) x y -> out "let "; txt_svar sv; out " = ";
- txt_set x; out " in "; txt_set y
- | M.Let None x y -> txt_set x; out " ;; "; txt_set y
- | M.Select av x y -> out "select "; txt_avar av; out " from ";
- txt_set x; out " where "; txt_set y
- | M.For k av x y -> out "for "; txt_avar av; out " in ";
- txt_set x; txt_gen k; txt_set y
- | M.While k x y -> out "while "; txt_set x; txt_gen k; txt_set y
- | M.Add d g x -> out "add "; txt_distr d; txt_grp g;
- out " in "; txt_set x
- | M.Gen p [x] -> out "gen "; txt_path out p; out " in "; txt_set x
- | M.Gen p l -> out "gen "; txt_path out p; out " {";
- P.flat_list out txt_set ", " l; out "}"
+ | M.Let (Some sv, x, y) -> out "let "; txt_svar sv; out " = ";
+ txt_set x; out " in "; txt_set y
+ | M.Let (None, x, y) -> txt_set x; out " ;; "; txt_set y
+ | M.Select (av, x, y) -> out "select "; txt_avar av; out " from ";
+ txt_set x; out " where "; txt_set y
+ | M.For (k, av, x, y) -> out "for "; txt_avar av; out " in ";
+ txt_set x; txt_gen k; txt_set y
+ | M.While (k, x, y) -> out "while "; txt_set x; txt_gen k; txt_set y
+ | M.Add (d, g, x) -> out "add "; txt_distr d; txt_grp g;
+ out " in "; txt_set x
+ | M.Gen (p, [x]) -> out "gen "; txt_path out p; out " in "; txt_set x
+ | M.Gen (p, l) -> out "gen "; txt_path out p; out " {";
+ P.flat_list out txt_set ", " l; out "}"
in
txt_set x; out sep
exception Found
+module U = AvsUtil
module M = MathQL
+module I = M.I
module P = MQueryUtil
module C = MQIConn
-module U = MQIUtil
module L = MQILib
module F = MQueryIO
(* contexts *****************************************************************)
-type svar_context = (M.svar * M.resource_set) list
+type svar_context = (M.svar * M.result) list
-type avar_context = (M.avar * M.resource) list
+type avar_context = (M.avar * (string * M.group list)) list
-type group_context = (M.avar * M.attribute_group) list
+type group_context = (M.avar * M.group) list
type context = {svars: svar_context;
avars: avar_context;
F.text_of_query (C.log h) "\n" q
end
in
- let proj v = List.map fst v in
let rec eval_query c = function
- | M.Const r -> c, r
- | M.Dot i p ->
+ | M.Const r ->
+ let aux2 s g = I.make s (eval_list c g) in
+ let aux (s, gl) = U.iter (aux2 s) gl in
+ c, U.iter aux r
+ | M.Dot (i, p) ->
begin
- try c, U.mql_subj (List.assoc p (List.assoc i c.groups))
- with Not_found -> warn (M.Dot i p); c, []
+ try c, I.grp_read (List.assoc i c.groups) p
+ with Not_found -> warn (M.Dot (i, p)); c, I.empty
end
- | M.Ex l y ->
+ | M.Ex (l, y) ->
let rec ex_aux h = function
| [] ->
let d = {c with groups = h} in
- if snd (eval_query d y) = U.mql_false then () else raise Found
+ if snd (eval_query d y) = U.val_false then () else raise Found
| i :: tail ->
begin
try
with Not_found -> ()
end
in
- begin try ex_aux [] l; c, U.mql_false with Found -> c, U.mql_true end
+ begin try ex_aux [] l; c, U.val_false with Found -> c, U.val_true end
| M.SVar i ->
begin
try c, List.assoc i c.svars
- with Not_found -> warn (M.SVar i); c, []
+ with Not_found -> warn (M.SVar i); c, I.empty
end
| M.AVar i ->
begin
- try c, [List.assoc i c.avars]
- with Not_found -> warn (M.AVar i); c, []
+ try
+ let s, gl = List.assoc i c.avars in
+ c, U.make_x s gl
+ with Not_found -> warn (M.AVar i); c, I.empty
end
- | M.Let (Some i) x1 x2 ->
+ | M.Let (Some i, x1, x2) ->
let d, r = eval_query c x1 in
let d = {d with svars = P.add_assoc (i, r) d.svars} in
eval_query d x2
- | M.Let None x1 x2 ->
+ | M.Let (None, x1, x2) ->
let d, r = eval_query c x1 in eval_query d x2
- | M.For k i x1 x2 ->
+ | M.For (k, i, x1, x2) ->
let f = match k with
- | M.GenFJoin -> U.mql_union
- | M.GenFMeet -> U.mql_intersect
+ | M.GenFJoin -> I.union
+ | M.GenFMeet -> I.intersect
in
- let rec for_aux (d, r) = match r with
- | [] -> d, []
- | h :: t ->
- let d = {d with avars = P.add_assoc (i, h) d.avars} in
- let d, r = eval_query d x2 in
- let d, s = for_aux (d, t) in
- d, f r s
- in
- for_aux (eval_query c x1)
- | M.While k x1 x2 ->
+ let for_aux (d, r) s gl _ =
+ let d = {d with avars = P.add_assoc (i, (s, gl)) d.avars} in
+ let d, s = eval_query d x2 in
+ d, f r s
+ in
+ let d, r = eval_query c x1 in
+ I.x_iter for_aux (d, I.empty) r
+ | M.While (k, x1, x2) ->
let f = match k with
- | M.GenFJoin -> U.mql_union
- | M.GenFMeet -> U.mql_intersect
+ | M.GenFJoin -> I.union
+ | M.GenFMeet -> I.intersect
in
let rec while_aux (d, r) =
let d, b = eval_query d x1 in
- if b = U.mql_false then d, r else
+ if b = U.val_false then d, r else
let d, s = eval_query d x2 in
while_aux (d, f r s)
in
- while_aux (c, U.mql_false)
- | M.Add b z x ->
- let f = if b then U.mql_prod else U.set_union in
- let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in
+ while_aux (c, U.val_false)
+ | M.Add (b, z, x) ->
+ let f = if b then I.d_union else I.union in
+ let agl = eval_grp c z in
+ let aux r sj gl _ =
+ I.append (f (U.make_x sj gl) (U.make_x sj agl)) r
+ in
let _, r = eval_query c x in
- c, List.fold_right g r []
- | M.Property q0 q1 q2 mc ct cfl el pat y ->
+ c, I.x_iter aux I.empty r
+ | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) ->
let _, r = eval_query c y in
let subj, mct =
if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r)
let r = MQIProperty.exec h q1 subj cons_true cons_false exp in
let s = P.stop_time t in
if C.set h C.Stat then
- C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
+ C.log h (Printf.sprintf "Property: %s,%i\n" s (U.count r));
c, r
- | M.Select i x y ->
- let rec select_aux (d, r) = match r with
- | [] -> d, []
- | h :: t ->
- let d = {d with avars = P.add_assoc (i, h) d.avars} in
- let d, r = eval_query d y in
- let d, s = select_aux (d, t) in
- if r = U.mql_false then d, s else d, (h :: s)
+ | M.Select (i, x, y) ->
+ let aux (d, r) sj gl _ =
+ let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in
+ let d, s = eval_query d y in
+ if s = U.val_false then d, r else d, (I.append (U.make_x sj gl) r)
in
- select_aux (eval_query c x)
- | M.Fun p pl xl ->
+ let d, r = eval_query c x in
+ I.x_iter aux (d, I.empty) r
+ | M.Fun (p, pl, xl) ->
let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec
p pl xl
- | M.Gen p xl ->
+ | M.Gen (p, xl) ->
let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
eval_query c (L.gen_eval e p xl)
+ and eval_list c l =
+ let aux (p, y) =
+ let _, r = eval_query c y in
+ U.x_grp_make_x p r
+ in
+ U.grp_iter aux l
and eval_grp c = function
| M.Attr gs ->
- let attr_aux g (p, y) =
- let _, r = eval_query c y in
- U.mql_union g [p, proj r]
- in
- let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
+ let attr_auxs s l = I.grps_make s (eval_list c l) in
List.fold_left attr_auxs [] gs
| M.From i ->
try snd (List.assoc i c.avars)
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+module U = AvsUtil
+module M = MathQL
+module I = M.I
module P = MQueryUtil
module C = MQIConn
-module U = MQIUtil
module L = MQILib
let init = ()
+let test f v1 v2 = U.avs_of_bool (f v1 v2)
+
+let num_test f v1 v2 = U.avs_of_bool (f (U.int_of_avs v1) (U.int_of_avs v2))
+
(* FALSE / EMPTY ************************************************************)
let false_fun b =
let s = if b then "false" else "empty" in
- L.fun_arity0 [] s U.mql_false
+ L.fun_arity0 [] s U.val_false
let _ = L.fun_register ["empty"] (false_fun false)
(* TRUE *********************************************************************)
-let true_fun = L.fun_arity0 [] "true" U.mql_true
+let true_fun = L.fun_arity0 [] "true" U.val_true
let _ = L.fun_register ["true"] true_fun
(* NOT **********************************************************************)
let not_fun =
- let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
+ let aux r = if r = U.val_false then U.val_true else U.val_false in
L.fun_arity1 [] "!" aux
let _ = L.fun_register ["not"] not_fun
(* COUNT ********************************************************************)
let count_fun =
- let aux r = [string_of_int (List.length r), []] in
+ let aux r = U.avs_of_int (U.count r) in
L.fun_arity1 [] "#" aux
let _ = L.fun_register ["count"] count_fun
(* PEEK *********************************************************************)
let peek_fun =
- let aux = function [] -> [] | hd :: _ -> [hd] in
+ let aux r =
+ match (I.peek r) with
+ | I.Empty
+ | I.Single _ -> r
+ | I.Many (s, gl) -> U.make_x s gl
+ in
L.fun_arity1 [] "peek" aux
let _ = L.fun_register ["peek"] peek_fun
(* DIFF *********************************************************************)
-let diff_fun = L.fun_arity2 [] "diff" U.mql_diff
+let diff_fun = L.fun_arity2 [] "diff" I.diff
let _ = L.fun_register ["diff"] diff_fun
(* XOR **********************************************************************)
-let xor_fun = L.fun_arity2 [] "xor" U.xor
+let xor_fun =
+ let aux v1 v2 =
+ let b = v1 <> U.val_false in
+ if b && v2 <> U.val_false then U.val_false else
+ if b then v1 else v2
+ in
+ L.fun_arity2 [] "xor" aux
let _ = L.fun_register ["xor"] xor_fun
(* SUB **********************************************************************)
-let sub_fun = L.fun_arity2 [] "sub" U.set_sub
+let sub_fun = L.fun_arity2 [] "sub" (test I.sub)
let _ = L.fun_register ["sub"] sub_fun
(* MEET *********************************************************************)
-let meet_fun = L.fun_arity2 [] "meet" U.set_meet
+let meet_fun = L.fun_arity2 [] "meet" (test I.meet)
let _ = L.fun_register ["meet"] meet_fun
(* EQ ***********************************************************************)
-let eq_fun = L.fun_arity2 [] "==" U.set_eq
+let eq_fun = L.fun_arity2 [] "==" (test I.eq)
let _ = L.fun_register ["eq"] eq_fun
(* LE ***********************************************************************)
-let le_fun =
- let le v1 v2 =
- if U.int_of_set v1 <= U.int_of_set v2 then U.mql_true else U.mql_false
- in
- L.fun_arity2 [] "<=" le
+let le_fun = L.fun_arity2 [] "<=" (num_test (<=))
let _ = L.fun_register ["le"] le_fun
(* LT ***********************************************************************)
-let lt_fun =
- let lt v1 v2 =
- if U.int_of_set v1 < U.int_of_set v2 then U.mql_true else U.mql_false
- in
- L.fun_arity2 [] "<" lt
+let lt_fun = L.fun_arity2 [] "<" (num_test (<))
let _ = L.fun_register ["lt"] lt_fun
let t = P.start_time () in
let r = (e.L.eval x) in
let s = P.stop_time t in
- o.L.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+ o.L.out (Printf.sprintf "Stat: %s,%i\n" s (U.count r));
r
| _ -> assert false
in
let rs = ref "" in
let out s = rs := ! rs ^ s in
o.L.result out " " (e.L.eval x);
- [! rs, []]
+ I.make ! rs I.grp_empty
| _ -> assert false
in
let txt_out o _ = function
let arity_s = L.Const 1 in
let body e o i _ = function
| [x] ->
- let aux av =
- let ich = open_in (fst av) in
+ let aux avs s _ =
+ let ich = open_in s in
let r = i.L.result_in (Lexing.from_channel ich) in
- close_in ich; r
+ close_in ich; I.union avs r
in
- U.mql_iter aux (e.L.eval x)
+ I.iter aux I.empty (e.L.eval x)
| _ -> assert false
in
let txt_out o _ = function
(* ALIGN ********************************************************************)
let align_fun =
- let aux l (v, g) =
+ let aux2 l v =
let c = String.length v in
- if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g]
- in
+ if c < l then String.make (l - c) ' ' ^ v else v
+ in
+ let aux l r s gl _ = I.append r (U.make_x (aux2 l s) gl) in
let arity_p = L.Const 0 in
let arity_s = L.Const 2 in
let body e _ _ _ = function
| [y; x] ->
- let l = U.int_of_set (e.L.eval y) in
- U.mql_iter (aux l) (e.L.eval x)
+ let l = U.int_of_avs (e.L.eval y) in
+ I.x_iter (aux l) I.empty (e.L.eval x)
| _ -> assert false
in
let txt_out o _ = function
let arity_s = L.Const 3 in
let body e _ _ _ = function
| [y; x1; x2] ->
- if (e.L.eval y) = U.mql_false then (e.L.eval x2) else (e.L.eval x1)
+ if U.bool_of_avs (e.L.eval y) then (e.L.eval x1) else (e.L.eval x2)
| _ -> assert false
in
let txt_out o _ = function
let rec iter f = function
| [] -> assert false
| [head] -> f head
- | head :: tail -> U.mql_intersect (f head) (iter f tail)
+ | head :: tail -> I.intersect (f head) (iter f tail)
in
let arity_p = L.Const 0 in
let arity_s = L.Positive in
let union_fun =
let arity_p = L.Const 0 in
let arity_s = L.Any in
- let body e _ _ _ xl = U.mql_iter e.L.eval xl in
+ let body e _ _ _ xl = U.iter e.L.eval xl in
let txt_out o _ xl = let o = L.std o in L.out_txt_ o [] xl
in
{L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
let or_fun =
let rec iter f = function
- | [] -> U.mql_false
+ | [] -> U.val_false
| head :: tail ->
let r1 = f head in
- if r1 = U.mql_false then (iter f tail) else r1
+ if U.bool_of_avs r1 then r1 else (iter f tail)
in
let arity_p = L.Const 0 in
let arity_s = L.Any in
let and_fun =
let rec iter f = function
- | [] -> U.mql_true
+ | [] -> U.val_true
| [head] -> f head
| head :: tail ->
- if f head = U.mql_false then U.mql_false else iter f tail
+ if U.bool_of_avs (f head) then iter f tail else U.val_false
in
let arity_p = L.Const 0 in
let arity_s = L.Any in
(* PROJ *********************************************************************)
let proj_fun =
- let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in
- let proj_group p a = U.mql_iter (proj_group_aux p) a in
- let proj_set p (_, g) = U.mql_iter (proj_group p) (List.rev g) in
+ let aux2 p a q v _ = if p = q then I.union a (U.subj v) else a in
+ let aux p a _ gl _ =
+ I.union a (U.iter (I.x_grp_iter (aux2 p) I.empty) gl)
+ in
let arity_p = L.Const 1 in
let arity_s = L.Const 1 in
let body e _ _ pl xl =
match pl, xl with
- | [p], [x] -> U.mql_iter (proj_set p) (e.L.eval x)
+ | [p], [x] -> I.x_iter (aux p) I.empty (e.L.eval x)
| _ -> assert false
in
let txt_out o pl xl =
(* KEEP *********************************************************************)
-let keep_fun b =
- let proj (r, _) = (r, []) in
- let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in
- let keep_grp l a = List.fold_right (keep_path l) a [] in
- let keep_set l a g =
- let kg = keep_grp l a in
- if kg = [] then g else kg :: g
+let keep_fun b =
+ let aux2 s l a q v _ =
+ if List.mem q l = b then a else I.union a (I.make s (U.grp_make_x q v))
in
- let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in
+ let aux l a s gl _ =
+ I.append a (
+ if l = [] then I.make s I.grp_empty else
+ U.iter (I.x_grp_iter (aux2 s l) I.empty) gl)
+ in
let txt_allbut o = if b then o.L.s_out "allbut " in
let txt_path_list o l = P.flat_list o.L.s_out o.L.s_path ", " l in
let arity_p = L.Any in
let body e _ _ pl xl =
match b, pl, xl with
| true, [], [x] -> e.L.eval x
- | false, [], [x] -> List.map proj (e.L.eval x)
- | _, l, [x] -> List.map (keep_av l) (e.L.eval x)
+ | _, l, [x] -> I.x_iter (aux l) I.empty (e.L.eval x)
| _ -> assert false
in
let txt_out o pl xl =
%{
module M = MathQL
+ module I = M.I
+ module U = AvsUtil
module L = MQILib
let make_fun p pl xl =
L.fun_arity p (List.length pl) (List.length xl);
- M.Fun p pl xl
+ M.Fun (p, pl, xl)
let make_gen p xl =
L.gen_arity p (List.length xl);
- M.Gen p xl
+ M.Gen (p, xl)
let analyze x =
let rec join l1 l2 = match l1, l2 with
| head :: tail -> join (f head) (iter f tail)
in
let rec an_set = function
- | M.Const _
+ | M.Const x -> iter fv x
| M.SVar _
| M.AVar _
- | M.Ex _ -> []
- | M.Dot rv _ -> [rv]
- | M.Let _ x y
- | M.Select _ x y
- | M.For _ _ x y -> iter an_set [x; y]
- | M.While _ x y -> iter an_set [x; y]
- | M.Fun _ _ l -> iter an_set l
- | M.Gen _ l -> iter an_set l
- | M.Add _ g x -> join (an_grp g) (an_set x)
- | M.Property _ _ _ _ c d _ _ x ->
+ | M.Ex _ -> []
+ | M.Dot (rv, _) -> [rv]
+ | M.Let (_, x, y)
+ | M.Select (_, x, y)
+ | M.For (_, _, x, y) -> iter an_set [x; y]
+ | M.While (_, x, y) -> iter an_set [x; y]
+ | M.Fun (_, _, l) -> iter an_set l
+ | M.Gen (_, l) -> iter an_set l
+ | M.Add (_, g, x) -> join (an_grp g) (an_set x)
+ | M.Property (_, _, _, _, c, d, _, _, x) ->
join (an_set x) (iter an_con [c; List.concat d])
and fc (_, _, v) = an_set v
and an_con c = iter fc c
and fg (_, v) = an_set v
and an_grp = function
| M.Attr g -> iter (iter fg) g
- | M.From _ -> []
+ | M.From _ -> []
+ and fv (_, g) = iter (iter fg) g
in
an_set x
| PAT { true }
| { false }
;
- ass:
- | set_exp AS path { ($3, $1) }
- ;
- asss:
- | ass CM asss { $1 :: $3 }
- | ass { [$1] }
- ;
- assg:
- | asss SC assg { $1 :: $3 }
- | asss { [$1] }
- ;
distr:
| DISTR { true }
| { false }
| { "text" }
;
grp_exp:
- | assg { M.Attr $1 }
- | avar { M.From $1 }
+ | x_groups { M.Attr $1 }
+ | avar { M.From $1 }
;
set_exp:
| STAT set_exp { make_fun ["stat"] [] [$2] }
| IF set_exp THEN set_exp ELSE set_exp
{ make_fun ["if"] [] [$2; $4; $6] }
| STR { M.Const [$1, []] }
- | LB resources RB { M.Const $2 }
- | avar FS path { M.Dot $1 $3 }
+ | LB x_resources RB { M.Const $2 }
+ | avar FS path { M.Dot ($1, $3) }
| LP set_exp RP { $2 }
- | EX set_exp { M.Ex (analyze $2) $2 }
+ | EX set_exp { M.Ex (analyze $2, $2) }
| svar { M.SVar $1 }
| avar { M.AVar $1 }
- | LET svar BE set_exp IN set_exp { M.Let (Some $2) $4 $6 }
- | set_exp SEQ set_exp { M.Let None $1 $3 }
- | FOR avar IN set_exp gen_op { M.For (fst $5) $2 $4 (snd $5) }
- | WHILE set_exp gen_op { M.While (fst $3) $2 (snd $3) }
- | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 }
+ | LET svar BE set_exp IN set_exp { M.Let (Some $2, $4, $6) }
+ | set_exp SEQ set_exp { M.Let (None, $1, $3) }
+ | FOR avar IN set_exp gen_op { M.For (fst $5, $2, $4, snd $5) }
+ | WHILE set_exp gen_op { M.While (fst $3, $2, snd $3) }
+ | ADD distr grp_exp IN set_exp { M.Add ($2, $3, $5) }
| PROP qualif mainc istrue isfalse attrc OF pattern set_exp
- { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 }
- | SELECT avar FROM set_exp WHERE set_exp { M.Select $2 $4 $6 }
+ { M.Property (f $2, s $2, t $2, $3, $4, $5, $6, $8, $9) }
+ | SELECT avar FROM set_exp WHERE set_exp { M.Select ($2, $4, $6) }
| GEN path LC sets RC { make_gen $2 $4 }
| GEN path IN set_exp { make_gen $2 [$4] }
;
| set_exp error { $1 }
| EOF { raise End_of_file }
;
+
+ x_attr:
+ | path BE set_exp { ($1, $3) }
+ | path { ($1, make_fun ["empty"] [] []) }
+ ;
+ x_attrs:
+ | x_attr SC x_attrs { $1 :: $3 }
+ | x_attr { [$1] }
+ ;
+ x_group:
+ LC x_attrs RC { $2 }
+ ;
+ x_groups:
+ | x_group CM x_groups { $1 :: $3 }
+ | x_group { [$1] }
+ ;
+ x_resource:
+ | STR ATTR x_groups { ($1, $3) }
+ | STR { ($1, []) }
+ ;
+ x_resources:
+ | x_resource SC x_resources { $1 :: $3 }
+ | x_resource { [$1] }
+ | { [] }
+ ;
+
attr:
- | path BE strs { $1, $3 }
- | path { $1, [] }
+ | path BE strs { U.grp_make_x $1 $3 }
+ | path { U.grp_make_x $1 [] }
;
attrs:
- | attr SC attrs { $1 :: $3 }
- | attr { [$1] }
+ | attr SC attrs { I.grp_union $1 $3 }
+ | attr { $1 }
;
group:
LC attrs RC { $2 }
| group { [$1] }
;
resource:
- | STR ATTR groups { ($1, $3) }
- | STR { ($1, []) }
+ | STR ATTR groups { U.make_x $1 $3 }
+ | STR { U.make_x $1 [] }
;
resources:
- | resource SC resources { $1 :: $3 }
- | resource { [$1] }
- | { [] }
+ | resource SC resources { I.union $1 $3 }
+ | resource { $1 }
+ | { U.val_false }
;
result:
| resources { $1 }
projects / helm.git / commitdiff