X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;fp=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=784bc11dcbfe37a639774c71015b166b5db48b20;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953 diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml new file mode 100644 index 000000000..784bc11dc --- /dev/null +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -0,0 +1,191 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +(* $Id$ *) + +module M = MathQL +module T = MQGTypes +module U = MQGUtil + +(* low level functions *****************************************************) + +let locate s = + let query = + M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) ) + in query + +let unreferred target_pattern source_pattern = + let query = + M.Bin (M.BinFDiff, + ( + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const target_pattern)) + ), ( + M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern)) + + )) + in query + +let compose cl = + let letin = ref [] in + let must = ref [] in + let onlyobj = ref [] in + let onlysort = ref [] in + let onlyrel = ref [] in + let only = ref true in + let univ = ref [] in + let set_val = function + | [s] -> M.Const s + | l -> + let msval = M.Set (List.map (fun s -> M.Const s) l) in + if ! only then begin + let vvar = "val" ^ string_of_int (List.length ! letin) in + letin := (vvar, msval) :: ! letin; + M.VVar vvar + end else msval + in + let cons o (r, s, p, d) = + let con p = function + | [] -> [] + | l -> [(false, [p], set_val l)] + in + only := o; + con "h:occurrence" r @ + con "h:sort" (List.map U.string_of_sort s) @ + con "h:position" (List.map U.string_of_position p) @ + con "h:depth" (List.map U.string_of_depth d) + in + let property_must n c = + M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const "")) + in + let property_only n cl = + let rec build = function + | [] -> [] + | c :: tl -> + let r = (cons true) c in + if r = [] then build tl else r :: build tl + in + let cll = build cl in + M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) + in + let rec aux = function + | [] -> () + | T.Universe l :: tail -> + only := true; + let l = List.map U.string_of_position l in + univ := [(false, ["h:position"], set_val l)]; aux tail + | T.MustObj(r,p,d) :: tail -> + must := property_must "refObj" (r, [], p, d) :: ! must; aux tail + | T.MustSort(s,p,d) :: tail -> + must := property_must "refSort" ([], s, p, d) :: ! must; aux tail + | T.MustRel(p,d) :: tail -> + must := property_must "refRel" ([], [], p, d) :: ! must; aux tail + | T.OnlyObj(r,p,d) :: tail -> + onlyobj := (r, [], p, d) :: ! onlyobj; aux tail + | T.OnlySort(s,p,d) :: tail -> + onlysort := ([], s, p, d) :: ! onlysort; aux tail + | T.OnlyRel(p,d) :: tail -> + onlyrel := ([], [], p, d) :: ! onlyrel; aux tail + in + let rec iter f g = function + | [] -> raise (Failure "MQueryGenerator.iter") + | [head] -> (f head) + | head :: tail -> let t = (iter f g tail) in g (f head) t + in + (* prerr_endline "(** Compose: received constraints **)"; + U.mathql_of_specs prerr_string cl; flush stderr; *) + aux cl; + let must_query = + if ! must = [] then + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*")) + else + iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must + in + let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in + let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in + let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in + let select_query x = + match ! onlyobj, ! onlysort, ! onlyrel with + | [], [], [] -> x + | _, [], [] -> M.Select("obj",x,onlyobj_val) + | [], _, [] -> M.Select("obj",x,onlysort_val) + | [], [], _ -> M.Select("obj",x,onlyrel_val) + | _, _, [] -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val))) + | _, [], _ -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val))) + | [], _, _ -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val))) + | _, _, _ -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val))) + in + let letin_query = + if ! letin = [] then fun x -> x + else + let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in + iter f (fun x y z -> x (y z)) ! letin + in + letin_query (select_query must_query) + +(* high-level functions ****************************************************) + +let query_of_constraints u (musts_obj, musts_rel, musts_sort) + (onlys_obj, onlys_rel, onlys_sort) = + let conv = function + | `MainHypothesis None -> [T.MainHypothesis], [] + | `MainHypothesis (Some d) -> [T.MainHypothesis], [d] + | `MainConclusion None -> [T.MainConclusion], [] + | `MainConclusion (Some d) -> [T.MainConclusion], [d] + | `InHypothesis -> [T.InHypothesis], [] + | `InConclusion -> [T.InConclusion], [] + | `InBody -> [T.InBody], [] + in + let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in + let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in + let must_rel p = let p, d = conv p in T.MustRel (p, d) in + let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in + let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in + let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in + let must = List.map must_obj musts_obj @ + List.map must_rel musts_rel @ + List.map must_sort musts_sort + in + let only = + (match onlys_obj with + | None -> [] + | Some [] -> [T.OnlyObj ([], [], [])] + | Some l -> List.map only_obj l + ) @ + (match onlys_rel with + | None -> [] + | Some [] -> [T.OnlyRel ([], [])] + | Some l -> List.map only_rel l + ) @ + (match onlys_sort with + | None -> [] + | Some [] -> [T.OnlySort ([], [], [])] + | Some l -> List.map only_sort l + ) + in + let univ = match u with None -> [] | Some l -> [T.Universe l] in + compose (must @ only @ univ)