--- /dev/null
+PACKAGE = mathql
+
+PREDICATES =
+
+INTERFACE_FILES =
+
+IMPLEMENTATION_FILES = mathQL.ml
+
+EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi
+
+EXTRA_OBJECTS_TO_CLEAN =
+
+include ../Makefile.common
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://www.cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+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
+ ->
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val get_constraints : Cic.term -> MQGTypes.must_restrictions
+
+exception NotAnInductiveDefinition
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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]
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val get_constraints: Cic.metasenv -> Cic.context -> Cic.term ->
+ MQGTypes.r_obj list list *
+ MQGTypes.r_obj list
+
+val universe : MQGTypes.universe
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 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]
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 02/12/2002 *)
+(* *)
+(* Missing description *)
+(* *)
+(******************************************************************************)
+
+val get_constraints : Cic.term -> MQGTypes.must_restrictions
+
+val universe : MQGTypes.universe
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTORS: Ferruccio Guidi <fguidi@cs.unibo.it>
+ * Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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)
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* 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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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")
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+type 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+type 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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")
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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"]
+*)
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val 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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val exec: MQIConn.handle ->
+ MathQL.refine -> MathQL.path ->
+ MathQL.path MQITypes.con_true -> MathQL.path MQITypes.con_false ->
+ MathQL.exp_list -> MathQL.result
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val mql_true : MathQL.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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val execute : MQIConn.handle -> MathQL.query -> MathQL.result
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+{
+ 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 }
--- /dev/null
+/* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ */
+
+/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ */
+
+%{
+ module M = MathQL
+
+ 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 <string> 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 <string> qstr
+ %type <MathQL.query> query
+ %type <MathQL.result> 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 }
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $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)
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val text_of_query : (string -> unit) -> 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
+++ /dev/null
-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
- ->
+++ /dev/null
-PACKAGE = mathql
-
-PREDICATES =
-
-INTERFACE_FILES =
-
-IMPLEMENTATION_FILES = mathQL.ml
-
-EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi
-
-EXTRA_OBJECTS_TO_CLEAN =
-
-include ../Makefile.common
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://www.cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val get_constraints : Cic.term -> MQGTypes.must_restrictions
-
-exception NotAnInductiveDefinition
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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]
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val get_constraints: Cic.metasenv -> Cic.context -> Cic.term ->
- MQGTypes.r_obj list list *
- MQGTypes.r_obj list
-
-val universe : MQGTypes.universe
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 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]
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 02/12/2002 *)
-(* *)
-(* Missing description *)
-(* *)
-(******************************************************************************)
-
-val get_constraints : Cic.term -> MQGTypes.must_restrictions
-
-val universe : MQGTypes.universe
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTORS: Ferruccio Guidi <fguidi@cs.unibo.it>
- * Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* 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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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)
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* 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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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")
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-type 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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-type 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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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")
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val 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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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"]
-*)
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val 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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val exec: MQIConn.handle ->
- MathQL.refine -> MathQL.path ->
- MathQL.path MQITypes.con_true -> MathQL.path MQITypes.con_false ->
- MathQL.exp_list -> MathQL.result
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val mql_true : MathQL.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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val execute : MQIConn.handle -> MathQL.query -> MathQL.result
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-{
- 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 }
+++ /dev/null
-/* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- */
-
-/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- */
-
-%{
- module M = MathQL
-
- 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 <string> 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 <string> qstr
- %type <MathQL.query> query
- %type <MathQL.result> 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 }
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* $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)
-
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val text_of_query : (string -> unit) -> 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
projects / helm.git / commitdiff