From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 10:13:14 +0000 (+0000) Subject: moved mathql side by side with ocaml/ X-Git-Tag: make_still_working~7692 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ab72cb44a09c93e1d540f7ac9bc7eae2f4d09f2f;p=helm.git moved mathql side by side with ocaml/ --- diff --git a/helm/mathql/mathql/.depend b/helm/mathql/mathql/.depend new file mode 100644 index 000000000..e69de29bb diff --git a/helm/mathql/mathql/Makefile b/helm/mathql/mathql/Makefile new file mode 100644 index 000000000..17cafb431 --- /dev/null +++ b/helm/mathql/mathql/Makefile @@ -0,0 +1,13 @@ +PACKAGE = mathql + +PREDICATES = + +INTERFACE_FILES = + +IMPLEMENTATION_FILES = mathQL.ml + +EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi + +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/mathql/mathql/mathQL.ml b/helm/mathql/mathql/mathQL.ml new file mode 100644 index 000000000..2504cfb4f --- /dev/null +++ b/helm/mathql/mathql/mathQL.ml @@ -0,0 +1,133 @@ +(* 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 + *) + +(* $Id$ *) + +(* output data structures ***************************************************) + +type path = string list (* the name of an attribute *) + +type value = string list (* the value of an attribute *) + +type attribute = path * value (* 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 + + +(* input data structures ****************************************************) + +type svar = string (* the name of a variable for a resource set *) + +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 + | RefineSub + | RefineSuper + +type main = path + +type pattern = bool + +type exp = path * (path option) + +type exp_list = exp list + +type allbut = bool + +type xml = bool + +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 + | AVar of avar + | Subj of msval + | 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 + | From of avar + +and con = pattern * path * msval + +and istrue = con list + +and isfalse = con list diff --git a/helm/mathql/mathql_db_map.txt b/helm/mathql/mathql_db_map.txt new file mode 100644 index 000000000..c58d843d2 --- /dev/null +++ b/helm/mathql/mathql_db_map.txt @@ -0,0 +1,26 @@ +objectName source <+ +objectName value <- objectName +refObj <- refObj +refObj source <- +refObj h_occurrence <- refObj h:occurrence +refObj h_position <- refObj h:position +refObj h_depth <- refObj h:depth +refRel <- refRel +refRel source <- +refRel h_position <- refRel h:position +refRel h_depth <- refRel h:depth +refSort <- refSort +refSort source <- +refSort h_sort <- refSort h:sort +refSort h_position <- refSort h:position +refSort h_depth <- refSort h:depth +backPointer <- backPointer +backPointer source <- backPointer h:occurrence +backPointer h_occurrence <- +backPointer h_position <- backPointer h:position +backPointer h_depth <- backPointer h:depth +no_inconcl_aux source <- +no_inconcl_aux no <- no_inconcl + +backPointer -> refObj + -> diff --git a/helm/mathql/mathql_generator/.depend b/helm/mathql/mathql_generator/.depend new file mode 100644 index 000000000..0dc5572a0 --- /dev/null +++ b/helm/mathql/mathql_generator/.depend @@ -0,0 +1,15 @@ +mQGUtil.cmi: mQGTypes.cmo +mQueryGenerator.cmi: mQGTypes.cmo +cGMatchConclusion.cmi: mQGTypes.cmo +cGSearchPattern.cmi: mQGTypes.cmo +cGLocateInductive.cmi: mQGTypes.cmo +mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi +mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi +mQueryGenerator.cmo: mQGUtil.cmi mQGTypes.cmo mQueryGenerator.cmi +mQueryGenerator.cmx: mQGUtil.cmx mQGTypes.cmx mQueryGenerator.cmi +cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi +cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi +cGSearchPattern.cmo: mQGUtil.cmi mQGTypes.cmo cGSearchPattern.cmi +cGSearchPattern.cmx: mQGUtil.cmx mQGTypes.cmx cGSearchPattern.cmi +cGLocateInductive.cmo: mQGTypes.cmo cGLocateInductive.cmi +cGLocateInductive.cmx: mQGTypes.cmx cGLocateInductive.cmi diff --git a/helm/mathql/mathql_generator/Makefile b/helm/mathql/mathql_generator/Makefile new file mode 100644 index 000000000..cf8e820d9 --- /dev/null +++ b/helm/mathql/mathql_generator/Makefile @@ -0,0 +1,15 @@ +PACKAGE = mathql_generator + +PREDICATES = + +INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ + cGMatchConclusion.mli cGSearchPattern.mli \ + cGLocateInductive.mli + +IMPLEMENTATION_FILES = mQGTypes.ml $(INTERFACE_FILES:%.mli=%.ml) + +EXTRA_OBJECTS_TO_INSTALL = mQGTypes.ml mQGTypes.cmi + +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/mathql/mathql_generator/cGLocateInductive.ml b/helm/mathql/mathql_generator/cGLocateInductive.ml new file mode 100644 index 000000000..261b29388 --- /dev/null +++ b/helm/mathql/mathql_generator/cGLocateInductive.ml @@ -0,0 +1,42 @@ +(* 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 + *) + +(* $Id$ *) + +exception NotAnInductiveDefinition + +let get_constraints = function + | Cic.MutInd (uri, t, _) -> + let uri = UriManager.string_of_uriref (uri, [t]) in + let constr_obj = + [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] + in + let constr_rel = [`MainConclusion None] in + let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in + (constr_obj, constr_rel, constr_sort) + | _ -> raise NotAnInductiveDefinition diff --git a/helm/mathql/mathql_generator/cGLocateInductive.mli b/helm/mathql/mathql_generator/cGLocateInductive.mli new file mode 100644 index 000000000..b6a51401e --- /dev/null +++ b/helm/mathql/mathql_generator/cGLocateInductive.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val get_constraints : Cic.term -> MQGTypes.must_restrictions + +exception NotAnInductiveDefinition diff --git a/helm/mathql/mathql_generator/cGMatchConclusion.ml b/helm/mathql/mathql_generator/cGMatchConclusion.ml new file mode 100644 index 000000000..0a67c2d0d --- /dev/null +++ b/helm/mathql/mathql_generator/cGMatchConclusion.ml @@ -0,0 +1,161 @@ +(* 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 + *) + +(* $Id$ *) + +module T = MQGTypes + +let text_of_entries out entries = + out "(** MatchConclusion: results of the term inspection **)\n"; + let text_of_entry (u, b, v) = + out (string_of_int v ^ " "); + out (if b then "$MC " else "$IC "); + out (u ^ "\n") + in List.iter text_of_entry entries + +let sort_entries entries = + let comparator (_, _, v1) (_, _, v2) = compare v1 v2 in + List.fast_sort comparator entries + +let levels_of_term metasenv context term = + let module TC = CicTypeChecker in + let module Red = CicReduction in + let degree t = + let rec degree_aux = function + | Cic.Sort _ -> 1 + | Cic.Cast (u, _) -> degree_aux u + | Cic.Prod (_, _, t) -> degree_aux t + | _ -> 2 + in + let u,_ = TC.type_of_aux' metasenv context t CicUniv.empty_ugraph in + degree_aux (Red.whd context u) + in + let entry_eq (s1, b1, v1) (s2, b2, v2) = + s1 = s2 && b1 = b2 + in + let rec entry_in e = function + | [] -> [e] + | head :: tail -> + head :: if entry_eq head e then tail else entry_in e tail + in + let inspect_uri main l uri tc v term = + let d = degree term in + entry_in (UriManager.string_of_uriref (uri, tc), main, 2 * v + d - 1) l + in + let rec inspect_term main l v term = match term with + Cic.Rel _ -> l + | Cic.Meta _ -> l + | Cic.Sort _ -> l + | Cic.Implicit _ -> l + | Cic.Var (u,exp_named_subst) -> + inspect_exp_named_subst l (succ v) exp_named_subst +(* + let l' = inspect_uri main l u [] v term in + inspect_exp_named_subst l' (succ v) exp_named_subst +*) + | Cic.Const (u,exp_named_subst) -> + let l' = inspect_uri main l u [] v term in + inspect_exp_named_subst l' (succ v) exp_named_subst + | Cic.MutInd (u, t, exp_named_subst) -> + let l' = inspect_uri main l u [t] v term in + inspect_exp_named_subst l' (succ v) exp_named_subst + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + let l' = inspect_uri main l u [t; c] v term in + inspect_exp_named_subst l' (succ v) exp_named_subst + | Cic.Cast (uu, _) -> + inspect_term main l v uu + | Cic.Prod (_, uu, tt) -> + let luu = inspect_term false l (succ v) uu in + inspect_term main luu (succ v) tt + | Cic.Lambda (_, uu, tt) -> + let luu = inspect_term false l (succ v) uu in + inspect_term false luu (succ v) tt + | Cic.LetIn (_, uu, tt) -> + let luu = inspect_term false l (succ v) uu in + inspect_term false luu (succ v) tt + | Cic.Appl m -> inspect_list main l true v m + | Cic.MutCase (u, t, tt, uu, m) -> + let lu = inspect_uri main l u [t] (succ v) term in + let ltt = inspect_term false lu (succ v) tt in + let luu = inspect_term false ltt (succ v) uu in + inspect_list main luu false (succ v) m + | Cic.Fix (_, m) -> inspect_ind l (succ v) m + | Cic.CoFix (_, m) -> inspect_coind l (succ v) m + and inspect_list main l head v = function + | [] -> l + | tt :: m -> + let ltt = inspect_term main l (if head then v else v + 1) tt in + inspect_list false ltt false v m + and inspect_exp_named_subst l v = function + [] -> l + | (_,t) :: tl -> + let l' = inspect_term false l v t in + inspect_exp_named_subst l' v tl + and inspect_ind l v = function + | [] -> l + | (_, _, tt, uu) :: m -> + let ltt = inspect_term false l v tt in + let luu = inspect_term false ltt v uu in + inspect_ind luu v m + and inspect_coind l v = function + | [] -> l + | (_, tt, uu) :: m -> + let ltt = inspect_term false l v tt in + let luu = inspect_term false ltt v uu in + inspect_coind luu v m + in + let rec inspect_backbone = function + | Cic.Cast (uu, _) -> inspect_backbone uu + | Cic.Prod (_, _, tt) -> inspect_backbone tt + | Cic.LetIn (_, uu, tt) -> inspect_backbone tt + | t -> inspect_term true [] 0 t + in + inspect_backbone term + +let get_constraints e c t = + let can = sort_entries (levels_of_term e c t) in (* can restrictions *) + text_of_entries prerr_string can; flush stderr; (* logging *) + let rest_of (u, b, _) = + let p = if b then `MainConclusion None else `InConclusion in (p, u) + in + let rec split vp = function + | [], ((_, _, v) as hd) :: tl -> split v ([rest_of hd], tl) + | prev, ((_, _, ve) as hd) :: tl when vp = ve -> + split vp (rest_of hd :: prev, tl) + | p, l -> p, l + in + let rec mk_musts prev acc = function + | [] -> prev, acc + | l -> + let slice, next = split 0 ([], l) in + let acc = acc @ slice in + mk_musts (prev @ [acc]) acc next + in + mk_musts [] [] can + +let universe = [T.MainConclusion; T.InConclusion] diff --git a/helm/mathql/mathql_generator/cGMatchConclusion.mli b/helm/mathql/mathql_generator/cGMatchConclusion.mli new file mode 100644 index 000000000..a9fbef47f --- /dev/null +++ b/helm/mathql/mathql_generator/cGMatchConclusion.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val get_constraints: Cic.metasenv -> Cic.context -> Cic.term -> + MQGTypes.r_obj list list * + MQGTypes.r_obj list + +val universe : MQGTypes.universe diff --git a/helm/mathql/mathql_generator/cGSearchPattern.ml b/helm/mathql/mathql_generator/cGSearchPattern.ml new file mode 100644 index 000000000..1d7e85937 --- /dev/null +++ b/helm/mathql/mathql_generator/cGSearchPattern.ml @@ -0,0 +1,197 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 02/12/2002 *) +(* *) +(* Missing description *) +(* *) +(******************************************************************************) + +(* $Id$ *) + +module T = MQGTypes +module U = MQGUtil + +type classification = + Backbone of int + | Branch of int + | InConclusion + | InHypothesis +;; + +let soften_classification = + function + Backbone _ -> InConclusion + | Branch _ -> InHypothesis + | k -> k +;; + +let (!!) = + function + Backbone n -> `MainConclusion (Some n) + | Branch n -> `MainHypothesis (Some n) + | _ -> assert false +;; + +let (!!!) = + function + Backbone n -> `MainConclusion (Some n) + | Branch n -> `MainHypothesis (Some n) + | InConclusion -> `InConclusion + | InHypothesis -> `InHypothesis +;; + + +let (@@) (l1,l2,l3) (l1',l2',l3') = + let merge l1 l2 = + List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1 + in + merge l1 l1', merge l2 l2', merge l3 l3' +;; + +let get_constraints term = + let module U = UriManager in + let module C = Cic in + let rec process_type_aux kind = + function + C.Var (uri,expl_named_subst) -> + (* andrea: this is a bug: variable are not indexedin the db + ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ *) + (process_type_aux_expl_named_subst kind expl_named_subst) + | C.Rel _ -> + (match kind with + | InConclusion + | InHypothesis -> [],[],[] + | _ -> [],[!!kind],[]) + | C.Sort s -> + (match kind with + Backbone _ + | Branch _ -> + let s' = + match s with + Cic.Prop -> T.Prop + | Cic.Set -> T.Set + | Cic.Type _ -> T.Type (* TASSI: ?? *) + | Cic.CProp -> T.CProp + in + [],[],[!!kind,s'] + | _ -> [],[],[]) + | C.Meta _ -> [],[],[] (* ???? To be understood *) + | C.Implicit _ -> assert false + | C.Cast (te,_) -> + (* type ignored *) + process_type_aux kind te + | C.Prod (_,sou,ta) -> + let (source_kind,target_kind) = + match kind with + Backbone n -> (Branch 0, Backbone (n+1)) + | Branch n -> (InHypothesis, Branch (n+1)) + | k -> (k,k) + in + process_type_aux source_kind sou @@ + process_type_aux target_kind ta + | C.Lambda (_,sou,ta) -> + let kind' = soften_classification kind in + process_type_aux kind' sou @@ + process_type_aux kind' ta + | C.LetIn (_,te,ta)-> + let kind' = soften_classification kind in + process_type_aux kind' te @@ + process_type_aux kind ta + | C.Appl (he::tl) -> + let kind' = soften_classification kind in + process_type_aux kind he @@ + List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl + | C.Appl _ -> assert false + | C.Const (uri,_) -> + [!!!kind, UriManager.string_of_uri uri],[],[] + | C.MutInd (uri,typeno,expl_named_subst) -> + ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (typeno + 1) ^ ")"],[],[]) @@ + (process_type_aux_expl_named_subst kind expl_named_subst) + | C.MutConstruct (uri,typeno,consno,expl_named_subst) -> + ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[]) + @@ (process_type_aux_expl_named_subst kind expl_named_subst) + | C.MutCase (_,_,_,term,patterns) -> + (* outtype ignored *) + let kind' = soften_classification kind in + process_type_aux kind' term @@ + List.fold_left (fun i t -> i @@ process_type_aux kind' t) + ([],[],[]) patterns + | C.Fix (_,funs) -> + let kind' = soften_classification kind in + List.fold_left + (fun i (_,_,bo,ty) -> + i @@ + process_type_aux kind' bo @@ + process_type_aux kind' ty + ) ([],[],[]) funs + | C.CoFix (_,funs) -> + let kind' = soften_classification kind in + List.fold_left + (fun i (_,bo,ty) -> + i @@ + process_type_aux kind' bo @@ + process_type_aux kind' ty + ) ([],[],[]) funs + and process_type_aux_expl_named_subst kind = + List.fold_left + (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t)) + ([],[],[]) +in + let obj_constraints,rel_constraints,sort_constraints = + process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term) + in + (obj_constraints,rel_constraints,sort_constraints) +;; + +(*CSC: Debugging only *) +(* +let get_constraints term = + let res = get_constraints term in + let (objs,rels,sorts) = res in + let text_of_pos p = + U.text_of_position p ^ " " ^ U.text_of_depth p "NULL" + in + prerr_endline "Constraints on objs:" ; + List.iter + (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ; + prerr_endline "Constraints on Rels:" ; + List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ; + prerr_endline "Constraints on Sorts:" ; + List.iter + (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s) + ) sorts ; + res +;; *) + +let universe = + [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion] diff --git a/helm/mathql/mathql_generator/cGSearchPattern.mli b/helm/mathql/mathql_generator/cGSearchPattern.mli new file mode 100644 index 000000000..528283387 --- /dev/null +++ b/helm/mathql/mathql_generator/cGSearchPattern.mli @@ -0,0 +1,39 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 02/12/2002 *) +(* *) +(* Missing description *) +(* *) +(******************************************************************************) + +val get_constraints : Cic.term -> MQGTypes.must_restrictions + +val universe : MQGTypes.universe diff --git a/helm/mathql/mathql_generator/mQGTypes.ml b/helm/mathql/mathql_generator/mQGTypes.ml new file mode 100644 index 000000000..9ed2ce253 --- /dev/null +++ b/helm/mathql/mathql_generator/mQGTypes.ml @@ -0,0 +1,77 @@ +(* 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/. + *) + +(* AUTORS: Ferruccio Guidi + * Claudio Sacerdoti Coen + *) + +(* $Id$ *) + +(* low level types *********************************************************) + +type uri = string +type position = MainHypothesis + | InHypothesis + | MainConclusion + | InConclusion + | InBody +type depth = int +type sort = Set + | Prop + | Type + | CProp + +type spec = MustObj of uri list * position list * depth list + | MustSort of sort list * position list * depth list + | MustRel of position list * depth list + | OnlyObj of uri list * position list * depth list + | OnlySort of sort list * position list * depth list + | OnlyRel of position list * depth list + | Universe of position list + +(* high-level types ********************************************************) + +type optional_depth = int option + +type full_position = [ `MainHypothesis of optional_depth + | `MainConclusion of optional_depth + | `InHypothesis + | `InConclusion + | `InBody + ] + +type main_position = [ `MainHypothesis of optional_depth + | `MainConclusion of optional_depth + ] + +type r_obj = full_position * uri +type r_sort = main_position * sort +type r_rel = main_position + +type must_restrictions = (r_obj list * r_rel list * r_sort list) +type only_restrictions = + (r_obj list option * r_rel list option * r_sort list option) + +type universe = position list diff --git a/helm/mathql/mathql_generator/mQGUtil.ml b/helm/mathql/mathql_generator/mQGUtil.ml new file mode 100644 index 000000000..7603ab9a6 --- /dev/null +++ b/helm/mathql/mathql_generator/mQGUtil.ml @@ -0,0 +1,150 @@ +(* 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 + *) + +(* $Id$ *) + +module T = MQGTypes + +(* low level functions *****************************************************) + +let string_of_position p = + let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in + match p with + | T.MainHypothesis -> ns ^ "MainHypothesis" + | T.InHypothesis -> ns ^ "InHypothesis" + | T.MainConclusion -> ns ^ "MainConclusion" + | T.InConclusion -> ns ^ "InConclusion" + | T.InBody -> ns ^ "InBody" + +let string_of_sort = function + | T.Set -> "Set" + | T.Prop -> "Prop" + | T.Type -> "Type" + | T.CProp -> "CProp" + +let string_of_depth = string_of_int + +let mathql_of_position = function + | T.MainHypothesis -> "$MH" + | T.InHypothesis -> "$IH" + | T.MainConclusion -> "$MC" + | T.InConclusion -> "$IC" + | T.InBody -> "$IB" + +let mathql_of_sort = function + | T.Set -> "$SET" + | T.Prop -> "$PROP" + | T.Type -> "$TYPE" + | T.CProp -> "$CPROP" + +let mathql_of_depth = string_of_int + +let mathql_of_uri u = u + +let mathql_of_specs out l = + let rec iter f = function + | [] -> () + | [s] -> out "\""; out (f s); out "\"" + | s :: tail -> out "\""; out (f s); out "\", "; iter f tail + in + let txt_uri l = out "{"; iter mathql_of_uri l; out "} " in + let txt_pos l = out "{"; iter mathql_of_position l; out "} " in + let txt_sort l = out "{"; iter mathql_of_sort l; out "} " in + let txt_depth l = out "{"; iter mathql_of_depth l; out "} " in + let txt_spec = function + | T.MustObj (u, p, d) -> out "mustobj "; txt_uri u; txt_pos p; txt_depth d; out "\n" + | T.MustSort (s, p, d) -> out "mustsort "; txt_sort s; txt_pos p; txt_depth d; out "\n" + | T.MustRel ( p, d) -> out "mustrel "; txt_pos p; txt_depth d; out "\n" + | T.OnlyObj (u, p, d) -> out "onlyobj "; txt_uri u; txt_pos p; txt_depth d; out "\n" + | T.OnlySort (s, p, d) -> out "onlysort "; txt_sort s; txt_pos p; txt_depth d; out "\n" + | T.OnlyRel ( p, d) -> out "onlyrel "; txt_pos p; txt_depth d; out "\n" + | T.Universe ( p ) -> out "universe "; txt_pos p; out "\n" + in + List.iter txt_spec l + +let position_of_mathql = function + | "$MH" -> T.MainHypothesis + | "$IH" -> T.InHypothesis + | "$MC" -> T.MainConclusion + | "$IC" -> T.InConclusion + | "$IB" -> T.InBody + | _ -> raise Parsing.Parse_error + +let sort_of_mathql = function + | "$SET" -> T.Set + | "$PROP" -> T.Prop + | "$TYPE" -> T.Type + | "$CPROP" -> T.CProp + | _ -> raise Parsing.Parse_error + +let depth_of_mathql s = + try + let d = int_of_string s in + if d < 0 then raise (Failure "") else d + with Failure _ -> raise Parsing.Parse_error + +let uri_of_mathql s = s + +(* high level functions ****************************************************) + +let text_of_position = function + | `MainHypothesis _ -> "MainHypothesis" + | `MainConclusion _ -> "MainConclusion" + | `InHypothesis -> "InHypothesis" + | `InConclusion -> "InConclusion" + | `InBody -> "InBody" + +let text_of_depth pos no_depth_text = match pos with + | `MainHypothesis (Some d) + | `MainConclusion (Some d) -> string_of_int d + | _ -> no_depth_text + +let text_of_sort = function + | T.Set -> "Set" + | T.Prop -> "Prop" + | T.Type -> "Type" + | T.CProp -> "CProp" + +let is_main_position = function + | `MainHypothesis _ + | `MainConclusion _ -> true + | _ -> false + +let is_conclusion = function + | `MainConclusion _ + | `InConclusion -> true + | _ -> false + +let set_full_position pos depth = match pos with + | `MainHypothesis _ -> `MainHypothesis depth + | `MainConclusion _ -> `MainConclusion depth + | _ -> pos + +let set_main_position pos depth = match pos with + | `MainHypothesis _ -> `MainHypothesis depth + | `MainConclusion _ -> `MainConclusion depth diff --git a/helm/mathql/mathql_generator/mQGUtil.mli b/helm/mathql/mathql_generator/mQGUtil.mli new file mode 100644 index 000000000..065abb157 --- /dev/null +++ b/helm/mathql/mathql_generator/mQGUtil.mli @@ -0,0 +1,69 @@ +(* 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 + *) + +(* low level functions *****************************************************) + +(* these functions give the string representation used in the db ----------*) + +val string_of_position : MQGTypes.position -> string +val string_of_depth : MQGTypes.depth -> string +val string_of_sort : MQGTypes.sort -> string + +(* these functions give the string representation used in MathQL ----------*) + +val mathql_of_position : MQGTypes.position -> string +val mathql_of_depth : MQGTypes.depth -> string +val mathql_of_uri : MQGTypes.uri -> string +val mathql_of_sort : MQGTypes.sort -> string + +val mathql_of_specs : (string -> unit) -> MQGTypes.spec list -> unit + +val position_of_mathql : string -> MQGTypes.position +val depth_of_mathql : string -> MQGTypes.depth +val uri_of_mathql : string -> MQGTypes.uri +val sort_of_mathql : string -> MQGTypes.sort + +(* high level functions ****************************************************) + +(* these functions give the textual representation used by umans ----------*) + +val text_of_position : MQGTypes.full_position -> string +val text_of_depth : MQGTypes.full_position -> string -> string +val text_of_sort : MQGTypes.sort -> string + +(* these functions classify the positions ---------------------------------*) + +val is_main_position : MQGTypes.full_position -> bool +val is_conclusion : MQGTypes.full_position -> bool + +(* these function apply changes to positions ------------------------------*) + +val set_full_position : MQGTypes.full_position -> MQGTypes.optional_depth -> + MQGTypes.full_position +val set_main_position : MQGTypes.main_position -> MQGTypes.optional_depth -> + MQGTypes.main_position diff --git a/helm/mathql/mathql_generator/mQueryGenerator.ml b/helm/mathql/mathql_generator/mQueryGenerator.ml new file mode 100644 index 000000000..784bc11dc --- /dev/null +++ b/helm/mathql/mathql_generator/mQueryGenerator.ml @@ -0,0 +1,191 @@ +(* 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 + *) + +(* $Id$ *) + +module M = MathQL +module T = MQGTypes +module U = MQGUtil + +(* low level functions *****************************************************) + +let locate s = + let query = + M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) ) + in query + +let unreferred target_pattern source_pattern = + let query = + M.Bin (M.BinFDiff, + ( + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const target_pattern)) + ), ( + M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern)) + + )) + in query + +let compose cl = + let letin = ref [] in + let must = ref [] in + let onlyobj = ref [] in + let onlysort = ref [] in + let onlyrel = ref [] in + let only = ref true in + let univ = ref [] in + let set_val = function + | [s] -> M.Const s + | l -> + let msval = M.Set (List.map (fun s -> M.Const s) l) in + if ! only then begin + let vvar = "val" ^ string_of_int (List.length ! letin) in + letin := (vvar, msval) :: ! letin; + M.VVar vvar + end else msval + in + let cons o (r, s, p, d) = + let con p = function + | [] -> [] + | l -> [(false, [p], set_val l)] + in + only := o; + con "h:occurrence" r @ + con "h:sort" (List.map U.string_of_sort s) @ + con "h:position" (List.map U.string_of_position p) @ + 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,(M.Const "")) + in + let property_only n cl = + let rec build = function + | [] -> [] + | c :: tl -> + let r = (cons true) c in + if r = [] then build tl else r :: build tl + in + let cll = build cl in + M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) + in + let rec aux = function + | [] -> () + | T.Universe l :: tail -> + 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 -> + must := property_must "refObj" (r, [], p, d) :: ! must; aux tail + | T.MustSort(s,p,d) :: tail -> + must := property_must "refSort" ([], s, p, d) :: ! must; aux tail + | T.MustRel(p,d) :: tail -> + must := property_must "refRel" ([], [], p, d) :: ! must; aux tail + | T.OnlyObj(r,p,d) :: tail -> + onlyobj := (r, [], p, d) :: ! onlyobj; aux tail + | T.OnlySort(s,p,d) :: tail -> + onlysort := ([], s, p, d) :: ! onlysort; aux tail + | T.OnlyRel(p,d) :: tail -> + onlyrel := ([], [], p, d) :: ! onlyrel; aux tail + in + let rec iter f g = function + | [] -> raise (Failure "MQueryGenerator.iter") + | [head] -> (f head) + | head :: tail -> let t = (iter f g tail) in g (f head) t + in + (* prerr_endline "(** Compose: received constraints **)"; + U.mathql_of_specs prerr_string cl; flush stderr; *) + aux cl; + let must_query = + if ! must = [] then + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*")) + else + iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must + in + let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in + let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in + let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in + let select_query x = + match ! onlyobj, ! onlysort, ! onlyrel with + | [], [], [] -> x + | _, [], [] -> M.Select("obj",x,onlyobj_val) + | [], _, [] -> M.Select("obj",x,onlysort_val) + | [], [], _ -> M.Select("obj",x,onlyrel_val) + | _, _, [] -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val))) + | _, [], _ -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val))) + | [], _, _ -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val))) + | _, _, _ -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val))) + in + let letin_query = + if ! letin = [] then fun x -> x + else + let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in + iter f (fun x y z -> x (y z)) ! letin + in + letin_query (select_query must_query) + +(* high-level functions ****************************************************) + +let query_of_constraints u (musts_obj, musts_rel, musts_sort) + (onlys_obj, onlys_rel, onlys_sort) = + let conv = function + | `MainHypothesis None -> [T.MainHypothesis], [] + | `MainHypothesis (Some d) -> [T.MainHypothesis], [d] + | `MainConclusion None -> [T.MainConclusion], [] + | `MainConclusion (Some d) -> [T.MainConclusion], [d] + | `InHypothesis -> [T.InHypothesis], [] + | `InConclusion -> [T.InConclusion], [] + | `InBody -> [T.InBody], [] + in + let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in + let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in + let must_rel p = let p, d = conv p in T.MustRel (p, d) in + let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in + let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in + let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in + let must = List.map must_obj musts_obj @ + List.map must_rel musts_rel @ + List.map must_sort musts_sort + in + let only = + (match onlys_obj with + | None -> [] + | Some [] -> [T.OnlyObj ([], [], [])] + | Some l -> List.map only_obj l + ) @ + (match onlys_rel with + | None -> [] + | Some [] -> [T.OnlyRel ([], [])] + | Some l -> List.map only_rel l + ) @ + (match onlys_sort with + | None -> [] + | Some [] -> [T.OnlySort ([], [], [])] + | Some l -> List.map only_sort l + ) + in + let univ = match u with None -> [] | Some l -> [T.Universe l] in + compose (must @ only @ univ) diff --git a/helm/mathql/mathql_generator/mQueryGenerator.mli b/helm/mathql/mathql_generator/mQueryGenerator.mli new file mode 100644 index 000000000..decaa0ea7 --- /dev/null +++ b/helm/mathql/mathql_generator/mQueryGenerator.mli @@ -0,0 +1,42 @@ +(* 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 + *) + +(* interface for the low-level constraints *********************************) + +val locate : string -> MathQL.query + +val unreferred : string -> string -> MathQL.query + +val compose : MQGTypes.spec list -> MathQL.query + +(* interface for the high-level constraints ********************************) + +val query_of_constraints : MQGTypes.universe option -> + MQGTypes.must_restrictions -> + MQGTypes.only_restrictions -> + MathQL.query diff --git a/helm/mathql/mathql_interpreter/.depend b/helm/mathql/mathql_interpreter/.depend new file mode 100644 index 000000000..186c81793 --- /dev/null +++ b/helm/mathql/mathql_interpreter/.depend @@ -0,0 +1,27 @@ +mQIPostgres.cmi: mQITypes.cmo +mQIMySql.cmi: mQITypes.cmo +mQIConn.cmi: mQITypes.cmo mQIMap.cmi +mQIProperty.cmi: mQITypes.cmo mQIConn.cmi +mQueryInterpreter.cmi: mQIConn.cmi +mQueryTParser.cmo: mQueryTParser.cmi +mQueryTParser.cmx: mQueryTParser.cmi +mQueryTLexer.cmo: mQueryTParser.cmi +mQueryTLexer.cmx: mQueryTParser.cmx +mQueryUtil.cmo: mQueryTParser.cmi mQueryTLexer.cmo mQueryUtil.cmi +mQueryUtil.cmx: mQueryTParser.cmx mQueryTLexer.cmx mQueryUtil.cmi +mQIUtil.cmo: mQIUtil.cmi +mQIUtil.cmx: mQIUtil.cmi +mQIPostgres.cmo: mQIPostgres.cmi +mQIPostgres.cmx: mQIPostgres.cmi +mQIMySql.cmo: mQIMySql.cmi +mQIMySql.cmx: mQIMySql.cmi +mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi +mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi +mQIConn.cmo: mQIPostgres.cmi mQIMySql.cmi mQIMap.cmi mQIConn.cmi +mQIConn.cmx: mQIPostgres.cmx mQIMySql.cmx mQIMap.cmx mQIConn.cmi +mQIProperty.cmo: mQIUtil.cmi mQIMap.cmi mQIConn.cmi mQIProperty.cmi +mQIProperty.cmx: mQIUtil.cmx mQIMap.cmx mQIConn.cmx mQIProperty.cmi +mQueryInterpreter.cmo: mQueryUtil.cmi mQIUtil.cmi mQIProperty.cmi mQIConn.cmi \ + mQueryInterpreter.cmi +mQueryInterpreter.cmx: mQueryUtil.cmx mQIUtil.cmx mQIProperty.cmx mQIConn.cmx \ + mQueryInterpreter.cmi diff --git a/helm/mathql/mathql_interpreter/Makefile b/helm/mathql/mathql_interpreter/Makefile new file mode 100644 index 000000000..bdd738135 --- /dev/null +++ b/helm/mathql/mathql_interpreter/Makefile @@ -0,0 +1,19 @@ +PACKAGE = mathql_interpreter + +PREDICATES = + +INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \ + mQIPostgres.mli mQIMySql.mli mQIMap.mli mQIConn.mli \ + mQIProperty.mli mQueryInterpreter.mli + +IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \ + mQITypes.ml $(INTERFACE_FILES:%.mli=%.ml) + +EXTRA_OBJECTS_TO_INSTALL = mQueryTLexer.cmi \ + mQueryTLexer.mll mQueryTParser.mly \ + mQITypes.ml mQITypes.cmi + +EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ + mQueryTLexer.ml + +include ../Makefile.common diff --git a/helm/mathql/mathql_interpreter/mQIConn.ml b/helm/mathql/mathql_interpreter/mQIConn.ml new file mode 100644 index 000000000..270d1f9d0 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIConn.ml @@ -0,0 +1,130 @@ +(* 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 + *) + +(* $Id$ *) + +type connection = MySQL_C of HMysql.dbd + | Postgres_C of Postgres.connection + | No_C + +type flag = Galax | Postgres | Queries | Result | Source | Times | Warn + +type handle = { + log : string -> unit; (* logging function *) + set : flag list; (* options *) + pgc : connection; (* PG connection *) + pgm : MQIMap.pg_map; (* PG conversion function *) + pga : MQIMap.pg_alias (* PG table aliases *) +} + +let tables handle p = MQIMap.get_tables handle.pgm p + +let field handle p t = MQIMap.get_field handle.pgm p t + +let resolve handle a = MQIMap.resolve handle.pga a + +let log handle = handle.log + +let set handle flag = List.mem flag handle.set + +let pgc handle = handle.pgc + +let flags handle = handle.set + +let string_of_flag = function + | Galax -> "G" + | Postgres -> "P" + | Queries -> "Q" + | Result -> "R" + | Source -> "S" + | Times -> "T" + | Warn -> "W" + +let flag_of_char = function + | 'G' -> [Galax] + | 'P' -> [Postgres] + | 'Q' -> [Queries] + | 'R' -> [Result] + | 'S' -> [Source] + | 'T' -> [Times] + | 'W' -> [Warn] + | _ -> [] + +let string_fold_left f a s = + let l = String.length s in + let rec aux b i = if i = l then b else aux (f b s.[i]) (succ i) in + aux a 0 + +let string_of_flags flags = + List.fold_left (fun s flag -> s ^ string_of_flag flag) "" flags + +let flags_of_string s = + string_fold_left (fun l c -> l @ flag_of_char c) [] s + +let init ?(flags = []) ?(log = ignore) () = + let flags = + if flags = [] then + flags_of_string (Helm_registry.get "mathql_interpreter.flags") + else + flags + in + let m, a = + let g = + if List.mem Galax flags + then MQIMap.empty_map else MQIMap.read_map + in g () + in + {log = log; set = flags; + pgc = begin + try + if List.mem Galax flags then No_C else + if List.mem Postgres flags then Postgres_C (MQIPostgres.init ()) else + MySQL_C (MQIMySql.init ()) + with Failure "mqi_connection" -> No_C + end; + pgm = m; pga = a + } + +let close handle = + match pgc handle with + | MySQL_C c -> MQIMySql.close c + | Postgres_C c -> MQIPostgres.close c + | No_C -> () + +let exec handle out table cols ct cfl = + match pgc handle with + | MySQL_C c -> MQIMySql.exec (c, out) table cols ct cfl + | Postgres_C c -> MQIPostgres.exec (c, out) table cols ct cfl + | No_C -> [] + +let connected handle = + pgc handle <> No_C + +let init_if_connected ?(flags = []) ?(log = ignore) () = + let handle = init ~flags:flags ~log:log () in + if connected handle then handle else raise (Failure "mqi connection failed") diff --git a/helm/mathql/mathql_interpreter/mQIConn.mli b/helm/mathql/mathql_interpreter/mQIConn.mli new file mode 100644 index 000000000..35c8b3ef0 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIConn.mli @@ -0,0 +1,65 @@ +(* 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 + *) + +type connection = MySQL_C of HMysql.dbd + | Postgres_C of Postgres.connection + | No_C + +type flag = Galax | Postgres | Queries | Result | Source | Times | Warn + +type handle = { + log : string -> unit; (* logging function *) + set : flag list; (* options *) + pgc : connection; (* PG connection *) + pgm : MQIMap.pg_map; (* PG conversion function *) + pga : MQIMap.pg_alias (* PG table aliases *) +} + +val string_of_flags : flag list -> string +val flags_of_string : string -> flag list + +val init : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> handle +val close : handle -> unit +val connected : handle -> bool +val exec : handle -> (MQITypes.query -> unit) -> + MQITypes.table -> MQITypes.columns -> + string MQITypes.con_true -> string MQITypes.con_false -> + MQITypes.result + +val init_if_connected : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> handle + +(* The following functions allow to read the handle internal fields. + * For exclusive use of the interpreter. + *) + +val log : handle -> string -> unit +val set : handle -> flag -> bool +val flags : handle -> flag list +val tables : handle -> MathQL.path -> MQIMap.pg_tables +val field : handle -> MathQL.path -> string -> string +val resolve : handle -> string -> string diff --git a/helm/mathql/mathql_interpreter/mQIMap.ml b/helm/mathql/mathql_interpreter/mQIMap.ml new file mode 100644 index 000000000..a5b6654c8 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIMap.ml @@ -0,0 +1,93 @@ +(* 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 + *) + +(* $Id$ *) + +module U = MQueryUtil + +type pg_map = (MathQL.path * (bool * string * string option)) list + +type pg_tables = (bool * string) list + +type pg_alias = (string * string) list + +let empty_map () = [], [] + +let read_map () = + let map = Helm_registry.get "mathql_interpreter.db_map" in + let ich = open_in map in + let rec aux r s = + let d = input_line ich in + match Str.split (Str.regexp "[ \t]+") d with + | [] -> aux r s + | "#" :: _ -> aux r s + | t :: "<-" :: p -> aux ((p, (false, t, None)) :: r) s + | t :: c :: "<-" :: p -> aux ((p, (false, t, Some c)) :: r) s + | t :: "<+" :: p -> aux ((p, (true, t, None)) :: r) s + | t :: c :: "<+" :: p -> aux ((p, (true, t, Some c)) :: r) s + | [a; "->"; t] -> aux r ((a, t) :: s) + | ["->"] -> r, s + | _ -> raise (Failure "MQIMap.read_map") + in + let pgm, pga = aux [] [] in + close_in ich; + pgm, pga + +let comp c1 c2 = match c1, c2 with + | (_, t1), (_, t2) when t1 < t2 -> U.Lt + | (_, t1), (_, t2) when t1 > t2 -> U.Gt + | (b1, t), (b2, _) -> U.Eq (b1 || b2, t) + +let get_tables pgm p = + let aux l = function + | q, (b, t, _) when q = p -> U.list_join comp l [(b, t)] + | _, _ -> l + in + List.fold_left aux [] pgm + +let rec refine_tables l1 l2 = + U.list_meet comp l1 l2 + +let default_table = function + | [(_, a)] -> a + | l -> + try List.assoc true l + with Not_found -> raise (Failure "MQIMap.default_table") + +let get_field pgm p t = + let aux = function + | q, (_, u, _) when q = p && u = t -> true + | _ -> false + in + match List.filter aux pgm with + | [_, (_, _, None)] -> "" + | [_, (_, _, Some c)] -> c + | _ -> raise (Failure "MQIMap.get_field") + +let resolve pga a = + try List.assoc a pga with Not_found -> a diff --git a/helm/mathql/mathql_interpreter/mQIMap.mli b/helm/mathql/mathql_interpreter/mQIMap.mli new file mode 100644 index 000000000..50f5bb0fa --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIMap.mli @@ -0,0 +1,47 @@ +(* 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 + *) + +type pg_map (* mathql path map for postgres *) + +type pg_tables + +type pg_alias + +val empty_map : unit -> pg_map * pg_alias + +val read_map : unit -> pg_map * pg_alias + +val get_tables : pg_map -> MathQL.path -> pg_tables + +val refine_tables : pg_tables -> pg_tables -> pg_tables + +val default_table : pg_tables -> string + +val get_field : pg_map -> MathQL.path -> string -> string + +val resolve : pg_alias -> string -> string diff --git a/helm/mathql/mathql_interpreter/mQIMySql.ml b/helm/mathql/mathql_interpreter/mQIMySql.ml new file mode 100644 index 000000000..3380e1f1f --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIMySql.ml @@ -0,0 +1,96 @@ +(* 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 + *) + +(* $Id$ *) + +let init () = + let module HR = Helm_registry in + let host = + HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.host" in + let database = + HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.database" in + let user = + HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.user" in + let port = + HR.get_opt HR.get_int "mathql_interpreter.mysql_connection.port" in + let password = + HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.password" in + try HMysql.quick_connect ?host ?database ?user ?port ?password () + with _ -> raise (Failure "mqi_connecion") + +let close c = HMysql.disconnect c + +let quote s = + let rec quote_aux s = + try + let l = String.length s in + let i = String.index s '\'' in + String.sub s 0 i ^ "\\'" ^ quote_aux (String.sub s (succ i) (l - (succ i))) + with Not_found -> s + in + "'" ^ quote_aux s ^ "'" + +let exec (c, out) q = + let g = function None -> "" | Some v -> v in + let f a = List.map g (Array.to_list a) in + out q; HMysql.map ~f:f (Mysql.exec c q) + +let exec c table cols ct cfl = + let rec iter f last sep = function + | [] -> last + | [head] -> f head + | head :: tail -> f head ^ sep ^ iter f last sep tail + in + let pg_cols = iter (fun x -> x) "" ", " cols in + let pg_msval v = iter quote "" ", " v in + let pg_con (pat, col, v) = + if col <> "" then + let f s = col ^ " regexp " ^ quote ("^" ^ s ^ "$") in + if pat then "(" ^ iter f "0" " or " v ^ ")" + else match v with + | [s] -> col ^ " = " ^ (quote s) + | v -> col ^ " in (" ^ pg_msval v ^ ")" + else "1" + in + let pg_cons l = iter pg_con "1" " and " l in + let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in + let pg_cons_not_l ll = iter pg_cons_not "1" " and " ll in + let pg_where = match ct, cfl with + | [], [] -> "" + | lt, [] -> " where " ^ pg_cons lt + | [], llf -> " where " ^ pg_cons_not_l llf + | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf + in + if cols = [] then + let r = exec c ("select count(source) from " ^ table ^ pg_where) in + match r with + | [[s]] when int_of_string s > 0 -> [[]] + | _ -> [] + else + exec c ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ + " order by " ^ List.hd cols ^ " asc") diff --git a/helm/mathql/mathql_interpreter/mQIMySql.mli b/helm/mathql/mathql_interpreter/mQIMySql.mli new file mode 100644 index 000000000..8afaf401d --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIMySql.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val init : unit -> HMysql.dbd + +val close : HMysql.dbd -> unit + +val exec : HMysql.dbd * (MQITypes.query -> unit) -> + MQITypes.table -> MQITypes.columns -> + string MQITypes.con_true -> string MQITypes.con_false -> + MQITypes.result diff --git a/helm/mathql/mathql_interpreter/mQIPostgres.ml b/helm/mathql/mathql_interpreter/mQIPostgres.ml new file mode 100644 index 000000000..bef07230f --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIPostgres.ml @@ -0,0 +1,96 @@ +(* 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 + *) + +(* $Id$ *) + +let init () = + let connection_string = + Helm_registry.get "mathql_interpreter.postgresql_connection_string" + in + try new Postgres.connection connection_string + with _ -> raise (Failure "mqi_connecion") + +let close c = c#close + +let quote s = + let rec quote_aux s = + try + let l = String.length s in + let i = String.index s '\'' in + String.sub s 0 i ^ "\\'" ^ quote_aux (String.sub s (succ i) (l - (succ i))) + with Not_found -> s + in + "'" ^ quote_aux s ^ "'" + +let exec (c, out) q = out q; (c#exec q)#get_list + +let exec c table cols ct cfl = + let rec iter f last sep = function + | [] -> last + | [head] -> f head + | head :: tail -> f head ^ sep ^ iter f last sep tail + in + let pg_cols = iter (fun x -> x) "" ", " cols in + let pg_msval v = iter quote "" ", " v in + let pg_con (pat, col, v) = + if col <> "" then + let f s = col ^ " ~ " ^ quote ("^" ^ s ^ "$") in + if pat then "(" ^ iter f "false" " or " v ^ ")" + else match v with + | [s] -> col ^ " = " ^ (quote s) + | v -> col ^ " in (" ^ pg_msval v ^ ")" + else "true" + in + let pg_cons l = iter pg_con "true" " and " l in + let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in + let pg_cons_not_l ll = iter pg_cons_not "true" " and " ll in + let pg_where = match ct, cfl with + | [], [] -> "" + | lt, [] -> " where " ^ pg_cons lt + | [], llf -> " where " ^ pg_cons_not_l llf + | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf + in + if cols = [] then + let r = exec c ("select count(source) from " ^ table ^ pg_where) in + match r with + | [[s]] when int_of_string s > 0 -> [[]] + | _ -> [] + else + exec c ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ + " order by " ^ List.hd cols ^ " asc") + +(* funzioni vecchie ********************************************************) +(* +let pg_name h s = + let q = "select id from registry where uri = " ^ quote s in + match exec h q with + | [[id]] -> "t" ^ id + | _ -> "" + +let get_id b = if b then ["B"] else ["F"] +*) diff --git a/helm/mathql/mathql_interpreter/mQIPostgres.mli b/helm/mathql/mathql_interpreter/mQIPostgres.mli new file mode 100644 index 000000000..cbbf3929d --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIPostgres.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val init : unit -> Postgres.connection + +val close : Postgres.connection -> unit + +val exec : Postgres.connection * (MQITypes.query -> unit) -> + MQITypes.table -> MQITypes.columns -> + string MQITypes.con_true -> string MQITypes.con_false -> + MQITypes.result diff --git a/helm/mathql/mathql_interpreter/mQIProperty.ml b/helm/mathql/mathql_interpreter/mQIProperty.ml new file mode 100644 index 000000000..0e3e2be72 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIProperty.ml @@ -0,0 +1,103 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +(* $Id$ *) + +module M = MathQL +module C = MQIConn +module U = MQIUtil +module A = MQIMap + +let not_supported s = + raise (Failure ("MQIProperty: feature not supported: " ^ s)) + +(* debugging ***************************************************************) + +let pg_print l = + let rec pg_record = function + | [] -> prerr_newline () + | head :: tail -> prerr_string (head ^ " "); pg_record tail + in + List.iter pg_record l + +let cl_print l = + let c_print (b, p, v) = + prerr_string (if b then "match " else "in "); + List.iter (fun x -> prerr_string ("/" ^ x)) p; + prerr_newline (); + List.iter prerr_endline v + in + List.iter c_print l + +(* 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 get_name = function (p, None) -> p | (_, Some p) -> p in + let names = List.map get_name el in + let mk_grp l = + let grp = U.mql_iter2 (fun p s -> [(p, [s])]) names l in + if grp = [] then [] else [grp] + in + let mk_avs l = + if subj = "" then ("", mk_grp l) else (List.hd l, mk_grp (List.tl l)) + in + compose mk_avs res + +let get_table h mc ct cfl el = + let aux_c ts (_, p, _) = A.refine_tables ts (C.tables h p) in + let aux_e ts (p, _) = A.refine_tables ts (C.tables h p) in + let fst = C.tables h mc in + let snd = List.fold_left aux_c fst (ct @ (List.concat cfl)) in + let trd = List.fold_left aux_e snd el in + A.default_table trd + +let exec_single h mc ct cfl el table = + let conv p = C.field h p table in + let first = conv mc in + let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in + let cons_true = mk_con ct in + let cons_false = List.map mk_con cfl in + let other_cols = List.map (fun (p, _) -> conv p) el in + let cols = if first = "" then other_cols else first :: other_cols in + let out q = if C.set h C.Queries then C.log h (q ^ "\n") in + let r = C.exec h out (C.resolve h table) cols cons_true cons_false in + pg_result false first el r + +let deadline = 100 + +let exec h refine mc ct cfl el = + if refine <> M.RefineExact then not_supported "exec"; + let table = get_table h mc ct cfl el in + let rec exec_aux ct = match ct with + | (pat, p, v) :: tail when List.length v > deadline -> + let single s = exec_aux ((pat, p, [s]) :: tail) in + U.mql_iter single v + | _ -> + exec_single h mc ct cfl el table + in exec_aux ct diff --git a/helm/mathql/mathql_interpreter/mQIProperty.mli b/helm/mathql/mathql_interpreter/mQIProperty.mli new file mode 100644 index 000000000..f8159aaa8 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIProperty.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val exec: MQIConn.handle -> + MathQL.refine -> MathQL.path -> + MathQL.path MQITypes.con_true -> MathQL.path MQITypes.con_false -> + MathQL.exp_list -> MathQL.result diff --git a/helm/mathql/mathql_interpreter/mQITypes.ml b/helm/mathql/mathql_interpreter/mQITypes.ml new file mode 100644 index 000000000..ad4a8cb1b --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQITypes.ml @@ -0,0 +1,43 @@ +(* 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 + *) + +(* $Id$ *) + +type 'a con = MathQL.pattern * 'a * MathQL.value + +type 'a con_true = 'a con list + +type 'a con_false = 'a con list list + +type table = string + +type columns = string list + +type result = string list list + +type query = string diff --git a/helm/mathql/mathql_interpreter/mQIUtil.ml b/helm/mathql/mathql_interpreter/mQIUtil.ml new file mode 100644 index 000000000..3f3fe6591 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIUtil.ml @@ -0,0 +1,155 @@ +(* 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 + *) + +(* $Id$ *) + +(* boolean constants *******************************************************) + +let mql_false = [] + +let mql_true = [""] + +(* set theoretic operations *************************************************) + +let rec set_sub v1 v2 = + match v1, v2 with + | [], _ -> mql_true + | _, [] -> mql_false + | h1 :: _, h2 :: _ when h1 < h2 -> mql_false + | h1 :: _, h2 :: t2 when h1 > h2 -> set_sub v1 t2 + | _ :: t1, _ :: t2 -> set_sub t1 t2 + +let rec set_meet v1 v2 = + match v1, v2 with + | [], _ -> mql_false + | _, [] -> mql_false + | h1 :: t1, h2 :: _ when h1 < h2 -> set_meet t1 v2 + | h1 :: _, h2 :: t2 when h1 > h2 -> set_meet v1 t2 + | _, _ -> mql_true + +let set_eq v1 v2 = + if v1 = v2 then mql_true else mql_false + +let rec set_union v1 v2 = + match v1, v2 with + | [], v -> v + | v, [] -> v + | 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 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 ******************************************************) + +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 diff --git a/helm/mathql/mathql_interpreter/mQIUtil.mli b/helm/mathql/mathql_interpreter/mQIUtil.mli new file mode 100644 index 000000000..76735a863 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQIUtil.mli @@ -0,0 +1,69 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val mql_true : MathQL.value + +val mql_false : MathQL.value + +val set_sub : MathQL.value -> MathQL.value -> MathQL.value + +val set_meet : MathQL.value -> MathQL.value -> MathQL.value + +val set_eq : MathQL.value -> MathQL.value -> MathQL.value + +val set_union : 'a list -> 'a list -> 'a list + +val 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_prod : MathQL.attribute_set -> MathQL.attribute_set -> + MathQL.attribute_set + +val mql_intersect : MathQL.result -> MathQL.result -> MathQL.result + +val mql_diff : MathQL.result -> MathQL.result -> MathQL.result + +val iter : ('a -> 'b list) -> 'a list -> 'b list + +val mql_iter : ('c -> ('a * 'b list) list) -> 'c list -> + ('a * 'b list) list + +val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list -> + 'd list -> ('a * 'b list) list + +val xor : MathQL.value -> MathQL.value -> MathQL.value + +val le : MathQL.value -> MathQL.value -> MathQL.value + +val lt : MathQL.value -> MathQL.value -> MathQL.value + +val align : string -> string -> MathQL.value + +val set : string * 'a -> (string * 'a) list -> (string * 'a) list diff --git a/helm/mathql/mathql_interpreter/mQueryInterpreter.ml b/helm/mathql/mathql_interpreter/mQueryInterpreter.ml new file mode 100644 index 000000000..9280a2c2a --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQueryInterpreter.ml @@ -0,0 +1,247 @@ +(* 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 + *) + +(* $Id$ *) + +(* contexts *****************************************************************) + +type svar_context = (MathQL.svar * MathQL.resource_set) list + +type avar_context = (MathQL.avar * MathQL.resource) list + +type group_context = (MathQL.avar * MathQL.attribute_group) list + +type vvar_context = (MathQL.vvar * MathQL.value) list + +type context = {svars: svar_context; + avars: avar_context; + groups: group_context; (* auxiliary context *) + vvars: vvar_context + } + +(* execute *****************************************************************) + +exception Found + +module M = MathQL +module P = MQueryUtil +module C = MQIConn +module U = MQIUtil + +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) "\n" q + end + in + let rec eval_val c = function + | M.False -> U.mql_false + | M.True -> U.mql_true + | M.Const s -> [s] + | M.Set l -> U.iter (eval_val c) l + | M.Test (k,y1,y2) -> + let cand y1 y2 = + if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2 + in + let cor y1 y2 = + let v1 = eval_val c y1 in + if v1 = U.mql_false then eval_val c y2 else v1 + in + let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in + let f = match k with + | M.And -> cand + | M.Or -> cor + | M.Xor -> h U.xor + | M.Sub -> h U.set_sub + | M.Meet -> h U.set_meet + | M.Eq -> h U.set_eq + | M.Le -> h U.le + | M.Lt -> h U.lt + in + f y1 y2 + | M.Not y -> + if eval_val c y = U.mql_false then U.mql_true else U.mql_false + | M.VVar i -> begin + try List.assoc i c.vvars + with Not_found -> warn (M.Subj (M.VVar i)); [] end + | M.Dot (i,p) -> begin + try List.assoc p (List.assoc i c.groups) + with Not_found -> warn (M.Subj (M.Dot (i,p))); [] end + | M.Proj (None,x) -> List.map (fun (r, _) -> r) (eval_query c x) + | M.Proj ((Some p),x) -> + let proj_group_aux (q, v) = if q = p then v else [] in + let proj_group a = U.iter proj_group_aux a in + let proj_set (_, g) = U.iter proj_group g in + U.iter proj_set (eval_query c x) + | M.Ex (l,y) -> + let rec ex_aux h = function + | [] -> + let d = {c with groups = h} in + if eval_val d y = U.mql_false then () else raise Found + | i :: tail -> + begin + try + let (_, a) = List.assoc i c.avars in + let rec add_group = function + | [] -> () + | g :: t -> ex_aux ((i, g) :: h) tail; add_group t + in + add_group a + with Not_found -> () + end + in + (try ex_aux [] l; U.mql_false with Found -> U.mql_true) + | M.StatVal y -> + let t = 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) "\n" x; + let s = P.stop_time t in + if C.set h C.Times 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) "\n" s; + let r = P.stop_time t in + if C.set h C.Times 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 + eval_query d x2 + | M.LetVVar (i,y,x) -> + let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in + eval_query d x + | M.For (k,i,x1,x2) -> + let f = match k with + | M.GenFJoin -> U.mql_union + | M.GenFMeet -> U.mql_intersect + in + let rec for_aux = function + | [] -> [] + | h :: t -> + let d = {c with avars = U.set (i, h) c.avars} in + f (eval_query d x2) (for_aux t) + in + for_aux (eval_query c x1) + | M.Add (b,z,x) -> + let f = if b then U.mql_prod else U.set_union in + let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in + List.fold_right g (eval_query c x) [] + | M.Property (q0,q1,q2,mc,ct,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) + in + let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in + let cons_true = mct :: List.map eval_cons ct in + let cons_false = List.map (List.map eval_cons) cfl in + let eval_exp (p, po) = (q2 @ p, po) in + let exp = List.map eval_exp el in + let t = P.start_time () in + 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.Times 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 + then select_aux t else h :: select_aux t + in + select_aux (eval_query c x) + | M.Keep (b,l,x) -> + let keep_path (p, v) t = + if List.mem p l = b then t else (p, v) :: t in + let keep_grp a = List.fold_right keep_path a [] in + let keep_set a g = + let kg = keep_grp a in + if kg = [] then g else kg :: g + in + let keep_av (s, g) = (s, List.fold_right keep_set g []) in + List.map keep_av (eval_query c x) + and eval_grp c = function + | M.Attr gs -> + let attr_aux g (p, y) = U.mql_union g [(p, eval_val 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 t = P.start_time () in + if C.set h C.Source then P.text_of_query (C.log h) "\n" x; + let r = eval_query c x in + if C.set h C.Result then P.text_of_result (C.log h) "\n" r; + let s = P.stop_time t in + if C.set h C.Times then + C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s + (C.string_of_flags (C.flags h))); + r diff --git a/helm/mathql/mathql_interpreter/mQueryInterpreter.mli b/helm/mathql/mathql_interpreter/mQueryInterpreter.mli new file mode 100644 index 000000000..9d7081fff --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQueryInterpreter.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val execute : MQIConn.handle -> MathQL.query -> MathQL.result diff --git a/helm/mathql/mathql_interpreter/mQueryTLexer.mll b/helm/mathql/mathql_interpreter/mQueryTLexer.mll new file mode 100644 index 000000000..ca51751f0 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQueryTLexer.mll @@ -0,0 +1,133 @@ +(* 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 + *) + +{ + open MQueryTParser + + let debug = false + + let out s = if debug then prerr_endline s +} + +let SPC = [' ' '\t' '\n']+ +let ALPHA = ['A'-'Z' 'a'-'z' '_'] +let NUM = ['0'-'9'] +let IDEN = ALPHA (NUM | ALPHA)* +let QSTR = [^ '"' '\\']+ + +rule comm_token = parse + | "(*" { comm_token lexbuf; comm_token lexbuf } + | "*)" { () } + | ['*' '('] { comm_token lexbuf } + | [^ '*' '(']* { comm_token lexbuf } +and string_token = parse + | '"' { DQ } + | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } + | QSTR { STR (Lexing.lexeme lexbuf) } + | eof { EOF } +and query_token = parse + | "(*" { comm_token lexbuf; query_token lexbuf } + | SPC { query_token lexbuf } + | '"' { let str = qstr string_token lexbuf in + out ("STR " ^ str); STR str } + | '(' { out "LP"; LP } + | ')' { out "RP"; RP } + | '{' { out "LC"; LC } + | '}' { out "RC"; RC } + | '@' { out "AT"; AT } + | '%' { out "PC"; PC } + | '$' { out "DL"; DL } + | '.' { out "FS"; FS } + | ',' { out "CM"; CM } + | ';' { out "SC"; SC } + | '/' { out "SL"; SL } + | "add" { out "ADD" ; ADD } + | "align" { out "ALIGN" ; ALIGN } + | "allbut" { out "BUT" ; BUT } + | "and" { out "AND" ; AND } + | "as" { out "AS" ; AS } + | "attr" { out "ATTR" ; ATTR } + | "be" { out "BE" ; BE } + | "count" { out "COUNT" ; COUNT } + | "diff" { out "DIFF" ; DIFF } + | "distr" { out "DISTR" ; DISTR } + | "else" { out "ELSE" ; ELSE } + | "empty" { out "EMPTY" ; EMPTY } + | "eq" { out "EQ" ; EQ } + | "ex" { out "EX" ; EX } + | "false" { out "FALSE" ; FALSE } + | "for" { out "FOR" ; FOR } + | "from" { out "FROM" ; FROM } + | "if" { out "IF" ; IF } + | "in" { out "IN" ; IN } + | "inf" { out "INF" ; INF } + | "intersect" { out "INTER" ; INTER } + | "inverse" { out "INV" ; INV } + | "istrue" { out "IST" ; IST } + | "isfalse" { out "ISF" ; ISF } + | "keep" { out "KEEP" ; KEEP } + | "le" { out "LE" ; LE } + | "let" { out "LET" ; LET } + | "log" { out "LOG" ; LOG } + | "lt" { out "LT" ; LT } + | "main" { out "MAIN" ; MAIN } + | "match" { out "MATCH" ; MATCH } + | "meet" { out "MEET" ; MEET } + | "not" { out "NOT" ; NOT } + | "of" { out "OF" ; OF } + | "or" { out "OR" ; OR } + | "pattern" { out "PAT" ; PAT } + | "proj" { out "PROJ" ; PROJ } + | "property" { out "PROP" ; PROP } + | "select" { out "SELECT"; SELECT } + | "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 } + | "true" { out "TRUE" ; TRUE } + | "union" { out "UNION" ; UNION } + | "where" { out "WHERE" ; WHERE } + | "xor" { out "XOR" ; XOR } + | IDEN { let id = Lexing.lexeme lexbuf in + out ("ID " ^ id); ID id } + | eof { out "EOF" ; EOF } +and result_token = parse + | SPC { result_token lexbuf } + | "(*" { comm_token lexbuf; result_token lexbuf } + | '"' { STR (qstr string_token lexbuf) } + | '/' { out "SL"; SL } + | '{' { LC } + | '}' { RC } + | ',' { CM } + | ';' { SC } + | '=' { IS } + | "attr" { ATTR } + | eof { EOF } diff --git a/helm/mathql/mathql_interpreter/mQueryTParser.mly b/helm/mathql/mathql_interpreter/mQueryTParser.mly new file mode 100644 index 000000000..2f8896185 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQueryTParser.mly @@ -0,0 +1,314 @@ +/* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + */ + +/* AUTOR: Ferruccio Guidi + */ + +%{ + module M = MathQL + + let analyze x = + let rec join l1 l2 = match l1, l2 with + | [], _ -> l2 + | _, [] -> l1 + | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 + | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 + | s1 :: tl1, s2 :: tl2 -> s1 :: join tl1 tl2 + in + let rec iter f = function + | [] -> [] + | 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] + | M.For (_,_,x,y) -> iter an_set [x; y] + | 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 + and an_con c = iter fc c + and fg (_, v) = an_val v + and an_grp = function + | M.Attr g -> iter (iter fg) g + | M.From _ -> [] + in + an_val x + + let f (x, y, z) = x + let s (x, y, z) = y + let t (x, y, z) = z +%} + %token ID STR + %token SL IS LC RC CM SC LP RP AT PC DL 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 + %left DIFF + %left UNION + %left INTER + %nonassoc WHERE EX + %left XOR OR + %left AND + %nonassoc NOT + %nonassoc SUB MEET EQ LT LE + %nonassoc SUBJ OF PROJ COUNT ALIGN + + %start qstr query result + %type qstr + %type query + %type result +%% + qstr: + | DQ { "" } + | STR qstr { $1 ^ $2 } + ; + svar: + | PC ID { $2 } + ; + avar: + | AT ID { $2 } + ; + vvar: + | DL ID { $2 } + ; + strs: + | STR CM strs { $1 :: $3 } + | STR { [$1] } + ; + subpath: + | STR SL subpath { $1 :: $3 } + | STR { [$1] } + ; + path: + | subpath { $1 } + | SL subpath { $2 } + | SL { [] } + ; + paths: + | path CM paths { $1 :: $3 } + | path { [$1] } + inv: + | INV { true } + | { false } + ; + ref: + | SUB { M.RefineSub } + | SUPER { M.RefineSuper } + | { M.RefineExact } + ; + qualif: + | inv ref path { $1, $2, $3 } + ; + cons: + | path IN val_exp { (false, $1, $3) } + | path MATCH val_exp { (true, $1, $3) } + ; + conss: + | cons CM conss { $1 :: $3 } + | cons { [$1] } + ; + istrue: + | IST conss { $2 } + | { [] } + ; + isfalse: + | { [] } + | ISF conss isfalse { $2 :: $3 } + ; + mainc: + | MAIN path { $2 } + | { [] } + ; + exp: + | path AS path { $1, Some $3 } + | path { $1, None } + ; + exps: + | exp CM exps { $1 :: $3 } + | exp { [$1] } + ; + attrc: + | ATTR exps { $2 } + | { [] } + ; + pattern: + | PAT { true } + | { false } + ; + opt_path: + | path { Some $1 } + | { None } + ; + ass: + | val_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 } + ; + 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 } + ; + 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 } + ; + xml: + | { false} + ; + 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) } + | 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 + { 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 } + ; + query: + | set_exp { $1 } + | set_exp error { $1 } + | EOF { raise End_of_file } + ; + attr: + | path IS strs { $1, $3 } + | path { $1, [] } + ; + attrs: + | attr SC attrs { $1 :: $3 } + | attr { [$1] } + ; + group: + LC attrs RC { $2 } + ; + groups: + | group CM groups { $1 :: $3 } + | group { [$1] } + ; + resource: + | STR ATTR groups { ($1, $3) } + | STR { ($1, []) } + ; + resources: + | resource SC resources { $1 :: $3 } + | resource { [$1] } + | { [] } + ; + result: + | resources { $1 } + | EOF { raise End_of_file } diff --git a/helm/mathql/mathql_interpreter/mQueryUtil.ml b/helm/mathql/mathql_interpreter/mQueryUtil.ml new file mode 100644 index 000000000..6323cc950 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQueryUtil.ml @@ -0,0 +1,220 @@ +(* 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 + *) + +(* $Id$ *) + +(* 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 sep x = + 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 sep x = + 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) + diff --git a/helm/mathql/mathql_interpreter/mQueryUtil.mli b/helm/mathql/mathql_interpreter/mQueryUtil.mli new file mode 100644 index 000000000..575400298 --- /dev/null +++ b/helm/mathql/mathql_interpreter/mQueryUtil.mli @@ -0,0 +1,49 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val text_of_query : (string -> unit) -> string -> MathQL.query -> unit + +val text_of_result : (string -> unit) -> string -> MathQL.result -> 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 diff --git a/helm/mathql_db_map.txt b/helm/mathql_db_map.txt deleted file mode 100644 index c58d843d2..000000000 --- a/helm/mathql_db_map.txt +++ /dev/null @@ -1,26 +0,0 @@ -objectName source <+ -objectName value <- objectName -refObj <- refObj -refObj source <- -refObj h_occurrence <- refObj h:occurrence -refObj h_position <- refObj h:position -refObj h_depth <- refObj h:depth -refRel <- refRel -refRel source <- -refRel h_position <- refRel h:position -refRel h_depth <- refRel h:depth -refSort <- refSort -refSort source <- -refSort h_sort <- refSort h:sort -refSort h_position <- refSort h:position -refSort h_depth <- refSort h:depth -backPointer <- backPointer -backPointer source <- backPointer h:occurrence -backPointer h_occurrence <- -backPointer h_position <- backPointer h:position -backPointer h_depth <- backPointer h:depth -no_inconcl_aux source <- -no_inconcl_aux no <- no_inconcl - -backPointer -> refObj - -> diff --git a/helm/ocaml/TODO b/helm/ocaml/TODO deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile deleted file mode 100644 index 17cafb431..000000000 --- a/helm/ocaml/mathql/Makefile +++ /dev/null @@ -1,13 +0,0 @@ -PACKAGE = mathql - -PREDICATES = - -INTERFACE_FILES = - -IMPLEMENTATION_FILES = mathQL.ml - -EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi - -EXTRA_OBJECTS_TO_CLEAN = - -include ../Makefile.common diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml deleted file mode 100644 index 2504cfb4f..000000000 --- a/helm/ocaml/mathql/mathQL.ml +++ /dev/null @@ -1,133 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://www.cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -(* output data structures ***************************************************) - -type path = string list (* the name of an attribute *) - -type value = string list (* the value of an attribute *) - -type attribute = path * value (* 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 - - -(* input data structures ****************************************************) - -type svar = string (* the name of a variable for a resource set *) - -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 - | RefineSub - | RefineSuper - -type main = path - -type pattern = bool - -type exp = path * (path option) - -type exp_list = exp list - -type allbut = bool - -type xml = bool - -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 - | AVar of avar - | Subj of msval - | 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 - | From of avar - -and con = pattern * path * msval - -and istrue = con list - -and isfalse = con list diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend deleted file mode 100644 index 0dc5572a0..000000000 --- a/helm/ocaml/mathql_generator/.depend +++ /dev/null @@ -1,15 +0,0 @@ -mQGUtil.cmi: mQGTypes.cmo -mQueryGenerator.cmi: mQGTypes.cmo -cGMatchConclusion.cmi: mQGTypes.cmo -cGSearchPattern.cmi: mQGTypes.cmo -cGLocateInductive.cmi: mQGTypes.cmo -mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi -mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi -mQueryGenerator.cmo: mQGUtil.cmi mQGTypes.cmo mQueryGenerator.cmi -mQueryGenerator.cmx: mQGUtil.cmx mQGTypes.cmx mQueryGenerator.cmi -cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi -cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi -cGSearchPattern.cmo: mQGUtil.cmi mQGTypes.cmo cGSearchPattern.cmi -cGSearchPattern.cmx: mQGUtil.cmx mQGTypes.cmx cGSearchPattern.cmi -cGLocateInductive.cmo: mQGTypes.cmo cGLocateInductive.cmi -cGLocateInductive.cmx: mQGTypes.cmx cGLocateInductive.cmi diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile deleted file mode 100644 index cf8e820d9..000000000 --- a/helm/ocaml/mathql_generator/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -PACKAGE = mathql_generator - -PREDICATES = - -INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ - cGMatchConclusion.mli cGSearchPattern.mli \ - cGLocateInductive.mli - -IMPLEMENTATION_FILES = mQGTypes.ml $(INTERFACE_FILES:%.mli=%.ml) - -EXTRA_OBJECTS_TO_INSTALL = mQGTypes.ml mQGTypes.cmi - -EXTRA_OBJECTS_TO_CLEAN = - -include ../Makefile.common diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml deleted file mode 100644 index 261b29388..000000000 --- a/helm/ocaml/mathql_generator/cGLocateInductive.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -exception NotAnInductiveDefinition - -let get_constraints = function - | Cic.MutInd (uri, t, _) -> - let uri = UriManager.string_of_uriref (uri, [t]) in - let constr_obj = - [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] - in - let constr_rel = [`MainConclusion None] in - let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in - (constr_obj, constr_rel, constr_sort) - | _ -> raise NotAnInductiveDefinition diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.mli b/helm/ocaml/mathql_generator/cGLocateInductive.mli deleted file mode 100644 index b6a51401e..000000000 --- a/helm/ocaml/mathql_generator/cGLocateInductive.mli +++ /dev/null @@ -1,31 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val get_constraints : Cic.term -> MQGTypes.must_restrictions - -exception NotAnInductiveDefinition diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml deleted file mode 100644 index 0a67c2d0d..000000000 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ /dev/null @@ -1,161 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -module T = MQGTypes - -let text_of_entries out entries = - out "(** MatchConclusion: results of the term inspection **)\n"; - let text_of_entry (u, b, v) = - out (string_of_int v ^ " "); - out (if b then "$MC " else "$IC "); - out (u ^ "\n") - in List.iter text_of_entry entries - -let sort_entries entries = - let comparator (_, _, v1) (_, _, v2) = compare v1 v2 in - List.fast_sort comparator entries - -let levels_of_term metasenv context term = - let module TC = CicTypeChecker in - let module Red = CicReduction in - let degree t = - let rec degree_aux = function - | Cic.Sort _ -> 1 - | Cic.Cast (u, _) -> degree_aux u - | Cic.Prod (_, _, t) -> degree_aux t - | _ -> 2 - in - let u,_ = TC.type_of_aux' metasenv context t CicUniv.empty_ugraph in - degree_aux (Red.whd context u) - in - let entry_eq (s1, b1, v1) (s2, b2, v2) = - s1 = s2 && b1 = b2 - in - let rec entry_in e = function - | [] -> [e] - | head :: tail -> - head :: if entry_eq head e then tail else entry_in e tail - in - let inspect_uri main l uri tc v term = - let d = degree term in - entry_in (UriManager.string_of_uriref (uri, tc), main, 2 * v + d - 1) l - in - let rec inspect_term main l v term = match term with - Cic.Rel _ -> l - | Cic.Meta _ -> l - | Cic.Sort _ -> l - | Cic.Implicit _ -> l - | Cic.Var (u,exp_named_subst) -> - inspect_exp_named_subst l (succ v) exp_named_subst -(* - let l' = inspect_uri main l u [] v term in - inspect_exp_named_subst l' (succ v) exp_named_subst -*) - | Cic.Const (u,exp_named_subst) -> - let l' = inspect_uri main l u [] v term in - inspect_exp_named_subst l' (succ v) exp_named_subst - | Cic.MutInd (u, t, exp_named_subst) -> - let l' = inspect_uri main l u [t] v term in - inspect_exp_named_subst l' (succ v) exp_named_subst - | Cic.MutConstruct (u, t, c, exp_named_subst) -> - let l' = inspect_uri main l u [t; c] v term in - inspect_exp_named_subst l' (succ v) exp_named_subst - | Cic.Cast (uu, _) -> - inspect_term main l v uu - | Cic.Prod (_, uu, tt) -> - let luu = inspect_term false l (succ v) uu in - inspect_term main luu (succ v) tt - | Cic.Lambda (_, uu, tt) -> - let luu = inspect_term false l (succ v) uu in - inspect_term false luu (succ v) tt - | Cic.LetIn (_, uu, tt) -> - let luu = inspect_term false l (succ v) uu in - inspect_term false luu (succ v) tt - | Cic.Appl m -> inspect_list main l true v m - | Cic.MutCase (u, t, tt, uu, m) -> - let lu = inspect_uri main l u [t] (succ v) term in - let ltt = inspect_term false lu (succ v) tt in - let luu = inspect_term false ltt (succ v) uu in - inspect_list main luu false (succ v) m - | Cic.Fix (_, m) -> inspect_ind l (succ v) m - | Cic.CoFix (_, m) -> inspect_coind l (succ v) m - and inspect_list main l head v = function - | [] -> l - | tt :: m -> - let ltt = inspect_term main l (if head then v else v + 1) tt in - inspect_list false ltt false v m - and inspect_exp_named_subst l v = function - [] -> l - | (_,t) :: tl -> - let l' = inspect_term false l v t in - inspect_exp_named_subst l' v tl - and inspect_ind l v = function - | [] -> l - | (_, _, tt, uu) :: m -> - let ltt = inspect_term false l v tt in - let luu = inspect_term false ltt v uu in - inspect_ind luu v m - and inspect_coind l v = function - | [] -> l - | (_, tt, uu) :: m -> - let ltt = inspect_term false l v tt in - let luu = inspect_term false ltt v uu in - inspect_coind luu v m - in - let rec inspect_backbone = function - | Cic.Cast (uu, _) -> inspect_backbone uu - | Cic.Prod (_, _, tt) -> inspect_backbone tt - | Cic.LetIn (_, uu, tt) -> inspect_backbone tt - | t -> inspect_term true [] 0 t - in - inspect_backbone term - -let get_constraints e c t = - let can = sort_entries (levels_of_term e c t) in (* can restrictions *) - text_of_entries prerr_string can; flush stderr; (* logging *) - let rest_of (u, b, _) = - let p = if b then `MainConclusion None else `InConclusion in (p, u) - in - let rec split vp = function - | [], ((_, _, v) as hd) :: tl -> split v ([rest_of hd], tl) - | prev, ((_, _, ve) as hd) :: tl when vp = ve -> - split vp (rest_of hd :: prev, tl) - | p, l -> p, l - in - let rec mk_musts prev acc = function - | [] -> prev, acc - | l -> - let slice, next = split 0 ([], l) in - let acc = acc @ slice in - mk_musts (prev @ [acc]) acc next - in - mk_musts [] [] can - -let universe = [T.MainConclusion; T.InConclusion] diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.mli b/helm/ocaml/mathql_generator/cGMatchConclusion.mli deleted file mode 100644 index a9fbef47f..000000000 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val get_constraints: Cic.metasenv -> Cic.context -> Cic.term -> - MQGTypes.r_obj list list * - MQGTypes.r_obj list - -val universe : MQGTypes.universe diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml deleted file mode 100644 index 1d7e85937..000000000 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ /dev/null @@ -1,197 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 02/12/2002 *) -(* *) -(* Missing description *) -(* *) -(******************************************************************************) - -(* $Id$ *) - -module T = MQGTypes -module U = MQGUtil - -type classification = - Backbone of int - | Branch of int - | InConclusion - | InHypothesis -;; - -let soften_classification = - function - Backbone _ -> InConclusion - | Branch _ -> InHypothesis - | k -> k -;; - -let (!!) = - function - Backbone n -> `MainConclusion (Some n) - | Branch n -> `MainHypothesis (Some n) - | _ -> assert false -;; - -let (!!!) = - function - Backbone n -> `MainConclusion (Some n) - | Branch n -> `MainHypothesis (Some n) - | InConclusion -> `InConclusion - | InHypothesis -> `InHypothesis -;; - - -let (@@) (l1,l2,l3) (l1',l2',l3') = - let merge l1 l2 = - List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1 - in - merge l1 l1', merge l2 l2', merge l3 l3' -;; - -let get_constraints term = - let module U = UriManager in - let module C = Cic in - let rec process_type_aux kind = - function - C.Var (uri,expl_named_subst) -> - (* andrea: this is a bug: variable are not indexedin the db - ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ *) - (process_type_aux_expl_named_subst kind expl_named_subst) - | C.Rel _ -> - (match kind with - | InConclusion - | InHypothesis -> [],[],[] - | _ -> [],[!!kind],[]) - | C.Sort s -> - (match kind with - Backbone _ - | Branch _ -> - let s' = - match s with - Cic.Prop -> T.Prop - | Cic.Set -> T.Set - | Cic.Type _ -> T.Type (* TASSI: ?? *) - | Cic.CProp -> T.CProp - in - [],[],[!!kind,s'] - | _ -> [],[],[]) - | C.Meta _ -> [],[],[] (* ???? To be understood *) - | C.Implicit _ -> assert false - | C.Cast (te,_) -> - (* type ignored *) - process_type_aux kind te - | C.Prod (_,sou,ta) -> - let (source_kind,target_kind) = - match kind with - Backbone n -> (Branch 0, Backbone (n+1)) - | Branch n -> (InHypothesis, Branch (n+1)) - | k -> (k,k) - in - process_type_aux source_kind sou @@ - process_type_aux target_kind ta - | C.Lambda (_,sou,ta) -> - let kind' = soften_classification kind in - process_type_aux kind' sou @@ - process_type_aux kind' ta - | C.LetIn (_,te,ta)-> - let kind' = soften_classification kind in - process_type_aux kind' te @@ - process_type_aux kind ta - | C.Appl (he::tl) -> - let kind' = soften_classification kind in - process_type_aux kind he @@ - List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl - | C.Appl _ -> assert false - | C.Const (uri,_) -> - [!!!kind, UriManager.string_of_uri uri],[],[] - | C.MutInd (uri,typeno,expl_named_subst) -> - ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ ")"],[],[]) @@ - (process_type_aux_expl_named_subst kind expl_named_subst) - | C.MutConstruct (uri,typeno,consno,expl_named_subst) -> - ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[]) - @@ (process_type_aux_expl_named_subst kind expl_named_subst) - | C.MutCase (_,_,_,term,patterns) -> - (* outtype ignored *) - let kind' = soften_classification kind in - process_type_aux kind' term @@ - List.fold_left (fun i t -> i @@ process_type_aux kind' t) - ([],[],[]) patterns - | C.Fix (_,funs) -> - let kind' = soften_classification kind in - List.fold_left - (fun i (_,_,bo,ty) -> - i @@ - process_type_aux kind' bo @@ - process_type_aux kind' ty - ) ([],[],[]) funs - | C.CoFix (_,funs) -> - let kind' = soften_classification kind in - List.fold_left - (fun i (_,bo,ty) -> - i @@ - process_type_aux kind' bo @@ - process_type_aux kind' ty - ) ([],[],[]) funs - and process_type_aux_expl_named_subst kind = - List.fold_left - (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t)) - ([],[],[]) -in - let obj_constraints,rel_constraints,sort_constraints = - process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term) - in - (obj_constraints,rel_constraints,sort_constraints) -;; - -(*CSC: Debugging only *) -(* -let get_constraints term = - let res = get_constraints term in - let (objs,rels,sorts) = res in - let text_of_pos p = - U.text_of_position p ^ " " ^ U.text_of_depth p "NULL" - in - prerr_endline "Constraints on objs:" ; - List.iter - (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ; - prerr_endline "Constraints on Rels:" ; - List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ; - prerr_endline "Constraints on Sorts:" ; - List.iter - (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s) - ) sorts ; - res -;; *) - -let universe = - [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion] diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.mli b/helm/ocaml/mathql_generator/cGSearchPattern.mli deleted file mode 100644 index 528283387..000000000 --- a/helm/ocaml/mathql_generator/cGSearchPattern.mli +++ /dev/null @@ -1,39 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 02/12/2002 *) -(* *) -(* Missing description *) -(* *) -(******************************************************************************) - -val get_constraints : Cic.term -> MQGTypes.must_restrictions - -val universe : MQGTypes.universe diff --git a/helm/ocaml/mathql_generator/mQGTypes.ml b/helm/ocaml/mathql_generator/mQGTypes.ml deleted file mode 100644 index 9ed2ce253..000000000 --- a/helm/ocaml/mathql_generator/mQGTypes.ml +++ /dev/null @@ -1,77 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTORS: Ferruccio Guidi - * Claudio Sacerdoti Coen - *) - -(* $Id$ *) - -(* low level types *********************************************************) - -type uri = string -type position = MainHypothesis - | InHypothesis - | MainConclusion - | InConclusion - | InBody -type depth = int -type sort = Set - | Prop - | Type - | CProp - -type spec = MustObj of uri list * position list * depth list - | MustSort of sort list * position list * depth list - | MustRel of position list * depth list - | OnlyObj of uri list * position list * depth list - | OnlySort of sort list * position list * depth list - | OnlyRel of position list * depth list - | Universe of position list - -(* high-level types ********************************************************) - -type optional_depth = int option - -type full_position = [ `MainHypothesis of optional_depth - | `MainConclusion of optional_depth - | `InHypothesis - | `InConclusion - | `InBody - ] - -type main_position = [ `MainHypothesis of optional_depth - | `MainConclusion of optional_depth - ] - -type r_obj = full_position * uri -type r_sort = main_position * sort -type r_rel = main_position - -type must_restrictions = (r_obj list * r_rel list * r_sort list) -type only_restrictions = - (r_obj list option * r_rel list option * r_sort list option) - -type universe = position list diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml deleted file mode 100644 index 7603ab9a6..000000000 --- a/helm/ocaml/mathql_generator/mQGUtil.ml +++ /dev/null @@ -1,150 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -module T = MQGTypes - -(* low level functions *****************************************************) - -let string_of_position p = - let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in - match p with - | T.MainHypothesis -> ns ^ "MainHypothesis" - | T.InHypothesis -> ns ^ "InHypothesis" - | T.MainConclusion -> ns ^ "MainConclusion" - | T.InConclusion -> ns ^ "InConclusion" - | T.InBody -> ns ^ "InBody" - -let string_of_sort = function - | T.Set -> "Set" - | T.Prop -> "Prop" - | T.Type -> "Type" - | T.CProp -> "CProp" - -let string_of_depth = string_of_int - -let mathql_of_position = function - | T.MainHypothesis -> "$MH" - | T.InHypothesis -> "$IH" - | T.MainConclusion -> "$MC" - | T.InConclusion -> "$IC" - | T.InBody -> "$IB" - -let mathql_of_sort = function - | T.Set -> "$SET" - | T.Prop -> "$PROP" - | T.Type -> "$TYPE" - | T.CProp -> "$CPROP" - -let mathql_of_depth = string_of_int - -let mathql_of_uri u = u - -let mathql_of_specs out l = - let rec iter f = function - | [] -> () - | [s] -> out "\""; out (f s); out "\"" - | s :: tail -> out "\""; out (f s); out "\", "; iter f tail - in - let txt_uri l = out "{"; iter mathql_of_uri l; out "} " in - let txt_pos l = out "{"; iter mathql_of_position l; out "} " in - let txt_sort l = out "{"; iter mathql_of_sort l; out "} " in - let txt_depth l = out "{"; iter mathql_of_depth l; out "} " in - let txt_spec = function - | T.MustObj (u, p, d) -> out "mustobj "; txt_uri u; txt_pos p; txt_depth d; out "\n" - | T.MustSort (s, p, d) -> out "mustsort "; txt_sort s; txt_pos p; txt_depth d; out "\n" - | T.MustRel ( p, d) -> out "mustrel "; txt_pos p; txt_depth d; out "\n" - | T.OnlyObj (u, p, d) -> out "onlyobj "; txt_uri u; txt_pos p; txt_depth d; out "\n" - | T.OnlySort (s, p, d) -> out "onlysort "; txt_sort s; txt_pos p; txt_depth d; out "\n" - | T.OnlyRel ( p, d) -> out "onlyrel "; txt_pos p; txt_depth d; out "\n" - | T.Universe ( p ) -> out "universe "; txt_pos p; out "\n" - in - List.iter txt_spec l - -let position_of_mathql = function - | "$MH" -> T.MainHypothesis - | "$IH" -> T.InHypothesis - | "$MC" -> T.MainConclusion - | "$IC" -> T.InConclusion - | "$IB" -> T.InBody - | _ -> raise Parsing.Parse_error - -let sort_of_mathql = function - | "$SET" -> T.Set - | "$PROP" -> T.Prop - | "$TYPE" -> T.Type - | "$CPROP" -> T.CProp - | _ -> raise Parsing.Parse_error - -let depth_of_mathql s = - try - let d = int_of_string s in - if d < 0 then raise (Failure "") else d - with Failure _ -> raise Parsing.Parse_error - -let uri_of_mathql s = s - -(* high level functions ****************************************************) - -let text_of_position = function - | `MainHypothesis _ -> "MainHypothesis" - | `MainConclusion _ -> "MainConclusion" - | `InHypothesis -> "InHypothesis" - | `InConclusion -> "InConclusion" - | `InBody -> "InBody" - -let text_of_depth pos no_depth_text = match pos with - | `MainHypothesis (Some d) - | `MainConclusion (Some d) -> string_of_int d - | _ -> no_depth_text - -let text_of_sort = function - | T.Set -> "Set" - | T.Prop -> "Prop" - | T.Type -> "Type" - | T.CProp -> "CProp" - -let is_main_position = function - | `MainHypothesis _ - | `MainConclusion _ -> true - | _ -> false - -let is_conclusion = function - | `MainConclusion _ - | `InConclusion -> true - | _ -> false - -let set_full_position pos depth = match pos with - | `MainHypothesis _ -> `MainHypothesis depth - | `MainConclusion _ -> `MainConclusion depth - | _ -> pos - -let set_main_position pos depth = match pos with - | `MainHypothesis _ -> `MainHypothesis depth - | `MainConclusion _ -> `MainConclusion depth diff --git a/helm/ocaml/mathql_generator/mQGUtil.mli b/helm/ocaml/mathql_generator/mQGUtil.mli deleted file mode 100644 index 065abb157..000000000 --- a/helm/ocaml/mathql_generator/mQGUtil.mli +++ /dev/null @@ -1,69 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* low level functions *****************************************************) - -(* these functions give the string representation used in the db ----------*) - -val string_of_position : MQGTypes.position -> string -val string_of_depth : MQGTypes.depth -> string -val string_of_sort : MQGTypes.sort -> string - -(* these functions give the string representation used in MathQL ----------*) - -val mathql_of_position : MQGTypes.position -> string -val mathql_of_depth : MQGTypes.depth -> string -val mathql_of_uri : MQGTypes.uri -> string -val mathql_of_sort : MQGTypes.sort -> string - -val mathql_of_specs : (string -> unit) -> MQGTypes.spec list -> unit - -val position_of_mathql : string -> MQGTypes.position -val depth_of_mathql : string -> MQGTypes.depth -val uri_of_mathql : string -> MQGTypes.uri -val sort_of_mathql : string -> MQGTypes.sort - -(* high level functions ****************************************************) - -(* these functions give the textual representation used by umans ----------*) - -val text_of_position : MQGTypes.full_position -> string -val text_of_depth : MQGTypes.full_position -> string -> string -val text_of_sort : MQGTypes.sort -> string - -(* these functions classify the positions ---------------------------------*) - -val is_main_position : MQGTypes.full_position -> bool -val is_conclusion : MQGTypes.full_position -> bool - -(* these function apply changes to positions ------------------------------*) - -val set_full_position : MQGTypes.full_position -> MQGTypes.optional_depth -> - MQGTypes.full_position -val set_main_position : MQGTypes.main_position -> MQGTypes.optional_depth -> - MQGTypes.main_position diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml deleted file mode 100644 index 784bc11dc..000000000 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ /dev/null @@ -1,191 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -module M = MathQL -module T = MQGTypes -module U = MQGUtil - -(* low level functions *****************************************************) - -let locate s = - let query = - M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) ) - in query - -let unreferred target_pattern source_pattern = - let query = - M.Bin (M.BinFDiff, - ( - M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const target_pattern)) - ), ( - M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern)) - - )) - in query - -let compose cl = - let letin = ref [] in - let must = ref [] in - let onlyobj = ref [] in - let onlysort = ref [] in - let onlyrel = ref [] in - let only = ref true in - let univ = ref [] in - let set_val = function - | [s] -> M.Const s - | l -> - let msval = M.Set (List.map (fun s -> M.Const s) l) in - if ! only then begin - let vvar = "val" ^ string_of_int (List.length ! letin) in - letin := (vvar, msval) :: ! letin; - M.VVar vvar - end else msval - in - let cons o (r, s, p, d) = - let con p = function - | [] -> [] - | l -> [(false, [p], set_val l)] - in - only := o; - con "h:occurrence" r @ - con "h:sort" (List.map U.string_of_sort s) @ - con "h:position" (List.map U.string_of_position p) @ - 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,(M.Const "")) - in - let property_only n cl = - let rec build = function - | [] -> [] - | c :: tl -> - let r = (cons true) c in - if r = [] then build tl else r :: build tl - in - let cll = build cl in - M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) - in - let rec aux = function - | [] -> () - | T.Universe l :: tail -> - 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 -> - must := property_must "refObj" (r, [], p, d) :: ! must; aux tail - | T.MustSort(s,p,d) :: tail -> - must := property_must "refSort" ([], s, p, d) :: ! must; aux tail - | T.MustRel(p,d) :: tail -> - must := property_must "refRel" ([], [], p, d) :: ! must; aux tail - | T.OnlyObj(r,p,d) :: tail -> - onlyobj := (r, [], p, d) :: ! onlyobj; aux tail - | T.OnlySort(s,p,d) :: tail -> - onlysort := ([], s, p, d) :: ! onlysort; aux tail - | T.OnlyRel(p,d) :: tail -> - onlyrel := ([], [], p, d) :: ! onlyrel; aux tail - in - let rec iter f g = function - | [] -> raise (Failure "MQueryGenerator.iter") - | [head] -> (f head) - | head :: tail -> let t = (iter f g tail) in g (f head) t - in - (* prerr_endline "(** Compose: received constraints **)"; - U.mathql_of_specs prerr_string cl; flush stderr; *) - aux cl; - let must_query = - if ! must = [] then - M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*")) - else - iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must - in - let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in - let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in - let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in - let select_query x = - match ! onlyobj, ! onlysort, ! onlyrel with - | [], [], [] -> x - | _, [], [] -> M.Select("obj",x,onlyobj_val) - | [], _, [] -> M.Select("obj",x,onlysort_val) - | [], [], _ -> M.Select("obj",x,onlyrel_val) - | _, _, [] -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val))) - | _, [], _ -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val))) - | [], _, _ -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val))) - | _, _, _ -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val))) - in - let letin_query = - if ! letin = [] then fun x -> x - else - let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in - iter f (fun x y z -> x (y z)) ! letin - in - letin_query (select_query must_query) - -(* high-level functions ****************************************************) - -let query_of_constraints u (musts_obj, musts_rel, musts_sort) - (onlys_obj, onlys_rel, onlys_sort) = - let conv = function - | `MainHypothesis None -> [T.MainHypothesis], [] - | `MainHypothesis (Some d) -> [T.MainHypothesis], [d] - | `MainConclusion None -> [T.MainConclusion], [] - | `MainConclusion (Some d) -> [T.MainConclusion], [d] - | `InHypothesis -> [T.InHypothesis], [] - | `InConclusion -> [T.InConclusion], [] - | `InBody -> [T.InBody], [] - in - let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in - let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in - let must_rel p = let p, d = conv p in T.MustRel (p, d) in - let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in - let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in - let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in - let must = List.map must_obj musts_obj @ - List.map must_rel musts_rel @ - List.map must_sort musts_sort - in - let only = - (match onlys_obj with - | None -> [] - | Some [] -> [T.OnlyObj ([], [], [])] - | Some l -> List.map only_obj l - ) @ - (match onlys_rel with - | None -> [] - | Some [] -> [T.OnlyRel ([], [])] - | Some l -> List.map only_rel l - ) @ - (match onlys_sort with - | None -> [] - | Some [] -> [T.OnlySort ([], [], [])] - | Some l -> List.map only_sort l - ) - in - let univ = match u with None -> [] | Some l -> [T.Universe l] in - compose (must @ only @ univ) diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli deleted file mode 100644 index decaa0ea7..000000000 --- a/helm/ocaml/mathql_generator/mQueryGenerator.mli +++ /dev/null @@ -1,42 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* interface for the low-level constraints *********************************) - -val locate : string -> MathQL.query - -val unreferred : string -> string -> MathQL.query - -val compose : MQGTypes.spec list -> MathQL.query - -(* interface for the high-level constraints ********************************) - -val query_of_constraints : MQGTypes.universe option -> - MQGTypes.must_restrictions -> - MQGTypes.only_restrictions -> - MathQL.query diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend deleted file mode 100644 index 186c81793..000000000 --- a/helm/ocaml/mathql_interpreter/.depend +++ /dev/null @@ -1,27 +0,0 @@ -mQIPostgres.cmi: mQITypes.cmo -mQIMySql.cmi: mQITypes.cmo -mQIConn.cmi: mQITypes.cmo mQIMap.cmi -mQIProperty.cmi: mQITypes.cmo mQIConn.cmi -mQueryInterpreter.cmi: mQIConn.cmi -mQueryTParser.cmo: mQueryTParser.cmi -mQueryTParser.cmx: mQueryTParser.cmi -mQueryTLexer.cmo: mQueryTParser.cmi -mQueryTLexer.cmx: mQueryTParser.cmx -mQueryUtil.cmo: mQueryTParser.cmi mQueryTLexer.cmo mQueryUtil.cmi -mQueryUtil.cmx: mQueryTParser.cmx mQueryTLexer.cmx mQueryUtil.cmi -mQIUtil.cmo: mQIUtil.cmi -mQIUtil.cmx: mQIUtil.cmi -mQIPostgres.cmo: mQIPostgres.cmi -mQIPostgres.cmx: mQIPostgres.cmi -mQIMySql.cmo: mQIMySql.cmi -mQIMySql.cmx: mQIMySql.cmi -mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi -mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi -mQIConn.cmo: mQIPostgres.cmi mQIMySql.cmi mQIMap.cmi mQIConn.cmi -mQIConn.cmx: mQIPostgres.cmx mQIMySql.cmx mQIMap.cmx mQIConn.cmi -mQIProperty.cmo: mQIUtil.cmi mQIMap.cmi mQIConn.cmi mQIProperty.cmi -mQIProperty.cmx: mQIUtil.cmx mQIMap.cmx mQIConn.cmx mQIProperty.cmi -mQueryInterpreter.cmo: mQueryUtil.cmi mQIUtil.cmi mQIProperty.cmi mQIConn.cmi \ - mQueryInterpreter.cmi -mQueryInterpreter.cmx: mQueryUtil.cmx mQIUtil.cmx mQIProperty.cmx mQIConn.cmx \ - mQueryInterpreter.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile deleted file mode 100644 index bdd738135..000000000 --- a/helm/ocaml/mathql_interpreter/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -PACKAGE = mathql_interpreter - -PREDICATES = - -INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \ - mQIPostgres.mli mQIMySql.mli mQIMap.mli mQIConn.mli \ - mQIProperty.mli mQueryInterpreter.mli - -IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \ - mQITypes.ml $(INTERFACE_FILES:%.mli=%.ml) - -EXTRA_OBJECTS_TO_INSTALL = mQueryTLexer.cmi \ - mQueryTLexer.mll mQueryTParser.mly \ - mQITypes.ml mQITypes.cmi - -EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ - mQueryTLexer.ml - -include ../Makefile.common diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml deleted file mode 100644 index 270d1f9d0..000000000 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ /dev/null @@ -1,130 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -type connection = MySQL_C of HMysql.dbd - | Postgres_C of Postgres.connection - | No_C - -type flag = Galax | Postgres | Queries | Result | Source | Times | Warn - -type handle = { - log : string -> unit; (* logging function *) - set : flag list; (* options *) - pgc : connection; (* PG connection *) - pgm : MQIMap.pg_map; (* PG conversion function *) - pga : MQIMap.pg_alias (* PG table aliases *) -} - -let tables handle p = MQIMap.get_tables handle.pgm p - -let field handle p t = MQIMap.get_field handle.pgm p t - -let resolve handle a = MQIMap.resolve handle.pga a - -let log handle = handle.log - -let set handle flag = List.mem flag handle.set - -let pgc handle = handle.pgc - -let flags handle = handle.set - -let string_of_flag = function - | Galax -> "G" - | Postgres -> "P" - | Queries -> "Q" - | Result -> "R" - | Source -> "S" - | Times -> "T" - | Warn -> "W" - -let flag_of_char = function - | 'G' -> [Galax] - | 'P' -> [Postgres] - | 'Q' -> [Queries] - | 'R' -> [Result] - | 'S' -> [Source] - | 'T' -> [Times] - | 'W' -> [Warn] - | _ -> [] - -let string_fold_left f a s = - let l = String.length s in - let rec aux b i = if i = l then b else aux (f b s.[i]) (succ i) in - aux a 0 - -let string_of_flags flags = - List.fold_left (fun s flag -> s ^ string_of_flag flag) "" flags - -let flags_of_string s = - string_fold_left (fun l c -> l @ flag_of_char c) [] s - -let init ?(flags = []) ?(log = ignore) () = - let flags = - if flags = [] then - flags_of_string (Helm_registry.get "mathql_interpreter.flags") - else - flags - in - let m, a = - let g = - if List.mem Galax flags - then MQIMap.empty_map else MQIMap.read_map - in g () - in - {log = log; set = flags; - pgc = begin - try - if List.mem Galax flags then No_C else - if List.mem Postgres flags then Postgres_C (MQIPostgres.init ()) else - MySQL_C (MQIMySql.init ()) - with Failure "mqi_connection" -> No_C - end; - pgm = m; pga = a - } - -let close handle = - match pgc handle with - | MySQL_C c -> MQIMySql.close c - | Postgres_C c -> MQIPostgres.close c - | No_C -> () - -let exec handle out table cols ct cfl = - match pgc handle with - | MySQL_C c -> MQIMySql.exec (c, out) table cols ct cfl - | Postgres_C c -> MQIPostgres.exec (c, out) table cols ct cfl - | No_C -> [] - -let connected handle = - pgc handle <> No_C - -let init_if_connected ?(flags = []) ?(log = ignore) () = - let handle = init ~flags:flags ~log:log () in - if connected handle then handle else raise (Failure "mqi connection failed") diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli deleted file mode 100644 index 35c8b3ef0..000000000 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ /dev/null @@ -1,65 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -type connection = MySQL_C of HMysql.dbd - | Postgres_C of Postgres.connection - | No_C - -type flag = Galax | Postgres | Queries | Result | Source | Times | Warn - -type handle = { - log : string -> unit; (* logging function *) - set : flag list; (* options *) - pgc : connection; (* PG connection *) - pgm : MQIMap.pg_map; (* PG conversion function *) - pga : MQIMap.pg_alias (* PG table aliases *) -} - -val string_of_flags : flag list -> string -val flags_of_string : string -> flag list - -val init : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> handle -val close : handle -> unit -val connected : handle -> bool -val exec : handle -> (MQITypes.query -> unit) -> - MQITypes.table -> MQITypes.columns -> - string MQITypes.con_true -> string MQITypes.con_false -> - MQITypes.result - -val init_if_connected : ?flags:(flag list) -> ?log:(string -> unit) -> unit -> handle - -(* The following functions allow to read the handle internal fields. - * For exclusive use of the interpreter. - *) - -val log : handle -> string -> unit -val set : handle -> flag -> bool -val flags : handle -> flag list -val tables : handle -> MathQL.path -> MQIMap.pg_tables -val field : handle -> MathQL.path -> string -> string -val resolve : handle -> string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIMap.ml b/helm/ocaml/mathql_interpreter/mQIMap.ml deleted file mode 100644 index a5b6654c8..000000000 --- a/helm/ocaml/mathql_interpreter/mQIMap.ml +++ /dev/null @@ -1,93 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -module U = MQueryUtil - -type pg_map = (MathQL.path * (bool * string * string option)) list - -type pg_tables = (bool * string) list - -type pg_alias = (string * string) list - -let empty_map () = [], [] - -let read_map () = - let map = Helm_registry.get "mathql_interpreter.db_map" in - let ich = open_in map in - let rec aux r s = - let d = input_line ich in - match Str.split (Str.regexp "[ \t]+") d with - | [] -> aux r s - | "#" :: _ -> aux r s - | t :: "<-" :: p -> aux ((p, (false, t, None)) :: r) s - | t :: c :: "<-" :: p -> aux ((p, (false, t, Some c)) :: r) s - | t :: "<+" :: p -> aux ((p, (true, t, None)) :: r) s - | t :: c :: "<+" :: p -> aux ((p, (true, t, Some c)) :: r) s - | [a; "->"; t] -> aux r ((a, t) :: s) - | ["->"] -> r, s - | _ -> raise (Failure "MQIMap.read_map") - in - let pgm, pga = aux [] [] in - close_in ich; - pgm, pga - -let comp c1 c2 = match c1, c2 with - | (_, t1), (_, t2) when t1 < t2 -> U.Lt - | (_, t1), (_, t2) when t1 > t2 -> U.Gt - | (b1, t), (b2, _) -> U.Eq (b1 || b2, t) - -let get_tables pgm p = - let aux l = function - | q, (b, t, _) when q = p -> U.list_join comp l [(b, t)] - | _, _ -> l - in - List.fold_left aux [] pgm - -let rec refine_tables l1 l2 = - U.list_meet comp l1 l2 - -let default_table = function - | [(_, a)] -> a - | l -> - try List.assoc true l - with Not_found -> raise (Failure "MQIMap.default_table") - -let get_field pgm p t = - let aux = function - | q, (_, u, _) when q = p && u = t -> true - | _ -> false - in - match List.filter aux pgm with - | [_, (_, _, None)] -> "" - | [_, (_, _, Some c)] -> c - | _ -> raise (Failure "MQIMap.get_field") - -let resolve pga a = - try List.assoc a pga with Not_found -> a diff --git a/helm/ocaml/mathql_interpreter/mQIMap.mli b/helm/ocaml/mathql_interpreter/mQIMap.mli deleted file mode 100644 index 50f5bb0fa..000000000 --- a/helm/ocaml/mathql_interpreter/mQIMap.mli +++ /dev/null @@ -1,47 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -type pg_map (* mathql path map for postgres *) - -type pg_tables - -type pg_alias - -val empty_map : unit -> pg_map * pg_alias - -val read_map : unit -> pg_map * pg_alias - -val get_tables : pg_map -> MathQL.path -> pg_tables - -val refine_tables : pg_tables -> pg_tables -> pg_tables - -val default_table : pg_tables -> string - -val get_field : pg_map -> MathQL.path -> string -> string - -val resolve : pg_alias -> string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.ml b/helm/ocaml/mathql_interpreter/mQIMySql.ml deleted file mode 100644 index 3380e1f1f..000000000 --- a/helm/ocaml/mathql_interpreter/mQIMySql.ml +++ /dev/null @@ -1,96 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -let init () = - let module HR = Helm_registry in - let host = - HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.host" in - let database = - HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.database" in - let user = - HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.user" in - let port = - HR.get_opt HR.get_int "mathql_interpreter.mysql_connection.port" in - let password = - HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.password" in - try HMysql.quick_connect ?host ?database ?user ?port ?password () - with _ -> raise (Failure "mqi_connecion") - -let close c = HMysql.disconnect c - -let quote s = - let rec quote_aux s = - try - let l = String.length s in - let i = String.index s '\'' in - String.sub s 0 i ^ "\\'" ^ quote_aux (String.sub s (succ i) (l - (succ i))) - with Not_found -> s - in - "'" ^ quote_aux s ^ "'" - -let exec (c, out) q = - let g = function None -> "" | Some v -> v in - let f a = List.map g (Array.to_list a) in - out q; HMysql.map ~f:f (Mysql.exec c q) - -let exec c table cols ct cfl = - let rec iter f last sep = function - | [] -> last - | [head] -> f head - | head :: tail -> f head ^ sep ^ iter f last sep tail - in - let pg_cols = iter (fun x -> x) "" ", " cols in - let pg_msval v = iter quote "" ", " v in - let pg_con (pat, col, v) = - if col <> "" then - let f s = col ^ " regexp " ^ quote ("^" ^ s ^ "$") in - if pat then "(" ^ iter f "0" " or " v ^ ")" - else match v with - | [s] -> col ^ " = " ^ (quote s) - | v -> col ^ " in (" ^ pg_msval v ^ ")" - else "1" - in - let pg_cons l = iter pg_con "1" " and " l in - let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in - let pg_cons_not_l ll = iter pg_cons_not "1" " and " ll in - let pg_where = match ct, cfl with - | [], [] -> "" - | lt, [] -> " where " ^ pg_cons lt - | [], llf -> " where " ^ pg_cons_not_l llf - | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf - in - if cols = [] then - let r = exec c ("select count(source) from " ^ table ^ pg_where) in - match r with - | [[s]] when int_of_string s > 0 -> [[]] - | _ -> [] - else - exec c ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ - " order by " ^ List.hd cols ^ " asc") diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.mli b/helm/ocaml/mathql_interpreter/mQIMySql.mli deleted file mode 100644 index 8afaf401d..000000000 --- a/helm/ocaml/mathql_interpreter/mQIMySql.mli +++ /dev/null @@ -1,36 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val init : unit -> HMysql.dbd - -val close : HMysql.dbd -> unit - -val exec : HMysql.dbd * (MQITypes.query -> unit) -> - MQITypes.table -> MQITypes.columns -> - string MQITypes.con_true -> string MQITypes.con_false -> - MQITypes.result diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml deleted file mode 100644 index bef07230f..000000000 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.ml +++ /dev/null @@ -1,96 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -let init () = - let connection_string = - Helm_registry.get "mathql_interpreter.postgresql_connection_string" - in - try new Postgres.connection connection_string - with _ -> raise (Failure "mqi_connecion") - -let close c = c#close - -let quote s = - let rec quote_aux s = - try - let l = String.length s in - let i = String.index s '\'' in - String.sub s 0 i ^ "\\'" ^ quote_aux (String.sub s (succ i) (l - (succ i))) - with Not_found -> s - in - "'" ^ quote_aux s ^ "'" - -let exec (c, out) q = out q; (c#exec q)#get_list - -let exec c table cols ct cfl = - let rec iter f last sep = function - | [] -> last - | [head] -> f head - | head :: tail -> f head ^ sep ^ iter f last sep tail - in - let pg_cols = iter (fun x -> x) "" ", " cols in - let pg_msval v = iter quote "" ", " v in - let pg_con (pat, col, v) = - if col <> "" then - let f s = col ^ " ~ " ^ quote ("^" ^ s ^ "$") in - if pat then "(" ^ iter f "false" " or " v ^ ")" - else match v with - | [s] -> col ^ " = " ^ (quote s) - | v -> col ^ " in (" ^ pg_msval v ^ ")" - else "true" - in - let pg_cons l = iter pg_con "true" " and " l in - let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in - let pg_cons_not_l ll = iter pg_cons_not "true" " and " ll in - let pg_where = match ct, cfl with - | [], [] -> "" - | lt, [] -> " where " ^ pg_cons lt - | [], llf -> " where " ^ pg_cons_not_l llf - | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf - in - if cols = [] then - let r = exec c ("select count(source) from " ^ table ^ pg_where) in - match r with - | [[s]] when int_of_string s > 0 -> [[]] - | _ -> [] - else - exec c ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ - " order by " ^ List.hd cols ^ " asc") - -(* funzioni vecchie ********************************************************) -(* -let pg_name h s = - let q = "select id from registry where uri = " ^ quote s in - match exec h q with - | [[id]] -> "t" ^ id - | _ -> "" - -let get_id b = if b then ["B"] else ["F"] -*) diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.mli b/helm/ocaml/mathql_interpreter/mQIPostgres.mli deleted file mode 100644 index cbbf3929d..000000000 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.mli +++ /dev/null @@ -1,36 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val init : unit -> Postgres.connection - -val close : Postgres.connection -> unit - -val exec : Postgres.connection * (MQITypes.query -> unit) -> - MQITypes.table -> MQITypes.columns -> - string MQITypes.con_true -> string MQITypes.con_false -> - MQITypes.result diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml deleted file mode 100644 index 0e3e2be72..000000000 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ /dev/null @@ -1,103 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -module M = MathQL -module C = MQIConn -module U = MQIUtil -module A = MQIMap - -let not_supported s = - raise (Failure ("MQIProperty: feature not supported: " ^ s)) - -(* debugging ***************************************************************) - -let pg_print l = - let rec pg_record = function - | [] -> prerr_newline () - | head :: tail -> prerr_string (head ^ " "); pg_record tail - in - List.iter pg_record l - -let cl_print l = - let c_print (b, p, v) = - prerr_string (if b then "match " else "in "); - List.iter (fun x -> prerr_string ("/" ^ x)) p; - prerr_newline (); - List.iter prerr_endline v - in - List.iter c_print l - -(* 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 get_name = function (p, None) -> p | (_, Some p) -> p in - let names = List.map get_name el in - let mk_grp l = - let grp = U.mql_iter2 (fun p s -> [(p, [s])]) names l in - if grp = [] then [] else [grp] - in - let mk_avs l = - if subj = "" then ("", mk_grp l) else (List.hd l, mk_grp (List.tl l)) - in - compose mk_avs res - -let get_table h mc ct cfl el = - let aux_c ts (_, p, _) = A.refine_tables ts (C.tables h p) in - let aux_e ts (p, _) = A.refine_tables ts (C.tables h p) in - let fst = C.tables h mc in - let snd = List.fold_left aux_c fst (ct @ (List.concat cfl)) in - let trd = List.fold_left aux_e snd el in - A.default_table trd - -let exec_single h mc ct cfl el table = - let conv p = C.field h p table in - let first = conv mc in - let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in - let cons_true = mk_con ct in - let cons_false = List.map mk_con cfl in - let other_cols = List.map (fun (p, _) -> conv p) el in - let cols = if first = "" then other_cols else first :: other_cols in - let out q = if C.set h C.Queries then C.log h (q ^ "\n") in - let r = C.exec h out (C.resolve h table) cols cons_true cons_false in - pg_result false first el r - -let deadline = 100 - -let exec h refine mc ct cfl el = - if refine <> M.RefineExact then not_supported "exec"; - let table = get_table h mc ct cfl el in - let rec exec_aux ct = match ct with - | (pat, p, v) :: tail when List.length v > deadline -> - let single s = exec_aux ((pat, p, [s]) :: tail) in - U.mql_iter single v - | _ -> - exec_single h mc ct cfl el table - in exec_aux ct diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.mli b/helm/ocaml/mathql_interpreter/mQIProperty.mli deleted file mode 100644 index f8159aaa8..000000000 --- a/helm/ocaml/mathql_interpreter/mQIProperty.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val exec: MQIConn.handle -> - MathQL.refine -> MathQL.path -> - MathQL.path MQITypes.con_true -> MathQL.path MQITypes.con_false -> - MathQL.exp_list -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQITypes.ml b/helm/ocaml/mathql_interpreter/mQITypes.ml deleted file mode 100644 index ad4a8cb1b..000000000 --- a/helm/ocaml/mathql_interpreter/mQITypes.ml +++ /dev/null @@ -1,43 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -type 'a con = MathQL.pattern * 'a * MathQL.value - -type 'a con_true = 'a con list - -type 'a con_false = 'a con list list - -type table = string - -type columns = string list - -type result = string list list - -type query = string diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml deleted file mode 100644 index 3f3fe6591..000000000 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ /dev/null @@ -1,155 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -(* boolean constants *******************************************************) - -let mql_false = [] - -let mql_true = [""] - -(* set theoretic operations *************************************************) - -let rec set_sub v1 v2 = - match v1, v2 with - | [], _ -> mql_true - | _, [] -> mql_false - | h1 :: _, h2 :: _ when h1 < h2 -> mql_false - | h1 :: _, h2 :: t2 when h1 > h2 -> set_sub v1 t2 - | _ :: t1, _ :: t2 -> set_sub t1 t2 - -let rec set_meet v1 v2 = - match v1, v2 with - | [], _ -> mql_false - | _, [] -> mql_false - | h1 :: t1, h2 :: _ when h1 < h2 -> set_meet t1 v2 - | h1 :: _, h2 :: t2 when h1 > h2 -> set_meet v1 t2 - | _, _ -> mql_true - -let set_eq v1 v2 = - if v1 = v2 then mql_true else mql_false - -let rec set_union v1 v2 = - match v1, v2 with - | [], v -> v - | v, [] -> v - | 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 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 ******************************************************) - -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 diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli deleted file mode 100644 index 76735a863..000000000 --- a/helm/ocaml/mathql_interpreter/mQIUtil.mli +++ /dev/null @@ -1,69 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val mql_true : MathQL.value - -val mql_false : MathQL.value - -val set_sub : MathQL.value -> MathQL.value -> MathQL.value - -val set_meet : MathQL.value -> MathQL.value -> MathQL.value - -val set_eq : MathQL.value -> MathQL.value -> MathQL.value - -val set_union : 'a list -> 'a list -> 'a list - -val 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_prod : MathQL.attribute_set -> MathQL.attribute_set -> - MathQL.attribute_set - -val mql_intersect : MathQL.result -> MathQL.result -> MathQL.result - -val mql_diff : MathQL.result -> MathQL.result -> MathQL.result - -val iter : ('a -> 'b list) -> 'a list -> 'b list - -val mql_iter : ('c -> ('a * 'b list) list) -> 'c list -> - ('a * 'b list) list - -val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list -> - 'd list -> ('a * 'b list) list - -val xor : MathQL.value -> MathQL.value -> MathQL.value - -val le : MathQL.value -> MathQL.value -> MathQL.value - -val lt : MathQL.value -> MathQL.value -> MathQL.value - -val align : string -> string -> MathQL.value - -val set : string * 'a -> (string * 'a) list -> (string * 'a) list diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml deleted file mode 100644 index 9280a2c2a..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ /dev/null @@ -1,247 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -(* contexts *****************************************************************) - -type svar_context = (MathQL.svar * MathQL.resource_set) list - -type avar_context = (MathQL.avar * MathQL.resource) list - -type group_context = (MathQL.avar * MathQL.attribute_group) list - -type vvar_context = (MathQL.vvar * MathQL.value) list - -type context = {svars: svar_context; - avars: avar_context; - groups: group_context; (* auxiliary context *) - vvars: vvar_context - } - -(* execute *****************************************************************) - -exception Found - -module M = MathQL -module P = MQueryUtil -module C = MQIConn -module U = MQIUtil - -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) "\n" q - end - in - let rec eval_val c = function - | M.False -> U.mql_false - | M.True -> U.mql_true - | M.Const s -> [s] - | M.Set l -> U.iter (eval_val c) l - | M.Test (k,y1,y2) -> - let cand y1 y2 = - if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2 - in - let cor y1 y2 = - let v1 = eval_val c y1 in - if v1 = U.mql_false then eval_val c y2 else v1 - in - let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in - let f = match k with - | M.And -> cand - | M.Or -> cor - | M.Xor -> h U.xor - | M.Sub -> h U.set_sub - | M.Meet -> h U.set_meet - | M.Eq -> h U.set_eq - | M.Le -> h U.le - | M.Lt -> h U.lt - in - f y1 y2 - | M.Not y -> - if eval_val c y = U.mql_false then U.mql_true else U.mql_false - | M.VVar i -> begin - try List.assoc i c.vvars - with Not_found -> warn (M.Subj (M.VVar i)); [] end - | M.Dot (i,p) -> begin - try List.assoc p (List.assoc i c.groups) - with Not_found -> warn (M.Subj (M.Dot (i,p))); [] end - | M.Proj (None,x) -> List.map (fun (r, _) -> r) (eval_query c x) - | M.Proj ((Some p),x) -> - let proj_group_aux (q, v) = if q = p then v else [] in - let proj_group a = U.iter proj_group_aux a in - let proj_set (_, g) = U.iter proj_group g in - U.iter proj_set (eval_query c x) - | M.Ex (l,y) -> - let rec ex_aux h = function - | [] -> - let d = {c with groups = h} in - if eval_val d y = U.mql_false then () else raise Found - | i :: tail -> - begin - try - let (_, a) = List.assoc i c.avars in - let rec add_group = function - | [] -> () - | g :: t -> ex_aux ((i, g) :: h) tail; add_group t - in - add_group a - with Not_found -> () - end - in - (try ex_aux [] l; U.mql_false with Found -> U.mql_true) - | M.StatVal y -> - let t = 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) "\n" x; - let s = P.stop_time t in - if C.set h C.Times 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) "\n" s; - let r = P.stop_time t in - if C.set h C.Times 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 - eval_query d x2 - | M.LetVVar (i,y,x) -> - let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in - eval_query d x - | M.For (k,i,x1,x2) -> - let f = match k with - | M.GenFJoin -> U.mql_union - | M.GenFMeet -> U.mql_intersect - in - let rec for_aux = function - | [] -> [] - | h :: t -> - let d = {c with avars = U.set (i, h) c.avars} in - f (eval_query d x2) (for_aux t) - in - for_aux (eval_query c x1) - | M.Add (b,z,x) -> - let f = if b then U.mql_prod else U.set_union in - let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in - List.fold_right g (eval_query c x) [] - | M.Property (q0,q1,q2,mc,ct,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) - in - let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in - let cons_true = mct :: List.map eval_cons ct in - let cons_false = List.map (List.map eval_cons) cfl in - let eval_exp (p, po) = (q2 @ p, po) in - let exp = List.map eval_exp el in - let t = P.start_time () in - 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.Times 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 - then select_aux t else h :: select_aux t - in - select_aux (eval_query c x) - | M.Keep (b,l,x) -> - let keep_path (p, v) t = - if List.mem p l = b then t else (p, v) :: t in - let keep_grp a = List.fold_right keep_path a [] in - let keep_set a g = - let kg = keep_grp a in - if kg = [] then g else kg :: g - in - let keep_av (s, g) = (s, List.fold_right keep_set g []) in - List.map keep_av (eval_query c x) - and eval_grp c = function - | M.Attr gs -> - let attr_aux g (p, y) = U.mql_union g [(p, eval_val 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 t = P.start_time () in - if C.set h C.Source then P.text_of_query (C.log h) "\n" x; - let r = eval_query c x in - if C.set h C.Result then P.text_of_result (C.log h) "\n" r; - let s = P.stop_time t in - if C.set h C.Times then - C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s - (C.string_of_flags (C.flags h))); - r diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli b/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli deleted file mode 100644 index 9d7081fff..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val execute : MQIConn.handle -> MathQL.query -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll deleted file mode 100644 index ca51751f0..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll +++ /dev/null @@ -1,133 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -{ - open MQueryTParser - - let debug = false - - let out s = if debug then prerr_endline s -} - -let SPC = [' ' '\t' '\n']+ -let ALPHA = ['A'-'Z' 'a'-'z' '_'] -let NUM = ['0'-'9'] -let IDEN = ALPHA (NUM | ALPHA)* -let QSTR = [^ '"' '\\']+ - -rule comm_token = parse - | "(*" { comm_token lexbuf; comm_token lexbuf } - | "*)" { () } - | ['*' '('] { comm_token lexbuf } - | [^ '*' '(']* { comm_token lexbuf } -and string_token = parse - | '"' { DQ } - | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } - | QSTR { STR (Lexing.lexeme lexbuf) } - | eof { EOF } -and query_token = parse - | "(*" { comm_token lexbuf; query_token lexbuf } - | SPC { query_token lexbuf } - | '"' { let str = qstr string_token lexbuf in - out ("STR " ^ str); STR str } - | '(' { out "LP"; LP } - | ')' { out "RP"; RP } - | '{' { out "LC"; LC } - | '}' { out "RC"; RC } - | '@' { out "AT"; AT } - | '%' { out "PC"; PC } - | '$' { out "DL"; DL } - | '.' { out "FS"; FS } - | ',' { out "CM"; CM } - | ';' { out "SC"; SC } - | '/' { out "SL"; SL } - | "add" { out "ADD" ; ADD } - | "align" { out "ALIGN" ; ALIGN } - | "allbut" { out "BUT" ; BUT } - | "and" { out "AND" ; AND } - | "as" { out "AS" ; AS } - | "attr" { out "ATTR" ; ATTR } - | "be" { out "BE" ; BE } - | "count" { out "COUNT" ; COUNT } - | "diff" { out "DIFF" ; DIFF } - | "distr" { out "DISTR" ; DISTR } - | "else" { out "ELSE" ; ELSE } - | "empty" { out "EMPTY" ; EMPTY } - | "eq" { out "EQ" ; EQ } - | "ex" { out "EX" ; EX } - | "false" { out "FALSE" ; FALSE } - | "for" { out "FOR" ; FOR } - | "from" { out "FROM" ; FROM } - | "if" { out "IF" ; IF } - | "in" { out "IN" ; IN } - | "inf" { out "INF" ; INF } - | "intersect" { out "INTER" ; INTER } - | "inverse" { out "INV" ; INV } - | "istrue" { out "IST" ; IST } - | "isfalse" { out "ISF" ; ISF } - | "keep" { out "KEEP" ; KEEP } - | "le" { out "LE" ; LE } - | "let" { out "LET" ; LET } - | "log" { out "LOG" ; LOG } - | "lt" { out "LT" ; LT } - | "main" { out "MAIN" ; MAIN } - | "match" { out "MATCH" ; MATCH } - | "meet" { out "MEET" ; MEET } - | "not" { out "NOT" ; NOT } - | "of" { out "OF" ; OF } - | "or" { out "OR" ; OR } - | "pattern" { out "PAT" ; PAT } - | "proj" { out "PROJ" ; PROJ } - | "property" { out "PROP" ; PROP } - | "select" { out "SELECT"; SELECT } - | "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 } - | "true" { out "TRUE" ; TRUE } - | "union" { out "UNION" ; UNION } - | "where" { out "WHERE" ; WHERE } - | "xor" { out "XOR" ; XOR } - | IDEN { let id = Lexing.lexeme lexbuf in - out ("ID " ^ id); ID id } - | eof { out "EOF" ; EOF } -and result_token = parse - | SPC { result_token lexbuf } - | "(*" { comm_token lexbuf; result_token lexbuf } - | '"' { STR (qstr string_token lexbuf) } - | '/' { out "SL"; SL } - | '{' { LC } - | '}' { RC } - | ',' { CM } - | ';' { SC } - | '=' { IS } - | "attr" { ATTR } - | eof { EOF } diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly deleted file mode 100644 index 2f8896185..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly +++ /dev/null @@ -1,314 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -/* AUTOR: Ferruccio Guidi - */ - -%{ - module M = MathQL - - let analyze x = - let rec join l1 l2 = match l1, l2 with - | [], _ -> l2 - | _, [] -> l1 - | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 - | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 - | s1 :: tl1, s2 :: tl2 -> s1 :: join tl1 tl2 - in - let rec iter f = function - | [] -> [] - | 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] - | M.For (_,_,x,y) -> iter an_set [x; y] - | 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 - and an_con c = iter fc c - and fg (_, v) = an_val v - and an_grp = function - | M.Attr g -> iter (iter fg) g - | M.From _ -> [] - in - an_val x - - let f (x, y, z) = x - let s (x, y, z) = y - let t (x, y, z) = z -%} - %token ID STR - %token SL IS LC RC CM SC LP RP AT PC DL 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 - %left DIFF - %left UNION - %left INTER - %nonassoc WHERE EX - %left XOR OR - %left AND - %nonassoc NOT - %nonassoc SUB MEET EQ LT LE - %nonassoc SUBJ OF PROJ COUNT ALIGN - - %start qstr query result - %type qstr - %type query - %type result -%% - qstr: - | DQ { "" } - | STR qstr { $1 ^ $2 } - ; - svar: - | PC ID { $2 } - ; - avar: - | AT ID { $2 } - ; - vvar: - | DL ID { $2 } - ; - strs: - | STR CM strs { $1 :: $3 } - | STR { [$1] } - ; - subpath: - | STR SL subpath { $1 :: $3 } - | STR { [$1] } - ; - path: - | subpath { $1 } - | SL subpath { $2 } - | SL { [] } - ; - paths: - | path CM paths { $1 :: $3 } - | path { [$1] } - inv: - | INV { true } - | { false } - ; - ref: - | SUB { M.RefineSub } - | SUPER { M.RefineSuper } - | { M.RefineExact } - ; - qualif: - | inv ref path { $1, $2, $3 } - ; - cons: - | path IN val_exp { (false, $1, $3) } - | path MATCH val_exp { (true, $1, $3) } - ; - conss: - | cons CM conss { $1 :: $3 } - | cons { [$1] } - ; - istrue: - | IST conss { $2 } - | { [] } - ; - isfalse: - | { [] } - | ISF conss isfalse { $2 :: $3 } - ; - mainc: - | MAIN path { $2 } - | { [] } - ; - exp: - | path AS path { $1, Some $3 } - | path { $1, None } - ; - exps: - | exp CM exps { $1 :: $3 } - | exp { [$1] } - ; - attrc: - | ATTR exps { $2 } - | { [] } - ; - pattern: - | PAT { true } - | { false } - ; - opt_path: - | path { Some $1 } - | { None } - ; - ass: - | val_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 } - ; - 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 } - ; - 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 } - ; - xml: - | { false} - ; - 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) } - | 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 - { 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 } - ; - query: - | set_exp { $1 } - | set_exp error { $1 } - | EOF { raise End_of_file } - ; - attr: - | path IS strs { $1, $3 } - | path { $1, [] } - ; - attrs: - | attr SC attrs { $1 :: $3 } - | attr { [$1] } - ; - group: - LC attrs RC { $2 } - ; - groups: - | group CM groups { $1 :: $3 } - | group { [$1] } - ; - resource: - | STR ATTR groups { ($1, $3) } - | STR { ($1, []) } - ; - resources: - | resource SC resources { $1 :: $3 } - | resource { [$1] } - | { [] } - ; - result: - | resources { $1 } - | EOF { raise End_of_file } diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml deleted file mode 100644 index 6323cc950..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.ml +++ /dev/null @@ -1,220 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* $Id$ *) - -(* 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 sep x = - 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 sep x = - 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) - diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.mli b/helm/ocaml/mathql_interpreter/mQueryUtil.mli deleted file mode 100644 index 575400298..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val text_of_query : (string -> unit) -> string -> MathQL.query -> unit - -val text_of_result : (string -> unit) -> string -> MathQL.result -> 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