1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
33 (* helpers *****************************************************************)
35 let diff x y = M.Fun (["diff"], [], [x; y])
36 let union xl = M.Fun (["union"], [], xl)
37 let const s = M.Const [(s, [])]
38 let intersect xl = M.Fun (["intersect"], [], xl)
39 let lnot x = M.Fun (["not"], [], [x])
40 let lamp xl = M.Fun (["and"], [], xl)
42 (* low level functions *****************************************************)
46 M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
50 let unreferred target_pattern source_pattern =
54 M.Property (false, M.RefineExact, [], [], [], [], [],
55 true, (const target_pattern))
57 M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
58 [], [], [], true, (const source_pattern))
65 let onlyobj = ref [] in
66 let onlysort = ref [] in
67 let onlyrel = ref [] in
68 let only = ref true in
70 let set_val = function
73 let msval = union (List.map (fun s -> const s) l) in
75 let vvar = "val" ^ string_of_int (List.length ! letin) in
76 letin := (vvar, msval) :: ! letin;
80 let cons o (r, s, p, d) =
83 | l -> [(false, [p], set_val l)]
86 con "h:occurrence" r @
87 con "h:sort" (List.map U.string_of_sort s) @
88 con "h:position" (List.map U.string_of_position p) @
89 con "h:depth" (List.map U.string_of_depth d)
91 let property_must n c =
92 M.Property (true, M.RefineExact, [n], [],
93 (cons false c), [], [], false, (const ""))
95 let property_only n cl =
96 let cll = List.map (cons true) cl in
97 M.Property (false, M.RefineExact, [n], [],
98 ! univ, cll, [], false, (M.AVar "obj"))
100 let rec aux = function
102 | T.Universe l :: tail ->
104 let l = List.map U.string_of_position l in
105 univ := [(false, ["h:position"], set_val l)]; aux tail
106 | T.MustObj (r, p, d) :: tail ->
107 must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
108 | T.MustSort (s, p, d) :: tail ->
109 must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
110 | T.MustRel (p, d) :: tail ->
111 must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
112 | T.OnlyObj (r, p, d) :: tail ->
113 onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
114 | T.OnlySort (s, p, d) :: tail ->
115 onlysort := ([], s, p, d) :: ! onlysort; aux tail
116 | T.OnlyRel (p, d) :: tail ->
117 onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
119 let rec iter f g = function
120 | [] -> raise (Failure "MQueryGenerator.iter")
122 | head :: tail -> let t = (iter f g tail) in g (f head) t
124 prerr_endline "(** Compose: received constraints **)";
125 U.mathql_of_specs prerr_string cl; flush stderr;
129 M.Property (false, M.RefineExact, [], [],
130 [], [], [], true, (const ".*"))
134 let onlyobj_val = lnot (property_only "refObj" ! onlyobj) in
135 let onlysort_val = lnot (property_only "refSort" ! onlysort) in
136 let onlyrel_val = lnot (property_only "refRel" ! onlyrel) in
138 match ! onlyobj, ! onlysort, ! onlyrel with
140 | _, [], [] -> M.Select ("obj", x, onlyobj_val)
141 | [], _, [] -> M.Select ("obj", x, onlysort_val)
142 | [], [], _ -> M.Select ("obj", x, onlyrel_val)
143 | _, _, [] -> M.Select ("obj", x, lamp [onlyobj_val; onlysort_val])
144 | _, [], _ -> M.Select ("obj", x, lamp [onlyobj_val; onlyrel_val])
145 | [], _, _ -> M.Select ("obj", x, lamp [onlysort_val; onlyrel_val])
146 | _, _, _ -> M.Select ("obj", x, lamp [onlyobj_val; onlysort_val; onlyrel_val])
149 if ! letin = [] then fun x -> x
151 let f (vvar, msval) x = M.Let (Some vvar, msval, x) in
152 iter f (fun x y z -> x (y z)) ! letin
154 letin_query (select_query must_query)
156 (* high-level functions ****************************************************)
158 let query_of_constraints u (musts_obj, musts_rel, musts_sort)
159 (onlys_obj, onlys_rel, onlys_sort) =
161 | `MainHypothesis None -> [T.MainHypothesis], []
162 | `MainHypothesis (Some d) -> [T.MainHypothesis], [d]
163 | `MainConclusion None -> [T.MainConclusion], []
164 | `MainConclusion (Some d) -> [T.MainConclusion], [d]
165 | `InHypothesis -> [T.InHypothesis], []
166 | `InConclusion -> [T.InConclusion], []
167 | `InBody -> [T.InBody], []
169 let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in
170 let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in
171 let must_rel p = let p, d = conv p in T.MustRel (p, d) in
172 let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in
173 let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in
174 let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in
175 let must = List.map must_obj musts_obj @
176 List.map must_rel musts_rel @
177 List.map must_sort musts_sort
180 (match onlys_obj with
182 | Some [] -> [T.OnlyObj ([], [], [])]
183 | Some l -> List.map only_obj l
185 (match onlys_rel with
187 | Some [] -> [T.OnlyRel ([], [])]
188 | Some l -> List.map only_rel l
190 (match onlys_sort with
192 | Some [] -> [T.OnlySort ([], [], [])]
193 | Some l -> List.map only_sort l
196 let univ = match u with None -> [] | Some l -> [T.Universe l] in
197 compose (must @ only @ univ)