--- /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)
projects / helm.git / blobdiff