]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
cosmetic fix to pp_location
[helm.git] / helm / ocaml / mathql_interpreter / mQueryInterpreter.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
27  *)
28
29 (* contexts *****************************************************************)
30
31 type svar_context = (MathQL.svar * MathQL.resource_set) list
32
33 type avar_context = (MathQL.avar * MathQL.resource) list
34
35 type group_context = (MathQL.avar * MathQL.attribute_group) list
36
37 type vvar_context = (MathQL.vvar * MathQL.value) list
38
39 type context = {svars: svar_context;   
40                 avars: avar_context;   
41                 groups: group_context; (* auxiliary context *)
42                 vvars: vvar_context  
43                }
44
45 (* execute  *****************************************************************)
46
47 exception Found
48
49 module M = MathQL
50 module P = MQueryUtil 
51 module C = MQIConn
52 module U = MQIUtil
53
54 let execute h x =
55    let warn q = 
56      if C.set h C.Warn then 
57      begin
58         C.log h "MQIExecute: waring: reference to undefined variables: ";
59         P.text_of_query (C.log h) "\n" q
60      end
61    in
62    let rec eval_val c = function
63       | M.False -> U.mql_false
64       | M.True -> U.mql_true
65       | M.Const s -> [s]
66       | M.Set l -> U.iter (eval_val c) l
67       | M.Test (k,y1,y2) ->
68          let cand y1 y2 =
69             if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2
70          in
71          let cor y1 y2 =
72             let v1 = eval_val c y1 in
73             if v1 = U.mql_false then eval_val c y2 else v1
74          in
75          let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in
76          let f = match k with
77             | M.And  -> cand
78             | M.Or   -> cor
79             | M.Xor  -> h U.xor
80             | M.Sub  -> h U.set_sub
81             | M.Meet -> h U.set_meet
82             | M.Eq   -> h U.set_eq
83             | M.Le   -> h U.le
84             | M.Lt   -> h U.lt
85          in
86          f y1 y2 
87       | M.Not y -> 
88          if eval_val c y = U.mql_false then U.mql_true else U.mql_false
89       | M.VVar i -> begin
90          try List.assoc i c.vvars 
91          with Not_found -> warn (M.Subj (M.VVar i)); [] end
92       | M.Dot (i,p) -> begin
93          try List.assoc p (List.assoc i c.groups) 
94          with Not_found -> warn (M.Subj (M.Dot (i,p))); [] end
95       | M.Proj (None,x) -> List.map (fun (r, _) -> r) (eval_query c x)
96       | M.Proj ((Some p),x) -> 
97          let proj_group_aux (q, v) = if q = p then v else [] in 
98          let proj_group a = U.iter proj_group_aux a in
99          let proj_set (_, g) = U.iter proj_group g in
100          U.iter proj_set (eval_query c x)
101       | M.Ex (l,y) -> 
102          let rec ex_aux h = function
103             | []        -> 
104                let d = {c with groups = h} in
105                if eval_val d y = U.mql_false then () else raise Found 
106             | i :: tail -> 
107                begin
108                   try 
109                      let (_, a) = List.assoc i c.avars in 
110                      let rec add_group = function
111                         | []     -> ()
112                         | g :: t -> ex_aux ((i, g) :: h) tail; add_group t 
113                      in
114                      add_group a
115                   with Not_found -> ()
116                end
117          in
118          (try ex_aux [] l; U.mql_false with Found -> U.mql_true)
119       | M.StatVal y ->
120          let t = P.start_time () in
121          let r = (eval_val c y) in
122          let s = P.stop_time t in
123          C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
124          r
125       | M.Count y -> [string_of_int (List.length (eval_val c y))]
126       | M.Align (s,y) -> U.iter (U.align s) (eval_val c y)
127    and eval_query c = function
128       | M.Empty -> [] 
129       | M.Subj x ->
130          List.map (fun s -> (s, [])) (eval_val c x)
131       | M.Log (_,b,x) ->
132          if b then begin
133             let t = P.start_time () in
134             P.text_of_query (C.log h) "\n" x;
135             let s = P.stop_time t in
136             if C.set h C.Times then 
137                C.log h (Printf.sprintf "Log source: %s\n" s);
138             eval_query c x
139          end else begin
140             let s = (eval_query c x) in
141             let t = P.start_time () in
142             P.text_of_result (C.log h) "\n" s; 
143             let r = P.stop_time t in
144             if C.set h C.Times then 
145                C.log h (Printf.sprintf "Log: %s\n" r);
146             s
147          end
148       | M.If (y,x1,x2) ->
149          if (eval_val c y) = U.mql_false 
150             then (eval_query c x2) else (eval_query c x1)
151       | M.Bin (k,x1,x2) ->
152          let f = match k with
153             | M.BinFJoin -> U.mql_union
154             | M.BinFMeet -> U.mql_intersect
155             | M.BinFDiff -> U.mql_diff
156          in
157          f (eval_query c x1) (eval_query c x2) 
158       | M.SVar i -> begin
159          try List.assoc i c.svars 
160          with Not_found -> warn (M.SVar i); [] end  
161       | M.AVar i -> begin
162          try [List.assoc i c.avars] 
163          with Not_found -> warn (M.AVar i); [] end
164       | M.LetSVar (i,x1,x2) ->
165          let d = {c with svars = U.set (i, eval_query c x1) c.svars} in
166          eval_query d x2
167       | M.LetVVar (i,y,x) ->
168          let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in
169          eval_query d x
170       | M.For (k,i,x1,x2) ->
171          let f = match k with
172             | M.GenFJoin -> U.mql_union
173             | M.GenFMeet -> U.mql_intersect
174          in
175          let rec for_aux = function
176             | []     -> []
177             | h :: t ->
178                let d = {c with avars = U.set (i, h) c.avars} in
179                f (eval_query d x2) (for_aux t)
180          in
181          for_aux (eval_query c x1)
182       | M.Add (b,z,x) ->
183          let f = if b then U.mql_prod else U.set_union in
184          let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in
185          List.fold_right g (eval_query c x) []
186       | M.Property (q0,q1,q2,mc,ct,cfl,el,pat,y) ->
187          let subj, mct = 
188             if q0 then [], (pat, q2 @ mc, eval_val c y)
189                   else (q2 @ mc), (pat, [], eval_val c y)  
190          in
191          let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in
192          let cons_true = mct :: List.map eval_cons ct in
193          let cons_false = List.map (List.map eval_cons) cfl in
194          let eval_exp (p, po) = (q2 @ p, po) in
195          let exp = List.map eval_exp el in
196          let t = P.start_time () in
197          let r = MQIProperty.exec h q1 subj cons_true cons_false exp in 
198          let s = P.stop_time t in
199          if C.set h C.Times then 
200             C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
201          r 
202       | M.StatQuery x ->
203          let t = P.start_time () in
204          let r = (eval_query c x) in
205          let s = P.stop_time t in
206          C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
207          r
208       | M.Select (i,x,y) ->
209          let rec select_aux = function
210             | []     -> []
211             | h :: t ->
212                let d = {c with avars = U.set (i, h) c.avars} in
213                if eval_val d y = U.mql_false 
214                   then select_aux t else h :: select_aux t
215          in
216          select_aux (eval_query c x)
217       | M.Keep (b,l,x) -> 
218          let keep_path (p, v) t = 
219             if List.mem p l = b then t else (p, v) :: t in
220          let keep_grp a = List.fold_right keep_path a [] in
221          let keep_set a g = 
222             let kg = keep_grp a in
223             if kg = [] then g else kg :: g
224          in
225          let keep_av (s, g) = (s, List.fold_right keep_set g []) in
226          List.map keep_av (eval_query c x) 
227    and eval_grp c = function
228       | M.Attr gs ->
229          let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] in
230          let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
231          List.fold_left attr_auxs [] gs
232       | M.From i ->
233          try snd (List.assoc i c.avars) 
234          with Not_found -> warn (M.AVar i); []
235    in
236    let c = {svars = []; avars = []; groups = []; vvars = []} in
237    let t = P.start_time () in   
238    if C.set h C.Source then P.text_of_query (C.log h) "\n" x;
239    let r = eval_query c x in
240    if C.set h C.Result then P.text_of_result (C.log h) "\n" r;
241    let s = P.stop_time t in
242    if C.set h C.Times then 
243       C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s 
244          (C.string_of_flags (C.flags h)));
245    r