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 (* contexts *****************************************************************)
28 type svar_context = (MathQL.svar * MathQL.resource_set) list
30 type avar_context = (MathQL.avar * MathQL.resource) list
32 type group_context = (MathQL.avar * MathQL.attribute_group) list
34 type vvar_context = (MathQL.vvar * MathQL.value) list
36 type context = {svars: svar_context;
38 groups: group_context; (* auxiliary context *)
42 (* execute *****************************************************************)
53 if C.set h C.Warn then
55 C.log h "MQIExecute: waring: reference to undefined variables: ";
56 P.text_of_query (C.log h) q "\n"
59 let rec eval_val c = function
60 | M.False -> U.mql_false
61 | M.True -> U.mql_true
63 | M.Set l -> U.iter (eval_val c) l
66 if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2
69 let v1 = eval_val c y1 in
70 if v1 = U.mql_false then eval_val c y2 else v1
72 let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in
77 | M.Sub -> h U.set_sub
78 | M.Meet -> h U.set_meet
85 if eval_val c y = U.mql_false then U.mql_true else U.mql_false
87 try List.assoc i c.vvars
88 with Not_found -> warn (M.Subj (M.VVar i)); [] end
90 try List.assoc p (List.assoc i c.groups)
91 with Not_found -> warn (M.Subj (M.Dot i p)); [] end
92 | M.Proj None x -> List.map (fun (r, _) -> r) (eval_query c x)
93 | M.Proj (Some p) x ->
94 let proj_group_aux (q, v) = if q = p then v else [] in
95 let proj_group a = U.iter proj_group_aux a in
96 let proj_set (_, g) = U.iter proj_group g in
97 U.iter proj_set (eval_query c x)
99 let rec ex_aux h = function
101 let d = {c with groups = h} in
102 if eval_val d y = U.mql_false then () else raise Found
106 let (_, a) = List.assoc i c.avars in
107 let rec add_group = function
109 | g :: t -> ex_aux ((i, g) :: h) tail; add_group t
115 (try ex_aux [] l; U.mql_false with Found -> U.mql_true)
117 let t = P.start_time () in
118 let r = (eval_val c y) in
119 let s = P.stop_time t in
120 C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
122 | M.Count y -> [string_of_int (List.length (eval_val c y))]
123 | M.Align s y -> U.iter (U.align s) (eval_val c y)
124 and eval_query c = function
127 List.map (fun s -> (s, [])) (eval_val c x)
130 let t = P.start_time () in
131 P.text_of_query (C.log h) x "\n";
132 let s = P.stop_time t in
133 if C.set h C.Stat then
134 C.log h (Printf.sprintf "Log source: %s\n" s);
137 let s = (eval_query c x) in
138 let t = P.start_time () in
139 P.text_of_result (C.log h) s "\n";
140 let r = P.stop_time t in
141 if C.set h C.Stat then
142 C.log h (Printf.sprintf "Log: %s\n" r);
146 if (eval_val c y) = U.mql_false
147 then (eval_query c x2) else (eval_query c x1)
150 | M.BinFJoin -> U.mql_union
151 | M.BinFMeet -> U.mql_intersect
152 | M.BinFDiff -> U.mql_diff
154 f (eval_query c x1) (eval_query c x2)
156 try List.assoc i c.svars
157 with Not_found -> warn (M.SVar i); [] end
159 try [List.assoc i c.avars]
160 with Not_found -> warn (M.AVar i); [] end
161 | M.LetSVar i x1 x2 ->
162 let d = {c with svars = U.set (i, eval_query c x1) c.svars} in
165 let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in
169 | M.GenFJoin -> U.mql_union
170 | M.GenFMeet -> U.mql_intersect
172 let rec for_aux = function
175 let d = {c with avars = U.set (i, h) c.avars} in
176 f (eval_query d x2) (for_aux t)
178 for_aux (eval_query c x1)
180 let f = if b then U.mql_prod else U.set_union in
181 let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in
182 List.fold_right g (eval_query c x) []
183 | M.Property q0 q1 q2 mc ct cfl el pat y ->
185 if q0 then [], (pat, q2 @ mc, eval_val c y)
186 else (q2 @ mc), (pat, [], eval_val c y)
188 let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in
189 let cons_true = mct :: List.map eval_cons ct in
190 let cons_false = List.map (List.map eval_cons) cfl in
191 let eval_exp (p, po) = (q2 @ p, po) in
192 let exp = List.map eval_exp el in
193 let t = P.start_time () in
194 let r = MQIProperty.exec h q1 subj cons_true cons_false exp in
195 let s = P.stop_time t in
196 if C.set h C.Stat then
197 C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
200 let t = P.start_time () in
201 let r = (eval_query c x) in
202 let s = P.stop_time t in
203 C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
206 let rec select_aux = function
209 let d = {c with avars = U.set (i, h) c.avars} in
210 if eval_val d y = U.mql_false
211 then select_aux t else h :: select_aux t
213 select_aux (eval_query c x)
215 let keep_path (p, v) t =
216 if List.mem p l = b then t else (p, v) :: t in
217 let keep_grp a = List.fold_right keep_path a [] in
219 let kg = keep_grp a in
220 if kg = [] then g else kg :: g
222 let keep_av (s, g) = (s, List.fold_right keep_set g []) in
223 List.map keep_av (eval_query c x)
224 and eval_grp c = function
226 let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] in
227 let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
228 List.fold_left attr_auxs [] gs
230 try snd (List.assoc i c.avars)
231 with Not_found -> warn (M.AVar i); []
233 let c = {svars = []; avars = []; groups = []; vvars = []} in
234 let t = P.start_time () in
235 let r = eval_query c x in
236 let s = P.stop_time t in
237 if C.set h C.Stat then
238 C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s
239 (C.string_of_flags (C.flags h)));