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