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=0000000000000000000000000000000000000000;hp=40c0ea0b8372dc063f79f4087ccde41aaa04c310;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml deleted file mode 100644 index 40c0ea0b8..000000000 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ /dev/null @@ -1,189 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -module M = MathQL -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 M.StatQuery 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 M.StatQuery 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 cll = List.map (cons true) 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 - M.StatQuery (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) -