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
65 let aux (s, gl) = U.iter (aux2 s) gl in
69 try c, I.grp_read (List.assoc i c.groups) p
70 with Not_found -> warn (M.Dot (i, p)); c, I.empty
73 let rec ex_aux h = function
75 let d = {c with groups = h} in
76 if snd (eval_query d y) = U.val_false then () else raise Found
80 let (_, a) = List.assoc i c.avars in
81 let rec add_group = function
83 | g :: t -> ex_aux ((i, g) :: h) tail; add_group t
89 begin try ex_aux [] l; c, U.val_false with Found -> c, U.val_true end
92 try c, List.assoc i c.svars
93 with Not_found -> warn (M.SVar i); c, I.empty
98 let s, gl = List.assoc i c.avars in
100 with Not_found -> warn (M.AVar i); c, I.empty
102 | M.Let (Some i, x1, x2) ->
103 let d, r = eval_query c x1 in
104 let d = {d with svars = P.add_assoc (i, r) d.svars} in
106 | M.Let (None, x1, x2) ->
107 let d, r = eval_query c x1 in eval_query d x2
108 | M.For (k, i, x1, x2) ->
110 | M.GenFJoin -> I.union
111 | M.GenFMeet -> I.intersect
113 let for_aux (d, r) s gl _ =
114 let d = {d with avars = P.add_assoc (i, (s, gl)) d.avars} in
115 let d, s = eval_query d x2 in
118 let d, r = eval_query c x1 in
119 I.x_iter for_aux (d, I.empty) r
120 | M.While (k, x1, x2) ->
122 | M.GenFJoin -> I.union
123 | M.GenFMeet -> I.intersect
125 let rec while_aux (d, r) =
126 let d, b = eval_query d x1 in
127 if b = U.val_false then d, r else
128 let d, s = eval_query d x2 in
131 while_aux (c, U.val_false)
133 let f = if b then I.d_union else I.union in
134 let agl = eval_grp c z in
136 I.append (f (U.make_x sj gl) (U.make_x sj agl)) r
138 let _, r = eval_query c x in
139 c, I.x_iter aux I.empty r
140 | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) ->
141 let _, r = eval_query c y in
143 if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r)
145 let eval_cons (pat, p, y) =
146 let _, r = eval_query c y in (pat, q2 @ p, r)
148 let cons_true = mct :: List.map eval_cons ct in
149 let cons_false = List.map (List.map eval_cons) cfl in
150 let eval_exp (p, po) = (q2 @ p, po) in
151 let exp = List.map eval_exp el in
152 let t = P.start_time () in
153 let r = MQIProperty.exec h q1 subj cons_true cons_false exp in
154 let s = P.stop_time t in
155 if C.set h C.Stat then
156 C.log h (Printf.sprintf "Property: %s,%i\n" s (U.count r));
158 | M.Select (i, x, y) ->
159 let aux (d, r) sj gl _ =
160 let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in
161 let d, s = eval_query d y in
162 if s = U.val_false then d, r else d, (I.append (U.make_x sj gl) r)
164 let d, r = eval_query c x in
165 I.x_iter aux (d, I.empty) r
166 | M.Fun (p, pl, xl) ->
167 let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
168 c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec
171 let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
172 eval_query c (L.gen_eval e p xl)
175 let _, r = eval_query c y in
179 and eval_grp c = function
181 let attr_auxs s l = I.grps_make s (eval_list c l) in
182 List.fold_left attr_auxs [] gs
184 try snd (List.assoc i c.avars)
185 with Not_found -> warn (M.AVar i); []
187 let c = {svars = []; avars = []; groups = []} in
188 let t = P.start_time () in
189 let _, r = eval_query c x in
190 let s = P.stop_time t in
191 if C.set h C.Stat then
192 C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s
193 (C.string_of_flags (C.flags h)));