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