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>
39 (* contexts *****************************************************************)
41 type svar_context = (M.svar * M.result) list
43 type avar_context = (M.avar * (string * M.group list)) list
45 type group_context = (M.avar * M.group) list
47 type context = {svars: svar_context;
49 groups: group_context (* auxiliary context *)
52 (* execute ******************************************************************)
56 if C.set h C.Warn then
58 C.log h "MQIExecute: waring: reference to undefined variables: ";
59 F.text_of_query (C.log h) "\n" q
62 let rec eval_query c = function
64 let aux2 s g = I.make s (eval_list c g) in
66 if gl = [] then U.avs_of_string s else U.iter (aux2 s) gl
71 try c, I.grp_read (List.assoc i c.groups) p
72 with Not_found -> warn (M.Dot (i, p)); c, I.empty
75 let rec ex_aux h = function
77 let d = {c with groups = h} in
78 if snd (eval_query d y) = U.val_false then () else raise Found
82 let (_, a) = List.assoc i c.avars in
83 let rec add_group = function
85 | g :: t -> ex_aux ((i, g) :: h) tail; add_group t
91 begin try ex_aux [] l; c, U.val_false with Found -> c, U.val_true end
94 try c, List.assoc i c.svars
95 with Not_found -> warn (M.SVar i); c, I.empty
100 let s, gl = List.assoc i c.avars in
102 with Not_found -> warn (M.AVar i); c, I.empty
104 | M.Let (Some i, x1, x2) ->
105 let d, r = eval_query c x1 in
106 let d = {d with svars = P.add_assoc (i, r) d.svars} in
108 | M.Let (None, x1, x2) ->
109 let d, r = eval_query c x1 in eval_query d x2
110 | M.For (k, i, x1, x2) ->
112 | M.GenFJoin -> I.union
113 | M.GenFMeet -> I.intersect
115 let for_aux (d, r) s gl _ =
116 let d = {d with avars = P.add_assoc (i, (s, gl)) d.avars} in
117 let d, s = eval_query d x2 in
120 let d, r = eval_query c x1 in
121 I.x_iter for_aux (d, I.empty) (I.optimize r)
122 | M.While (k, x1, x2) ->
124 | M.GenFJoin -> I.union
125 | M.GenFMeet -> I.intersect
127 let rec while_aux (d, r) =
128 let d, b = eval_query d x1 in
129 if b = U.val_false then d, r else
130 let d, s = eval_query d x2 in
133 while_aux (c, U.val_false)
135 let f = if b then I.d_union else I.union in
136 let agl = eval_grp c z in
138 I.union r (f (U.make_x sj gl) (U.make_x sj agl))
140 let _, r = eval_query c x in
141 c, I.x_iter aux I.empty (I.optimize r)
142 | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) ->
143 let _, r = eval_query c y in
145 if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r)
147 let eval_cons (pat, p, y) =
148 let _, r = eval_query c y in (pat, q2 @ p, r)
150 let cons_true = mct :: List.map eval_cons ct in
151 let cons_false = List.map (List.map eval_cons) cfl in
152 let eval_exp (p, po) = (q2 @ p, po) in
153 let exp = List.map eval_exp el in
154 let t = P.start_time () in
155 let r = MQIProperty.exec h q1 subj cons_true cons_false exp in
156 let s = P.stop_time t in
157 if C.set h C.Times then
158 C.log h (Printf.sprintf "Property: %s,%i\n" s (U.count r));
160 | M.Select (i, x, y) ->
161 let aux (d, r) sj gl _ =
162 let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in
163 let d, s = eval_query d y in
164 if s = U.val_false then d, r else d, (I.union r (U.make_x sj gl))
166 let d, r = eval_query c x in
167 I.x_iter aux (d, I.empty) (I.optimize r)
168 | M.Fun (p, pl, xl) ->
169 let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
170 c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec
173 let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
174 eval_query c (L.gen_eval e p xl)
177 let _, r = eval_query c y in
181 and eval_grp c = function
183 let attr_auxs s l = I.grps_make s (eval_list c l) in
184 List.fold_left attr_auxs [] gs
186 try snd (List.assoc i c.avars)
187 with Not_found -> warn (M.AVar i); []
189 let c = {svars = []; avars = []; groups = []} in
190 let t = P.start_time () in
191 if C.set h C.Source then F.text_of_query (C.log h) "\n" x;
192 let _, r = eval_query c x in
193 if C.set h C.Result then F.text_of_result (C.log h) "\n" r;
194 let s = P.stop_time t in
195 if C.set h C.Times then
196 C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s
197 (C.string_of_flags (C.flags h)));